pip: comparison CpsG.thy~

equal deleted inserted replaced

-:f8194fd6214f
+:031d2ae9c9b8
 *}
 theory CpsG
 imports PrioG Max RTree
 begin
+text {* @{text "the_preced"} is also the same as @{text "preced"}, the only
+difference is the order of arguemts. *}
 definition "the_preced s th = preced th s"
+text {* @{term "the_thread"} extracts thread out of RAG node. *}
 fun the_thread :: "node \<Rightarrow> thread" where
 "the_thread (Th th) = th"
+text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}
 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"
+text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}
 definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"
-definition "tRAG s = wRAG s O hRAG s"
+text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}
-definition "cp_gen s x =
-Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
-(* ccc *)
 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
 by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
 s_holding_abv cs_RAG_def, auto)
+text {*
+The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.
+It characterizes the dependency between threads when calculating current
+precedences. It is defined as the composition of the above two sub-graphs,
+names @{term "wRAG"} and @{term "hRAG"}.
+*}
+definition "tRAG s = wRAG s O hRAG s"
+(* ccc *)
+definition "cp_gen s x =
+Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
 lemma tRAG_alt_def:
 "tRAG s = {(Th th1, Th th2) | th1 th2.
 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
 from finite_RAG[OF vt] show "finite (RAG s)" .
 next
 from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
 qed
-end
-context valid_trace
-begin
 lemma sgv_wRAG: "single_valued (wRAG s)"
 using waiting_unique[OF vt]
 by (unfold single_valued_def wRAG_def, auto)
 lemma sgv_hRAG: "single_valued (hRAG s)"
 using unique_RAG[OF vt] by (auto simp:single_valued_def)
 lemma rtree_RAG: "rtree (RAG s)"
 using sgv_RAG acyclic_RAG[OF vt]
 by (unfold rtree_def rtree_axioms_def sgv_def, auto)
 end
+sublocale valid_trace < rtree_RAG: rtree "RAG s"
+proof
+show "single_valued (RAG s)"
+apply (intro_locales)
+by (unfold single_valued_def,
+auto intro:unique_RAG[OF vt])
+show "acyclic (RAG s)"
+by (rule acyclic_RAG[OF vt])
+qed
 sublocale valid_trace < rtree_s: rtree "tRAG s"
 proof(unfold_locales)
 from sgv_tRAG show "single_valued (tRAG s)" .
 next
 have "?R = Max (insert y A)" by simp
 also from assms have "... = ?L"
 by (subst Max.insert, simp+)
 finally show ?thesis by simp
 qed
 context valid_trace
 begin
 (* ddd *)
 qed
 qed
 end
