1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Imperative_HOL/Relational.thy Thu Jan 08 17:10:41 2009 +0100
1.3 @@ -0,0 +1,700 @@
1.4 +theory Relational
1.5 +imports Array Ref
1.6 +begin
1.7 +
1.8 +section{* Definition of the Relational framework *}
1.9 +
1.10 +text {* The crel predicate states that when a computation c runs with the heap h
1.11 + will result in return value r and a heap h' (if no exception occurs). *}
1.12 +
1.13 +definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
1.14 +where
1.15 + crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = (Inl r, h')"
1.16 +
1.17 +lemma crel_def: -- FIXME
1.18 + "crel c h h' r \<longleftrightarrow> (Inl r, h') = Heap_Monad.execute c h"
1.19 + unfolding crel_def' by auto
1.20 +
1.21 +lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
1.22 +unfolding crel_def' by auto
1.23 +
1.24 +section {* Elimination rules *}
1.25 +
1.26 +text {* For all commands, we define simple elimination rules. *}
1.27 +(* FIXME: consumes 1 necessary ?? *)
1.28 +
1.29 +subsection {* Elimination rules for basic monadic commands *}
1.30 +
1.31 +lemma crelE[consumes 1]:
1.32 + assumes "crel (f >>= g) h h'' r'"
1.33 + obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
1.34 + using assms
1.35 + by (auto simp add: crel_def bindM_def Let_def prod_case_beta split_def Pair_fst_snd_eq split add: sum.split_asm)
1.36 +
1.37 +lemma crelE'[consumes 1]:
1.38 + assumes "crel (f >> g) h h'' r'"
1.39 + obtains h' r where "crel f h h' r" "crel g h' h'' r'"
1.40 + using assms
1.41 + by (elim crelE) auto
1.42 +
1.43 +lemma crel_return[consumes 1]:
1.44 + assumes "crel (return x) h h' r"
1.45 + obtains "r = x" "h = h'"
1.46 + using assms
1.47 + unfolding crel_def return_def by simp
1.48 +
1.49 +lemma crel_raise[consumes 1]:
1.50 + assumes "crel (raise x) h h' r"
1.51 + obtains "False"
1.52 + using assms
1.53 + unfolding crel_def raise_def by simp
1.54 +
1.55 +lemma crel_if:
1.56 + assumes "crel (if c then t else e) h h' r"
1.57 + obtains "c" "crel t h h' r"
1.58 + | "\<not>c" "crel e h h' r"
1.59 + using assms
1.60 + unfolding crel_def by auto
1.61 +
1.62 +lemma crel_option_case:
1.63 + assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
1.64 + obtains "x = None" "crel n h h' r"
1.65 + | y where "x = Some y" "crel (s y) h h' r"
1.66 + using assms
1.67 + unfolding crel_def by auto
1.68 +
1.69 +lemma crel_mapM:
1.70 + assumes "crel (mapM f xs) h h' r"
1.71 + assumes "\<And>h h'. P f [] h h' []"
1.72 + assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (mapM f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
1.73 + shows "P f xs h h' r"
1.74 +using assms(1)
1.75 +proof (induct xs arbitrary: h h' r)
1.76 + case Nil with assms(2) show ?case
1.77 + by (auto elim: crel_return)
1.78 +next
1.79 + case (Cons x xs)
1.80 + from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
1.81 + and crel_mapM: "crel (mapM f xs) h1 h' ys"
1.82 + and r_def: "r = y#ys"
1.83 + unfolding mapM.simps
1.84 + by (auto elim!: crelE crel_return)
1.85 + from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
1.86 + show ?case by auto
1.87 +qed
1.88 +
1.89 +lemma crel_heap:
1.90 + assumes "crel (Heap_Monad.heap f) h h' r"
1.91 + obtains "h' = snd (f h)" "r = fst (f h)"
1.92 + using assms
1.93 + unfolding heap_def crel_def apfst_def split_def prod_fun_def by simp_all
1.94 +
1.95 +subsection {* Elimination rules for array commands *}
1.96 +
1.97 +lemma crel_length:
1.98 + assumes "crel (length a) h h' r"
1.99 + obtains "h = h'" "r = Heap.length a h'"
1.100 + using assms
1.101 + unfolding length_def
1.102 + by (elim crel_heap) simp
1.103 +
1.104 +(* Strong version of the lemma for this operation is missing *)
1.105 +lemma crel_new_weak:
1.106 + assumes "crel (Array.new n v) h h' r"
1.107 + obtains "get_array r h' = List.replicate n v"
1.108 + using assms unfolding Array.new_def
1.109 + by (elim crel_heap) (auto simp:Heap.array_def Let_def split_def)
1.110 +
1.111 +lemma crel_nth[consumes 1]:
1.112 + assumes "crel (nth a i) h h' r"
1.113 + obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
1.114 + using assms
1.115 + unfolding nth_def
1.116 + by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
1.117 +
1.118 +lemma crel_upd[consumes 1]:
1.119 + assumes "crel (upd i v a) h h' r"
1.120 + obtains "r = a" "h' = Heap.upd a i v h"
1.121 + using assms
1.122 + unfolding upd_def
1.123 + by (elim crelE crel_if crel_return crel_raise
1.124 + crel_length crel_heap) auto
1.125 +
1.126 +(* Strong version of the lemma for this operation is missing *)
1.127 +lemma crel_of_list_weak:
1.128 + assumes "crel (Array.of_list xs) h h' r"
1.129 + obtains "get_array r h' = xs"
1.130 + using assms
1.131 + unfolding of_list_def
1.132 + by (elim crel_heap) (simp add:get_array_init_array_list)
1.133 +
1.134 +lemma crel_map_entry:
1.135 + assumes "crel (Array.map_entry i f a) h h' r"
1.136 + obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
1.137 + using assms
1.138 + unfolding Array.map_entry_def
1.139 + by (elim crelE crel_upd crel_nth) auto
1.140 +
1.141 +lemma crel_swap:
1.142 + assumes "crel (Array.swap i x a) h h' r"
1.143 + obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
1.144 + using assms
1.145 + unfolding Array.swap_def
1.146 + by (elim crelE crel_upd crel_nth crel_return) auto
1.147 +
1.148 +(* Strong version of the lemma for this operation is missing *)
1.149 +lemma crel_make_weak:
1.150 + assumes "crel (Array.make n f) h h' r"
1.151 + obtains "i < n \<Longrightarrow> get_array r h' ! i = f i"
1.152 + using assms
1.153 + unfolding Array.make_def
1.154 + by (elim crel_of_list_weak) auto
1.155 +
1.156 +lemma upt_conv_Cons':
1.157 + assumes "Suc a \<le> b"
1.158 + shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
1.159 +proof -
1.160 + from assms have l: "b - Suc a < b" by arith
1.161 + from assms have "Suc (b - Suc a) = b - a" by arith
1.162 + with l show ?thesis by (simp add: upt_conv_Cons)
1.163 +qed
1.164 +
1.165 +lemma crel_mapM_nth:
1.166 + assumes
1.167 + "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' xs"
1.168 + assumes "n \<le> Heap.length a h"
1.169 + shows "h = h' \<and> xs = drop (Heap.length a h - n) (get_array a h)"
1.170 +using assms
1.171 +proof (induct n arbitrary: xs h h')
1.172 + case 0 thus ?case
1.173 + by (auto elim!: crel_return simp add: Heap.length_def)
1.174 +next
1.175 + case (Suc n)
1.176 + from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
1.177 + by (simp add: upt_conv_Cons')
1.178 + with Suc(2) obtain r where
1.179 + crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
1.180 + and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
1.181 + by (auto elim!: crelE crel_nth crel_return)
1.182 + from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)"
1.183 + by arith
1.184 + with Suc.hyps[OF crel_mapM] xs_def show ?case
1.185 + unfolding Heap.length_def
1.186 + by (auto simp add: nth_drop')
1.187 +qed
1.188 +
1.189 +lemma crel_freeze:
1.190 + assumes "crel (Array.freeze a) h h' xs"
1.191 + obtains "h = h'" "xs = get_array a h"
1.192 +proof
1.193 + from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
1.194 + unfolding freeze_def
1.195 + by (auto elim: crelE crel_length)
1.196 + hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
1.197 + by simp
1.198 + from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
1.199 +qed
1.200 +
1.201 +lemma crel_mapM_map_entry_remains:
1.202 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
1.203 + assumes "i < Heap.length a h - n"
1.204 + shows "get_array a h ! i = get_array a h' ! i"
1.205 +using assms
1.206 +proof (induct n arbitrary: h h' r)
1.207 + case 0
1.208 + thus ?case
1.209 + by (auto elim: crel_return)
1.210 +next
1.211 + case (Suc n)
1.212 + let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
1.213 + from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
1.214 + by (simp add: upt_conv_Cons')
1.215 + from Suc(2) this obtain r where
1.216 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
1.217 + by (auto simp add: elim!: crelE crel_map_entry crel_return)
1.218 + have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
1.219 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
1.220 + by simp
1.221 + from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
1.222 +qed
1.223 +
1.224 +lemma crel_mapM_map_entry_changes:
1.225 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
1.226 + assumes "n \<le> Heap.length a h"
1.227 + assumes "i \<ge> Heap.length a h - n"
1.228 + assumes "i < Heap.length a h"
1.229 + shows "get_array a h' ! i = f (get_array a h ! i)"
1.230 +using assms
1.231 +proof (induct n arbitrary: h h' r)
1.232 + case 0
1.233 + thus ?case
1.234 + by (auto elim!: crel_return)
1.235 +next
1.236 + case (Suc n)
1.237 + let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
1.238 + from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
1.239 + by (simp add: upt_conv_Cons')
1.240 + from Suc(2) this obtain r where
1.241 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
1.242 + by (auto simp add: elim!: crelE crel_map_entry crel_return)
1.243 + have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
1.244 + from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
1.245 + from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
1.246 + from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
1.247 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
1.248 + by simp
1.249 + from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
1.250 + crel_mapM_map_entry_remains[OF this, of "Heap.length a h - Suc n", symmetric] less less2
1.251 + show ?case
1.252 + by (auto simp add: nth_list_update_eq Heap.length_def)
1.253 +qed
1.254 +
1.255 +lemma crel_mapM_map_entry_length:
1.256 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
1.257 + assumes "n \<le> Heap.length a h"
1.258 + shows "Heap.length a h' = Heap.length a h"
1.259 +using assms
1.260 +proof (induct n arbitrary: h h' r)
1.261 + case 0
1.262 + thus ?case by (auto elim!: crel_return)
1.263 +next
1.264 + case (Suc n)
1.265 + let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
1.266 + from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
1.267 + by (simp add: upt_conv_Cons')
1.268 + from Suc(2) this obtain r where
1.269 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
1.270 + by (auto elim!: crelE crel_map_entry crel_return)
1.271 + have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
1.272 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
1.273 + by simp
1.274 + from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
1.275 +qed
1.276 +
1.277 +lemma crel_mapM_map_entry:
1.278 +assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Heap.length a h]) h h' r"
1.279 + shows "get_array a h' = List.map f (get_array a h)"
1.280 +proof -
1.281 + from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - Heap.length a h..<Heap.length a h]) h h' r" by simp
1.282 + from crel_mapM_map_entry_length[OF this]
1.283 + crel_mapM_map_entry_changes[OF this] show ?thesis
1.284 + unfolding Heap.length_def
1.285 + by (auto intro: nth_equalityI)
1.286 +qed
1.287 +
1.288 +lemma crel_map_weak:
1.289 + assumes crel_map: "crel (Array.map f a) h h' r"
1.290 + obtains "r = a" "get_array a h' = List.map f (get_array a h)"
1.291 +proof
1.292 + from assms crel_mapM_map_entry show "get_array a h' = List.map f (get_array a h)"
1.293 + unfolding Array.map_def
1.294 + by (fastsimp elim!: crelE crel_length crel_return)
1.295 + from assms show "r = a"
1.296 + unfolding Array.map_def
1.297 + by (elim crelE crel_return)
1.298 +qed
1.299 +
1.300 +subsection {* Elimination rules for reference commands *}
1.301 +
1.302 +(* TODO:
1.303 +maybe introduce a new predicate "extends h' h x"
1.304 +which means h' extends h with a new reference x.
1.305 +Then crel_new: would be
1.306 +assumes "crel (Ref.new v) h h' x"
1.307 +obtains "get_ref x h' = v"
1.308 +and "extends h' h x"
1.309 +
1.310 +and we would need further rules for extends:
1.311 +extends h' h x \<Longrightarrow> \<not> ref_present x h
1.312 +extends h' h x \<Longrightarrow> ref_present x h'
1.313 +extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> ref_present y h'
1.314 +extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> get_ref y h = get_ref y h'
1.315 +extends h' h x \<Longrightarrow> lim h' = Suc (lim h)
1.316 +*)
1.317 +
1.318 +lemma crel_Ref_new:
1.319 + assumes "crel (Ref.new v) h h' x"
1.320 + obtains "get_ref x h' = v"
1.321 + and "\<not> ref_present x h"
1.322 + and "ref_present x h'"
1.323 + and "\<forall>y. ref_present y h \<longrightarrow> get_ref y h = get_ref y h'"
1.324 + (* and "lim h' = Suc (lim h)" *)
1.325 + and "\<forall>y. ref_present y h \<longrightarrow> ref_present y h'"
1.326 + using assms
1.327 + unfolding Ref.new_def
1.328 + apply (elim crel_heap)
1.329 + unfolding Heap.ref_def
1.330 + apply (simp add: Let_def)
1.331 + unfolding Heap.new_ref_def
1.332 + apply (simp add: Let_def)
1.333 + unfolding ref_present_def
1.334 + apply auto
1.335 + unfolding get_ref_def set_ref_def
1.336 + apply auto
1.337 + done
1.338 +
1.339 +lemma crel_lookup:
1.340 + assumes "crel (!ref) h h' r"
1.341 + obtains "h = h'" "r = get_ref ref h"
1.342 +using assms
1.343 +unfolding Ref.lookup_def
1.344 +by (auto elim: crel_heap)
1.345 +
1.346 +lemma crel_update:
1.347 + assumes "crel (ref := v) h h' r"
1.348 + obtains "h' = set_ref ref v h" "r = ()"
1.349 +using assms
1.350 +unfolding Ref.update_def
1.351 +by (auto elim: crel_heap)
1.352 +
1.353 +lemma crel_change:
1.354 + assumes "crel (Ref.change f ref) h h' r"
1.355 + obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
1.356 +using assms
1.357 +unfolding Ref.change_def Let_def
1.358 +by (auto elim!: crelE crel_lookup crel_update crel_return)
1.359 +
1.360 +subsection {* Elimination rules for the assert command *}
1.361 +
1.362 +lemma crel_assert[consumes 1]:
1.363 + assumes "crel (assert P x) h h' r"
1.364 + obtains "P x" "r = x" "h = h'"
1.365 + using assms
1.366 + unfolding assert_def
1.367 + by (elim crel_if crel_return crel_raise) auto
1.368 +
1.369 +lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
1.370 +unfolding crel_def bindM_def Let_def assert_def
1.371 + raise_def return_def prod_case_beta
1.372 +apply (cases f)
1.373 +apply simp
1.374 +apply (simp add: expand_fun_eq split_def)
1.375 +apply auto
1.376 +apply (case_tac "fst (fun x)")
1.377 +apply (simp_all add: Pair_fst_snd_eq)
1.378 +apply (erule_tac x="x" in meta_allE)
1.379 +apply fastsimp
1.380 +done
1.381 +
1.382 +section {* Introduction rules *}
1.383 +
1.384 +subsection {* Introduction rules for basic monadic commands *}
1.385 +
1.386 +lemma crelI:
1.387 + assumes "crel f h h' r" "crel (g r) h' h'' r'"
1.388 + shows "crel (f >>= g) h h'' r'"
1.389 + using assms by (simp add: crel_def' bindM_def)
1.390 +
1.391 +lemma crelI':
1.392 + assumes "crel f h h' r" "crel g h' h'' r'"
1.393 + shows "crel (f >> g) h h'' r'"
1.394 + using assms by (intro crelI) auto
1.395 +
1.396 +lemma crel_returnI:
1.397 + shows "crel (return x) h h x"
1.398 + unfolding crel_def return_def by simp
1.399 +
1.400 +lemma crel_raiseI:
1.401 + shows "\<not> (crel (raise x) h h' r)"
1.402 + unfolding crel_def raise_def by simp
1.403 +
1.404 +lemma crel_ifI:
1.405 + assumes "c \<longrightarrow> crel t h h' r"
1.406 + "\<not>c \<longrightarrow> crel e h h' r"
1.407 + shows "crel (if c then t else e) h h' r"
1.408 + using assms
1.409 + unfolding crel_def by auto
1.410 +
1.411 +lemma crel_option_caseI:
1.412 + assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
1.413 + assumes "x = None \<Longrightarrow> crel n h h' r"
1.414 + shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
1.415 +using assms
1.416 +by (auto split: option.split)
1.417 +
1.418 +lemma crel_heapI:
1.419 + shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
1.420 + by (simp add: crel_def apfst_def split_def prod_fun_def)
1.421 +
1.422 +lemma crel_heapI':
1.423 + assumes "h' = snd (f h)" "r = fst (f h)"
1.424 + shows "crel (Heap_Monad.heap f) h h' r"
1.425 + using assms
1.426 + by (simp add: crel_def split_def apfst_def prod_fun_def)
1.427 +
1.428 +lemma crelI2:
1.429 + assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
1.430 + shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
1.431 + oops
1.432 +
1.433 +lemma crel_ifI2:
1.434 + assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
1.435 + "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
1.436 + shows "\<exists> h' r. crel (if c then t else e) h h' r"
1.437 + oops
1.438 +
1.439 +subsection {* Introduction rules for array commands *}
1.440 +
1.441 +lemma crel_lengthI:
1.442 + shows "crel (length a) h h (Heap.length a h)"
1.443 + unfolding length_def
1.444 + by (rule crel_heapI') auto
1.445 +
1.446 +(* thm crel_newI for Array.new is missing *)
1.447 +
1.448 +lemma crel_nthI:
1.449 + assumes "i < Heap.length a h"
1.450 + shows "crel (nth a i) h h ((get_array a h) ! i)"
1.451 + using assms
1.452 + unfolding nth_def
1.453 + by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
1.454 +
1.455 +lemma crel_updI:
1.456 + assumes "i < Heap.length a h"
1.457 + shows "crel (upd i v a) h (Heap.upd a i v h) a"
1.458 + using assms
1.459 + unfolding upd_def
1.460 + by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
1.461 + crel_lengthI crel_heapI')
1.462 +
1.463 +(* thm crel_of_listI is missing *)
1.464 +
1.465 +(* thm crel_map_entryI is missing *)
1.466 +
1.467 +(* thm crel_swapI is missing *)
1.468 +
1.469 +(* thm crel_makeI is missing *)
1.470 +
1.471 +(* thm crel_freezeI is missing *)
1.472 +
1.473 +(* thm crel_mapI is missing *)
1.474 +
1.475 +subsection {* Introduction rules for reference commands *}
1.476 +
1.477 +lemma crel_lookupI:
1.478 + shows "crel (!ref) h h (get_ref ref h)"
1.479 + unfolding lookup_def by (auto intro!: crel_heapI')
1.480 +
1.481 +lemma crel_updateI:
1.482 + shows "crel (ref := v) h (set_ref ref v h) ()"
1.483 + unfolding update_def by (auto intro!: crel_heapI')
1.484 +
1.485 +lemma crel_changeI:
1.486 + shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
1.487 +unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
1.488 +
1.489 +subsection {* Introduction rules for the assert command *}
1.490 +
1.491 +lemma crel_assertI:
1.492 + assumes "P x"
1.493 + shows "crel (assert P x) h h x"
1.494 + using assms
1.495 + unfolding assert_def
1.496 + by (auto intro!: crel_ifI crel_returnI crel_raiseI)
1.497 +
1.498 +section {* Defintion of the noError predicate *}
1.499 +
1.500 +text {* We add a simple definitional setting for crel intro rules
1.501 + where we only would like to show that the computation does not result in a exception for heap h,
1.502 + but we do not care about statements about the resulting heap and return value.*}
1.503 +
1.504 +definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
1.505 +where
1.506 + "noError c h \<longleftrightarrow> (\<exists>r h'. (Inl r, h') = Heap_Monad.execute c h)"
1.507 +
1.508 +lemma noError_def': -- FIXME
1.509 + "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = (Inl r, h'))"
1.510 + unfolding noError_def apply auto proof -
1.511 + fix r h'
1.512 + assume "(Inl r, h') = Heap_Monad.execute c h"
1.513 + then have "Heap_Monad.execute c h = (Inl r, h')" ..
1.514 + then show "\<exists>r h'. Heap_Monad.execute c h = (Inl r, h')" by blast
1.515 +qed
1.516 +
1.517 +subsection {* Introduction rules for basic monadic commands *}
1.518 +
1.519 +lemma noErrorI:
1.520 + assumes "noError f h"
1.521 + assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
1.522 + shows "noError (f \<guillemotright>= g) h"
1.523 + using assms
1.524 + by (auto simp add: noError_def' crel_def' bindM_def)
1.525 +
1.526 +lemma noErrorI':
1.527 + assumes "noError f h"
1.528 + assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
1.529 + shows "noError (f \<guillemotright> g) h"
1.530 + using assms
1.531 + by (auto simp add: noError_def' crel_def' bindM_def)
1.532 +
1.533 +lemma noErrorI2:
1.534 +"\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
1.535 +\<Longrightarrow> noError (f \<guillemotright>= g) h"
1.536 +by (auto simp add: noError_def' crel_def' bindM_def)
1.537 +
1.538 +lemma noError_return:
1.539 + shows "noError (return x) h"
1.540 + unfolding noError_def return_def
1.541 + by auto
1.542 +
1.543 +lemma noError_if:
1.544 + assumes "c \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
1.545 + shows "noError (if c then t else e) h"
1.546 + using assms
1.547 + unfolding noError_def
1.548 + by auto
1.549 +
1.550 +lemma noError_option_case:
1.551 + assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
1.552 + assumes "noError n h"
1.553 + shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
1.554 +using assms
1.555 +by (auto split: option.split)
1.556 +
1.557 +lemma noError_mapM:
1.558 +assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)"
1.559 +shows "noError (mapM f xs) h"
1.560 +using assms
1.561 +proof (induct xs)
1.562 + case Nil
1.563 + thus ?case
1.564 + unfolding mapM.simps by (intro noError_return)
1.565 +next
1.566 + case (Cons x xs)
1.567 + thus ?case
1.568 + unfolding mapM.simps
1.569 + by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
1.570 +qed
1.571 +
1.572 +lemma noError_heap:
1.573 + shows "noError (Heap_Monad.heap f) h"
1.574 + by (simp add: noError_def' apfst_def prod_fun_def split_def)
1.575 +
1.576 +subsection {* Introduction rules for array commands *}
1.577 +
1.578 +lemma noError_length:
1.579 + shows "noError (Array.length a) h"
1.580 + unfolding length_def
1.581 + by (intro noError_heap)
1.582 +
1.583 +lemma noError_new:
1.584 + shows "noError (Array.new n v) h"
1.585 +unfolding Array.new_def by (intro noError_heap)
1.586 +
1.587 +lemma noError_upd:
1.588 + assumes "i < Heap.length a h"
1.589 + shows "noError (Array.upd i v a) h"
1.590 + using assms
1.591 + unfolding upd_def
1.592 + by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
1.593 +
1.594 +lemma noError_nth:
1.595 +assumes "i < Heap.length a h"
1.596 + shows "noError (Array.nth a i) h"
1.597 + using assms
1.598 + unfolding nth_def
1.599 + by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
1.600 +
1.601 +lemma noError_of_list:
1.602 + shows "noError (of_list ls) h"
1.603 + unfolding of_list_def by (rule noError_heap)
1.604 +
1.605 +lemma noError_map_entry:
1.606 + assumes "i < Heap.length a h"
1.607 + shows "noError (map_entry i f a) h"
1.608 + using assms
1.609 + unfolding map_entry_def
1.610 + by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
1.611 +
1.612 +lemma noError_swap:
1.613 + assumes "i < Heap.length a h"
1.614 + shows "noError (swap i x a) h"
1.615 + using assms
1.616 + unfolding swap_def
1.617 + by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
1.618 +
1.619 +lemma noError_make:
1.620 + shows "noError (make n f) h"
1.621 + unfolding make_def
1.622 + by (auto intro: noError_of_list)
1.623 +
1.624 +(*TODO: move to HeapMonad *)
1.625 +lemma mapM_append:
1.626 + "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
1.627 + by (induct xs) (simp_all add: monad_simp)
1.628 +
1.629 +lemma noError_freeze:
1.630 + shows "noError (freeze a) h"
1.631 +unfolding freeze_def
1.632 +by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
1.633 + noError_nth crel_nthI elim: crel_length)
1.634 +
1.635 +lemma noError_mapM_map_entry:
1.636 + assumes "n \<le> Heap.length a h"
1.637 + shows "noError (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h"
1.638 +using assms
1.639 +proof (induct n arbitrary: h)
1.640 + case 0
1.641 + thus ?case by (auto intro: noError_return)
1.642 +next
1.643 + case (Suc n)
1.644 + from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
1.645 + by (simp add: upt_conv_Cons')
1.646 + with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
1.647 + by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
1.648 +qed
1.649 +
1.650 +lemma noError_map:
1.651 + shows "noError (Array.map f a) h"
1.652 +using noError_mapM_map_entry[of "Heap.length a h" a h]
1.653 +unfolding Array.map_def
1.654 +by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
1.655 +
1.656 +subsection {* Introduction rules for the reference commands *}
1.657 +
1.658 +lemma noError_Ref_new:
1.659 + shows "noError (Ref.new v) h"
1.660 +unfolding Ref.new_def by (intro noError_heap)
1.661 +
1.662 +lemma noError_lookup:
1.663 + shows "noError (!ref) h"
1.664 + unfolding lookup_def by (intro noError_heap)
1.665 +
1.666 +lemma noError_update:
1.667 + shows "noError (ref := v) h"
1.668 + unfolding update_def by (intro noError_heap)
1.669 +
1.670 +lemma noError_change:
1.671 + shows "noError (Ref.change f ref) h"
1.672 + unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
1.673 +
1.674 +subsection {* Introduction rules for the assert command *}
1.675 +
1.676 +lemma noError_assert:
1.677 + assumes "P x"
1.678 + shows "noError (assert P x) h"
1.679 + using assms
1.680 + unfolding assert_def
1.681 + by (auto intro: noError_if noError_return)
1.682 +
1.683 +section {* Cumulative lemmas *}
1.684 +
1.685 +lemmas crel_elim_all =
1.686 + crelE crelE' crel_return crel_raise crel_if crel_option_case
1.687 + crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze crel_map_weak
1.688 + crel_Ref_new crel_lookup crel_update crel_change
1.689 + crel_assert
1.690 +
1.691 +lemmas crel_intro_all =
1.692 + crelI crelI' crel_returnI crel_raiseI crel_ifI crel_option_caseI
1.693 + crel_lengthI (* crel_newI *) crel_nthI crel_updI (* crel_of_listI crel_map_entryI crel_swapI crel_makeI crel_freezeI crel_mapI *)
1.694 + (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
1.695 + crel_assert
1.696 +
1.697 +lemmas noError_intro_all =
1.698 + noErrorI noErrorI' noError_return noError_if noError_option_case
1.699 + noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze noError_map
1.700 + noError_Ref_new noError_lookup noError_update noError_change
1.701 + noError_assert
1.702 +
1.703 +end
1.704 \ No newline at end of file