--- a/CpsG.thy Tue Dec 15 21:45:46 2015 +0800
+++ b/CpsG.thy Tue Dec 15 15:10:40 2015 +0000
@@ -1842,6 +1842,7 @@
Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" .
also have "... =
Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"
+
proof -
from preced_kept have "the_preced s th2 = the_preced s' th2" by simp
moreover have "cp_gen s ` RTree.children (tRAG s) x =
@@ -2000,7 +2001,6 @@
by (insert eq_child_left[OF nd] eq_child_right, auto)
lemma eq_cp:
- fixes th'
assumes nd: "th \<notin> dependants s th'"
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
@@ -2048,7 +2048,6 @@
qed
lemma eq_up:
- fixes th' th''
assumes dp1: "th \<in> dependants s th'"
and dp2: "th' \<in> dependants s th''"
and eq_cps: "cp s th' = cp s' th'"
--- a/CpsG.thy~ Tue Dec 15 21:45:46 2015 +0800
+++ b/CpsG.thy~ Tue Dec 15 15:10:40 2015 +0000
@@ -1843,7 +1843,7 @@
also have "... =
Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"
proof -
- have "the_preced s th2 = the_preced s' th2" sorry
+ from preced_kept have "the_preced s th2 = the_preced s' th2" by simp
moreover have "cp_gen s ` RTree.children (tRAG s) x =
cp_gen s' ` RTree.children (tRAG s') x"
proof -
@@ -1871,52 +1871,58 @@
qed
moreover have "cp_gen s ` RTree.children (tRAG s) x =
cp_gen s' ` RTree.children (tRAG s) x" (is "?f ` ?A = ?g ` ?A")
- proof -
- have h: "?A = ({y. y \<in> ?A \<and> y \<in> ancestors (tRAG s) u} \<union>
- {y. y \<in> ?A \<and> \<not> (y \<in> ancestors (tRAG s) u)})" (is "_ = ?B \<union> ?C")
- by (rule set_prop_split)
- show ?thesis
- proof(subst h, subst (3) h, rule f_image_union_eq)
- show "?f ` ?B = ?g ` ?B"
- proof(rule f_image_eq)
- fix a
- assume "a \<in> ?B"
- hence h: "a \<in> RTree.children (tRAG s) x" "a \<in> ancestors (tRAG s) u" by auto
- show "?f a = ?g a"
- proof(rule 1(1)[rule_format])
- from h(2) show "a \<in> ancestors (tRAG s) u" .
- next
- from h(1) show "(a, x) \<in> tRAG s"
- unfolding RTree.children_def by auto
- qed
- qed
+ proof(rule f_image_eq)
+ fix a
+ assume a_in: "a \<in> ?A"
+ from 1(2)
+ show "?f a = ?g a"
+ proof(cases rule:vat_s.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
+ case in_ch
+ show ?thesis
+ proof(cases "a = u")
+ case True
+ from assms(2)[folded this] show ?thesis .
+ next
+ case False
+ have a_not_in: "a \<notin> ancestors (tRAG s) (Th th)"
+ proof
+ assume a_in': "a \<in> ancestors (tRAG s) (Th th)"
+ have "a = u"
+ proof(rule vat_s.rtree_s.ancestors_children_unique)
+ from a_in' a_in show "a \<in> ancestors (tRAG s) (Th th) \<inter>
+ RTree.children (tRAG s) x" by auto
+ next
+ from assms(1) in_ch show "u \<in> ancestors (tRAG s) (Th th) \<inter>
+ RTree.children (tRAG s) x" by auto
+ qed
+ with False show False by simp
+ qed
+ from a_in obtain th_a where eq_a: "a = Th th_a"
+ by (unfold RTree.children_def tRAG_alt_def, auto)
+ from cp_kept[OF a_not_in[unfolded eq_a]]
+ have "cp s th_a = cp s' th_a" .
+ from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
+ show ?thesis .
+ qed
next
- show "?f ` ?C = ?g ` ?C"
- proof(rule f_image_eq)
- fix a
- assume "a \<in> ?C"
- hence h: "a \<in> RTree.children (tRAG s) x" "a \<notin> ancestors (tRAG s) u" by auto
- from h(1) obtain th3 where eq_a: "a = Th th3"
- by (unfold RTree.children_def tRAG_alt_def, auto)
- thm cp_gen_def_cond[OF eq_a, folded eq_a]
- show "?f a = ?g a"
- proof(fold cp_gen_def_cond[OF eq_a, folded eq_a], rule cp_kept)
- show "Th th3 \<notin> ancestors (tRAG s) (Th th)"
- proof
- assume "Th th3 \<in> ancestors (tRAG s) (Th th)"
- from this[folded eq_a] have "(Th th, a) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
- from plus_rpath[OF this] obtain xs1
- where h_a: "rpath (tRAG s) (Th th) xs1 a" "xs1 \<noteq> []" by auto
- from assms(1) have "(Th th, u) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
- from plus_rpath[OF this] obtain xs2
- where h_u: "rpath (tRAG s) (Th th) xs2 u" "xs2 \<noteq> []" by auto
- show False
- proof(cases rule:vat_s.rtree_s.rpath_overlap[OF h_a(1) h_u(1)])
- case (1 xs3)
- (* ccc *)
- qed
- qed
- qed
+ case (out_ch z)
+ hence h: "z \<in> ancestors (tRAG s) u" "z \<in> RTree.children (tRAG s) x" by auto
+ show ?thesis
+ proof(cases "a = z")
+ case True
+ from h(2) have zx_in: "(z, x) \<in> (tRAG s)" by (auto simp:RTree.children_def)
+ from 1(1)[rule_format, OF this h(1)]
+ have eq_cp_gen: "cp_gen s z = cp_gen s' z" .
+ with True show ?thesis by metis
+ next
+ case False
+ from a_in obtain th_a where eq_a: "a = Th th_a"
+ by (auto simp:RTree.children_def tRAG_alt_def)
+ have "a \<notin> ancestors (tRAG s) (Th th)" sorry
+ from cp_kept[OF this[unfolded eq_a]]
+ have "cp s th_a = cp s' th_a" .
+ from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
+ show ?thesis .
qed
qed
qed
--- a/ROOT Tue Dec 15 21:45:46 2015 +0800
+++ b/ROOT Tue Dec 15 15:10:40 2015 +0000
@@ -1,5 +1,5 @@
session "PIP" = HOL +
- theories [document = false]
+ theories [document = false, quick_and_dirty]
"CpsG"
"ExtGG"
"Test"