src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
 changeset 37802 f2e9c104cebd parent 37798 0b0570445a2a child 37805 0f797d586ce5
```     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 11:23:21 2010 +0100
1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 15:34:02 2010 +0200
1.3 @@ -22,7 +22,7 @@
1.4       }"
1.5
1.6  lemma crel_swapI [crel_intros]:
1.7 -  assumes "i < Array.length a h" "j < Array.length a h"
1.8 +  assumes "i < Array.length h a" "j < Array.length h a"
1.9      "x = get_array a h ! i" "y = get_array a h ! j"
1.10      "h' = Array.update a j x (Array.update a i y h)"
1.11    shows "crel (swap a i j) h h' r"
1.12 @@ -108,7 +108,7 @@
1.13
1.14  lemma part_length_remains:
1.15    assumes "crel (part1 a l r p) h h' rs"
1.16 -  shows "Array.length a h = Array.length a h'"
1.17 +  shows "Array.length h a = Array.length h' a"
1.18  using assms
1.19  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.20    case (1 a l r p h h' rs)
1.21 @@ -250,7 +250,7 @@
1.22
1.23  lemma partition_length_remains:
1.24    assumes "crel (partition a l r) h h' rs"
1.25 -  shows "Array.length a h = Array.length a h'"
1.26 +  shows "Array.length h a = Array.length h' a"
1.27  proof -
1.28    from assms part_length_remains show ?thesis
1.29      unfolding partition.simps swap_def
1.30 @@ -298,10 +298,10 @@
1.31      (Array.update a rs (get_array a h1 ! r) h1)"
1.32      unfolding swap_def
1.33      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
1.34 -  from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
1.35 +  from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
1.36      unfolding swap_def
1.37      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
1.38 -  from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
1.39 +  from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
1.40      unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
1.41    from `l < r` have "l \<le> r - 1" by simp
1.42    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
1.43 @@ -321,7 +321,7 @@
1.44        fix i
1.45        assume i_is_left: "l \<le> i \<and> i < rs"
1.46        with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
1.47 -      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.48 +      have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
1.49        from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
1.50        with part_partitions[OF part] right_remains True
1.51        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
1.52 @@ -338,7 +338,7 @@
1.53        proof
1.54          assume i_is: "rs < i \<and> i \<le> r - 1"
1.55          with swap_length_remains in_bounds middle_in_bounds rs_equals
1.56 -        have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.57 +        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
1.58          from part_partitions[OF part] rs_equals right_remains i_is
1.59          have "get_array a h' ! rs \<le> get_array a h1 ! i"
1.60            by fastsimp
1.61 @@ -364,7 +364,7 @@
1.62        fix i
1.63        assume i_is_left: "l \<le> i \<and> i < rs"
1.64        with swap_length_remains in_bounds middle_in_bounds rs_equals
1.65 -      have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.66 +      have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
1.67        from part_partitions[OF part] rs_equals right_remains i_is_left
1.68        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
1.69        with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
1.70 @@ -379,7 +379,7 @@
1.71        proof
1.72          assume i_is: "rs < i \<and> i \<le> r - 1"
1.73          with swap_length_remains in_bounds middle_in_bounds rs_equals
1.74 -        have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.75 +        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
1.76          from part_partitions[OF part] rs_equals right_remains i_is
1.77          have "get_array a h' ! rs \<le> get_array a h1 ! i"
1.78            by fastsimp
1.79 @@ -432,7 +432,7 @@
1.80
1.81  lemma length_remains:
1.82    assumes "crel (quicksort a l r) h h' rs"
1.83 -  shows "Array.length a h = Array.length a h'"
1.84 +  shows "Array.length h a = Array.length h' a"
1.85  using assms
1.86  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.87    case (1 a l r h h' rs)
1.88 @@ -489,7 +489,7 @@
1.89
1.90  lemma quicksort_sorts:
1.91    assumes "crel (quicksort a l r) h h' rs"
1.92 -  assumes l_r_length: "l < Array.length a h" "r < Array.length a h"
1.93 +  assumes l_r_length: "l < Array.length h a" "r < Array.length h a"
1.94    shows "sorted (subarray l (r + 1) a h')"
1.95    using assms
1.96  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.97 @@ -563,7 +563,7 @@
1.98
1.99
1.100  lemma quicksort_is_sort:
1.101 -  assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
1.102 +  assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
1.103    shows "get_array a h' = sort (get_array a h)"
1.104  proof (cases "get_array a h = []")
1.105    case True
1.106 @@ -583,7 +583,7 @@
1.107  We will now show that exceptions do not occur. *}
1.108
1.109  lemma success_part1I:
1.110 -  assumes "l < Array.length a h" "r < Array.length a h"
1.111 +  assumes "l < Array.length h a" "r < Array.length h a"
1.112    shows "success (part1 a l r p) h"
1.113    using assms
1.114  proof (induct a l r p arbitrary: h rule: part1.induct)
1.115 @@ -606,7 +606,7 @@
1.116  qed
1.117
1.118  lemma success_partitionI:
1.119 -  assumes "l < r" "l < Array.length a h" "r < Array.length a h"
1.120 +  assumes "l < r" "l < Array.length h a" "r < Array.length h a"
1.121    shows "success (partition a l r) h"
1.122  using assms unfolding partition.simps swap_def
1.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:)
1.124 @@ -621,7 +621,7 @@
1.125  done
1.126
1.127  lemma success_quicksortI:
1.128 -  assumes "l < Array.length a h" "r < Array.length a h"
1.129 +  assumes "l < Array.length h a" "r < Array.length h a"
1.130    shows "success (quicksort a l r) h"
1.131  using assms
1.132  proof (induct a l r arbitrary: h rule: quicksort.induct)
```