diff -r e861aff29655 -r 9b9f2117561f CpsG.thy
--- a/CpsG.thy	Tue May 06 14:36:40 2014 +0100
+++ b/CpsG.thy	Thu May 15 16:02:44 2014 +0100
@@ -1,3 +1,4 @@
+
 theory CpsG
 imports PrioG 
 begin
@@ -158,13 +159,7 @@
   assumes nt1: "next_th s th cs th1"
   and nt2: "next_th s th cs th2"
   shows "th1 = th2"
-proof -
-  from assms show ?thesis
-    by (unfold next_th_def, auto)
-qed
-
-lemma pp_sub: "(r^+)^+ \<subseteq> r^+"
-  by auto
+using assms by (unfold next_th_def, auto)
 
 lemma wf_depend:
   assumes vt: "vt s"
@@ -246,7 +241,7 @@
 
 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}"
@@ -263,31 +258,18 @@
   and ch1: "(Th th, Th th1) \<in> child s"
   and ch2: "(Th th, Th th2) \<in> child s"
   shows "th1 = th2"
-proof -
-  from ch1 ch2 show ?thesis
-  proof(unfold child_def, clarsimp)
-    fix cs csa
-    assume h1: "(Th th, Cs cs) \<in> depend s"
-      and h2: "(Cs cs, Th th1) \<in> depend s"
-      and h3: "(Th th, Cs csa) \<in> depend s"
-      and h4: "(Cs csa, Th th2) \<in> depend s"
-    from unique_depend[OF vt h1 h3] have "cs = csa" by simp
-    with h4 have "(Cs cs, Th th2) \<in> depend s" by simp
-    from unique_depend[OF vt h2 this]
-    show "th1 = th2" by simp
-  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
+using ch1 ch2 
+proof(unfold child_def, clarsimp)
+  fix cs csa
+  assume h1: "(Th th, Cs cs) \<in> depend s"
+    and h2: "(Cs cs, Th th1) \<in> depend s"
+    and h3: "(Th th, Cs csa) \<in> depend s"
+    and h4: "(Cs csa, Th th2) \<in> depend s"
+  from unique_depend[OF vt h1 h3] have "cs = csa" by simp
+  with h4 have "(Cs cs, Th th2) \<in> depend s" by simp
+  from unique_depend[OF vt h2 this]
+  show "th1 = th2" by simp
+qed 
 
 lemma depend_children:
   assumes h: "(Th th1, Th th2) \<in> (depend s)^+"
@@ -334,12 +316,10 @@
 lemma wf_child: 
   assumes vt: "vt s"
   shows "wf (child s)"
-proof(rule wf_subset)
-  from wf_trancl[OF wf_depend[OF vt]]
-  show "wf ((depend s)\<^sup>+)" .
-next
-  from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .
-qed
+apply(rule wf_subset)
+apply(rule wf_trancl[OF wf_depend[OF vt]])
+apply(rule sub_child)
+done
 
 lemma depend_child_pre:
   assumes vt: "vt s"
@@ -396,9 +376,7 @@
 
 lemma child_depend_eq: 
   assumes vt: "vt s"
-  shows 
-  "((Th th1, Th th2) \<in> (child s)^+) = 
-   ((Th th1, Th th2) \<in> (depend s)^+)"
+  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (depend s)^+"
   by (auto intro: depend_child[OF vt] child_depend_p)
 
 lemma children_no_dep:
@@ -413,7 +391,6 @@
   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
@@ -473,152 +450,135 @@
   } 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)
-  let ?f = "(\<lambda>th. preced th s)"
-  show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
-        Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th)"
-  proof(cases " children s th = {}")
-    case False
-    have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th = 
-          {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) | th' . th' \<in> children s th}"
-      (is "?L = ?R")
-      by auto
-    also have "\<dots> = 
-      Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) | th' . th' \<in> children s th}"
-      (is "_ = Max ` ?C")
-      by auto
-    finally have "Max ?L = Max (Max ` ?C)" by auto
-    also have "\<dots> = Max (\<Union> ?C)"
-    proof(rule Max_Union[symmetric])
-      from children_dependants[of s th] finite_threads[OF vt] and dependants_threads[OF vt, of th]
-      show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
-        by (auto simp:finite_subset)
-    next
-      from False
-      show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
-        by simp
-    next
-      show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
-        finite A \<and> A \<noteq> {}"
-        apply (auto simp:finite_subset)
-      proof -
-        fix th'
-        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)
-      qed
-    qed
-    also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependants (wq s) th)"
-      (is "Max ?A = Max ?B")
-    proof -
-      have "?A = ?B"
-      proof
-        show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}
-                    \<subseteq> (\<lambda>th. preced th s) ` dependants (wq s) th"
-        proof
-          fix x 
-          assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
-          then obtain th' where 
-             th'_in: "th' \<in> children s th"
-            and x_in: "x \<in> ?f ` ({th'} \<union> dependants (wq s) th')" by auto
-          hence "x = ?f th' \<or> x \<in> (?f ` dependants (wq s) th')" by auto
-          thus "x \<in> ?f ` dependants (wq s) th"
-          proof
-            assume "x = preced th' s"
-            with th'_in and children_dependants
-            show "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th" by auto
-          next
-            assume "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th'"
-            moreover note th'_in
-            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)
-          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
+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_compr[symmetric])
+  
+    have not_emptyness_facts[simp]: 
+      "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
+      using False dependands_expand2[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 dependands_expand2[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
 
@@ -1936,7 +1896,7 @@
 
 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