canonical argument order for length
authorhaftmann
Tue Jul 13 15:34:02 2010 +0200 (2010-07-13 ago)
changeset 37802f2e9c104cebd
parent 37801 868ceaa6b039
child 37803 582d0fbd201e
canonical argument order for length
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 11:23:21 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 15:34:02 2010 +0200
     1.3 @@ -31,9 +31,8 @@
     1.4       h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
     1.5     in (r, h''))"
     1.6  
     1.7 -definition (*FIXME length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where*)
     1.8 -  length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
     1.9 -  "length a h = List.length (get_array a h)"
    1.10 +definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where
    1.11 +  "length h a = List.length (get_array a h)"
    1.12    
    1.13  definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
    1.14    "update a i x h = set_array a ((get_array a h)[i:=x]) h"
    1.15 @@ -55,22 +54,22 @@
    1.16    [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
    1.17  
    1.18  definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
    1.19 -  [code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)"
    1.20 +  [code del]: "len a = Heap_Monad.tap (\<lambda>h. length h a)"
    1.21  
    1.22  definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
    1.23 -  [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.24 +  [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length h a)
    1.25      (\<lambda>h. (get_array a h ! i, h))"
    1.26  
    1.27  definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
    1.28 -  [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.29 +  [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
    1.30      (\<lambda>h. (a, update a i x h))"
    1.31  
    1.32  definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
    1.33 -  [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.34 +  [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length h a)
    1.35      (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))"
    1.36  
    1.37  definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
    1.38 -  [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.39 +  [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
    1.40      (\<lambda>h. (get_array a h ! i, update a i x h))"
    1.41  
    1.42  definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
    1.43 @@ -121,8 +120,8 @@
    1.44    by simp
    1.45  
    1.46  lemma length_update [simp]: 
    1.47 -  "length a (update b i v h) = length a h"
    1.48 -  by (simp add: update_def length_def set_array_def get_array_def)
    1.49 +  "length (update b i v h) = length h"
    1.50 +  by (simp add: update_def length_def set_array_def get_array_def expand_fun_eq)
    1.51  
    1.52  lemma update_swap_neqArray:
    1.53    "a =!!= a' \<Longrightarrow> 
    1.54 @@ -223,7 +222,7 @@
    1.55    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.56  
    1.57  lemma execute_len [execute_simps]:
    1.58 -  "execute (len a) h = Some (length a h, h)"
    1.59 +  "execute (len a) h = Some (length h a, h)"
    1.60    by (simp add: len_def execute_simps)
    1.61  
    1.62  lemma success_lenI [success_intros]:
    1.63 @@ -231,100 +230,100 @@
    1.64    by (auto intro: success_intros simp add: len_def)
    1.65  
    1.66  lemma crel_lengthI [crel_intros]:
    1.67 -  assumes "h' = h" "r = length a h"
    1.68 +  assumes "h' = h" "r = length h a"
    1.69    shows "crel (len a) h h' r"
    1.70    by (rule crelI) (simp add: assms execute_simps)
    1.71  
    1.72  lemma crel_lengthE [crel_elims]:
    1.73    assumes "crel (len a) h h' r"
    1.74 -  obtains "r = length a h'" "h' = h" 
    1.75 +  obtains "r = length h' a" "h' = h" 
    1.76    using assms by (rule crelE) (simp add: execute_simps)
    1.77  
    1.78  lemma execute_nth [execute_simps]:
    1.79 -  "i < length a h \<Longrightarrow>
    1.80 +  "i < length h a \<Longrightarrow>
    1.81      execute (nth a i) h = Some (get_array a h ! i, h)"
    1.82 -  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
    1.83 +  "i \<ge> length h a \<Longrightarrow> execute (nth a i) h = None"
    1.84    by (simp_all add: nth_def execute_simps)
    1.85  
    1.86  lemma success_nthI [success_intros]:
    1.87 -  "i < length a h \<Longrightarrow> success (nth a i) h"
    1.88 +  "i < length h a \<Longrightarrow> success (nth a i) h"
    1.89    by (auto intro: success_intros simp add: nth_def)
    1.90  
    1.91  lemma crel_nthI [crel_intros]:
    1.92 -  assumes "i < length a h" "h' = h" "r = get_array a h ! i"
    1.93 +  assumes "i < length h a" "h' = h" "r = get_array a h ! i"
    1.94    shows "crel (nth a i) h h' r"
    1.95    by (rule crelI) (insert assms, simp add: execute_simps)
    1.96  
    1.97  lemma crel_nthE [crel_elims]:
    1.98    assumes "crel (nth a i) h h' r"
    1.99 -  obtains "i < length a h" "r = get_array a h ! i" "h' = h"
   1.100 +  obtains "i < length h a" "r = get_array a h ! i" "h' = h"
   1.101    using assms by (rule crelE)
   1.102 -    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.103 +    (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.104  
   1.105  lemma execute_upd [execute_simps]:
   1.106 -  "i < length a h \<Longrightarrow>
   1.107 +  "i < length h a \<Longrightarrow>
   1.108      execute (upd i x a) h = Some (a, update a i x h)"
   1.109 -  "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
   1.110 +  "i \<ge> length h a \<Longrightarrow> execute (upd i x a) h = None"
   1.111    by (simp_all add: upd_def execute_simps)
   1.112  
   1.113  lemma success_updI [success_intros]:
   1.114 -  "i < length a h \<Longrightarrow> success (upd i x a) h"
   1.115 +  "i < length h a \<Longrightarrow> success (upd i x a) h"
   1.116    by (auto intro: success_intros simp add: upd_def)
   1.117  
   1.118  lemma crel_updI [crel_intros]:
   1.119 -  assumes "i < length a h" "h' = update a i v h"
   1.120 +  assumes "i < length h a" "h' = update a i v h"
   1.121    shows "crel (upd i v a) h h' a"
   1.122    by (rule crelI) (insert assms, simp add: execute_simps)
   1.123  
   1.124  lemma crel_updE [crel_elims]:
   1.125    assumes "crel (upd i v a) h h' r"
   1.126 -  obtains "r = a" "h' = update a i v h" "i < length a h"
   1.127 +  obtains "r = a" "h' = update a i v h" "i < length h a"
   1.128    using assms by (rule crelE)
   1.129 -    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.130 +    (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.131  
   1.132  lemma execute_map_entry [execute_simps]:
   1.133 -  "i < length a h \<Longrightarrow>
   1.134 +  "i < length h a \<Longrightarrow>
   1.135     execute (map_entry i f a) h =
   1.136        Some (a, update a i (f (get_array a h ! i)) h)"
   1.137 -  "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
   1.138 +  "i \<ge> length h a \<Longrightarrow> execute (map_entry i f a) h = None"
   1.139    by (simp_all add: map_entry_def execute_simps)
   1.140  
   1.141  lemma success_map_entryI [success_intros]:
   1.142 -  "i < length a h \<Longrightarrow> success (map_entry i f a) h"
   1.143 +  "i < length h a \<Longrightarrow> success (map_entry i f a) h"
   1.144    by (auto intro: success_intros simp add: map_entry_def)
   1.145  
   1.146  lemma crel_map_entryI [crel_intros]:
   1.147 -  assumes "i < length a h" "h' = update a i (f (get_array a h ! i)) h" "r = a"
   1.148 +  assumes "i < length h a" "h' = update a i (f (get_array a h ! i)) h" "r = a"
   1.149    shows "crel (map_entry i f a) h h' r"
   1.150    by (rule crelI) (insert assms, simp add: execute_simps)
   1.151  
   1.152  lemma crel_map_entryE [crel_elims]:
   1.153    assumes "crel (map_entry i f a) h h' r"
   1.154 -  obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length a h"
   1.155 +  obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length h a"
   1.156    using assms by (rule crelE)
   1.157 -    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.158 +    (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.159  
   1.160  lemma execute_swap [execute_simps]:
   1.161 -  "i < length a h \<Longrightarrow>
   1.162 +  "i < length h a \<Longrightarrow>
   1.163     execute (swap i x a) h =
   1.164        Some (get_array a h ! i, update a i x h)"
   1.165 -  "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
   1.166 +  "i \<ge> length h a \<Longrightarrow> execute (swap i x a) h = None"
   1.167    by (simp_all add: swap_def execute_simps)
   1.168  
   1.169  lemma success_swapI [success_intros]:
   1.170 -  "i < length a h \<Longrightarrow> success (swap i x a) h"
   1.171 +  "i < length h a \<Longrightarrow> success (swap i x a) h"
   1.172    by (auto intro: success_intros simp add: swap_def)
   1.173  
   1.174  lemma crel_swapI [crel_intros]:
   1.175 -  assumes "i < length a h" "h' = update a i x h" "r = get_array a h ! i"
   1.176 +  assumes "i < length h a" "h' = update a i x h" "r = get_array a h ! i"
   1.177    shows "crel (swap i x a) h h' r"
   1.178    by (rule crelI) (insert assms, simp add: execute_simps)
   1.179  
   1.180  lemma crel_swapE [crel_elims]:
   1.181    assumes "crel (swap i x a) h h' r"
   1.182 -  obtains "r = get_array a h ! i" "h' = update a i x h" "i < length a h"
   1.183 +  obtains "r = get_array a h ! i" "h' = update a i x h" "i < length h a"
   1.184    using assms by (rule crelE)
   1.185 -    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.186 +    (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.187  
   1.188  lemma execute_freeze [execute_simps]:
   1.189    "execute (freeze a) h = Some (get_array a h, h)"
   1.190 @@ -428,12 +427,12 @@
   1.191  proof (rule Heap_eqI)
   1.192    fix h
   1.193    have *: "List.map
   1.194 -     (\<lambda>x. fst (the (if x < length a h
   1.195 +     (\<lambda>x. fst (the (if x < length h a
   1.196                      then Some (get_array a h ! x, h) else None)))
   1.197 -     [0..<length a h] =
   1.198 -       List.map (List.nth (get_array a h)) [0..<length a h]"
   1.199 +     [0..<length h a] =
   1.200 +       List.map (List.nth (get_array a h)) [0..<length h a]"
   1.201      by simp
   1.202 -  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
   1.203 +  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length h a]) h =
   1.204      Some (get_array a h, h)"
   1.205      apply (subst execute_fold_map_unchanged_heap)
   1.206      apply (simp_all add: nth_def guard_def *)
     2.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 11:23:21 2010 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 15:34:02 2010 +0200
     2.3 @@ -239,7 +239,7 @@
     2.4    by (simp add: Array.update_def get_array_def set_array_def set_def)
     2.5  
     2.6  lemma length_alloc [simp]: 
     2.7 -  "Array.length a (snd (alloc v h)) = Array.length a h"
     2.8 +  "Array.length (snd (alloc v h)) a = Array.length h a"
     2.9    by (simp add: Array.length_def get_array_def alloc_def set_def Let_def)
    2.10  
    2.11  lemma get_array_alloc [simp]: 
     3.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 11:23:21 2010 +0100
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 15:34:02 2010 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4       }"
     3.5  
     3.6  lemma crel_swapI [crel_intros]:
     3.7 -  assumes "i < Array.length a h" "j < Array.length a h"
     3.8 +  assumes "i < Array.length h a" "j < Array.length h a"
     3.9      "x = get_array a h ! i" "y = get_array a h ! j"
    3.10      "h' = Array.update a j x (Array.update a i y h)"
    3.11    shows "crel (swap a i j) h h' r"
    3.12 @@ -108,7 +108,7 @@
    3.13  
    3.14  lemma part_length_remains:
    3.15    assumes "crel (part1 a l r p) h h' rs"
    3.16 -  shows "Array.length a h = Array.length a h'"
    3.17 +  shows "Array.length h a = Array.length h' a"
    3.18  using assms
    3.19  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    3.20    case (1 a l r p h h' rs)
    3.21 @@ -250,7 +250,7 @@
    3.22  
    3.23  lemma partition_length_remains:
    3.24    assumes "crel (partition a l r) h h' rs"
    3.25 -  shows "Array.length a h = Array.length a h'"
    3.26 +  shows "Array.length h a = Array.length h' a"
    3.27  proof -
    3.28    from assms part_length_remains show ?thesis
    3.29      unfolding partition.simps swap_def
    3.30 @@ -298,10 +298,10 @@
    3.31      (Array.update a rs (get_array a h1 ! r) h1)"
    3.32      unfolding swap_def
    3.33      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
    3.34 -  from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
    3.35 +  from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
    3.36      unfolding swap_def
    3.37      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
    3.38 -  from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
    3.39 +  from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
    3.40      unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
    3.41    from `l < r` have "l \<le> r - 1" by simp
    3.42    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
    3.43 @@ -321,7 +321,7 @@
    3.44        fix i
    3.45        assume i_is_left: "l \<le> i \<and> i < rs"
    3.46        with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
    3.47 -      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    3.48 +      have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    3.49        from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
    3.50        with part_partitions[OF part] right_remains True
    3.51        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    3.52 @@ -338,7 +338,7 @@
    3.53        proof
    3.54          assume i_is: "rs < i \<and> i \<le> r - 1"
    3.55          with swap_length_remains in_bounds middle_in_bounds rs_equals
    3.56 -        have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    3.57 +        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    3.58          from part_partitions[OF part] rs_equals right_remains i_is
    3.59          have "get_array a h' ! rs \<le> get_array a h1 ! i"
    3.60            by fastsimp
    3.61 @@ -364,7 +364,7 @@
    3.62        fix i
    3.63        assume i_is_left: "l \<le> i \<and> i < rs"
    3.64        with swap_length_remains in_bounds middle_in_bounds rs_equals
    3.65 -      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    3.66 +      have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    3.67        from part_partitions[OF part] rs_equals right_remains i_is_left
    3.68        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    3.69        with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
    3.70 @@ -379,7 +379,7 @@
    3.71        proof
    3.72          assume i_is: "rs < i \<and> i \<le> r - 1"
    3.73          with swap_length_remains in_bounds middle_in_bounds rs_equals
    3.74 -        have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    3.75 +        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    3.76          from part_partitions[OF part] rs_equals right_remains i_is
    3.77          have "get_array a h' ! rs \<le> get_array a h1 ! i"
    3.78            by fastsimp
    3.79 @@ -432,7 +432,7 @@
    3.80  
    3.81  lemma length_remains:
    3.82    assumes "crel (quicksort a l r) h h' rs"
    3.83 -  shows "Array.length a h = Array.length a h'"
    3.84 +  shows "Array.length h a = Array.length h' a"
    3.85  using assms
    3.86  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
    3.87    case (1 a l r h h' rs)
    3.88 @@ -489,7 +489,7 @@
    3.89   
    3.90  lemma quicksort_sorts:
    3.91    assumes "crel (quicksort a l r) h h' rs"
    3.92 -  assumes l_r_length: "l < Array.length a h" "r < Array.length a h" 
    3.93 +  assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
    3.94    shows "sorted (subarray l (r + 1) a h')"
    3.95    using assms
    3.96  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
    3.97 @@ -563,7 +563,7 @@
    3.98  
    3.99  
   3.100  lemma quicksort_is_sort:
   3.101 -  assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
   3.102 +  assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
   3.103    shows "get_array a h' = sort (get_array a h)"
   3.104  proof (cases "get_array a h = []")
   3.105    case True
   3.106 @@ -583,7 +583,7 @@
   3.107  We will now show that exceptions do not occur. *}
   3.108  
   3.109  lemma success_part1I: 
   3.110 -  assumes "l < Array.length a h" "r < Array.length a h"
   3.111 +  assumes "l < Array.length h a" "r < Array.length h a"
   3.112    shows "success (part1 a l r p) h"
   3.113    using assms
   3.114  proof (induct a l r p arbitrary: h rule: part1.induct)
   3.115 @@ -606,7 +606,7 @@
   3.116  qed
   3.117  
   3.118  lemma success_partitionI:
   3.119 -  assumes "l < r" "l < Array.length a h" "r < Array.length a h"
   3.120 +  assumes "l < r" "l < Array.length h a" "r < Array.length h a"
   3.121    shows "success (partition a l r) h"
   3.122  using assms unfolding partition.simps swap_def
   3.123  apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:)
   3.124 @@ -621,7 +621,7 @@
   3.125  done
   3.126  
   3.127  lemma success_quicksortI:
   3.128 -  assumes "l < Array.length a h" "r < Array.length a h"
   3.129 +  assumes "l < Array.length h a" "r < Array.length h a"
   3.130    shows "success (quicksort a l r) h"
   3.131  using assms
   3.132  proof (induct a l r arbitrary: h rule: quicksort.induct)
     4.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 11:23:21 2010 +0100
     4.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 15:34:02 2010 +0200
     4.3 @@ -64,7 +64,7 @@
     4.4  
     4.5  lemma rev_length:
     4.6    assumes "crel (rev a i j) h h' r"
     4.7 -  shows "Array.length a h = Array.length a h'"
     4.8 +  shows "Array.length h a = Array.length h' a"
     4.9  using assms
    4.10  proof (induct a i j arbitrary: h h' rule: rev.induct)
    4.11    case (1 a i j h h'')
    4.12 @@ -88,7 +88,7 @@
    4.13  qed
    4.14  
    4.15  lemma rev2_rev': assumes "crel (rev a i j) h h' u"
    4.16 -  assumes "j < Array.length a h"
    4.17 +  assumes "j < Array.length h a"
    4.18    shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
    4.19  proof - 
    4.20    {
    4.21 @@ -103,10 +103,10 @@
    4.22  qed
    4.23  
    4.24  lemma rev2_rev: 
    4.25 -  assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
    4.26 +  assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
    4.27    shows "get_array a h' = List.rev (get_array a h)"
    4.28    using rev2_rev'[OF assms] rev_length[OF assms] assms
    4.29 -    by (cases "Array.length a h = 0", auto simp add: Array.length_def
    4.30 +    by (cases "Array.length h a = 0", auto simp add: Array.length_def
    4.31        subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
    4.32    (drule sym[of "List.length (get_array a h)"], simp)
    4.33  
     5.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 11:23:21 2010 +0100
     5.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 15:34:02 2010 +0200
     5.3 @@ -123,7 +123,7 @@
     5.4    "array_ran a h = {e. Some e \<in> set (get_array a h)}"
     5.5      -- {*FIXME*}
     5.6  
     5.7 -lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
     5.8 +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.9  unfolding array_ran_def Array.length_def by simp
    5.10  
    5.11  lemma array_ran_upd_array_Some:
    5.12 @@ -477,7 +477,7 @@
    5.13      fix clj
    5.14      let ?rs = "merge (remove l cli) (remove (compl l) clj)"
    5.15      let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
    5.16 -    assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length a h'"
    5.17 +    assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length h' a"
    5.18      with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj"
    5.19        unfolding correctArray_def by (auto intro: array_ranI)
    5.20      with clj l_not_zero correct_cli
    5.21 @@ -491,7 +491,7 @@
    5.22    }
    5.23    {
    5.24      fix v clj
    5.25 -    assume "Some clj = get_array a h ! j" "j < Array.length a h"
    5.26 +    assume "Some clj = get_array a h ! j" "j < Array.length h a"
    5.27      with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
    5.28        unfolding correctArray_def by (auto intro: array_ranI)
    5.29      assume "crel (res_thm' l cli clj) h h' rs"
     6.1 --- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 11:23:21 2010 +0100
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 15:34:02 2010 +0200
     6.3 @@ -30,20 +30,20 @@
     6.4  lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
     6.5  by (simp add: subarray_def sublist'_Nil')
     6.6  
     6.7 -lemma subarray_single: "\<lbrakk> n < Array.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
     6.8 +lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
     6.9  by (simp add: subarray_def length_def sublist'_single)
    6.10  
    6.11 -lemma length_subarray: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
    6.12 +lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
    6.13  by (simp add: subarray_def length_def length_sublist')
    6.14  
    6.15 -lemma length_subarray_0: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
    6.16 +lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
    6.17  by (simp add: length_subarray)
    6.18  
    6.19 -lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
    6.20 +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.21  unfolding Array.length_def subarray_def
    6.22  by (simp add: sublist'_front)
    6.23  
    6.24 -lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
    6.25 +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.26  unfolding Array.length_def subarray_def
    6.27  by (simp add: sublist'_back)
    6.28  
    6.29 @@ -51,21 +51,21 @@
    6.30  unfolding subarray_def
    6.31  by (simp add: sublist'_append)
    6.32  
    6.33 -lemma subarray_all: "subarray 0 (Array.length a h) a h = get_array a h"
    6.34 +lemma subarray_all: "subarray 0 (Array.length h a) a h = get_array a h"
    6.35  unfolding Array.length_def subarray_def
    6.36  by (simp add: sublist'_all)
    6.37  
    6.38 -lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
    6.39 +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.40  unfolding Array.length_def subarray_def
    6.41  by (simp add: nth_sublist')
    6.42  
    6.43 -lemma subarray_eq_samelength_iff: "Array.length a h = Array.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
    6.44 +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.45  unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
    6.46  
    6.47 -lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))"
    6.48 +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.49  unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
    6.50  
    6.51 -lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))"
    6.52 +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.53  unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
    6.54  
    6.55  end
    6.56 \ No newline at end of file