# HG changeset patch
# User haftmann
# Date 1279028042 -7200
# Node ID f2e9c104cebd341dd33dd9f3565e6ac5bb106c9b
# Parent  868ceaa6b039245bcd73a7ddb7582f45e1925f12
canonical argument order for length

diff -r 868ceaa6b039 -r f2e9c104cebd src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 11:23:21 2010 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 15:34:02 2010 +0200
@@ -31,9 +31,8 @@
      h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
    in (r, h''))"
 
-definition (*FIXME length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where*)
-  length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
-  "length a h = List.length (get_array a h)"
+definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where
+  "length h a = List.length (get_array a h)"
   
 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"
@@ -55,22 +54,22 @@
   [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
 
 definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
-  [code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)"
+  [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 a h)
+  [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length h a)
     (\<lambda>h. (get_array a h ! 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 a h)
+  [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
     (\<lambda>h. (a, update a i x h))"
 
 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 a h)
+  [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))"
 
 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 a h)
+  [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))"
 
 definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
@@ -121,8 +120,8 @@
   by simp
 
 lemma length_update [simp]: 
-  "length a (update b i v h) = length a h"
-  by (simp add: update_def length_def set_array_def get_array_def)
+  "length (update b i v h) = length h"
+  by (simp add: update_def length_def set_array_def get_array_def expand_fun_eq)
 
 lemma update_swap_neqArray:
   "a =!!= a' \<Longrightarrow> 
@@ -223,7 +222,7 @@
   using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
 
 lemma execute_len [execute_simps]:
-  "execute (len a) h = Some (length a h, h)"
+  "execute (len a) h = Some (length h a, h)"
   by (simp add: len_def execute_simps)
 
 lemma success_lenI [success_intros]:
@@ -231,100 +230,100 @@
   by (auto intro: success_intros simp add: len_def)
 
 lemma crel_lengthI [crel_intros]:
-  assumes "h' = h" "r = length a h"
+  assumes "h' = h" "r = length h a"
   shows "crel (len a) h h' r"
   by (rule crelI) (simp add: assms execute_simps)
 
 lemma crel_lengthE [crel_elims]:
   assumes "crel (len a) h h' r"
-  obtains "r = length a h'" "h' = h" 
+  obtains "r = length h' a" "h' = h" 
   using assms by (rule crelE) (simp add: execute_simps)
 
 lemma execute_nth [execute_simps]:
-  "i < length a h \<Longrightarrow>
+  "i < length h a \<Longrightarrow>
     execute (nth a i) h = Some (get_array a h ! i, h)"
-  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+  "i \<ge> length h a \<Longrightarrow> execute (nth a i) h = None"
   by (simp_all add: nth_def execute_simps)
 
 lemma success_nthI [success_intros]:
-  "i < length a h \<Longrightarrow> success (nth a i) h"
+  "i < length h a \<Longrightarrow> success (nth a i) h"
   by (auto intro: success_intros simp add: nth_def)
 
 lemma crel_nthI [crel_intros]:
-  assumes "i < length a h" "h' = h" "r = get_array a h ! i"
+  assumes "i < length h a" "h' = h" "r = get_array a h ! 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 a h" "r = get_array a h ! i" "h' = h"
+  obtains "i < length h a" "r = get_array a h ! i" "h' = h"
   using assms by (rule crelE)
-    (erule successE, cases "i < length a h", simp_all add: execute_simps)
+    (erule successE, cases "i < length h a", simp_all add: execute_simps)
 
 lemma execute_upd [execute_simps]:
-  "i < length a h \<Longrightarrow>
+  "i < length h a \<Longrightarrow>
     execute (upd i x a) h = Some (a, update a i x h)"
-  "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
+  "i \<ge> length h a \<Longrightarrow> execute (upd i x a) h = None"
   by (simp_all add: upd_def execute_simps)
 
 lemma success_updI [success_intros]:
-  "i < length a h \<Longrightarrow> success (upd i x a) h"
+  "i < length h a \<Longrightarrow> success (upd i x a) h"
   by (auto intro: success_intros simp add: upd_def)
 
 lemma crel_updI [crel_intros]:
-  assumes "i < length a h" "h' = update a i v h"
+  assumes "i < length h a" "h' = update a i v h"
   shows "crel (upd i v a) h h' a"
   by (rule crelI) (insert assms, simp add: execute_simps)
 
 lemma crel_updE [crel_elims]:
   assumes "crel (upd i v a) h h' r"
-  obtains "r = a" "h' = update a i v h" "i < length a h"
+  obtains "r = a" "h' = update a i v h" "i < length h a"
   using assms by (rule crelE)
-    (erule successE, cases "i < length a h", simp_all add: execute_simps)
+    (erule successE, cases "i < length h a", simp_all add: execute_simps)
 
 lemma execute_map_entry [execute_simps]:
-  "i < length a h \<Longrightarrow>
+  "i < length h a \<Longrightarrow>
    execute (map_entry i f a) h =
       Some (a, update a i (f (get_array a h ! i)) h)"
-  "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
+  "i \<ge> length h a \<Longrightarrow> execute (map_entry i f a) h = None"
   by (simp_all add: map_entry_def execute_simps)
 
 lemma success_map_entryI [success_intros]:
-  "i < length a h \<Longrightarrow> success (map_entry i f a) h"
+  "i < length h a \<Longrightarrow> success (map_entry i f a) h"
   by (auto intro: success_intros simp add: map_entry_def)
 
 lemma crel_map_entryI [crel_intros]:
-  assumes "i < length a h" "h' = update a i (f (get_array a h ! i)) h" "r = a"
+  assumes "i < length h a" "h' = update a i (f (get_array a h ! 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 a h"
+  obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length h a"
   using assms by (rule crelE)
-    (erule successE, cases "i < length a h", simp_all add: execute_simps)
+    (erule successE, cases "i < length h a", simp_all add: execute_simps)
 
 lemma execute_swap [execute_simps]:
-  "i < length a h \<Longrightarrow>
+  "i < length h a \<Longrightarrow>
    execute (swap i x a) h =
       Some (get_array a h ! i, update a i x h)"
-  "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
+  "i \<ge> length h a \<Longrightarrow> execute (swap i x a) h = None"
   by (simp_all add: swap_def execute_simps)
 
 lemma success_swapI [success_intros]:
-  "i < length a h \<Longrightarrow> success (swap i x a) h"
+  "i < length h a \<Longrightarrow> success (swap i x a) h"
   by (auto intro: success_intros simp add: swap_def)
 
 lemma crel_swapI [crel_intros]:
-  assumes "i < length a h" "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_array a h ! 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 a h"
+  obtains "r = get_array a h ! i" "h' = update a i x h" "i < length h a"
   using assms by (rule crelE)
-    (erule successE, cases "i < length a h", simp_all add: execute_simps)
+    (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)"
@@ -428,12 +427,12 @@
 proof (rule Heap_eqI)
   fix h
   have *: "List.map
-     (\<lambda>x. fst (the (if x < length a h
+     (\<lambda>x. fst (the (if x < length h a
                     then Some (get_array a h ! x, h) else None)))
-     [0..<length a h] =
-       List.map (List.nth (get_array a h)) [0..<length a h]"
+     [0..<length h a] =
+       List.map (List.nth (get_array a h)) [0..<length h a]"
     by simp
-  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
+  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length h a]) h =
     Some (get_array a h, h)"
     apply (subst execute_fold_map_unchanged_heap)
     apply (simp_all add: nth_def guard_def *)
diff -r 868ceaa6b039 -r f2e9c104cebd src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 11:23:21 2010 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 15:34:02 2010 +0200
@@ -239,7 +239,7 @@
   by (simp add: Array.update_def get_array_def set_array_def set_def)
 
 lemma length_alloc [simp]: 
-  "Array.length a (snd (alloc v h)) = Array.length a h"
+  "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)
 
 lemma get_array_alloc [simp]: 
diff -r 868ceaa6b039 -r f2e9c104cebd src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 11:23:21 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 15:34:02 2010 +0200
@@ -22,7 +22,7 @@
      }"
 
 lemma crel_swapI [crel_intros]:
-  assumes "i < Array.length a h" "j < Array.length a h"
+  assumes "i < Array.length h a" "j < Array.length h a"
     "x = get_array a h ! i" "y = get_array a h ! j"
     "h' = Array.update a j x (Array.update a i y h)"
   shows "crel (swap a i j) h h' r"
@@ -108,7 +108,7 @@
 
 lemma part_length_remains:
   assumes "crel (part1 a l r p) h h' rs"
-  shows "Array.length a h = Array.length a h'"
+  shows "Array.length h a = Array.length 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)
@@ -250,7 +250,7 @@
 
 lemma partition_length_remains:
   assumes "crel (partition a l r) h h' rs"
-  shows "Array.length a h = Array.length a h'"
+  shows "Array.length h a = Array.length h' a"
 proof -
   from assms part_length_remains show ?thesis
     unfolding partition.simps swap_def
@@ -298,10 +298,10 @@
     (Array.update a rs (get_array a h1 ! r) h1)"
     unfolding swap_def
     by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
-  from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
+  from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
     unfolding swap_def
     by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
-  from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
+  from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
     unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
   from `l < r` have "l \<le> r - 1" by simp
   note middle_in_bounds = part_returns_index_in_bounds[OF part this]
@@ -321,7 +321,7 @@
       fix i
       assume i_is_left: "l \<le> i \<and> i < rs"
       with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
