# HG changeset patch
# User urbanc
# Date 1330434812 0
# Node ID f9e0d3274c14473fdba2c3a6126aeca592a7e310
# Parent  7fe2a20017c0fef87b59a2150af57601c4d6e8b3
fixed typo

diff -r 7fe2a20017c0 -r f9e0d3274c14 prio/CpsG.thy
--- a/prio/CpsG.thy	Mon Feb 27 18:53:53 2012 +0000
+++ b/prio/CpsG.thy	Tue Feb 28 13:13:32 2012 +0000
@@ -2,6 +2,7 @@
 imports PrioG 
 begin
 
+
 lemma not_thread_holdents:
   fixes th s
   assumes vt: "vt s"
diff -r 7fe2a20017c0 -r f9e0d3274c14 prio/Moment.thy
--- a/prio/Moment.thy	Mon Feb 27 18:53:53 2012 +0000
+++ b/prio/Moment.thy	Tue Feb 28 13:13:32 2012 +0000
@@ -112,37 +112,12 @@
 qed
 
 lemma moment_restm_s: "(restm n s)@(moment n s) = s"
-proof -
-  have " rev  ((firstn n (rev s)) @ (restn n (rev s))) = s" (is "rev ?x = s")
-  proof -
-    have "?x = rev s" by (simp only:firstn_restn_s)
-    thus ?thesis by auto
-  qed
-  thus ?thesis 
-    by (auto simp:restm_def moment_def)
-qed
+by (metis firstn_restn_s moment_def restm_def rev_append rev_rev_ident)
 
 declare restn.simps [simp del] firstn.simps[simp del]
 
 lemma length_firstn_ge: "length s \<le> n \<Longrightarrow> length (firstn n s) = length s"
-proof(induct n arbitrary:s, simp add:firstn.simps)
-  case (Suc k)
-  assume ih: "\<And> s. length (s::'a list) \<le> k \<Longrightarrow> length (firstn k s) = length s"
-  and le: "length s \<le> Suc k"
-  show ?case
-  proof(cases s)
-    case Nil
-    from Nil show ?thesis by simp
-  next
-    case (Cons x xs)
-    from le and Cons have "length xs \<le> k" by simp
-    from ih [OF this] have "length (firstn k xs) = length xs" .
-    moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" 
-      by (simp add:firstn.simps)
-    moreover note Cons
-    ultimately show ?thesis by simp
-  qed
-qed
+by (metis firstn_ge)
 
 lemma length_firstn_le: "n \<le> length s \<Longrightarrow> length (firstn n s) = n"
 proof(induct n arbitrary:s, simp add:firstn.simps)
@@ -166,78 +141,26 @@
 lemma app_firstn_restn: 
   fixes s1 s2
   shows "s1 = firstn (length s1) (s1 @ s2) \<and> s2 = restn (length s1) (s1 @ s2)"
-proof(rule length_eq_elim_l)
-  have "length s1 \<le> length (s1 @ s2)" by simp
-  from length_firstn_le [OF this]
-  show "length s1 = length (firstn (length s1) (s1 @ s2))" by simp
-next
-  from firstn_restn_s 
-  show "s1 @ s2 = firstn (length s1) (s1 @ s2) @ restn (length s1) (s1 @ s2)"
-    by metis
-qed
-
-
+by (metis append_eq_conv_conj firstn_ge firstn_le firstn_restn_s le_refl)
 lemma length_moment_le:
   fixes k s
   assumes le_k: "k \<le> length s"
   shows "length (moment k s) = k"
-proof -
-  have "length (rev (firstn k (rev s))) = k"
-  proof -
-    have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp
-    also have "\<dots> = k" 
-    proof(rule length_firstn_le)
-      from le_k show "k \<le> length (rev s)" by simp
-    qed
-    finally show ?thesis .
-  qed
-  thus ?thesis by (simp add:moment_def)
-qed
+by (metis assms length_firstn_le length_rev moment_def)
 
 lemma app_moment_restm: 
   fixes s1 s2
   shows "s1 = restm (length s2) (s1 @ s2) \<and> s2 = moment (length s2) (s1 @ s2)"
