diff -r f8194fd6214f -r 031d2ae9c9b8 ExtGG.thy
--- a/ExtGG.thy	Fri Dec 18 22:47:32 2015 +0800
+++ b/ExtGG.thy	Tue Dec 22 23:13:31 2015 +0800
@@ -1,5 +1,5 @@
 theory ExtGG
-imports PrioG
+imports PrioG CpsG
 begin
 
 lemma birth_time_lt:  "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
@@ -34,44 +34,24 @@
   and highest: "preced th s = Max ((cp s)`threads s)"
   and preced_th: "preced th s = Prc prio tm"
 
+sublocale highest_gen < vat_s: valid_trace "s"
+  by (unfold_locales, insert vt_s, simp)
+
 context highest_gen
 begin
 
-
-
 lemma lt_tm: "tm < length s"
   by (insert preced_tm_lt[OF threads_s preced_th], simp)
 
-lemma eq_cp_s_th: "cp s th = preced th s"
+lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
 proof -
-  from highest and max_cp_eq[OF vt_s]
-  have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp
-  have sbs: "({th} \<union> dependants (wq s) th) \<subseteq> threads s"
-  proof -
-    from threads_s and dependants_threads[OF vt_s, of th]
-    show ?thesis by auto
-  qed
-  show ?thesis
-  proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
-    show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" by simp
-  next
-    fix y 
-    assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)"
-    then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependants (wq s) th)"
-      and eq_y: "y = preced th1 s" by auto
-    show "y \<le> preced th s"
-    proof(unfold is_max, rule Max_ge)
-      from finite_threads[OF vt_s] 
-      show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
-    next
-      from sbs th1_in and eq_y 
-      show "y \<in> (\<lambda>th. preced th s) ` threads s" by auto
-    qed
-  next
-    from sbs and finite_threads[OF vt_s]
-    show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))"
-      by (auto intro:finite_subset)
-  qed
+  have "?L \<le> ?R"
+  by (unfold highest, rule Max_ge, 
+        auto simp:threads_s finite_threads[OF vt_s])
+  moreover have "?R \<le> ?L"
+    by (unfold vat_s.cp_rec, rule Max_ge, 
+        auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)
+  ultimately show ?thesis by auto
 qed
 
 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"
@@ -117,18 +97,28 @@
   qed
 qed
 
-context extend_highest_gen
-begin
 
-thm extend_highest_gen_axioms_def
+locale red_extend_highest_gen = extend_highest_gen +
+   fixes i::nat
 
-lemma red_moment:
-  "extend_highest_gen s th prio tm (moment i t)"
+sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
   apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
   apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
   by (unfold highest_gen_def, auto dest:step_back_vt_app)
 
-lemma ind [consumes 0, case_names Nil Cons, induct type]:
+
+context extend_highest_gen
+begin
+
+(*
+ lemma red_moment:
+  "extend_highest_gen s th prio tm (moment i t)"
+  apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
+  apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
+  by (unfold highest_gen_def, auto dest:step_back_vt_app) 
+*)
+
+ lemma ind [consumes 0, case_names Nil Cons, induct type]:
   assumes 
     h0: "R []"
   and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; 
@@ -164,237 +154,195 @@
   qed
 qed
 
+
 lemma th_kept: "th \<in> threads (t @ s) \<and> 
-                 preced th (t@s) = preced th s" (is "?Q t")
+                 preced th (t@s) = preced th s" (is "?Q t") 
 proof -
   show ?thesis
   proof(induct rule:ind)
     case Nil
     from threads_s
-    show "th \<in> threads ([] @ s) \<and> preced th ([] @ s) = preced th s"
+    show ?case
       by auto
   next
     case (Cons e t)
+    interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
+    interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
     show ?case
     proof(cases e)
       case (Create thread prio)
-      assume eq_e: " e = Create thread prio"
       show ?thesis
       proof -
-        from Cons and eq_e have "step (t@s) (Create thread prio)" by auto
+        from Cons and Create have "step (t@s) (Create thread prio)" by auto
         hence "th \<noteq> thread"
         proof(cases)
-          assume "thread \<notin> threads (t @ s)"
+          case thread_create
           with Cons show ?thesis by auto
         qed
         hence "preced th ((e # t) @ s)  = preced th (t @ s)"
