
diff -r e7504bfdbd50 -r b3add51e2e0f prio/PrioG.thy
--- a/prio/PrioG.thy	Fri Apr 13 13:12:43 2012 +0000
+++ b/prio/PrioG.thy	Sun Apr 15 21:53:12 2012 +0000
@@ -2,7 +2,6 @@
 imports PrioGDef 
 begin
 
-
 lemma runing_ready: 
   shows "runing s \<subseteq> readys s"
   unfolding runing_def readys_def
@@ -416,7 +415,26 @@
   and xz: "(x, z) \<in> r^+"
   and neq: "y \<noteq> z"
   shows "(y, z) \<in> r^+"
-by (metis neq rtranclD tranclD unique xy xz)
+proof -
+ from xz and neq show ?thesis
+ proof(induct)
+   case (base ya)
+   have "(x, ya) \<in> r" by fact
+   from unique [OF xy this] have "y = ya" .
+   with base show ?case by auto
+ next
+   case (step ya z)
+   show ?case
+   proof(cases "y = ya")
+     case True
+     from step True show ?thesis by simp
+   next
+     case False
+     from step False
+     show ?thesis by auto
+   qed
+ qed
+qed
 
 lemma unique_base:
   fixes r x y z
@@ -425,7 +443,25 @@
   and xz: "(x, z) \<in> r^+"
   and neq_yz: "y \<noteq> z"
   shows "(y, z) \<in> r^+"
-by (metis neq_yz unique unique_minus xy xz)
+proof -
+  from xz neq_yz show ?thesis
+  proof(induct)
+    case (base ya)
+    from xy unique base show ?case by auto
+  next
+    case (step ya z)
+    show ?case
+    proof(cases "y = ya")
+      case True
+      from True step show ?thesis by auto
+    next
+      case False
+      from False step 
+      have "(y, ya) \<in> r\<^sup>+" by auto
+      with step show ?thesis by auto
+    qed
+  qed
+qed
 
 lemma unique_chain:
   fixes r x y z
@@ -636,7 +672,25 @@
   "\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
   apply (unfold cs_holding_def next_th_def wq_def,
          auto simp:Let_def)
-by (metis (lifting, full_types) List.member_def distinct.simps(2) hd_in_set member_rec(2) someI_ex step_back_vt wq_def wq_distinct)
+proof -
+  fix rest
+  assume vt: "vt (V th cs # s)"
+    and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest"
+    and nrest: "rest \<noteq> []"
+    and ni: "hd (SOME q. distinct q \<and> set q = set rest)
+            \<notin> set (SOME q. distinct q \<and> set q = set rest)"
+  have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+  proof(rule someI2)
+    from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+    show "distinct rest \<and> set rest = set rest" by auto
+  next
+    fix x assume "distinct x \<and> set x = set rest"
+    hence "set x = set rest" by auto
+    with nrest
+    show "x \<noteq> []" by (case_tac x, auto)
+  qed
+  with ni show "False" by auto
+qed
 
 lemma step_v_release_inv[elim_format]:
 "\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> 
@@ -664,7 +718,61 @@
 
 lemma step_v_waiting_mono:
   "\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
-by (metis abs2 block_pre cs_waiting_def event.simps(20))
+proof -
+  fix t c
+  let ?s' = "(V th cs # s)"
+  assume vt: "vt ?s'" 
+    and wt: "waiting (wq ?s') t c"
+  show "waiting (wq s) t c"
+  proof(cases "c = cs")
+    case False
+    assume neq_cs: "c \<noteq> cs"
+    hence "waiting (wq ?s') t c = waiting (wq s) t c"
+      by (unfold cs_waiting_def wq_def, auto simp:Let_def)
+    with wt show ?thesis by simp
+  next
+    case True
+    with wt show ?thesis
+      apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits)
+    proof -
+      fix a list
+      assume not_in: "t \<notin> set list"
+        and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)"
+        and eq_wq: "wq_fun (schs s) cs = a # list"
+      have "set (SOME q. distinct q \<and> set q = set list) = set list"
+      proof(rule someI2)
+        from wq_distinct [OF step_back_vt[OF vt], of cs]
+        and eq_wq[folded wq_def]
+        show "distinct list \<and> set list = set list" by auto
+      next
+        fix x assume "distinct x \<and> set x = set list"
+        thus "set x = set list" by auto
+      qed
+      with not_in is_in show "t = a" by auto
+    next
+      fix list
+      assume is_waiting: "waiting (wq (V th cs # s)) t cs"
+      and eq_wq: "wq_fun (schs s) cs = t # list"
+      hence "t \<in> set list"
+        apply (unfold wq_def, auto simp:Let_def cs_waiting_def)
+      proof -
+        assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
+        moreover have "\<dots> = set list" 
+        proof(rule someI2)
+          from wq_distinct [OF step_back_vt[OF vt], of cs]
+            and eq_wq[folded wq_def]
+          show "distinct list \<and> set list = set list" by auto
+        next
+          fix x assume "distinct x \<and> set x = set list" 
+          thus "set x = set list" by auto
+        qed
+        ultimately show "t \<in> set list" by simp
+      qed
+      with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def]
+      show False by auto
+    qed
+  qed
+qed
 
 lemma step_depend_v:
 fixes th::thread
