pip: comparison CpsG.thy

equal deleted inserted replaced

-:e861aff29655
+:9b9f2117561f
 theory CpsG
 imports PrioG
 begin
 lemma not_thread_holdents:
 lemma next_th_unique:
 assumes nt1: "next_th s th cs th1"
 and nt2: "next_th s th cs th2"
 shows "th1 = th2"
-proof -
+using assms by (unfold next_th_def, auto)
-from assms show ?thesis
-by (unfold next_th_def, auto)
-qed
-lemma pp_sub: "(r^+)^+ \<subseteq> r^+"
-by auto
 lemma wf_depend:
 assumes vt: "vt s"
 shows "wf (depend s)"
 proof(rule finite_acyclic_wf)
 qed
 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> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+{(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend 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:
 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"
-proof -
+using ch1 ch2
-from ch1 ch2 show ?thesis
+proof(unfold child_def, clarsimp)
-proof(unfold child_def, clarsimp)
+fix cs csa
-fix cs csa
+assume h1: "(Th th, Cs cs) \<in> depend s"
-assume h1: "(Th th, Cs cs) \<in> depend s"
+and h2: "(Cs cs, Th th1) \<in> depend s"
-and h2: "(Cs cs, Th th1) \<in> depend s"
+and h3: "(Th th, Cs csa) \<in> depend s"
-and h3: "(Th th, Cs csa) \<in> depend s"
+and h4: "(Cs csa, Th th2) \<in> depend s"
-and h4: "(Cs csa, Th th2) \<in> depend s"
+from unique_depend[OF vt h1 h3] have "cs = csa" by simp
-from unique_depend[OF vt h1 h3] have "cs = csa" by simp
+with h4 have "(Cs cs, Th th2) \<in> depend s" by simp
-with h4 have "(Cs cs, Th th2) \<in> depend s" by simp
+from unique_depend[OF vt h2 this]
-from unique_depend[OF vt h2 this]
+show "th1 = th2" by simp
-show "th1 = th2" by simp
+qed
-qed
-qed
-lemma cp_eq_cpreced_f: "cp s = cpreced (wq s) s"
-proof -
-from fun_eq_iff
-have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto
-show ?thesis
-proof(rule h)
-from cp_eq_cpreced show "\<forall>x. cp s x = cpreced (wq s) s x" by auto
-qed
-qed
 lemma depend_children:
 assumes h: "(Th th1, Th th2) \<in> (depend s)^+"
 shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)^+)"
 proof -
 by (unfold child_def, auto)
 lemma wf_child:
 assumes vt: "vt s"
 shows "wf (child s)"
-proof(rule wf_subset)
+apply(rule wf_subset)
-from wf_trancl[OF wf_depend[OF vt]]
+apply(rule wf_trancl[OF wf_depend[OF vt]])
-show "wf ((depend s)\<^sup>+)" .
+apply(rule sub_child)
-next
+done
-from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .
-qed
 lemma depend_child_pre:
 assumes vt: "vt s"
 shows
 "(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
 qed
 qed
 lemma child_depend_eq:
 assumes vt: "vt s"
-shows
+shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (depend s)^+"
-"((Th th1, Th th2) \<in> (child s)^+) =
-((Th th1, Th th2) \<in> (depend s)^+)"
 by (auto intro: depend_child[OF vt] child_depend_p)
 lemma children_no_dep:
 fixes s th th1 th2 th3
 assumes vt: "vt s"
 proof -
 from depend_child[OF vt ch3]
 have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
 thus ?thesis
 proof(rule converse_tranclE)
-thm tranclD
 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
 from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
 qed
 } thus ?thesis by auto
 qed
