diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Sep 12 07:55:43 2011 +0200
@@ -105,7 +105,7 @@
unfolding part1.simps[of a l r p]
by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
from rec_condition have "l \ r - 1" by arith
- from 1(2) [OF rec_condition False rec2 `l \ r - 1`] show ?thesis by fastsimp
+ from 1(2) [OF rec_condition False rec2 `l \ r - 1`] show ?thesis by fastforce
qed
qed
qed
@@ -128,7 +128,7 @@
case False (* recursive case *)
with cr 1 show ?thesis
unfolding part1.simps [of a l r p] swap_def
- by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastsimp
+ by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastforce
qed
qed
@@ -158,7 +158,7 @@
unfolding part1.simps[of a l r p]
by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
from 1(1)[OF rec_condition True rec1]
- show ?thesis by fastsimp
+ show ?thesis by fastforce
next
case False
with rec_condition cr
@@ -170,7 +170,7 @@
"\i. i < l \ r < i \ Array.get h a ! i = Array.get h1 a ! i"
unfolding swap_def
by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
- with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
+ with 1(2) [OF rec_condition False rec2] show ?thesis by fastforce
qed
qed
qed
@@ -205,7 +205,7 @@
unfolding part1.simps[of a l r p]
by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \ p"
- by fastsimp
+ by fastforce
have "\i. (l \ i = (l = i \ Suc l \ i))" by arith
with 1(1)[OF False True rec1] a_l show ?thesis
by auto
@@ -220,7 +220,7 @@
unfolding swap_def
by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \ p"
- by fastsimp
+ by fastforce
have "\i. (i \ r = (i = r \ i \ r - 1))" by arith
with 1(2)[OF lr False rec2] a_r show ?thesis
by auto
@@ -268,7 +268,7 @@
proof -
from assms part_outer_remains part_returns_index_in_bounds show ?thesis
unfolding partition.simps swap_def
- by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastsimp
+ by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce
qed
lemma partition_returns_index_in_bounds:
@@ -311,7 +311,7 @@
note middle_in_bounds = part_returns_index_in_bounds[OF part this]
from part_outer_remains[OF part] `l < r`
have "Array.get h a ! r = Array.get h1 a ! r"
- by fastsimp
+ by fastforce
with swap
have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
unfolding swap_def
@@ -328,7 +328,7 @@
have i_props: "i < Array.length h' a" "i \ r" "i \ rs" by auto
from i_is_left rs_equals have "l \ i \ i < middle \ i = middle" by arith
with part_partitions[OF part] right_remains True
- have "Array.get h1 a ! i \ Array.get h' a ! rs" by fastsimp
+ have "Array.get h1 a ! i \ Array.get h' a ! rs" by fastforce
with i_props h'_def in_bounds have "Array.get h' a ! i \ Array.get h' a ! rs"
unfolding Array.update_def Array.length_def by simp
}
@@ -345,15 +345,15 @@
have i_props: "i < Array.length h' a" "i \ r" "i \ rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is
have "Array.get h' a ! rs \ Array.get h1 a ! i"
- by fastsimp
- with i_props h'_def show ?thesis by fastsimp
+ by fastforce
+ with i_props h'_def show ?thesis by fastforce
next
assume i_is: "rs < i \ i = r"
with rs_equals have "Suc middle \ r" by arith
with middle_in_bounds `l < r` have "Suc middle \ r - 1" by arith
with part_partitions[OF part] right_remains
have "Array.get h' a ! rs \ Array.get h1 a ! (Suc middle)"
- by fastsimp
+ by fastforce
with i_is True rs_equals right_remains h'_def
show ?thesis using in_bounds
unfolding Array.update_def Array.length_def
@@ -370,7 +370,7 @@
with swap_length_remains in_bounds middle_in_bounds rs_equals
have i_props: "i < Array.length h' a" "i \ r" "i \ rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is_left
- have "Array.get h1 a ! i \ Array.get h' a ! rs" by fastsimp
+ have "Array.get h1 a ! i \ Array.get h' a ! rs" by fastforce
with i_props h'_def have "Array.get h' a ! i \ Array.get h' a ! rs"
unfolding Array.update_def by simp
}
@@ -386,8 +386,8 @@
have i_props: "i < Array.length h' a" "i \ r" "i \ rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is
have "Array.get h' a ! rs \ Array.get h1 a ! i"
- by fastsimp
- with i_props h'_def show ?thesis by fastsimp
+ by fastforce
+ with i_props h'_def show ?thesis by fastforce
next
assume i_is: "i = r"
from i_is False rs_equals right_remains h'_def
@@ -469,7 +469,7 @@
assume pivot: "l \ p \ p \ r"
assume i_outer: "i < l \ r < i"
from partition_outer_remains [OF part True] i_outer
- have "Array.get h a !i = Array.get h1 a ! i" by fastsimp
+ have "Array.get h a !i = Array.get h1 a ! i" by fastforce
moreover
with 1(1) [OF True pivot qs1] pivot i_outer
have "Array.get h1 a ! i = Array.get h2 a ! i" by auto
@@ -579,7 +579,7 @@
unfolding Array.length_def subarray_def by auto
with length_remains[OF effect] have "sorted (Array.get h' a)"
unfolding Array.length_def by simp
- with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastsimp
+ with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastforce
qed
subsection {* No Errors in quicksort *}