1.1 --- a/src/HOL/ex/ImperativeQuicksort.thy	Wed Aug 27 11:24:29 2008 +0200
     1.2 +++ b/src/HOL/ex/ImperativeQuicksort.thy	Wed Aug 27 11:24:31 2008 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4          unfolding part1.simps[of a l r p] run_drop
     1.5          by (elim crelE crel_nth crel_if crel_return) auto
     1.6        from swp rec_condition have
     1.7 -	"\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
     1.8 +        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
     1.9  	unfolding swap_def run_drop
    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 @@ -501,7 +501,7 @@
    1.13       note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
    1.14        from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
    1.15        have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
    1.16 -	(*-- First of all, by induction hypothesis both sublists are sorted. *)
    1.17 +        (*-- First of all, by induction hypothesis both sublists are sorted. *)
    1.18        from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
    1.19        have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
    1.20        from quicksort_outer_remains [OF qs2] length_remains
    1.21 @@ -510,32 +510,32 @@
    1.22        with IH1 have IH1': "sorted (subarray l p a h')" by simp
    1.23        from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
    1.24        have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
    1.25 -	by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
    1.26 -	  (* -- Secondly, both sublists remain partitioned. *)
    1.27 +        by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
    1.28 +           (* -- Secondly, both sublists remain partitioned. *)
    1.29        from partition_partitions[OF part True]
    1.30        have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
    1.31 -	and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
    1.32 -	by (auto simp add: all_in_set_subarray_conv)
    1.33 +        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
    1.34 +        by (auto simp add: all_in_set_subarray_conv)
    1.35        from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
    1.36 -	length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
    1.37 +        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
    1.38        have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
    1.39  	unfolding Heap.length_def subarray_def by (cases p, auto)
    1.40        with left_subarray_remains part_conds1 pivot_unchanged
    1.41        have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
    1.42 -	by (simp, subst set_of_multiset_of[symmetric], simp)
    1.43 -	  (* -- These steps are the analogous for the right sublist \<dots> *)
    1.44 +        by (simp, subst set_of_multiset_of[symmetric], simp)
    1.45 +          (* -- These steps are the analogous for the right sublist \<dots> *)
    1.46        from quicksort_outer_remains [OF qs1] length_remains
    1.47        have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
    1.48  	by (auto simp add: subarray_eq_samelength_iff)
    1.49        from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
    1.50 -	length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
    1.51 +        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
    1.52        have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
    1.53 -	unfolding Heap.length_def subarray_def by auto
    1.54 +        unfolding Heap.length_def subarray_def by auto
    1.55        with right_subarray_remains part_conds2 pivot_unchanged
    1.56        have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
    1.57 -	by (simp, subst set_of_multiset_of[symmetric], simp)
    1.58 -	  (* -- Thirdly and finally, we show that the array is sorted
    1.59 -	  following from the facts above. *)
    1.60 +        by (simp, subst set_of_multiset_of[symmetric], simp)
    1.61 +          (* -- Thirdly and finally, we show that the array is sorted
    1.62 +          following from the facts above. *)
    1.63        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.64  	by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
    1.65        with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis