author haftmann Wed, 27 Aug 2008 11:24:31 +0200 changeset 28013 e892cedcd638 parent 28012 2308843f8b66 child 28014 fe36718702aa
untabification
```--- a/src/HOL/ex/ImperativeQuicksort.thy	Wed Aug 27 11:24:29 2008 +0200
+++ b/src/HOL/ex/ImperativeQuicksort.thy	Wed Aug 27 11:24:31 2008 +0200
@@ -151,7 +151,7 @@
unfolding part1.simps[of a l r p] run_drop
by (elim crelE crel_nth crel_if crel_return) auto
from swp rec_condition have
-	"\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
+        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
unfolding swap_def run_drop
by (elim crelE crel_nth crel_upd crel_return) auto
with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
@@ -501,7 +501,7 @@
note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
-	(*-- First of all, by induction hypothesis both sublists are sorted. *)
+        (*-- First of all, by induction hypothesis both sublists are sorted. *)
from 1(1)[OF True pivot qs1] length_remains pivot 1(5)
have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
from quicksort_outer_remains [OF qs2] length_remains
@@ -510,32 +510,32 @@
with IH1 have IH1': "sorted (subarray l p a h')" by simp
from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
-	by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
-	  (* -- Secondly, both sublists remain partitioned. *)
+        by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
+           (* -- Secondly, both sublists remain partitioned. *)
from partition_partitions[OF part True]
have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
-	and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
-	by (auto simp add: all_in_set_subarray_conv)
+        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
+        by (auto simp add: all_in_set_subarray_conv)
from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
-	length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
+        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
unfolding Heap.length_def subarray_def by (cases p, auto)
with left_subarray_remains part_conds1 pivot_unchanged
have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
-	by (simp, subst set_of_multiset_of[symmetric], simp)
-	  (* -- These steps are the analogous for the right sublist \<dots> *)
+        by (simp, subst set_of_multiset_of[symmetric], simp)
+          (* -- These steps are the analogous for the right sublist \<dots> *)
from quicksort_outer_remains [OF qs1] length_remains
have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
-	length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
+        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
-	unfolding Heap.length_def subarray_def by auto
+        unfolding Heap.length_def subarray_def by auto
with right_subarray_remains part_conds2 pivot_unchanged
have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
-	by (simp, subst set_of_multiset_of[symmetric], simp)
-	  (* -- Thirdly and finally, we show that the array is sorted
-	  following from the facts above. *)
+        by (simp, subst set_of_multiset_of[symmetric], simp)
+          (* -- Thirdly and finally, we show that the array is sorted
+          following from the facts above. *)
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'"
by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis```