src/HOL/Imperative_HOL/ex/SatChecker.thy

 *)
 
 header {* An efficient checker for proofs from a SAT solver *}
 
 theory SatChecker
-imports RBT_Impl Sorted_List "~~/src/HOL/Imperative_HOL/Imperative_HOL" 
+imports RBT_Impl Sorted_List Imperative_HOL
 begin
 
 section{* General settings and functions for our representation of clauses *}
 
 subsection{* Types for Literals, Clauses and ProofSteps *}

 assumes "crel (res_mem l xs) h h' r"
   shows "l \<in> set xs \<and> r = remove1 l xs"
 using assms
 proof (induct xs arbitrary: r)
   case Nil
-  thus ?case unfolding res_mem.simps by (auto elim: crel_raise)
+  thus ?case unfolding res_mem.simps by (auto elim: crel_raiseE)
 next
   case (Cons x xs')
   thus ?case
     unfolding res_mem.simps
-    by (elim crel_raise crel_return crel_if crelE) auto
+    by (elim crel_raiseE crel_returnE crel_ifE crel_bindE) auto
 qed
 
 lemma resolve1_Inv:
 assumes "crel (resolve1 l xs ys) h h' r"
   shows "l \<in> set xs \<and> r = merge (remove1 l xs) ys"
 using assms
 proof (induct xs ys arbitrary: r rule: resolve1.induct)
   case (1 l x xs y ys r)
   thus ?case
     unfolding resolve1.simps
-    by (elim crelE crel_if crel_return) auto
+    by (elim crel_bindE crel_ifE crel_returnE) auto
 next
   case (2 l ys r)
   thus ?case
     unfolding resolve1.simps
-    by (elim crel_raise) auto
+    by (elim crel_raiseE) auto
 next
   case (3 l v va r)
   thus ?case
     unfolding resolve1.simps
     by (fastsimp dest!: res_mem)

 using assms
 proof (induct xs ys arbitrary: r rule: resolve2.induct)
   case (1 l x xs y ys r)
   thus ?case
     unfolding resolve2.simps
-    by (elim crelE crel_if crel_return) auto
+    by (elim crel_bindE crel_ifE crel_returnE) auto
 next
   case (2 l ys r)
   thus ?case
     unfolding resolve2.simps
-    by (elim crel_raise) auto
+    by (elim crel_raiseE) auto
 next
   case (3 l v va r)
   thus ?case
     unfolding resolve2.simps
     by (fastsimp dest!: res_mem simp add: merge_Nil)

     from "1.hyps"(3) [OF cond res_thm] cond return have ?case by auto
   } moreover
   note "1.prems"
   ultimately show ?case
     unfolding res_thm'.simps
-    apply (elim crelE crel_if crel_return)
+    apply (elim crel_bindE crel_ifE crel_returnE)
     apply simp
     apply simp
     apply simp
     apply simp
     apply fastsimp
     done
 next
   case (2 l ys r)
   thus ?case
     unfolding res_thm'.simps
-    by (elim crel_raise) auto
+    by (elim crel_raiseE) auto
 next
   case (3 l v va r)
   thus ?case
     unfolding res_thm'.simps
-    by (elim crel_raise) auto
+    by (elim crel_raiseE) auto
 qed
 
 lemma res_mem_no_heap:
 assumes "crel (res_mem l xs) h h' r"
   shows "h = h'"
 using assms
 apply (induct xs arbitrary: r)
 unfolding res_mem.simps
-apply (elim crel_raise)
+apply (elim crel_raiseE)
 apply auto
-apply (elim crel_if crelE crel_raise crel_return)
+apply (elim crel_ifE crel_bindE crel_raiseE crel_returnE)
 apply auto
 done
 
 lemma resolve1_no_heap:
 assumes "crel (resolve1 l xs ys) h h' r"
   shows "h = h'"
 using assms
 apply (induct xs ys arbitrary: r rule: resolve1.induct)
 unfolding resolve1.simps
-apply (elim crelE crel_if crel_return crel_raise)
+apply (elim crel_bindE crel_ifE crel_returnE crel_raiseE)
 apply (auto simp add: res_mem_no_heap)
-by (elim crel_raise) auto
+by (elim crel_raiseE) auto
 
 lemma resolve2_no_heap:
 assumes "crel (resolve2 l xs ys) h h' r"
   shows "h = h'"
 using assms
 apply (induct xs ys arbitrary: r rule: resolve2.induct)
 unfolding resolve2.simps
-apply (elim crelE crel_if crel_return crel_raise)
+apply (elim crel_bindE crel_ifE crel_returnE crel_raiseE)
 apply (auto simp add: res_mem_no_heap)
-by (elim crel_raise) auto
+by (elim crel_raiseE) auto
 
 
 lemma res_thm'_no_heap:
   assumes "crel (res_thm' l xs ys) h h' r"
   shows "h = h'"
   using assms
 proof (induct xs ys arbitrary: r rule: res_thm'.induct)
   case (1 l x xs y ys r)
   thus ?thesis
     unfolding res_thm'.simps
-    by (elim crelE crel_if crel_return)
+    by (elim crel_bindE crel_ifE crel_returnE)
   (auto simp add: resolve1_no_heap resolve2_no_heap)
 next
   case (2 l ys r)
   thus ?case
     unfolding res_thm'.simps
-    by (elim crel_raise) auto
+    by (elim crel_raiseE) auto
 next
   case (3 l v va r)
   thus ?case
     unfolding res_thm'.simps
-    by (elim crel_raise) auto
+    by (elim crel_raiseE) auto
 qed
 
 
 lemma res_thm'_Inv2:
   assumes res_thm: "crel (res_thm' l xs ys) h h' rcl"

   assumes correct_a: "correctArray r a h"
   assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli"
   shows "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs"
 proof -
   from res_thm have l_not_zero: "l \<noteq> 0" 
-    by (auto elim: crel_raise)
+    by (auto elim: crel_raiseE)
   {
     fix clj
     let ?rs = "merge (remove l cli) (remove (compl l) clj)"
     let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
     assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length a h'"

     from res_thm'_no_heap[OF this] res_thm'_Inv2[OF this l_not_zero clj correct_cli]
     have "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs" by simp
   }
   with assms show ?thesis
     unfolding res_thm2.simps get_clause_def
-    by (elim crelE crelE' crel_if crel_nth crel_raise crel_return crel_option_case) auto
+    by (elim crel_bindE crel_ifE crel_nthE crel_raiseE crel_returnE crel_option_case) auto
 qed
 
 lemma foldM_Inv2:
   assumes "crel (foldM (res_thm2 a) rs cli) h h' rcl"
   assumes correct_a: "correctArray r a h"

   shows "h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl"
 using assms
 proof (induct rs arbitrary: h h' cli)
   case Nil thus ?case
     unfolding foldM.simps
-    by (elim crel_return) auto
+    by (elim crel_returnE) auto
 next
   case (Cons x xs)
   {
     fix h1 ret
     obtain l j where x_is: "x = (l, j)" by fastsimp

     from step Cons.hyps [OF foldM correct_a ret] have
     "h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl" by auto
   }
   with Cons show ?case
     unfolding foldM.simps
-    by (elim crelE) auto
+    by (elim crel_bindE) auto
 qed
 
 
 lemma step_correct2:
   assumes crel: "crel (doProofStep2 a step rcs) h h' res"

 proof (cases "(a,step,rcs)" rule: doProofStep2.cases)
   case (1 a saveTo i rs rcs)
   with crel correctArray
   show ?thesis
     apply auto
-    apply (auto simp: get_clause_def elim!: crelE crel_nth)
-    apply (auto elim!: crelE crel_nth crel_option_case crel_raise 
-      crel_return crel_upd)
+    apply (auto simp: get_clause_def elim!: crel_bindE crel_nthE)
+    apply (auto elim!: crel_bindE crel_nthE crel_option_case crel_raiseE
+      crel_returnE crel_updE)
     apply (frule foldM_Inv2)
     apply assumption
     apply (simp add: correctArray_def)
     apply (drule_tac x="y" in bspec)
     apply (rule array_ranI[where i=i])
     by (auto intro: correctArray_update)
 next
   case (2 a cid rcs)
   with crel correctArray
   show ?thesis
-    by (auto simp: correctArray_def elim!: crelE crel_upd crel_return
+    by (auto simp: correctArray_def elim!: crel_bindE crel_updE crel_returnE
      dest: array_ran_upd_array_None)
 next
   case (3 a cid c rcs)
   with crel correctArray
   show ?thesis
-    apply (auto elim!: crelE crel_upd crel_return)
+    apply (auto elim!: crel_bindE crel_updE crel_returnE)
     apply (auto simp: correctArray_def dest!: array_ran_upd_array_Some)
     apply (auto intro: correctClause_mono)
     by (auto simp: correctClause_def)
 next
   case 4
   with crel correctArray
-  show ?thesis by (auto elim: crel_raise)
+  show ?thesis by (auto elim: crel_raiseE)
 next
   case 5
   with crel correctArray
-  show ?thesis by (auto elim: crel_raise)
+  show ?thesis by (auto elim: crel_raiseE)
 qed
   
 
 theorem fold_steps_correct:
   assumes "crel (foldM (doProofStep2 a) steps rcs) h h' res"
   assumes "correctArray rcs a h"
   shows "correctArray res a h'"
 using assms
 by (induct steps arbitrary: rcs h h' res)
- (auto elim!: crelE crel_return dest:step_correct2)
+ (auto elim!: crel_bindE crel_returnE dest:step_correct2)
 
 theorem checker_soundness:
   assumes "crel (checker n p i) h h' cs"
   shows "inconsistent cs"
 using assms unfolding checker_def
-apply (elim crelE crel_nth crel_if crel_return crel_raise crel_new_weak)
+apply (elim crel_bindE crel_nthE crel_ifE crel_returnE crel_raiseE crel_newE)
 prefer 2 apply simp
 apply auto
 apply (drule fold_steps_correct)
 apply (simp add: correctArray_def array_ran_def)
 apply (rule implies_empty_inconsistent)