# HG changeset patch
# User haftmann
# Date 1278943508 -7200
# Node ID 1bec64044b5e1e550917742eb3105785b5e0c92c
# Parent  cddb3106adb898c18f173e17a3be1a818c63c3bf
spelt out relational framework in a consistent way

diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -155,6 +155,14 @@
   "array_present a (change b i v h) = array_present a h"
   by (simp add: change_def array_present_def set_array_def get_array_def)
 
+lemma array_present_array [simp]:
+  "array_present (fst (array xs h)) (snd (array xs h))"
+  by (simp add: array_present_def array_def set_array_def Let_def)
+
+lemma not_array_present_array [simp]:
+  "\<not> array_present (fst (array xs h)) h"
+  by (simp add: array_present_def array_def Let_def)
+
 
 text {* Monad operations *}
 
@@ -166,6 +174,17 @@
   "success (new n x) h"
   by (simp add: new_def)
 
+lemma crel_newI [crel_intros]:
+  assumes "(a, h') = array (replicate n x) h"
+  shows "crel (new n x) h h' a"
+  by (rule crelI) (simp add: assms)
+
+lemma crel_newE [crel_elims]:
+  assumes "crel (new n x) h h' r"
+  obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
+    "get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h"
+  using assms by (rule crelE) (simp add: get_array_init_array_list)
+
 lemma execute_of_list [simp, execute_simps]:
   "execute (of_list xs) h = Some (array xs h)"
   by (simp add: of_list_def)
@@ -174,6 +193,17 @@
   "success (of_list xs) h"
   by (simp add: of_list_def)
 
+lemma crel_of_listI [crel_intros]:
+  assumes "(a, h') = array xs h"
+  shows "crel (of_list xs) h h' a"
+  by (rule crelI) (simp add: assms)
+
+lemma crel_of_listE [crel_elims]:
+  assumes "crel (of_list xs) h h' r"
+  obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
+    "get_array r h' = xs" "array_present r h'" "\<not> array_present r h"
+  using assms by (rule crelE) (simp add: get_array_init_array_list)
+
 lemma execute_make [simp, execute_simps]:
   "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
   by (simp add: make_def)
@@ -182,6 +212,17 @@
   "success (make n f) h"
   by (simp add: make_def)
 
+lemma crel_makeI [crel_intros]:
+  assumes "(a, h') = array (map f [0 ..< n]) h"
+  shows "crel (make n f) h h' a"
+  by (rule crelI) (simp add: assms)
+
+lemma crel_makeE [crel_elims]:
+  assumes "crel (make n f) h h' r"
+  obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
+    "get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h"
+  using assms by (rule crelE) (simp add: get_array_init_array_list)
+
 lemma execute_len [simp, execute_simps]:
   "execute (len a) h = Some (length a h, h)"
   by (simp add: len_def)
@@ -190,6 +231,16 @@
   "success (len a) h"
   by (simp add: len_def)
 
+lemma crel_lengthI [crel_intros]:
+  assumes "h' = h" "r = length a h"
+  shows "crel (len a) h h' r"
+  by (rule crelI) (simp add: assms)
+
+lemma crel_lengthE [crel_elims]:
+  assumes "crel (len a) h h' r"
+  obtains "r = length a h'" "h' = h" 
+  using assms by (rule crelE) simp
+
 lemma execute_nth [execute_simps]:
   "i < length a h \<Longrightarrow>
     execute (nth a i) h = Some (get_array a h ! i, h)"
@@ -200,38 +251,82 @@
   "i < length a h \<Longrightarrow> success (nth a i) h"
   by (auto intro: success_intros simp add: nth_def)
 
+lemma crel_nthI [crel_intros]:
+  assumes "i < length a h" "h' = h" "r = get_array a h ! i"
+  shows "crel (nth a i) h h' r"
+  by (rule crelI) (insert assms, simp add: execute_simps)
+
+lemma crel_nthE [crel_elims]:
+  assumes "crel (nth a i) h h' r"
+  obtains "i < length a h" "r = get_array a h ! i" "h' = h"
+  using assms by (rule crelE)
+    (erule successE, cases "i < length a h", simp_all add: execute_simps)
+
 lemma execute_upd [execute_simps]:
   "i < length a h \<Longrightarrow>
     execute (upd i x a) h = Some (a, change a i x h)"
-  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+  "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
   by (simp_all add: upd_def execute_simps)
 
 lemma success_updI [success_intros]:
   "i < length a h \<Longrightarrow> success (upd i x a) h"
   by (auto intro: success_intros simp add: upd_def)
 
+lemma crel_updI [crel_intros]:
+  assumes "i < length a h" "h' = change a i v h"
+  shows "crel (upd i v a) h h' a"
+  by (rule crelI) (insert assms, simp add: execute_simps)
+
+lemma crel_updE [crel_elims]:
+  assumes "crel (upd i v a) h h' r"
+  obtains "r = a" "h' = change a i v h" "i < length a h"
+  using assms by (rule crelE)
+    (erule successE, cases "i < length a h", simp_all add: execute_simps)
+
 lemma execute_map_entry [execute_simps]:
   "i < length a h \<Longrightarrow>
    execute (map_entry i f a) h =
       Some (a, change a i (f (get_array a h ! i)) h)"
-  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+  "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
   by (simp_all add: map_entry_def execute_simps)
 
 lemma success_map_entryI [success_intros]:
   "i < length a h \<Longrightarrow> success (map_entry i f a) h"
   by (auto intro: success_intros simp add: map_entry_def)
 
+lemma crel_map_entryI [crel_intros]:
+  assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a"
+  shows "crel (map_entry i f a) h h' r"
+  by (rule crelI) (insert assms, simp add: execute_simps)
+
+lemma crel_map_entryE [crel_elims]:
+  assumes "crel (map_entry i f a) h h' r"
+  obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h"
+  using assms by (rule crelE)
+    (erule successE, cases "i < length a h", simp_all add: execute_simps)
+
 lemma execute_swap [execute_simps]:
   "i < length a h \<Longrightarrow>
    execute (swap i x a) h =
       Some (get_array a h ! i, change a i x h)"
-  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+  "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
   by (simp_all add: swap_def execute_simps)
 
 lemma success_swapI [success_intros]:
   "i < length a h \<Longrightarrow> success (swap i x a) h"
   by (auto intro: success_intros simp add: swap_def)
 
+lemma crel_swapI [crel_intros]:
+  assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i"
+  shows "crel (swap i x a) h h' r"
+  by (rule crelI) (insert assms, simp add: execute_simps)
+
+lemma crel_swapE [crel_elims]:
+  assumes "crel (swap i x a) h h' r"
+  obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h"
+  using assms by (rule crelE)
+    (erule successE, cases "i < length a h", simp_all add: execute_simps)
+
 lemma execute_freeze [simp, execute_simps]:
   "execute (freeze a) h = Some (get_array a h, h)"
   by (simp add: freeze_def)
@@ -240,6 +335,16 @@
   "success (freeze a) h"
   by (simp add: freeze_def)
 
+lemma crel_freezeI [crel_intros]:
+  assumes "h' = h" "r = get_array a h"
+  shows "crel (freeze a) h h' r"
+  by (rule crelI) (insert assms, simp add: execute_simps)
+
+lemma crel_freezeE [crel_elims]:
+  assumes "crel (freeze a) h h' r"
+  obtains "h' = h" "r = get_array a h"
+  using assms by (rule crelE) simp
+
 lemma upd_return:
   "upd i x a \<guillemotright> return a = upd i x a"
   by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
