src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 32960 69916a850301
parent 31887 b662352477c6
child 35041 6eb917794a5c
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -153,8 +153,8 @@
     1.4          by (elim crelE crel_nth crel_if crel_return) auto
     1.5        from swp rec_condition have
     1.6          "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
     1.7 -	unfolding swap_def
     1.8 -	by (elim crelE crel_nth crel_upd crel_return) auto
     1.9 +        unfolding swap_def
    1.10 +        by (elim crelE crel_nth crel_upd crel_return) auto
    1.11        with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
    1.12      qed
    1.13    qed
    1.14 @@ -190,10 +190,10 @@
    1.15          unfolding part1.simps[of a l r p]
    1.16          by (elim crelE crel_nth crel_if crel_return) auto
    1.17        from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
    1.18 -	by fastsimp
    1.19 +        by fastsimp
    1.20        have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
    1.21        with 1(1)[OF False True rec1] a_l show ?thesis
    1.22 -	by auto
    1.23 +        by auto
    1.24      next
    1.25        case False
    1.26        with lr cr
    1.27 @@ -202,13 +202,13 @@
    1.28          unfolding part1.simps[of a l r p]
    1.29          by (elim crelE crel_nth crel_if crel_return) auto
    1.30        from swp False have "get_array a h1 ! r \<ge> p"
    1.31 -	unfolding swap_def
    1.32 -	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
    1.33 +        unfolding swap_def
    1.34 +        by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
    1.35        with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
    1.36 -	by fastsimp
    1.37 +        by fastsimp
    1.38        have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
    1.39        with 1(2)[OF lr False rec2] a_r show ?thesis
    1.40 -	by auto
    1.41 +        by auto
    1.42      qed
    1.43    qed
    1.44  qed
    1.45 @@ -315,7 +315,7 @@
    1.46        with part_partitions[OF part] right_remains True
    1.47        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    1.48        with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
    1.49 -	unfolding Heap.upd_def Heap.length_def by simp
    1.50 +        unfolding Heap.upd_def Heap.length_def by simp
    1.51      }
    1.52      moreover
    1.53      {
    1.54 @@ -325,24 +325,24 @@
    1.55        hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
    1.56        hence "get_array a h' ! rs \<le> get_array a h' ! i"
    1.57        proof
    1.58 -	assume i_is: "rs < i \<and> i \<le> r - 1"
    1.59 -	with swap_length_remains in_bounds middle_in_bounds rs_equals
    1.60 -	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    1.61 -	from part_partitions[OF part] rs_equals right_remains i_is
    1.62 -	have "get_array a h' ! rs \<le> get_array a h1 ! i"
    1.63 -	  by fastsimp
    1.64 -	with i_props h'_def show ?thesis by fastsimp
    1.65 +        assume i_is: "rs < i \<and> i \<le> r - 1"
    1.66 +        with swap_length_remains in_bounds middle_in_bounds rs_equals
    1.67 +        have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
    1.68 +        from part_partitions[OF part] rs_equals right_remains i_is
    1.69 +        have "get_array a h' ! rs \<le> get_array a h1 ! i"
    1.70 +          by fastsimp
    1.71 +        with i_props h'_def show ?thesis by fastsimp
    1.72        next
    1.73 -	assume i_is: "rs < i \<and> i = r"
    1.74 -	with rs_equals have "Suc middle \<noteq> r" by arith
    1.75 -	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
    1.76 -	with part_partitions[OF part] right_remains 
    1.77 -	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
    1.78 -	  by fastsimp
    1.79 -	with i_is True rs_equals right_remains h'_def
    1.80 -	show ?thesis using in_bounds
    1.81 -	  unfolding Heap.upd_def Heap.length_def
    1.82 -	  by auto
    1.83 +        assume i_is: "rs < i \<and> i = r"
    1.84 +        with rs_equals have "Suc middle \<noteq> r" by arith
    1.85 +        with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
    1.86 +        with part_partitions[OF part] right_remains 
    1.87 +        have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
    1.88 +          by fastsimp
    1.89 +        with i_is True rs_equals right_remains h'_def
    1.90 +        show ?thesis using in_bounds
    1.91 +          unfolding Heap.upd_def Heap.length_def
    1.92 +          by auto
    1.93        qed
    1.94      }
    1.95      ultimately show ?thesis by auto
    1.96 @@ -357,7 +357,7 @@
    1.97        from part_partitions[OF part] rs_equals right_remains i_is_left
    1.98        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    1.99        with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
   1.100 -	unfolding Heap.upd_def by simp
   1.101 +        unfolding Heap.upd_def by simp
   1.102      }
   1.103      moreover
   1.104      {
   1.105 @@ -366,19 +366,19 @@
   1.106        hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
   1.107        hence "get_array a h' ! rs \<le> get_array a h' ! i"
   1.108        proof
   1.109 -	assume i_is: "rs < i \<and> i \<le> r - 1"
   1.110 -	with swap_length_remains in_bounds middle_in_bounds rs_equals
   1.111 -	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   1.112 -	from part_partitions[OF part] rs_equals right_remains i_is
   1.113 -	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   1.114 -	  by fastsimp
   1.115 -	with i_props h'_def show ?thesis by fastsimp
   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 +        from part_partitions[OF part] rs_equals right_remains i_is
   1.120 +        have "get_array a h' ! rs \<le> get_array a h1 ! i"
   1.121 +          by fastsimp
   1.122 +        with i_props h'_def show ?thesis by fastsimp
   1.123        next
   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 -	  by auto
   1.129 +        assume i_is: "i = r"
   1.130 +        from i_is False rs_equals right_remains h'_def
   1.131 +        show ?thesis using in_bounds
   1.132 +          unfolding Heap.upd_def Heap.length_def
   1.133 +          by auto
   1.134        qed
   1.135      }
   1.136      ultimately
   1.137 @@ -507,7 +507,7 @@
   1.138        have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
   1.139        from quicksort_outer_remains [OF qs2] length_remains
   1.140        have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
   1.141 -	by (simp add: subarray_eq_samelength_iff)
   1.142 +        by (simp add: subarray_eq_samelength_iff)
   1.143        with IH1 have IH1': "sorted (subarray l p a h')" by simp
   1.144        from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
   1.145        have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
   1.146 @@ -520,14 +520,14 @@
   1.147        from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
   1.148          length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
   1.149        have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
   1.150 -	unfolding Heap.length_def subarray_def by (cases p, auto)
   1.151 +        unfolding Heap.length_def subarray_def by (cases p, auto)
   1.152        with left_subarray_remains part_conds1 pivot_unchanged
   1.153        have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
   1.154          by (simp, subst set_of_multiset_of[symmetric], simp)
   1.155            (* -- These steps are the analogous for the right sublist \<dots> *)
   1.156        from quicksort_outer_remains [OF qs1] length_remains
   1.157        have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
   1.158 -	by (auto simp add: subarray_eq_samelength_iff)
   1.159 +        by (auto simp add: subarray_eq_samelength_iff)
   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 @@ -538,11 +538,11 @@
   1.164            (* -- Thirdly and finally, we show that the array is sorted
   1.165            following from the facts above. *)
   1.166        from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [get_array a h' ! p] @ subarray (p + 1) (r + 1) a h'"
   1.167 -	by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
   1.168 +        by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
   1.169        with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
   1.170 -	unfolding subarray_def
   1.171 -	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
   1.172 -	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
   1.173 +        unfolding subarray_def
   1.174 +        apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
   1.175 +        by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
   1.176      }
   1.177      with True cr show ?thesis
   1.178        unfolding quicksort.simps [of a l r]