-(* ccc *)
+(* keep *)
-(* obvious lemma *)
-lemma wf_RAG:
-assumes vt: "vt s"
-shows "wf (RAG s)"
-proof(rule finite_acyclic_wf)
-from finite_RAG[OF vt] show "finite (RAG s)" .
-next
-from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
-qed
-definition child :: "state \<Rightarrow> (node \<times> node) set"
-where "child s \<equiv>
-{(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
-definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
-where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
-lemma children_def2:
-"children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
-unfolding child_def children_def by simp
-lemma children_dependants:
-"children s th \<subseteq> dependants (wq s) th"
-unfolding children_def2
-unfolding cs_dependants_def
-by (auto simp add: eq_RAG)
-lemma child_unique:
-assumes vt: "vt s"
-and ch1: "(Th th, Th th1) \<in> child s"
-and ch2: "(Th th, Th th2) \<in> child s"
-shows "th1 = th2"
-using ch1 ch2
-proof(unfold child_def, clarsimp)
-fix cs csa
-assume h1: "(Th th, Cs cs) \<in> RAG s"
-and h2: "(Cs cs, Th th1) \<in> RAG s"
-and h3: "(Th th, Cs csa) \<in> RAG s"
-and h4: "(Cs csa, Th th2) \<in> RAG s"
-from unique_RAG[OF vt h1 h3] have "cs = csa" by simp
-with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp
-from unique_RAG[OF vt h2 this]
-show "th1 = th2" by simp
-qed
-lemma RAG_children:
-assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"
-shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"
-proof -
-from h show ?thesis
-proof(induct rule: tranclE)
-fix c th2
-assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"
-and h2: "(c, Th th2) \<in> RAG s"
-from h2 obtain cs where eq_c: "c = Cs cs"
-by (case_tac c, auto simp:s_RAG_def)
-show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
-proof(rule tranclE[OF h1])
-fix ca
-assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"
-and h4: "(ca, c) \<in> RAG s"
-show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
-proof -
-from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
-by (case_tac ca, auto simp:s_RAG_def)
-from eq_ca h4 h2 eq_c
-have "th3 \<in> children s th2" by (auto simp:children_def child_def)
-moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp
-ultimately show ?thesis by auto
-qed
-next
-assume "(Th th1, c) \<in> RAG s"
-with h2 eq_c
-have "th1 \<in> children s th2"
-by (auto simp:children_def child_def)
-thus ?thesis by auto
-qed
-next
-assume "(Th th1, Th th2) \<in> RAG s"
-thus ?thesis
-by (auto simp:s_RAG_def)
-qed
-qed
-lemma sub_child: "child s \<subseteq> (RAG s)^+"
-by (unfold child_def, auto)
-lemma wf_child:
-assumes vt: "vt s"
-shows "wf (child s)"
-apply(rule wf_subset)
-apply(rule wf_trancl[OF wf_RAG[OF vt]])
-apply(rule sub_child)
-done
-lemma RAG_child_pre:
-assumes vt: "vt s"
-shows
-"(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
-proof -
-from wf_trancl[OF wf_RAG[OF vt]]
-have wf: "wf ((RAG s)^+)" .
-show ?thesis
-proof(rule wf_induct[OF wf, of ?P], clarsimp)
-fix th'
-assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>
-(Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
-and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"
-show "(Th th, Th th') \<in> (child s)\<^sup>+"
-proof -
-from RAG_children[OF h]
-have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .
-thus ?thesis
-proof
-assume "th \<in> children s th'"
-thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
-next
-assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"
-then obtain th3 where th3_in: "th3 \<in> children s th'"
-and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto
-from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)
-from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
-with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
-qed
-qed
-qed
-qed
-lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
-by (insert RAG_child_pre, auto)
-lemma child_RAG_p:
-assumes "(n1, n2) \<in> (child s)^+"
-shows "(n1, n2) \<in> (RAG s)^+"
-proof -
-from assms show ?thesis
-proof(induct)
-case (base y)
-with sub_child show ?case by auto
-next
-case (step y z)
-assume "(y, z) \<in> child s"
-with sub_child have "(y, z) \<in> (RAG s)^+" by auto
-moreover have "(n1, y) \<in> (RAG s)^+" by fact
-ultimately show ?case by auto
-qed
-qed
-text {* (* ddd *)
-*}
-lemma child_RAG_eq:
-assumes vt: "vt s"
-shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
-by (auto intro: RAG_child[OF vt] child_RAG_p)
-text {* (* ddd *)
-*}
-lemma children_no_dep:
-fixes s th th1 th2 th3
-assumes vt: "vt s"
-and ch1: "(Th th1, Th th) \<in> child s"
-and ch2: "(Th th2, Th th) \<in> child s"
-and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"
-shows "False"
-proof -
-from RAG_child[OF vt ch3]
-have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
-thus ?thesis
-proof(rule converse_tranclE)
-assume "(Th th1, Th th2) \<in> child s"
-from child_unique[OF vt ch1 this] have "th = th2" by simp
-with ch2 have "(Th th2, Th th2) \<in> child s" by simp
-with wf_child[OF vt] show ?thesis by auto
-next
-fix c
-assume h1: "(Th th1, c) \<in> child s"
-and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
-from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
-with h1 have "(Th th1, Th th3) \<in> child s" by simp
-from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
-with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
-with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
-moreover have "wf ((child s)\<^sup>+)"
-proof(rule wf_trancl)
-from wf_child[OF vt] show "wf (child s)" .
-qed
-ultimately show False by auto
-qed
-qed
-text {* (* ddd *)
-*}
-lemma unique_RAG_p:
-assumes vt: "vt s"
-and dp1: "(n, n1) \<in> (RAG s)^+"
-and dp2: "(n, n2) \<in> (RAG s)^+"
-and neq: "n1 \<noteq> n2"
-shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"
-proof(rule unique_chain [OF _ dp1 dp2 neq])
-from unique_RAG[OF vt]
-show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
-qed
-text {* (* ddd *)
-*}
-lemma dependants_child_unique:
-fixes s th th1 th2 th3
-assumes vt: "vt s"
-and ch1: "(Th th1, Th th) \<in> child s"
-and ch2: "(Th th2, Th th) \<in> child s"
-and dp1: "th3 \<in> dependants s th1"
-and dp2: "th3 \<in> dependants s th2"
-shows "th1 = th2"
-proof -
-{ assume neq: "th1 \<noteq> th2"
-from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+"
-by (simp add:s_dependants_def eq_RAG)
-from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+"
-by (simp add:s_dependants_def eq_RAG)
-from unique_RAG_p[OF vt dp1 dp2] and neq
-have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
-hence False
-proof
-assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "
-from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
-next
-assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"
-from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
-qed
-} thus ?thesis by auto
-qed
-lemma RAG_plus_elim:
-assumes "vt s"
-fixes x
-assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"
-shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
-using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
-apply (unfold children_def)
-by (metis assms(2) children_def RAG_children eq_RAG)
-text {* (* ddd *)
-*}
-lemma dependants_expand:
-assumes "vt s"
-shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
-apply(simp add: image_def)
-unfolding cs_dependants_def
-apply(auto)
-apply (metis assms RAG_plus_elim mem_Collect_eq)
-apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')
-by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)
-lemma finite_children:
-assumes "vt s"
-shows "finite (children s th)"
-using children_dependants dependants_threads[OF assms] finite_threads[OF assms]
-by (metis rev_finite_subset)
-lemma finite_dependants:
-assumes "vt s"
-shows "finite (dependants (wq s) th')"
-using dependants_threads[OF assms] finite_threads[OF assms]
-by (metis rev_finite_subset)
-abbreviation
-"preceds s ths \<equiv> {preced th s| th. th \<in> ths}"
-abbreviation
-"cpreceds s ths \<equiv> (cp s) ` ths"
-lemma Un_compr:
-"{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"
-by auto
-lemma in_disj:
-shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"
-by metis
-lemma UN_exists:
-shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
-by auto
-text {* (* ddd *)
-This is the recursive equation used to compute the current precedence of
-a thread (the @{text "th"}) here.
-*}
-lemma cp_rec:
-fixes s th
-assumes vt: "vt s"
-shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
-proof(cases "children s th = {}")
-case True
-show ?thesis
-unfolding cp_eq_cpreced cpreced_def
-by (subst dependants_expand[OF `vt s`]) (simp add: True)
-next
-case False
-show ?thesis (is "?LHS = ?RHS")
-proof -
-have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"
-by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])
-have not_emptyness_facts[simp]:
-"dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
-using False dependants_expand[OF assms] by(auto simp only: Un_empty)
-have finiteness_facts[simp]:
-"\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"
-by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])
-(* expanding definition *)
-have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"
-unfolding eq_cp by (simp add: Un_compr)
-(* moving Max in *)
-also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"
-by (simp add: Max_Un)
-(* expanding dependants *)
-also have "\<dots> = max (Max {preced th s})
-(Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"
-by (subst dependants_expand[OF `vt s`]) (simp)
-(* moving out big Union *)
-also have "\<dots> = max (Max {preced th s})
-(Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"
-by simp
-(* moving in small union *)
-also have "\<dots> = max (Max {preced th s})
-(Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"
-by (simp add: in_disj)
-(* moving in preceds *)
-also have "\<dots> = max (Max {preced th s})
-(Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))"
-by (simp add: UN_exists)
-(* moving in Max *)
-also have "\<dots> = max (Max {preced th s})
-(Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))"
-by (subst Max_Union) (auto simp add: image_image)
-(* folding cp + moving out Max *)
-also have "\<dots> = ?RHS"
-unfolding eq_cp by (simp add: Max_insert)
-finally show "?LHS = ?RHS" .
-qed
-qed
 lemma next_th_holding:
 assumes vt: "vt s"
 and nxt: "next_th s th cs th'"
 shows "holding (wq s) th cs"
 proof -
 defines s_def : "s \<equiv> (Set th prio#s')"
 -- {* @{text "s"} is assumed to be a legitimate state, from which
 the legitimacy of @{text "s"} can be derived. *}
 assumes vt_s: "vt s"
+sublocale step_set_cps < vat_s : valid_trace "s"
+proof
+from vt_s show "vt s" .
+qed
+sublocale step_set_cps < vat_s' : valid_trace "s'"
+proof
+from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
+qed
 context step_set_cps
 begin
 text {* (* ddd *)
 The following two lemmas confirm that @{text "Set"}-operating only changes the precedence
 of the initiating thread.
 *}
 lemma eq_preced:
-fixes th'
 assumes "th' \<noteq> th"
 shows "preced th' s = preced th' s'"
 proof -
 from assms show ?thesis
 by (unfold s_def, auto simp:preced_def)
 from step_back_step [OF vt_s[unfolded s_def]]
 have "step s' (Set th prio)" .
 hence "th \<in> runing s'" by (cases, simp)
 thus ?thesis by (simp add:readys_def runing_def)
 qed
-from readys_in_no_subtree[OF step_back_vt[OF vt_s[unfolded s_def]] this assms(1)]
+find_theorems readys subtree
+from vat_s'.readys_in_no_subtree[OF this assms(1)]
 show ?thesis by blast
 qed
 text {*
 By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"},
 fixes s' th cs s    -- {* @{text "s'"} is the state before operation*}
 defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}
 -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
 assumes vt_s: "vt s"
+sublocale step_v_cps < vat_s : valid_trace "s"
+proof
+from vt_s show "vt s" .
+qed
+sublocale step_v_cps < vat_s' : valid_trace "s'"
+proof
+from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
+qed
 context step_v_cps
 begin
-lemma rtree_RAGs: "rtree (RAG s)"
-proof
-show "single_valued (RAG s)"
-apply (intro_locales)
-by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
-show "acyclic (RAG s)"
-by (rule acyclic_RAG[OF vt_s])
-qed
-lemma rtree_RAGs': "rtree (RAG s')"
-proof
-show "single_valued (RAG s')"
-apply (intro_locales)
-by (unfold single_valued_def,
-auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
-show "acyclic (RAG s')"
-by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
-qed
-lemmas vt_s' = step_back_vt[OF vt_s[unfolded s_def]]
 lemma ready_th_s': "th \<in> readys s'"
 using step_back_step[OF vt_s[unfolded s_def]]
 by (cases, simp add:runing_def)
 lemma ancestors_th: "ancestors (RAG s') (Th th) = {}"
 proof -
-from readys_root[OF vt_s' ready_th_s']
+from vat_s'.readys_root[OF ready_th_s']
 show ?thesis
 by (unfold root_def, simp)
 qed
 lemma holding_th: "holding s' th cs"
 qed
 lemma ancestors_cs:
 "ancestors (RAG s') (Cs cs) = {Th th}"
 proof -
