# HG changeset patch
# User haftmann
# Date 1219829071 -7200
# Node ID e892cedcd6389aa940bb22c398a5774660310de2
# Parent  2308843f8b66f7b4fc9380e9121e4f38860aa028
untabification

diff -r 2308843f8b66 -r e892cedcd638 src/HOL/ex/ImperativeQuicksort.thy
--- 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"
 	by (auto simp add: subarray_eq_samelength_iff)
       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