1.1 --- a/src/HOL/Imperative_HOL/Array.thy Mon Jul 05 15:36:37 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Array.thy Mon Jul 05 16:46:23 2010 +0200
1.3 @@ -8,24 +8,132 @@
1.4 imports Heap_Monad
1.5 begin
1.6
1.7 +subsection {* Primitive layer *}
1.8 +
1.9 +definition
1.10 + array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
1.11 + "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
1.12 +
1.13 +definition
1.14 + get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
1.15 + "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
1.16 +
1.17 +definition
1.18 + set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
1.19 + "set_array a x =
1.20 + arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
1.21 +
1.22 +definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
1.23 + "array xs h = (let
1.24 + l = lim h;
1.25 + r = Array l;
1.26 + h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
1.27 + in (r, h''))"
1.28 +
1.29 +definition length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
1.30 + "length a h = List.length (get_array a h)"
1.31 +
1.32 +definition change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
1.33 + "change a i x h = set_array a ((get_array a h)[i:=x]) h"
1.34 +
1.35 +text {* Properties of imperative arrays *}
1.36 +
1.37 +text {* FIXME: Does there exist a "canonical" array axiomatisation in
1.38 +the literature? *}
1.39 +
1.40 +definition noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) where
1.41 + "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
1.42 +
1.43 +lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
1.44 + and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
1.45 + unfolding noteq_arrs_def by auto
1.46 +
1.47 +lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
1.48 + unfolding noteq_arrs_def by auto
1.49 +
1.50 +lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
1.51 + by (simp add: array_present_def noteq_arrs_def array_def Let_def)
1.52 +
1.53 +lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
1.54 + by (simp add: get_array_def set_array_def o_def)
1.55 +
1.56 +lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
1.57 + by (simp add: noteq_arrs_def get_array_def set_array_def)
1.58 +
1.59 +lemma set_array_same [simp]:
1.60 + "set_array r x (set_array r y h) = set_array r x h"
1.61 + by (simp add: set_array_def)
1.62 +
1.63 +lemma array_set_set_swap:
1.64 + "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
1.65 + by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
1.66 +
1.67 +lemma get_array_change_eq [simp]:
1.68 + "get_array a (change a i v h) = (get_array a h) [i := v]"
1.69 + by (simp add: change_def)
1.70 +
1.71 +lemma nth_change_array_neq_array [simp]:
1.72 + "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
1.73 + by (simp add: change_def noteq_arrs_def)
1.74 +
1.75 +lemma get_arry_array_change_elem_neqIndex [simp]:
1.76 + "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
1.77 + by simp
1.78 +
1.79 +lemma length_change [simp]:
1.80 + "length a (change b i v h) = length a h"
1.81 + by (simp add: change_def length_def set_array_def get_array_def)
1.82 +
1.83 +lemma change_swap_neqArray:
1.84 + "a =!!= a' \<Longrightarrow>
1.85 + change a i v (change a' i' v' h)
1.86 + = change a' i' v' (change a i v h)"
1.87 +apply (unfold change_def)
1.88 +apply simp
1.89 +apply (subst array_set_set_swap, assumption)
1.90 +apply (subst array_get_set_neq)
1.91 +apply (erule noteq_arrs_sym)
1.92 +apply (simp)
1.93 +done
1.94 +
1.95 +lemma change_swap_neqIndex:
1.96 + "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)"
1.97 + by (auto simp add: change_def array_set_set_swap list_update_swap)
1.98 +
1.99 +lemma get_array_init_array_list:
1.100 + "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
1.101 + by (simp add: Let_def split_def array_def)
1.102 +
1.103 +lemma set_array:
1.104 + "set_array (fst (array ls h))
1.105 + new_ls (snd (array ls h))
1.106 + = snd (array new_ls h)"
1.107 + by (simp add: Let_def split_def array_def)
1.108 +
1.109 +lemma array_present_change [simp]:
1.110 + "array_present a (change b i v h) = array_present a h"
1.111 + by (simp add: change_def array_present_def set_array_def get_array_def)
1.112 +
1.113 +
1.114 +
1.115 subsection {* Primitives *}
1.116
1.117 definition
1.118 new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
1.119 - [code del]: "new n x = Heap_Monad.heap (Heap.array (replicate n x))"
1.120 + [code del]: "new n x = Heap_Monad.heap (Array.array (replicate n x))"
1.121
1.122 definition
1.123 of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
1.124 - [code del]: "of_list xs = Heap_Monad.heap (Heap.array xs)"
1.125 + [code del]: "of_list xs = Heap_Monad.heap (Array.array xs)"
1.126
1.127 definition
1.128 - length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
1.129 - [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
1.130 + len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
1.131 + [code del]: "len arr = Heap_Monad.heap (\<lambda>h. (Array.length arr h, h))"
1.132
1.133 definition
1.134 nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
1.135 where
1.136 - [code del]: "nth a i = (do len \<leftarrow> length a;
1.137 + [code del]: "nth a i = (do len \<leftarrow> len a;
1.138 (if i < len
1.139 then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
1.140 else raise ''array lookup: index out of range'')
1.141 @@ -34,9 +142,9 @@
1.142 definition
1.143 upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
1.144 where
1.145 - [code del]: "upd i x a = (do len \<leftarrow> length a;
1.146 + [code del]: "upd i x a = (do len \<leftarrow> len a;
1.147 (if i < len
1.148 - then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
1.149 + then Heap_Monad.heap (\<lambda>h. (a, change a i x h))
1.150 else raise ''array update: index out of range'')
1.151 done)"
1.152
1.153 @@ -73,7 +181,7 @@
1.154 freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
1.155 where
1.156 "freeze a = (do
1.157 - n \<leftarrow> length a;
1.158 + n \<leftarrow> len a;
1.159 mapM (nth a) [0..<n]
1.160 done)"
1.161
1.162 @@ -81,12 +189,11 @@
1.163 map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
1.164 where
1.165 "map f a = (do
1.166 - n \<leftarrow> length a;
1.167 + n \<leftarrow> len a;
1.168 mapM (\<lambda>n. map_entry n f a) [0..<n];
1.169 return a
1.170 done)"
1.171
1.172 -hide_const (open) new map -- {* avoid clashed with some popular names *}
1.173
1.174
1.175 subsection {* Properties *}
1.176 @@ -125,12 +232,12 @@
1.177 "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
1.178 by (simp add: make'_def o_def)
1.179
1.180 -definition length' where
1.181 - [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
1.182 -hide_const (open) length'
1.183 +definition len' where
1.184 + [code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
1.185 +hide_const (open) len'
1.186 lemma [code]:
1.187 - "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
1.188 - by (simp add: length'_def)
1.189 + "Array.len a = Array.len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
1.190 + by (simp add: len'_def)
1.191
1.192 definition nth' where
1.193 [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
1.194 @@ -154,7 +261,7 @@
1.195 code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
1.196 code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
1.197 code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
1.198 -code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
1.199 +code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
1.200 code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
1.201 code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
1.202
1.203 @@ -167,7 +274,7 @@
1.204 code_const Array (OCaml "failwith/ \"bare Array\"")
1.205 code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
1.206 code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
1.207 -code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
1.208 +code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
1.209 code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
1.210 code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
1.211
1.212 @@ -180,8 +287,10 @@
1.213 code_const Array (Haskell "error/ \"bare Array\"")
1.214 code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
1.215 code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
1.216 -code_const Array.length' (Haskell "Heap.lengthArray")
1.217 +code_const Array.len' (Haskell "Heap.lengthArray")
1.218 code_const Array.nth' (Haskell "Heap.readArray")
1.219 code_const Array.upd' (Haskell "Heap.writeArray")
1.220
1.221 +hide_const (open) new map -- {* avoid clashed with some popular names *}
1.222 +
1.223 end
2.1 --- a/src/HOL/Imperative_HOL/Heap.thy Mon Jul 05 15:36:37 2010 +0200
2.2 +++ b/src/HOL/Imperative_HOL/Heap.thy Mon Jul 05 16:46:23 2010 +0200
2.3 @@ -37,7 +37,10 @@
2.4
2.5 subsection {* A polymorphic heap with dynamic arrays and references *}
2.6
2.7 -subsubsection {* Type definitions *}
2.8 +text {*
2.9 + References and arrays are developed in parallel,
2.10 + but keeping them separate makes some later proofs simpler.
2.11 +*}
2.12
2.13 types addr = nat -- "untyped heap references"
2.14 types heap_rep = nat -- "representable values"
2.15 @@ -82,283 +85,4 @@
2.16 #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
2.17 *}
2.18
2.19 -
2.20 -subsection {* Imperative references and arrays *}
2.21 -
2.22 -text {*
2.23 - References and arrays are developed in parallel,
2.24 - but keeping them separate makes some later proofs simpler.
2.25 -*}
2.26 -
2.27 -subsubsection {* Primitive operations *}
2.28 -
2.29 -definition
2.30 - ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
2.31 - "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
2.32 -
2.33 -definition
2.34 - array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
2.35 - "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
2.36 -
2.37 -definition
2.38 - get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where
2.39 - "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))"
2.40 -
2.41 -definition
2.42 - get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
2.43 - "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
2.44 -
2.45 -definition
2.46 - set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
2.47 - "set_ref r x =
2.48 - refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
2.49 -
2.50 -definition
2.51 - set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
2.52 - "set_array a x =
2.53 - arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
2.54 -
2.55 -definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
2.56 - "ref x h = (let
2.57 - l = lim h;
2.58 - r = Ref l;
2.59 - h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>)
2.60 - in (r, h''))"
2.61 -
2.62 -definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
2.63 - "array xs h = (let
2.64 - l = lim h;
2.65 - r = Array l;
2.66 - h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
2.67 - in (r, h''))"
2.68 -
2.69 -definition
2.70 - upd :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
2.71 - "upd a i x h = set_array a ((get_array a h)[i:=x]) h"
2.72 -
2.73 -definition
2.74 - length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
2.75 - "length a h = size (get_array a h)"
2.76 -
2.77 -
2.78 -subsubsection {* Reference equality *}
2.79 -
2.80 -text {*
2.81 - The following relations are useful for comparing arrays and references.
2.82 -*}
2.83 -
2.84 -definition
2.85 - noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70)
2.86 -where
2.87 - "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
2.88 -
2.89 -definition
2.90 - noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70)
2.91 -where
2.92 - "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
2.93 -
2.94 -lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
2.95 - and noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
2.96 - and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
2.97 - and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
2.98 -unfolding noteq_refs_def noteq_arrs_def by auto
2.99 -
2.100 -lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
2.101 - unfolding noteq_refs_def by auto
2.102 -
2.103 -lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
2.104 - by (simp add: ref_present_def ref_def Let_def noteq_refs_def)
2.105 -
2.106 -lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
2.107 - by (simp add: array_present_def noteq_arrs_def array_def Let_def)
2.108 -
2.109 -
2.110 -subsubsection {* Properties of heap containers *}
2.111 -
2.112 -text {* Properties of imperative arrays *}
2.113 -
2.114 -text {* FIXME: Does there exist a "canonical" array axiomatisation in
2.115 -the literature? *}
2.116 -
2.117 -lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
2.118 - by (simp add: get_array_def set_array_def o_def)
2.119 -
2.120 -lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
2.121 - by (simp add: noteq_arrs_def get_array_def set_array_def)
2.122 -
2.123 -lemma set_array_same [simp]:
2.124 - "set_array r x (set_array r y h) = set_array r x h"
2.125 - by (simp add: set_array_def)
2.126 -
2.127 -lemma array_set_set_swap:
2.128 - "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
2.129 - by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
2.130 -
2.131 -lemma array_ref_set_set_swap:
2.132 - "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)"
2.133 - by (simp add: Let_def expand_fun_eq set_array_def set_ref_def)
2.134 -
2.135 -lemma get_array_upd_eq [simp]:
2.136 - "get_array a (upd a i v h) = (get_array a h) [i := v]"
2.137 - by (simp add: upd_def)
2.138 -
2.139 -lemma nth_upd_array_neq_array [simp]:
2.140 - "a =!!= b \<Longrightarrow> get_array a (upd b j v h) ! i = get_array a h ! i"
2.141 - by (simp add: upd_def noteq_arrs_def)
2.142 -
2.143 -lemma get_arry_array_upd_elem_neqIndex [simp]:
2.144 - "i \<noteq> j \<Longrightarrow> get_array a (upd a j v h) ! i = get_array a h ! i"
2.145 - by simp
2.146 -
2.147 -lemma length_upd_eq [simp]:
2.148 - "length a (upd a i v h) = length a h"
2.149 - by (simp add: length_def upd_def)
2.150 -
2.151 -lemma length_upd_neq [simp]:
2.152 - "length a (upd b i v h) = length a h"
2.153 - by (simp add: upd_def length_def set_array_def get_array_def)
2.154 -
2.155 -lemma upd_swap_neqArray:
2.156 - "a =!!= a' \<Longrightarrow>
2.157 - upd a i v (upd a' i' v' h)
2.158 - = upd a' i' v' (upd a i v h)"
2.159 -apply (unfold upd_def)
2.160 -apply simp
2.161 -apply (subst array_set_set_swap, assumption)
2.162 -apply (subst array_get_set_neq)
2.163 -apply (erule noteq_arrs_sym)
2.164 -apply (simp)
2.165 -done
2.166 -
2.167 -lemma upd_swap_neqIndex:
2.168 - "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> upd a i v (upd a i' v' h) = upd a i' v' (upd a i v h)"
2.169 -by (auto simp add: upd_def array_set_set_swap list_update_swap)
2.170 -
2.171 -lemma get_array_init_array_list:
2.172 - "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
2.173 - by (simp add: Let_def split_def array_def)
2.174 -
2.175 -lemma set_array:
2.176 - "set_array (fst (array ls h))
2.177 - new_ls (snd (array ls h))
2.178 - = snd (array new_ls h)"
2.179 - by (simp add: Let_def split_def array_def)
2.180 -
2.181 -lemma array_present_upd [simp]:
2.182 - "array_present a (upd b i v h) = array_present a h"
2.183 - by (simp add: upd_def array_present_def set_array_def get_array_def)
2.184 -
2.185 -(*lemma array_of_list_replicate:
2.186 - "array_of_list (replicate n x) = array n x"
2.187 - by (simp add: expand_fun_eq array_of_list_def array_def)*)
2.188 -
2.189 -text {* Properties of imperative references *}
2.190 -
2.191 -lemma next_ref_fresh [simp]:
2.192 - assumes "(r, h') = ref x h"
2.193 - shows "\<not> ref_present r h"
2.194 - using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def)
2.195 -
2.196 -lemma next_ref_present [simp]:
2.197 - assumes "(r, h') = ref x h"
2.198 - shows "ref_present r h'"
2.199 - using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def)
2.200 -
2.201 -lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
2.202 - by (simp add: get_ref_def set_ref_def)
2.203 -
2.204 -lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h"
2.205 - by (simp add: noteq_refs_def get_ref_def set_ref_def)
2.206 -
2.207 -(* FIXME: We need some infrastructure to infer that locally generated
2.208 - new refs (by new_ref(_no_init), new_array(')) are distinct
2.209 - from all existing refs.
2.210 -*)
2.211 -
2.212 -lemma ref_set_get: "set_ref r (get_ref r h) h = h"
2.213 -apply (simp add: set_ref_def get_ref_def)
2.214 -oops
2.215 -
2.216 -lemma set_ref_same[simp]:
2.217 - "set_ref r x (set_ref r y h) = set_ref r x h"
2.218 - by (simp add: set_ref_def)
2.219 -
2.220 -lemma ref_set_set_swap:
2.221 - "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)"
2.222 - by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
2.223 -
2.224 -lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
2.225 - by (simp add: ref_def set_ref_def Let_def)
2.226 -
2.227 -lemma ref_get_new [simp]:
2.228 - "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
2.229 - by (simp add: ref_def Let_def split_def)
2.230 -
2.231 -lemma ref_set_new [simp]:
2.232 - "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)"
2.233 - by (simp add: ref_def Let_def split_def)
2.234 -
2.235 -lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow>
2.236 - get_ref r (snd (ref v h)) = get_ref r h"
2.237 - by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def)
2.238 -
2.239 -lemma lim_set_ref [simp]:
2.240 - "lim (set_ref r v h) = lim h"
2.241 - by (simp add: set_ref_def)
2.242 -
2.243 -lemma ref_present_new_ref [simp]:
2.244 - "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
2.245 - by (simp add: ref_present_def ref_def Let_def)
2.246 -
2.247 -lemma ref_present_set_ref [simp]:
2.248 - "ref_present r (set_ref r' v h) = ref_present r h"
2.249 - by (simp add: set_ref_def ref_present_def)
2.250 -
2.251 -lemma noteq_refsI: "\<lbrakk> ref_present r h; \<not>ref_present r' h \<rbrakk> \<Longrightarrow> r =!= r'"
2.252 - unfolding noteq_refs_def ref_present_def
2.253 - by auto
2.254 -
2.255 -text {* Non-interaction between imperative array and imperative references *}
2.256 -
2.257 -lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
2.258 - by (simp add: get_array_def set_ref_def)
2.259 -
2.260 -lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i"
2.261 - by simp
2.262 -
2.263 -lemma get_ref_upd [simp]: "get_ref r (upd a i v h) = get_ref r h"
2.264 - by (simp add: get_ref_def set_array_def upd_def)
2.265 -
2.266 -lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
2.267 - by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def)
2.268 -
2.269 -text {*not actually true ???*}
2.270 -lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
2.271 -apply (case_tac a)
2.272 -apply (simp add: Let_def upd_def)
2.273 -apply auto
2.274 -oops
2.275 -
2.276 -lemma length_new_ref[simp]:
2.277 - "length a (snd (ref v h)) = length a h"
2.278 - by (simp add: get_array_def set_ref_def length_def ref_def Let_def)
2.279 -
2.280 -lemma get_array_new_ref [simp]:
2.281 - "get_array a (snd (ref v h)) = get_array a h"
2.282 - by (simp add: ref_def set_ref_def get_array_def Let_def)
2.283 -
2.284 -lemma ref_present_upd [simp]:
2.285 - "ref_present r (upd a i v h) = ref_present r h"
2.286 - by (simp add: upd_def ref_present_def set_array_def get_array_def)
2.287 -
2.288 -lemma array_present_set_ref [simp]:
2.289 - "array_present a (set_ref r v h) = array_present a h"
2.290 - by (simp add: array_present_def set_ref_def)
2.291 -
2.292 -lemma array_present_new_ref [simp]:
2.293 - "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
2.294 - by (simp add: array_present_def ref_def Let_def)
2.295 -
2.296 -hide_const (open) empty upd length array ref
2.297 -
2.298 end
3.1 --- a/src/HOL/Imperative_HOL/Ref.thy Mon Jul 05 15:36:37 2010 +0200
3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy Mon Jul 05 16:46:23 2010 +0200
3.3 @@ -5,7 +5,7 @@
3.4 header {* Monadic references *}
3.5
3.6 theory Ref
3.7 -imports Heap_Monad
3.8 +imports Array
3.9 begin
3.10
3.11 text {*
3.12 @@ -14,11 +14,111 @@
3.13 and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
3.14 *}
3.15
3.16 +subsection {* Primitive layer *}
3.17 +
3.18 +definition
3.19 + ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
3.20 + "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
3.21 +
3.22 +definition
3.23 + get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where
3.24 + "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))"
3.25 +
3.26 +definition
3.27 + set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
3.28 + "set_ref r x =
3.29 + refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
3.30 +
3.31 +definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
3.32 + "ref x h = (let
3.33 + l = lim h;
3.34 + r = Ref l;
3.35 + h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>)
3.36 + in (r, h''))"
3.37 +
3.38 +definition noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70) where
3.39 + "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
3.40 +
3.41 +lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
3.42 + and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
3.43 + unfolding noteq_refs_def by auto
3.44 +
3.45 +lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
3.46 + unfolding noteq_refs_def by auto
3.47 +
3.48 +lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
3.49 + by (simp add: ref_present_def ref_def Let_def noteq_refs_def)
3.50 +
3.51 +lemma next_ref_fresh [simp]:
3.52 + assumes "(r, h') = ref x h"
3.53 + shows "\<not> ref_present r h"
3.54 + using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def)
3.55 +
3.56 +lemma next_ref_present [simp]:
3.57 + assumes "(r, h') = ref x h"
3.58 + shows "ref_present r h'"
3.59 + using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def)
3.60 +
3.61 +lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
3.62 + by (simp add: get_ref_def set_ref_def)
3.63 +
3.64 +lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h"
3.65 + by (simp add: noteq_refs_def get_ref_def set_ref_def)
3.66 +
3.67 +(* FIXME: We need some infrastructure to infer that locally generated
3.68 + new refs (by new_ref(_no_init), new_array(')) are distinct
3.69 + from all existing refs.
3.70 +*)
3.71 +
3.72 +lemma ref_set_get: "set_ref r (get_ref r h) h = h"
3.73 +apply (simp add: set_ref_def get_ref_def)
3.74 +oops
3.75 +
3.76 +lemma set_ref_same[simp]:
3.77 + "set_ref r x (set_ref r y h) = set_ref r x h"
3.78 + by (simp add: set_ref_def)
3.79 +
3.80 +lemma ref_set_set_swap:
3.81 + "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)"
3.82 + by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
3.83 +
3.84 +lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
3.85 + by (simp add: ref_def set_ref_def Let_def)
3.86 +
3.87 +lemma ref_get_new [simp]:
3.88 + "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
3.89 + by (simp add: ref_def Let_def split_def)
3.90 +
3.91 +lemma ref_set_new [simp]:
3.92 + "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)"
3.93 + by (simp add: ref_def Let_def split_def)
3.94 +
3.95 +lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow>
3.96 + get_ref r (snd (ref v h)) = get_ref r h"
3.97 + by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def)
3.98 +
3.99 +lemma lim_set_ref [simp]:
3.100 + "lim (set_ref r v h) = lim h"
3.101 + by (simp add: set_ref_def)
3.102 +
3.103 +lemma ref_present_new_ref [simp]:
3.104 + "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
3.105 + by (simp add: ref_present_def ref_def Let_def)
3.106 +
3.107 +lemma ref_present_set_ref [simp]:
3.108 + "ref_present r (set_ref r' v h) = ref_present r h"
3.109 + by (simp add: set_ref_def ref_present_def)
3.110 +
3.111 +lemma noteq_refsI: "\<lbrakk> ref_present r h; \<not>ref_present r' h \<rbrakk> \<Longrightarrow> r =!= r'"
3.112 + unfolding noteq_refs_def ref_present_def
3.113 + by auto
3.114 +
3.115 +
3.116 subsection {* Primitives *}
3.117
3.118 definition
3.119 new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
3.120 - [code del]: "new v = Heap_Monad.heap (Heap.ref v)"
3.121 + [code del]: "new v = Heap_Monad.heap (Ref.ref v)"
3.122
3.123 definition
3.124 lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
3.125 @@ -55,6 +155,48 @@
3.126 by (auto simp add: change_def lookup_chain)
3.127
3.128
3.129 +text {* Non-interaction between imperative array and imperative references *}
3.130 +
3.131 +lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
3.132 + by (simp add: get_array_def set_ref_def)
3.133 +
3.134 +lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i"
3.135 + by simp
3.136 +
3.137 +lemma get_ref_upd [simp]: "get_ref r (Array.change a i v h) = get_ref r h"
3.138 + by (simp add: get_ref_def set_array_def Array.change_def)
3.139 +
3.140 +lemma new_ref_upd: "fst (ref v (Array.change a i v' h)) = fst (ref v h)"
3.141 + by (simp add: set_array_def get_array_def Let_def ref_new_set Array.change_def ref_def)
3.142 +
3.143 +lemma upd_set_ref_swap: "Array.change a i v (set_ref r v' h) = set_ref r v' (Array.change a i v h)"
3.144 + by (simp add: set_ref_def Array.change_def get_array_def set_array_def)
3.145 +
3.146 +lemma length_new_ref[simp]:
3.147 + "length a (snd (ref v h)) = length a h"
3.148 + by (simp add: get_array_def set_ref_def length_def ref_def Let_def)
3.149 +
3.150 +lemma get_array_new_ref [simp]:
3.151 + "get_array a (snd (ref v h)) = get_array a h"
3.152 + by (simp add: ref_def set_ref_def get_array_def Let_def)
3.153 +
3.154 +lemma ref_present_upd [simp]:
3.155 + "ref_present r (Array.change a i v h) = ref_present r h"
3.156 + by (simp add: Array.change_def ref_present_def set_array_def get_array_def)
3.157 +
3.158 +lemma array_present_set_ref [simp]:
3.159 + "array_present a (set_ref r v h) = array_present a h"
3.160 + by (simp add: array_present_def set_ref_def)
3.161 +
3.162 +lemma array_present_new_ref [simp]:
3.163 + "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
3.164 + by (simp add: array_present_def ref_def Let_def)
3.165 +
3.166 +lemma array_ref_set_set_swap:
3.167 + "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)"
3.168 + by (simp add: Let_def expand_fun_eq set_array_def set_ref_def)
3.169 +
3.170 +
3.171 subsection {* Code generator setup *}
3.172
3.173 subsubsection {* SML *}
4.1 --- a/src/HOL/Imperative_HOL/Relational.thy Mon Jul 05 15:36:37 2010 +0200
4.2 +++ b/src/HOL/Imperative_HOL/Relational.thy Mon Jul 05 16:46:23 2010 +0200
4.3 @@ -91,10 +91,10 @@
4.4 subsection {* Elimination rules for array commands *}
4.5
4.6 lemma crel_length:
4.7 - assumes "crel (length a) h h' r"
4.8 - obtains "h = h'" "r = Heap.length a h'"
4.9 + assumes "crel (len a) h h' r"
4.10 + obtains "h = h'" "r = Array.length a h'"
4.11 using assms
4.12 - unfolding length_def
4.13 + unfolding Array.len_def
4.14 by (elim crel_heap) simp
4.15
4.16 (* Strong version of the lemma for this operation is missing *)
4.17 @@ -106,14 +106,14 @@
4.18
4.19 lemma crel_nth[consumes 1]:
4.20 assumes "crel (nth a i) h h' r"
4.21 - obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
4.22 + obtains "r = (get_array a h) ! i" "h = h'" "i < Array.length a h"
4.23 using assms
4.24 unfolding nth_def
4.25 by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
4.26
4.27 lemma crel_upd[consumes 1]:
4.28 assumes "crel (upd i v a) h h' r"
4.29 - obtains "r = a" "h' = Heap.upd a i v h"
4.30 + obtains "r = a" "h' = Array.change a i v h"
4.31 using assms
4.32 unfolding upd_def
4.33 by (elim crelE crel_if crel_return crel_raise
4.34 @@ -129,14 +129,14 @@
4.35
4.36 lemma crel_map_entry:
4.37 assumes "crel (Array.map_entry i f a) h h' r"
4.38 - obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
4.39 + obtains "r = a" "h' = Array.change a i (f (get_array a h ! i)) h"
4.40 using assms
4.41 unfolding Array.map_entry_def
4.42 by (elim crelE crel_upd crel_nth) auto
4.43
4.44 lemma crel_swap:
4.45 assumes "crel (Array.swap i x a) h h' r"
4.46 - obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
4.47 + obtains "r = get_array a h ! i" "h' = Array.change a i x h"
4.48 using assms
4.49 unfolding Array.swap_def
4.50 by (elim crelE crel_upd crel_nth crel_return) auto
4.51 @@ -160,25 +160,25 @@
4.52
4.53 lemma crel_mapM_nth:
4.54 assumes
4.55 - "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' xs"
4.56 - assumes "n \<le> Heap.length a h"
4.57 - shows "h = h' \<and> xs = drop (Heap.length a h - n) (get_array a h)"
4.58 + "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
4.59 + assumes "n \<le> Array.length a h"
4.60 + shows "h = h' \<and> xs = drop (Array.length a h - n) (get_array a h)"
4.61 using assms
4.62 proof (induct n arbitrary: xs h h')
4.63 case 0 thus ?case
4.64 - by (auto elim!: crel_return simp add: Heap.length_def)
4.65 + by (auto elim!: crel_return simp add: Array.length_def)
4.66 next
4.67 case (Suc n)
4.68 - 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]"
4.69 + 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]"
4.70 by (simp add: upt_conv_Cons')
4.71 with Suc(2) obtain r where
4.72 - crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
4.73 - and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
4.74 + crel_mapM: "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
4.75 + and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
4.76 by (auto elim!: crelE crel_nth crel_return)
4.77 - from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)"
4.78 + from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)"
4.79 by arith
4.80 with Suc.hyps[OF crel_mapM] xs_def show ?case
4.81 - unfolding Heap.length_def
4.82 + unfolding Array.length_def
4.83 by (auto simp add: nth_drop')
4.84 qed
4.85
4.86 @@ -186,17 +186,17 @@
4.87 assumes "crel (Array.freeze a) h h' xs"
4.88 obtains "h = h'" "xs = get_array a h"
4.89 proof
4.90 - from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
4.91 + from assms have "crel (mapM (Array.nth a) [0..<Array.length a h]) h h' xs"
4.92 unfolding freeze_def
4.93 by (auto elim: crelE crel_length)
4.94 - hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
4.95 + hence "crel (mapM (Array.nth a) [(Array.length a h - Array.length a h)..<Array.length a h]) h h' xs"
4.96 by simp
4.97 from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
4.98 qed
4.99
4.100 lemma crel_mapM_map_entry_remains:
4.101 - assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
4.102 - assumes "i < Heap.length a h - n"
4.103 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
4.104 + assumes "i < Array.length a h - n"
4.105 shows "get_array a h ! i = get_array a h' ! i"
4.106 using assms
4.107 proof (induct n arbitrary: h h' r)
4.108 @@ -205,23 +205,23 @@
4.109 by (auto elim: crel_return)
4.110 next
4.111 case (Suc n)
4.112 - let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
4.113 - 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]"
4.114 + let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
4.115 + 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]"
4.116 by (simp add: upt_conv_Cons')
4.117 from Suc(2) this obtain r where
4.118 - crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
4.119 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
4.120 by (auto simp add: elim!: crelE crel_map_entry crel_return)
4.121 - have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
4.122 - 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"
4.123 + have length_remains: "Array.length a ?h1 = Array.length a h" by simp
4.124 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
4.125 by simp
4.126 from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
4.127 qed
4.128
4.129 lemma crel_mapM_map_entry_changes:
4.130 - assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
4.131 - assumes "n \<le> Heap.length a h"
4.132 - assumes "i \<ge> Heap.length a h - n"
4.133 - assumes "i < Heap.length a h"
4.134 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
4.135 + assumes "n \<le> Array.length a h"
4.136 + assumes "i \<ge> Array.length a h - n"
4.137 + assumes "i < Array.length a h"
4.138 shows "get_array a h' ! i = f (get_array a h ! i)"
4.139 using assms
4.140 proof (induct n arbitrary: h h' r)
4.141 @@ -230,54 +230,54 @@
4.142 by (auto elim!: crel_return)
4.143 next
4.144 case (Suc n)
4.145 - let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
4.146 - 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]"
4.147 + let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
4.148 + 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]"
4.149 by (simp add: upt_conv_Cons')
4.150 from Suc(2) this obtain r where
4.151 - crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
4.152 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
4.153 by (auto simp add: elim!: crelE crel_map_entry crel_return)
4.154 - have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
4.155 - from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
4.156 - from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
4.157 - from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
4.158 - 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"
4.159 + have length_remains: "Array.length a ?h1 = Array.length a h" by simp
4.160 + from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
4.161 + from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
4.162 + from Suc(4) length_remains have cases: "i = Array.length a ?h1 - Suc n \<or> i \<ge> Array.length a ?h1 - n" by arith
4.163 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
4.164 by simp
4.165 from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
4.166 - crel_mapM_map_entry_remains[OF this, of "Heap.length a h - Suc n", symmetric] less less2
4.167 + crel_mapM_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
4.168 show ?case
4.169 - by (auto simp add: nth_list_update_eq Heap.length_def)
4.170 + by (auto simp add: nth_list_update_eq Array.length_def)
4.171 qed
4.172
4.173 lemma crel_mapM_map_entry_length:
4.174 - assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
4.175 - assumes "n \<le> Heap.length a h"
4.176 - shows "Heap.length a h' = Heap.length a h"
4.177 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
4.178 + assumes "n \<le> Array.length a h"
4.179 + shows "Array.length a h' = Array.length a h"
4.180 using assms
4.181 proof (induct n arbitrary: h h' r)
4.182 case 0
4.183 thus ?case by (auto elim!: crel_return)
4.184 next
4.185 case (Suc n)
4.186 - let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
4.187 - 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]"
4.188 + let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
4.189 + 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]"
4.190 by (simp add: upt_conv_Cons')
4.191 from Suc(2) this obtain r where
4.192 - crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
4.193 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
4.194 by (auto elim!: crelE crel_map_entry crel_return)
4.195 - have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
4.196 - 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"
4.197 + have length_remains: "Array.length a ?h1 = Array.length a h" by simp
4.198 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
4.199 by simp
4.200 from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
4.201 qed
4.202
4.203 lemma crel_mapM_map_entry:
4.204 -assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Heap.length a h]) h h' r"
4.205 +assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
4.206 shows "get_array a h' = List.map f (get_array a h)"
4.207 proof -
4.208 - 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
4.209 + from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - Array.length a h..<Array.length a h]) h h' r" by simp
4.210 from crel_mapM_map_entry_length[OF this]
4.211 crel_mapM_map_entry_changes[OF this] show ?thesis
4.212 - unfolding Heap.length_def
4.213 + unfolding Array.length_def
4.214 by (auto intro: nth_equalityI)
4.215 qed
4.216
4.217 @@ -322,7 +322,7 @@
4.218 using assms
4.219 unfolding Ref.new_def
4.220 apply (elim crel_heap)
4.221 - unfolding Heap.ref_def
4.222 + unfolding Ref.ref_def
4.223 apply (simp add: Let_def)
4.224 unfolding ref_present_def
4.225 apply auto
4.226 @@ -331,22 +331,22 @@
4.227 done
4.228
4.229 lemma crel_lookup:
4.230 - assumes "crel (!ref) h h' r"
4.231 - obtains "h = h'" "r = get_ref ref h"
4.232 + assumes "crel (!r') h h' r"
4.233 + obtains "h = h'" "r = get_ref r' h"
4.234 using assms
4.235 unfolding Ref.lookup_def
4.236 by (auto elim: crel_heap)
4.237
4.238 lemma crel_update:
4.239 - assumes "crel (ref := v) h h' r"
4.240 - obtains "h' = set_ref ref v h" "r = ()"
4.241 + assumes "crel (r' := v) h h' r"
4.242 + obtains "h' = set_ref r' v h" "r = ()"
4.243 using assms
4.244 unfolding Ref.update_def
4.245 by (auto elim: crel_heap)
4.246
4.247 lemma crel_change:
4.248 - assumes "crel (Ref.change f ref) h h' r"
4.249 - obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
4.250 + assumes "crel (Ref.change f r') h h' r"
4.251 + obtains "h' = set_ref r' (f (get_ref r' h)) h" "r = f (get_ref r' h)"
4.252 using assms
4.253 unfolding Ref.change_def Let_def
4.254 by (auto elim!: crelE crel_lookup crel_update crel_return)
4.255 @@ -431,22 +431,22 @@
4.256 subsection {* Introduction rules for array commands *}
4.257
4.258 lemma crel_lengthI:
4.259 - shows "crel (length a) h h (Heap.length a h)"
4.260 - unfolding length_def
4.261 + shows "crel (Array.len a) h h (Array.length a h)"
4.262 + unfolding len_def
4.263 by (rule crel_heapI') auto
4.264
4.265 (* thm crel_newI for Array.new is missing *)
4.266
4.267 lemma crel_nthI:
4.268 - assumes "i < Heap.length a h"
4.269 + assumes "i < Array.length a h"
4.270 shows "crel (nth a i) h h ((get_array a h) ! i)"
4.271 using assms
4.272 unfolding nth_def
4.273 by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
4.274
4.275 lemma crel_updI:
4.276 - assumes "i < Heap.length a h"
4.277 - shows "crel (upd i v a) h (Heap.upd a i v h) a"
4.278 + assumes "i < Array.length a h"
4.279 + shows "crel (upd i v a) h (Array.change a i v h) a"
4.280 using assms
4.281 unfolding upd_def
4.282 by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
4.283 @@ -467,15 +467,15 @@
4.284 subsubsection {* Introduction rules for reference commands *}
4.285
4.286 lemma crel_lookupI:
4.287 - shows "crel (!ref) h h (get_ref ref h)"
4.288 + shows "crel (!r) h h (get_ref r h)"
4.289 unfolding lookup_def by (auto intro!: crel_heapI')
4.290
4.291 lemma crel_updateI:
4.292 - shows "crel (ref := v) h (set_ref ref v h) ()"
4.293 + shows "crel (r := v) h (set_ref r v h) ()"
4.294 unfolding update_def by (auto intro!: crel_heapI')
4.295
4.296 lemma crel_changeI:
4.297 - shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
4.298 + shows "crel (Ref.change f r) h (set_ref r (f (get_ref r h)) h) (f (get_ref r h))"
4.299 unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
4.300
4.301 subsubsection {* Introduction rules for the assert command *}
4.302 @@ -587,8 +587,8 @@
4.303 subsection {* Introduction rules for array commands *}
4.304
4.305 lemma noError_length:
4.306 - shows "noError (Array.length a) h"
4.307 - unfolding length_def
4.308 + shows "noError (Array.len a) h"
4.309 + unfolding len_def
4.310 by (intro noError_heap)
4.311
4.312 lemma noError_new:
4.313 @@ -596,14 +596,14 @@
4.314 unfolding Array.new_def by (intro noError_heap)
4.315
4.316 lemma noError_upd:
4.317 - assumes "i < Heap.length a h"
4.318 + assumes "i < Array.length a h"
4.319 shows "noError (Array.upd i v a) h"
4.320 using assms
4.321 unfolding upd_def
4.322 by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
4.323
4.324 lemma noError_nth:
4.325 -assumes "i < Heap.length a h"
4.326 +assumes "i < Array.length a h"
4.327 shows "noError (Array.nth a i) h"
4.328 using assms
4.329 unfolding nth_def
4.330 @@ -614,14 +614,14 @@
4.331 unfolding of_list_def by (rule noError_heap)
4.332
4.333 lemma noError_map_entry:
4.334 - assumes "i < Heap.length a h"
4.335 + assumes "i < Array.length a h"
4.336 shows "noError (map_entry i f a) h"
4.337 using assms
4.338 unfolding map_entry_def
4.339 by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
4.340
4.341 lemma noError_swap:
4.342 - assumes "i < Heap.length a h"
4.343 + assumes "i < Array.length a h"
4.344 shows "noError (swap i x a) h"
4.345 using assms
4.346 unfolding swap_def
4.347 @@ -644,23 +644,23 @@
4.348 noError_nth crel_nthI elim: crel_length)
4.349
4.350 lemma noError_mapM_map_entry:
4.351 - assumes "n \<le> Heap.length a h"
4.352 - shows "noError (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h"
4.353 + assumes "n \<le> Array.length a h"
4.354 + shows "noError (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
4.355 using assms
4.356 proof (induct n arbitrary: h)
4.357 case 0
4.358 thus ?case by (auto intro: noError_return)
4.359 next
4.360 case (Suc n)
4.361 - 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]"
4.362 + from Suc.prems 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]"
4.363 by (simp add: upt_conv_Cons')
4.364 - 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
4.365 + 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
4.366 by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
4.367 qed
4.368
4.369 lemma noError_map:
4.370 shows "noError (Array.map f a) h"
4.371 -using noError_mapM_map_entry[of "Heap.length a h" a h]
4.372 +using noError_mapM_map_entry[of "Array.length a h" a h]
4.373 unfolding Array.map_def
4.374 by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
4.375
4.376 @@ -671,15 +671,15 @@
4.377 unfolding Ref.new_def by (intro noError_heap)
4.378
4.379 lemma noError_lookup:
4.380 - shows "noError (!ref) h"
4.381 + shows "noError (!r) h"
4.382 unfolding lookup_def by (intro noError_heap)
4.383
4.384 lemma noError_update:
4.385 - shows "noError (ref := v) h"
4.386 + shows "noError (r := v) h"
4.387 unfolding update_def by (intro noError_heap)
4.388
4.389 lemma noError_change:
4.390 - shows "noError (Ref.change f ref) h"
4.391 + shows "noError (Ref.change f r) h"
4.392 unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
4.393
4.394 subsection {* Introduction rules for the assert command *}
5.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Jul 05 15:36:37 2010 +0200
5.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Jul 05 16:46:23 2010 +0200
5.3 @@ -27,7 +27,7 @@
5.4 = multiset_of (get_array a h)"
5.5 using assms
5.6 unfolding swap_def
5.7 - by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
5.8 + by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
5.9
5.10 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
5.11 where
5.12 @@ -101,7 +101,7 @@
5.13
5.14 lemma part_length_remains:
5.15 assumes "crel (part1 a l r p) h h' rs"
5.16 - shows "Heap.length a h = Heap.length a h'"
5.17 + shows "Array.length a h = Array.length a h'"
5.18 using assms
5.19 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
5.20 case (1 a l r p h h' rs)
5.21 @@ -207,7 +207,7 @@
5.22 by (elim crelE crel_nth crel_if crel_return) auto
5.23 from swp False have "get_array a h1 ! r \<ge> p"
5.24 unfolding swap_def
5.25 - by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
5.26 + by (auto simp add: Array.length_def elim!: crelE crel_nth crel_upd crel_return)
5.27 with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
5.28 by fastsimp
5.29 have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
5.30 @@ -243,7 +243,7 @@
5.31
5.32 lemma partition_length_remains:
5.33 assumes "crel (partition a l r) h h' rs"
5.34 - shows "Heap.length a h = Heap.length a h'"
5.35 + shows "Array.length a h = Array.length a h'"
5.36 proof -
5.37 from assms part_length_remains show ?thesis
5.38 unfolding partition.simps swap_def
5.39 @@ -287,14 +287,14 @@
5.40 else middle)"
5.41 unfolding partition.simps
5.42 by (elim crelE crel_return crel_nth crel_if crel_upd) simp
5.43 - from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
5.44 - (Heap.upd a rs (get_array a h1 ! r) h1)"
5.45 + from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
5.46 + (Array.change a rs (get_array a h1 ! r) h1)"
5.47 unfolding swap_def
5.48 by (elim crelE crel_return crel_nth crel_upd) simp
5.49 - from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
5.50 + from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
5.51 unfolding swap_def
5.52 by (elim crelE crel_return crel_nth crel_upd) simp
5.53 - from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
5.54 + from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
5.55 unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
5.56 from `l < r` have "l \<le> r - 1" by simp
5.57 note middle_in_bounds = part_returns_index_in_bounds[OF part this]
5.58 @@ -304,7 +304,7 @@
5.59 with swap
5.60 have right_remains: "get_array a h ! r = get_array a h' ! rs"
5.61 unfolding swap_def
5.62 - by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
5.63 + by (auto simp add: Array.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
5.64 from part_partitions [OF part]
5.65 show ?thesis
5.66 proof (cases "get_array a h1 ! middle \<le> ?pivot")
5.67 @@ -314,12 +314,12 @@
5.68 fix i
5.69 assume i_is_left: "l \<le> i \<and> i < rs"
5.70 with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
5.71 - have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
5.72 + have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
5.73 from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
5.74 with part_partitions[OF part] right_remains True
5.75 have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
5.76 with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
5.77 - unfolding Heap.upd_def Heap.length_def by simp
5.78 + unfolding Array.change_def Array.length_def by simp
5.79 }
5.80 moreover
5.81 {
5.82 @@ -331,7 +331,7 @@
5.83 proof
5.84 assume i_is: "rs < i \<and> i \<le> r - 1"
5.85 with swap_length_remains in_bounds middle_in_bounds rs_equals
5.86 - have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
5.87 + have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
5.88 from part_partitions[OF part] rs_equals right_remains i_is
5.89 have "get_array a h' ! rs \<le> get_array a h1 ! i"
5.90 by fastsimp
5.91 @@ -345,7 +345,7 @@
5.92 by fastsimp
5.93 with i_is True rs_equals right_remains h'_def
5.94 show ?thesis using in_bounds
5.95 - unfolding Heap.upd_def Heap.length_def
5.96 + unfolding Array.change_def Array.length_def
5.97 by auto
5.98 qed
5.99 }
5.100 @@ -357,11 +357,11 @@
5.101 fix i
5.102 assume i_is_left: "l \<le> i \<and> i < rs"
5.103 with swap_length_remains in_bounds middle_in_bounds rs_equals
5.104 - have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
5.105 + have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
5.106 from part_partitions[OF part] rs_equals right_remains i_is_left
5.107 have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
5.108 with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
5.109 - unfolding Heap.upd_def by simp
5.110 + unfolding Array.change_def by simp
5.111 }
5.112 moreover
5.113 {
5.114 @@ -372,7 +372,7 @@
5.115 proof
5.116 assume i_is: "rs < i \<and> i \<le> r - 1"
5.117 with swap_length_remains in_bounds middle_in_bounds rs_equals
5.118 - have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
5.119 + have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
5.120 from part_partitions[OF part] rs_equals right_remains i_is
5.121 have "get_array a h' ! rs \<le> get_array a h1 ! i"
5.122 by fastsimp
5.123 @@ -381,7 +381,7 @@
5.124 assume i_is: "i = r"
5.125 from i_is False rs_equals right_remains h'_def
5.126 show ?thesis using in_bounds
5.127 - unfolding Heap.upd_def Heap.length_def
5.128 + unfolding Array.change_def Array.length_def
5.129 by auto
5.130 qed
5.131 }
5.132 @@ -425,7 +425,7 @@
5.133
5.134 lemma length_remains:
5.135 assumes "crel (quicksort a l r) h h' rs"
5.136 - shows "Heap.length a h = Heap.length a h'"
5.137 + shows "Array.length a h = Array.length a h'"
5.138 using assms
5.139 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
5.140 case (1 a l r h h' rs)
5.141 @@ -482,7 +482,7 @@
5.142
5.143 lemma quicksort_sorts:
5.144 assumes "crel (quicksort a l r) h h' rs"
5.145 - assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h"
5.146 + assumes l_r_length: "l < Array.length a h" "r < Array.length a h"
5.147 shows "sorted (subarray l (r + 1) a h')"
5.148 using assms
5.149 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
5.150 @@ -524,7 +524,7 @@
5.151 from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
5.152 length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
5.153 have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
5.154 - unfolding Heap.length_def subarray_def by (cases p, auto)
5.155 + unfolding Array.length_def subarray_def by (cases p, auto)
5.156 with left_subarray_remains part_conds1 pivot_unchanged
5.157 have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
5.158 by (simp, subst set_of_multiset_of[symmetric], simp)
5.159 @@ -535,7 +535,7 @@
5.160 from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
5.161 length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
5.162 have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
5.163 - unfolding Heap.length_def subarray_def by auto
5.164 + unfolding Array.length_def subarray_def by auto
5.165 with right_subarray_remains part_conds2 pivot_unchanged
5.166 have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
5.167 by (simp, subst set_of_multiset_of[symmetric], simp)
5.168 @@ -556,18 +556,18 @@
5.169
5.170
5.171 lemma quicksort_is_sort:
5.172 - assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
5.173 + assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
5.174 shows "get_array a h' = sort (get_array a h)"
5.175 proof (cases "get_array a h = []")
5.176 case True
5.177 with quicksort_is_skip[OF crel] show ?thesis
5.178 - unfolding Heap.length_def by simp
5.179 + unfolding Array.length_def by simp
5.180 next
5.181 case False
5.182 from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
5.183 - unfolding Heap.length_def subarray_def by auto
5.184 + unfolding Array.length_def subarray_def by auto
5.185 with length_remains[OF crel] have "sorted (get_array a h')"
5.186 - unfolding Heap.length_def by simp
5.187 + unfolding Array.length_def by simp
5.188 with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
5.189 qed
5.190
5.191 @@ -576,7 +576,7 @@
5.192 We will now show that exceptions do not occur. *}
5.193
5.194 lemma noError_part1:
5.195 - assumes "l < Heap.length a h" "r < Heap.length a h"
5.196 + assumes "l < Array.length a h" "r < Array.length a h"
5.197 shows "noError (part1 a l r p) h"
5.198 using assms
5.199 proof (induct a l r p arbitrary: h rule: part1.induct)
5.200 @@ -587,7 +587,7 @@
5.201 qed
5.202
5.203 lemma noError_partition:
5.204 - assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
5.205 + assumes "l < r" "l < Array.length a h" "r < Array.length a h"
5.206 shows "noError (partition a l r) h"
5.207 using assms
5.208 unfolding partition.simps swap_def
5.209 @@ -603,7 +603,7 @@
5.210 done
5.211
5.212 lemma noError_quicksort:
5.213 - assumes "l < Heap.length a h" "r < Heap.length a h"
5.214 + assumes "l < Array.length a h" "r < Array.length a h"
5.215 shows "noError (quicksort a l r) h"
5.216 using assms
5.217 proof (induct a l r arbitrary: h rule: quicksort.induct)
5.218 @@ -628,7 +628,7 @@
5.219 subsection {* Example *}
5.220
5.221 definition "qsort a = do
5.222 - k \<leftarrow> length a;
5.223 + k \<leftarrow> len a;
5.224 quicksort a 0 (k - 1);
5.225 return a
5.226 done"
6.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon Jul 05 15:36:37 2010 +0200
6.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon Jul 05 16:46:23 2010 +0200
6.3 @@ -37,7 +37,7 @@
6.4 else get_array a h ! k)"
6.5 using assms unfolding swap.simps
6.6 by (elim crel_elim_all)
6.7 - (auto simp: Heap.length_def)
6.8 + (auto simp: length_def)
6.9
6.10 lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
6.11 shows "get_array a h' ! k = (if k < i then get_array a h ! k
6.12 @@ -69,7 +69,7 @@
6.13
6.14 lemma rev_length:
6.15 assumes "crel (rev a i j) h h' r"
6.16 - shows "Heap.length a h = Heap.length a h'"
6.17 + shows "Array.length a h = Array.length a h'"
6.18 using assms
6.19 proof (induct a i j arbitrary: h h' rule: rev.induct)
6.20 case (1 a i j h h'')
6.21 @@ -93,7 +93,7 @@
6.22 qed
6.23
6.24 lemma rev2_rev': assumes "crel (rev a i j) h h' u"
6.25 - assumes "j < Heap.length a h"
6.26 + assumes "j < Array.length a h"
6.27 shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
6.28 proof -
6.29 {
6.30 @@ -103,15 +103,15 @@
6.31 by auto
6.32 }
6.33 with assms(2) rev_length[OF assms(1)] show ?thesis
6.34 - unfolding subarray_def Heap.length_def
6.35 + unfolding subarray_def Array.length_def
6.36 by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
6.37 qed
6.38
6.39 lemma rev2_rev:
6.40 - assumes "crel (rev a 0 (Heap.length a h - 1)) h h' u"
6.41 + assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
6.42 shows "get_array a h' = List.rev (get_array a h)"
6.43 using rev2_rev'[OF assms] rev_length[OF assms] assms
6.44 - by (cases "Heap.length a h = 0", auto simp add: Heap.length_def
6.45 + by (cases "Array.length a h = 0", auto simp add: Array.length_def
6.46 subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all)
6.47 (drule sym[of "List.length (get_array a h)"], simp)
6.48
7.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Jul 05 15:36:37 2010 +0200
7.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Jul 05 16:46:23 2010 +0200
7.3 @@ -123,25 +123,25 @@
7.4 "array_ran a h = {e. Some e \<in> set (get_array a h)}"
7.5 -- {*FIXME*}
7.6
7.7 -lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
7.8 -unfolding array_ran_def Heap.length_def by simp
7.9 +lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
7.10 +unfolding array_ran_def Array.length_def by simp
7.11
7.12 lemma array_ran_upd_array_Some:
7.13 - assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)"
7.14 + assumes "cl \<in> array_ran a (Array.change a i (Some b) h)"
7.15 shows "cl \<in> array_ran a h \<or> cl = b"
7.16 proof -
7.17 have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
7.18 with assms show ?thesis
7.19 - unfolding array_ran_def Heap.upd_def by fastsimp
7.20 + unfolding array_ran_def Array.change_def by fastsimp
7.21 qed
7.22
7.23 lemma array_ran_upd_array_None:
7.24 - assumes "cl \<in> array_ran a (Heap.upd a i None h)"
7.25 + assumes "cl \<in> array_ran a (Array.change a i None h)"
7.26 shows "cl \<in> array_ran a h"
7.27 proof -
7.28 have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
7.29 with assms show ?thesis
7.30 - unfolding array_ran_def Heap.upd_def by auto
7.31 + unfolding array_ran_def Array.change_def by auto
7.32 qed
7.33
7.34 definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
7.35 @@ -152,7 +152,7 @@
7.36 lemma correctArray_update:
7.37 assumes "correctArray rcs a h"
7.38 assumes "correctClause rcs c" "sorted c" "distinct c"
7.39 - shows "correctArray rcs a (Heap.upd a i (Some c) h)"
7.40 + shows "correctArray rcs a (Array.change a i (Some c) h)"
7.41 using assms
7.42 unfolding correctArray_def
7.43 by (auto dest:array_ran_upd_array_Some)
7.44 @@ -471,7 +471,7 @@
7.45 fix clj
7.46 let ?rs = "merge (remove l cli) (remove (compl l) clj)"
7.47 let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
7.48 - assume "h = h'" "Some clj = get_array a h' ! j" "j < Heap.length a h'"
7.49 + assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length a h'"
7.50 with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj"
7.51 unfolding correctArray_def by (auto intro: array_ranI)
7.52 with clj l_not_zero correct_cli
7.53 @@ -485,7 +485,7 @@
7.54 }
7.55 {
7.56 fix v clj
7.57 - assume "Some clj = get_array a h ! j" "j < Heap.length a h"
7.58 + assume "Some clj = get_array a h ! j" "j < Array.length a h"
7.59 with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
7.60 unfolding correctArray_def by (auto intro: array_ranI)
7.61 assume "crel (res_thm' l cli clj) h h' rs"
8.1 --- a/src/HOL/Imperative_HOL/ex/Subarray.thy Mon Jul 05 15:36:37 2010 +0200
8.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Mon Jul 05 16:46:23 2010 +0200
8.3 @@ -8,65 +8,64 @@
8.4 imports Array Sublist
8.5 begin
8.6
8.7 -definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
8.8 -where
8.9 +definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
8.10 "subarray n m a h \<equiv> sublist' n m (get_array a h)"
8.11
8.12 -lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
8.13 -apply (simp add: subarray_def Heap.upd_def)
8.14 +lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
8.15 +apply (simp add: subarray_def Array.change_def)
8.16 apply (simp add: sublist'_update1)
8.17 done
8.18
8.19 -lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
8.20 -apply (simp add: subarray_def Heap.upd_def)
8.21 +lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
8.22 +apply (simp add: subarray_def Array.change_def)
8.23 apply (subst sublist'_update2)
8.24 apply fastsimp
8.25 apply simp
8.26 done
8.27
8.28 -lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]"
8.29 -unfolding subarray_def Heap.upd_def
8.30 +lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h[i - n := v]"
8.31 +unfolding subarray_def Array.change_def
8.32 by (simp add: sublist'_update3)
8.33
8.34 lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
8.35 by (simp add: subarray_def sublist'_Nil')
8.36
8.37 -lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]"
8.38 -by (simp add: subarray_def Heap.length_def sublist'_single)
8.39 +lemma subarray_single: "\<lbrakk> n < Array.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]"
8.40 +by (simp add: subarray_def length_def sublist'_single)
8.41
8.42 -lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
8.43 -by (simp add: subarray_def Heap.length_def length_sublist')
8.44 +lemma length_subarray: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
8.45 +by (simp add: subarray_def length_def length_sublist')
8.46
8.47 -lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
8.48 +lemma length_subarray_0: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
8.49 by (simp add: length_subarray)
8.50
8.51 -lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
8.52 -unfolding Heap.length_def subarray_def
8.53 +lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
8.54 +unfolding Array.length_def subarray_def
8.55 by (simp add: sublist'_front)
8.56
8.57 -lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
8.58 -unfolding Heap.length_def subarray_def
8.59 +lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
8.60 +unfolding Array.length_def subarray_def
8.61 by (simp add: sublist'_back)
8.62
8.63 lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
8.64 unfolding subarray_def
8.65 by (simp add: sublist'_append)
8.66
8.67 -lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
8.68 -unfolding Heap.length_def subarray_def
8.69 +lemma subarray_all: "subarray 0 (Array.length a h) a h = get_array a h"
8.70 +unfolding Array.length_def subarray_def
8.71 by (simp add: sublist'_all)
8.72
8.73 -lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
8.74 -unfolding Heap.length_def subarray_def
8.75 +lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
8.76 +unfolding Array.length_def subarray_def
8.77 by (simp add: nth_sublist')
8.78
8.79 -lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
8.80 -unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
8.81 +lemma subarray_eq_samelength_iff: "Array.length a h = Array.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
8.82 +unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
8.83
8.84 -lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
8.85 -unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
8.86 +lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))"
8.87 +unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
8.88
8.89 -lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
8.90 -unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
8.91 +lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))"
8.92 +unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
8.93
8.94 end
8.95 \ No newline at end of file