canonical argument order for get
authorhaftmann
Tue Jul 13 16:12:40 2010 +0200 (2010-07-13 ago)
changeset 378050f797d586ce5
parent 37804 0145e59c1f6c
child 37806 a7679be14442
canonical argument order for get
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
src/HOL/Imperative_HOL/ex/Subarray.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 16:00:56 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 16:12:40 2010 +0200
     1.3 @@ -13,9 +13,9 @@
     1.4  definition present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where
     1.5    "present h a \<longleftrightarrow> addr_of_array a < lim h"
     1.6  
     1.7 -definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*)
     1.8 -  get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
     1.9 -  "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
    1.10 +definition (*FIXME get *)
    1.11 +  get_array :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where
    1.12 +  "get_array h a = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
    1.13  
    1.14  definition set :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
    1.15    "set a x = arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
    1.16 @@ -28,10 +28,10 @@
    1.17     in (r, h''))"
    1.18  
    1.19  definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where
    1.20 -  "length h a = List.length (get_array a h)"
    1.21 +  "length h a = List.length (get_array h a)"
    1.22    
    1.23  definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
    1.24 -  "update a i x h = set a ((get_array a h)[i:=x]) h"
    1.25 +  "update a i x h = set a ((get_array h a)[i:=x]) h"
    1.26  
    1.27  definition noteq :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
    1.28    "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
    1.29 @@ -53,7 +53,7 @@
    1.30  
    1.31  definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
    1.32    [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length h a)
    1.33 -    (\<lambda>h. (get_array a h ! i, h))"
    1.34 +    (\<lambda>h. (get_array h a ! i, h))"
    1.35  
    1.36  definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
    1.37    [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
    1.38 @@ -61,14 +61,14 @@
    1.39  
    1.40  definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
    1.41    [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length h a)
    1.42 -    (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))"
    1.43 +    (\<lambda>h. (a, update a i (f (get_array h a ! i)) h))"
    1.44  
    1.45  definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
    1.46    [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
    1.47 -    (\<lambda>h. (get_array a h ! i, update a i x h))"
    1.48 +    (\<lambda>h. (get_array h a ! i, update a i x h))"
    1.49  
    1.50  definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
    1.51 -  [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
    1.52 +  [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array h a)"
    1.53  
    1.54  
    1.55  subsection {* Properties *}
    1.56 @@ -88,10 +88,10 @@
    1.57  lemma present_new_arr: "present h a \<Longrightarrow> a =!!= fst (alloc xs h)"
    1.58    by (simp add: present_def noteq_def alloc_def Let_def)
    1.59  
    1.60 -lemma array_get_set_eq [simp]: "get_array r (set r x h) = x"
    1.61 +lemma array_get_set_eq [simp]: "get_array (set r x h) r = x"
    1.62    by (simp add: get_array_def set_def o_def)
    1.63  
    1.64 -lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set s x h) = get_array r h"
    1.65 +lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array (set s x h) r = get_array h r"
    1.66    by (simp add: noteq_def get_array_def set_def)
    1.67  
    1.68  lemma set_array_same [simp]:
    1.69 @@ -103,15 +103,15 @@
    1.70    by (simp add: Let_def expand_fun_eq noteq_def set_def)
    1.71  
    1.72  lemma get_array_update_eq [simp]:
    1.73 -  "get_array a (update a i v h) = (get_array a h) [i := v]"
    1.74 +  "get_array (update a i v h) a = (get_array h a) [i := v]"
    1.75    by (simp add: update_def)
    1.76  
    1.77  lemma nth_update_array_neq_array [simp]:
    1.78 -  "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i"
    1.79 +  "a =!!= b \<Longrightarrow> get_array (update b j v h) a ! i = get_array h a ! i"
    1.80    by (simp add: update_def noteq_def)
    1.81  
    1.82  lemma get_arry_array_update_elem_neqIndex [simp]:
    1.83 -  "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i"
    1.84 +  "i \<noteq> j \<Longrightarrow> get_array (update a j v h) a ! i = get_array h a ! i"
    1.85    by simp
    1.86  
    1.87  lemma length_update [simp]: 
    1.88 @@ -135,7 +135,7 @@
    1.89    by (auto simp add: update_def array_set_set_swap list_update_swap)
    1.90  
    1.91  lemma get_array_init_array_list:
    1.92 -  "get_array (fst (alloc ls h)) (snd (alloc ls' h)) = ls'"
    1.93 +  "get_array (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
    1.94    by (simp add: Let_def split_def alloc_def)
    1.95  
    1.96  lemma set_array:
    1.97 @@ -175,7 +175,7 @@
    1.98  lemma crel_newE [crel_elims]:
    1.99    assumes "crel (new n x) h h' r"
   1.100    obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" 
   1.101 -    "get_array r h' = replicate n x" "present h' r" "\<not> present h r"
   1.102 +    "get_array h' r = replicate n x" "present h' r" "\<not> present h r"
   1.103    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
   1.104  
   1.105  lemma execute_of_list [execute_simps]:
   1.106 @@ -194,7 +194,7 @@
   1.107  lemma crel_of_listE [crel_elims]:
   1.108    assumes "crel (of_list xs) h h' r"
   1.109    obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" 
   1.110 -    "get_array r h' = xs" "present h' r" "\<not> present h r"
   1.111 +    "get_array h' r = xs" "present h' r" "\<not> present h r"
   1.112    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
   1.113  
   1.114  lemma execute_make [execute_simps]:
   1.115 @@ -213,7 +213,7 @@
   1.116  lemma crel_makeE [crel_elims]:
   1.117    assumes "crel (make n f) h h' r"
   1.118    obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" 
   1.119 -    "get_array r h' = map f [0 ..< n]" "present h' r" "\<not> present h r"
   1.120 +    "get_array h' r = map f [0 ..< n]" "present h' r" "\<not> present h r"
   1.121    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
   1.122  
   1.123  lemma execute_len [execute_simps]:
   1.124 @@ -236,7 +236,7 @@
   1.125  
   1.126  lemma execute_nth [execute_simps]:
   1.127    "i < length h a \<Longrightarrow>
   1.128 -    execute (nth a i) h = Some (get_array a h ! i, h)"
   1.129 +    execute (nth a i) h = Some (get_array h a ! i, h)"
   1.130    "i \<ge> length h a \<Longrightarrow> execute (nth a i) h = None"
   1.131    by (simp_all add: nth_def execute_simps)
   1.132  
   1.133 @@ -245,13 +245,13 @@
   1.134    by (auto intro: success_intros simp add: nth_def)
   1.135  
   1.136  lemma crel_nthI [crel_intros]:
   1.137 -  assumes "i < length h a" "h' = h" "r = get_array a h ! i"
   1.138 +  assumes "i < length h a" "h' = h" "r = get_array h a ! i"
   1.139    shows "crel (nth a i) h h' r"
   1.140    by (rule crelI) (insert assms, simp add: execute_simps)
   1.141  
   1.142  lemma crel_nthE [crel_elims]:
   1.143    assumes "crel (nth a i) h h' r"
   1.144 -  obtains "i < length h a" "r = get_array a h ! i" "h' = h"
   1.145 +  obtains "i < length h a" "r = get_array h a ! i" "h' = h"
   1.146    using assms by (rule crelE)
   1.147      (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.148  
   1.149 @@ -279,7 +279,7 @@
   1.150  lemma execute_map_entry [execute_simps]:
   1.151    "i < length h a \<Longrightarrow>
   1.152     execute (map_entry i f a) h =
   1.153 -      Some (a, update a i (f (get_array a h ! i)) h)"
   1.154 +      Some (a, update a i (f (get_array h a ! i)) h)"
   1.155    "i \<ge> length h a \<Longrightarrow> execute (map_entry i f a) h = None"
   1.156    by (simp_all add: map_entry_def execute_simps)
   1.157  
   1.158 @@ -288,20 +288,20 @@
   1.159    by (auto intro: success_intros simp add: map_entry_def)
   1.160  
   1.161  lemma crel_map_entryI [crel_intros]:
   1.162 -  assumes "i < length h a" "h' = update a i (f (get_array a h ! i)) h" "r = a"
   1.163 +  assumes "i < length h a" "h' = update a i (f (get_array h a ! i)) h" "r = a"
   1.164    shows "crel (map_entry i f a) h h' r"
   1.165    by (rule crelI) (insert assms, simp add: execute_simps)
   1.166  
   1.167  lemma crel_map_entryE [crel_elims]:
   1.168    assumes "crel (map_entry i f a) h h' r"
   1.169 -  obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length h a"
   1.170 +  obtains "r = a" "h' = update a i (f (get_array h a ! i)) h" "i < length h a"
   1.171    using assms by (rule crelE)
   1.172      (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.173  
   1.174  lemma execute_swap [execute_simps]:
   1.175    "i < length h a \<Longrightarrow>
   1.176     execute (swap i x a) h =
   1.177 -      Some (get_array a h ! i, update a i x h)"
   1.178 +      Some (get_array h a ! i, update a i x h)"
   1.179    "i \<ge> length h a \<Longrightarrow> execute (swap i x a) h = None"
   1.180    by (simp_all add: swap_def execute_simps)
   1.181  
   1.182 @@ -310,18 +310,18 @@
   1.183    by (auto intro: success_intros simp add: swap_def)
   1.184  
   1.185  lemma crel_swapI [crel_intros]:
   1.186 -  assumes "i < length h a" "h' = update a i x h" "r = get_array a h ! i"
   1.187 +  assumes "i < length h a" "h' = update a i x h" "r = get_array h a ! i"
   1.188    shows "crel (swap i x a) h h' r"
   1.189    by (rule crelI) (insert assms, simp add: execute_simps)
   1.190  
   1.191  lemma crel_swapE [crel_elims]:
   1.192    assumes "crel (swap i x a) h h' r"
   1.193 -  obtains "r = get_array a h ! i" "h' = update a i x h" "i < length h a"
   1.194 +  obtains "r = get_array h a ! i" "h' = update a i x h" "i < length h a"
   1.195    using assms by (rule crelE)
   1.196      (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.197  
   1.198  lemma execute_freeze [execute_simps]:
   1.199 -  "execute (freeze a) h = Some (get_array a h, h)"
   1.200 +  "execute (freeze a) h = Some (get_array h a, h)"
   1.201    by (simp add: freeze_def execute_simps)
   1.202  
   1.203  lemma success_freezeI [success_intros]:
   1.204 @@ -329,13 +329,13 @@
   1.205    by (auto intro: success_intros simp add: freeze_def)
   1.206  
   1.207  lemma crel_freezeI [crel_intros]:
   1.208 -  assumes "h' = h" "r = get_array a h"
   1.209 +  assumes "h' = h" "r = get_array h a"
   1.210    shows "crel (freeze a) h h' r"
   1.211    by (rule crelI) (insert assms, simp add: execute_simps)
   1.212  
   1.213  lemma crel_freezeE [crel_elims]:
   1.214    assumes "crel (freeze a) h h' r"
   1.215 -  obtains "h' = h" "r = get_array a h"
   1.216 +  obtains "h' = h" "r = get_array h a"
   1.217    using assms by (rule crelE) (simp add: execute_simps)
   1.218  
   1.219  lemma upd_return:
   1.220 @@ -423,12 +423,12 @@
   1.221    fix h
   1.222    have *: "List.map
   1.223       (\<lambda>x. fst (the (if x < Array.length h a
   1.224 -                    then Some (get_array a h ! x, h) else None)))
   1.225 +                    then Some (get_array h a ! x, h) else None)))
   1.226       [0..<Array.length h a] =
   1.227 -       List.map (List.nth (get_array a h)) [0..<Array.length h a]"
   1.228 +       List.map (List.nth (get_array h a)) [0..<Array.length h a]"
   1.229      by simp
   1.230    have "execute (Heap_Monad.fold_map (Array.nth a) [0..<Array.length h a]) h =
   1.231 -    Some (get_array a h, h)"
   1.232 +    Some (get_array h a, h)"
   1.233      apply (subst execute_fold_map_unchanged_heap)
   1.234      apply (simp_all add: nth_def guard_def *)
   1.235      apply (simp add: length_def map_nth)
   1.236 @@ -436,7 +436,7 @@
   1.237    then have "execute (do {
   1.238        n \<leftarrow> Array.len a;
   1.239        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.240 -    }) h = Some (get_array a h, h)"
   1.241 +    }) h = Some (get_array h a, h)"
   1.242      by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
   1.243    then show "execute (Array.freeze a) h = execute (do {
   1.244        n \<leftarrow> Array.len a;
     2.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 16:00:56 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 16:12:40 2010 +0200
     2.3 @@ -219,15 +219,11 @@
     2.4  text {* Non-interaction between imperative array and imperative references *}
     2.5  
     2.6  lemma get_array_set [simp]:
     2.7 -  "get_array a (set r v h) = get_array a h"
     2.8 -  by (simp add: get_array_def set_def)
     2.9 -
    2.10 -lemma nth_set [simp]:
    2.11 -  "get_array a (set r v h) ! i = get_array a h ! i"
    2.12 -  by simp
    2.13 +  "get_array (set r v h) = get_array h"
    2.14 +  by (simp add: get_array_def set_def expand_fun_eq)
    2.15  
    2.16  lemma get_update [simp]:
    2.17 -  "get (Array.update a i v h) r  = get h r"
    2.18 +  "get (Array.update a i v h) r = get h r"
    2.19    by (simp add: get_def Array.update_def Array.set_def)
    2.20  
    2.21  lemma alloc_update:
    2.22 @@ -243,8 +239,8 @@
    2.23    by (simp add: Array.length_def get_array_def alloc_def set_def Let_def)
    2.24  
    2.25  lemma get_array_alloc [simp]: 
    2.26 -  "get_array a (snd (alloc v h)) = get_array a h"
    2.27 -  by (simp add: get_array_def alloc_def set_def Let_def)
    2.28 +  "get_array (snd (alloc v h)) = get_array h"
    2.29 +  by (simp add: get_array_def alloc_def set_def Let_def expand_fun_eq)
    2.30  
    2.31  lemma present_update [simp]: 
    2.32    "present (Array.update a i v h) = present h"
     3.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 16:00:56 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 16:12:40 2010 +0200
     3.3 @@ -23,15 +23,15 @@
     3.4  
     3.5  lemma crel_swapI [crel_intros]:
     3.6    assumes "i < Array.length h a" "j < Array.length h a"
     3.7 -    "x = get_array a h ! i" "y = get_array a h ! j"
     3.8 +    "x = get_array h a ! i" "y = get_array h a ! j"
     3.9      "h' = Array.update a j x (Array.update a i y h)"
    3.10    shows "crel (swap a i j) h h' r"
    3.11    unfolding swap_def using assms by (auto intro!: crel_intros)
    3.12  
    3.13  lemma swap_permutes:
    3.14    assumes "crel (swap a i j) h h' rs"
    3.15 -  shows "multiset_of (get_array a h') 
    3.16 -  = multiset_of (get_array a h)"
    3.17 +  shows "multiset_of (get_array h' a) 
    3.18 +  = multiset_of (get_array h a)"
    3.19    using assms
    3.20    unfolding swap_def
    3.21    by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
    3.22 @@ -55,8 +55,8 @@
    3.23  
    3.24  lemma part_permutes:
    3.25    assumes "crel (part1 a l r p) h h' rs"
    3.26 -  shows "multiset_of (get_array a h') 
    3.27 -  = multiset_of (get_array a h)"
    3.28 +  shows "multiset_of (get_array h' a) 
    3.29 +  = multiset_of (get_array h a)"
    3.30    using assms
    3.31  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    3.32    case (1 a l r p h h' rs)
    3.33 @@ -82,7 +82,7 @@
    3.34    next
    3.35      case False (* recursive case *)
    3.36      note rec_condition = this
    3.37 -    let ?v = "get_array a h ! l"
    3.38 +    let ?v = "get_array h a ! l"
    3.39      show ?thesis
    3.40      proof (cases "?v \<le> p")
    3.41        case True
    3.42 @@ -130,7 +130,7 @@
    3.43  
    3.44  lemma part_outer_remains:
    3.45    assumes "crel (part1 a l r p) h h' rs"
    3.46 -  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
    3.47 +  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array h (a::nat array) ! i = get_array h' a ! i"
    3.48    using assms
    3.49  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    3.50    case (1 a l r p h h' rs)
    3.51 @@ -145,7 +145,7 @@
    3.52    next
    3.53      case False (* recursive case *)
    3.54      note rec_condition = this
    3.55 -    let ?v = "get_array a h ! l"
    3.56 +    let ?v = "get_array h a ! l"
    3.57      show ?thesis
    3.58      proof (cases "?v \<le> p")
    3.59        case True
    3.60 @@ -163,7 +163,7 @@
    3.61          unfolding part1.simps[of a l r p]
    3.62          by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
    3.63        from swp rec_condition have
    3.64 -        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
    3.65 +        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array h a ! i = get_array h1 a ! i"
    3.66          unfolding swap_def
    3.67          by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
    3.68        with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
    3.69 @@ -174,8 +174,8 @@
    3.70  
    3.71  lemma part_partitions:
    3.72    assumes "crel (part1 a l r p) h h' rs"
    3.73 -  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
    3.74 -  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
    3.75 +  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array h' (a::nat array) ! i \<le> p)
    3.76 +  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array h' a ! i \<ge> p)"
    3.77    using assms
    3.78  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    3.79    case (1 a l r p h h' rs)
    3.80 @@ -192,7 +192,7 @@
    3.81    next
    3.82      case False (* recursive case *)
    3.83      note lr = this
    3.84 -    let ?v = "get_array a h ! l"
    3.85 +    let ?v = "get_array h a ! l"
    3.86      show ?thesis
    3.87      proof (cases "?v \<le> p")
    3.88        case True
    3.89 @@ -200,7 +200,7 @@
    3.90        have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    3.91          unfolding part1.simps[of a l r p]
    3.92          by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
    3.93 -      from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
    3.94 +      from True part_outer_remains[OF rec1] have a_l: "get_array h' a ! l \<le> p"
    3.95          by fastsimp
    3.96        have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
    3.97        with 1(1)[OF False True rec1] a_l show ?thesis
    3.98 @@ -212,10 +212,10 @@
    3.99          and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   3.100          unfolding part1.simps[of a l r p]
   3.101          by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   3.102 -      from swp False have "get_array a h1 ! r \<ge> p"
   3.103 +      from swp False have "get_array h1 a ! r \<ge> p"
   3.104          unfolding swap_def
   3.105          by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
   3.106 -      with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
   3.107 +      with part_outer_remains [OF rec2] lr have a_r: "get_array h' a ! r \<ge> p"
   3.108          by fastsimp
   3.109        have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
   3.110        with 1(2)[OF lr False rec2] a_r show ?thesis
   3.111 @@ -240,8 +240,8 @@
   3.112  
   3.113  lemma partition_permutes:
   3.114    assumes "crel (partition a l r) h h' rs"
   3.115 -  shows "multiset_of (get_array a h') 
   3.116 -  = multiset_of (get_array a h)"
   3.117 +  shows "multiset_of (get_array h' a) 
   3.118 +  = multiset_of (get_array h a)"
   3.119  proof -
   3.120      from assms part_permutes swap_permutes show ?thesis
   3.121        unfolding partition.simps
   3.122 @@ -260,7 +260,7 @@
   3.123  lemma partition_outer_remains:
   3.124    assumes "crel (partition a l r) h h' rs"
   3.125    assumes "l < r"
   3.126 -  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   3.127 +  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array h (a::nat array) ! i = get_array h' a ! i"
   3.128  proof -
   3.129    from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   3.130      unfolding partition.simps swap_def
   3.131 @@ -273,10 +273,10 @@
   3.132    shows "l \<le> rs \<and> rs \<le> r"
   3.133  proof -
   3.134    from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
   3.135 -    and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
   3.136 +    and rs_equals: "rs = (if get_array h'' a ! middle \<le> get_array h a ! r then middle + 1
   3.137           else middle)"
   3.138      unfolding partition.simps
   3.139 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
   3.140 +    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp 
   3.141    from `l < r` have "l \<le> r - 1" by arith
   3.142    from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   3.143  qed
   3.144 @@ -284,18 +284,18 @@
   3.145  lemma partition_partitions:
   3.146    assumes crel: "crel (partition a l r) h h' rs"
   3.147    assumes "l < r"
   3.148 -  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
   3.149 -  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
   3.150 +  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array h' (a::nat array) ! i \<le> get_array h' a ! rs) \<and>
   3.151 +  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array h' a ! rs \<le> get_array h' a ! i)"
   3.152  proof -
   3.153 -  let ?pivot = "get_array a h ! r" 
   3.154 +  let ?pivot = "get_array h a ! r" 
   3.155    from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
   3.156      and swap: "crel (swap a rs r) h1 h' ()"
   3.157 -    and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
   3.158 +    and rs_equals: "rs = (if get_array h1 a ! middle \<le> ?pivot then middle + 1
   3.159           else middle)"
   3.160      unfolding partition.simps
   3.161      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
   3.162 -  from swap have h'_def: "h' = Array.update a r (get_array a h1 ! rs)
   3.163 -    (Array.update a rs (get_array a h1 ! r) h1)"
   3.164 +  from swap have h'_def: "h' = Array.update a r (get_array h1 a ! rs)
   3.165 +    (Array.update a rs (get_array h1 a ! r) h1)"
   3.166      unfolding swap_def
   3.167      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   3.168    from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
   3.169 @@ -306,15 +306,15 @@
   3.170    from `l < r` have "l \<le> r - 1" by simp
   3.171    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   3.172    from part_outer_remains[OF part] `l < r`
   3.173 -  have "get_array a h ! r = get_array a h1 ! r"
   3.174 +  have "get_array h a ! r = get_array h1 a ! r"
   3.175      by fastsimp
   3.176    with swap
   3.177 -  have right_remains: "get_array a h ! r = get_array a h' ! rs"
   3.178 +  have right_remains: "get_array h a ! r = get_array h' a ! rs"
   3.179      unfolding swap_def
   3.180      by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
   3.181    from part_partitions [OF part]
   3.182    show ?thesis
   3.183 -  proof (cases "get_array a h1 ! middle \<le> ?pivot")
   3.184 +  proof (cases "get_array h1 a ! middle \<le> ?pivot")
   3.185      case True
   3.186      with rs_equals have rs_equals: "rs = middle + 1" by simp
   3.187      { 
   3.188 @@ -324,8 +324,8 @@
   3.189        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
   3.190        from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
   3.191        with part_partitions[OF part] right_remains True
   3.192 -      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   3.193 -      with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
   3.194 +      have "get_array h1 a ! i \<le> get_array h' a ! rs" by fastsimp
   3.195 +      with i_props h'_def in_bounds have "get_array h' a ! i \<le> get_array h' a ! rs"
   3.196          unfolding Array.update_def Array.length_def by simp
   3.197      }
   3.198      moreover
   3.199 @@ -334,13 +334,13 @@
   3.200        assume "rs < i \<and> i \<le> r"
   3.201  
   3.202        hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
   3.203 -      hence "get_array a h' ! rs \<le> get_array a h' ! i"
   3.204 +      hence "get_array h' a ! rs \<le> get_array h' a ! i"
   3.205        proof
   3.206          assume i_is: "rs < i \<and> i \<le> r - 1"
   3.207          with swap_length_remains in_bounds middle_in_bounds rs_equals
   3.208          have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
   3.209          from part_partitions[OF part] rs_equals right_remains i_is
   3.210 -        have "get_array a h' ! rs \<le> get_array a h1 ! i"
   3.211 +        have "get_array h' a ! rs \<le> get_array h1 a ! i"
   3.212            by fastsimp
   3.213          with i_props h'_def show ?thesis by fastsimp
   3.214        next
   3.215 @@ -348,7 +348,7 @@
   3.216          with rs_equals have "Suc middle \<noteq> r" by arith
   3.217          with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
   3.218          with part_partitions[OF part] right_remains 
   3.219 -        have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
   3.220 +        have "get_array h' a ! rs \<le> get_array h1 a ! (Suc middle)"
   3.221            by fastsimp
   3.222          with i_is True rs_equals right_remains h'_def
   3.223          show ?thesis using in_bounds
   3.224 @@ -366,8 +366,8 @@
   3.225        with swap_length_remains in_bounds middle_in_bounds rs_equals
   3.226        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
   3.227        from part_partitions[OF part] rs_equals right_remains i_is_left
   3.228 -      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   3.229 -      with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
   3.230 +      have "get_array h1 a ! i \<le> get_array h' a ! rs" by fastsimp
   3.231 +      with i_props h'_def have "get_array h' a ! i \<le> get_array h' a ! rs"
   3.232          unfolding Array.update_def by simp
   3.233      }
   3.234      moreover
   3.235 @@ -375,13 +375,13 @@
   3.236        fix i
   3.237        assume "rs < i \<and> i \<le> r"
   3.238        hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
   3.239 -      hence "get_array a h' ! rs \<le> get_array a h' ! i"
   3.240 +      hence "get_array h' a ! rs \<le> get_array h' a ! i"
   3.241        proof
   3.242          assume i_is: "rs < i \<and> i \<le> r - 1"
   3.243          with swap_length_remains in_bounds middle_in_bounds rs_equals
   3.244          have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
   3.245          from part_partitions[OF part] rs_equals right_remains i_is
   3.246 -        have "get_array a h' ! rs \<le> get_array a h1 ! i"
   3.247 +        have "get_array h' a ! rs \<le> get_array h1 a ! i"
   3.248            by fastsimp
   3.249          with i_props h'_def show ?thesis by fastsimp
   3.250        next
   3.251 @@ -420,8 +420,8 @@
   3.252  
   3.253  lemma quicksort_permutes:
   3.254    assumes "crel (quicksort a l r) h h' rs"
   3.255 -  shows "multiset_of (get_array a h') 
   3.256 -  = multiset_of (get_array a h)"
   3.257 +  shows "multiset_of (get_array h' a) 
   3.258 +  = multiset_of (get_array h a)"
   3.259    using assms
   3.260  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   3.261    case (1 a l r h h' rs)
   3.262 @@ -443,7 +443,7 @@
   3.263  
   3.264  lemma quicksort_outer_remains:
   3.265    assumes "crel (quicksort a l r) h h' rs"
   3.266 -   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   3.267 +   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array h (a::nat array) ! i = get_array h' a ! i"
   3.268    using assms
   3.269  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   3.270    case (1 a l r h h' rs)
   3.271 @@ -465,14 +465,14 @@
   3.272        assume pivot: "l \<le> p \<and> p \<le> r"
   3.273        assume i_outer: "i < l \<or> r < i"
   3.274        from  partition_outer_remains [OF part True] i_outer
   3.275 -      have "get_array a h !i = get_array a h1 ! i" by fastsimp
   3.276 +      have "get_array h a !i = get_array h1 a ! i" by fastsimp
   3.277        moreover
   3.278        with 1(1) [OF True pivot qs1] pivot i_outer
   3.279 -      have "get_array a h1 ! i = get_array a h2 ! i" by auto
   3.280 +      have "get_array h1 a ! i = get_array h2 a ! i" by auto
   3.281        moreover
   3.282        with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
   3.283 -      have "get_array a h2 ! i = get_array a h' ! i" by auto
   3.284 -      ultimately have "get_array a h ! i= get_array a h' ! i" by simp
   3.285 +      have "get_array h2 a ! i = get_array h' a ! i" by auto
   3.286 +      ultimately have "get_array h a ! i= get_array h' a ! i" by simp
   3.287      }
   3.288      with cr show ?thesis
   3.289        unfolding quicksort.simps [of a l r]
   3.290 @@ -512,7 +512,7 @@
   3.291        have pivot: "l\<le> p \<and> p \<le> r" .
   3.292       note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
   3.293        from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
   3.294 -      have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
   3.295 +      have pivot_unchanged: "get_array h1 a ! p = get_array h' a ! p" by (cases p, auto)
   3.296          (*-- First of all, by induction hypothesis both sublists are sorted. *)
   3.297        from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
   3.298        have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
   3.299 @@ -525,35 +525,35 @@
   3.300          by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
   3.301             (* -- Secondly, both sublists remain partitioned. *)
   3.302        from partition_partitions[OF part True]
   3.303 -      have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
   3.304 -        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
   3.305 +      have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array h1 a ! p "
   3.306 +        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array h1 a ! p \<le> j"
   3.307          by (auto simp add: all_in_set_subarray_conv)
   3.308        from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
   3.309 -        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
   3.310 +        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array h1 a" "get_array h2 a"]
   3.311        have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
   3.312          unfolding Array.length_def subarray_def by (cases p, auto)
   3.313        with left_subarray_remains part_conds1 pivot_unchanged
   3.314 -      have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
   3.315 +      have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array h' a ! p"
   3.316          by (simp, subst set_of_multiset_of[symmetric], simp)
   3.317            (* -- These steps are the analogous for the right sublist \<dots> *)
   3.318        from quicksort_outer_remains [OF qs1] length_remains
   3.319        have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
   3.320          by (auto simp add: subarray_eq_samelength_iff)
   3.321        from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
   3.322 -        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
   3.323 +        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array h2 a" "get_array h' a"]
   3.324        have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
   3.325          unfolding Array.length_def subarray_def by auto
   3.326        with right_subarray_remains part_conds2 pivot_unchanged
   3.327 -      have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
   3.328 +      have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array h' a ! p \<le> j"
   3.329          by (simp, subst set_of_multiset_of[symmetric], simp)
   3.330            (* -- Thirdly and finally, we show that the array is sorted
   3.331            following from the facts above. *)
   3.332 -      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'"
   3.333 +      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'"
   3.334          by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
   3.335        with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
   3.336          unfolding subarray_def
   3.337          apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
   3.338 -        by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
   3.339 +        by (auto simp add: set_sublist' dest: le_trans [of _ "get_array h' a ! p"])
   3.340      }
   3.341      with True cr show ?thesis
   3.342        unfolding quicksort.simps [of a l r]
   3.343 @@ -564,16 +564,16 @@
   3.344  
   3.345  lemma quicksort_is_sort:
   3.346    assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
   3.347 -  shows "get_array a h' = sort (get_array a h)"
   3.348 -proof (cases "get_array a h = []")
   3.349 +  shows "get_array h' a = sort (get_array h a)"
   3.350 +proof (cases "get_array h a = []")
   3.351    case True
   3.352    with quicksort_is_skip[OF crel] show ?thesis
   3.353    unfolding Array.length_def by simp
   3.354  next
   3.355    case False
   3.356 -  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
   3.357 +  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array h a)) (get_array h' a))"
   3.358      unfolding Array.length_def subarray_def by auto
   3.359 -  with length_remains[OF crel] have "sorted (get_array a h')"
   3.360 +  with length_remains[OF crel] have "sorted (get_array h' a)"
   3.361      unfolding Array.length_def by simp
   3.362    with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
   3.363  qed
     4.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 16:00:56 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 16:12:40 2010 +0200
     4.3 @@ -27,17 +27,17 @@
     4.4  declare swap.simps [simp del] rev.simps [simp del]
     4.5  
     4.6  lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
     4.7 -  shows "get_array a h' ! k = (if k = i then get_array a h ! j
     4.8 -      else if k = j then get_array a h ! i
     4.9 -      else get_array a h ! k)"
    4.10 +  shows "get_array h' a ! k = (if k = i then get_array h a ! j
    4.11 +      else if k = j then get_array h a ! i
    4.12 +      else get_array h a ! k)"
    4.13  using assms unfolding swap.simps
    4.14  by (elim crel_elims)
    4.15   (auto simp: length_def)
    4.16  
    4.17  lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
    4.18 -  shows "get_array a h' ! k = (if k < i then get_array a h ! k
    4.19 -      else if j < k then get_array a h ! k
    4.20 -      else get_array a h ! (j - (k - i)))" (is "?P a i j h h'")
    4.21 +  shows "get_array h' a ! k = (if k < i then get_array h a ! k
    4.22 +      else if j < k then get_array h a ! k
    4.23 +      else get_array h a ! (j - (k - i)))" (is "?P a i j h h'")
    4.24  using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
    4.25    case (1 a i j h h'')
    4.26    thus ?case
    4.27 @@ -94,7 +94,7 @@
    4.28    {
    4.29      fix k
    4.30      assume "k < Suc j - i"
    4.31 -    with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - k)"
    4.32 +    with rev_pointwise[OF assms(1)] have "get_array h' a ! (i + k) = get_array h a ! (j - k)"
    4.33        by auto
    4.34    } 
    4.35    with assms(2) rev_length[OF assms(1)] show ?thesis
    4.36 @@ -104,10 +104,10 @@
    4.37  
    4.38  lemma rev2_rev: 
    4.39    assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
    4.40 -  shows "get_array a h' = List.rev (get_array a h)"
    4.41 +  shows "get_array h' a = List.rev (get_array h a)"
    4.42    using rev2_rev'[OF assms] rev_length[OF assms] assms
    4.43      by (cases "Array.length h a = 0", auto simp add: Array.length_def
    4.44        subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
    4.45 -  (drule sym[of "List.length (get_array a h)"], simp)
    4.46 +  (drule sym[of "List.length (get_array h a)"], simp)
    4.47  
    4.48  end
     5.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 16:00:56 2010 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 16:12:40 2010 +0200
     5.3 @@ -120,17 +120,17 @@
     5.4  
     5.5  definition
     5.6    array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
     5.7 -  "array_ran a h = {e. Some e \<in> set (get_array a h)}"
     5.8 +  "array_ran a h = {e. Some e \<in> set (get_array h a)}"
     5.9      -- {*FIXME*}
    5.10  
    5.11 -lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length h a \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
    5.12 +lemma array_ranI: "\<lbrakk> Some b = get_array h a ! i; i < Array.length h a \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
    5.13  unfolding array_ran_def Array.length_def by simp
    5.14  
    5.15  lemma array_ran_upd_array_Some:
    5.16    assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
    5.17    shows "cl \<in> array_ran a h \<or> cl = b"
    5.18  proof -
    5.19 -  have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
    5.20 +  have "set (get_array h a[i := Some b]) \<subseteq> insert (Some b) (set (get_array h a))" by (rule set_update_subset_insert)
    5.21    with assms show ?thesis 
    5.22      unfolding array_ran_def Array.update_def by fastsimp
    5.23  qed
    5.24 @@ -139,7 +139,7 @@
    5.25    assumes "cl \<in> array_ran a (Array.update a i None h)"
    5.26    shows "cl \<in> array_ran a h"
    5.27  proof -
    5.28 -  have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
    5.29 +  have "set (get_array h a[i := None]) \<subseteq> insert None (set (get_array h a))" by (rule set_update_subset_insert)
    5.30    with assms show ?thesis
    5.31      unfolding array_ran_def Array.update_def by auto
    5.32  qed
    5.33 @@ -477,7 +477,7 @@
    5.34      fix clj
    5.35      let ?rs = "merge (remove l cli) (remove (compl l) clj)"
    5.36      let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
    5.37 -    assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length h' a"
    5.38 +    assume "h = h'" "Some clj = get_array h' a ! j" "j < Array.length h' a"
    5.39      with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj"
    5.40        unfolding correctArray_def by (auto intro: array_ranI)
    5.41      with clj l_not_zero correct_cli
    5.42 @@ -491,7 +491,7 @@
    5.43    }
    5.44    {
    5.45      fix v clj
    5.46 -    assume "Some clj = get_array a h ! j" "j < Array.length h a"
    5.47 +    assume "Some clj = get_array h a ! j" "j < Array.length h a"
    5.48      with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
    5.49        unfolding correctArray_def by (auto intro: array_ranI)
    5.50      assume "crel (res_thm' l cli clj) h h' rs"
     6.1 --- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 16:00:56 2010 +0200
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 16:12:40 2010 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  begin
     6.5  
     6.6  definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
     6.7 -  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
     6.8 +  "subarray n m a h \<equiv> sublist' n m (get_array h a)"
     6.9  
    6.10  lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
    6.11  apply (simp add: subarray_def Array.update_def)
    6.12 @@ -30,7 +30,7 @@
    6.13  lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
    6.14  by (simp add: subarray_def sublist'_Nil')
    6.15  
    6.16 -lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
    6.17 +lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array h a ! n]" 
    6.18  by (simp add: subarray_def length_def sublist'_single)
    6.19  
    6.20  lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
    6.21 @@ -39,11 +39,11 @@
    6.22  lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
    6.23  by (simp add: length_subarray)
    6.24  
    6.25 -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"
    6.26 +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"
    6.27  unfolding Array.length_def subarray_def
    6.28  by (simp add: sublist'_front)
    6.29  
    6.30 -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)]"
    6.31 +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)]"
    6.32  unfolding Array.length_def subarray_def
    6.33  by (simp add: sublist'_back)
    6.34  
    6.35 @@ -51,21 +51,21 @@
    6.36  unfolding subarray_def
    6.37  by (simp add: sublist'_append)
    6.38  
    6.39 -lemma subarray_all: "subarray 0 (Array.length h a) a h = get_array a h"
    6.40 +lemma subarray_all: "subarray 0 (Array.length h a) a h = get_array h a"
    6.41  unfolding Array.length_def subarray_def
    6.42  by (simp add: sublist'_all)
    6.43  
    6.44 -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)"
    6.45 +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)"
    6.46  unfolding Array.length_def subarray_def
    6.47  by (simp add: nth_sublist')
    6.48  
    6.49 -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')"
    6.50 +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')"
    6.51  unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
    6.52  
    6.53 -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))"
    6.54 +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))"
    6.55  unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
    6.56  
    6.57 -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))"
    6.58 +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))"
    6.59  unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
    6.60  
    6.61  end
    6.62 \ No newline at end of file