-proof(rule length_eq_elim_r)
-  have "length s2 \<le> length (s1 @ s2)" by simp
-  from length_moment_le [OF this]
-  show "length s2 = length (moment (length s2) (s1 @ s2))" by simp
-next
-  from moment_restm_s 
-  show "s1 @ s2 = restm (length s2) (s1 @ s2) @ moment (length s2) (s1 @ s2)"
-    by metis
-qed
+by (metis app_firstn_restn length_rev moment_def restm_def rev_append rev_rev_ident)
 
 lemma length_moment_ge:
   fixes k s
   assumes le_k: "length s \<le> k"
   shows "length (moment k s) = (length s)"
-proof -
-  have "length (rev (firstn k (rev s))) = length s"
-  proof -
-    have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp
-    also have "\<dots> = length s" 
-    proof -
-      have "\<dots> = length (rev s)"
-      proof(rule length_firstn_ge)
-        from le_k show "length (rev s) \<le> k" by simp
-      qed
-      also have "\<dots> = length s" by simp
-      finally show ?thesis .
-    qed
-    finally show ?thesis .
-  qed
-  thus ?thesis by (simp add:moment_def)
-qed
+by (metis assms firstn_ge length_rev moment_def)
 
 lemma length_firstn: "(length (firstn n s) = length s) \<or> (length (firstn n s) = n)"
-proof(cases "n \<le> length s")
-  case True
-  from length_firstn_le [OF True] show ?thesis by auto
-next
-  case False
-  from False have "length s \<le> n" by simp
-  from firstn_ge [OF this] show ?thesis by auto
-qed
+by (metis length_firstn_ge length_firstn_le nat_le_linear)
 
 lemma firstn_conc: 
   fixes m n
@@ -270,45 +193,7 @@
   fixes i j k s
   assumes eq_k: "j + i = k"
   shows "restn k s = restn j (restn i s)"
