src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 44890 22f665a2e91c
parent 41413 64cd30d6b0b8
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4          unfolding part1.simps[of a l r p]
     1.5          by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
     1.6        from rec_condition have "l \<le> r - 1" by arith
     1.7 -      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
     1.8 +      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastforce
     1.9      qed
    1.10    qed
    1.11  qed
    1.12 @@ -128,7 +128,7 @@
    1.13      case False (* recursive case *)
    1.14      with cr 1 show ?thesis
    1.15        unfolding part1.simps [of a l r p] swap_def
    1.16 -      by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastsimp
    1.17 +      by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastforce
    1.18    qed
    1.19  qed
    1.20  
    1.21 @@ -158,7 +158,7 @@
    1.22          unfolding part1.simps[of a l r p]
    1.23          by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
    1.24        from 1(1)[OF rec_condition True rec1]
    1.25 -      show ?thesis by fastsimp
    1.26 +      show ?thesis by fastforce
    1.27      next
    1.28        case False
    1.29        with rec_condition cr
    1.30 @@ -170,7 +170,7 @@
    1.31          "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
    1.32          unfolding swap_def
    1.33          by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
    1.34 -      with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
    1.35 +      with 1(2) [OF rec_condition False rec2] show ?thesis by fastforce
    1.36      qed
    1.37    qed
    1.38  qed
    1.39 @@ -205,7 +205,7 @@
    1.40          unfolding part1.simps[of a l r p]
    1.41          by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
    1.42        from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
    1.43 -        by fastsimp
    1.44 +        by fastforce
    1.45        have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
    1.46        with 1(1)[OF False True rec1] a_l show ?thesis
    1.47          by auto
    1.48 @@ -220,7 +220,7 @@
    1.49          unfolding swap_def
    1.50          by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
    1.51        with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
    1.52 -        by fastsimp
    1.53 +        by fastforce
    1.54        have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
    1.55        with 1(2)[OF lr False rec2] a_r show ?thesis
    1.56          by auto
    1.57 @@ -268,7 +268,7 @@
    1.58  proof -
    1.59    from assms part_outer_remains part_returns_index_in_bounds show ?thesis
    1.60      unfolding partition.simps swap_def
    1.61 -    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastsimp
    1.62 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce
    1.63  qed
    1.64  
    1.65  lemma partition_returns_index_in_bounds:
    1.66 @@ -311,7 +311,7 @@
    1.67    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
    1.68    from part_outer_remains[OF part] `l < r`
    1.69    have "Array.get h a ! r = Array.get h1 a ! r"
    1.70 -    by fastsimp
    1.71 +    by fastforce
    1.72    with swap
    1.73    have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
    1.74      unfolding swap_def
    1.75 @@ -328,7 +328,7 @@
    1.76        have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    1.77        from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
    1.78        with part_partitions[OF part] right_remains True
    1.79 -      have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp
    1.80 +      have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastforce
    1.81        with i_props h'_def in_bounds have "Array.get h' a ! i \<le> Array.get h' a ! rs"
    1.82          unfolding Array.update_def Array.length_def by simp
    1.83      }
    1.84 @@ -345,15 +345,15 @@
    1.85          have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
    1.86          from part_partitions[OF part] rs_equals right_remains i_is
    1.87          have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
    1.88 -          by fastsimp
    1.89 -        with i_props h'_def show ?thesis by fastsimp
    1.90 +          by fastforce
    1.91 +        with i_props h'_def show ?thesis by fastforce
    1.92        next
    1.93          assume i_is: "rs < i \<and> i = r"
    1.94          with rs_equals have "Suc middle \<noteq> r" by arith
    1.95          with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
    1.96          with part_partitions[OF part] right_remains 
    1.97          have "Array.get h' a ! rs \<le> Array.get h1 a ! (Suc middle)"
    1.98 -          by fastsimp
    1.99 +          by fastforce
   1.100          with i_is True rs_equals right_remains h'_def
   1.101          show ?thesis using in_bounds
   1.102            unfolding Array.update_def Array.length_def
   1.103 @@ -370,7 +370,7 @@
   1.104        with swap_length_remains in_bounds middle_in_bounds rs_equals
   1.105        have i_props: "i < Array.length h' a" "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 "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp
   1.108 +      have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastforce
   1.109        with i_props h'_def have "Array.get h' a ! i \<le> Array.get h' a ! rs"
   1.110          unfolding Array.update_def by simp
   1.111      }
   1.112 @@ -386,8 +386,8 @@
   1.113          have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
   1.114          from part_partitions[OF part] rs_equals right_remains i_is
   1.115          have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
   1.116 -          by fastsimp
   1.117 -        with i_props h'_def show ?thesis by fastsimp
   1.118 +          by fastforce
   1.119 +        with i_props h'_def show ?thesis by fastforce
   1.120        next
   1.121          assume i_is: "i = r"
   1.122          from i_is False rs_equals right_remains h'_def
   1.123 @@ -469,7 +469,7 @@
   1.124        assume pivot: "l \<le> p \<and> p \<le> r"
   1.125        assume i_outer: "i < l \<or> r < i"
   1.126        from  partition_outer_remains [OF part True] i_outer
   1.127 -      have "Array.get h a !i = Array.get h1 a ! i" by fastsimp
   1.128 +      have "Array.get h a !i = Array.get h1 a ! i" by fastforce
   1.129        moreover
   1.130        with 1(1) [OF True pivot qs1] pivot i_outer
   1.131        have "Array.get h1 a ! i = Array.get h2 a ! i" by auto
   1.132 @@ -579,7 +579,7 @@
   1.133      unfolding Array.length_def subarray_def by auto
   1.134    with length_remains[OF effect] have "sorted (Array.get h' a)"
   1.135      unfolding Array.length_def by simp
   1.136 -  with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastsimp
   1.137 +  with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastforce
   1.138  qed
   1.139  
   1.140  subsection {* No Errors in quicksort *}