@@ -252,7 +357,7 @@
   "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   by (rule Heap_eqI) (simp add: map_nth)
 
-hide_const (open) new map
+hide_const (open) new
 
 
 subsection {* Code generator setup *}
@@ -339,7 +444,7 @@
       n \<leftarrow> len a;
       Heap_Monad.fold_map (Array.nth a) [0..<n]
     done) h = Some (get_array a h, h)"
-    by (auto intro: execute_eq_SomeI)
+    by (auto intro: execute_bind_eq_SomeI)
   then show "execute (freeze a) h = execute (do
       n \<leftarrow> len a;
       Heap_Monad.fold_map (Array.nth a) [0..<n]
diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -2,7 +2,7 @@
     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
-header {* A monad with a polymorphic heap *}
+header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
 
 theory Heap_Monad
 imports Heap
@@ -81,8 +81,10 @@
 
 lemma successE:
   assumes "success f h"
-  obtains r h' where "execute f h = Some (r, h')"
-  using assms by (auto simp add: success_def)
+  obtains r h' where "r = fst (the (execute c h))"
+    and "h' = snd (the (execute c h))"
+    and "execute f h \<noteq> None"
+  using assms by (simp add: success_def)
 
 ML {* structure Success_Intros = Named_Thms(
   val name = "success_intros"
@@ -107,6 +109,121 @@
   "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
   by (simp add: Let_def)
 
+lemma success_ifI:
+  "(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow>
+    success (if c then t else e) h"
+  by (simp add: success_def)
+
+
+subsubsection {* Predicate for a simple relational calculus *}
+
+text {*
+  The @{text crel} predicate states that when a computation @{text c}
+  runs with the heap @{text h} will result in return value @{text r}
+  and a heap @{text "h'"}, i.e.~no exception occurs.
+*}  
+
+definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
+  crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
+
+lemma crelI:
+  "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
+  by (simp add: crel_def)
+
+lemma crelE:
+  assumes "crel c h h' r"
+  obtains "r = fst (the (execute c h))"
+    and "h' = snd (the (execute c h))"
+    and "success c h"
+proof (rule that)
+  from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def)
+  then show "success c h" by (simp add: success_def)
+  from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
+    by simp_all
+  then show "r = fst (the (execute c h))"
+    and "h' = snd (the (execute c h))" by simp_all
+qed
+
+lemma crel_success:
+  "crel c h h' r \<Longrightarrow> success c h"
+  by (simp add: crel_def success_def)
+
+lemma success_crelE:
+  assumes "success c h"
+  obtains r h' where "crel c h h' r"
+  using assms by (auto simp add: crel_def success_def)
+
+lemma crel_deterministic:
+  assumes "crel f h h' a"
+    and "crel f h h'' b"
+  shows "a = b" and "h' = h''"
+  using assms unfolding crel_def by auto
+
+ML {* structure Crel_Intros = Named_Thms(
+  val name = "crel_intros"
+  val description = "introduction rules for crel"
+) *}
+
+ML {* structure Crel_Elims = Named_Thms(
+  val name = "crel_elims"
+  val description = "elimination rules for crel"
+) *}
+
+setup "Crel_Intros.setup #> Crel_Elims.setup"
+
+lemma crel_LetI [crel_intros]:
+  assumes "x = t" "crel (f x) h h' r"
+  shows "crel (let x = t in f x) h h' r"
+  using assms by simp
+
+lemma crel_LetE [crel_elims]:
+  assumes "crel (let x = t in f x) h h' r"
+  obtains "crel (f t) h h' r"
+  using assms by simp
+
+lemma crel_ifI:
+  assumes "c \<Longrightarrow> crel t h h' r"
+    and "\<not> c \<Longrightarrow> crel e h h' r"
+  shows "crel (if c then t else e) h h' r"
+  by (cases c) (simp_all add: assms)
+
+lemma crel_ifE:
+  assumes "crel (if c then t else e) h h' r"
+  obtains "c" "crel t h h' r"
+    | "\<not> c" "crel e h h' r"
+  using assms by (cases c) simp_all
+
+lemma crel_tapI [crel_intros]:
+  assumes "h' = h" "r = f h"
+  shows "crel (tap f) h h' r"
+  by (rule crelI) (simp add: assms)
+
+lemma crel_tapE [crel_elims]:
+  assumes "crel (tap f) h h' r"
+  obtains "h' = h" and "r = f h"
+  using assms by (rule crelE) auto
+
+lemma crel_heapI [crel_intros]:
+  assumes "h' = snd (f h)" "r = fst (f h)"
+  shows "crel (heap f) h h' r"
+  by (rule crelI) (simp add: assms)
+
+lemma crel_heapE [crel_elims]:
+  assumes "crel (heap f) h h' r"
+  obtains "h' = snd (f h)" and "r = fst (f h)"
+  using assms by (rule crelE) simp
+
+lemma crel_guardI [crel_intros]:
+  assumes "P h" "h' = snd (f h)" "r = fst (f h)"
+  shows "crel (guard P f) h h' r"
+  by (rule crelI) (simp add: assms execute_simps)
+
+lemma crel_guardE [crel_elims]:
+  assumes "crel (guard P f) h h' r"
+  obtains "h' = snd (f h)" "r = fst (f h)" "P h"
+  using assms by (rule crelE)
+    (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)
+
 
 subsubsection {* Monad combinators *}
 
@@ -121,6 +238,15 @@
   "success (return x) h"
   by (rule successI) simp
 
+lemma crel_returnI [crel_intros]:
+  "h = h' \<Longrightarrow> crel (return x) h h' x"
+  by (rule crelI) simp
+
+lemma crel_returnE [crel_elims]:
+  assumes "crel (return x) h h' r"
+  obtains "r = x" "h' = h"
+  using assms by (rule crelE) simp
+
 definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   [code del]: "raise s = Heap (\<lambda>_. None)"
 
@@ -128,6 +254,11 @@
   "execute (raise s) = (\<lambda>_. None)"
   by (simp add: raise_def)
 
+lemma crel_raiseE [crel_elims]:
+  assumes "crel (raise x) h h' r"
+  obtains "False"
+  using assms by (rule crelE) (simp add: success_def)
+
 definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
   [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
                   Some (x, h') \<Rightarrow> execute (g x) h'
@@ -140,15 +271,32 @@
   "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   by (simp_all add: bind_def)
 
-lemma success_bindI [success_intros]:
-  "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
+lemma execute_bind_success:
+  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
+  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
+
+lemma success_bind_executeI:
+  "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   by (auto intro!: successI elim!: successE simp add: bind_def)
 
-lemma execute_bind_successI [execute_simps]:
-  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
-  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
-  
-lemma execute_eq_SomeI:
+lemma success_bind_crelI [success_intros]:
+  "crel f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
+  by (auto simp add: crel_def success_def bind_def)
+
+lemma crel_bindI [crel_intros]:
+  assumes "crel f h h' r" "crel (g r) h' h'' r'"
+  shows "crel (f \<guillemotright>= g) h h'' r'"
+  using assms
+  apply (auto intro!: crelI elim!: crelE successE)
+  apply (subst execute_bind, simp_all)
+  done
+
+lemma crel_bindE [crel_elims]:
+  assumes "crel (f \<guillemotright>= g) h h'' r'"
+  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
+  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
+
+lemma execute_bind_eq_SomeI:
   assumes "Heap_Monad.execute f h = Some (x, h')"
     and "Heap_Monad.execute (g x) h' = Some (y, h'')"
   shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
@@ -269,6 +417,15 @@
   "P x \<Longrightarrow> success (assert P x) h"
   by (rule successI) (simp add: execute_assert)
 
+lemma crel_assertI [crel_intros]:
+  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> crel (assert P x) h h' r"
+  by (rule crelI) (simp add: execute_assert)
+ 
+lemma crel_assertE [crel_elims]:
+  assumes "crel (assert P x) h h' r"
+  obtains "P x" "r = x" "h' = h"
+  using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def)
+
 lemma assert_cong [fundef_cong]:
   assumes "P = P'"
   assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -6,8 +6,8 @@
 header {* Monadic imperative HOL with examples *}
 
 theory Imperative_HOL_ex
-imports Imperative_HOL "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists"
-  "ex/SatChecker"
+imports Imperative_HOL
+  "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
 begin
 
 end
diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -92,6 +92,10 @@
   "set r x (set r y h) = set r x h"
   by (simp add: set_def)
 
+lemma not_present_alloc [simp]:
+  "\<not> present h (fst (alloc v h))"
+  by (simp add: present_def alloc_def Let_def)
+
 lemma set_set_swap:
   "r =!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
   by (simp add: noteq_def set_def expand_fun_eq)
@@ -139,6 +143,16 @@
   "success (ref v) h"
   by (auto simp add: ref_def)
 
+lemma crel_refI [crel_intros]:
+  assumes "(r, h') = alloc v h"
+  shows "crel (ref v) h h' r"
+  by (rule crelI) (insert assms, simp)
+
+lemma crel_refE [crel_elims]:
+  assumes "crel (ref v) h h' r"
+  obtains "Ref.get h' r = v" and "Ref.present h' r" and "\<not> Ref.present h r"
+  using assms by (rule crelE) simp
+
 lemma execute_lookup [simp, execute_simps]:
   "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
   by (simp add: lookup_def)
@@ -147,6 +161,16 @@
   "success (lookup r) h"
   by (auto simp add: lookup_def)
 
+lemma crel_lookupI [crel_intros]:
+  assumes "h' = h" "x = Ref.get h r"
+  shows "crel (!r) h h' x"
+  by (rule crelI) (insert assms, simp)
+
+lemma crel_lookupE [crel_elims]:
+  assumes "crel (!r) h h' x"
+  obtains "h' = h" "x = Ref.get h r"
+  using assms by (rule crelE) simp
+
 lemma execute_update [simp, execute_simps]:
   "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
   by (simp add: update_def)
@@ -155,17 +179,37 @@
   "success (update r v) h"
   by (auto simp add: update_def)
 
+lemma crel_updateI [crel_intros]:
+  assumes "h' = Ref.set r v h"
+  shows "crel (r := v) h h' x"
+  by (rule crelI) (insert assms, simp)
+
+lemma crel_updateE [crel_elims]:
+  assumes "crel (r' := v) h h' r"
+  obtains "h' = Ref.set r' v h"
+  using assms by (rule crelE) simp
+
 lemma execute_change [simp, execute_simps]:
   "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
   by (simp add: change_def bind_def Let_def)
 
 lemma success_changeI [iff, success_intros]:
   "success (change f r) h"
-  by (auto intro!: success_intros simp add: change_def)
+  by (auto intro!: success_intros crel_intros simp add: change_def)
+
+lemma crel_changeI [crel_intros]: 
+  assumes "h' = Ref.set r (f (Ref.get h r)) h" "x = f (Ref.get h r)"
+  shows "crel (Ref.change f r) h h' x"
+  by (rule crelI) (insert assms, simp)  
+
+lemma crel_changeE [crel_elims]:
+  assumes "crel (Ref.change f r') h h' r"
+  obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
+  using assms by (rule crelE) simp
 
 lemma lookup_chain:
   "(!r \<guillemotright> f) = f"
-  by (rule Heap_eqI) (auto simp add: lookup_def execute_simps)
+  by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
 
 lemma update_change [code]:
   "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/Relational.thy
--- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -2,81 +2,38 @@
 imports Array Ref
 begin
 
-section{* Definition of the Relational framework *}
-
-text {* The crel predicate states that when a computation c runs with the heap h
-  will result in return value r and a heap h' (if no exception occurs). *}  
-
-definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
-
-lemma crel_def: -- FIXME
-  "crel c h h' r \<longleftrightarrow> Some (r, h') = Heap_Monad.execute c h"
-  unfolding crel_def' by auto
-
-lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
-unfolding crel_def' by auto
-
-section {* Elimination rules *}
-
-text {* For all commands, we define simple elimination rules. *}
-(* FIXME: consumes 1 necessary ?? *)
-
-lemma crel_tap:
-  assumes "crel (Heap_Monad.tap f) h h' r"
-  obtains "h' = h" "r = f h"
-  using assms by (simp add: crel_def)
-
-lemma crel_heap:
-  assumes "crel (Heap_Monad.heap f) h h' r"
-  obtains "h' = snd (f h)" "r = fst (f h)"
-  using assms by (cases "f h") (simp add: crel_def)
+lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
+unfolding crel_def bind_def Let_def assert_def
+  raise_def return_def prod_case_beta
+apply (cases f)
+apply simp
+apply (simp add: expand_fun_eq split_def)
+apply (auto split: option.split)
+done
 
-lemma crel_guard:
-  assumes "crel (Heap_Monad.guard P f) h h' r"
-  obtains "h' = snd (f h)" "r = fst (f h)" "P h"
-  using assms by (cases "f h", cases "P h") (simp_all add: crel_def execute_simps)
-
-
-subsection {* Elimination rules for basic monadic commands *}
-
-lemma crelE[consumes 1]:
-  assumes "crel (f >>= g) h h'' r'"
-  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
-  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
-
-lemma crelE'[consumes 1]:
-  assumes "crel (f >> g) h h'' r'"
-  obtains h' r where "crel f h h' r" "crel g h' h'' r'"
-  using assms
-  by (elim crelE) auto
+lemma crel_option_caseI:
+  assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
+  assumes "x = None \<Longrightarrow> crel n h h' r"
+  shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
+using assms
+by (auto split: option.split)
 
-lemma crel_return[consumes 1]:
-  assumes "crel (return x) h h' r"
-  obtains "r = x" "h = h'"
-  using assms
-  unfolding crel_def return_def by simp
+lemma crelI2:
+  assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
+  shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
+  oops
 
-lemma crel_raise[consumes 1]:
-  assumes "crel (raise x) h h' r"
-  obtains "False"
-  using assms
-  unfolding crel_def raise_def by simp
-
-lemma crel_if:
-  assumes "crel (if c then t else e) h h' r"
-  obtains "c" "crel t h h' r"
-        | "\<not>c" "crel e h h' r"
-  using assms
-  unfolding crel_def by auto
+lemma crel_ifI2:
+  assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
+  "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
+  shows "\<exists> h' r. crel (if c then t else e) h h' r"
+  oops
 
 lemma crel_option_case:
   assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
   obtains "x = None" "crel n h h' r"
         | y where "x = Some y" "crel (s y) h h' r" 
-  using assms
-  unfolding crel_def by auto
+  using assms unfolding crel_def by (auto split: option.splits)
 
 lemma crel_fold_map:
   assumes "crel (Heap_Monad.fold_map f xs) h h' r"
@@ -86,73 +43,19 @@
 using assms(1)
 proof (induct xs arbitrary: h h' r)
   case Nil  with assms(2) show ?case
-    by (auto elim: crel_return)
+    by (auto elim: crel_returnE)
 next
   case (Cons x xs)
   from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
     and crel_fold_map: "crel (Heap_Monad.fold_map f xs) h1 h' ys"
     and r_def: "r = y#ys"
     unfolding fold_map.simps
-    by (auto elim!: crelE crel_return)
+    by (auto elim!: crel_bindE crel_returnE)
   from Cons(1)[OF crel_fold_map] crel_fold_map crel_f assms(3) r_def
   show ?case by auto
 qed
 
-
-subsection {* Elimination rules for array commands *}
-
-(* Strong version of the lemma for this operation is missing *) 
-lemma crel_new_weak:
-  assumes "crel (Array.new n v) h h' r"
-  obtains "get_array r h' = List.replicate n v"
-  using assms unfolding Array.new_def
-  by (elim crel_heap) (auto simp: array_def Let_def split_def)
-
-(* Strong version of the lemma for this operation is missing *)
-lemma crel_of_list_weak:
-  assumes "crel (Array.of_list xs) h h' r"
-  obtains "get_array r h' = xs"
-  using assms unfolding of_list_def 
-  by (elim crel_heap) (simp add: get_array_init_array_list)
-
-(* Strong version of the lemma for this operation is missing *)
-lemma crel_make_weak:
-  assumes "crel (Array.make n f) h h' r"
-  obtains "i < n \<Longrightarrow> get_array r h' ! i = f i"
-  using assms unfolding Array.make_def
-  by (elim crel_heap) (auto simp: array_def Let_def split_def)
-
-lemma crel_length:
-  assumes "crel (len a) h h' r"
-  obtains "h = h'" "r = Array.length a h'"
-  using assms unfolding Array.len_def
-  by (elim crel_tap) simp
-
-lemma crel_nth[consumes 1]:
-  assumes "crel (nth a i) h h' r"
-  obtains "r = get_array a h ! i" "h = h'" "i < Array.length a h"
-  using assms unfolding nth_def
-  by (elim crel_guard) (clarify, simp)
-
-lemma crel_upd[consumes 1]:
-  assumes "crel (upd i v a) h h' r"
-  obtains "r = a" "h' = Array.change a i v h" "i < Array.length a h"
-  using assms unfolding upd_def
-  by (elim crel_guard) simp
-
-lemma crel_map_entry:
-  assumes "crel (Array.map_entry i f a) h h' r"
-  obtains "r = a" "h' = Array.change a i (f (get_array a h ! i)) h" "i < Array.length a h"
-  using assms unfolding Array.map_entry_def
-  by (elim crel_guard) simp
-
-lemma crel_swap:
-  assumes "crel (Array.swap i x a) h h' r"
-  obtains "r = get_array a h ! i" "h' = Array.change a i x h"
-  using assms unfolding Array.swap_def
-  by (elim crel_guard) simp
-
-lemma upt_conv_Cons': (*FIXME move*)
+lemma upt_conv_Cons':
   assumes "Suc a \<le> b"
   shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
 proof -
@@ -169,7 +72,7 @@
 using assms
 proof (induct n arbitrary: xs h h')
   case 0 thus ?case
-    by (auto elim!: crel_return simp add: Array.length_def)
+    by (auto elim!: crel_returnE simp add: Array.length_def)
 next
   case (Suc n)
   from Suc(3) have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
@@ -177,7 +80,7 @@
   with Suc(2) obtain r where
     crel_fold_map: "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
     and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
-    by (auto elim!: crelE crel_nth crel_return)
+    by (auto elim!: crel_bindE crel_nthE crel_returnE)
   from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)" 
     by arith
   with Suc.hyps[OF crel_fold_map] xs_def show ?case
@@ -185,12 +88,6 @@
     by (auto simp add: nth_drop')
 qed
 
-lemma crel_freeze:
-  assumes "crel (Array.freeze a) h h' xs"
-  obtains "h = h'" "xs = get_array a h"
-  using assms unfolding freeze_def
-  by (elim crel_tap) simp
-
 lemma crel_fold_map_map_entry_remains:
   assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
   assumes "i < Array.length a h - n"
@@ -199,7 +96,7 @@
 proof (induct n arbitrary: h h' r)
   case 0
   thus ?case
-    by (auto elim: crel_return)
+    by (auto elim: crel_returnE)
 next
   case (Suc n)
   let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
@@ -207,7 +104,7 @@
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
     crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
-    by (auto simp add: elim!: crelE crel_map_entry crel_return)
+    by (auto simp add: elim!: crel_bindE crel_map_entryE crel_returnE)
   have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
     by simp
@@ -224,7 +121,7 @@
 proof (induct n arbitrary: h h' r)
   case 0
   thus ?case
-    by (auto elim!: crel_return)
+    by (auto elim!: crel_returnE)
 next
   case (Suc n)
   let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
@@ -232,7 +129,7 @@
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where
     crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
-    by (auto simp add: elim!: crelE crel_map_entry crel_return)
+    by (auto simp add: elim!: crel_bindE crel_map_entryE crel_returnE)
   have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
   from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
@@ -252,7 +149,7 @@
 using assms
 proof (induct n arbitrary: h h' r)
   case 0
-  thus ?case by (auto elim!: crel_return)
+  thus ?case by (auto elim!: crel_returnE)
 next
   case (Suc n)
   let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
@@ -260,7 +157,7 @@
     by (simp add: upt_conv_Cons')
   from Suc(2) this obtain r where 
     crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
-    by (auto elim!: crelE crel_map_entry crel_return)
+    by (auto elim!: crel_bindE crel_map_entryE crel_returnE)
   have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
     by simp
@@ -278,222 +175,6 @@
     by (auto intro: nth_equalityI)
 qed
 
-
-subsection {* Elimination rules for reference commands *}
-
-(* TODO:
-maybe introduce a new predicate "extends h' h x"
-which means h' extends h with a new reference x.
-Then crel_new: would be
-assumes "crel (Ref.new v) h h' x"
-obtains "get_ref x h' = v"
-and "extends h' h x"
-
-and we would need further rules for extends:
-extends h' h x \<Longrightarrow> \<not> ref_present x h
-extends h' h x \<Longrightarrow>  ref_present x h'
-extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> ref_present y h'
-extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> get_ref y h = get_ref y h'
-extends h' h x \<Longrightarrow> lim h' = Suc (lim h)
-*)
-
-lemma crel_ref:
-  assumes "crel (ref v) h h' x"
-  obtains "Ref.get h' x = v"
-  and "\<not> Ref.present h x"
-  and "Ref.present h' x"
-  and "\<forall>y. Ref.present h y \<longrightarrow> Ref.get h y = Ref.get h' y"
- (* and "lim h' = Suc (lim h)" *)
-  and "\<forall>y. Ref.present h y \<longrightarrow> Ref.present h' y"
-  using assms
-  unfolding Ref.ref_def
-  apply (elim crel_heap)
-  unfolding Ref.alloc_def
-  apply (simp add: Let_def)
-  unfolding Ref.present_def
-  apply auto
-  unfolding Ref.get_def Ref.set_def
-  apply auto
-  done
-
-lemma crel_lookup:
-  assumes "crel (!r') h h' r"
-  obtains "h = h'" "r = Ref.get h r'"
-  using assms unfolding Ref.lookup_def
-  by (auto elim: crel_tap)
-
-lemma crel_update:
-  assumes "crel (r' := v) h h' r"
-  obtains "h' = Ref.set r' v h" "r = ()"
-  using assms unfolding Ref.update_def
-  by (auto elim: crel_heap)
-
-lemma crel_change:
-  assumes "crel (Ref.change f r') h h' r"
-  obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
-  using assms unfolding Ref.change_def Let_def
-  by (auto elim!: crelE crel_lookup crel_update crel_return)
-
-subsection {* Elimination rules for the assert command *}
-
-lemma crel_assert[consumes 1]:
-  assumes "crel (assert P x) h h' r"
-  obtains "P x" "r = x" "h = h'"
-  using assms
-  unfolding assert_def
-  by (elim crel_if crel_return crel_raise) auto
-
-lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
-unfolding crel_def bind_def Let_def assert_def
-  raise_def return_def prod_case_beta
-apply (cases f)
-apply simp
-apply (simp add: expand_fun_eq split_def)
-apply (auto split: option.split)
-apply (erule_tac x="x" in meta_allE)
-apply auto
-done
-
-section {* Introduction rules *}
-
-subsection {* Introduction rules for basic monadic commands *}
-
-lemma crelI:
-  assumes "crel f h h' r" "crel (g r) h' h'' r'"
-  shows "crel (f >>= g) h h'' r'"
-  using assms by (simp add: crel_def' bind_def)
-
-lemma crelI':
-  assumes "crel f h h' r" "crel g h' h'' r'"
-  shows "crel (f >> g) h h'' r'"
-  using assms by (intro crelI) auto
-
-lemma crel_returnI:
-  shows "crel (return x) h h x"
-  unfolding crel_def return_def by simp
-
-lemma crel_raiseI:
-  shows "\<not> (crel (raise x) h h' r)"
-  unfolding crel_def raise_def by simp
-
-lemma crel_ifI:
-  assumes "c \<longrightarrow> crel t h h' r"
-  "\<not>c \<longrightarrow> crel e h h' r"
-  shows "crel (if c then t else e) h h' r"
-  using assms
-  unfolding crel_def by auto
-
-lemma crel_option_caseI:
-  assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
-  assumes "x = None \<Longrightarrow> crel n h h' r"
-  shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
-using assms
-by (auto split: option.split)
-
-lemma crel_tapI:
-  assumes "h' = h" "r = f h"
-  shows "crel (Heap_Monad.tap f) h h' r"
-  using assms by (simp add: crel_def)
-
-lemma crel_heapI:
-  shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
-  by (simp add: crel_def apfst_def split_def prod_fun_def)
-
-lemma crel_heapI': (*FIXME keep only this version*)
-  assumes "h' = snd (f h)" "r = fst (f h)"
-  shows "crel (Heap_Monad.heap f) h h' r"
-  using assms
-  by (simp add: crel_def split_def apfst_def prod_fun_def)
-
-lemma crel_guardI:
-  assumes "P h" "h' = snd (f h)" "r = fst (f h)"
-  shows "crel (Heap_Monad.guard P f) h h' r"
-  using assms by (simp add: crel_def execute_simps)
-
-lemma crelI2:
-  assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
-  shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
-  oops
-
-lemma crel_ifI2:
-  assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
-  "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
-  shows "\<exists> h' r. crel (if c then t else e) h h' r"
-  oops
-
-subsection {* Introduction rules for array commands *}
-
-lemma crel_lengthI:
-  shows "crel (Array.len a) h h (Array.length a h)"
-  unfolding len_def by (rule crel_tapI) simp_all
-
-(* thm crel_newI for Array.new is missing *)
-
-lemma crel_nthI:
-  assumes "i < Array.length a h"
-  shows "crel (nth a i) h h ((get_array a h) ! i)"
-  using assms unfolding nth_def by (auto intro: crel_guardI)
-
-lemma crel_updI:
-  assumes "i < Array.length a h"
-  shows "crel (upd i v a) h (Array.change a i v h) a"
-  using assms unfolding upd_def by (auto intro: crel_guardI)
-
-(* thm crel_of_listI is missing *)
-
-(* thm crel_map_entryI is missing *)
-
-(* thm crel_swapI is missing *)
-
-(* thm crel_makeI is missing *)
-
-(* thm crel_freezeI is missing *)
-
-(* thm crel_mapI is missing *)
-
-subsubsection {* Introduction rules for reference commands *}
-
-lemma crel_lookupI:
-  shows "crel (!r) h h (Ref.get h r)"
-  unfolding lookup_def by (auto intro!: crel_tapI)
-
-lemma crel_updateI:
-  shows "crel (r := v) h (Ref.set r v h) ()"
-  unfolding update_def by (auto intro!: crel_heapI')
-
-lemma crel_changeI: 
-  shows "crel (Ref.change f r) h (Ref.set r (f (Ref.get h r)) h) (f (Ref.get h r))"
-  unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
-
-subsubsection {* Introduction rules for the assert command *}
-
-lemma crel_assertI:
-  assumes "P x"
-  shows "crel (assert P x) h h x"
-  using assms
-  unfolding assert_def
-  by (auto intro!: crel_ifI crel_returnI crel_raiseI)
- 
-subsection {* Induction rule for the MREC combinator *}
-
-lemma MREC_induct:
-  assumes "crel (MREC f g x) h h' r"
-  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
-  assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
-    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
-  shows "P x h h' r"
-proof (rule MREC_pinduct[OF assms(1)[unfolded crel_def, symmetric]])
-  fix x h h1 h2 h' s z r
-  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
-    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
-    "P s h1 h2 z"
-    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
-  from assms(3)[unfolded crel_def, OF this(1)[symmetric] this(2)[symmetric] this(3) this(4)[symmetric]]
-  show "P x h h' r" .
-next
-qed (auto simp add: assms(2)[unfolded crel_def])
-
-
 lemma success_fold_map_map_entry:
   assumes "n \<le> Array.length a h"
   shows "success (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
@@ -507,25 +188,26 @@
     (Array.length a h - Suc n) # [Array.length a h - n..<Array.length a h]"
     by (simp add: upt_conv_Cons')
   with Suc.hyps [of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case apply -
-    apply (auto simp add: execute_simps intro!: successI success_returnI success_map_entryI elim: crel_map_entry)
-    apply (subst execute_bind) apply (auto simp add: execute_simps)
+    apply (auto simp add: execute_simps execute_bind_success intro!: successI success_returnI success_map_entryI elim: crel_map_entryE)
+    apply (subst execute_bind) apply (auto simp add: execute_simps execute_bind_success intro: execute_bind)
     done
 qed
 
-
-section {* Cumulative lemmas *}
-
-lemmas crel_elim_all =
-  crelE crelE' crel_return crel_raise crel_if crel_option_case
-  crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze
-  crel_ref crel_lookup crel_update crel_change
-  crel_assert
+lemma MREC_induct:
+  assumes "crel (MREC f g x) h h' r"
+  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
+  assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
+    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
+  shows "P x h h' r"
+proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
+  fix x h h1 h2 h' s z r
+  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
+    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
+    "P s h1 h2 z"
+    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
+  from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
+  show "P x h h' r" .
+next
+qed (auto simp add: assms(2)[unfolded crel_def])
 
-lemmas crel_intro_all =
-  crelI crelI' crel_returnI crel_raiseI crel_ifI crel_option_caseI
-  crel_lengthI (* crel_newI *) crel_nthI crel_updI (* crel_of_listI crel_map_entryI crel_swapI crel_makeI crel_freezeI crel_mapI *)
-  (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
-  crel_assert
-
-
-end
\ No newline at end of file
+end
diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -5,7 +5,7 @@
 header {* An imperative implementation of Quicksort on arrays *}
 
 theory Imperative_Quicksort
-imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
+imports Imperative_HOL Subarray Multiset Efficient_Nat
 begin
 
 text {* We prove QuickSort correct in the Relational Calculus. *}
@@ -21,13 +21,20 @@
        return ()
      done)"
 
+lemma crel_swapI [crel_intros]:
+  assumes "i < Array.length a h" "j < Array.length a h"
+    "x = get_array a h ! i" "y = get_array a h ! j"
+    "h' = Array.change a j x (Array.change a i y h)"
+  shows "crel (swap a i j) h h' r"
+  unfolding swap_def using assms by (auto intro!: crel_intros)
+
 lemma swap_permutes:
   assumes "crel (swap a i j) h h' rs"
   shows "multiset_of (get_array a h') 
   = multiset_of (get_array a h)"
   using assms
   unfolding swap_def
-  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
+  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
 
 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
 where
@@ -55,7 +62,7 @@
   case (1 a l r p h h' rs)
   thus ?case
     unfolding part1.simps [of a l r p]
-    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
+    by (elim crel_bindE crel_ifE crel_returnE crel_nthE) (auto simp add: swap_permutes)
 qed
 
 lemma part_returns_index_in_bounds:
@@ -71,7 +78,7 @@
     case True (* Terminating case *)
     with cr `l \<le> r` show ?thesis
       unfolding part1.simps[of a l r p]
-      by (elim crelE crel_if crel_return crel_nth) auto
+      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   next
     case False (* recursive case *)
     note rec_condition = this
@@ -82,7 +89,7 @@
       with cr False
       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
+        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
       from rec_condition have "l + 1 \<le> r" by arith
       from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
       show ?thesis by simp
@@ -92,7 +99,7 @@
       obtain h1 where swp: "crel (swap a l r) h h1 ()"
         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
+        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
       from rec_condition have "l \<le> r - 1" by arith
       from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
     qed
@@ -112,12 +119,12 @@
     case True (* Terminating case *)
     with cr show ?thesis
       unfolding part1.simps[of a l r p]
-      by (elim crelE crel_if crel_return crel_nth) auto
+      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   next
     case False (* recursive case *)
     with cr 1 show ?thesis
       unfolding part1.simps [of a l r p] swap_def
-      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
+      by (auto elim!: crel_bindE crel_ifE crel_nthE crel_returnE crel_updE) fastsimp
   qed
 qed
 
@@ -134,7 +141,7 @@
     case True (* Terminating case *)
     with cr show ?thesis
       unfolding part1.simps[of a l r p]
-      by (elim crelE crel_if crel_return crel_nth) auto
+      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   next
     case False (* recursive case *)
     note rec_condition = this
@@ -145,7 +152,7 @@
       with cr False
       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
+        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
       from 1(1)[OF rec_condition True rec1]
       show ?thesis by fastsimp
     next
@@ -154,11 +161,11 @@
       obtain h1 where swp: "crel (swap a l r) h h1 ()"
         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
+        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
       from swp rec_condition have
         "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
         unfolding swap_def
-        by (elim crelE crel_nth crel_upd crel_return) auto
+        by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
       with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
     qed
   qed
@@ -179,7 +186,7 @@
     case True (* Terminating case *)
     with cr have "rs = r"
       unfolding part1.simps[of a l r p]
-      by (elim crelE crel_if crel_return crel_nth) auto
+      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
     with True
     show ?thesis by auto
   next
@@ -192,7 +199,7 @@
       with lr cr
       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
+        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
       from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
         by fastsimp
       have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
@@ -204,10 +211,10 @@
       obtain h1 where swp: "crel (swap a l r) h h1 ()"
         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
+        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
       from swp False have "get_array a h1 ! r \<ge> p"
         unfolding swap_def
-        by (auto simp add: Array.length_def elim!: crelE crel_nth crel_upd crel_return)
+        by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
       with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
         by fastsimp
       have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
@@ -238,7 +245,7 @@
 proof -
     from assms part_permutes swap_permutes show ?thesis
       unfolding partition.simps
-      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
+      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
 qed
 
 lemma partition_length_remains:
@@ -247,7 +254,7 @@
 proof -
   from assms part_length_remains show ?thesis
     unfolding partition.simps swap_def
-    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
+    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
 qed
 
 lemma partition_outer_remains:
@@ -257,7 +264,7 @@
 proof -
   from assms part_outer_remains part_returns_index_in_bounds show ?thesis
     unfolding partition.simps swap_def
-    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
+    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) fastsimp
 qed
 
 lemma partition_returns_index_in_bounds:
@@ -269,7 +276,7 @@
     and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
          else middle)"
     unfolding partition.simps
-    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
+    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
   from `l < r` have "l \<le> r - 1" by arith
   from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
 qed
@@ -286,17 +293,17 @@
     and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
          else middle)"
     unfolding partition.simps
-    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
+    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
   from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
     (Array.change a rs (get_array a h1 ! r) h1)"
     unfolding swap_def
-    by (elim crelE crel_return crel_nth crel_upd) simp
+    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
     unfolding swap_def
-    by (elim crelE crel_return crel_nth crel_upd) simp
+    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
-    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
-  from `l < r` have "l \<le> r - 1" by simp 
+    unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
+  from `l < r` have "l \<le> r - 1" by simp
   note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   from part_outer_remains[OF part] `l < r`
   have "get_array a h ! r = get_array a h1 ! r"
@@ -304,7 +311,7 @@
   with swap
   have right_remains: "get_array a h ! r = get_array a h' ! rs"
     unfolding swap_def
-    by (auto simp add: Array.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
+    by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
   from part_partitions [OF part]
   show ?thesis
   proof (cases "get_array a h1 ! middle \<le> ?pivot")
@@ -420,7 +427,7 @@
   case (1 a l r h h' rs)
   with partition_permutes show ?case
     unfolding quicksort.simps [of a l r]
-    by (elim crel_if crelE crel_assert crel_return) auto
+    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
 qed
 
 lemma length_remains:
@@ -431,7 +438,7 @@
   case (1 a l r h h' rs)
   with partition_length_remains show ?case
     unfolding quicksort.simps [of a l r]
-    by (elim crel_if crelE crel_assert crel_return) auto
+    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
 qed
 
 lemma quicksort_outer_remains:
@@ -446,7 +453,7 @@
     case False
     with cr have "h' = h"
       unfolding quicksort.simps [of a l r]
-      by (elim crel_if crel_return) auto
+      by (elim crel_ifE crel_returnE) auto
     thus ?thesis by simp
   next
   case True
@@ -469,7 +476,7 @@
     }
     with cr show ?thesis
       unfolding quicksort.simps [of a l r]
-      by (elim crel_if crelE crel_assert crel_return) auto
+      by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   qed
 qed
 
@@ -478,7 +485,7 @@
   shows "r \<le> l \<longrightarrow> h = h'"
   using assms
   unfolding quicksort.simps [of a l r]
-  by (elim crel_if crel_return) auto
+  by (elim crel_ifE crel_returnE) auto
  
 lemma quicksort_sorts:
   assumes "crel (quicksort a l r) h h' rs"
@@ -550,7 +557,7 @@
     }
     with True cr show ?thesis
       unfolding quicksort.simps [of a l r]
-      by (elim crel_if crel_return crelE crel_assert) auto
+      by (elim crel_ifE crel_returnE crel_bindE crel_assertE) auto
   qed
 qed
 
@@ -581,29 +588,28 @@
   using assms
 proof (induct a l r p arbitrary: h rule: part1.induct)
   case (1 a l r p)
-  thus ?case
-    unfolding part1.simps [of a l r] swap_def
-    by (auto simp add: execute_simps intro!: success_intros elim!: crelE crel_upd crel_nth crel_return)
+  thus ?case unfolding part1.simps [of a l r]
+  apply (auto intro!: success_intros del: success_ifI simp add: not_le)
+  apply (auto intro!: crel_intros crel_swapI)
+  done
 qed
 
-lemma success_ifI: (*FIXME move*)
-  assumes "c \<Longrightarrow> success t h" "\<not> c \<Longrightarrow> success e h"
-  shows "success (if c then t else e) h"
-  using assms
-  unfolding success_def
-  by auto
-
 lemma success_bindI' [success_intros]: (*FIXME move*)
   assumes "success f h"
   assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
   shows "success (f \<guillemotright>= g) h"
-  using assms by (auto intro!: successI elim!: successE simp add: bind_def crel_def success_def) blast
+using assms(1) proof (rule success_crelE)
+  fix h' r
+  assume "crel f h h' r"
+  moreover with assms(2) have "success (g r) h'" .
+  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_crelI)
+qed
 
 lemma success_partitionI:
   assumes "l < r" "l < Array.length a h" "r < Array.length a h"
   shows "success (partition a l r) h"
 using assms unfolding partition.simps swap_def
-apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crelE crel_upd crel_nth crel_return simp add:)
+apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:)
 apply (frule part_length_remains)
 apply (frule part_returns_index_in_bounds)
 apply auto
@@ -627,7 +633,7 @@
     apply auto
     apply (frule partition_returns_index_in_bounds)
     apply auto
-    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
+    apply (auto elim!: crel_assertE dest!: partition_length_remains length_remains)
     apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
     apply (erule disjE)
     apply auto
diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -5,7 +5,7 @@
 header {* An imperative in-place reversal on arrays *}
 
 theory Imperative_Reverse
-imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray
+imports Imperative_HOL Subarray
 begin
 
 hide_const (open) swap rev
@@ -36,7 +36,7 @@
       else if k = j then get_array a h ! i
       else get_array a h ! k)"
 using assms unfolding swap.simps
-by (elim crel_elim_all)
+by (elim crel_elims)
  (auto simp: length_def)
 
 lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
@@ -52,7 +52,7 @@
     obtain h' where
       swp: "crel (swap a i j) h h' ()"
       and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
-      by (auto elim: crel_elim_all)
+      by (auto elim: crel_elims)
     from rev 1 True
     have eq: "?P a (i + 1) (j - 1) h' h''" by auto
 
@@ -63,7 +63,7 @@
     case False
     with 1[unfolded rev.simps[of a i j]]
     show ?thesis
-      by (cases "k = j") (auto elim: crel_elim_all)
+      by (cases "k = j") (auto elim: crel_elims)
   qed
 qed
 
@@ -80,15 +80,15 @@
     obtain h' where
       swp: "crel (swap a i j) h h' ()"
       and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
-      by (auto elim: crel_elim_all)
+      by (auto elim: crel_elims)
     from swp rev 1 True show ?thesis
       unfolding swap.simps
-      by (elim crel_elim_all) fastsimp
+      by (elim crel_elims) fastsimp
   next
     case False
     with 1[unfolded rev.simps[of a i j]]
     show ?thesis
-      by (auto elim: crel_elim_all)
+      by (auto elim: crel_elims)
   qed
 qed
 
@@ -112,7 +112,7 @@
   shows "get_array a h' = List.rev (get_array a h)"
   using rev2_rev'[OF assms] rev_length[OF assms] assms
     by (cases "Array.length a h = 0", auto simp add: Array.length_def
-      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all)
+      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   (drule sym[of "List.length (get_array a h)"], simp)
 
 end
diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -5,7 +5,7 @@
 header {* Linked Lists by ML references *}
 
 theory Linked_Lists
-imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Code_Integer
+imports Imperative_HOL Code_Integer
 begin
 
 section {* Definition of Linked Lists *}
@@ -42,7 +42,7 @@
 definition
   traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
 where
-  "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
+[code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
                                 | Node x r \<Rightarrow> (do tl \<leftarrow> Ref.lookup r;
                                                   return (Inr tl) done))
                    (\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
@@ -452,18 +452,37 @@
     by simp
 qed
 
+lemma crel_ref:
+  assumes "crel (ref v) h h' x"
+  obtains "Ref.get h' x = v"
+  and "\<not> Ref.present h x"
+  and "Ref.present h' x"
+  and "\<forall>y. Ref.present h y \<longrightarrow> Ref.get h y = Ref.get h' y"
+ (* and "lim h' = Suc (lim h)" *)
+  and "\<forall>y. Ref.present h y \<longrightarrow> Ref.present h' y"
+  using assms
+  unfolding Ref.ref_def
+  apply (elim crel_heapE)
+  unfolding Ref.alloc_def
+  apply (simp add: Let_def)
+  unfolding Ref.present_def
+  apply auto
+  unfolding Ref.get_def Ref.set_def
+  apply auto
+  done
+
 lemma make_llist:
 assumes "crel (make_llist xs) h h' r"
 shows "list_of h' r xs \<and> (\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref \<in> (set rs). Ref.present h' ref))"
 using assms 
 proof (induct xs arbitrary: h h' r)
-  case Nil thus ?case by (auto elim: crel_return simp add: make_llist.simps)
+  case Nil thus ?case by (auto elim: crel_returnE simp add: make_llist.simps)
 next
   case (Cons x xs')
   from Cons.prems obtain h1 r1 r' where make_llist: "crel (make_llist xs') h h1 r1"
     and crel_refnew:"crel (ref r1) h1 h' r'" and Node: "r = Node x r'"
     unfolding make_llist.simps
-    by (auto elim!: crelE crel_return)
+    by (auto elim!: crel_bindE crel_returnE)
   from Cons.hyps[OF make_llist] have list_of_h1: "list_of h1 r1 xs'" ..
   from Cons.hyps[OF make_llist] obtain rs' where rs'_def: "refs_of h1 r1 rs'" by (auto intro: list_of_refs_of)
   from Cons.hyps[OF make_llist] rs'_def have refs_present: "\<forall>ref\<in>set rs'. Ref.present h1 ref" by simp
@@ -472,11 +491,11 @@
     by (auto elim!: crel_ref dest: refs_of_is_fun)
   with list_of_invariant[OF list_of_h1 refs_unchanged] Node crel_refnew have fstgoal: "list_of h' r (x # xs')"
     unfolding list_of.simps
-    by (auto elim!: crel_ref)
+    by (auto elim!: crel_refE)
   from refs_unchanged rs'_def have refs_still_present: "\<forall>ref\<in>set rs'. Ref.present h' ref" by auto
   from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node crel_refnew refs_still_present
   have sndgoal: "\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref\<in>set rs. Ref.present h' ref)"
-    by (fastsimp elim!: crel_ref dest: refs_of_is_fun)
+    by (fastsimp elim!: crel_refE dest: refs_of_is_fun)
   from fstgoal sndgoal show ?case ..
 qed
 
@@ -489,7 +508,7 @@
   case (Cons x xs)
   thus ?case
   apply (cases n, auto)
-  by (auto intro!: crelI crel_returnI crel_lookupI)
+  by (auto intro!: crel_bindI crel_returnI crel_lookupI)
 qed
 
 lemma traverse_make_llist':
@@ -499,7 +518,7 @@
   from crel obtain h1 r1
     where makell: "crel (make_llist xs) h h1 r1"
     and trav: "crel (traverse r1) h1 h' r"
-    by (auto elim!: crelE)
+    by (auto elim!: crel_bindE)
   from make_llist[OF makell] have "list_of h1 r1 xs" ..
   from traverse [OF this] trav show ?thesis
     using crel_deterministic by fastsimp
@@ -551,7 +570,7 @@
   case Nil
   thus ?case
     unfolding rev'_simps[of q p] list_of'_def
-    by (auto elim!: crelE crel_lookup crel_return)
+    by (auto elim!: crel_bindE crel_lookupE crel_returnE)
 next
   case (Cons x xs)
   (*"LinkedList.list_of h' (get_ref v h') (List.rev xs @ x # qsa)"*)
@@ -561,7 +580,7 @@
     and list_of'_ref: "list_of' h ref xs"
     unfolding list_of'_def by (cases "Ref.get h p", auto)
   from p_is_Node Cons(2) have crel_rev': "crel (rev' (p, ref)) (Ref.set p (Node x q) h) h' v"
-    by (auto simp add: rev'_simps [of q p] elim!: crelE crel_lookup crel_update)
+    by (auto simp add: rev'_simps [of q p] elim!: crel_bindE crel_lookupE crel_updateE)
   from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of')
   from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of')
   from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp
@@ -602,7 +621,7 @@
 proof (cases r)
   case Empty
   with list_of_h crel_rev show ?thesis
-    by (auto simp add: list_of_Empty elim!: crel_return)
+    by (auto simp add: list_of_Empty elim!: crel_returnE)
 next
   case (Node x ps)
   with crel_rev obtain p q h1 h2 h3 v where
@@ -611,7 +630,7 @@
     and crel_rev':"crel (rev' (q, p)) h2 h3 v"
     and lookup: "crel (!v) h3 h' r'"
     using rev.simps
-    by (auto elim!: crelE)
+    by (auto elim!: crel_bindE)
   from init have a1:"list_of' h2 q []"
     unfolding list_of'_def
     by (auto elim!: crel_ref)
@@ -622,7 +641,7 @@
   from init this Node have a2: "list_of' h2 p xs"
     apply -
     unfolding list_of'_def
-    apply (auto elim!: crel_ref)
+    apply (auto elim!: crel_refE)
     done
   from init have refs_of_q: "refs_of' h2 q [q]"
     by (auto elim!: crel_ref)
@@ -633,15 +652,15 @@
     by (fastsimp elim!: crel_ref dest: refs_of'_is_fun)
   from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" .
   with init have refs_of_p: "refs_of' h2 p (p#refs)"
-    by (auto elim!: crel_ref simp add: refs_of'_def')
+    by (auto elim!: crel_refE simp add: refs_of'_def')
   with init all_ref_present have q_is_new: "q \<notin> set (p#refs)"
-    by (auto elim!: crel_ref intro!: Ref.noteq_I)
+    by (auto elim!: crel_refE intro!: Ref.noteq_I)
   from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}"
     by (fastsimp simp only: set.simps dest: refs_of'_is_fun)
   from rev'_invariant [OF crel_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
     unfolding list_of'_def by auto
   with lookup show ?thesis
-    by (auto elim: crel_lookup)
+    by (auto elim: crel_lookupE)
 qed
 
 
@@ -796,13 +815,13 @@
   case (1 ys p q)
   from 1(3-4) have "h = h' \<and> r = q"
     unfolding merge_simps[of p q]
-    by (auto elim!: crel_lookup crelE crel_return)
+    by (auto elim!: crel_lookupE crel_bindE crel_returnE)
   with assms(4)[OF 1(1) 1(2) 1(3)] show ?case by simp
 next
   case (2 x xs' p q pn)
   from 2(3-5) have "h = h' \<and> r = p"
     unfolding merge_simps[of p q]
-    by (auto elim!: crel_lookup crelE crel_return)
+    by (auto elim!: crel_lookupE crel_bindE crel_returnE)
   with assms(5)[OF 2(1-4)] show ?case by simp
 next
   case (3 x xs' y ys' p q pn qn)
@@ -810,7 +829,7 @@
     1: "crel (merge pn q) h h1 r1" 
     and 2: "h' = Ref.set p (Node x r1) h1 \<and> r = p"
     unfolding merge_simps[of p q]
-    by (auto elim!: crel_lookup crelE crel_return crel_if crel_update)
+    by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
   from 3(6)[OF 1] assms(6) [OF 3(1-5)] 1 2 show ?case by simp
 next
   case (4 x xs' y ys' p q pn qn)
@@ -818,7 +837,7 @@
     1: "crel (merge p qn) h h1 r1" 
     and 2: "h' = Ref.set q (Node y r1) h1 \<and> r = q"
     unfolding merge_simps[of p q]
-    by (auto elim!: crel_lookup crelE crel_return crel_if crel_update)
+    by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
   from 4(6)[OF 1] assms(7) [OF 4(1-5)] 1 2 show ?case by simp
 qed
 
diff -r cddb3106adb8 -r 1bec64044b5e src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 12 11:39:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 12 16:05:08 2010 +0200
@@ -5,7 +5,7 @@
 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 *}
@@ -217,12 +217,12 @@
 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:
@@ -233,12 +233,12 @@
   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
@@ -254,12 +254,12 @@
   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
@@ -312,7 +312,7 @@
   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
@@ -323,12 +323,12 @@
   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:
@@ -337,9 +337,9 @@
 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
 
@@ -349,9 +349,9 @@
 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"
@@ -359,9 +359,9 @@
 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:
@@ -372,18 +372,18 @@
   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
 
 
@@ -466,7 +466,7 @@
   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)"
@@ -494,7 +494,7 @@
   }
   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:
@@ -506,7 +506,7 @@
 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)
   {
@@ -523,7 +523,7 @@
   }
   with Cons show ?case
     unfolding foldM.simps
-    by (elim crelE) auto
+    by (elim crel_bindE) auto
 qed
 
 
@@ -536,9 +536,9 @@
   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)
@@ -549,24 +549,24 @@
   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
   
 
@@ -576,13 +576,13 @@
   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)