-proof -
-  have "(firstn (length s - k) (rev s)) =
-        (firstn (length (rev (firstn (length s - i) (rev s))) - j) 
-                            (rev (rev (firstn (length s - i) (rev s)))))"
-  proof  -
-    have "(firstn (length s - k) (rev s)) =
-            (firstn (length (rev (firstn (length s - i) (rev s))) - j) 
-                                           (firstn (length s - i) (rev s)))"
-    proof -
-      have " (length (rev (firstn (length s - i) (rev s))) - j) = length s - k"
-      proof -
-        have "(length (rev (firstn (length s - i) (rev s))) - j) = (length s - i) - j"
-        proof -
-          have "(length (rev (firstn (length s - i) (rev s))) - j) = 
-                                         length ((firstn (length s - i) (rev s))) - j"
-            by simp
-          also have "\<dots> = length ((firstn (length (rev s) - i) (rev s))) - j" by simp
-          also have "\<dots> = (length (rev s) - i) - j" 
-          proof -
-            have "length ((firstn (length (rev s) - i) (rev s))) = (length (rev s) - i)"
-              by (rule length_firstn_le, simp)
-            thus ?thesis by simp
-          qed
-          also have "\<dots> = (length s - i) - j" by simp
-          finally show ?thesis .
-        qed
-        with eq_k show ?thesis by auto
-      qed
-      moreover have "(firstn (length s - k) (rev s)) =
-                             (firstn (length s - k) (firstn (length s - i) (rev s)))"
-      proof(rule firstn_conc)
-        from eq_k show "length s - k \<le> length s - i" by simp
-      qed
-      ultimately show ?thesis by simp
-    qed
-    thus ?thesis by simp
-  qed
-  thus ?thesis by (simp only:restn.simps)
-qed
+by (metis app_moment_restm append_take_drop_id assms drop_drop length_drop moment_def restn.simps)
 
 (*
 value "down_to 2 0 [5, 4, 3, 2, 1, 0]"
@@ -319,28 +204,12 @@
 by (simp add:from_to_def restn.simps)
 
 lemma moment_app [simp]:
-  assumes 
-  ile: "i \<le> length s"
+  assumes ile: "i \<le> length s"
   shows "moment i (s'@s) = moment i s"
-proof -
-  have "moment i (s'@s) = rev (firstn i (rev (s'@s)))" by (simp add:moment_def)
-  moreover have "firstn i (rev (s'@s)) = firstn i (rev s @ rev s')" by simp
-  moreover have "\<dots> = firstn i (rev s)"
-  proof(rule firstn_le)
-    have "length (rev s) = length s" by simp
-    with ile show "i \<le> length (rev s)" by simp
-  qed
-  ultimately show ?thesis by (simp add:moment_def)
-qed
+by (metis assms firstn_le length_rev moment_def rev_append)
 
 lemma moment_eq [simp]: "moment (length s) (s'@s) = s"
-proof -
-  have "length s \<le> length s" by simp
-  from moment_app [OF this, of s'] 
-  have " moment (length s) (s' @ s) = moment (length s) s" .
-  moreover have "\<dots> = s" by (simp add:moment_def)
-  ultimately show ?thesis by simp
-qed
+by (metis app_moment_restm)
 
 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s"
   by (unfold moment_def, simp)
@@ -534,42 +403,16 @@
   assumes le_ij: "i \<le> j"
   and le_jk: "j \<le> k"
   shows "down_to k j s @ down_to j i s = down_to k i s"
-proof -
-  have "rev (from_to j k (rev s)) @ rev (from_to i j (rev s)) = rev (from_to i k (rev s))"
-    (is "?L = ?R")
-  proof -
-    have "?L = rev (from_to i j (rev s) @ from_to j k (rev s))" by simp
-    also have "\<dots> = ?R" (is "rev ?x = rev ?y")
-    proof -
-      have "?x = ?y" by (rule from_to_conc[OF le_ij le_jk])
-      thus ?thesis by simp
-    qed
-    finally show ?thesis .
-  qed
-  thus ?thesis by (simp add:down_to_def)
-qed
+by (metis down_to_def from_to_conc le_ij le_jk rev_append)
 
 lemma restn_ge:
   fixes s k
   assumes le_k: "length s \<le> k"
   shows "restn k s = []"
-proof -
-  from firstn_restn_s [of k s, symmetric] have "s = (firstn k s) @ (restn k s)" .
-  hence "length s = length \<dots>" by simp
-  also have "\<dots> = length (firstn k s) + length (restn k s)" by simp
-  finally have "length s = ..." by simp
-  moreover from length_firstn_ge and le_k 
-  have "length (firstn k s) = length s" by simp
-  ultimately have "length (restn k s) = 0" by auto
-  thus ?thesis by auto
-qed
+by (metis assms diff_is_0_eq moment_def moment_zero restn.simps)
 
 lemma from_to_ge: "length s \<le> k \<Longrightarrow> from_to k j s = []"
-proof(simp only:from_to_def)
-  assume "length s \<le> k"
-  from restn_ge [OF this] 
-  show "firstn (j - k) (restn k s) = []" by simp
-qed
+by (metis firstn_nil from_to_def restn_ge)
 
 (*
 value "from_to 2 5 [0, 1, 2, 3, 4]"
@@ -580,166 +423,31 @@
   fixes k j s
   assumes le_j: "length s \<le> j"
   shows "from_to k j s = restn k s"
-proof -
-  have "from_to 0 k s @ from_to k j s = from_to 0 j s"
-  proof(cases "k \<le> j")
-    case True
-    from from_to_conc True show ?thesis by auto
-  next
-    case False
-    from False le_j have lek: "length s \<le>  k" by auto
-    from from_to_ge [OF this] have "from_to k j s = []" .
-    hence "from_to 0 k s @ from_to k j s = from_to 0 k s" by simp
-    also have "\<dots> = s"
-    proof -
-      from from_to_firstn [of k s]
-      have "\<dots> = firstn k s" .
-      also have "\<dots> = s" by (rule firstn_ge [OF lek])
-      finally show ?thesis .
-    qed
-    finally have "from_to 0 k s @ from_to k j s = s" .
-    moreover have "from_to 0 j s = s"
-    proof -
-      have "from_to 0 j s = firstn j s" by (simp add:from_to_firstn)
-      also have "\<dots> = s"
-      proof(rule firstn_ge)
-        from le_j show "length s \<le> j " by simp
-      qed
-      finally show ?thesis .
-    qed
-    ultimately show ?thesis by auto
-  qed
-  also have "\<dots> = s" 
-  proof -
-    from from_to_firstn have "\<dots> = firstn j s" .
-    also have "\<dots> = s"
-    proof(rule firstn_ge)
-      from le_j show "length s \<le> j" by simp
-    qed
-    finally show ?thesis .
-  qed
-  finally have "from_to 0 k s @ from_to k j s = s" .
-  moreover have "from_to 0 k s @ restn k s = s"
-  proof -
-    from from_to_firstn [of k s]
-    have "from_to 0 k s = firstn k s" .
-    thus ?thesis by (simp add:firstn_restn_s)
-  qed
-  ultimately have "from_to 0 k s @ from_to k j s  = 
-                    from_to 0 k s @ restn k s" by simp
-  thus ?thesis by auto
-qed
+by (metis app_moment_restm append_Nil2 append_take_drop_id assms diff_is_0_eq' drop_take firstn_restn_s from_to_def length_drop moment_def moment_zero restn.simps)
 
 lemma down_to_moment: "down_to k 0 s = moment k s"
-proof -
-  have "rev (from_to 0 k (rev s)) = rev (firstn k (rev s))" 
-    using from_to_firstn by metis
-  thus ?thesis by (simp add:down_to_def moment_def)
-qed
+by (metis down_to_def from_to_firstn moment_def)
 
 lemma down_to_restm:
   assumes le_s: "length s \<le> j"
   shows "down_to j k s = restm k s"
-proof -
-  have "rev (from_to k j (rev s)) = rev (restn k (rev s))" (is "?L = ?R")
-  proof -
-    from le_s have "length (rev s) \<le> j" by simp
-    from from_to_restn [OF this, of k] show ?thesis by simp
-  qed
-  thus ?thesis by (simp add:down_to_def restm_def)
-qed
+by (metis assms down_to_def from_to_restn length_rev restm_def)
 
 lemma moment_split: "moment (m+i) s = down_to (m+i) i s @down_to i 0 s"
-proof -
-  have "moment (m + i) s = down_to (m+i) 0 s" using down_to_moment by metis
-  also have "\<dots> = (down_to (m+i) i s) @ (down_to i 0 s)" 
-    by(rule down_to_conc[symmetric], auto)
-  finally show ?thesis .
-qed
+by (metis down_to_conc down_to_moment le0 le_add1 nat_add_commute)
 
 lemma length_restn: "length (restn i s) = length s - i"
-proof(cases "i \<le> length s")
-  case True
-  from length_firstn_le [OF this] have "length (firstn i s) = i" .
-  moreover have "length s = length (firstn i s) + length (restn i s)"
-  proof -
-    have "s = firstn i s @ restn i s" using firstn_restn_s by metis
-    hence "length s = length \<dots>" by simp
-    thus ?thesis by simp
-  qed
-  ultimately show ?thesis by simp
-next 
-  case False
-  hence "length s \<le> i" by simp
-  from restn_ge [OF this] have "restn i s = []" .
-  with False show ?thesis by simp
-qed
+by (metis diff_le_self length_firstn_le length_rev restn.simps)
 
 lemma length_from_to_in:
   fixes i j s
   assumes le_ij: "i \<le> j"
   and le_j: "j \<le> length s"
   shows "length (from_to i j s) = j - i"
-proof -
-  have "from_to 0 j s = from_to 0 i s @ from_to i j s"
-    by (rule from_to_conc[symmetric, OF _ le_ij], simp)
-  moreover have "length (from_to 0 j s) = j"
-  proof -
-    have "from_to 0 j s = firstn j s" using from_to_firstn by metis
-    moreover have "length \<dots> = j" by (rule length_firstn_le [OF le_j])
-    ultimately show ?thesis by simp
-  qed
-  moreover have "length (from_to 0 i s) = i"
-  proof -
-    have "from_to 0 i s = firstn i s" using from_to_firstn by metis
-    moreover have "length \<dots> = i" 
-    proof (rule length_firstn_le)
-      from le_ij le_j show "i \<le> length s" by simp
-    qed
-    ultimately show ?thesis by simp
-  qed
-  ultimately show ?thesis by auto
-qed
+by (metis diff_le_mono from_to_def le_j length_firstn_le length_restn)
 
 lemma firstn_restn_from_to: "from_to i (m + i) s = firstn m (restn i s)"
-proof(cases "m+i \<le> length s")
-  case True
-  have "restn i s = from_to i (m+i) s @ from_to (m+i) (length s) s"
-  proof -
-    have "restn i s = from_to i (length s) s"
-      by(rule from_to_restn[symmetric], simp)
-    also have "\<dots> = from_to i (m+i) s @ from_to (m+i) (length s) s"
-      by(rule from_to_conc[symmetric, OF _ True], simp)
-    finally show ?thesis .
-  qed
-  hence "firstn m (restn i s) = firstn m \<dots>" by simp
-  moreover have "\<dots> = firstn (length (from_to i (m+i) s)) 
-                    (from_to i (m+i) s @ from_to (m+i) (length s) s)"
-  proof -
-    have "length (from_to i (m+i) s) = m"
-    proof -
-      have "length (from_to i (m+i) s) = (m+i) - i"
-        by(rule length_from_to_in [OF _ True], simp)
-      thus ?thesis by simp
-    qed
-    thus ?thesis by simp
-  qed
-  ultimately show ?thesis using app_firstn_restn by metis
-next
-  case False
-  hence "length s \<le> m + i" by simp
-  from from_to_restn [OF this]
-  have "from_to i (m + i) s = restn i s" .
-  moreover have "firstn m (restn i s) = restn i s" 
-  proof(rule firstn_ge)
-    show "length (restn i s) \<le> m"
-    proof -
-      have "length (restn i s) = length s - i" using length_restn by metis
-      with False show ?thesis by simp
-    qed
-  qed
-  ultimately show ?thesis by simp
-qed
+by (metis diff_add_inverse2 from_to_def)
 
 lemma down_to_moment_restm:
   fixes m i s
@@ -749,25 +457,9 @@
 lemma moment_plus_split:
   fixes m i s
   shows "moment (m + i) s = moment m (restm i s) @ moment i s"
-proof -
-  from moment_split [of m i s]
-  have "moment (m + i) s = down_to (m + i) i s @ down_to i 0 s" .
-  also have "\<dots> = down_to (m+i) i s @ moment i s" using down_to_moment by simp
-  also from down_to_moment_restm have "\<dots> = moment m (restm i s) @ moment i s"
-    by simp
-  finally show ?thesis .
-qed
+by (metis down_to_moment down_to_moment_restm moment_split)
 
 lemma length_restm: "length (restm i s) = length s - i"
-proof -
-  have "length (rev (restn i (rev s))) = length s - i" (is "?L = ?R")
-  proof -
-    have "?L = length (restn i (rev s))" by simp
-    also have "\<dots>  = length (rev s) - i" using length_restn by metis
-    also have "\<dots> = ?R" by simp
-    finally show ?thesis .
-  qed
-  thus ?thesis by (simp add:restm_def)
-qed
+by (metis length_restn length_rev restm_def)
 
 end
\ No newline at end of file
diff -r 7fe2a20017c0 -r f9e0d3274c14 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Feb 27 18:53:53 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Feb 28 13:13:32 2012 +0000
@@ -11,6 +11,7 @@
 find_unused_assms PrioG 
 find_unused_assms PrioGDef
 *)
+
 ML {*
   open Printer;
   show_question_marks_default := false;
@@ -1161,7 +1162,7 @@
   \end{isabelle}
 
   \noindent
-  This means we do not need to add a holding edge to the @{text RAG} and no
+  This means we need to add a holding edge to the @{text RAG} and no
   current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
   \noindent
   In the second case we know that resource @{text cs} is locked. We can show that
diff -r 7fe2a20017c0 -r f9e0d3274c14 prio/PrioG.thy
--- a/prio/PrioG.thy	Mon Feb 27 18:53:53 2012 +0000
+++ b/prio/PrioG.thy	Tue Feb 28 13:13:32 2012 +0000
@@ -2,6 +2,7 @@
 imports PrioGDef 
 begin
 
+
 lemma runing_ready: 
   shows "runing s \<subseteq> readys s"
   unfolding runing_def readys_def
@@ -415,26 +416,7 @@
   and xz: "(x, z) \<in> r^+"
   and neq: "y \<noteq> z"
   shows "(y, z) \<in> r^+"
-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
+by (metis neq rtranclD tranclD unique xy xz)
 
 lemma unique_base:
   fixes r x y z
@@ -443,25 +425,7 @@
   and xz: "(x, z) \<in> r^+"
   and neq_yz: "y \<noteq> z"
   shows "(y, z) \<in> r^+"
-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
+by (metis neq_yz unique unique_minus xy xz)
 
 lemma unique_chain:
   fixes r x y z
@@ -672,25 +636,7 @@
   "\<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)
-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
+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)
 
 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> 
@@ -718,61 +664,7 @@
 
 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"
-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
+by (metis abs2 block_pre cs_waiting_def event.simps(20))
 
 lemma step_depend_v:
 fixes th::thread
@@ -808,13 +700,7 @@
   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})"
-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
+by (metis assms insertCI nonempty_iff)
 
 lemma depend_target_th: "(Th th, x) \<in> depend (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
   by (unfold s_depend_def, auto)
@@ -1076,13 +962,7 @@
   fixes s
   assumes vt: "vt s"
   shows "wf ((depend s)^-1)"
-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
+by (metis acyclic_depend assms finite_acyclic_wf_converse finite_depend)
 
 lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
 by (induct l, auto)
@@ -1203,31 +1083,17 @@
   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)"