-          by (unfold eq_e, auto simp:preced_def)
+          by (unfold Create, auto simp:preced_def)
         moreover note Cons
         ultimately show ?thesis
-          by (auto simp:eq_e)
+          by (auto simp:Create)
       qed
     next
       case (Exit thread)
-      assume eq_e: "e = Exit thread"
-      from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-      from extend_highest_gen.exit_diff [OF this] and eq_e
+      from h_e.exit_diff and Exit
       have neq_th: "thread \<noteq> th" by auto
       with Cons
       show ?thesis
-        by (unfold eq_e, auto simp:preced_def)
+        by (unfold Exit, auto simp:preced_def)
     next
       case (P thread cs)
-      assume eq_e: "e = P thread cs"
       with Cons
       show ?thesis 
-        by (auto simp:eq_e preced_def)
+        by (auto simp:P preced_def)
     next
       case (V thread cs)
-      assume eq_e: "e = V thread cs"
       with Cons
       show ?thesis 
-        by (auto simp:eq_e preced_def)
+        by (auto simp:V preced_def)
     next
       case (Set thread prio')
-      assume eq_e: " e = Set thread prio'"
       show ?thesis
       proof -
-        from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-        from extend_highest_gen.set_diff_low[OF this] and eq_e
+        from h_e.set_diff_low and Set
         have "th \<noteq> thread" by auto
         hence "preced th ((e # t) @ s)  = preced th (t @ s)"
-          by (unfold eq_e, auto simp:preced_def)
+          by (unfold Set, auto simp:preced_def)
         moreover note Cons
         ultimately show ?thesis
-          by (auto simp:eq_e)
+          by (auto simp:Set)
       qed
     qed
   qed
 qed
 
-lemma max_kept: "Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s))) = preced th s"
+lemma Max_remove_less:
+  assumes "finite A"
+  and "a \<in> A"
+  and "b \<in> A"
+  and "a \<noteq> b"
+  and "inj_on f A"
+  and "f a = Max (f ` A)" 
+  shows "Max (f ` (A - {b})) = (Max (f ` A))"
+proof -
+  have "Max (f ` (A - {b})) = Max (f`A - {f b})"
+  proof -
+    have "f ` (A - {b}) = f ` A - f ` {b}"
+    by (rule inj_on_image_set_diff[OF assms(5)], insert assms(3), auto)
+    thus ?thesis by simp
+  qed
+  also have "... =  
+       (if f ` A - {f b} - {f a} = {} then f a else max (f a) (Max (f ` A - {f b} - {f a})))" 
+  proof(subst Max.remove)
+    from assms show "f a \<in> f ` A - {f b}"
+      by (meson DiffI empty_iff imageI inj_on_eq_iff insert_iff) 
+  next
+    from assms(1) show "finite (f ` A - {f b})" by auto
+  qed auto
+  also have "... = Max (f ` A)" (is "?L = ?R")
+  proof(cases "f ` A - {f b} - {f a} = {}")
+    case True
+    with assms show ?thesis by auto
+  next
+    case False
+    hence "?L =  max (f a) (Max (f ` A - {f b} - {f a}))" 
+      by simp
+    also have "... = ?R" 
+    proof -
+      from assms False
+      have "(Max (f ` A - {f b} - {f a})) \<le> f a" by auto
+      thus ?thesis by (simp add: assms(6) max_def) 
+    qed
+    finally show ?thesis .
+  qed
+  finally show ?thesis .
+qed
+
+lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
 proof(induct rule:ind)
   case Nil
   from highest_preced_thread
-  show "Max ((\<lambda>th'. preced th' ([] @ s)) ` threads ([] @ s)) = preced th s"
-    by simp
+  show ?case
+    by (unfold the_preced_def, simp)
 next
   case (Cons e t)
