--- a/src/HOL/Imperative_HOL/Array.thy Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Mon Jul 05 16:46:23 2010 +0200
@@ -8,24 +8,132 @@
imports Heap_Monad
begin
+subsection {* Primitive layer *}
+
+definition
+ array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
+ "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
+
+definition
+ get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
+ "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
+
+definition
+ set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
+ "set_array a x =
+ arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
+
+definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
+ "array xs h = (let
+ l = lim h;
+ r = Array l;
+ h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
+ in (r, h''))"
+
+definition length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
+ "length a h = List.length (get_array a h)"
+
+definition change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
+ "change a i x h = set_array a ((get_array a h)[i:=x]) h"
+
+text {* Properties of imperative arrays *}
+
+text {* FIXME: Does there exist a "canonical" array axiomatisation in
+the literature? *}
+
+definition noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) where
+ "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
+
+lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
+ and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
+ unfolding noteq_arrs_def by auto
+
+lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
+ unfolding noteq_arrs_def by auto
+
+lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
+ by (simp add: array_present_def noteq_arrs_def array_def Let_def)
+
+lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
+ by (simp add: get_array_def set_array_def o_def)
+
+lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
+ by (simp add: noteq_arrs_def get_array_def set_array_def)
+
+lemma set_array_same [simp]:
+ "set_array r x (set_array r y h) = set_array r x h"
+ by (simp add: set_array_def)
+
+lemma array_set_set_swap:
+ "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
+ by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
+
+lemma get_array_change_eq [simp]:
+ "get_array a (change a i v h) = (get_array a h) [i := v]"
+ by (simp add: change_def)
+
+lemma nth_change_array_neq_array [simp]:
+ "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
+ by (simp add: change_def noteq_arrs_def)
+
+lemma get_arry_array_change_elem_neqIndex [simp]:
+ "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
+ by simp
+
+lemma length_change [simp]:
+ "length a (change b i v h) = length a h"
+ by (simp add: change_def length_def set_array_def get_array_def)
+
+lemma change_swap_neqArray:
+ "a =!!= a' \<Longrightarrow>
+ change a i v (change a' i' v' h)
+ = change a' i' v' (change a i v h)"
+apply (unfold change_def)
+apply simp
+apply (subst array_set_set_swap, assumption)
+apply (subst array_get_set_neq)
+apply (erule noteq_arrs_sym)
+apply (simp)
+done
+
+lemma change_swap_neqIndex:
+ "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)"
+ by (auto simp add: change_def array_set_set_swap list_update_swap)
+
+lemma get_array_init_array_list:
+ "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
+ by (simp add: Let_def split_def array_def)
+
+lemma set_array:
+ "set_array (fst (array ls h))
+ new_ls (snd (array ls h))
+ = snd (array new_ls h)"
+ by (simp add: Let_def split_def array_def)
+
+lemma array_present_change [simp]:
+ "array_present a (change b i v h) = array_present a h"
+ by (simp add: change_def array_present_def set_array_def get_array_def)
+
+
+
subsection {* Primitives *}
definition
new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
- [code del]: "new n x = Heap_Monad.heap (Heap.array (replicate n x))"
+ [code del]: "new n x = Heap_Monad.heap (Array.array (replicate n x))"
definition
of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
- [code del]: "of_list xs = Heap_Monad.heap (Heap.array xs)"
+ [code del]: "of_list xs = Heap_Monad.heap (Array.array xs)"
definition
- length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
- [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
+ len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
+ [code del]: "len arr = Heap_Monad.heap (\<lambda>h. (Array.length arr h, h))"
definition
nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
where
- [code del]: "nth a i = (do len \<leftarrow> length a;
+ [code del]: "nth a i = (do len \<leftarrow> len a;
(if i < len
then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
else raise ''array lookup: index out of range'')
@@ -34,9 +142,9 @@
definition
upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
where
- [code del]: "upd i x a = (do len \<leftarrow> length a;
+ [code del]: "upd i x a = (do len \<leftarrow> len a;
(if i < len
- then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
+ then Heap_Monad.heap (\<lambda>h. (a, change a i x h))
else raise ''array update: index out of range'')
done)"
@@ -73,7 +181,7 @@
freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
where
"freeze a = (do
- n \<leftarrow> length a;
+ n \<leftarrow> len a;
mapM (nth a) [0..<n]
done)"
@@ -81,12 +189,11 @@
map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
where
"map f a = (do
- n \<leftarrow> length a;
+ n \<leftarrow> len a;
mapM (\<lambda>n. map_entry n f a) [0..<n];
return a
done)"
-hide_const (open) new map -- {* avoid clashed with some popular names *}
subsection {* Properties *}
@@ -125,12 +232,12 @@
"Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
by (simp add: make'_def o_def)
-definition length' where
- [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
-hide_const (open) length'
+definition len' where
+ [code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
+hide_const (open) len'
lemma [code]:
- "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
- by (simp add: length'_def)
+ "Array.len a = Array.len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
+ by (simp add: len'_def)
definition nth' where
[code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
@@ -154,7 +261,7 @@
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
-code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
+code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
@@ -167,7 +274,7 @@
code_const Array (OCaml "failwith/ \"bare Array\"")
code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
-code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
+code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
@@ -180,8 +287,10 @@
code_const Array (Haskell "error/ \"bare Array\"")
code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
-code_const Array.length' (Haskell "Heap.lengthArray")
+code_const Array.len' (Haskell "Heap.lengthArray")
code_const Array.nth' (Haskell "Heap.readArray")
code_const Array.upd' (Haskell "Heap.writeArray")
+hide_const (open) new map -- {* avoid clashed with some popular names *}
+
end
--- a/src/HOL/Imperative_HOL/Heap.thy Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Mon Jul 05 16:46:23 2010 +0200
@@ -37,7 +37,10 @@
subsection {* A polymorphic heap with dynamic arrays and references *}
-subsubsection {* Type definitions *}
+text {*
+ References and arrays are developed in parallel,
+ but keeping them separate makes some later proofs simpler.
+*}
types addr = nat -- "untyped heap references"
types heap_rep = nat -- "representable values"
@@ -82,283 +85,4 @@
#> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
*}
-
-subsection {* Imperative references and arrays *}
-
-text {*
- References and arrays are developed in parallel,
- but keeping them separate makes some later proofs simpler.
-*}
-
-subsubsection {* Primitive operations *}
-
-definition
- ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
- "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
-
-definition
- array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
- "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
-
-definition
- get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where
- "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))"
-
-definition
- get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
- "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
-
-definition
- set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
- "set_ref r x =
- refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
-
-definition
- set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
- "set_array a x =
- arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
-
-definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
- "ref x h = (let
- l = lim h;
- r = Ref l;
- h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>)
- in (r, h''))"
-
-definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
- "array xs h = (let
- l = lim h;
- r = Array l;
- h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
- in (r, h''))"
-
-definition
- upd :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
- "upd a i x h = set_array a ((get_array a h)[i:=x]) h"
-
-definition
- length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
- "length a h = size (get_array a h)"
-
-
-subsubsection {* Reference equality *}
-
-text {*
- The following relations are useful for comparing arrays and references.
-*}
-
-definition
- noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70)
-where
- "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
-
-definition
- noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70)
-where
- "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
-
-lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
- and noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
- and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
- and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
-unfolding noteq_refs_def noteq_arrs_def by auto
-
-lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
- unfolding noteq_refs_def by auto
-
-lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
- by (simp add: ref_present_def ref_def Let_def noteq_refs_def)
-
-lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
- by (simp add: array_present_def noteq_arrs_def array_def Let_def)
-
-
-subsubsection {* Properties of heap containers *}
-
-text {* Properties of imperative arrays *}
-
-text {* FIXME: Does there exist a "canonical" array axiomatisation in
-the literature? *}
-
-lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
- by (simp add: get_array_def set_array_def o_def)
-
-lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
- by (simp add: noteq_arrs_def get_array_def set_array_def)
-
-lemma set_array_same [simp]:
- "set_array r x (set_array r y h) = set_array r x h"
- by (simp add: set_array_def)
-
-lemma array_set_set_swap:
- "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
- by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
-
-lemma array_ref_set_set_swap:
- "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)"
- by (simp add: Let_def expand_fun_eq set_array_def set_ref_def)
-
-lemma get_array_upd_eq [simp]:
- "get_array a (upd a i v h) = (get_array a h) [i := v]"
- by (simp add: upd_def)
-
-lemma nth_upd_array_neq_array [simp]:
- "a =!!= b \<Longrightarrow> get_array a (upd b j v h) ! i = get_array a h ! i"
- by (simp add: upd_def noteq_arrs_def)
-
-lemma get_arry_array_upd_elem_neqIndex [simp]:
- "i \<noteq> j \<Longrightarrow> get_array a (upd a j v h) ! i = get_array a h ! i"
- by simp
-
-lemma length_upd_eq [simp]:
- "length a (upd a i v h) = length a h"
- by (simp add: length_def upd_def)
-
-lemma length_upd_neq [simp]:
- "length a (upd b i v h) = length a h"
- by (simp add: upd_def length_def set_array_def get_array_def)
-
-lemma upd_swap_neqArray:
- "a =!!= a' \<Longrightarrow>
- upd a i v (upd a' i' v' h)
- = upd a' i' v' (upd a i v h)"
-apply (unfold upd_def)
-apply simp
-apply (subst array_set_set_swap, assumption)
-apply (subst array_get_set_neq)
-apply (erule noteq_arrs_sym)
-apply (simp)
-done
-
-lemma upd_swap_neqIndex:
- "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> upd a i v (upd a i' v' h) = upd a i' v' (upd a i v h)"
-by (auto simp add: upd_def array_set_set_swap list_update_swap)
-
-lemma get_array_init_array_list:
- "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
- by (simp add: Let_def split_def array_def)
-
-lemma set_array:
- "set_array (fst (array ls h))
- new_ls (snd (array ls h))
- = snd (array new_ls h)"
- by (simp add: Let_def split_def array_def)
-
-lemma array_present_upd [simp]:
- "array_present a (upd b i v h) = array_present a h"
- by (simp add: upd_def array_present_def set_array_def get_array_def)
-
-(*lemma array_of_list_replicate:
- "array_of_list (replicate n x) = array n x"
- by (simp add: expand_fun_eq array_of_list_def array_def)*)
-
-text {* Properties of imperative references *}
-
-lemma next_ref_fresh [simp]:
- assumes "(r, h') = ref x h"
- shows "\<not> ref_present r h"
- using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def)
-
-lemma next_ref_present [simp]:
- assumes "(r, h') = ref x h"
- shows "ref_present r h'"
- using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def)
-
-lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
- by (simp add: get_ref_def set_ref_def)
-
-lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h"
- by (simp add: noteq_refs_def get_ref_def set_ref_def)
-
-(* FIXME: We need some infrastructure to infer that locally generated
- new refs (by new_ref(_no_init), new_array(')) are distinct
- from all existing refs.
-*)
-
-lemma ref_set_get: "set_ref r (get_ref r h) h = h"
-apply (simp add: set_ref_def get_ref_def)
-oops
-
-lemma set_ref_same[simp]:
- "set_ref r x (set_ref r y h) = set_ref r x h"
- by (simp add: set_ref_def)
-
-lemma ref_set_set_swap:
- "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)"
- by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
-
-lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
- by (simp add: ref_def set_ref_def Let_def)
-
-lemma ref_get_new [simp]:
- "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
- by (simp add: ref_def Let_def split_def)
-
-lemma ref_set_new [simp]:
- "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)"
- by (simp add: ref_def Let_def split_def)
-
-lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow>
- get_ref r (snd (ref v h)) = get_ref r h"
- by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def)
-
-lemma lim_set_ref [simp]:
- "lim (set_ref r v h) = lim h"
- by (simp add: set_ref_def)
-
-lemma ref_present_new_ref [simp]:
- "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
- by (simp add: ref_present_def ref_def Let_def)
-
-lemma ref_present_set_ref [simp]:
- "ref_present r (set_ref r' v h) = ref_present r h"
- by (simp add: set_ref_def ref_present_def)
-
-lemma noteq_refsI: "\<lbrakk> ref_present r h; \<not>ref_present r' h \<rbrakk> \<Longrightarrow> r =!= r'"
- unfolding noteq_refs_def ref_present_def
- by auto
-
-text {* Non-interaction between imperative array and imperative references *}
-
-lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
- by (simp add: get_array_def set_ref_def)
-
-lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i"
- by simp
-
-lemma get_ref_upd [simp]: "get_ref r (upd a i v h) = get_ref r h"
- by (simp add: get_ref_def set_array_def upd_def)
-
-lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
- by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def)
-
-text {*not actually true ???*}
-lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
-apply (case_tac a)
-apply (simp add: Let_def upd_def)
-apply auto
-oops
-
-lemma length_new_ref[simp]:
- "length a (snd (ref v h)) = length a h"
- by (simp add: get_array_def set_ref_def length_def ref_def Let_def)
-
-lemma get_array_new_ref [simp]:
- "get_array a (snd (ref v h)) = get_array a h"
- by (simp add: ref_def set_ref_def get_array_def Let_def)
-
-lemma ref_present_upd [simp]:
- "ref_present r (upd a i v h) = ref_present r h"
- by (simp add: upd_def ref_present_def set_array_def get_array_def)
-
-lemma array_present_set_ref [simp]:
- "array_present a (set_ref r v h) = array_present a h"
- by (simp add: array_present_def set_ref_def)
-
-lemma array_present_new_ref [simp]:
- "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
- by (simp add: array_present_def ref_def Let_def)
-
-hide_const (open) empty upd length array ref
-
end
--- a/src/HOL/Imperative_HOL/Ref.thy Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Mon Jul 05 16:46:23 2010 +0200
@@ -5,7 +5,7 @@
header {* Monadic references *}
theory Ref
-imports Heap_Monad
+imports Array
begin
text {*
@@ -14,11 +14,111 @@
and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
*}
+subsection {* Primitive layer *}
+
+definition
+ ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
+ "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
+
+definition
+ get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where
+ "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))"
+
+definition
+ set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
+ "set_ref r x =
+ refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
+
+definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
+ "ref x h = (let
+ l = lim h;
+ r = Ref l;
+ h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>)
+ in (r, h''))"
+
+definition noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70) where
+ "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
+
+lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
+ and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
+ unfolding noteq_refs_def by auto
+
+lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
+ unfolding noteq_refs_def by auto
+
+lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
+ by (simp add: ref_present_def ref_def Let_def noteq_refs_def)
+
+lemma next_ref_fresh [simp]:
+ assumes "(r, h') = ref x h"
+ shows "\<not> ref_present r h"
+ using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def)
+
+lemma next_ref_present [simp]:
+ assumes "(r, h') = ref x h"
+ shows "ref_present r h'"
+ using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def)
+
+lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
+ by (simp add: get_ref_def set_ref_def)
+
+lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h"
+ by (simp add: noteq_refs_def get_ref_def set_ref_def)
+
+(* FIXME: We need some infrastructure to infer that locally generated
+ new refs (by new_ref(_no_init), new_array(')) are distinct
+ from all existing refs.
+*)
+
+lemma ref_set_get: "set_ref r (get_ref r h) h = h"
+apply (simp add: set_ref_def get_ref_def)
+oops
+
+lemma set_ref_same[simp]:
+ "set_ref r x (set_ref r y h) = set_ref r x h"
+ by (simp add: set_ref_def)
+
+lemma ref_set_set_swap:
+ "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)"
+ by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
+
+lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
+ by (simp add: ref_def set_ref_def Let_def)
+
+lemma ref_get_new [simp]:
+ "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
+ by (simp add: ref_def Let_def split_def)
+
+lemma ref_set_new [simp]:
+ "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)"
+ by (simp add: ref_def Let_def split_def)
+
+lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow>
+ get_ref r (snd (ref v h)) = get_ref r h"
+ by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def)
+
+lemma lim_set_ref [simp]:
+ "lim (set_ref r v h) = lim h"
+ by (simp add: set_ref_def)
+
+lemma ref_present_new_ref [simp]:
+ "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
+ by (simp add: ref_present_def ref_def Let_def)
+
+lemma ref_present_set_ref [simp]:
+ "ref_present r (set_ref r' v h) = ref_present r h"
+ by (simp add: set_ref_def ref_present_def)
+
+lemma noteq_refsI: "\<lbrakk> ref_present r h; \<not>ref_present r' h \<rbrakk> \<Longrightarrow> r =!= r'"
+ unfolding noteq_refs_def ref_present_def
+ by auto
+
+
subsection {* Primitives *}
definition
new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
- [code del]: "new v = Heap_Monad.heap (Heap.ref v)"
+ [code del]: "new v = Heap_Monad.heap (Ref.ref v)"
definition
lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
@@ -55,6 +155,48 @@
by (auto simp add: change_def lookup_chain)
+text {* Non-interaction between imperative array and imperative references *}
+
+lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
+ by (simp add: get_array_def set_ref_def)
+
+lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i"
+ by simp
+
+lemma get_ref_upd [simp]: "get_ref r (Array.change a i v h) = get_ref r h"
+ by (simp add: get_ref_def set_array_def Array.change_def)
+
+lemma new_ref_upd: "fst (ref v (Array.change a i v' h)) = fst (ref v h)"
+ by (simp add: set_array_def get_array_def Let_def ref_new_set Array.change_def ref_def)
+
+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)"
+ by (simp add: set_ref_def Array.change_def get_array_def set_array_def)
+
+lemma length_new_ref[simp]:
+ "length a (snd (ref v h)) = length a h"
+ by (simp add: get_array_def set_ref_def length_def ref_def Let_def)
+
+lemma get_array_new_ref [simp]:
+ "get_array a (snd (ref v h)) = get_array a h"
+ by (simp add: ref_def set_ref_def get_array_def Let_def)
+
+lemma ref_present_upd [simp]:
+ "ref_present r (Array.change a i v h) = ref_present r h"
+ by (simp add: Array.change_def ref_present_def set_array_def get_array_def)
+
+lemma array_present_set_ref [simp]:
+ "array_present a (set_ref r v h) = array_present a h"
+ by (simp add: array_present_def set_ref_def)
+
+lemma array_present_new_ref [simp]:
+ "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
+ by (simp add: array_present_def ref_def Let_def)
+
+lemma array_ref_set_set_swap:
+ "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)"
+ by (simp add: Let_def expand_fun_eq set_array_def set_ref_def)
+
+
subsection {* Code generator setup *}
subsubsection {* SML *}
--- a/src/HOL/Imperative_HOL/Relational.thy Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy Mon Jul 05 16:46:23 2010 +0200
@@ -91,10 +91,10 @@
subsection {* Elimination rules for array commands *}
lemma crel_length:
- assumes "crel (length a) h h' r"
- obtains "h = h'" "r = Heap.length a h'"
+ assumes "crel (len a) h h' r"
+ obtains "h = h'" "r = Array.length a h'"
using assms
- unfolding length_def
+ unfolding Array.len_def
by (elim crel_heap) simp
(* Strong version of the lemma for this operation is missing *)
@@ -106,14 +106,14 @@
lemma crel_nth[consumes 1]:
assumes "crel (nth a i) h h' r"
- obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
+ obtains "r = (get_array a h) ! i" "h = h'" "i < Array.length a h"
using assms
unfolding nth_def
by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
lemma crel_upd[consumes 1]:
assumes "crel (upd i v a) h h' r"
- obtains "r = a" "h' = Heap.upd a i v h"
+ obtains "r = a" "h' = Array.change a i v h"
using assms
unfolding upd_def
by (elim crelE crel_if crel_return crel_raise
@@ -129,14 +129,14 @@
lemma crel_map_entry:
assumes "crel (Array.map_entry i f a) h h' r"
- obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
+ obtains "r = a" "h' = Array.change a i (f (get_array a h ! i)) h"
using assms
unfolding Array.map_entry_def
by (elim crelE crel_upd crel_nth) auto
lemma crel_swap:
assumes "crel (Array.swap i x a) h h' r"
- obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
+ obtains "r = get_array a h ! i" "h' = Array.change a i x h"
using assms
unfolding Array.swap_def
by (elim crelE crel_upd crel_nth crel_return) auto
@@ -160,25 +160,25 @@
lemma crel_mapM_nth:
assumes
- "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' xs"
- assumes "n \<le> Heap.length a h"
- shows "h = h' \<and> xs = drop (Heap.length a h - n) (get_array a h)"
+ "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' xs"
+ assumes "n \<le> Array.length a h"
+ shows "h = h' \<and> xs = drop (Array.length a h - n) (get_array a h)"
using assms
proof (induct n arbitrary: xs h h')
case 0 thus ?case
- by (auto elim!: crel_return simp add: Heap.length_def)
+ by (auto elim!: crel_return simp add: Array.length_def)
next
case (Suc n)
- 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]"
+ 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]"
by (simp add: upt_conv_Cons')
with Suc(2) obtain r where
- crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
- and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
+ crel_mapM: "crel (mapM (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
+ and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
by (auto elim!: crelE crel_nth crel_return)
- from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)"
+ from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)"
by arith
with Suc.hyps[OF crel_mapM] xs_def show ?case
- unfolding Heap.length_def
+ unfolding Array.length_def
by (auto simp add: nth_drop')
qed
@@ -186,17 +186,17 @@
assumes "crel (Array.freeze a) h h' xs"
obtains "h = h'" "xs = get_array a h"
proof
- from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
+ from assms have "crel (mapM (Array.nth a) [0..<Array.length a h]) h h' xs"
unfolding freeze_def
by (auto elim: crelE crel_length)
- hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
+ hence "crel (mapM (Array.nth a) [(Array.length a h - Array.length a h)..<Array.length a h]) h h' xs"
by simp
from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
qed
lemma crel_mapM_map_entry_remains:
- assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
- assumes "i < Heap.length a h - n"
+ assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+ assumes "i < Array.length a h - n"
shows "get_array a h ! i = get_array a h' ! i"
using assms
proof (induct n arbitrary: h h' r)
@@ -205,23 +205,23 @@
by (auto elim: crel_return)
next
case (Suc n)
- let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
- 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]"
+ let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
+ 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]"
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
- crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
+ crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
by (auto simp add: elim!: crelE crel_map_entry crel_return)
- have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
- 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"
+ have length_remains: "Array.length a ?h1 = Array.length a h" by simp
+ 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"
by simp
from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
qed
lemma crel_mapM_map_entry_changes:
- assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
- assumes "n \<le> Heap.length a h"
- assumes "i \<ge> Heap.length a h - n"
- assumes "i < Heap.length a h"
+ assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+ assumes "n \<le> Array.length a h"
+ assumes "i \<ge> Array.length a h - n"
+ assumes "i < Array.length a h"
shows "get_array a h' ! i = f (get_array a h ! i)"
using assms
proof (induct n arbitrary: h h' r)
@@ -230,54 +230,54 @@
by (auto elim!: crel_return)
next
case (Suc n)
- let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
- 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]"
+ let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
+ 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]"
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
- crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
+ crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
by (auto simp add: elim!: crelE crel_map_entry crel_return)
- have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
- from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
- from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
- from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
- 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"
+ have length_remains: "Array.length a ?h1 = Array.length a h" by simp
+ from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
+ from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
+ from Suc(4) length_remains have cases: "i = Array.length a ?h1 - Suc n \<or> i \<ge> Array.length a ?h1 - n" by arith
+ 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"
by simp
from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
- crel_mapM_map_entry_remains[OF this, of "Heap.length a h - Suc n", symmetric] less less2
+ crel_mapM_map_entry_remains[OF this, of "Array.length a h - Suc n", symmetric] less less2
show ?case
- by (auto simp add: nth_list_update_eq Heap.length_def)
+ by (auto simp add: nth_list_update_eq Array.length_def)
qed
lemma crel_mapM_map_entry_length:
- assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
- assumes "n \<le> Heap.length a h"
- shows "Heap.length a h' = Heap.length a h"
+ assumes "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
+ assumes "n \<le> Array.length a h"
+ shows "Array.length a h' = Array.length a h"
using assms
proof (induct n arbitrary: h h' r)
case 0
thus ?case by (auto elim!: crel_return)
next
case (Suc n)
- let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
- 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]"
+ let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
+ 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]"
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
- crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
+ crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
by (auto elim!: crelE crel_map_entry crel_return)
- have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
- 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"
+ have length_remains: "Array.length a ?h1 = Array.length a h" by simp
+ 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"
by simp
from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
qed
lemma crel_mapM_map_entry:
-assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Heap.length a h]) h h' r"
+assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Array.length a h]) h h' r"
shows "get_array a h' = List.map f (get_array a h)"
proof -
- 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
+ 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
from crel_mapM_map_entry_length[OF this]
crel_mapM_map_entry_changes[OF this] show ?thesis
- unfolding Heap.length_def
+ unfolding Array.length_def
by (auto intro: nth_equalityI)
qed
@@ -322,7 +322,7 @@
using assms
unfolding Ref.new_def
apply (elim crel_heap)
- unfolding Heap.ref_def
+ unfolding Ref.ref_def
apply (simp add: Let_def)
unfolding ref_present_def
apply auto
@@ -331,22 +331,22 @@
done
lemma crel_lookup:
- assumes "crel (!ref) h h' r"
- obtains "h = h'" "r = get_ref ref h"
+ assumes "crel (!r') h h' r"
+ obtains "h = h'" "r = get_ref r' h"
using assms
unfolding Ref.lookup_def
by (auto elim: crel_heap)
lemma crel_update:
- assumes "crel (ref := v) h h' r"
- obtains "h' = set_ref ref v h" "r = ()"
+ assumes "crel (r' := v) h h' r"
+ obtains "h' = set_ref r' v h" "r = ()"
using assms
unfolding Ref.update_def
by (auto elim: crel_heap)
lemma crel_change:
- assumes "crel (Ref.change f ref) h h' r"
- obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
+ assumes "crel (Ref.change f r') h h' r"
+ obtains "h' = set_ref r' (f (get_ref r' h)) h" "r = f (get_ref r' h)"
using assms
unfolding Ref.change_def Let_def
by (auto elim!: crelE crel_lookup crel_update crel_return)
@@ -431,22 +431,22 @@
subsection {* Introduction rules for array commands *}
lemma crel_lengthI:
- shows "crel (length a) h h (Heap.length a h)"
- unfolding length_def
+ shows "crel (Array.len a) h h (Array.length a h)"
+ unfolding len_def
by (rule crel_heapI') auto
(* thm crel_newI for Array.new is missing *)
lemma crel_nthI:
- assumes "i < Heap.length a h"
+ assumes "i < Array.length a h"
shows "crel (nth a i) h h ((get_array a h) ! i)"
using assms
unfolding nth_def
by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
lemma crel_updI:
- assumes "i < Heap.length a h"
- shows "crel (upd i v a) h (Heap.upd a i v h) a"
+ assumes "i < Array.length a h"
+ shows "crel (upd i v a) h (Array.change a i v h) a"
using assms
unfolding upd_def
by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
@@ -467,15 +467,15 @@
subsubsection {* Introduction rules for reference commands *}
lemma crel_lookupI:
- shows "crel (!ref) h h (get_ref ref h)"
+ shows "crel (!r) h h (get_ref r h)"
unfolding lookup_def by (auto intro!: crel_heapI')
lemma crel_updateI:
- shows "crel (ref := v) h (set_ref ref v h) ()"
+ shows "crel (r := v) h (set_ref r v h) ()"
unfolding update_def by (auto intro!: crel_heapI')
lemma crel_changeI:
- shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
+ shows "crel (Ref.change f r) h (set_ref r (f (get_ref r h)) h) (f (get_ref r h))"
unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
subsubsection {* Introduction rules for the assert command *}
@@ -587,8 +587,8 @@
subsection {* Introduction rules for array commands *}
lemma noError_length:
- shows "noError (Array.length a) h"
- unfolding length_def
+ shows "noError (Array.len a) h"
+ unfolding len_def
by (intro noError_heap)
lemma noError_new:
@@ -596,14 +596,14 @@
unfolding Array.new_def by (intro noError_heap)
lemma noError_upd:
- assumes "i < Heap.length a h"
+ assumes "i < Array.length a h"
shows "noError (Array.upd i v a) h"
using assms
unfolding upd_def
by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
lemma noError_nth:
-assumes "i < Heap.length a h"
+assumes "i < Array.length a h"
shows "noError (Array.nth a i) h"
using assms
unfolding nth_def
@@ -614,14 +614,14 @@
unfolding of_list_def by (rule noError_heap)
lemma noError_map_entry:
- assumes "i < Heap.length a h"
+ assumes "i < Array.length a h"
shows "noError (map_entry i f a) h"
using assms
unfolding map_entry_def
by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
lemma noError_swap:
- assumes "i < Heap.length a h"
+ assumes "i < Array.length a h"
shows "noError (swap i x a) h"
using assms
unfolding swap_def
@@ -644,23 +644,23 @@
noError_nth crel_nthI elim: crel_length)
lemma noError_mapM_map_entry:
- assumes "n \<le> Heap.length a h"
- shows "noError (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h"
+ assumes "n \<le> Array.length a h"
+ shows "noError (mapM (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
using assms
proof (induct n arbitrary: h)
case 0
thus ?case by (auto intro: noError_return)
next
case (Suc n)
- 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]"
+ 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]"
by (simp add: upt_conv_Cons')
- 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
+ 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
by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
qed
lemma noError_map:
shows "noError (Array.map f a) h"
-using noError_mapM_map_entry[of "Heap.length a h" a h]
+using noError_mapM_map_entry[of "Array.length a h" a h]
unfolding Array.map_def
by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
@@ -671,15 +671,15 @@
unfolding Ref.new_def by (intro noError_heap)
lemma noError_lookup:
- shows "noError (!ref) h"
+ shows "noError (!r) h"
unfolding lookup_def by (intro noError_heap)
lemma noError_update:
- shows "noError (ref := v) h"
+ shows "noError (r := v) h"
unfolding update_def by (intro noError_heap)
lemma noError_change:
- shows "noError (Ref.change f ref) h"
+ shows "noError (Ref.change f r) h"
unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
subsection {* Introduction rules for the assert command *}
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Jul 05 16:46:23 2010 +0200
@@ -27,7 +27,7 @@
= multiset_of (get_array a h)"
using assms
unfolding swap_def
- by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
+ by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
where
@@ -101,7 +101,7 @@
lemma part_length_remains:
assumes "crel (part1 a l r p) h h' rs"
- shows "Heap.length a h = Heap.length a h'"
+ shows "Array.length a h = Array.length a h'"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -207,7 +207,7 @@
by (elim crelE crel_nth crel_if crel_return) auto
from swp False have "get_array a h1 ! r \<ge> p"
unfolding swap_def
- by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
+ by (auto simp add: Array.length_def elim!: crelE crel_nth crel_upd crel_return)
with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
by fastsimp
have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
@@ -243,7 +243,7 @@
lemma partition_length_remains:
assumes "crel (partition a l r) h h' rs"
- shows "Heap.length a h = Heap.length a h'"
+ shows "Array.length a h = Array.length a h'"
proof -
from assms part_length_remains show ?thesis
unfolding partition.simps swap_def
@@ -287,14 +287,14 @@
else middle)"
unfolding partition.simps
by (elim crelE crel_return crel_nth crel_if crel_upd) simp
- from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
- (Heap.upd a rs (get_array a h1 ! r) h1)"
+ from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
+ (Array.change a rs (get_array a h1 ! r) h1)"
unfolding swap_def
by (elim crelE crel_return crel_nth crel_upd) simp
- from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
+ from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
unfolding swap_def
by (elim crelE crel_return crel_nth crel_upd) simp
- from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
+ from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
from `l < r` have "l \<le> r - 1" by simp
note middle_in_bounds = part_returns_index_in_bounds[OF part this]
@@ -304,7 +304,7 @@
with swap
have right_remains: "get_array a h ! r = get_array a h' ! rs"
unfolding swap_def
- by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
+ by (auto simp add: Array.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
from part_partitions [OF part]
show ?thesis
proof (cases "get_array a h1 ! middle \<le> ?pivot")
@@ -314,12 +314,12 @@
fix i
assume i_is_left: "l \<le> i \<and> i < rs"
with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
- have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+ have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
with part_partitions[OF part] right_remains True
have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
- unfolding Heap.upd_def Heap.length_def by simp
+ unfolding Array.change_def Array.length_def by simp
}
moreover
{
@@ -331,7 +331,7 @@
proof
assume i_is: "rs < i \<and> i \<le> r - 1"
with swap_length_remains in_bounds middle_in_bounds rs_equals
- have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+ have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is
have "get_array a h' ! rs \<le> get_array a h1 ! i"
by fastsimp
@@ -345,7 +345,7 @@
by fastsimp
with i_is True rs_equals right_remains h'_def
show ?thesis using in_bounds
- unfolding Heap.upd_def Heap.length_def
+ unfolding Array.change_def Array.length_def
by auto
qed
}
@@ -357,11 +357,11 @@
fix i
assume i_is_left: "l \<le> i \<and> i < rs"
with swap_length_remains in_bounds middle_in_bounds rs_equals
- have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+ have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is_left
have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
- unfolding Heap.upd_def by simp
+ unfolding Array.change_def by simp
}
moreover
{
@@ -372,7 +372,7 @@
proof
assume i_is: "rs < i \<and> i \<le> r - 1"
with swap_length_remains in_bounds middle_in_bounds rs_equals
- have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+ have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is
have "get_array a h' ! rs \<le> get_array a h1 ! i"
by fastsimp
@@ -381,7 +381,7 @@
assume i_is: "i = r"
from i_is False rs_equals right_remains h'_def
show ?thesis using in_bounds
- unfolding Heap.upd_def Heap.length_def
+ unfolding Array.change_def Array.length_def
by auto
qed
}
@@ -425,7 +425,7 @@
lemma length_remains:
assumes "crel (quicksort a l r) h h' rs"
- shows "Heap.length a h = Heap.length a h'"
+ shows "Array.length a h = Array.length a h'"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
@@ -482,7 +482,7 @@
lemma quicksort_sorts:
assumes "crel (quicksort a l r) h h' rs"
- assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h"
+ assumes l_r_length: "l < Array.length a h" "r < Array.length a h"
shows "sorted (subarray l (r + 1) a h')"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
@@ -524,7 +524,7 @@
from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
- unfolding Heap.length_def subarray_def by (cases p, auto)
+ unfolding Array.length_def subarray_def by (cases p, auto)
with left_subarray_remains part_conds1 pivot_unchanged
have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
by (simp, subst set_of_multiset_of[symmetric], simp)
@@ -535,7 +535,7 @@
from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
- unfolding Heap.length_def subarray_def by auto
+ unfolding Array.length_def subarray_def by auto
with right_subarray_remains part_conds2 pivot_unchanged
have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
by (simp, subst set_of_multiset_of[symmetric], simp)
@@ -556,18 +556,18 @@
lemma quicksort_is_sort:
- assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
+ assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
shows "get_array a h' = sort (get_array a h)"
proof (cases "get_array a h = []")
case True
with quicksort_is_skip[OF crel] show ?thesis
- unfolding Heap.length_def by simp
+ unfolding Array.length_def by simp
next
case False
from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
- unfolding Heap.length_def subarray_def by auto
+ unfolding Array.length_def subarray_def by auto
with length_remains[OF crel] have "sorted (get_array a h')"
- unfolding Heap.length_def by simp
+ unfolding Array.length_def by simp
with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
qed
@@ -576,7 +576,7 @@
We will now show that exceptions do not occur. *}
lemma noError_part1:
- assumes "l < Heap.length a h" "r < Heap.length a h"
+ assumes "l < Array.length a h" "r < Array.length a h"
shows "noError (part1 a l r p) h"
using assms
proof (induct a l r p arbitrary: h rule: part1.induct)
@@ -587,7 +587,7 @@
qed
lemma noError_partition:
- assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
+ assumes "l < r" "l < Array.length a h" "r < Array.length a h"
shows "noError (partition a l r) h"
using assms
unfolding partition.simps swap_def
@@ -603,7 +603,7 @@
done
lemma noError_quicksort:
- assumes "l < Heap.length a h" "r < Heap.length a h"
+ assumes "l < Array.length a h" "r < Array.length a h"
shows "noError (quicksort a l r) h"
using assms
proof (induct a l r arbitrary: h rule: quicksort.induct)
@@ -628,7 +628,7 @@
subsection {* Example *}
definition "qsort a = do
- k \<leftarrow> length a;
+ k \<leftarrow> len a;
quicksort a 0 (k - 1);
return a
done"
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon Jul 05 16:46:23 2010 +0200
@@ -37,7 +37,7 @@
else get_array a h ! k)"
using assms unfolding swap.simps
by (elim crel_elim_all)
- (auto simp: Heap.length_def)
+ (auto simp: length_def)
lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
shows "get_array a h' ! k = (if k < i then get_array a h ! k
@@ -69,7 +69,7 @@
lemma rev_length:
assumes "crel (rev a i j) h h' r"
- shows "Heap.length a h = Heap.length a h'"
+ shows "Array.length a h = Array.length a h'"
using assms
proof (induct a i j arbitrary: h h' rule: rev.induct)
case (1 a i j h h'')
@@ -93,7 +93,7 @@
qed
lemma rev2_rev': assumes "crel (rev a i j) h h' u"
- assumes "j < Heap.length a h"
+ assumes "j < Array.length a h"
shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
proof -
{
@@ -103,15 +103,15 @@
by auto
}
with assms(2) rev_length[OF assms(1)] show ?thesis
- unfolding subarray_def Heap.length_def
+ unfolding subarray_def Array.length_def
by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
qed
lemma rev2_rev:
- assumes "crel (rev a 0 (Heap.length a h - 1)) h h' u"
+ assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
shows "get_array a h' = List.rev (get_array a h)"
using rev2_rev'[OF assms] rev_length[OF assms] assms
- by (cases "Heap.length a h = 0", auto simp add: Heap.length_def
+ by (cases "Array.length a h = 0", auto simp add: Array.length_def
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all)
(drule sym[of "List.length (get_array a h)"], simp)
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Jul 05 16:46:23 2010 +0200
@@ -123,25 +123,25 @@
"array_ran a h = {e. Some e \<in> set (get_array a h)}"
-- {*FIXME*}
-lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
-unfolding array_ran_def Heap.length_def by simp
+lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
+unfolding array_ran_def Array.length_def by simp
lemma array_ran_upd_array_Some:
- assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)"
+ assumes "cl \<in> array_ran a (Array.change a i (Some b) h)"
shows "cl \<in> array_ran a h \<or> cl = b"
proof -
have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
with assms show ?thesis
- unfolding array_ran_def Heap.upd_def by fastsimp
+ unfolding array_ran_def Array.change_def by fastsimp
qed
lemma array_ran_upd_array_None:
- assumes "cl \<in> array_ran a (Heap.upd a i None h)"
+ assumes "cl \<in> array_ran a (Array.change a i None h)"
shows "cl \<in> array_ran a h"
proof -
have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
with assms show ?thesis
- unfolding array_ran_def Heap.upd_def by auto
+ unfolding array_ran_def Array.change_def by auto
qed
definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
@@ -152,7 +152,7 @@
lemma correctArray_update:
assumes "correctArray rcs a h"
assumes "correctClause rcs c" "sorted c" "distinct c"
- shows "correctArray rcs a (Heap.upd a i (Some c) h)"
+ shows "correctArray rcs a (Array.change a i (Some c) h)"
using assms
unfolding correctArray_def
by (auto dest:array_ran_upd_array_Some)
@@ -471,7 +471,7 @@
fix clj
let ?rs = "merge (remove l cli) (remove (compl l) clj)"
let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
- assume "h = h'" "Some clj = get_array a h' ! j" "j < Heap.length a h'"
+ assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length a h'"
with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj"
unfolding correctArray_def by (auto intro: array_ranI)
with clj l_not_zero correct_cli
@@ -485,7 +485,7 @@
}
{
fix v clj
- assume "Some clj = get_array a h ! j" "j < Heap.length a h"
+ assume "Some clj = get_array a h ! j" "j < Array.length a h"
with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
unfolding correctArray_def by (auto intro: array_ranI)
assume "crel (res_thm' l cli clj) h h' rs"
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Mon Jul 05 15:36:37 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Mon Jul 05 16:46:23 2010 +0200
@@ -8,65 +8,64 @@
imports Array Sublist
begin
-definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
-where
+definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
"subarray n m a h \<equiv> sublist' n m (get_array a h)"
-lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
-apply (simp add: subarray_def Heap.upd_def)
+lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
+apply (simp add: subarray_def Array.change_def)
apply (simp add: sublist'_update1)
done
-lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
-apply (simp add: subarray_def Heap.upd_def)
+lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
+apply (simp add: subarray_def Array.change_def)
apply (subst sublist'_update2)
apply fastsimp
apply simp
done
-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]"
-unfolding subarray_def Heap.upd_def
+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]"
+unfolding subarray_def Array.change_def
by (simp add: sublist'_update3)
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
by (simp add: subarray_def sublist'_Nil')
-lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]"
-by (simp add: subarray_def Heap.length_def sublist'_single)
+lemma subarray_single: "\<lbrakk> n < Array.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]"
+by (simp add: subarray_def length_def sublist'_single)
-lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
-by (simp add: subarray_def Heap.length_def length_sublist')
+lemma length_subarray: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
+by (simp add: subarray_def length_def length_sublist')
-lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
+lemma length_subarray_0: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
by (simp add: length_subarray)
-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"
-unfolding Heap.length_def subarray_def
+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"
+unfolding Array.length_def subarray_def
by (simp add: sublist'_front)
-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)]"
-unfolding Heap.length_def subarray_def
+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)]"
+unfolding Array.length_def subarray_def
by (simp add: sublist'_back)
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"
unfolding subarray_def
by (simp add: sublist'_append)
-lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
-unfolding Heap.length_def subarray_def
+lemma subarray_all: "subarray 0 (Array.length a h) a h = get_array a h"
+unfolding Array.length_def subarray_def
by (simp add: sublist'_all)
-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)"
-unfolding Heap.length_def subarray_def
+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)"
+unfolding Array.length_def subarray_def
by (simp add: nth_sublist')
-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')"
-unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
+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')"
+unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
-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))"
-unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
+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))"
+unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
-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))"
-unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
+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))"
+unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
end
\ No newline at end of file