Theory HOL-ZF.LProd

(*  Title:      HOL/ZF/LProd.thy
    Author:     Steven Obua

    Introduces the lprod relation.
    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
*)

theory LProd 
imports "HOL-Library.Multiset"
begin

inductive_set
  lprod :: "('a * 'a) set ⇒ ('a list * 'a list) set"
  for R :: "('a * 'a) set"
where
  lprod_single[intro!]: "(a, b) ∈ R ⟹ ([a], [b]) ∈ lprod R"
| lprod_list[intro!]: "(ah@at, bh@bt) ∈ lprod R ⟹ (a,b) ∈ R ∨ a = b ⟹ (ah@a#at, bh@b#bt) ∈ lprod R"

lemma "(as,bs) ∈ lprod R ⟹ length as = length bs"
  apply (induct as bs rule: lprod.induct)
  apply auto
  done

lemma "(as, bs) ∈ lprod R ⟹ 1 ≤ length as ∧ 1 ≤ length bs"
  apply (induct as bs rule: lprod.induct)
  apply auto
  done

lemma lprod_subset_elem: "(as, bs) ∈ lprod S ⟹ S ⊆ R ⟹ (as, bs) ∈ lprod R"
  apply (induct as bs rule: lprod.induct)
  apply (auto)
  done

lemma lprod_subset: "S ⊆ R ⟹ lprod S ⊆ lprod R"
  by (auto intro: lprod_subset_elem)

lemma lprod_implies_mult: "(as, bs) ∈ lprod R ⟹ trans R ⟹ (mset as, mset bs) ∈ mult R"
proof (induct as bs rule: lprod.induct)
  case (lprod_single a b)
  note step = one_step_implies_mult[
    where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified]    
  show ?case by (auto intro: lprod_single step)
next
  case (lprod_list ah at bh bt a b)
  then have transR: "trans R" by auto
  have as: "mset (ah @ a # at) = mset (ah @ at) + {#a#}" (is "_ = ?ma + _")
    by (simp add: algebra_simps)
  have bs: "mset (bh @ b # bt) = mset (bh @ bt) + {#b#}" (is "_ = ?mb + _")
    by (simp add: algebra_simps)
  from lprod_list have "(?ma, ?mb) ∈ mult R"
    by auto
  with mult_implies_one_step[OF transR] have 
    "∃I J K. ?mb = I + J ∧ ?ma = I + K ∧ J ≠ {#} ∧ (∀k∈set_mset K. ∃j∈set_mset J. (k, j) ∈ R)"
    by blast
  then obtain I J K where 
    decomposed: "?mb = I + J ∧ ?ma = I + K ∧ J ≠ {#} ∧ (∀k∈set_mset K. ∃j∈set_mset J. (k, j) ∈ R)"
    by blast   
  show ?case
  proof (cases "a = b")
    case True    
    have "((I + {#b#}) + K, (I + {#b#}) + J) ∈ mult R"
      apply (rule one_step_implies_mult)
      apply (auto simp add: decomposed)
      done
    then show ?thesis
      apply (simp only: as bs)
      apply (simp only: decomposed True)
      apply (simp add: algebra_simps)
      done
  next
    case False
    from False lprod_list have False: "(a, b) ∈ R" by blast
    have "(I + (K + {#a#}), I + (J + {#b#})) ∈ mult R"
      apply (rule one_step_implies_mult)
      apply (auto simp add: False decomposed)
      done
    then show ?thesis
      apply (simp only: as bs)
      apply (simp only: decomposed)
      apply (simp add: algebra_simps)
      done
  qed
qed

lemma wf_lprod[simp,intro]:
  assumes wf_R: "wf R"
  shows "wf (lprod R)"
proof -
  have subset: "lprod (R⇧+) ⊆ inv_image (mult (R⇧+)) mset"
    by (auto simp add: lprod_implies_mult trans_trancl)
  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R⇧+)" and f="mset", 
    OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
  note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
  show ?thesis by (auto intro: lprod)
qed