@@ -700,7 +808,13 @@
   fixes A
   assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
   shows "A = {} \<or> (\<exists> a. A = {a})"
-by (metis assms insertCI nonempty_iff)
+proof(cases "A = {}")
+  case True thus ?thesis by simp
+next
+  case False then obtain a where "a \<in> A" by auto
+  with h have "A = {a}" by auto
+  thus ?thesis by simp
+qed
 
 lemma depend_target_th: "(Th th, x) \<in> depend (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
   by (unfold s_depend_def, auto)
@@ -962,7 +1076,13 @@
   fixes s
   assumes vt: "vt s"
   shows "wf ((depend s)^-1)"
-by (metis acyclic_depend assms finite_acyclic_wf_converse finite_depend)
+proof(rule finite_acyclic_wf_converse)
+  from finite_depend [OF vt]
+  show "finite (depend s)" .
+next
+  from acyclic_depend[OF vt]
+  show "acyclic (depend s)" .
+qed
 
 lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
 by (induct l, auto)
@@ -1083,17 +1203,31 @@
   and eq_wq: "wq s cs = thread#rest"
   and not_in: "th \<notin>  set rest"
   shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
-using assms 
-apply (auto simp:readys_def)
-apply(simp add:s_waiting_def[folded wq_def])
-apply (erule_tac x = csa in allE)
-apply (simp add:s_waiting_def wq_def Let_def split:if_splits)
-apply (case_tac "csa = cs", simp)
-apply (erule_tac x = cs in allE)
-apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits)
-apply(auto simp add: wq_def)
-apply (auto simp:s_waiting_def wq_def Let_def split:list.splits)
-by (metis (lifting, full_types) distinct.simps(2) someI_ex wq_def wq_distinct)
+proof -
+  from assms show ?thesis
+    apply (auto simp:readys_def)
+    apply(simp add:s_waiting_def[folded wq_def])
+    apply (erule_tac x = csa in allE)
+    apply (simp add:s_waiting_def wq_def Let_def split:if_splits)
+    apply (case_tac "csa = cs", simp)
+    apply (erule_tac x = cs in allE)
+    apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits)
+    apply(auto simp add: wq_def)
+    apply (auto simp:s_waiting_def wq_def Let_def split:list.splits)
+    proof -
+       assume th_nin: "th \<notin> set rest"
+        and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
+        and eq_wq: "wq_fun (schs s) cs = thread # rest"
+      have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
+      proof(rule someI2)
+        from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
+        show "distinct rest \<and> set rest = set rest" by auto
+      next
+        show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+      qed
+      with th_nin th_in show False by auto
+    qed
+qed
 
 lemma chain_building:
   assumes vt: "vt s"
@@ -1270,8 +1404,51 @@
     apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
     apply (unfold holdents_def, unfold step_depend_v[OF vtv],
             auto simp:next_th_def)