+lemma depend_plus_elim:
+assumes "vt s"
+fixes x
+assumes "(Th x, Th th) \<in> (depend (wq s))\<^sup>+"
+shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (depend (wq s))\<^sup>+"
+using assms(2)[unfolded eq_depend, folded child_depend_eq[OF `vt s`]]
+apply (unfold children_def)
+by (metis assms(2) children_def depend_children eq_depend)
+lemma dependants_expand_pre:
+assumes "vt s"
+shows "dependants (wq s) th = (\<Union> th' \<in> children s th. {th'} \<union> dependants (wq s) th')"
+apply (unfold cs_dependants_def)
+apply (auto elim!:depend_plus_elim[OF assms])
+apply (metis children_def eq_depend mem_Collect_eq set_mp sub_child)
+apply (unfold children_def, auto)
+apply (unfold eq_depend, fold  child_depend_eq[OF `vt s`])
+by (metis trancl.simps)
+lemma dependants_expand:
+assumes "vt s"
+shows "dependants (wq s) th = (\<Union> ((\<lambda> th. {th} \<union> dependants (wq s) th) ` (children s th)))"
+apply (subst dependants_expand_pre[OF assms])
+by simp
+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)
+lemma Max_insert:
+assumes "finite B"
+and  "B \<noteq> {}"
+shows "Max ({x} \<union> B) = max x (Max B)"
+by (metis Max_insert assms insert_is_Un)
+lemma dependands_expand2:
+assumes "vt s"
+shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
+by (subst dependants_expand[OF assms]) (auto)
+abbreviation
+"preceds s Ths \<equiv> {preced th s| th. th \<in> Ths}"
+lemma image_compr:
+"f ` A = {f x | x. x \<in> A}"
+by auto
+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
 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(unfold cp_eq_cpreced_f cpreced_def)
+proof(cases "children s th = {}")
-let ?f = "(\<lambda>th. preced th s)"
+case True
-show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
+show ?thesis
-Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th)"
+unfolding cp_eq_cpreced cpreced_def
-proof(cases " children s th = {}")
+by (subst dependants_expand[OF `vt s`]) (simp add: True)
-case False
+next
-have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th =
+case False
-{Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) | th' . th' \<in> children s th}"
+show ?thesis (is "?LHS = ?RHS")
-(is "?L = ?R")
+proof -
-by auto
+have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"
-also have "\<dots> =
+by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_compr[symmetric])
-Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) | th' . th' \<in> children s th}"
-(is "_ = Max ` ?C")
+have not_emptyness_facts[simp]:
-by auto
+"dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
-finally have "Max ?L = Max (Max ` ?C)" by auto
+using False dependands_expand2[OF assms] by(auto simp only: Un_empty)
-also have "\<dots> = Max (\<Union> ?C)"
-proof(rule Max_Union[symmetric])
+have finiteness_facts[simp]:
-from children_dependants[of s th] finite_threads[OF vt] and dependants_threads[OF vt, of th]
+"\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"
-show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
+by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])
-by (auto simp:finite_subset)
-next
+(* expanding definition *)
-from False
+have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"
-show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
+unfolding eq_cp by (simp add: Un_compr)
-by simp
-next
+(* moving Max in *)
-show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
+also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"
-finite A \<and> A \<noteq> {}"
+by (simp add: Max_Un)
-apply (auto simp:finite_subset)
-proof -
+(* expanding dependants *)
-fix th'
+also have "\<dots> = max (Max {preced th s})
-from finite_threads[OF vt] and dependants_threads[OF vt, of th']
+(Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"
-show "finite ((\<lambda>th. preced th s) ` dependants (wq s) th')" by (auto simp:finite_subset)
+by (subst dependands_expand2[OF `vt s`]) (simp)
-qed
-qed
+(* moving out big Union *)
-also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependants (wq s) th)"
+also have "\<dots> = max (Max {preced th s})
-(is "Max ?A = Max ?B")
+(Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"
-proof -
+by simp
-have "?A = ?B"
-proof
+(* moving in small union *)
-show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}
+also have "\<dots> = max (Max {preced th s})
-\<subseteq> (\<lambda>th. preced th s) ` dependants (wq s) th"
+(Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"
-proof
+by (simp add: in_disj)
-fix x
-assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
+(* moving in preceds *)
-then obtain th' where
+also have "\<dots> = max (Max {preced th s})
-th'_in: "th' \<in> children s th"
+(Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))"
-and x_in: "x \<in> ?f ` ({th'} \<union> dependants (wq s) th')" by auto
+by (simp add: UN_exists)
-hence "x = ?f th' \<or> x \<in> (?f ` dependants (wq s) th')" by auto
-thus "x \<in> ?f ` dependants (wq s) th"
+(* moving in Max *)
-proof
+also have "\<dots> = max (Max {preced th s})
-assume "x = preced th' s"
+(Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))"
-with th'_in and children_dependants
+by (subst Max_Union) (auto simp add: image_image)
-show "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th" by auto
-next
+(* folding cp + moving out Max *)
-assume "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th'"
+also have "\<dots> = ?RHS"
-moreover note th'_in
+unfolding eq_cp by (simp add: Max_insert)
-ultimately show " x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th"
-by (unfold cs_dependants_def children_def child_def, auto simp:eq_depend)
+finally show "?LHS = ?RHS" .
-qed
-qed
-next
-show "?f ` dependants (wq s) th
-\<subseteq> \<Union>{?f ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
-proof
-fix x
-assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th"
-then obtain th' where
-eq_x: "x = ?f th'" and dp: "(Th th', Th th) \<in> (depend s)^+"
-by (auto simp:cs_dependants_def eq_depend)
-from depend_children[OF dp]
-have "th' \<in> children s th \<or> (\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+)" .
-thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
-proof
-assume "th' \<in> children s th"
-with eq_x
-show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
-by auto
-next
-assume "\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+"
-then obtain th3 where th3_in: "th3 \<in> children s th"
-and dp3: "(Th th', Th th3) \<in> (depend s)\<^sup>+" by auto
-show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
-proof -
-from dp3
-have "th' \<in> dependants (wq s) th3"
-by (auto simp:cs_dependants_def eq_depend)
-with eq_x th3_in show ?thesis by auto
-qed
-qed
-qed
-qed
-thus ?thesis by simp
-qed
-finally have "Max ((\<lambda>th. preced th s) ` dependants (wq s) th) = Max (?L)"
-(is "?X = ?Y") by auto
-moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
-max (?f th) ?X"
-proof -
-have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
-Max ({?f th} \<union> ?f ` (dependants (wq s) th))" by simp
-also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependants (wq s) th)))"
-proof(rule Max_Un, auto)
-from finite_threads[OF vt] and dependants_threads[OF vt, of th]
-show "finite ((\<lambda>th. preced th s) ` dependants (wq s) th)" by (auto simp:finite_subset)
-next
-assume "dependants (wq s) th = {}"
-with False and children_dependants show False by auto
-qed
-also have "\<dots> = max (?f th) ?X" by simp
-finally show ?thesis .
-qed
-moreover have "Max ({preced th s} \<union>
-(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th) =
-max (?f th) ?Y"
-proof -
-have "Max ({preced th s} \<union>
-(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th) =
-max (Max {preced th s}) ?Y"
-proof(rule Max_Un, auto)
-from finite_threads[OF vt] dependants_threads[OF vt, of th] children_dependants [of s th]
-show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependants (wq s) th))) `
-children s th)"
-by (auto simp:finite_subset)
-next
-assume "children s th = {}"
-with False show False by auto
-qed
-thus ?thesis by simp
-qed
-ultimately show ?thesis by auto
-next
-case True
-moreover have "dependants (wq s) th = {}"
-proof -
-{ fix th'
-assume "th' \<in> dependants (wq s) th"
-hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependants_def eq_depend)
-from depend_children[OF this] and True
-have "False" by auto
-} thus ?thesis by auto
-qed
-ultimately show ?thesis by auto
 qed
 qed
 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
 where "cps s = {(th, cp s th) | th . th \<in> threads s}"
 end
 locale step_exit_cps =
 fixes s' th prio s
-defines s_def : "s \<equiv> (Exit th#s')"
+defines s_def : "s \<equiv> Exit th # s'"
 assumes vt_s: "vt s"
 context step_exit_cps
 begin

changeset 33	9b9f2117561f
parent 32	e861aff29655
child 35	92f61f6a0fe7