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"