-    apply (metis (lifting, full_types) hd_in_set hd_np_in someI_ex)
-    by (metis (lifting, full_types) hd_in_set hd_np_in someI_ex)
+  proof -
+    fix rest
+    assume dst: "distinct (rest::thread list)"
+      and ne: "rest \<noteq> []"
+    and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+    moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
+    proof(rule someI2)
+      from dst show "distinct rest \<and> set rest = set rest" by auto
+    next
+      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+    qed
+    ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> 
+                     set (SOME q. distinct q \<and> set q = set rest)" by simp
+    moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+    proof(rule someI2)
+      from dst show "distinct rest \<and> set rest = set rest" by auto
+    next
+      fix x assume " distinct x \<and> set x = set rest" with ne
+      show "x \<noteq> []" by auto
+    qed
+    ultimately 
+    show "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> depend s"
+      by auto
+  next
+    fix rest
+    assume dst: "distinct (rest::thread list)"
+      and ne: "rest \<noteq> []"
+    and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+    moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
+    proof(rule someI2)
+      from dst show "distinct rest \<and> set rest = set rest" by auto
+    next
+      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+    qed
+    ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> 
+                     set (SOME q. distinct q \<and> set q = set rest)" by simp
+    moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+    proof(rule someI2)
+      from dst show "distinct rest \<and> set rest = set rest" by auto
+    next
+      fix x assume " distinct x \<and> set x = set rest" with ne
+      show "x \<noteq> []" by auto
+    qed
+    ultimately show "False" by auto 
+  qed
   ultimately 
   have "holdents s thread = insert cs (holdents (V thread cs#s) thread)"
     by auto
@@ -1368,7 +1545,7 @@
       assume eq_e: "e = P thread cs"
         and is_runing: "thread \<in> runing s"
         and no_dep: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"
-      from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto
+      from thread_P vt stp ih  have vtp: "vt (P thread cs#s)" by auto
       show ?thesis 
       proof -
         { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -2052,8 +2229,9 @@
       with eq_th12 eq_th' have "th1 \<in> dependents (wq s) th2" by simp
       hence "(Th th1, Th th2) \<in> (depend s)^+"
         by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
-      hence "Th th1 \<in> Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"]
-        by auto
+      hence "Th th1 \<in> Domain ((depend s)^+)" 
+        apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+        by (auto simp:Domain_def)
       hence "Th th1 \<in> Domain (depend s)" by (simp add:trancl_domain)
       then obtain n where d: "(Th th1, n) \<in> depend s" by (auto simp:Domain_def)
       from depend_target_th [OF this]
@@ -2073,8 +2251,9 @@
       with th1'_in eq_th12 have "th2 \<in> dependents (wq s) th1" by simp
       hence "(Th th2, Th th1) \<in> (depend s)^+"
         by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
-      hence "Th th2 \<in> Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"]
-        by auto
+      hence "Th th2 \<in> Domain ((depend s)^+)" 
+        apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+        by (auto simp:Domain_def)
       hence "Th th2 \<in> Domain (depend s)" by (simp add:trancl_domain)
       then obtain n where d: "(Th th2, n) \<in> depend s" by (auto simp:Domain_def)
       from depend_target_th [OF this]
@@ -2131,20 +2310,106 @@
   assumes le_ij: "i \<le> j"
     and le_js: "j \<le> length s"
   shows "length (down_to j i s) = j - i"
-by (metis down_to_def le_ij le_js length_from_to_in length_rev)
+proof -
+  have "length (down_to j i s) = length (from_to i j (rev s))"
+    by (unfold down_to_def, auto)
+  also have "\<dots> = j - i"
+  proof(rule length_from_to_in[OF le_ij])
+    from le_js show "j \<le> length (rev s)" by simp
+  qed
+  finally show ?thesis .
+qed
 
 
 lemma moment_head: 
   assumes le_it: "Suc i \<le> length t"
   obtains e where "moment (Suc i) t = e#moment i t"
-by (metis assms moment_plus)
+proof -
+  have "i \<le> Suc i" by simp
+  from length_down_to_in [OF this le_it]
+  have "length (down_to (Suc i) i t) = 1" by auto
+  then obtain e where "down_to (Suc i) i t = [e]"
+    apply (cases "(down_to (Suc i) i t)") by auto
+  moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"
+    by (rule down_to_conc[symmetric], auto)
+  ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"
+    by (auto simp:down_to_moment)
+  from that [OF this] show ?thesis .
+qed
 
 lemma cnp_cnv_eq:
   fixes th s
   assumes "vt s"
   and "th \<notin> threads s"
   shows "cntP s th = cntV s th"
