--- a/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 16:12:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 16:21:49 2010 +0200
@@ -13,9 +13,8 @@
definition present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where
"present h a \<longleftrightarrow> addr_of_array a < lim h"
-definition (*FIXME get *)
- get_array :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where
- "get_array h a = 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 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))))"
@@ -28,10 +27,10 @@
in (r, h''))"
definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where
- "length h a = List.length (get_array h a)"
+ "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 a ((get_array h a)[i:=x]) h"
+ "update a i x h = set a ((get h a)[i:=x]) h"
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"
@@ -53,7 +52,7 @@
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 h a ! 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)
@@ -61,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 h a ! 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 h a ! 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 h a)"
+ [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get h a)"
subsection {* Properties *}
@@ -88,11 +87,11 @@
lemma present_new_arr: "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 (set r x h) r = x"
- by (simp add: get_array_def set_def o_def)
+lemma array_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 (set s x h) r = get_array h r"
- by (simp add: noteq_def get_array_def set_def)
+lemma array_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 r x (set r y h) = set r x h"
@@ -102,21 +101,21 @@
"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 (update a i v h) a = (get_array h a) [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 (update b j v h) a ! i = get_array h a ! i"
+ "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 (update a j v h) a ! i = get_array h a ! i"
+ "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_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:
"a =!!= a' \<Longrightarrow>
@@ -134,8 +133,8 @@
"\<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)
-lemma get_array_init_array_list:
- "get_array (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
+lemma get_init_array_list:
+ "get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
by (simp add: Let_def split_def alloc_def)
lemma set_array:
@@ -146,7 +145,7 @@
lemma array_present_update [simp]:
"present (update b i v h) = present h"
- by (simp add: update_def present_def set_def get_array_def expand_fun_eq)
+ by (simp add: update_def present_def set_def get_def expand_fun_eq)
lemma array_present_array [simp]:
"present (snd (alloc xs h)) (fst (alloc xs h))"
@@ -175,8 +174,8 @@
lemma crel_newE [crel_elims]:
assumes "crel (new n x) h h' r"
obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)"
- "get_array h' r = replicate n x" "present h' r" "\<not> present h r"
- using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
+ "get h' r = replicate n x" "present h' r" "\<not> present h r"
+ using assms by (rule crelE) (simp add: get_init_array_list execute_simps)
lemma execute_of_list [execute_simps]:
"execute (of_list xs) h = Some (alloc xs h)"
@@ -194,8 +193,8 @@
lemma crel_of_listE [crel_elims]:
assumes "crel (of_list xs) h h' r"
obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)"
- "get_array h' r = xs" "present h' r" "\<not> present h r"
- using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
+ "get h' r = xs" "present h' r" "\<not> present h r"
+ using assms by (rule crelE) (simp add: get_init_array_list execute_simps)
lemma execute_make [execute_simps]:
"execute (make n f) h = Some (alloc (map f [0 ..< n]) h)"
@@ -213,8 +212,8 @@
lemma crel_makeE [crel_elims]:
assumes "crel (make n f) h h' r"
obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)"
- "get_array h' r = map f [0 ..< n]" "present h' r" "\<not> present h r"
- using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
+ "get h' r = map f [0 ..< n]" "present h' r" "\<not> present h r"
+ using assms by (rule crelE) (simp add: get_init_array_list execute_simps)
lemma execute_len [execute_simps]:
"execute (len a) h = Some (length h a, h)"
@@ -236,7 +235,7 @@
lemma execute_nth [execute_simps]:
"i < length h a \<Longrightarrow>
- execute (nth a i) h = Some (get_array h a ! 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)
@@ -245,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 h a ! 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 h a ! 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)
@@ -279,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 h a ! 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)
@@ -288,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 h a ! 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 h a ! 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 h a ! 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)
@@ -310,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 h a ! 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 h a ! 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 h a, h)"
+ "execute (freeze a) h = Some (get h a, h)"
by (simp add: freeze_def execute_simps)
lemma success_freezeI [success_intros]:
@@ -329,13 +328,13 @@
by (auto intro: success_intros simp add: freeze_def)
lemma crel_freezeI [crel_intros]:
- assumes "h' = h" "r = get_array h a"
+ 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 h a"
+ obtains "h' = h" "r = get h a"
using assms by (rule crelE) (simp add: execute_simps)
lemma upd_return:
@@ -350,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) present (*get*) set alloc length update noteq 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 *}
@@ -423,12 +422,12 @@
fix h
have *: "List.map
(\<lambda>x. fst (the (if x < Array.length h a
- then Some (get_array h a ! x, h) else None)))
+ then Some (Array.get h a ! x, h) else None)))
[0..<Array.length h a] =
- List.map (List.nth (get_array h a)) [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..<Array.length h a]) h =
- Some (get_array 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)
@@ -436,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 h a, 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 16:12:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 16:21:49 2010 +0200
@@ -218,9 +218,9 @@
text {* Non-interaction between imperative array and imperative references *}
-lemma get_array_set [simp]:
- "get_array (set r v h) = get_array h"
- by (simp add: get_array_def set_def expand_fun_eq)
+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"
@@ -228,19 +228,19 @@
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 Array.set_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 Array.set_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 (snd (alloc v h)) = get_array h"
- by (simp add: get_array_def alloc_def set_def Let_def expand_fun_eq)
+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"
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 16:12:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 16:21:49 2010 +0200
@@ -23,15 +23,15 @@
lemma crel_swapI [crel_intros]:
assumes "i < Array.length h a" "j < Array.length h a"
- "x = get_array h a ! i" "y = get_array h a ! 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 h' a)
- = multiset_of (get_array h a)"
+ 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 h' a)
- = multiset_of (get_array h a)"
+ 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 h a ! 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 h (a::nat array) ! i = get_array h' a ! 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 h a ! 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 h a ! i = get_array h1 a ! 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 h' (a::nat array) ! i \<le> p)
- \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array h' a ! 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 h a ! 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 h' a ! 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 h1 a ! 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 h' a ! 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 h' a)
- = multiset_of (get_array h a)"
+ 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 h (a::nat array) ! i = get_array h' a ! 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,7 +273,7 @@
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 h'' a ! middle \<le> get_array h a ! 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
@@ -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 h' (a::nat array) ! i \<le> get_array h' a ! rs) \<and>
- (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array h' a ! rs \<le> get_array h' a ! 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 h a ! 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 h1 a ! 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 h1 a ! rs)
- (Array.update a rs (get_array h1 a ! 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 h a ! r = get_array h1 a ! r"
+ have "Array.get h a ! r = Array.get h1 a ! r"
by fastsimp
with swap
- have right_remains: "get_array h a ! r = get_array h' a ! 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 h1 a ! 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 h1 a ! i \<le> get_array h' a ! rs" by fastsimp
- with i_props h'_def in_bounds have "get_array h' a ! i \<le> get_array h' a ! 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 h' a ! rs \<le> get_array h' a ! 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 h' a ! rs \<le> get_array h1 a ! 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 h' a ! rs \<le> get_array h1 a ! (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 h1 a ! i \<le> get_array h' a ! rs" by fastsimp
- with i_props h'_def have "get_array h' a ! i \<le> get_array h' a ! 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 h' a ! rs \<le> get_array h' a ! 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 h' a ! rs \<le> get_array h1 a ! 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 h' a)
- = multiset_of (get_array h a)"
+ 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 h (a::nat array) ! i = get_array h' a ! 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 h a !i = get_array h1 a ! 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 h1 a ! i = get_array h2 a ! 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 h2 a ! i = get_array h' a ! i" by auto
- ultimately have "get_array h a ! i= get_array h' a ! 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 h1 a ! p = get_array h' a ! 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 h1 a ! p "
- and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array h1 a ! 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 h1 a" "get_array h2 a"]
+ 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 h' a ! 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 h2 a" "get_array h' a"]
+ 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 h' a ! 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 h' a ! 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 h' a ! 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 h' a = sort (get_array h a)"
-proof (cases "get_array h a = []")
+ 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 h a)) (get_array h' a))"
+ 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 h' a)"
+ 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 16:12:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 16:21:49 2010 +0200
@@ -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 h' a ! k = (if k = i then get_array h a ! j
- else if k = j then get_array h a ! i
- else get_array h a ! 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 h' a ! k = (if k < i then get_array h a ! k
- else if j < k then get_array h a ! k
- else get_array h a ! (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 h' a ! (i + k) = get_array h a ! (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 h' a = List.rev (get_array h a)"
+ 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 h a)"], simp)
+ (drule sym[of "List.length (Array.get h a)"], simp)
end
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 16:12:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 16:21:49 2010 +0200
@@ -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 h a)}"
+ "array_ran a h = {e. Some e \<in> set (Array.get h a)}"
-- {*FIXME*}
-lemma array_ranI: "\<lbrakk> Some b = get_array h a ! 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 h a[i := Some b]) \<subseteq> insert (Some b) (set (get_array h a))" 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 h a[i := None]) \<subseteq> insert None (set (get_array h a))" 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 h' a ! 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 h a ! 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 16:12:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Tue Jul 13 16:21:49 2010 +0200
@@ -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 h a)"
+ "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 h a ! 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 h a ! 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 h a ! (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 h a"
+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 h a ! (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 h a ! i' = get_array h' a ! 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 h a ! 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 h a ! 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