-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
+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)
 
 lemma chain_building:
   assumes vt: "vt s"
@@ -1404,51 +1270,8 @@
     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)
-  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
+    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)
   ultimately 
   have "holdents s thread = insert cs (holdents (V thread cs#s) thread)"
     by auto
@@ -2308,106 +2131,20 @@
   assumes le_ij: "i \<le> j"
     and le_js: "j \<le> length s"
   shows "length (down_to j i s) = j - i"
-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
+by (metis down_to_def le_ij le_js length_from_to_in length_rev)
 
 
 lemma moment_head: 
   assumes le_it: "Suc i \<le> length t"
   obtains e where "moment (Suc i) t = e#moment i t"
-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
+by (metis assms moment_plus)
 
 lemma cnp_cnv_eq:
   fixes th s
   assumes "vt s"
   and "th \<notin> threads s"
   shows "cntP s th = cntV s th"
-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
+by (metis (full_types) add_0_right assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
 
 lemma eq_depend: 
   "depend (wq s) = depend s"
@@ -2515,43 +2252,8 @@
 lemma le_cp:
   assumes vt: "vt s"
   shows "preced th s \<le> cp s th"
-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
+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)
 
 lemma max_cp_eq: 
   assumes vt: "vt s"
diff -r 7fe2a20017c0 -r f9e0d3274c14 prio/paper.pdf
Binary file prio/paper.pdf has changed