-      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+      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
@@ -338,7 +338,7 @@
       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 a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+        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"
           by fastsimp
@@ -364,7 +364,7 @@
       fix i
       assume i_is_left: "l \<le> i \<and> i < rs"
       with swap_length_remains in_bounds middle_in_bounds rs_equals
-      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+      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"
@@ -379,7 +379,7 @@
       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 a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+        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"
           by fastsimp
@@ -432,7 +432,7 @@
 
 lemma length_remains:
   assumes "crel (quicksort a l r) h h' rs"
-  shows "Array.length a h = Array.length a h'"
+  shows "Array.length h a = Array.length h' a"
 using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
@@ -489,7 +489,7 @@
  
 lemma quicksort_sorts:
   assumes "crel (quicksort a l r) h h' rs"
-  assumes l_r_length: "l < Array.length a h" "r < Array.length a h" 
+  assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
   shows "sorted (subarray l (r + 1) a h')"
   using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
@@ -563,7 +563,7 @@
 
 
 lemma quicksort_is_sort:
-  assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
+  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 = []")
   case True
@@ -583,7 +583,7 @@
 We will now show that exceptions do not occur. *}
 
 lemma success_part1I: 
-  assumes "l < Array.length a h" "r < Array.length a h"
+  assumes "l < Array.length h a" "r < Array.length h a"
   shows "success (part1 a l r p) h"
   using assms
 proof (induct a l r p arbitrary: h rule: part1.induct)
@@ -606,7 +606,7 @@
 qed
 
 lemma success_partitionI:
-  assumes "l < r" "l < Array.length a h" "r < Array.length a h"
+  assumes "l < r" "l < Array.length h a" "r < Array.length h a"
   shows "success (partition a l r) h"
 using assms unfolding partition.simps swap_def
 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:)
@@ -621,7 +621,7 @@
 done
 
 lemma success_quicksortI:
-  assumes "l < Array.length a h" "r < Array.length a h"
+  assumes "l < Array.length h a" "r < Array.length h a"
   shows "success (quicksort a l r) h"
 using assms
 proof (induct a l r arbitrary: h rule: quicksort.induct)
diff -r 868ceaa6b039 -r f2e9c104cebd src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 11:23:21 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 15:34:02 2010 +0200
@@ -64,7 +64,7 @@
 
 lemma rev_length:
   assumes "crel (rev a i j) h h' r"
-  shows "Array.length a h = Array.length a h'"
+  shows "Array.length h a = Array.length h' a"
 using assms
 proof (induct a i j arbitrary: h h' rule: rev.induct)
   case (1 a i j h h'')
@@ -88,7 +88,7 @@
 qed
 
 lemma rev2_rev': assumes "crel (rev a i j) h h' u"
-  assumes "j < Array.length a h"
+  assumes "j < Array.length h a"
   shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
 proof - 
   {
@@ -103,10 +103,10 @@
 qed
 
 lemma rev2_rev: 
-  assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
+  assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
   shows "get_array a h' = List.rev (get_array a h)"
   using rev2_rev'[OF assms] rev_length[OF assms] assms
-    by (cases "Array.length a h = 0", auto simp add: Array.length_def
+    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)
 
diff -r 868ceaa6b039 -r f2e9c104cebd src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 11:23:21 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 15:34:02 2010 +0200
@@ -123,7 +123,7 @@
   "array_ran a h = {e. Some e \<in> set (get_array a h)}"
     -- {*FIXME*}
 
-lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
+lemma array_ranI: "\<lbrakk> Some b = get_array a h ! 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:
@@ -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 a h'"
+    assume "h = h'" "Some clj = get_array a h' ! 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 a h"
+    assume "Some clj = get_array a h ! 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 868ceaa6b039 -r f2e9c104cebd src/HOL/Imperative_HOL/ex/Subarray.thy
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 11:23:21 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 15:34:02 2010 +0200
@@ -30,20 +30,20 @@
 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 a h \<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 = [get_array a h ! n]" 
 by (simp add: subarray_def length_def sublist'_single)
 
-lemma length_subarray: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
+lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
 by (simp add: subarray_def length_def length_sublist')
 
-lemma length_subarray_0: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
+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 a h; 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> (get_array a h ! 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 a h\<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 @ [get_array a h ! (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 a h) a h = get_array a h"
+lemma subarray_all: "subarray 0 (Array.length h a) a h = get_array a h"
 unfolding Array.length_def subarray_def
 by (simp add: sublist'_all)
 
-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)"
+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)"
 unfolding Array.length_def subarray_def
 by (simp add: nth_sublist')
 
-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')"
+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')"
 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 a h \<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 (get_array a h ! 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 a h \<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 (get_array a h ! k))"
 unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
 
 end
\ No newline at end of file