diff -r c7db2ccba18a -r 3a801bbd2687 Implementation.thy --- a/Implementation.thy Wed Feb 03 12:04:03 2016 +0800 +++ b/Implementation.thy Wed Feb 03 21:05:15 2016 +0800 @@ -376,9 +376,6 @@ context valid_trace_p_w begin -interpretation vat_e: valid_trace "e#s" - by (unfold_locales, insert vt_e, simp) - lemma cs_held: "(Cs cs, Th holder) \<in> RAG s" using holding_s_holder by (unfold s_RAG_def, fold holding_eq, auto) @@ -428,13 +425,13 @@ and "y \<in> ancestors (tRAG (e#s)) u" shows "cp_gen (e#s) y = cp_gen s y" using assms(3) -proof(induct rule:wf_induct[OF vat_e.fsbttRAGs.wf]) +proof(induct rule:wf_induct[OF vat_es.fsbttRAGs.wf]) case (1 x) show ?case (is "?L = ?R") proof - from tRAG_ancestorsE[OF 1(2)] obtain th2 where eq_x: "x = Th th2" by blast - from vat_e.cp_gen_rec[OF this] + from vat_es.cp_gen_rec[OF this] have "?L = Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" . also have "... = @@ -454,15 +451,15 @@ assume "x \<in> Range {(Th th, Th holder)}" hence eq_x: "x = Th holder" using RangeE by auto show False - proof(cases rule:vat_e.ancestors_headE[OF assms(1) start]) + proof(cases rule:vat_es.ancestors_headE[OF assms(1) start]) case 1 - from x_u[folded this, unfolded eq_x] vat_e.acyclic_tRAG + from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG show ?thesis by (auto simp:ancestors_def acyclic_def) next case 2 with x_u[unfolded eq_x] have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def) - with vat_e.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) + with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) qed qed qed @@ -473,7 +470,7 @@ assume a_in: "a \<in> ?A" from 1(2) show "?f a = ?g a" - proof(cases rule:vat_e.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) + proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) case in_ch show ?thesis proof(cases "a = u") @@ -485,7 +482,7 @@ proof assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" have "a = u" - proof(rule vat_e.rtree_s.ancestors_children_unique) + proof(rule vat_es.rtree_s.ancestors_children_unique) from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> RTree.children (tRAG (e#s)) x" by auto next @@ -519,7 +516,7 @@ proof assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" have "a = z" - proof(rule vat_e.rtree_s.ancestors_children_unique) + proof(rule vat_es.rtree_s.ancestors_children_unique) from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)" by (auto simp:ancestors_def) with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> @@ -570,9 +567,6 @@ context valid_trace_create begin -interpretation vat_e: valid_trace "e#s" - by (unfold_locales, insert vt_e, simp) - lemma tRAG_kept: "tRAG (e#s) = tRAG s" by (unfold tRAG_alt_def RAG_unchanged, auto) @@ -632,7 +626,7 @@ qed lemma eq_cp_th: "cp (e#s) th = preced th (e#s)" - by (unfold vat_e.cp_rec children_of_th, simp add:the_preced_def) + by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def) end @@ -706,4 +700,3 @@ end -