definition gprod_2_2 :: "('a * 'a) set ⇒ (('a * 'a) * ('a * 'a)) set" where
  "gprod_2_2 R ≡ { ((a,b), (c,d)) . (a = c ∧ (b,d) ∈ R) ∨ (b = d ∧ (a,c) ∈ R) }"

definition gprod_2_1 :: "('a * 'a) set ⇒ (('a * 'a) * ('a * 'a)) set" where
  "gprod_2_1 R ≡  { ((a,b), (c,d)) . (a = d ∧ (b,c) ∈ R) ∨ (b = c ∧ (a,d) ∈ R) }"

lemma lprod_2_3: "(a, b) ∈ R ⟹ ([a, c], [b, c]) ∈ lprod R"
  by (auto intro: lprod_list[where a=c and b=c and 
    ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) 

lemma lprod_2_4: "(a, b) ∈ R ⟹ ([c, a], [c, b]) ∈ lprod R"
  by (auto intro: lprod_list[where a=c and b=c and 
    ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified])

lemma lprod_2_1: "(a, b) ∈ R ⟹ ([c, a], [b, c]) ∈ lprod R"
  by (auto intro: lprod_list[where a=c and b=c and 
    ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified]) 

lemma lprod_2_2: "(a, b) ∈ R ⟹ ([a, c], [c, b]) ∈ lprod R"
  by (auto intro: lprod_list[where a=c and b=c and 
    ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])

lemma [simp, intro]:
  assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
proof -
  have "gprod_2_1 R ⊆ inv_image (lprod R) (λ (a,b). [a,b])"
    by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2)
  with wfR show ?thesis
    by (rule_tac wf_subset, auto)
qed

lemma [simp, intro]:
  assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
proof -
  have "gprod_2_2 R ⊆ inv_image (lprod R) (λ (a,b). [a,b])"
    by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4)
  with wfR show ?thesis
    by (rule_tac wf_subset, auto)
qed

lemma lprod_3_1: assumes "(x', x) ∈ R" shows "([y, z, x'], [x, y, z]) ∈ lprod R"
  apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
  apply (auto simp add: lprod_2_1 assms)
  done

lemma lprod_3_2: assumes "(z',z) ∈ R" shows "([z', x, y], [x,y,z]) ∈ lprod R"
  apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
  apply (auto simp add: lprod_2_2 assms)
  done

lemma lprod_3_3: assumes xr: "(xr, x) ∈ R" shows "([xr, y, z], [x, y, z]) ∈ lprod R"
  apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified])
  apply (simp add: xr lprod_2_3)
  done

lemma lprod_3_4: assumes yr: "(yr, y) ∈ R" shows "([x, yr, z], [x, y, z]) ∈ lprod R"
  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified])
  apply (simp add: yr lprod_2_3)
  done

lemma lprod_3_5: assumes zr: "(zr, z) ∈ R" shows "([x, y, zr], [x, y, z]) ∈ lprod R"
  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified])
  apply (simp add: zr lprod_2_4)
  done

lemma lprod_3_6: assumes y': "(y', y) ∈ R" shows "([x, z, y'], [x, y, z]) ∈ lprod R"
  apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified])
  apply (simp add: y' lprod_2_4)
  done

lemma lprod_3_7: assumes z': "(z',z) ∈ R" shows "([x, z', y], [x, y, z]) ∈ lprod R"
  apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified])
  apply (simp add: z' lprod_2_4)
  done

definition perm :: "('a ⇒ 'a) ⇒ 'a set ⇒ bool" where
   "perm f A ≡ inj_on f A ∧ f ` A = A"

lemma "((as,bs) ∈ lprod R) = 
  (∃ f. perm f {0 ..< (length as)} ∧ 
  (∀ j. j < length as ⟶ ((nth as j, nth bs (f j)) ∈ R ∨ (nth as j = nth bs (f j)))) ∧ 
  (∃ i. i < length as ∧ (nth as i, nth bs (f i)) ∈ R))"
oops

lemma "trans R ⟹ (ah@a#at, bh@b#bt) ∈ lprod R ⟹ (b, a) ∈ R ∨ a = b ⟹ (ah@at, bh@bt) ∈ lprod R" 
oops

end