-by (metis (full_types) add_0_right assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
+proof -
+  from assms show ?thesis
+  proof(induct)
+    case (vt_cons s e)
+    have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact
+    have not_in: "th \<notin> threads (e # s)" by fact
+    have "step s e" by fact
+    thus ?case proof(cases)
+      case (thread_create thread prio)
+      assume eq_e: "e = Create thread prio"
+      hence "thread \<in> threads (e#s)" by simp
+      with not_in and eq_e have "th \<notin> threads s" by auto
+      from ih [OF this] show ?thesis using eq_e
+        by (auto simp:cntP_def cntV_def count_def)
+    next
+      case (thread_exit thread)
+      assume eq_e: "e = Exit thread"
+        and not_holding: "holdents s thread = {}"
+      have vt_s: "vt s" by fact
+      from finite_holding[OF vt_s] have "finite (holdents s thread)" .
+      with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
+      moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
+      moreover note cnp_cnv_cncs[OF vt_s, of thread]
+      ultimately have eq_thread: "cntP s thread = cntV s thread" by auto
+      show ?thesis
+      proof(cases "th = thread")
+        case True
+        with eq_thread eq_e show ?thesis 
+          by (auto simp:cntP_def cntV_def count_def)
+      next
+        case False
+        with not_in and eq_e have "th \<notin> threads s" by simp
+        from ih[OF this] and eq_e show ?thesis 
+           by (auto simp:cntP_def cntV_def count_def)
+      qed
+    next
+      case (thread_P thread cs)
+      assume eq_e: "e = P thread cs"
+      have "thread \<in> runing s" by fact
+      with not_in eq_e have neq_th: "thread \<noteq> th" 
+        by (auto simp:runing_def readys_def)
+      from not_in eq_e have "th \<notin> threads s" by simp
+      from ih[OF this] and neq_th and eq_e show ?thesis
+        by (auto simp:cntP_def cntV_def count_def)
+    next
+      case (thread_V thread cs)
+      assume eq_e: "e = V thread cs"
+      have "thread \<in> runing s" by fact
+      with not_in eq_e have neq_th: "thread \<noteq> th" 
+        by (auto simp:runing_def readys_def)
+      from not_in eq_e have "th \<notin> threads s" by simp
+      from ih[OF this] and neq_th and eq_e show ?thesis
+        by (auto simp:cntP_def cntV_def count_def)
+    next
+      case (thread_set thread prio)
+      assume eq_e: "e = Set thread prio"
+        and "thread \<in> runing s"
+      hence "thread \<in> threads (e#s)" 
+        by (simp add:runing_def readys_def)
+      with not_in and eq_e have "th \<notin> threads s" by auto
+      from ih [OF this] show ?thesis using eq_e
+        by (auto simp:cntP_def cntV_def count_def)  
+    qed
+  next
+    case vt_nil
+    show ?case by (auto simp:cntP_def cntV_def count_def)
+  qed
+qed
 
 lemma eq_depend: 
   "depend (wq s) = depend s"
@@ -2252,8 +2517,43 @@
 lemma le_cp:
   assumes vt: "vt s"
   shows "preced th s \<le> cp s th"
-apply(unfold cp_eq_cpreced preced_def cpreced_def, simp)
-by (metis (mono_tags) Max_ge assms dependents_threads finite_imageI finite_insert finite_threads insertI1 preced_def rev_finite_subset)
+proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
+  show "Prc (original_priority th s) (birthtime th s)
+    \<le> Max (insert (Prc (original_priority th s) (birthtime th s))
+            ((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))"
+    (is "?l \<le> Max (insert ?l ?A)")
+  proof(cases "?A = {}")
+    case False
+    have "finite ?A" (is "finite (?f ` ?B)")
+    proof -
+      have "finite ?B" 
+      proof-
+        have "finite {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}"
+        proof -
+          let ?F = "\<lambda> (x, y). the_th x"
+          have "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (wq s))\<^sup>+)"
+            apply (auto simp:image_def)
+            by (rule_tac x = "(Th x, Th th)" in bexI, auto)
+          moreover have "finite \<dots>"
+          proof -
+            from finite_depend[OF vt] have "finite (depend s)" .
+            hence "finite ((depend (wq s))\<^sup>+)"
+              apply (unfold finite_trancl)
+              by (auto simp: s_depend_def cs_depend_def wq_def)
+            thus ?thesis by auto
+          qed
+          ultimately show ?thesis by (auto intro:finite_subset)
+        qed
+        thus ?thesis by (simp add:cs_dependents_def)
+      qed
+      thus ?thesis by simp
+    qed
+    from Max_insert [OF this False, of ?l] show ?thesis by auto
+  next
+    case True
+    thus ?thesis by auto
+  qed
+qed
 
 lemma max_cp_eq: 
   assumes vt: "vt s"