-find_theorems ancestors
 have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th)  \<union>  {Th th}"
-proof(rule RTree.rtree.ancestors_accum[OF rtree_RAGs'])
+proof(rule vat_s'.rtree_RAG.ancestors_accum)
 from vt_s[unfolded s_def]
 have " PIP s' (V th cs)" by (cases, simp)
 thus "(Cs cs, Th th) \<in> RAG s'"
 proof(cases)
 assume "holding s' th cs"
 lemma preced_kept: "the_preced s = the_preced s'"
 by (auto simp: s_def the_preced_def preced_def)
 end
 text {*
 The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation,
 which represents the case when there is another thread @{text "th'"}
 to take over the critical resource released by the initiating thread @{text "th"}.
 |
 th7 ----|
 *)
 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"
-using next_th_RAG[OF vt_s' nt] .
+using next_th_RAG[OF vat_s'.vt nt]  .
 lemma ancestors_th':
 "ancestors (RAG s') (Th th') = {Th th, Cs cs}"
 proof -
 have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}"
-proof(rule  RTree.rtree.ancestors_accum[OF rtree_RAGs'])
+proof(rule  vat_s'.rtree_RAG.ancestors_accum)
 from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto
 qed
 thus ?thesis using ancestors_th ancestors_cs by auto
 qed
 ultimately show ?thesis by auto
 qed
 lemma subtree_th:
 "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}"
-proof(unfold RAG_s, fold subtree_cs, rule RTree.rtree.subtree_del_inside[OF rtree_RAGs'])
+find_theorems "subtree" "_ - _" RAG
+proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside)
 from edge_of_th
 show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)"
 by (unfold edges_in_def, auto simp:subtree_def)
 qed
 lemma eq_cp:
 fixes th'
 shows "cp s th' = cp s' th'"
 using cp_kept_1 cp_kept_2
 by (cases "th' = th", auto)
 end
-find_theorems "_`_" "\<Union> _"
-find_theorems "Max" "\<Union> _"
-find_theorems wf RAG
-thm wf_def
-thm image_Union
 locale step_P_cps =
 fixes s' th cs s
 defines s_def : "s \<equiv> (P th cs#s')"
 assumes vt_s: "vt s"
 sublocale step_P_cps < vat_s' : valid_trace "s'"
 proof
 from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
 qed
 context step_P_cps
 begin
 lemma readys_th: "th \<in> readys s'"
 proof -
 hence "th \<in> runing s'" by (cases, simp)
 thus ?thesis by (simp add:readys_def runing_def)
 qed
 lemma root_th: "root (RAG s') (Th th)"
-using readys_root[OF vat_s'.vt readys_th] .
+using readys_root[OF readys_th] .
 lemma in_no_others_subtree:
 assumes "th' \<noteq> th"
 shows "Th th \<notin> subtree (RAG s') (Th th')"
 proof
 from ancestors_Field[OF 2(2)]
 and that show ?thesis by (unfold tRAG_alt_def, auto)
 qed auto
 have neq_th_a: "th_a \<noteq> th"
 proof -
-from readys_in_no_subtree[OF vat_s'.vt th_ready assms]
+find_theorems readys subtree s'
+from vat_s'.readys_in_no_subtree[OF th_ready assms]
 have "(Th th) \<notin> subtree (RAG s') (Th th')" .
 with tRAG_subtree_RAG[of s' "Th th'"]
 have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto
 with a_in[unfolded eq_a] show ?thesis by auto
 qed

changeset 62	031d2ae9c9b8
parent 61	f8194fd6214f
child 63	b620a2a0806a