--- a/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 17:19:08 2010 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 17:19:35 2010 +0100
@@ -10,55 +10,49 @@
subsection {* Primitives *}
-definition (*FIXME present *)
- array_present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where
- "array_present h a \<longleftrightarrow> addr_of_array a < lim h"
+definition present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where
+ "present h a \<longleftrightarrow> addr_of_array a < lim h"
-definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*)
- 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 get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where
+ "get h a = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
-definition (*FIXME set*)
- 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 set :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
+ "set a x = arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
-definition (*FIXME alloc*)
- array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
- "array xs h = (let
+definition alloc :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
+ "alloc xs h = (let
l = lim h;
r = Array l;
- h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
+ h'' = set r xs (h\<lparr>lim := l + 1\<rparr>)
in (r, h''))"
definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where
- "length h a = List.length (get_array a h)"
+ "length h a = List.length (get h a)"
definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
- "update a i x h = set_array a ((get_array a h)[i:=x]) h"
+ "update a i x h = set a ((get h a)[i:=x]) h"
-definition (*FIXME noteq*)
- noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
+definition noteq :: "'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"
subsection {* Monad operations *}
definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
- [code del]: "new n x = Heap_Monad.heap (array (replicate n x))"
+ [code del]: "new n x = Heap_Monad.heap (alloc (replicate n x))"
definition of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
- [code del]: "of_list xs = Heap_Monad.heap (array xs)"
+ [code del]: "of_list xs = Heap_Monad.heap (alloc xs)"
definition make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" where
- [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
+ [code del]: "make n f = Heap_Monad.heap (alloc (map f [0 ..< n]))"
definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
[code del]: "len a = Heap_Monad.tap (\<lambda>h. length h a)"
definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
[code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length h a)
- (\<lambda>h. (get_array a h ! i, h))"
+ (\<lambda>h. (get h a ! i, h))"
definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
[code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
@@ -66,14 +60,14 @@
definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
[code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length h a)
- (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))"
+ (\<lambda>h. (a, update a i (f (get h a ! i)) h))"
definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
[code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
- (\<lambda>h. (get_array a h ! i, update a i x h))"
+ (\<lambda>h. (get h a ! i, update a i x h))"
definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
- [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
+ [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get h a)"
subsection {* Properties *}
@@ -83,89 +77,89 @@
text {* Primitives *}
-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_sym: "a =!!= b \<Longrightarrow> b =!!= a"
+ and unequal [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
+ unfolding noteq_def by auto
-lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
- unfolding noteq_arrs_def by auto
+lemma noteq_irrefl: "r =!!= r \<Longrightarrow> False"
+ unfolding noteq_def by auto
-lemma present_new_arr: "array_present h a \<Longrightarrow> a =!!= fst (array xs h)"
- by (simp add: array_present_def noteq_arrs_def array_def Let_def)
+lemma present_alloc_noteq: "present h a \<Longrightarrow> a =!!= fst (alloc xs h)"
+ by (simp add: present_def noteq_def alloc_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 get_set_eq [simp]: "get (set r x h) r = x"
+ by (simp add: get_def set_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 get_set_neq [simp]: "r =!!= s \<Longrightarrow> get (set s x h) r = get h r"
+ by (simp add: noteq_def get_def set_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 set_same [simp]:
+ "set r x (set r y h) = set r x h"
+ by (simp add: set_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 set_set_swap:
+ "r =!!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
+ by (simp add: Let_def expand_fun_eq noteq_def set_def)
-lemma get_array_update_eq [simp]:
- "get_array a (update a i v h) = (get_array a h) [i := v]"
+lemma get_update_eq [simp]:
+ "get (update a i v h) a = (get h a) [i := v]"
by (simp add: update_def)
-lemma nth_update_array_neq_array [simp]:
- "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i"
- by (simp add: update_def noteq_arrs_def)
+lemma nth_update_neq [simp]:
+ "a =!!= b \<Longrightarrow> get (update b j v h) a ! i = get h a ! i"
+ by (simp add: update_def noteq_def)
-lemma get_arry_array_update_elem_neqIndex [simp]:
- "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i"
+lemma get_update_elem_neqIndex [simp]:
+ "i \<noteq> j \<Longrightarrow> get (update a j v h) a ! i = get h a ! i"
by simp
lemma length_update [simp]:
"length (update b i v h) = length h"
- by (simp add: update_def length_def set_array_def get_array_def expand_fun_eq)
+ by (simp add: update_def length_def set_def get_def expand_fun_eq)
-lemma update_swap_neqArray:
+lemma update_swap_neq:
"a =!!= a' \<Longrightarrow>
update a i v (update a' i' v' h)
= update a' i' v' (update a i v h)"
apply (unfold update_def)
apply simp
-apply (subst array_set_set_swap, assumption)
-apply (subst array_get_set_neq)
-apply (erule noteq_arrs_sym)
-apply (simp)
+apply (subst set_set_swap, assumption)
+apply (subst get_set_neq)
+apply (erule noteq_sym)
+apply simp
done
lemma update_swap_neqIndex:
"\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)"
- by (auto simp add: update_def array_set_set_swap list_update_swap)
+ by (auto simp add: update_def 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 get_alloc:
+ "get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
+ by (simp add: Let_def split_def alloc_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 set:
+ "set (fst (alloc ls h))
+ new_ls (snd (alloc ls h))
+ = snd (alloc new_ls h)"
+ by (simp add: Let_def split_def alloc_def)
-lemma array_present_update [simp]:
- "array_present (update b i v h) = array_present h"
- by (simp add: update_def array_present_def set_array_def get_array_def expand_fun_eq)
+lemma present_update [simp]:
+ "present (update b i v h) = present h"
+ by (simp add: update_def present_def set_def get_def expand_fun_eq)
-lemma array_present_array [simp]:
- "array_present (snd (array xs h)) (fst (array xs h))"
- by (simp add: array_present_def array_def set_array_def Let_def)
+lemma present_alloc [simp]:
+ "present (snd (alloc xs h)) (fst (alloc xs h))"
+ by (simp add: present_def alloc_def set_def Let_def)
-lemma not_array_present_array [simp]:
- "\<not> array_present h (fst (array xs h))"
- by (simp add: array_present_def array_def Let_def)
+lemma not_present_alloc [simp]:
+ "\<not> present h (fst (alloc xs h))"
+ by (simp add: present_def alloc_def Let_def)
text {* Monad operations *}
lemma execute_new [execute_simps]:
- "execute (new n x) h = Some (array (replicate n x) h)"
+ "execute (new n x) h = Some (alloc (replicate n x) h)"
by (simp add: new_def execute_simps)
lemma success_newI [success_intros]:
@@ -173,18 +167,18 @@
by (auto intro: success_intros simp add: new_def)
lemma crel_newI [crel_intros]:
- assumes "(a, h') = array (replicate n x) h"
+ assumes "(a, h') = alloc (replicate n x) h"
shows "crel (new n x) h h' a"
by (rule crelI) (simp add: assms execute_simps)
lemma crel_newE [crel_elims]:
assumes "crel (new n x) h h' r"
- obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)"
- "get_array r h' = replicate n x" "array_present h' r" "\<not> array_present h r"
- using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
+ obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)"
+ "get h' r = replicate n x" "present h' r" "\<not> present h r"
+ using assms by (rule crelE) (simp add: get_alloc execute_simps)
lemma execute_of_list [execute_simps]:
- "execute (of_list xs) h = Some (array xs h)"
+ "execute (of_list xs) h = Some (alloc xs h)"
by (simp add: of_list_def execute_simps)
lemma success_of_listI [success_intros]:
@@ -192,18 +186,18 @@
by (auto intro: success_intros simp add: of_list_def)
lemma crel_of_listI [crel_intros]:
- assumes "(a, h') = array xs h"
+ assumes "(a, h') = alloc xs h"
shows "crel (of_list xs) h h' a"
by (rule crelI) (simp add: assms execute_simps)
lemma crel_of_listE [crel_elims]:
assumes "crel (of_list xs) h h' r"
- obtains "r = fst (array xs h)" "h' = snd (array xs h)"
- "get_array r h' = xs" "array_present h' r" "\<not> array_present h r"
- using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
+ obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)"
+ "get h' r = xs" "present h' r" "\<not> present h r"
+ using assms by (rule crelE) (simp add: get_alloc execute_simps)
lemma execute_make [execute_simps]:
- "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
+ "execute (make n f) h = Some (alloc (map f [0 ..< n]) h)"
by (simp add: make_def execute_simps)
lemma success_makeI [success_intros]:
@@ -211,15 +205,15 @@
by (auto intro: success_intros simp add: make_def)
lemma crel_makeI [crel_intros]:
- assumes "(a, h') = array (map f [0 ..< n]) h"
+ assumes "(a, h') = alloc (map f [0 ..< n]) h"
shows "crel (make n f) h h' a"
by (rule crelI) (simp add: assms execute_simps)
lemma crel_makeE [crel_elims]:
assumes "crel (make n f) h h' r"
- obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)"
- "get_array r h' = map f [0 ..< n]" "array_present h' r" "\<not> array_present h r"
- using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
+ obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)"
+ "get h' r = map f [0 ..< n]" "present h' r" "\<not> present h r"
+ using assms by (rule crelE) (simp add: get_alloc execute_simps)
lemma execute_len [execute_simps]:
"execute (len a) h = Some (length h a, h)"
@@ -241,7 +235,7 @@
lemma execute_nth [execute_simps]:
"i < length h a \<Longrightarrow>
- execute (nth a i) h = Some (get_array a h ! i, h)"
+ execute (nth a i) h = Some (get h a ! i, h)"
"i \<ge> length h a \<Longrightarrow> execute (nth a i) h = None"
by (simp_all add: nth_def execute_simps)
@@ -250,13 +244,13 @@
by (auto intro: success_intros simp add: nth_def)
lemma crel_nthI [crel_intros]:
- assumes "i < length h a" "h' = h" "r = get_array a h ! i"
+ assumes "i < length h a" "h' = h" "r = get h a ! i"
shows "crel (nth a i) h h' r"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_nthE [crel_elims]:
assumes "crel (nth a i) h h' r"
- obtains "i < length h a" "r = get_array a h ! i" "h' = h"
+ obtains "i < length h a" "r = get h a ! i" "h' = h"
using assms by (rule crelE)
(erule successE, cases "i < length h a", simp_all add: execute_simps)
@@ -284,7 +278,7 @@
lemma execute_map_entry [execute_simps]:
"i < length h a \<Longrightarrow>
execute (map_entry i f a) h =
- Some (a, update a i (f (get_array a h ! i)) h)"
+ Some (a, update a i (f (get h a ! i)) h)"
"i \<ge> length h a \<Longrightarrow> execute (map_entry i f a) h = None"
by (simp_all add: map_entry_def execute_simps)
@@ -293,20 +287,20 @@
by (auto intro: success_intros simp add: map_entry_def)
lemma crel_map_entryI [crel_intros]:
- assumes "i < length h a" "h' = update a i (f (get_array a h ! i)) h" "r = a"
+ assumes "i < length h a" "h' = update a i (f (get h a ! i)) h" "r = a"
shows "crel (map_entry i f a) h h' r"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_map_entryE [crel_elims]:
assumes "crel (map_entry i f a) h h' r"
- obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length h a"
+ obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a"
using assms by (rule crelE)
(erule successE, cases "i < length h a", simp_all add: execute_simps)
lemma execute_swap [execute_simps]:
"i < length h a \<Longrightarrow>
execute (swap i x a) h =
- Some (get_array a h ! i, update a i x h)"
+ Some (get h a ! i, update a i x h)"
"i \<ge> length h a \<Longrightarrow> execute (swap i x a) h = None"
by (simp_all add: swap_def execute_simps)
@@ -315,18 +309,18 @@
by (auto intro: success_intros simp add: swap_def)
lemma crel_swapI [crel_intros]:
- assumes "i < length h a" "h' = update a i x h" "r = get_array a h ! i"
+ assumes "i < length h a" "h' = update a i x h" "r = get h a ! i"
shows "crel (swap i x a) h h' r"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_swapE [crel_elims]:
assumes "crel (swap i x a) h h' r"
- obtains "r = get_array a h ! i" "h' = update a i x h" "i < length h a"
+ obtains "r = get h a ! i" "h' = update a i x h" "i < length h a"
using assms by (rule crelE)
(erule successE, cases "i < length h a", simp_all add: execute_simps)
lemma execute_freeze [execute_simps]:
- "execute (freeze a) h = Some (get_array a h, h)"
+ "execute (freeze a) h = Some (get h a, h)"
by (simp add: freeze_def execute_simps)
lemma success_freezeI [success_intros]:
@@ -334,13 +328,13 @@
by (auto intro: success_intros simp add: freeze_def)
lemma crel_freezeI [crel_intros]:
- assumes "h' = h" "r = get_array a h"
+ assumes "h' = h" "r = get h a"
shows "crel (freeze a) h h' r"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_freezeE [crel_elims]:
assumes "crel (freeze a) h h' r"
- obtains "h' = h" "r = get_array a h"
+ obtains "h' = h" "r = get h a"
using assms by (rule crelE) (simp add: execute_simps)
lemma upd_return:
@@ -355,7 +349,7 @@
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
by (rule Heap_eqI) (simp add: map_nth execute_simps)
-hide_const (open) update new of_list make len nth upd map_entry swap freeze
+hide_const (open) present get set alloc length update noteq new of_list make len nth upd map_entry swap freeze
subsection {* Code generator setup *}
@@ -427,13 +421,13 @@
proof (rule Heap_eqI)
fix h
have *: "List.map
- (\<lambda>x. fst (the (if x < length h a
- then Some (get_array a h ! x, h) else None)))
- [0..<length h a] =
- List.map (List.nth (get_array a h)) [0..<length h a]"
+ (\<lambda>x. fst (the (if x < Array.length h a
+ then Some (Array.get h a ! x, h) else None)))
+ [0..<Array.length h a] =
+ List.map (List.nth (Array.get h a)) [0..<Array.length h a]"
by simp
- have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length h a]) h =
- Some (get_array a h, h)"
+ have "execute (Heap_Monad.fold_map (Array.nth a) [0..<Array.length h a]) h =
+ Some (Array.get h a, h)"
apply (subst execute_fold_map_unchanged_heap)
apply (simp_all add: nth_def guard_def *)
apply (simp add: length_def map_nth)
@@ -441,7 +435,7 @@
then have "execute (do {
n \<leftarrow> Array.len a;
Heap_Monad.fold_map (Array.nth a) [0..<n]
- }) h = Some (get_array a h, h)"
+ }) h = Some (Array.get h a, h)"
by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
then show "execute (Array.freeze a) h = execute (do {
n \<leftarrow> Array.len a;
--- a/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 17:19:08 2010 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 17:19:35 2010 +0100
@@ -218,49 +218,45 @@
text {* Non-interaction between imperative array and imperative references *}
-lemma get_array_set [simp]:
- "get_array a (set r v h) = get_array a h"
- by (simp add: get_array_def set_def)
-
-lemma nth_set [simp]:
- "get_array a (set r v h) ! i = get_array a h ! i"
- by simp
+lemma array_get_set [simp]:
+ "Array.get (set r v h) = Array.get h"
+ by (simp add: Array.get_def set_def expand_fun_eq)
lemma get_update [simp]:
- "get (Array.update a i v h) r = get h r"
- by (simp add: get_def Array.update_def set_array_def)
+ "get (Array.update a i v h) r = get h r"
+ by (simp add: get_def Array.update_def Array.set_def)
lemma alloc_update:
"fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
- by (simp add: Array.update_def get_array_def set_array_def alloc_def Let_def)
+ by (simp add: Array.update_def Array.get_def Array.set_def alloc_def Let_def)
lemma update_set_swap:
"Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
- by (simp add: Array.update_def get_array_def set_array_def set_def)
+ by (simp add: Array.update_def Array.get_def Array.set_def set_def)
lemma length_alloc [simp]:
"Array.length (snd (alloc v h)) a = Array.length h a"
- by (simp add: Array.length_def get_array_def alloc_def set_def Let_def)
+ by (simp add: Array.length_def Array.get_def alloc_def set_def Let_def)
-lemma get_array_alloc [simp]:
- "get_array a (snd (alloc v h)) = get_array a h"
- by (simp add: get_array_def alloc_def set_def Let_def)
+lemma array_get_alloc [simp]:
+ "Array.get (snd (alloc v h)) = Array.get h"
+ by (simp add: Array.get_def alloc_def set_def Let_def expand_fun_eq)
lemma present_update [simp]:
"present (Array.update a i v h) = present h"
- by (simp add: Array.update_def set_array_def expand_fun_eq present_def)
+ by (simp add: Array.update_def Array.set_def expand_fun_eq present_def)
lemma array_present_set [simp]:
- "array_present (set r v h) = array_present h"
- by (simp add: array_present_def set_def expand_fun_eq)
+ "Array.present (set r v h) = Array.present h"
+ by (simp add: Array.present_def set_def expand_fun_eq)
lemma array_present_alloc [simp]:
- "array_present h a \<Longrightarrow> array_present (snd (alloc v h)) a"
- by (simp add: array_present_def alloc_def Let_def)
+ "Array.present h a \<Longrightarrow> Array.present (snd (alloc v h)) a"
+ by (simp add: Array.present_def alloc_def Let_def)
lemma set_array_set_swap:
- "set_array a xs (set r x' h) = set r x' (set_array a xs h)"
- by (simp add: set_array_def set_def)
+ "Array.set a xs (set r x' h) = set r x' (Array.set a xs h)"
+ by (simp add: Array.set_def set_def)
hide_const (open) present get set alloc noteq lookup update change
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 17:19:08 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 17:19:35 2010 +0100
@@ -23,15 +23,15 @@
lemma crel_swapI [crel_intros]:
assumes "i < Array.length h a" "j < Array.length h a"
- "x = get_array a h ! i" "y = get_array a h ! j"
+ "x = Array.get h a ! i" "y = Array.get h a ! j"
"h' = Array.update a j x (Array.update a i y h)"
shows "crel (swap a i j) h h' r"
unfolding swap_def using assms by (auto intro!: crel_intros)
lemma swap_permutes:
assumes "crel (swap a i j) h h' rs"
- shows "multiset_of (get_array a h')
- = multiset_of (get_array a h)"
+ shows "multiset_of (Array.get h' a)
+ = multiset_of (Array.get h a)"
using assms
unfolding swap_def
by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
@@ -55,8 +55,8 @@
lemma part_permutes:
assumes "crel (part1 a l r p) h h' rs"
- shows "multiset_of (get_array a h')
- = multiset_of (get_array a h)"
+ shows "multiset_of (Array.get h' a)
+ = multiset_of (Array.get h a)"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -82,7 +82,7 @@
next
case False (* recursive case *)
note rec_condition = this
- let ?v = "get_array a h ! l"
+ let ?v = "Array.get h a ! l"
show ?thesis
proof (cases "?v \<le> p")
case True
@@ -130,7 +130,7 @@
lemma part_outer_remains:
assumes "crel (part1 a l r p) h h' rs"
- shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+ shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -145,7 +145,7 @@
next
case False (* recursive case *)
note rec_condition = this
- let ?v = "get_array a h ! l"
+ let ?v = "Array.get h a ! l"
show ?thesis
proof (cases "?v \<le> p")
case True
@@ -163,7 +163,7 @@
unfolding part1.simps[of a l r p]
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
from swp rec_condition have
- "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
+ "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
unfolding swap_def
by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
@@ -174,8 +174,8 @@
lemma part_partitions:
assumes "crel (part1 a l r p) h h' rs"
- shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
- \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
+ shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> p)
+ \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -192,7 +192,7 @@
next
case False (* recursive case *)
note lr = this
- let ?v = "get_array a h ! l"
+ let ?v = "Array.get h a ! l"
show ?thesis
proof (cases "?v \<le> p")
case True
@@ -200,7 +200,7 @@
have rec1: "crel (part1 a (l + 1) r p) h h' rs"
unfolding part1.simps[of a l r p]
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
- from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
+ from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
by fastsimp
have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
with 1(1)[OF False True rec1] a_l show ?thesis
@@ -212,10 +212,10 @@
and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
unfolding part1.simps[of a l r p]
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
- from swp False have "get_array a h1 ! r \<ge> p"
+ from swp False have "Array.get h1 a ! r \<ge> p"
unfolding swap_def
by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
- with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
+ with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
by fastsimp
have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
with 1(2)[OF lr False rec2] a_r show ?thesis
@@ -240,8 +240,8 @@
lemma partition_permutes:
assumes "crel (partition a l r) h h' rs"
- shows "multiset_of (get_array a h')
- = multiset_of (get_array a h)"
+ shows "multiset_of (Array.get h' a)
+ = multiset_of (Array.get h a)"
proof -
from assms part_permutes swap_permutes show ?thesis
unfolding partition.simps
@@ -260,7 +260,7 @@
lemma partition_outer_remains:
assumes "crel (partition a l r) h h' rs"
assumes "l < r"
- shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+ shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
proof -
from assms part_outer_remains part_returns_index_in_bounds show ?thesis
unfolding partition.simps swap_def
@@ -273,10 +273,10 @@
shows "l \<le> rs \<and> rs \<le> r"
proof -
from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
- and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
+ and rs_equals: "rs = (if Array.get h'' a ! middle \<le> Array.get h a ! r then middle + 1
else middle)"
unfolding partition.simps
- by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
+ by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
from `l < r` have "l \<le> r - 1" by arith
from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
qed
@@ -284,18 +284,18 @@
lemma partition_partitions:
assumes crel: "crel (partition a l r) h h' rs"
assumes "l < r"
- shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
- (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
+ shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> Array.get h' a ! rs) \<and>
+ (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)"
proof -
- let ?pivot = "get_array a h ! r"
+ let ?pivot = "Array.get h a ! r"
from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
and swap: "crel (swap a rs r) h1 h' ()"
- and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
+ and rs_equals: "rs = (if Array.get h1 a ! middle \<le> ?pivot then middle + 1
else middle)"
unfolding partition.simps
by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
- from swap have h'_def: "h' = Array.update a r (get_array a h1 ! rs)
- (Array.update a rs (get_array a h1 ! r) h1)"
+ from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs)
+ (Array.update a rs (Array.get h1 a ! r) h1)"
unfolding swap_def
by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
@@ -306,15 +306,15 @@
from `l < r` have "l \<le> r - 1" by simp
note middle_in_bounds = part_returns_index_in_bounds[OF part this]
from part_outer_remains[OF part] `l < r`
- have "get_array a h ! r = get_array a h1 ! r"
+ have "Array.get h a ! r = Array.get h1 a ! r"
by fastsimp
with swap
- have right_remains: "get_array a h ! r = get_array a h' ! rs"
+ have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
unfolding swap_def
by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
from part_partitions [OF part]
show ?thesis
- proof (cases "get_array a h1 ! middle \<le> ?pivot")
+ proof (cases "Array.get h1 a ! middle \<le> ?pivot")
case True
with rs_equals have rs_equals: "rs = middle + 1" by simp
{
@@ -324,8 +324,8 @@
have i_props: "i < Array.length h' a" "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"
+ have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp
+ with i_props h'_def in_bounds have "Array.get h' a ! i \<le> Array.get h' a ! rs"
unfolding Array.update_def Array.length_def by simp
}
moreover
@@ -334,13 +334,13 @@
assume "rs < i \<and> i \<le> r"
hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
- hence "get_array a h' ! rs \<le> get_array a h' ! i"
+ hence "Array.get h' a ! rs \<le> Array.get h' a ! i"
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 < Array.length h' a" "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"
+ have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
by fastsimp
with i_props h'_def show ?thesis by fastsimp
next
@@ -348,7 +348,7 @@
with rs_equals have "Suc middle \<noteq> r" by arith
with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
with part_partitions[OF part] right_remains
- have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
+ have "Array.get h' a ! rs \<le> Array.get h1 a ! (Suc middle)"
by fastsimp
with i_is True rs_equals right_remains h'_def
show ?thesis using in_bounds
@@ -366,8 +366,8 @@
with swap_length_remains in_bounds middle_in_bounds rs_equals
have i_props: "i < Array.length h' a" "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"
+ have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp
+ with i_props h'_def have "Array.get h' a ! i \<le> Array.get h' a ! rs"
unfolding Array.update_def by simp
}
moreover
@@ -375,13 +375,13 @@
fix i
assume "rs < i \<and> i \<le> r"
hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
- hence "get_array a h' ! rs \<le> get_array a h' ! i"
+ hence "Array.get h' a ! rs \<le> Array.get h' a ! i"
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 < Array.length h' a" "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"
+ have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
by fastsimp
with i_props h'_def show ?thesis by fastsimp
next
@@ -420,8 +420,8 @@
lemma quicksort_permutes:
assumes "crel (quicksort a l r) h h' rs"
- shows "multiset_of (get_array a h')
- = multiset_of (get_array a h)"
+ shows "multiset_of (Array.get h' a)
+ = multiset_of (Array.get h a)"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
@@ -443,7 +443,7 @@
lemma quicksort_outer_remains:
assumes "crel (quicksort a l r) h h' rs"
- shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+ shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
@@ -465,14 +465,14 @@
assume pivot: "l \<le> p \<and> p \<le> r"
assume i_outer: "i < l \<or> r < i"
from partition_outer_remains [OF part True] i_outer
- have "get_array a h !i = get_array a h1 ! i" by fastsimp
+ have "Array.get h a !i = Array.get h1 a ! i" by fastsimp
moreover
with 1(1) [OF True pivot qs1] pivot i_outer
- have "get_array a h1 ! i = get_array a h2 ! i" by auto
+ have "Array.get h1 a ! i = Array.get h2 a ! i" by auto
moreover
with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
- have "get_array a h2 ! i = get_array a h' ! i" by auto
- ultimately have "get_array a h ! i= get_array a h' ! i" by simp
+ have "Array.get h2 a ! i = Array.get h' a ! i" by auto
+ ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp
}
with cr show ?thesis
unfolding quicksort.simps [of a l r]
@@ -512,7 +512,7 @@
have pivot: "l\<le> p \<and> p \<le> r" .
note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
- have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
+ have pivot_unchanged: "Array.get h1 a ! p = Array.get h' a ! p" by (cases p, auto)
(*-- First of all, by induction hypothesis both sublists are sorted. *)
from 1(1)[OF True pivot qs1] length_remains pivot 1(5)
have IH1: "sorted (subarray l p a h2)" by (cases p, auto simp add: subarray_Nil)
@@ -525,35 +525,35 @@
by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
(* -- Secondly, both sublists remain partitioned. *)
from partition_partitions[OF part True]
- have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
- and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
+ have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> Array.get h1 a ! p "
+ and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j"
by (auto simp add: all_in_set_subarray_conv)
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"]
+ length_remains 1(5) pivot multiset_of_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
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"
+ have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
by (simp, subst set_of_multiset_of[symmetric], simp)
(* -- These steps are the analogous for the right sublist \<dots> *)
from quicksort_outer_remains [OF qs1] length_remains
have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
by (auto simp add: subarray_eq_samelength_iff)
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'"]
+ length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
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"
+ have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
by (simp, subst set_of_multiset_of[symmetric], simp)
(* -- Thirdly and finally, we show that the array is sorted
following from the facts above. *)
- from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [get_array a h' ! p] @ subarray (p + 1) (r + 1) a h'"
+ from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'"
by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
unfolding subarray_def
apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
- by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
+ by (auto simp add: set_sublist' dest: le_trans [of _ "Array.get h' a ! p"])
}
with True cr show ?thesis
unfolding quicksort.simps [of a l r]
@@ -564,16 +564,16 @@
lemma quicksort_is_sort:
assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
- shows "get_array a h' = sort (get_array a h)"
-proof (cases "get_array a h = []")
+ shows "Array.get h' a = sort (Array.get h a)"
+proof (cases "Array.get h a = []")
case True
with quicksort_is_skip[OF crel] show ?thesis
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'))"
+ from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
unfolding Array.length_def subarray_def by auto
- with length_remains[OF crel] have "sorted (get_array a h')"
+ with length_remains[OF crel] have "sorted (Array.get h' a)"
unfolding Array.length_def by simp
with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
qed
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 17:19:08 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 17:19:35 2010 +0100
@@ -27,17 +27,17 @@
declare swap.simps [simp del] rev.simps [simp del]
lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
- shows "get_array a h' ! k = (if k = i then get_array a h ! j
- else if k = j then get_array a h ! i
- else get_array a h ! k)"
+ shows "Array.get h' a ! k = (if k = i then Array.get h a ! j
+ else if k = j then Array.get h a ! i
+ else Array.get h a ! k)"
using assms unfolding swap.simps
by (elim crel_elims)
(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
- else if j < k then get_array a h ! k
- else get_array a h ! (j - (k - i)))" (is "?P a i j h h'")
+ shows "Array.get h' a ! k = (if k < i then Array.get h a ! k
+ else if j < k then Array.get h a ! k
+ else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'")
using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
case (1 a i j h h'')
thus ?case
@@ -94,7 +94,7 @@
{
fix k
assume "k < Suc j - i"
- with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - k)"
+ with rev_pointwise[OF assms(1)] have "Array.get h' a ! (i + k) = Array.get h a ! (j - k)"
by auto
}
with assms(2) rev_length[OF assms(1)] show ?thesis
@@ -104,10 +104,10 @@
lemma rev2_rev:
assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
- shows "get_array a h' = List.rev (get_array a h)"
+ shows "Array.get h' a = List.rev (Array.get h a)"
using rev2_rev'[OF assms] rev_length[OF assms] assms
by (cases "Array.length h a = 0", auto simp add: Array.length_def
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
- (drule sym[of "List.length (get_array a h)"], simp)
+ (drule sym[of "List.length (Array.get h a)"], simp)
end
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 17:19:08 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 17:19:35 2010 +0100
@@ -120,17 +120,17 @@
definition
array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
- "array_ran a h = {e. Some e \<in> set (get_array a h)}"
+ "array_ran a h = {e. Some e \<in> set (Array.get h a)}"
-- {*FIXME*}
-lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length h a \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
+lemma array_ranI: "\<lbrakk> Some b = Array.get h a ! i; i < Array.length h a \<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 (Array.update 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)
+ have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
unfolding array_ran_def Array.update_def by fastsimp
qed
@@ -139,7 +139,7 @@
assumes "cl \<in> array_ran a (Array.update 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)
+ have "set (Array.get h a[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
unfolding array_ran_def Array.update_def by auto
qed
@@ -477,7 +477,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 < Array.length h' a"
+ assume "h = h'" "Some clj = Array.get h' a ! j" "j < Array.length h' a"
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
@@ -491,7 +491,7 @@
}
{
fix v clj
- assume "Some clj = get_array a h ! j" "j < Array.length h a"
+ assume "Some clj = Array.get h a ! j" "j < Array.length h a"
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 Tue Jul 13 17:19:08 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Tue Jul 13 17:19:35 2010 +0100
@@ -9,7 +9,7 @@
begin
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)"
+ "subarray n m a h \<equiv> sublist' n m (Array.get h a)"
lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
apply (simp add: subarray_def Array.update_def)
@@ -30,7 +30,7 @@
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
by (simp add: subarray_def sublist'_Nil')
-lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]"
+lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [Array.get h a ! n]"
by (simp add: subarray_def length_def sublist'_single)
lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
@@ -39,11 +39,11 @@
lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
by (simp add: length_subarray)
-lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length h a; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
+lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length h a; i < j \<rbrakk> \<Longrightarrow> (Array.get h a ! 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> Array.length h a\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
+lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length h a\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [Array.get h a ! (j - 1)]"
unfolding Array.length_def subarray_def
by (simp add: sublist'_back)
@@ -51,21 +51,21 @@
unfolding subarray_def
by (simp add: sublist'_append)
-lemma subarray_all: "subarray 0 (Array.length h a) a h = get_array a h"
+lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a"
unfolding Array.length_def subarray_def
by (simp add: sublist'_all)
-lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length h a \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
+lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length h a \<rbrakk> \<Longrightarrow> subarray i j a h ! k = Array.get h a ! (i + k)"
unfolding Array.length_def subarray_def
by (simp add: nth_sublist')
-lemma subarray_eq_samelength_iff: "Array.length h a = Array.length h' a \<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')"
+lemma subarray_eq_samelength_iff: "Array.length h a = Array.length h' a \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> Array.get h a ! i' = Array.get h' a ! 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 < Array.length h a \<longrightarrow> P (get_array a h ! k))"
+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 h a \<longrightarrow> P (Array.get h a ! 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 < Array.length h a \<longrightarrow> P (get_array a h ! k))"
+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 h a \<longrightarrow> P (Array.get h a ! k))"
unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
end
\ No newline at end of file
--- a/src/HOL/Product_Type.thy Tue Jul 13 17:19:08 2010 +0100
+++ b/src/HOL/Product_Type.thy Tue Jul 13 17:19:35 2010 +0100
@@ -289,7 +289,7 @@
fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
*}
attach (test) {*
-fun term_of_prod aG aT bG bT i =
+fun gen_prod aG aT bG bT i =
let
val (x, t) = aG i;
val (y, u) = bG i