src/HOL/Imperative_HOL/Array.thy
changeset 37787 30dc3abf4a58
parent 37771 1bec64044b5e
child 37792 ba0bc31b90d7
child 37796 08bd610b2583
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 02:29:05 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 11:38:03 2010 +0200
     1.3 @@ -166,80 +166,80 @@
     1.4  
     1.5  text {* Monad operations *}
     1.6  
     1.7 -lemma execute_new [simp, execute_simps]:
     1.8 +lemma execute_new [execute_simps]:
     1.9    "execute (new n x) h = Some (array (replicate n x) h)"
    1.10 -  by (simp add: new_def)
    1.11 +  by (simp add: new_def execute_simps)
    1.12  
    1.13 -lemma success_newI [iff, success_intros]:
    1.14 +lemma success_newI [success_intros]:
    1.15    "success (new n x) h"
    1.16 -  by (simp add: new_def)
    1.17 +  by (auto intro: success_intros simp add: new_def)
    1.18  
    1.19  lemma crel_newI [crel_intros]:
    1.20    assumes "(a, h') = array (replicate n x) h"
    1.21    shows "crel (new n x) h h' a"
    1.22 -  by (rule crelI) (simp add: assms)
    1.23 +  by (rule crelI) (simp add: assms execute_simps)
    1.24  
    1.25  lemma crel_newE [crel_elims]:
    1.26    assumes "crel (new n x) h h' r"
    1.27    obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
    1.28      "get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h"
    1.29 -  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.30 +  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.31  
    1.32 -lemma execute_of_list [simp, execute_simps]:
    1.33 +lemma execute_of_list [execute_simps]:
    1.34    "execute (of_list xs) h = Some (array xs h)"
    1.35 -  by (simp add: of_list_def)
    1.36 +  by (simp add: of_list_def execute_simps)
    1.37  
    1.38 -lemma success_of_listI [iff, success_intros]:
    1.39 +lemma success_of_listI [success_intros]:
    1.40    "success (of_list xs) h"
    1.41 -  by (simp add: of_list_def)
    1.42 +  by (auto intro: success_intros simp add: of_list_def)
    1.43  
    1.44  lemma crel_of_listI [crel_intros]:
    1.45    assumes "(a, h') = array xs h"
    1.46    shows "crel (of_list xs) h h' a"
    1.47 -  by (rule crelI) (simp add: assms)
    1.48 +  by (rule crelI) (simp add: assms execute_simps)
    1.49  
    1.50  lemma crel_of_listE [crel_elims]:
    1.51    assumes "crel (of_list xs) h h' r"
    1.52    obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
    1.53      "get_array r h' = xs" "array_present r h'" "\<not> array_present r h"
    1.54 -  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.55 +  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.56  
    1.57 -lemma execute_make [simp, execute_simps]:
    1.58 +lemma execute_make [execute_simps]:
    1.59    "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
    1.60 -  by (simp add: make_def)
    1.61 +  by (simp add: make_def execute_simps)
    1.62  
    1.63 -lemma success_makeI [iff, success_intros]:
    1.64 +lemma success_makeI [success_intros]:
    1.65    "success (make n f) h"
    1.66 -  by (simp add: make_def)
    1.67 +  by (auto intro: success_intros simp add: make_def)
    1.68  
    1.69  lemma crel_makeI [crel_intros]:
    1.70    assumes "(a, h') = array (map f [0 ..< n]) h"
    1.71    shows "crel (make n f) h h' a"
    1.72 -  by (rule crelI) (simp add: assms)
    1.73 +  by (rule crelI) (simp add: assms execute_simps)
    1.74  
    1.75  lemma crel_makeE [crel_elims]:
    1.76    assumes "crel (make n f) h h' r"
    1.77    obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
    1.78      "get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h"
    1.79 -  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.80 +  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.81  
    1.82 -lemma execute_len [simp, execute_simps]:
    1.83 +lemma execute_len [execute_simps]:
    1.84    "execute (len a) h = Some (length a h, h)"
    1.85 -  by (simp add: len_def)
    1.86 +  by (simp add: len_def execute_simps)
    1.87  
    1.88 -lemma success_lenI [iff, success_intros]:
    1.89 +lemma success_lenI [success_intros]:
    1.90    "success (len a) h"
    1.91 -  by (simp add: len_def)
    1.92 +  by (auto intro: success_intros simp add: len_def)
    1.93  
    1.94  lemma crel_lengthI [crel_intros]:
    1.95    assumes "h' = h" "r = length a h"
    1.96    shows "crel (len a) h h' r"
    1.97 -  by (rule crelI) (simp add: assms)
    1.98 +  by (rule crelI) (simp add: assms execute_simps)
    1.99  
   1.100  lemma crel_lengthE [crel_elims]:
   1.101    assumes "crel (len a) h h' r"
   1.102    obtains "r = length a h'" "h' = h" 
   1.103 -  using assms by (rule crelE) simp
   1.104 +  using assms by (rule crelE) (simp add: execute_simps)
   1.105  
   1.106  lemma execute_nth [execute_simps]:
   1.107    "i < length a h \<Longrightarrow>
   1.108 @@ -327,13 +327,13 @@
   1.109    using assms by (rule crelE)
   1.110      (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.111  
   1.112 -lemma execute_freeze [simp, execute_simps]:
   1.113 +lemma execute_freeze [execute_simps]:
   1.114    "execute (freeze a) h = Some (get_array a h, h)"
   1.115 -  by (simp add: freeze_def)
   1.116 +  by (simp add: freeze_def execute_simps)
   1.117  
   1.118 -lemma success_freezeI [iff, success_intros]:
   1.119 +lemma success_freezeI [success_intros]:
   1.120    "success (freeze a) h"
   1.121 -  by (simp add: freeze_def)
   1.122 +  by (auto intro: success_intros simp add: freeze_def)
   1.123  
   1.124  lemma crel_freezeI [crel_intros]:
   1.125    assumes "h' = h" "r = get_array a h"
   1.126 @@ -343,19 +343,19 @@
   1.127  lemma crel_freezeE [crel_elims]:
   1.128    assumes "crel (freeze a) h h' r"
   1.129    obtains "h' = h" "r = get_array a h"
   1.130 -  using assms by (rule crelE) simp
   1.131 +  using assms by (rule crelE) (simp add: execute_simps)
   1.132  
   1.133  lemma upd_return:
   1.134    "upd i x a \<guillemotright> return a = upd i x a"
   1.135 -  by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
   1.136 +  by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps)
   1.137  
   1.138  lemma array_make:
   1.139    "new n x = make n (\<lambda>_. x)"
   1.140 -  by (rule Heap_eqI) (simp add: map_replicate_trivial)
   1.141 +  by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps)
   1.142  
   1.143  lemma array_of_list_make:
   1.144    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   1.145 -  by (rule Heap_eqI) (simp add: map_nth)
   1.146 +  by (rule Heap_eqI) (simp add: map_nth execute_simps)
   1.147  
   1.148  hide_const (open) new
   1.149  
   1.150 @@ -444,11 +444,11 @@
   1.151        n \<leftarrow> len a;
   1.152        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.153      done) h = Some (get_array a h, h)"
   1.154 -    by (auto intro: execute_bind_eq_SomeI)
   1.155 +    by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
   1.156    then show "execute (freeze a) h = execute (do
   1.157        n \<leftarrow> len a;
   1.158        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.159 -    done) h" by simp
   1.160 +    done) h" by (simp add: execute_simps)
   1.161  qed
   1.162  
   1.163  hide_const (open) new' of_list' make' len' nth' upd'