# HG changeset patch
# User paulson
# Date 1279037975 -3600
# Node ID 4270d4b0284ab9d99a60334bad408877bc2f79e3
# Parent  e604e5f9bb6aba135b5ce9f5f33b1cdc0802ef52# Parent  6c87cdad912dd56fd1109b6e94a63585a48b6812
merged

diff -r 6c87cdad912d -r 4270d4b0284a src/HOL/Imperative_HOL/Array.thy
--- 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;
diff -r 6c87cdad912d -r 4270d4b0284a src/HOL/Imperative_HOL/Ref.thy
--- 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
 
diff -r 6c87cdad912d -r 4270d4b0284a src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- 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
diff -r 6c87cdad912d -r 4270d4b0284a src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- 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
diff -r 6c87cdad912d -r 4270d4b0284a src/HOL/Imperative_HOL/ex/SatChecker.thy
--- 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"
diff -r 6c87cdad912d -r 4270d4b0284a src/HOL/Imperative_HOL/ex/Subarray.thy
--- 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
diff -r 6c87cdad912d -r 4270d4b0284a src/HOL/Product_Type.thy
--- 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