src/HOL/Imperative_HOL/Array.thy
changeset 37771 1bec64044b5e
parent 37758 bf86a65403a8
child 37787 30dc3abf4a58
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 12 11:39:27 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 12 16:05:08 2010 +0200
     1.3 @@ -155,6 +155,14 @@
     1.4    "array_present a (change b i v h) = array_present a h"
     1.5    by (simp add: change_def array_present_def set_array_def get_array_def)
     1.6  
     1.7 +lemma array_present_array [simp]:
     1.8 +  "array_present (fst (array xs h)) (snd (array xs h))"
     1.9 +  by (simp add: array_present_def array_def set_array_def Let_def)
    1.10 +
    1.11 +lemma not_array_present_array [simp]:
    1.12 +  "\<not> array_present (fst (array xs h)) h"
    1.13 +  by (simp add: array_present_def array_def Let_def)
    1.14 +
    1.15  
    1.16  text {* Monad operations *}
    1.17  
    1.18 @@ -166,6 +174,17 @@
    1.19    "success (new n x) h"
    1.20    by (simp add: new_def)
    1.21  
    1.22 +lemma crel_newI [crel_intros]:
    1.23 +  assumes "(a, h') = array (replicate n x) h"
    1.24 +  shows "crel (new n x) h h' a"
    1.25 +  by (rule crelI) (simp add: assms)
    1.26 +
    1.27 +lemma crel_newE [crel_elims]:
    1.28 +  assumes "crel (new n x) h h' r"
    1.29 +  obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
    1.30 +    "get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h"
    1.31 +  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.32 +
    1.33  lemma execute_of_list [simp, execute_simps]:
    1.34    "execute (of_list xs) h = Some (array xs h)"
    1.35    by (simp add: of_list_def)
    1.36 @@ -174,6 +193,17 @@
    1.37    "success (of_list xs) h"
    1.38    by (simp add: of_list_def)
    1.39  
    1.40 +lemma crel_of_listI [crel_intros]:
    1.41 +  assumes "(a, h') = array xs h"
    1.42 +  shows "crel (of_list xs) h h' a"
    1.43 +  by (rule crelI) (simp add: assms)
    1.44 +
    1.45 +lemma crel_of_listE [crel_elims]:
    1.46 +  assumes "crel (of_list xs) h h' r"
    1.47 +  obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
    1.48 +    "get_array r h' = xs" "array_present r h'" "\<not> array_present r h"
    1.49 +  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.50 +
    1.51  lemma execute_make [simp, execute_simps]:
    1.52    "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
    1.53    by (simp add: make_def)
    1.54 @@ -182,6 +212,17 @@
    1.55    "success (make n f) h"
    1.56    by (simp add: make_def)
    1.57  
    1.58 +lemma crel_makeI [crel_intros]:
    1.59 +  assumes "(a, h') = array (map f [0 ..< n]) h"
    1.60 +  shows "crel (make n f) h h' a"
    1.61 +  by (rule crelI) (simp add: assms)
    1.62 +
    1.63 +lemma crel_makeE [crel_elims]:
    1.64 +  assumes "crel (make n f) h h' r"
    1.65 +  obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
    1.66 +    "get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h"
    1.67 +  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.68 +
    1.69  lemma execute_len [simp, execute_simps]:
    1.70    "execute (len a) h = Some (length a h, h)"
    1.71    by (simp add: len_def)
    1.72 @@ -190,6 +231,16 @@
    1.73    "success (len a) h"
    1.74    by (simp add: len_def)
    1.75  
    1.76 +lemma crel_lengthI [crel_intros]:
    1.77 +  assumes "h' = h" "r = length a h"
    1.78 +  shows "crel (len a) h h' r"
    1.79 +  by (rule crelI) (simp add: assms)
    1.80 +
    1.81 +lemma crel_lengthE [crel_elims]:
    1.82 +  assumes "crel (len a) h h' r"
    1.83 +  obtains "r = length a h'" "h' = h" 
    1.84 +  using assms by (rule crelE) simp
    1.85 +
    1.86  lemma execute_nth [execute_simps]:
    1.87    "i < length a h \<Longrightarrow>
    1.88      execute (nth a i) h = Some (get_array a h ! i, h)"
    1.89 @@ -200,38 +251,82 @@
    1.90    "i < length a h \<Longrightarrow> success (nth a i) h"
    1.91    by (auto intro: success_intros simp add: nth_def)
    1.92  
    1.93 +lemma crel_nthI [crel_intros]:
    1.94 +  assumes "i < length a h" "h' = h" "r = get_array a h ! i"
    1.95 +  shows "crel (nth a i) h h' r"
    1.96 +  by (rule crelI) (insert assms, simp add: execute_simps)
    1.97 +
    1.98 +lemma crel_nthE [crel_elims]:
    1.99 +  assumes "crel (nth a i) h h' r"
   1.100 +  obtains "i < length a h" "r = get_array a h ! i" "h' = h"
   1.101 +  using assms by (rule crelE)
   1.102 +    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.103 +
   1.104  lemma execute_upd [execute_simps]:
   1.105    "i < length a h \<Longrightarrow>
   1.106      execute (upd i x a) h = Some (a, change a i x h)"
   1.107 -  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.108 +  "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
   1.109    by (simp_all add: upd_def execute_simps)
   1.110  
   1.111  lemma success_updI [success_intros]:
   1.112    "i < length a h \<Longrightarrow> success (upd i x a) h"
   1.113    by (auto intro: success_intros simp add: upd_def)
   1.114  
   1.115 +lemma crel_updI [crel_intros]:
   1.116 +  assumes "i < length a h" "h' = change a i v h"
   1.117 +  shows "crel (upd i v a) h h' a"
   1.118 +  by (rule crelI) (insert assms, simp add: execute_simps)
   1.119 +
   1.120 +lemma crel_updE [crel_elims]:
   1.121 +  assumes "crel (upd i v a) h h' r"
   1.122 +  obtains "r = a" "h' = change a i v h" "i < length a h"
   1.123 +  using assms by (rule crelE)
   1.124 +    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.125 +
   1.126  lemma execute_map_entry [execute_simps]:
   1.127    "i < length a h \<Longrightarrow>
   1.128     execute (map_entry i f a) h =
   1.129        Some (a, change a i (f (get_array a h ! i)) h)"
   1.130 -  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.131 +  "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
   1.132    by (simp_all add: map_entry_def execute_simps)
   1.133  
   1.134  lemma success_map_entryI [success_intros]:
   1.135    "i < length a h \<Longrightarrow> success (map_entry i f a) h"
   1.136    by (auto intro: success_intros simp add: map_entry_def)
   1.137  
   1.138 +lemma crel_map_entryI [crel_intros]:
   1.139 +  assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a"
   1.140 +  shows "crel (map_entry i f a) h h' r"
   1.141 +  by (rule crelI) (insert assms, simp add: execute_simps)
   1.142 +
   1.143 +lemma crel_map_entryE [crel_elims]:
   1.144 +  assumes "crel (map_entry i f a) h h' r"
   1.145 +  obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h"
   1.146 +  using assms by (rule crelE)
   1.147 +    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.148 +
   1.149  lemma execute_swap [execute_simps]:
   1.150    "i < length a h \<Longrightarrow>
   1.151     execute (swap i x a) h =
   1.152        Some (get_array a h ! i, change a i x h)"
   1.153 -  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.154 +  "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
   1.155    by (simp_all add: swap_def execute_simps)
   1.156  
   1.157  lemma success_swapI [success_intros]:
   1.158    "i < length a h \<Longrightarrow> success (swap i x a) h"
   1.159    by (auto intro: success_intros simp add: swap_def)
   1.160  
   1.161 +lemma crel_swapI [crel_intros]:
   1.162 +  assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i"
   1.163 +  shows "crel (swap i x a) h h' r"
   1.164 +  by (rule crelI) (insert assms, simp add: execute_simps)
   1.165 +
   1.166 +lemma crel_swapE [crel_elims]:
   1.167 +  assumes "crel (swap i x a) h h' r"
   1.168 +  obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h"
   1.169 +  using assms by (rule crelE)
   1.170 +    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.171 +
   1.172  lemma execute_freeze [simp, execute_simps]:
   1.173    "execute (freeze a) h = Some (get_array a h, h)"
   1.174    by (simp add: freeze_def)
   1.175 @@ -240,6 +335,16 @@
   1.176    "success (freeze a) h"
   1.177    by (simp add: freeze_def)
   1.178  
   1.179 +lemma crel_freezeI [crel_intros]:
   1.180 +  assumes "h' = h" "r = get_array a h"
   1.181 +  shows "crel (freeze a) h h' r"
   1.182 +  by (rule crelI) (insert assms, simp add: execute_simps)
   1.183 +
   1.184 +lemma crel_freezeE [crel_elims]:
   1.185 +  assumes "crel (freeze a) h h' r"
   1.186 +  obtains "h' = h" "r = get_array a h"
   1.187 +  using assms by (rule crelE) simp
   1.188 +
   1.189  lemma upd_return:
   1.190    "upd i x a \<guillemotright> return a = upd i x a"
   1.191    by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
   1.192 @@ -252,7 +357,7 @@
   1.193    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   1.194    by (rule Heap_eqI) (simp add: map_nth)
   1.195  
   1.196 -hide_const (open) new map
   1.197 +hide_const (open) new
   1.198  
   1.199  
   1.200  subsection {* Code generator setup *}
   1.201 @@ -339,7 +444,7 @@
   1.202        n \<leftarrow> len a;
   1.203        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.204      done) h = Some (get_array a h, h)"
   1.205 -    by (auto intro: execute_eq_SomeI)
   1.206 +    by (auto intro: execute_bind_eq_SomeI)
   1.207    then show "execute (freeze a) h = execute (do
   1.208        n \<leftarrow> len a;
   1.209        Heap_Monad.fold_map (Array.nth a) [0..<n]