src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
 changeset 37719 271ecd4fb9f9 parent 36098 53992c639da5 child 37750 82e0fe8b07eb
```     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"
```