(* 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\<^sup>+) \ inv_image (mult (R\<^sup>+)) mset"
by (auto simp add: lprod_implies_mult trans_trancl)
note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R\<^sup>+)" 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) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> 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) \<in> R" shows "([x, z', y], [x, y, z]) \<in> 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) =
(\<exists> f. perm f {0 ..< (length as)} \<and>
(\<forall> j. j < length as \<longrightarrow> ((nth as j, nth bs (f j)) \<in> R \<or> (nth as j = nth bs (f j)))) \<and>
(\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> 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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
