1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Jul 05 15:36:37 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Jul 05 16:46:23 2010 +0200
1.3 @@ -27,7 +27,7 @@
1.4 = multiset_of (get_array a h)"
1.5 using assms
1.6 unfolding swap_def
1.7 - by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
1.8 + by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
1.9
1.10 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
1.11 where
1.12 @@ -101,7 +101,7 @@
1.13
1.14 lemma part_length_remains:
1.15 assumes "crel (part1 a l r p) h h' rs"
1.16 - shows "Heap.length a h = Heap.length a h'"
1.17 + shows "Array.length a h = Array.length a h'"
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 @@ -207,7 +207,7 @@
1.22 by (elim crelE crel_nth crel_if crel_return) auto
1.23 from swp False have "get_array a h1 ! r \<ge> p"
1.24 unfolding swap_def
1.25 - by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
1.26 + by (auto simp add: Array.length_def elim!: crelE crel_nth crel_upd crel_return)
1.27 with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
1.28 by fastsimp
1.29 have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
1.30 @@ -243,7 +243,7 @@
1.31
1.32 lemma partition_length_remains:
1.33 assumes "crel (partition a l r) h h' rs"
1.34 - shows "Heap.length a h = Heap.length a h'"
1.35 + shows "Array.length a h = Array.length a h'"
1.36 proof -
1.37 from assms part_length_remains show ?thesis
1.38 unfolding partition.simps swap_def
1.39 @@ -287,14 +287,14 @@
1.40 else middle)"
1.41 unfolding partition.simps
1.42 by (elim crelE crel_return crel_nth crel_if crel_upd) simp
1.43 - from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
1.44 - (Heap.upd a rs (get_array a h1 ! r) h1)"
1.45 + from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
1.46 + (Array.change a rs (get_array a h1 ! r) h1)"
1.47 unfolding swap_def
1.48 by (elim crelE crel_return crel_nth crel_upd) simp
1.49 - from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
1.50 + from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
1.51 unfolding swap_def
1.52 by (elim crelE crel_return crel_nth crel_upd) simp
1.53 - from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
1.54 + from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
1.55 unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
1.56 from `l < r` have "l \<le> r - 1" by simp
1.57 note middle_in_bounds = part_returns_index_in_bounds[OF part this]
1.58 @@ -304,7 +304,7 @@
1.59 with swap
1.60 have right_remains: "get_array a h ! r = get_array a h' ! rs"
1.61 unfolding swap_def
1.62 - by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
1.63 + by (auto simp add: Array.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
1.64 from part_partitions [OF part]
1.65 show ?thesis
1.66 proof (cases "get_array a h1 ! middle \<le> ?pivot")
1.67 @@ -314,12 +314,12 @@
1.68 fix i
1.69 assume i_is_left: "l \<le> i \<and> i < rs"
1.70 with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
1.71 - have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.72 + have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.73 from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
1.74 with part_partitions[OF part] right_remains True
1.75 have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
1.76 with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
1.77 - unfolding Heap.upd_def Heap.length_def by simp
1.78 + unfolding Array.change_def Array.length_def by simp
1.79 }
1.80 moreover
1.81 {
1.82 @@ -331,7 +331,7 @@
1.83 proof
1.84 assume i_is: "rs < i \<and> i \<le> r - 1"
1.85 with swap_length_remains in_bounds middle_in_bounds rs_equals
1.86 - have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.87 + have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.88 from part_partitions[OF part] rs_equals right_remains i_is
1.89 have "get_array a h' ! rs \<le> get_array a h1 ! i"
1.90 by fastsimp
1.91 @@ -345,7 +345,7 @@
1.92 by fastsimp
1.93 with i_is True rs_equals right_remains h'_def
1.94 show ?thesis using in_bounds
1.95 - unfolding Heap.upd_def Heap.length_def
1.96 + unfolding Array.change_def Array.length_def
1.97 by auto
1.98 qed
1.99 }
1.100 @@ -357,11 +357,11 @@
1.101 fix i
1.102 assume i_is_left: "l \<le> i \<and> i < rs"
1.103 with swap_length_remains in_bounds middle_in_bounds rs_equals
1.104 - have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.105 + have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.106 from part_partitions[OF part] rs_equals right_remains i_is_left
1.107 have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
1.108 with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
1.109 - unfolding Heap.upd_def by simp
1.110 + unfolding Array.change_def by simp
1.111 }
1.112 moreover
1.113 {
1.114 @@ -372,7 +372,7 @@
1.115 proof
1.116 assume i_is: "rs < i \<and> i \<le> r - 1"
1.117 with swap_length_remains in_bounds middle_in_bounds rs_equals
1.118 - have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.119 + have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.120 from part_partitions[OF part] rs_equals right_remains i_is
1.121 have "get_array a h' ! rs \<le> get_array a h1 ! i"
1.122 by fastsimp
1.123 @@ -381,7 +381,7 @@
1.124 assume i_is: "i = r"
1.125 from i_is False rs_equals right_remains h'_def
1.126 show ?thesis using in_bounds
1.127 - unfolding Heap.upd_def Heap.length_def
1.128 + unfolding Array.change_def Array.length_def
1.129 by auto
1.130 qed
1.131 }
1.132 @@ -425,7 +425,7 @@
1.133
1.134 lemma length_remains:
1.135 assumes "crel (quicksort a l r) h h' rs"
1.136 - shows "Heap.length a h = Heap.length a h'"
1.137 + shows "Array.length a h = Array.length a h'"
1.138 using assms
1.139 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.140 case (1 a l r h h' rs)
1.141 @@ -482,7 +482,7 @@
1.142
1.143 lemma quicksort_sorts:
1.144 assumes "crel (quicksort a l r) h h' rs"
1.145 - assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h"
1.146 + assumes l_r_length: "l < Array.length a h" "r < Array.length a h"
1.147 shows "sorted (subarray l (r + 1) a h')"
1.148 using assms
1.149 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.150 @@ -524,7 +524,7 @@
1.151 from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
1.152 length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
1.153 have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
1.154 - unfolding Heap.length_def subarray_def by (cases p, auto)
1.155 + unfolding Array.length_def subarray_def by (cases p, auto)
1.156 with left_subarray_remains part_conds1 pivot_unchanged
1.157 have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
1.158 by (simp, subst set_of_multiset_of[symmetric], simp)
1.159 @@ -535,7 +535,7 @@
1.160 from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
1.161 length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
1.162 have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
1.163 - unfolding Heap.length_def subarray_def by auto
1.164 + unfolding Array.length_def subarray_def by auto
1.165 with right_subarray_remains part_conds2 pivot_unchanged
1.166 have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
1.167 by (simp, subst set_of_multiset_of[symmetric], simp)
1.168 @@ -556,18 +556,18 @@
1.169
1.170
1.171 lemma quicksort_is_sort:
1.172 - assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
1.173 + assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
1.174 shows "get_array a h' = sort (get_array a h)"
1.175 proof (cases "get_array a h = []")
1.176 case True
1.177 with quicksort_is_skip[OF crel] show ?thesis
1.178 - unfolding Heap.length_def by simp
1.179 + unfolding Array.length_def by simp
1.180 next
1.181 case False
1.182 from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
1.183 - unfolding Heap.length_def subarray_def by auto
1.184 + unfolding Array.length_def subarray_def by auto
1.185 with length_remains[OF crel] have "sorted (get_array a h')"
1.186 - unfolding Heap.length_def by simp
1.187 + unfolding Array.length_def by simp
1.188 with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
1.189 qed
1.190
1.191 @@ -576,7 +576,7 @@
1.192 We will now show that exceptions do not occur. *}
1.193
1.194 lemma noError_part1:
1.195 - assumes "l < Heap.length a h" "r < Heap.length a h"
1.196 + assumes "l < Array.length a h" "r < Array.length a h"
1.197 shows "noError (part1 a l r p) h"
1.198 using assms
1.199 proof (induct a l r p arbitrary: h rule: part1.induct)
1.200 @@ -587,7 +587,7 @@
1.201 qed
1.202
1.203 lemma noError_partition:
1.204 - assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
1.205 + assumes "l < r" "l < Array.length a h" "r < Array.length a h"
1.206 shows "noError (partition a l r) h"
1.207 using assms
1.208 unfolding partition.simps swap_def
1.209 @@ -603,7 +603,7 @@
1.210 done
1.211
1.212 lemma noError_quicksort:
1.213 - assumes "l < Heap.length a h" "r < Heap.length a h"
1.214 + assumes "l < Array.length a h" "r < Array.length a h"
1.215 shows "noError (quicksort a l r) h"
1.216 using assms
1.217 proof (induct a l r arbitrary: h rule: quicksort.induct)
1.218 @@ -628,7 +628,7 @@
1.219 subsection {* Example *}
1.220
1.221 definition "qsort a = do
1.222 - k \<leftarrow> length a;
1.223 + k \<leftarrow> len a;
1.224 quicksort a 0 (k - 1);
1.225 return a
1.226 done"