+    interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
+    interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
   show ?case
   proof(cases e)
     case (Create thread prio')
-    assume eq_e: " e = Create thread prio'"
-    from Cons and eq_e have stp: "step (t@s) (Create thread prio')" by auto
-    hence neq_thread: "thread \<noteq> th"
-    proof(cases)
-      assume "thread \<notin> threads (t @ s)"
-      moreover have "th \<in> threads (t@s)"
-      proof -
-        from Cons have "extend_highest_gen s th prio tm t" by auto
-        from extend_highest_gen.th_kept[OF this] show ?thesis by (simp)
-      qed
-      ultimately show ?thesis by auto
-    qed
-    from Cons have "extend_highest_gen s th prio tm t" by auto
-    from extend_highest_gen.th_kept[OF this]
-    have h': " th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" 
-      by (auto)
-    from stp
-    have thread_ts: "thread \<notin> threads (t @ s)"
-      by (cases, auto)
+    from Cons(2)[unfolded this] 
+    have thread_not_in: "thread \<notin> threads (t@s)" by (cases, simp)
     show ?thesis (is "Max (?f ` ?A) = ?t")
     proof -
-      have "Max (?f ` ?A) = Max(insert (?f thread) (?f ` (threads (t@s))))"
-        by (unfold eq_e, simp)
+      have "Max (?f ` ?A) = Max (insert (?f thread) (?f ` (threads (t@s))))"
+        by (unfold Create, simp)
       moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"
-      proof(rule Max_insert)
-        from Cons have "vt (t @ s)" by auto
-        from finite_threads[OF this]
+      proof(rule Max.insert)
+        from finite_threads[OF Cons(1)]
         show "finite (?f ` (threads (t@s)))" by simp
-      next
-        from h' show "(?f ` (threads (t@s))) \<noteq> {}" by auto
-      qed
-      moreover have "(Max (?f ` (threads (t@s)))) = ?t"
+      qed (insert h_t.th_kept, auto)
+      moreover have "(Max (?f ` (threads (t@s)))) = ?t" 
       proof -
         have "(\<lambda>th'. preced th' ((e # t) @ s)) ` threads (t @ s) = 
-          (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" (is "?f1 ` ?B = ?f2 ` ?B")
-        proof -
-          { fix th' 
-            assume "th' \<in> ?B"
-            with thread_ts eq_e
-            have "?f1 th' = ?f2 th'" by (auto simp:preced_def)
-          } thus ?thesis 
-            apply (auto simp:Image_def)
-          proof -
-            fix th'
-            assume h: "\<And>th'. th' \<in> threads (t @ s) \<Longrightarrow> 
-              preced th' (e # t @ s) = preced th' (t @ s)"
-              and h1: "th' \<in> threads (t @ s)"
-            show "preced th' (t @ s) \<in> (\<lambda>th'. preced th' (e # t @ s)) ` threads (t @ s)"
-            proof -
-              from h1 have "?f1 th' \<in> ?f1 ` ?B" by auto
-              moreover from h[OF h1] have "?f1 th' = ?f2 th'" by simp
-              ultimately show ?thesis by simp
-            qed
-          qed
-        qed
-        with Cons show ?thesis by auto
+                (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" 
+        by (intro f_image_eq, insert thread_not_in, auto simp:Create preced_def)
+        with Cons show ?thesis by (auto simp:the_preced_def)
       qed
       moreover have "?f thread < ?t"
       proof -
-        from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-        from extend_highest_gen.create_low[OF this] and eq_e
+        from h_e.create_low and Create
         have "prio' \<le> prio" by auto
         thus ?thesis
-        by (unfold preced_th, unfold eq_e, insert lt_tm, 
-          auto simp:preced_def precedence_less_def preced_th)
+        by (unfold preced_th, unfold Create, insert lt_tm, 
+          auto simp:preced_def precedence_less_def preced_th the_preced_def)
+     qed
+     ultimately show ?thesis by (auto simp:max_def)
     qed
-    ultimately show ?thesis by (auto simp:max_def)
-  qed
-next
+  next 
     case (Exit thread)
-    assume eq_e: "e = Exit thread"
-    from Cons have vt_e: "vt (e#(t @ s))" by auto
-    from Cons and eq_e have stp: "step (t@s) (Exit thread)" by auto
-    from stp have thread_ts: "thread \<in> threads (t @ s)"
-      by(cases, unfold runing_def readys_def, auto)
-    from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-    from extend_highest_gen.exit_diff[OF this] and eq_e
-    have neq_thread: "thread \<noteq> th" by auto
-    from Cons have "extend_highest_gen s th prio tm t" by auto
-    from extend_highest_gen.th_kept[OF this]
-    have h': "th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" .
-    show ?thesis (is "Max (?f ` ?A) = ?t")
+    show ?thesis
     proof -
-      have "threads (t@s) = insert thread ?A"
-        by (insert stp thread_ts, unfold eq_e, auto)
-      hence "Max (?f ` (threads (t@s))) = Max (?f ` \<dots>)" by simp
-      also from this have "\<dots> = Max (insert (?f thread) (?f ` ?A))" by simp
-      also have "\<dots> = max (?f thread) (Max (?f ` ?A))"
-      proof(rule Max_insert)
-        from finite_threads [OF vt_e]
-        show "finite (?f ` ?A)" by simp
+      have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = 
+            Max (the_preced (t @ s) ` (threads (t @ s)))"
+      proof(rule Max_remove_less)
+        show "th \<noteq> thread" using Exit h_e.exit_diff by auto 
+      next
+        from Cons(2)[unfolded Exit]
+        show "thread \<in> threads (t @ s)" 
+          by (cases, simp add: readys_def runing_def)
       next
-        from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-        from extend_highest_gen.th_kept[OF this]
-        show "?f ` ?A \<noteq> {}" by  auto
-      qed
-      finally have "Max (?f ` (threads (t@s))) = max (?f thread) (Max (?f ` ?A))" .
-      moreover have "Max (?f ` (threads (t@s))) = ?t"
-      proof -
-        from Cons show ?thesis
-          by (unfold eq_e, auto simp:preced_def)
+        show "finite (threads (t @ s))" by (simp add: finite_threads h_t.vt_t) 
+      next
+        show "th \<in> threads (t @ s)" by (simp add: h_t.th_kept) 
+      next
+        show "inj_on (the_preced (t @ s)) (threads (t @ s))" by (simp add: inj_the_preced) 
+      next
+        show "the_preced (t @ s) th = Max (the_preced (t @ s) ` threads (t @ s))"
+            by (simp add: Cons.hyps(5) h_t.th_kept the_preced_def)
       qed
-      ultimately have "max (?f thread) (Max (?f ` ?A)) = ?t" by simp
-      moreover have "?f thread < ?t"
-      proof(unfold eq_e, simp add:preced_def, fold preced_def)
-        show "preced thread (t @ s) < ?t"
-        proof -
-          have "preced thread (t @ s) \<le> ?t" 
-          proof -
-            from Cons
-            have "?t = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" 
-              (is "?t = Max (?g ` ?B)") by simp
-            moreover have "?g thread \<le> \<dots>"
-            proof(rule Max_ge)
-              have "vt (t@s)" by fact
-              from finite_threads [OF this]
-              show "finite (?g ` ?B)" by simp
-            next
-              from thread_ts
-              show "?g thread \<in> (?g ` ?B)" by auto
-            qed
-            ultimately show ?thesis by auto
-          qed
-          moreover have "preced thread (t @ s) \<noteq> ?t"
-          proof
-            assume "preced thread (t @ s) = preced th s"
-            with h' have "preced thread (t @ s) = preced th (t@s)" by simp
-            from preced_unique [OF this] have "thread = th"
-            proof
-              from h' show "th \<in> threads (t @ s)" by simp
-            next
-              from thread_ts show "thread \<in> threads (t @ s)" .
-            qed(simp)
-            with neq_thread show "False" by simp
-          qed
-          ultimately show ?thesis by auto
-        qed
-      qed
-      ultimately show ?thesis 
-        by (auto simp:max_def split:if_splits)
+      from this[unfolded Cons(5)]
+      have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = preced th s" .
+      moreover have "the_preced ((e # t) @ s) = the_preced (t@s)"
+                             by (auto simp:Exit the_preced_def preced_def)
+      ultimately show ?thesis by (simp add:Exit)
     qed
   next
     case (P thread cs)
     with Cons
-    show ?thesis by (auto simp:preced_def)
+    show ?thesis by (auto simp:preced_def the_preced_def)
   next
     case (V thread cs)
     with Cons
-    show ?thesis by (auto simp:preced_def)
-  next
+    show ?thesis by (auto simp:preced_def the_preced_def)
+  next (* ccc *)
     case (Set thread prio')
-    show ?thesis (is "Max (?f ` ?A) = ?t")
+    show ?thesis
+    apply (unfold Set, simp, insert Cons(5)) (* ccc *)
+    find_theorems priority Set
+    find_theorems preced Set
     proof -
       let ?B = "threads (t@s)"
       from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
@@ -964,8 +912,6 @@
 apply(auto simp add: detached_eq[OF vt_s])
 done
 
-
-
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto