merged
authornipkow
Tue, 24 Mar 2009 12:45:23 +0100
changeset 30698 7b09a2d9bcfc
parent 30695 182fb8d27b48 (diff)
parent 30697 48f5a5524e11 (current diff)
child 30699 08760e217eb7
merged
--- a/doc-src/HOL/HOL.tex	Tue Mar 24 12:45:01 2009 +0100
+++ b/doc-src/HOL/HOL.tex	Tue Mar 24 12:45:23 2009 +0100
@@ -1427,7 +1427,7 @@
 provides a decision procedure for \emph{linear arithmetic}: formulae involving
 addition and subtraction. The simplifier invokes a weak version of this
 decision procedure automatically. If this is not sufficent, you can invoke the
-full procedure \ttindex{arith_tac} explicitly.  It copes with arbitrary
+full procedure \ttindex{linear_arith_tac} explicitly.  It copes with arbitrary
 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
   min}, {\tt max} and numerical constants. Other subterms are treated as
 atomic, while subformulae not involving numerical types are ignored. Quantified
@@ -1438,10 +1438,10 @@
 If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
 {\tt k dvd} are also supported. The former two are eliminated
 by case distinctions, again blowing up the running time.
-If the formula involves explicit quantifiers, \texttt{arith_tac} may take
+If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take
 super-exponential time and space.
 
-If \texttt{arith_tac} fails, try to find relevant arithmetic results in
+If \texttt{linear_arith_tac} fails, try to find relevant arithmetic results in
 the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
 theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
 Theory \texttt{Divides} contains theorems about \texttt{div} and
--- a/src/HOL/Arith_Tools.thy	Tue Mar 24 12:45:01 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,388 +0,0 @@
-(*  Title:      HOL/Arith_Tools.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Amine Chaieb, TU Muenchen
-*)
-
-header {* Setup of arithmetic tools *}
-
-theory Arith_Tools
-imports NatBin
-uses
-  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
-  "~~/src/Provers/Arith/extract_common_term.ML"
-  "Tools/int_factor_simprocs.ML"
-  "Tools/nat_simprocs.ML"
-  "Tools/Qelim/qelim.ML"
-begin
-
-subsection {* Simprocs for the Naturals *}
-
-declaration {* K nat_simprocs_setup *}
-
-subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
-
-text{*Where K above is a literal*}
-
-lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
-by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
-
-text {*Now just instantiating @{text n} to @{text "number_of v"} does
-  the right simplification, but with some redundant inequality
-  tests.*}
-lemma neg_number_of_pred_iff_0:
-  "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
-apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
-apply (simp only: less_Suc_eq_le le_0_eq)
-apply (subst less_number_of_Suc, simp)
-done
-
-text{*No longer required as a simprule because of the @{text inverse_fold}
-   simproc*}
-lemma Suc_diff_number_of:
-     "Int.Pls < v ==>
-      Suc m - (number_of v) = m - (number_of (Int.pred v))"
-apply (subst Suc_diff_eq_diff_pred)
-apply simp
-apply (simp del: nat_numeral_1_eq_1)
-apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
-                        neg_number_of_pred_iff_0)
-done
-
-lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
-by (simp add: numerals split add: nat_diff_split)
-
-
-subsubsection{*For @{term nat_case} and @{term nat_rec}*}
-
-lemma nat_case_number_of [simp]:
-     "nat_case a f (number_of v) =
-        (let pv = number_of (Int.pred v) in
-         if neg pv then a else f (nat pv))"
-by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
-
-lemma nat_case_add_eq_if [simp]:
-     "nat_case a f ((number_of v) + n) =
-       (let pv = number_of (Int.pred v) in
-         if neg pv then nat_case a f n else f (nat pv + n))"
-apply (subst add_eq_if)
-apply (simp split add: nat.split
-            del: nat_numeral_1_eq_1
-            add: nat_numeral_1_eq_1 [symmetric]
-                 numeral_1_eq_Suc_0 [symmetric]
-                 neg_number_of_pred_iff_0)
-done
-
-lemma nat_rec_number_of [simp]:
-     "nat_rec a f (number_of v) =
-        (let pv = number_of (Int.pred v) in
-         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
-apply (case_tac " (number_of v) ::nat")
-apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
-apply (simp split add: split_if_asm)
-done
-
-lemma nat_rec_add_eq_if [simp]:
-     "nat_rec a f (number_of v + n) =
-        (let pv = number_of (Int.pred v) in
-         if neg pv then nat_rec a f n
-                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
-apply (subst add_eq_if)
-apply (simp split add: nat.split
-            del: nat_numeral_1_eq_1
-            add: nat_numeral_1_eq_1 [symmetric]
-                 numeral_1_eq_Suc_0 [symmetric]
-                 neg_number_of_pred_iff_0)
-done
-
-
-subsubsection{*Various Other Lemmas*}
-
-text {*Evens and Odds, for Mutilated Chess Board*}
-
-text{*Lemmas for specialist use, NOT as default simprules*}
-lemma nat_mult_2: "2 * z = (z+z::nat)"
-proof -
-  have "2*z = (1 + 1)*z" by simp
-  also have "... = z+z" by (simp add: left_distrib)
-  finally show ?thesis .
-qed
-
-lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
-by (subst mult_commute, rule nat_mult_2)
-
-text{*Case analysis on @{term "n<2"}*}
-lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
-by arith
-
-lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
-by arith
-
-lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: nat_mult_2 [symmetric])
-
-lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
-apply (subgoal_tac "m mod 2 < 2")
-apply (erule less_2_cases [THEN disjE])
-apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
-done
-
-lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
-apply (subgoal_tac "m mod 2 < 2")
-apply (force simp del: mod_less_divisor, simp)
-done
-
-text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
-
-lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
-by simp
-
-lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
-by simp
-
-text{*Can be used to eliminate long strings of Sucs, but not by default*}
-lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
-by simp
-
-
-text{*These lemmas collapse some needless occurrences of Suc:
-    at least three Sucs, since two and fewer are rewritten back to Suc again!
-    We already have some rules to simplify operands smaller than 3.*}
-
-lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
-by (simp add: Suc3_eq_add_3)
-
-lemmas Suc_div_eq_add3_div_number_of =
-    Suc_div_eq_add3_div [of _ "number_of v", standard]
-declare Suc_div_eq_add3_div_number_of [simp]
-
-lemmas Suc_mod_eq_add3_mod_number_of =
-    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
-declare Suc_mod_eq_add3_mod_number_of [simp]
-
-
-subsubsection{*Special Simplification for Constants*}
-
-text{*These belong here, late in the development of HOL, to prevent their
-interfering with proofs of abstract properties of instances of the function
-@{term number_of}*}
-
-text{*These distributive laws move literals inside sums and differences.*}
-lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard]
-declare left_distrib_number_of [simp]
-
-lemmas right_distrib_number_of = right_distrib [of "number_of v", standard]
-declare right_distrib_number_of [simp]
-
-
-lemmas left_diff_distrib_number_of =
-    left_diff_distrib [of _ _ "number_of v", standard]
-declare left_diff_distrib_number_of [simp]
-
-lemmas right_diff_distrib_number_of =
-    right_diff_distrib [of "number_of v", standard]
-declare right_diff_distrib_number_of [simp]
-
-
-text{*These are actually for fields, like real: but where else to put them?*}
-lemmas zero_less_divide_iff_number_of =
-    zero_less_divide_iff [of "number_of w", standard]
-declare zero_less_divide_iff_number_of [simp,noatp]
-
-lemmas divide_less_0_iff_number_of =
-    divide_less_0_iff [of "number_of w", standard]
-declare divide_less_0_iff_number_of [simp,noatp]
-
-lemmas zero_le_divide_iff_number_of =
-    zero_le_divide_iff [of "number_of w", standard]
-declare zero_le_divide_iff_number_of [simp,noatp]
-
-lemmas divide_le_0_iff_number_of =
-    divide_le_0_iff [of "number_of w", standard]
-declare divide_le_0_iff_number_of [simp,noatp]
-
-
-(****
-IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
-then these special-case declarations may be useful.
-
-text{*These simprules move numerals into numerators and denominators.*}
-lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
-by (simp add: times_divide_eq)
-
-lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
-by (simp add: times_divide_eq)
-
-lemmas times_divide_eq_right_number_of =
-    times_divide_eq_right [of "number_of w", standard]
-declare times_divide_eq_right_number_of [simp]
-
-lemmas times_divide_eq_right_number_of =
-    times_divide_eq_right [of _ _ "number_of w", standard]
-declare times_divide_eq_right_number_of [simp]
-
-lemmas times_divide_eq_left_number_of =
-    times_divide_eq_left [of _ "number_of w", standard]
-declare times_divide_eq_left_number_of [simp]
-
-lemmas times_divide_eq_left_number_of =
-    times_divide_eq_left [of _ _ "number_of w", standard]
-declare times_divide_eq_left_number_of [simp]
-
-****)
-
-text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
-  strange, but then other simprocs simplify the quotient.*}
-
-lemmas inverse_eq_divide_number_of =
-    inverse_eq_divide [of "number_of w", standard]
-declare inverse_eq_divide_number_of [simp]
-
-
-text {*These laws simplify inequalities, moving unary minus from a term
-into the literal.*}
-lemmas less_minus_iff_number_of =
-    less_minus_iff [of "number_of v", standard]
-declare less_minus_iff_number_of [simp,noatp]
-
-lemmas le_minus_iff_number_of =
-    le_minus_iff [of "number_of v", standard]
-declare le_minus_iff_number_of [simp,noatp]
-
-lemmas equation_minus_iff_number_of =
-    equation_minus_iff [of "number_of v", standard]
-declare equation_minus_iff_number_of [simp,noatp]
-
-
-lemmas minus_less_iff_number_of =
-    minus_less_iff [of _ "number_of v", standard]
-declare minus_less_iff_number_of [simp,noatp]
-
-lemmas minus_le_iff_number_of =
-    minus_le_iff [of _ "number_of v", standard]
-declare minus_le_iff_number_of [simp,noatp]
-
-lemmas minus_equation_iff_number_of =
-    minus_equation_iff [of _ "number_of v", standard]
-declare minus_equation_iff_number_of [simp,noatp]
-
-
-text{*To Simplify Inequalities Where One Side is the Constant 1*}
-
-lemma less_minus_iff_1 [simp,noatp]:
-  fixes b::"'b::{ordered_idom,number_ring}"
-  shows "(1 < - b) = (b < -1)"
-by auto
-
-lemma le_minus_iff_1 [simp,noatp]:
-  fixes b::"'b::{ordered_idom,number_ring}"
-  shows "(1 \<le> - b) = (b \<le> -1)"
-by auto
-
-lemma equation_minus_iff_1 [simp,noatp]:
-  fixes b::"'b::number_ring"
-  shows "(1 = - b) = (b = -1)"
-by (subst equation_minus_iff, auto)
-
-lemma minus_less_iff_1 [simp,noatp]:
-  fixes a::"'b::{ordered_idom,number_ring}"
-  shows "(- a < 1) = (-1 < a)"
-by auto
-
-lemma minus_le_iff_1 [simp,noatp]:
-  fixes a::"'b::{ordered_idom,number_ring}"
-  shows "(- a \<le> 1) = (-1 \<le> a)"
-by auto
-
-lemma minus_equation_iff_1 [simp,noatp]:
-  fixes a::"'b::number_ring"
-  shows "(- a = 1) = (a = -1)"
-by (subst minus_equation_iff, auto)
-
-
-text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
-
-lemmas mult_less_cancel_left_number_of =
-    mult_less_cancel_left [of "number_of v", standard]
-declare mult_less_cancel_left_number_of [simp,noatp]
-
-lemmas mult_less_cancel_right_number_of =
-    mult_less_cancel_right [of _ "number_of v", standard]
-declare mult_less_cancel_right_number_of [simp,noatp]
-
-lemmas mult_le_cancel_left_number_of =
-    mult_le_cancel_left [of "number_of v", standard]
-declare mult_le_cancel_left_number_of [simp,noatp]
-
-lemmas mult_le_cancel_right_number_of =
-    mult_le_cancel_right [of _ "number_of v", standard]
-declare mult_le_cancel_right_number_of [simp,noatp]
-
-
-text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
-
-lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
-lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
-lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
-
-
-subsubsection{*Optional Simplification Rules Involving Constants*}
-
-text{*Simplify quotients that are compared with a literal constant.*}
-
-lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
-lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
-lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
-lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
-lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
-lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
-
-
-text{*Not good as automatic simprules because they cause case splits.*}
-lemmas divide_const_simps =
-  le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
-  divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
-  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
-
-text{*Division By @{text "-1"}*}
-
-lemma divide_minus1 [simp]:
-     "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
-by simp
-
-lemma minus1_divide [simp]:
-     "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
-by (simp add: divide_inverse inverse_minus_eq)
-
-lemma half_gt_zero_iff:
-     "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
-by auto
-
-lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard]
-declare half_gt_zero [simp]
-
-(* The following lemma should appear in Divides.thy, but there the proof
-   doesn't work. *)
-
-lemma nat_dvd_not_less:
-  "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
-  by (unfold dvd_def) auto
-
-ML {*
-val divide_minus1 = @{thm divide_minus1};
-val minus1_divide = @{thm minus1_divide};
-*}
-
-end
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -299,7 +299,7 @@
 *} "Langford's algorithm for quantifier elimination in dense linear orders"
 
 
-section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
+section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields *}
 
 text {* Linear order without upper bounds *}
 
--- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1995,6 +1995,8 @@
   "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
 
+code_reserved SML oo
+
 ML {* @{code ferrack_test} () *}
 
 oracle linr_oracle = {*
--- a/src/HOL/Divides.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Divides.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1148,4 +1148,9 @@
   with j show ?thesis by blast
 qed
 
+lemma nat_dvd_not_less:
+  fixes m n :: nat
+  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
 end
--- a/src/HOL/Groebner_Basis.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Semiring normalization and Groebner Bases *}
 
 theory Groebner_Basis
-imports Arith_Tools
+imports NatBin
 uses
   "Tools/Groebner_Basis/misc.ML"
   "Tools/Groebner_Basis/normalizer_data.ML"
--- a/src/HOL/HoareParallel/OG_Examples.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -443,7 +443,7 @@
 --{* 32 subgoals left *}
 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
 
-apply(tactic {* TRYALL (simple_arith_tac @{context}) *})
+apply(tactic {* TRYALL (linear_arith_tac @{context}) *})
 --{* 9 subgoals left *}
 apply (force simp add:less_Suc_eq)
 apply(drule sym)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -0,0 +1,11 @@
+(*  Title:      HOL/Imperative_HOL/Imperative_HOL_ex.thy
+    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
+*)
+
+header {* Mmonadic imperative HOL with examples *}
+
+theory Imperative_HOL_ex
+imports Imperative_HOL "ex/Imperative_Quicksort"
+begin
+
+end
--- a/src/HOL/Imperative_HOL/ROOT.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Imperative_HOL/ROOT.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -1,2 +1,2 @@
 
-use_thy "Imperative_HOL";
+use_thy "Imperative_HOL_ex";
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -0,0 +1,639 @@
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+theory Imperative_Quicksort
+imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
+begin
+
+text {* We prove QuickSort correct in the Relational Calculus. *}
+
+definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
+where
+  "swap arr i j = (
+     do
+       x \<leftarrow> nth arr i;
+       y \<leftarrow> nth arr j;
+       upd i y arr;
+       upd j x arr;
+       return ()
+     done)"
+
+lemma swap_permutes:
+  assumes "crel (swap a i j) h h' rs"
+  shows "multiset_of (get_array a h') 
+  = multiset_of (get_array a h)"
+  using assms
+  unfolding swap_def
+  by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
+
+function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
+where
+  "part1 a left right p = (
+     if (right \<le> left) then return right
+     else (do
+       v \<leftarrow> nth a left;
+       (if (v \<le> p) then (part1 a (left + 1) right p)
+                    else (do swap a left right;
+  part1 a left (right - 1) p done))
+     done))"
+by pat_completeness auto
+
+termination
+by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
+
+declare part1.simps[simp del]
+
+lemma part_permutes:
+  assumes "crel (part1 a l r p) h h' rs"
+  shows "multiset_of (get_array a h') 
+  = multiset_of (get_array a h)"
+  using assms
+proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
+  case (1 a l r p h h' rs)
+  thus ?case
+    unfolding part1.simps [of a l r p]
+    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
+qed
+
+lemma part_returns_index_in_bounds:
+  assumes "crel (part1 a l r p) h h' rs"
+  assumes "l \<le> r"
+  shows "l \<le> rs \<and> rs \<le> r"
+using assms
+proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
+  case (1 a l r p h h' rs)
+  note cr = `crel (part1 a l r p) h h' rs`
+  show ?case
+  proof (cases "r \<le> l")
+    case True (* Terminating case *)
+    with cr `l \<le> r` show ?thesis
+      unfolding part1.simps[of a l r p]
+      by (elim crelE crel_if crel_return crel_nth) auto
+  next
+    case False (* recursive case *)
+    note rec_condition = this
+    let ?v = "get_array a h ! l"
+    show ?thesis
+    proof (cases "?v \<le> p")
+      case True
+      with cr False
+      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
+        unfolding part1.simps[of a l r p]
+        by (elim crelE crel_nth crel_if crel_return) auto
+      from rec_condition have "l + 1 \<le> r" by arith
+      from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
+      show ?thesis by simp
+    next
+      case False
+      with rec_condition cr
+      obtain h1 where swp: "crel (swap a l r) h h1 ()"
+        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
+        unfolding part1.simps[of a l r p]
+        by (elim crelE crel_nth crel_if crel_return) auto
+      from rec_condition have "l \<le> r - 1" by arith
+      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
+    qed
+  qed
+qed
+
+lemma part_length_remains:
+  assumes "crel (part1 a l r p) h h' rs"
+  shows "Heap.length a h = Heap.length a h'"
+using assms
+proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
+  case (1 a l r p h h' rs)
+  note cr = `crel (part1 a l r p) h h' rs`
+  
+  show ?case
+  proof (cases "r \<le> l")
+    case True (* Terminating case *)
+    with cr show ?thesis
+      unfolding part1.simps[of a l r p]
+      by (elim crelE crel_if crel_return crel_nth) auto
+  next
+    case False (* recursive case *)
+    with cr 1 show ?thesis
+      unfolding part1.simps [of a l r p] swap_def
+      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
+  qed
+qed
+
+lemma part_outer_remains:
+  assumes "crel (part1 a l r p) h h' rs"
+  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+  using assms
+proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
+  case (1 a l r p h h' rs)
+  note cr = `crel (part1 a l r p) h h' rs`
+  
+  show ?case
+  proof (cases "r \<le> l")
+    case True (* Terminating case *)
+    with cr show ?thesis
+      unfolding part1.simps[of a l r p]
+      by (elim crelE crel_if crel_return crel_nth) auto
+  next
+    case False (* recursive case *)
+    note rec_condition = this
+    let ?v = "get_array a h ! l"
+    show ?thesis
+    proof (cases "?v \<le> p")
+      case True
+      with cr False
+      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
+        unfolding part1.simps[of a l r p]
+        by (elim crelE crel_nth crel_if crel_return) auto
+      from 1(1)[OF rec_condition True rec1]
+      show ?thesis by fastsimp
+    next
+      case False
+      with rec_condition cr
+      obtain h1 where swp: "crel (swap a l r) h h1 ()"
+        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
+        unfolding part1.simps[of a l r p]
+        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"
+	unfolding swap_def
+	by (elim crelE crel_nth crel_upd crel_return) auto
+      with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
+    qed
+  qed
+qed
+
+
+lemma part_partitions:
+  assumes "crel (part1 a l r p) h h' rs"
+  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
+  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
+  using assms
+proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
+  case (1 a l r p h h' rs)
+  note cr = `crel (part1 a l r p) h h' rs`
+  
+  show ?case
+  proof (cases "r \<le> l")
+    case True (* Terminating case *)
+    with cr have "rs = r"
+      unfolding part1.simps[of a l r p]
+      by (elim crelE crel_if crel_return crel_nth) auto
+    with True
+    show ?thesis by auto
+  next
+    case False (* recursive case *)
+    note lr = this
+    let ?v = "get_array a h ! l"
+    show ?thesis
+    proof (cases "?v \<le> p")
+      case True
+      with lr cr
+      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
+        unfolding part1.simps[of a l r p]
+        by (elim crelE crel_nth crel_if crel_return) auto
+      from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
+	by fastsimp
+      have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
+      with 1(1)[OF False True rec1] a_l show ?thesis
+	by auto
+    next
+      case False
+      with lr cr
+      obtain h1 where swp: "crel (swap a l r) h h1 ()"
+        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
+        unfolding part1.simps[of a l r p]
+        by (elim crelE crel_nth crel_if crel_return) auto
+      from swp False have "get_array a h1 ! r \<ge> p"
+	unfolding swap_def
+	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
+      with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
+	by fastsimp
+      have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
+      with 1(2)[OF lr False rec2] a_r show ?thesis
+	by auto
+    qed
+  qed
+qed
+
+
+fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
+where
+  "partition a left right = (do
+     pivot \<leftarrow> nth a right;
+     middle \<leftarrow> part1 a left (right - 1) pivot;
+     v \<leftarrow> nth a middle;
+     m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
+     swap a m right;
+     return m
+   done)"
+
+declare partition.simps[simp del]
+
+lemma partition_permutes:
+  assumes "crel (partition a l r) h h' rs"
+  shows "multiset_of (get_array a h') 
+  = multiset_of (get_array a h)"
+proof -
+    from assms part_permutes swap_permutes show ?thesis
+      unfolding partition.simps
+      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
+qed
+
+lemma partition_length_remains:
+  assumes "crel (partition a l r) h h' rs"
+  shows "Heap.length a h = Heap.length a h'"
+proof -
+  from assms part_length_remains show ?thesis
+    unfolding partition.simps swap_def
+    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
+qed
+
+lemma partition_outer_remains:
+  assumes "crel (partition a l r) h h' rs"
+  assumes "l < r"
+  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+proof -
+  from assms part_outer_remains part_returns_index_in_bounds show ?thesis
+    unfolding partition.simps swap_def
+    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
+qed
+
+lemma partition_returns_index_in_bounds:
+  assumes crel: "crel (partition a l r) h h' rs"
+  assumes "l < r"
+  shows "l \<le> rs \<and> rs \<le> r"
+proof -
+  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
+    and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
+         else middle)"
+    unfolding partition.simps
+    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
+  from `l < r` have "l \<le> r - 1" by arith
+  from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
+qed
+
+lemma partition_partitions:
+  assumes crel: "crel (partition a l r) h h' rs"
+  assumes "l < r"
+  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
+  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
+proof -
+  let ?pivot = "get_array a h ! r" 
+  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
+    and swap: "crel (swap a rs r) h1 h' ()"
+    and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
+         else middle)"
+    unfolding partition.simps
+    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
+  from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
+    (Heap.upd a rs (get_array a h1 ! r) h1)"
+    unfolding swap_def
+    by (elim crelE crel_return crel_nth crel_upd) simp
+  from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
+    unfolding swap_def
+    by (elim crelE crel_return crel_nth crel_upd) simp
+  from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
+    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
+  from `l < r` have "l \<le> r - 1" by simp 
+  note middle_in_bounds = part_returns_index_in_bounds[OF part this]
+  from part_outer_remains[OF part] `l < r`
+  have "get_array a h ! r = get_array a h1 ! r"
+    by fastsimp
+  with swap
+  have right_remains: "get_array a h ! r = get_array a h' ! rs"
+    unfolding swap_def
+    by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
+  from part_partitions [OF part]
+  show ?thesis
+  proof (cases "get_array a h1 ! middle \<le> ?pivot")
+    case True
+    with rs_equals have rs_equals: "rs = middle + 1" by simp
+    { 
+      fix i
+      assume i_is_left: "l \<le> i \<and> i < rs"
+      with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
+      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+      from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
+      with part_partitions[OF part] right_remains True
+      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
+      with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
+	unfolding Heap.upd_def Heap.length_def by simp
+    }
+    moreover
+    {
+      fix i
+      assume "rs < i \<and> i \<le> r"
+
+      hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
+      hence "get_array a h' ! rs \<le> get_array a h' ! i"
+      proof
+	assume i_is: "rs < i \<and> i \<le> r - 1"
+	with swap_length_remains in_bounds middle_in_bounds rs_equals
+	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+	from part_partitions[OF part] rs_equals right_remains i_is
+	have "get_array a h' ! rs \<le> get_array a h1 ! i"
+	  by fastsimp
+	with i_props h'_def show ?thesis by fastsimp
+      next
+	assume i_is: "rs < i \<and> i = r"
+	with rs_equals have "Suc middle \<noteq> r" by arith
+	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
+	with part_partitions[OF part] right_remains 
+	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
+	  by fastsimp
+	with i_is True rs_equals right_remains h'_def
+	show ?thesis using in_bounds
+	  unfolding Heap.upd_def Heap.length_def
+	  by auto
+      qed
+    }
+    ultimately show ?thesis by auto
+  next
+    case False
+    with rs_equals have rs_equals: "middle = rs" by simp
+    { 
+      fix i
+      assume i_is_left: "l \<le> i \<and> i < rs"
+      with swap_length_remains in_bounds middle_in_bounds rs_equals
+      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+      from part_partitions[OF part] rs_equals right_remains i_is_left
+      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
+      with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
+	unfolding Heap.upd_def by simp
+    }
+    moreover
+    {
+      fix i
+      assume "rs < i \<and> i \<le> r"
+      hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
+      hence "get_array a h' ! rs \<le> get_array a h' ! i"
+      proof
+	assume i_is: "rs < i \<and> i \<le> r - 1"
+	with swap_length_remains in_bounds middle_in_bounds rs_equals
+	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+	from part_partitions[OF part] rs_equals right_remains i_is
+	have "get_array a h' ! rs \<le> get_array a h1 ! i"
+	  by fastsimp
+	with i_props h'_def show ?thesis by fastsimp
+      next
+	assume i_is: "i = r"
+	from i_is False rs_equals right_remains h'_def
+	show ?thesis using in_bounds
+	  unfolding Heap.upd_def Heap.length_def
+	  by auto
+      qed
+    }
+    ultimately
+    show ?thesis by auto
+  qed
+qed
+
+
+function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
+where
+  "quicksort arr left right =
+     (if (right > left)  then
+        do
+          pivotNewIndex \<leftarrow> partition arr left right;
+          pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
+          quicksort arr left (pivotNewIndex - 1);
+          quicksort arr (pivotNewIndex + 1) right
+        done
+     else return ())"
+by pat_completeness auto
+
+(* For termination, we must show that the pivotNewIndex is between left and right *) 
+termination
+by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
+
+declare quicksort.simps[simp del]
+
+
+lemma quicksort_permutes:
+  assumes "crel (quicksort a l r) h h' rs"
+  shows "multiset_of (get_array a h') 
+  = multiset_of (get_array a h)"
+  using assms
+proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
+  case (1 a l r h h' rs)
+  with partition_permutes show ?case
+    unfolding quicksort.simps [of a l r]
+    by (elim crel_if crelE crel_assert crel_return) auto
+qed
+
+lemma length_remains:
+  assumes "crel (quicksort a l r) h h' rs"
+  shows "Heap.length a h = Heap.length a h'"
+using assms
+proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
+  case (1 a l r h h' rs)
+  with partition_length_remains show ?case
+    unfolding quicksort.simps [of a l r]
+    by (elim crel_if crelE crel_assert crel_return) auto
+qed
+
+lemma quicksort_outer_remains:
+  assumes "crel (quicksort a l r) h h' rs"
+   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+  using assms
+proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
+  case (1 a l r h h' rs)
+  note cr = `crel (quicksort a l r) h h' rs`
+  thus ?case
+  proof (cases "r > l")
+    case False
+    with cr have "h' = h"
+      unfolding quicksort.simps [of a l r]
+      by (elim crel_if crel_return) auto
+    thus ?thesis by simp
+  next
+  case True
+   { 
+      fix h1 h2 p ret1 ret2 i
+      assume part: "crel (partition a l r) h h1 p"
+      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
+      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
+      assume pivot: "l \<le> p \<and> p \<le> r"
+      assume i_outer: "i < l \<or> r < i"
+      from  partition_outer_remains [OF part True] i_outer
+      have "get_array a h !i = get_array a h1 ! i" by fastsimp
+      moreover
+      with 1(1) [OF True pivot qs1] pivot i_outer
+      have "get_array a h1 ! i = get_array a h2 ! i" by auto
+      moreover
+      with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
+      have "get_array a h2 ! i = get_array a h' ! i" by auto
+      ultimately have "get_array a h ! i= get_array a h' ! i" by simp
+    }
+    with cr show ?thesis
+      unfolding quicksort.simps [of a l r]
+      by (elim crel_if crelE crel_assert crel_return) auto
+  qed
+qed
+
+lemma quicksort_is_skip:
+  assumes "crel (quicksort a l r) h h' rs"
+  shows "r \<le> l \<longrightarrow> h = h'"
+  using assms
+  unfolding quicksort.simps [of a l r]
+  by (elim crel_if crel_return) auto
+ 
+lemma quicksort_sorts:
+  assumes "crel (quicksort a l r) h h' rs"
+  assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" 
+  shows "sorted (subarray l (r + 1) a h')"
+  using assms
+proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
+  case (1 a l r h h' rs)
+  note cr = `crel (quicksort a l r) h h' rs`
+  thus ?case
+  proof (cases "r > l")
+    case False
+    hence "l \<ge> r + 1 \<or> l = r" by arith 
+    with length_remains[OF cr] 1(5) show ?thesis
+      by (auto simp add: subarray_Nil subarray_single)
+  next
+    case True
+    { 
+      fix h1 h2 p
+      assume part: "crel (partition a l r) h h1 p"
+      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
+      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
+      from partition_returns_index_in_bounds [OF part True]
+      have pivot: "l\<le> p \<and> p \<le> r" .
+     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. *)
+      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
+      have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
+	by (simp add: subarray_eq_samelength_iff)
+      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. *)
+      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)
+      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"]
+      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> *)
+      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'"]
+      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
+      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. *)
+      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
+	unfolding subarray_def
+	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
+	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
+    }
+    with True cr show ?thesis
+      unfolding quicksort.simps [of a l r]
+      by (elim crel_if crel_return crelE crel_assert) auto
+  qed
+qed
+
+
+lemma quicksort_is_sort:
+  assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
+  shows "get_array a h' = sort (get_array a h)"
+proof (cases "get_array a h = []")
+  case True
+  with quicksort_is_skip[OF crel] show ?thesis
+  unfolding Heap.length_def by simp
+next
+  case False
+  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
+    unfolding Heap.length_def subarray_def by auto
+  with length_remains[OF crel] have "sorted (get_array a h')"
+    unfolding Heap.length_def by simp
+  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
+qed
+
+subsection {* No Errors in quicksort *}
+text {* We have proved that quicksort sorts (if no exceptions occur).
+We will now show that exceptions do not occur. *}
+
+lemma noError_part1: 
+  assumes "l < Heap.length a h" "r < Heap.length a h"
+  shows "noError (part1 a l r p) h"
+  using assms
+proof (induct a l r p arbitrary: h rule: part1.induct)
+  case (1 a l r p)
+  thus ?case
+    unfolding part1.simps [of a l r] swap_def
+    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
+qed
+
+lemma noError_partition:
+  assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
+  shows "noError (partition a l r) h"
+using assms
+unfolding partition.simps swap_def
+apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
+apply (frule part_length_remains)
+apply (frule part_returns_index_in_bounds)
+apply auto
+apply (frule part_length_remains)
+apply (frule part_returns_index_in_bounds)
+apply auto
+apply (frule part_length_remains)
+apply auto
+done
+
+lemma noError_quicksort:
+  assumes "l < Heap.length a h" "r < Heap.length a h"
+  shows "noError (quicksort a l r) h"
+using assms
+proof (induct a l r arbitrary: h rule: quicksort.induct)
+  case (1 a l ri h)
+  thus ?case
+    unfolding quicksort.simps [of a l ri]
+    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
+    apply (frule partition_returns_index_in_bounds)
+    apply auto
+    apply (frule partition_returns_index_in_bounds)
+    apply auto
+    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
+    apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
+    apply (erule disjE)
+    apply auto
+    unfolding quicksort.simps [of a "Suc ri" ri]
+    apply (auto intro!: noError_if noError_return)
+    done
+qed
+
+
+subsection {* Example *}
+
+definition "qsort a = do
+    k \<leftarrow> length a;
+    quicksort a 0 (k - 1);
+    return a
+  done"
+
+ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
+
+export_code qsort in SML_imp module_name QSort
+export_code qsort in OCaml module_name QSort file -
+export_code qsort in OCaml_imp module_name QSort file -
+export_code qsort in Haskell module_name QSort file -
+
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -0,0 +1,66 @@
+theory Subarray
+imports Array Sublist
+begin
+
+definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
+where
+  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
+
+lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
+apply (simp add: subarray_def Heap.upd_def)
+apply (simp add: sublist'_update1)
+done
+
+lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
+apply (simp add: subarray_def Heap.upd_def)
+apply (subst sublist'_update2)
+apply fastsimp
+apply simp
+done
+
+lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]"
+unfolding subarray_def Heap.upd_def
+by (simp add: sublist'_update3)
+
+lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
+by (simp add: subarray_def sublist'_Nil')
+
+lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
+by (simp add: subarray_def Heap.length_def sublist'_single)
+
+lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
+by (simp add: subarray_def Heap.length_def length_sublist')
+
+lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
+by (simp add: length_subarray)
+
+lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
+unfolding Heap.length_def subarray_def
+by (simp add: sublist'_front)
+
+lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
+unfolding Heap.length_def subarray_def
+by (simp add: sublist'_back)
+
+lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
+unfolding subarray_def
+by (simp add: sublist'_append)
+
+lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
+unfolding Heap.length_def subarray_def
+by (simp add: sublist'_all)
+
+lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
+unfolding Heap.length_def subarray_def
+by (simp add: nth_sublist')
+
+lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
+unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
+
+lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
+unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
+
+lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
+unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
+
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -0,0 +1,505 @@
+(* $Id$ *)
+
+header {* Slices of lists *}
+
+theory Sublist
+imports Multiset
+begin
+
+
+lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
+apply (induct xs arbitrary: i j k)
+apply simp
+apply (simp only: sublist_Cons)
+apply simp
+apply safe
+apply simp
+apply (erule_tac x="0" in meta_allE)
+apply (erule_tac x="j - 1" in meta_allE)
+apply (erule_tac x="k - 1" in meta_allE)
+apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
+apply simp
+apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
+apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
+apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
+apply simp
+apply fastsimp
+apply fastsimp
+apply fastsimp
+apply fastsimp
+apply (erule_tac x="i - 1" in meta_allE)
+apply (erule_tac x="j - 1" in meta_allE)
+apply (erule_tac x="k - 1" in meta_allE)
+apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
+apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
+apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
+apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
+apply simp
+apply fastsimp
+apply fastsimp
+apply fastsimp
+apply fastsimp
+done
+
+lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
+apply (induct xs arbitrary: i inds)
+apply simp
+apply (case_tac i)
+apply (simp add: sublist_Cons)
+apply (simp add: sublist_Cons)
+done
+
+lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
+proof (induct xs arbitrary: i inds)
+  case Nil thus ?case by simp
+next
+  case (Cons x xs)
+  thus ?case
+  proof (cases i)
+    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
+  next
+    case (Suc i')
+    with Cons show ?thesis
+      apply simp
+      apply (simp add: sublist_Cons)
+      apply auto
+      apply (auto simp add: nat.split)
+      apply (simp add: card_less_Suc[symmetric])
+      apply (simp add: card_less_Suc2)
+      done
+  qed
+qed
+
+lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
+by (simp add: sublist_update1 sublist_update2)
+
+lemma sublist_take: "sublist xs {j. j < m} = take m xs"
+apply (induct xs arbitrary: m)
+apply simp
+apply (case_tac m)
+apply simp
+apply (simp add: sublist_Cons)
+done
+
+lemma sublist_take': "sublist xs {0..<m} = take m xs"
+apply (induct xs arbitrary: m)
+apply simp
+apply (case_tac m)
+apply simp
+apply (simp add: sublist_Cons sublist_take)
+done
+
+lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
+apply (induct xs)
+apply simp
+apply (simp add: sublist_Cons)
+done
+
+lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
+apply (induct xs)
+apply simp
+apply (simp add: sublist_Cons)
+done
+
+lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
+apply (induct xs arbitrary: a)
+apply simp
+apply(case_tac aa)
+apply simp
+apply (simp add: sublist_Cons)
+apply simp
+apply (simp add: sublist_Cons)
+done
+
+lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
+apply (induct xs arbitrary: inds)
+apply simp
+apply (simp add: sublist_Cons)
+apply auto
+apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
+apply auto
+done
+
+lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
+apply (induct xs arbitrary: inds)
+apply simp
+apply (simp add: sublist_Cons)
+apply (auto split: if_splits)
+apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
+apply (case_tac x, auto)
+done
+
+lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
+apply (induct xs arbitrary: inds)
+apply simp
+apply (simp add: sublist_Cons)
+apply auto
+apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
+apply (case_tac x, auto)
+done
+
+lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
+apply (induct xs arbitrary: ys inds inds')
+apply simp
+apply (drule sym, rule sym)
+apply (simp add: sublist_Nil, fastsimp)
+apply (case_tac ys)
+apply (simp add: sublist_Nil, fastsimp)
+apply (auto simp add: sublist_Cons)
+apply (erule_tac x="list" in meta_allE)
+apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
+apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
+apply fastsimp
+apply (erule_tac x="list" in meta_allE)
+apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
+apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
+apply fastsimp
+done
+
+lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
+apply (induct xs arbitrary: ys inds)
+apply simp
+apply (rule sym, simp add: sublist_Nil)
+apply (case_tac ys)
+apply (simp add: sublist_Nil)
+apply (auto simp add: sublist_Cons)
+apply (erule_tac x="list" in meta_allE)
+apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
+apply fastsimp
+apply (erule_tac x="list" in meta_allE)
+apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
+apply fastsimp
+done
+
+lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
+by (rule sublist_eq, auto)
+
+lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
+apply (induct xs arbitrary: ys inds)
+apply simp
+apply (rule sym, simp add: sublist_Nil)
+apply (case_tac ys)
+apply (simp add: sublist_Nil)
+apply (auto simp add: sublist_Cons)
+apply (case_tac i)
+apply auto
+apply (case_tac i)
+apply auto
+done
+
+section {* Another sublist function *}
+
+function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+  "sublist' n m [] = []"
+| "sublist' n 0 xs = []"
+| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
+| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
+by pat_completeness auto
+termination by lexicographic_order
+
+subsection {* Proving equivalence to the other sublist command *}
+
+lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
+apply (induct xs arbitrary: n m)
+apply simp
+apply (case_tac n)
+apply (case_tac m)
+apply simp
+apply (simp add: sublist_Cons)
+apply (case_tac m)
+apply simp
+apply (simp add: sublist_Cons)
+done
+
+
+lemma "sublist' n m xs = sublist xs {n..<m}"
+apply (induct xs arbitrary: n m)
+apply simp
+apply (case_tac n, case_tac m)
+apply simp
+apply simp
+apply (simp add: sublist_take')
+apply (case_tac m)
+apply simp
+apply (simp add: sublist_Cons sublist'_sublist)
+done
+
+
+subsection {* Showing equivalence to use of drop and take for definition *}
+
+lemma "sublist' n m xs = take (m - n) (drop n xs)"
+apply (induct xs arbitrary: n m)
+apply simp
+apply (case_tac m)
+apply simp
+apply (case_tac n)
+apply simp
+apply simp
+done
+
+subsection {* General lemma about sublist *}
+
+lemma sublist'_Nil[simp]: "sublist' i j [] = []"
+by simp
+
+lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow>  sublist' i' j xs)"
+by (cases i) auto
+
+lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
+apply (cases j)
+apply auto
+apply (cases i)
+apply auto
+done
+
+lemma sublist_n_0: "sublist' n 0 xs = []"
+by (induct xs, auto)
+
+lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
+apply (induct xs arbitrary: n m)
+apply simp
+apply (case_tac m)
+apply simp
+apply (case_tac n)
+apply simp
+apply simp
+done
+
+lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
+apply (induct xs arbitrary: n m)
+apply simp
+apply (case_tac m)
+apply simp
+apply (case_tac n)
+apply simp
+apply simp
+done
+
+lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
+apply (induct xs arbitrary: n m)
+apply simp
+apply (case_tac m)
+apply simp
+apply (case_tac n)
+apply simp
+apply simp
+done
+
+lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
+apply (induct xs arbitrary: n m)
+apply simp
+apply (case_tac m)
+apply simp
+apply (case_tac n)
+apply simp
+apply simp
+done
+
+lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
+apply (induct xs arbitrary: n)
+apply simp
+apply simp
+apply (case_tac n)
+apply (simp add: sublist_n_0)
+apply simp
+done
+
+lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
+apply (induct xs arbitrary: n m i)
+apply simp
+apply simp
+apply (case_tac i)
+apply simp
+apply simp
+done
+
+lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
+apply (induct xs arbitrary: n m i)
+apply simp
+apply simp
+apply (case_tac i)
+apply simp
+apply simp
+done
+
+lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
+proof (induct xs arbitrary: n m i)
+  case Nil thus ?case by auto
+next
+  case (Cons x xs)
+  thus ?case
+    apply -
+    apply auto
+    apply (cases i)
+    apply auto
+    apply (cases i)
+    apply auto
+    done
+qed
+
+lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
+proof (induct xs arbitrary: i j ys n m)
+  case Nil
+  thus ?case
+    apply -
+    apply (rule sym, drule sym)
+    apply (simp add: sublist'_Nil)
+    apply (simp add: sublist'_Nil3)
+    apply arith
+    done
+next
+  case (Cons x xs i j ys n m)
+  note c = this
+  thus ?case
+  proof (cases m)
+    case 0 thus ?thesis by (simp add: sublist_n_0)
+  next
+    case (Suc m')
+    note a = this
+    thus ?thesis
+    proof (cases n)
+      case 0 note b = this
+      show ?thesis
+      proof (cases ys)
+	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
+      next
+	case (Cons y ys)
+	show ?thesis
+	proof (cases j)
+	  case 0 with a b Cons.prems show ?thesis by simp
+	next
+	  case (Suc j') with a b Cons.prems Cons show ?thesis 
+	    apply -
+	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
+	    done
+	qed
+      qed
+    next
+      case (Suc n')
+      show ?thesis
+      proof (cases ys)
+	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
+      next
+	case (Cons y ys) with Suc a Cons.prems show ?thesis
+	  apply -
+	  apply simp
+	  apply (cases j)
+	  apply simp
+	  apply (cases i)
+	  apply simp
+	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
+	  apply simp
+	  apply simp
+	  apply simp
+	  apply simp
+	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
+	  apply simp
+	  apply simp
+	  apply simp
+	  done
+      qed
+    qed
+  qed
+qed
+
+lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
+by (induct xs arbitrary: i j, auto)
+
+lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
+apply (induct xs arbitrary: a i j)
+apply simp
+apply (case_tac j)
+apply simp
+apply (case_tac i)
+apply simp
+apply simp
+done
+
+lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
+apply (induct xs arbitrary: a i j)
+apply simp
+apply simp
+apply (case_tac j)
+apply simp
+apply auto
+apply (case_tac nat)
+apply auto
+done
+
+(* suffices that j \<le> length xs and length ys *) 
+lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs  = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
+proof (induct xs arbitrary: ys i j)
+  case Nil thus ?case by simp
+next
+  case (Cons x xs)
+  thus ?case
+    apply -
+    apply (cases ys)
+    apply simp
+    apply simp
+    apply auto
+    apply (case_tac i', auto)
+    apply (erule_tac x="Suc i'" in allE, auto)
+    apply (erule_tac x="i' - 1" in allE, auto)
+    apply (case_tac i', auto)
+    apply (erule_tac x="Suc i'" in allE, auto)
+    done
+qed
+
+lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
+by (induct xs, auto)
+
+lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
+by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
+
+lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
+by (induct xs arbitrary: i j k) auto
+
+lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
+apply (induct xs arbitrary: i j k)
+apply auto
+apply (case_tac k)
+apply auto
+apply (case_tac i)
+apply auto
+done
+
+lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
+apply (simp add: sublist'_sublist)
+apply (simp add: set_sublist)
+apply auto
+done
+
+lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
+unfolding set_sublist' by blast
+
+lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
+unfolding set_sublist' by blast
+
+
+lemma multiset_of_sublist:
+assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
+assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
+assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
+assumes multiset: "multiset_of xs = multiset_of ys"
+  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
+proof -
+  from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
+    by (simp add: sublist'_append)
+  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
+  with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
+    by (simp add: sublist'_append)
+  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
+  moreover
+  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
+    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
+  moreover
+  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
+    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
+  moreover
+  ultimately show ?thesis by (simp add: multiset_of_append)
+qed
+
+
+end
--- a/src/HOL/Import/HOL4Compat.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,11 +1,14 @@
 (*  Title:      HOL/Import/HOL4Compat.thy
-    ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum
+theory HOL4Compat
+imports HOL4Setup Complex_Main Primes ContNotDenum
 begin
 
+no_notation differentiable (infixl "differentiable" 60)
+no_notation sums (infixr "sums" 80)
+
 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
   by auto
 
@@ -22,7 +25,7 @@
 lemmas [hol4rew] = ONE_ONE_rew
 
 lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
-  by simp;
+  by simp
 
 lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
   by safe
--- a/src/HOL/Int.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Int.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1256,14 +1256,14 @@
 by (simp add: algebra_simps diff_number_of_eq [symmetric])
 
 
+
+
 subsection {* The Set of Integers *}
 
 context ring_1
 begin
 
-definition
-  Ints  :: "'a set"
-where
+definition Ints  :: "'a set" where
   [code del]: "Ints = range of_int"
 
 end
@@ -1854,7 +1854,7 @@
 qed
 
 
-subsection{*Integer Powers*} 
+subsection {* Integer Powers *} 
 
 instantiation int :: recpower
 begin
@@ -1896,6 +1896,161 @@
 
 lemmas zpower_int = int_power [symmetric]
 
+
+subsection {* Further theorems on numerals *}
+
+subsubsection{*Special Simplification for Constants*}
+
+text{*These distributive laws move literals inside sums and differences.*}
+
+lemmas left_distrib_number_of [simp] =
+  left_distrib [of _ _ "number_of v", standard]
+
+lemmas right_distrib_number_of [simp] =
+  right_distrib [of "number_of v", standard]
+
+lemmas left_diff_distrib_number_of [simp] =
+  left_diff_distrib [of _ _ "number_of v", standard]
+
+lemmas right_diff_distrib_number_of [simp] =
+  right_diff_distrib [of "number_of v", standard]
+
+text{*These are actually for fields, like real: but where else to put them?*}
+
+lemmas zero_less_divide_iff_number_of [simp, noatp] =
+  zero_less_divide_iff [of "number_of w", standard]
+
+lemmas divide_less_0_iff_number_of [simp, noatp] =
+  divide_less_0_iff [of "number_of w", standard]
+
+lemmas zero_le_divide_iff_number_of [simp, noatp] =
+  zero_le_divide_iff [of "number_of w", standard]
+
+lemmas divide_le_0_iff_number_of [simp, noatp] =
+  divide_le_0_iff [of "number_of w", standard]
+
+
+text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
+  strange, but then other simprocs simplify the quotient.*}
+
+lemmas inverse_eq_divide_number_of [simp] =
+  inverse_eq_divide [of "number_of w", standard]
+
+text {*These laws simplify inequalities, moving unary minus from a term
+into the literal.*}
+
+lemmas less_minus_iff_number_of [simp, noatp] =
+  less_minus_iff [of "number_of v", standard]
+
+lemmas le_minus_iff_number_of [simp, noatp] =
+  le_minus_iff [of "number_of v", standard]
+
+lemmas equation_minus_iff_number_of [simp, noatp] =
+  equation_minus_iff [of "number_of v", standard]
+
+lemmas minus_less_iff_number_of [simp, noatp] =
+  minus_less_iff [of _ "number_of v", standard]
+
+lemmas minus_le_iff_number_of [simp, noatp] =
+  minus_le_iff [of _ "number_of v", standard]
+
+lemmas minus_equation_iff_number_of [simp, noatp] =
+  minus_equation_iff [of _ "number_of v", standard]
+
+
+text{*To Simplify Inequalities Where One Side is the Constant 1*}
+
+lemma less_minus_iff_1 [simp,noatp]:
+  fixes b::"'b::{ordered_idom,number_ring}"
+  shows "(1 < - b) = (b < -1)"
+by auto
+
+lemma le_minus_iff_1 [simp,noatp]:
+  fixes b::"'b::{ordered_idom,number_ring}"
+  shows "(1 \<le> - b) = (b \<le> -1)"
+by auto
+
+lemma equation_minus_iff_1 [simp,noatp]:
+  fixes b::"'b::number_ring"
+  shows "(1 = - b) = (b = -1)"
+by (subst equation_minus_iff, auto)
+
+lemma minus_less_iff_1 [simp,noatp]:
+  fixes a::"'b::{ordered_idom,number_ring}"
+  shows "(- a < 1) = (-1 < a)"
+by auto
+
+lemma minus_le_iff_1 [simp,noatp]:
+  fixes a::"'b::{ordered_idom,number_ring}"
+  shows "(- a \<le> 1) = (-1 \<le> a)"
+by auto
+
+lemma minus_equation_iff_1 [simp,noatp]:
+  fixes a::"'b::number_ring"
+  shows "(- a = 1) = (a = -1)"
+by (subst minus_equation_iff, auto)
+
+
+text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
+
+lemmas mult_less_cancel_left_number_of [simp, noatp] =
+  mult_less_cancel_left [of "number_of v", standard]
+
+lemmas mult_less_cancel_right_number_of [simp, noatp] =
+  mult_less_cancel_right [of _ "number_of v", standard]
+
+lemmas mult_le_cancel_left_number_of [simp, noatp] =
+  mult_le_cancel_left [of "number_of v", standard]
+
+lemmas mult_le_cancel_right_number_of [simp, noatp] =
+  mult_le_cancel_right [of _ "number_of v", standard]
+
+
+text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
+
+lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
+lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
+lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
+
+
+subsubsection{*Optional Simplification Rules Involving Constants*}
+
+text{*Simplify quotients that are compared with a literal constant.*}
+
+lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
+lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
+lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
+lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
+lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
+lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
+
+
+text{*Not good as automatic simprules because they cause case splits.*}
+lemmas divide_const_simps =
+  le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
+  divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
+  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
+
+text{*Division By @{text "-1"}*}
+
+lemma divide_minus1 [simp]:
+     "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
+by simp
+
+lemma minus1_divide [simp]:
+     "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
+by (simp add: divide_inverse inverse_minus_eq)
+
+lemma half_gt_zero_iff:
+     "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
+by auto
+
+lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
+
+
 subsection {* Configuration of the code generator *}
 
 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
--- a/src/HOL/IntDiv.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/IntDiv.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -8,6 +8,10 @@
 
 theory IntDiv
 imports Int Divides FunDef
+uses
+  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+  "~~/src/Provers/Arith/extract_common_term.ML"
+  ("Tools/int_factor_simprocs.ML")
 begin
 
 definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
@@ -920,9 +924,10 @@
 next
   assume "a\<noteq>0" and le_a: "0\<le>a"   
   hence a_pos: "1 \<le> a" by arith
-  hence one_less_a2: "1 < 2*a" by arith
+  hence one_less_a2: "1 < 2 * a" by arith
   hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
-    by (simp add: mult_le_cancel_left add_commute [of 1] add1_zle_eq)
+    unfolding mult_le_cancel_left
+    by (simp add: add1_zle_eq add_commute [of 1])
   with a_pos have "0 \<le> b mod a" by simp
   hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
     by (simp add: mod_pos_pos_trivial one_less_a2)
@@ -1357,6 +1362,11 @@
 qed
 
 
+subsection {* Simproc setup *}
+
+use "Tools/int_factor_simprocs.ML"
+
+
 subsection {* Code generation *}
 
 definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--- a/src/HOL/IsaMakefile	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/IsaMakefile	Tue Mar 24 12:45:23 2009 +0100
@@ -204,7 +204,6 @@
 	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
 
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
-  Arith_Tools.thy \
   ATP_Linkup.thy \
   Code_Eval.thy \
   Code_Message.thy \
@@ -650,7 +649,11 @@
 $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \
   Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \
   Imperative_HOL/Relational.thy \
-  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy
+  Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy \
+  Imperative_HOL/Imperative_HOL_ex.thy \
+  Imperative_HOL/ex/Imperative_Quicksort.thy \
+  Imperative_HOL/ex/Subarray.thy \
+  Imperative_HOL/ex/Sublist.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
 
 
@@ -837,7 +840,7 @@
   ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy			\
   ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
   ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
-  ex/Hilbert_Classical.thy ex/ImperativeQuicksort.thy			\
+  ex/Hilbert_Classical.thy			\
   ex/Induction_Scheme.thy ex/InductiveInvariant.thy			\
   ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
   ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
@@ -846,8 +849,8 @@
   ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML	\
   ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
-  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy		\
-  ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
+  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
+  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
   ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
   ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
   ex/Predicate_Compile.thy ex/predicate_compile.ML
--- a/src/HOL/Library/Abstract_Rat.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Abstract_Rat.thy
-    ID:         $Id$
     Author:     Amine Chaieb
 *)
 
 header {* Abstract rational numbers *}
 
 theory Abstract_Rat
-imports Plain GCD
+imports GCD Main
 begin
 
 types Num = "int \<times> int"
--- a/src/HOL/Library/AssocList.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/AssocList.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/AssocList.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser
 *)
 
 header {* Map operations implemented on association lists*}
 
 theory AssocList 
-imports Plain "~~/src/HOL/Map"
+imports Map Main
 begin
 
 text {*
--- a/src/HOL/Library/Binomial.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Binomial.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -6,7 +6,7 @@
 header {* Binomial Coefficients *}
 
 theory Binomial
-imports Fact Plain "~~/src/HOL/SetInterval" Presburger 
+imports Fact SetInterval Presburger Main
 begin
 
 text {* This development is based on the work of Andy Gordon and
--- a/src/HOL/Library/Boolean_Algebra.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Boolean Algebras *}
 
 theory Boolean_Algebra
-imports Plain
+imports Main
 begin
 
 locale boolean =
--- a/src/HOL/Library/Char_nat.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Char_nat.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Char_nat.thy
-    ID:         $Id$
     Author:     Norbert Voelker, Florian Haftmann
 *)
 
 header {* Mapping between characters and natural numbers *}
 
 theory Char_nat
-imports Plain "~~/src/HOL/List"
+imports List Main
 begin
 
 text {* Conversions between nibbles and natural numbers in [0..15]. *}
--- a/src/HOL/Library/Char_ord.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Char_ord.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Char_ord.thy
-    ID:         $Id$
     Author:     Norbert Voelker, Florian Haftmann
 *)
 
 header {* Order on characters *}
 
 theory Char_ord
-imports Plain Product_ord Char_nat
+imports Product_ord Char_nat Main
 begin
 
 instantiation nibble :: linorder
--- a/src/HOL/Library/Code_Char.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Code_Char.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Code generation of pretty characters (and strings) *}
 
 theory Code_Char
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
+imports List Code_Eval Main
 begin
 
 code_type char
--- a/src/HOL/Library/Code_Char_chr.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Code_Char_chr.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Code_Char_chr.thy
-    ID:         $Id$
     Author:     Florian Haftmann
 *)
 
 header {* Code generation of pretty characters with character codes *}
 
 theory Code_Char_chr
-imports Plain Char_nat Code_Char Code_Integer
+imports Char_nat Code_Char Code_Integer Main
 begin
 
 definition
--- a/src/HOL/Library/Code_Index.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Code_Index.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -3,7 +3,7 @@
 header {* Type of indices *}
 
 theory Code_Index
-imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
+imports Main
 begin
 
 text {*
--- a/src/HOL/Library/Code_Integer.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Pretty integer literals for code generation *}
 
 theory Code_Integer
-imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
+imports Main
 begin
 
 text {*
--- a/src/HOL/Library/Coinductive_List.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Coinductive_Lists.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson and Makarius
 *)
 
 header {* Potentially infinite lists as greatest fixed-point *}
 
 theory Coinductive_List
-imports Plain "~~/src/HOL/List"
+imports List Main
 begin
 
 subsection {* List constructors over the datatype universe *}
--- a/src/HOL/Library/Commutative_Ring.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Commutative_Ring.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -6,7 +6,7 @@
 header {* Proving equalities in commutative rings *}
 
 theory Commutative_Ring
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Parity"
+imports List Parity Main
 uses ("comm_ring.ML")
 begin
 
--- a/src/HOL/Library/ContNotDenum.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Non-denumerability of the Continuum. *}
 
 theory ContNotDenum
-imports RComplete Hilbert_Choice
+imports Complex_Main
 begin
 
 subsection {* Abstract *}
--- a/src/HOL/Library/Continuity.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Continuity.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Continuity.thy
-    ID:         $Id$
     Author:     David von Oheimb, TU Muenchen
 *)
 
 header {* Continuity and iterations (of set transformers) *}
 
 theory Continuity
-imports Plain "~~/src/HOL/Relation_Power"
+imports Relation_Power Main
 begin
 
 subsection {* Continuity for complete lattices *}
--- a/src/HOL/Library/Countable.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Countable.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -6,11 +6,11 @@
 
 theory Countable
 imports
-  Plain
   "~~/src/HOL/List"
   "~~/src/HOL/Hilbert_Choice"
   "~~/src/HOL/Nat_Int_Bij"
   "~~/src/HOL/Rational"
+  Main
 begin
 
 subsection {* The class of countable types *}
--- a/src/HOL/Library/Determinants.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Determinants.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Traces, Determinant of square matrices and some properties *}
 
 theory Determinants
-  imports Euclidean_Space Permutations
+imports Euclidean_Space Permutations
 begin
 
 subsection{* First some facts about products*}
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Implementation of natural numbers by target-language integers *}
 
 theory Efficient_Nat
-imports Code_Index Code_Integer
+imports Code_Index Code_Integer Main
 begin
 
 text {*
--- a/src/HOL/Library/Enum.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Enum.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Finite types as explicit enumerations *}
 
 theory Enum
-imports Plain "~~/src/HOL/Map"
+imports Map Main
 begin
 
 subsection {* Class @{text enum} *}
--- a/src/HOL/Library/Euclidean_Space.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,10 +5,11 @@
 header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
 
 theory Euclidean_Space
-  imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
+imports
+  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
   Inner_Product
-  uses ("normarith.ML")
+uses ("normarith.ML")
 begin
 
 text{* Some common special cases.*}
--- a/src/HOL/Library/Eval_Witness.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Evaluation Oracle with ML witnesses *}
 
 theory Eval_Witness
-imports Plain "~~/src/HOL/List"
+imports List Main
 begin
 
 text {* 
--- a/src/HOL/Library/Executable_Set.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Executable_Set.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 *)
 
 header {* Implementation of finite sets by lists *}
 
 theory Executable_Set
-imports Plain "~~/src/HOL/List"
+imports Main
 begin
 
 subsection {* Definitional rewrites *}
--- a/src/HOL/Library/Finite_Cartesian_Product.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,12 +5,9 @@
 header {* Definition of finite Cartesian product types. *}
 
 theory Finite_Cartesian_Product
-  (* imports Plain SetInterval ATP_Linkup *)
-imports Main
+imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
 begin
 
-  (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*)
-
 definition hassize (infixr "hassize" 12) where
   "(S hassize n) = (finite S \<and> card S = n)"
 
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      Formal_Power_Series.thy
-    ID:
     Author:     Amine Chaieb, University of Cambridge
 *)
 
 header{* A formalization of formal power series *}
 
 theory Formal_Power_Series
-  imports Main Fact Parity
+imports Main Fact Parity
 begin
 
 subsection {* The type of formal power series*}
--- a/src/HOL/Library/FrechetDeriv.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title       : FrechetDeriv.thy
-    ID          : $Id$
     Author      : Brian Huffman
 *)
 
 header {* Frechet Derivative *}
 
 theory FrechetDeriv
-imports Lim
+imports Lim Complex_Main
 begin
 
 definition
--- a/src/HOL/Library/FuncSet.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/FuncSet.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/FuncSet.thy
-    ID:         $Id$
     Author:     Florian Kammueller and Lawrence C Paulson
 *)
 
 header {* Pi and Function Sets *}
 
 theory FuncSet
-imports Plain "~~/src/HOL/Hilbert_Choice"
+imports Hilbert_Choice Main
 begin
 
 definition
--- a/src/HOL/Library/Glbs.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Glbs.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,8 +1,6 @@
-(* Title:      Glbs
-   Author:     Amine Chaieb, University of Cambridge
-*)
+(* Author: Amine Chaieb, University of Cambridge *)
 
-header{*Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs*}
+header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
 
 theory Glbs
 imports Lubs
--- a/src/HOL/Library/Infinite_Set.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,15 +1,13 @@
 (*  Title:      HOL/Library/Infinite_Set.thy
-    ID:         $Id$
     Author:     Stephan Merz
 *)
 
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports Main "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
+imports Main
 begin
 
-
 subsection "Infinite Sets"
 
 text {*
--- a/src/HOL/Library/Inner_Product.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Inner Product Spaces and the Gradient Derivative *}
 
 theory Inner_Product
-imports Complex FrechetDeriv
+imports Complex_Main FrechetDeriv
 begin
 
 subsection {* Real inner product spaces *}
--- a/src/HOL/Library/LaTeXsugar.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 
 (*<*)
 theory LaTeXsugar
-imports Plain "~~/src/HOL/List"
+imports Main
 begin
 
 (* LOGIC *)
--- a/src/HOL/Library/ListVector.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/ListVector.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,11 +1,9 @@
-(*  ID:         $Id$
-    Author:     Tobias Nipkow, 2007
-*)
+(*  Author: Tobias Nipkow, 2007 *)
 
-header "Lists as vectors"
+header {* Lists as vectors *}
 
 theory ListVector
-imports Plain "~~/src/HOL/List"
+imports List Main
 begin
 
 text{* \noindent
--- a/src/HOL/Library/List_Prefix.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/List_Prefix.thy
-    ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 *)
 
 header {* List prefixes and postfixes *}
 
 theory List_Prefix
-imports Plain "~~/src/HOL/List"
+imports List Main
 begin
 
 subsection {* Prefix order on lists *}
--- a/src/HOL/Library/List_lexord.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/List_lexord.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/List_lexord.thy
-    ID:         $Id$
     Author:     Norbert Voelker
 *)
 
 header {* Lexicographic order on lists *}
 
 theory List_lexord
-imports Plain "~~/src/HOL/List"
+imports List Main
 begin
 
 instantiation list :: (ord) ord
--- a/src/HOL/Library/Mapping.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Mapping.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* An abstract view on maps for code generation. *}
 
 theory Mapping
-imports Map
+imports Map Main
 begin
 
 subsection {* Type definition and primitive operations *}
--- a/src/HOL/Library/Multiset.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Multisets *}
 
 theory Multiset
-imports Plain "~~/src/HOL/List"
+imports List Main
 begin
 
 subsection {* The type of multisets *}
--- a/src/HOL/Library/Nat_Infinity.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Natural numbers with infinity *}
 
 theory Nat_Infinity
-imports Plain "~~/src/HOL/Presburger"
+imports Main
 begin
 
 subsection {* Type definition *}
--- a/src/HOL/Library/Nat_Int_Bij.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Nat_Int_Bij.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Nat_Int_Bij.thy
-    ID:         $Id$
     Author:     Stefan Richter, Tobias Nipkow
 *)
 
 header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
 
 theory Nat_Int_Bij
-imports Hilbert_Choice Presburger
+imports Main
 begin
 
 subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
--- a/src/HOL/Library/Nested_Environment.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Nested_Environment.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Nested_Environment.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Nested environments *}
 
 theory Nested_Environment
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
+imports Main
 begin
 
 text {*
--- a/src/HOL/Library/Numeral_Type.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Numeral Syntax for Types *}
 
 theory Numeral_Type
-imports Plain "~~/src/HOL/Presburger"
+imports Main
 begin
 
 subsection {* Preliminary lemmas *}
--- a/src/HOL/Library/Option_ord.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Option_ord.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,15 +1,14 @@
 (*  Title:      HOL/Library/Option_ord.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Canonical order on option type *}
 
 theory Option_ord
-imports Plain
+imports Option Main
 begin
 
-instantiation option :: (order) order
+instantiation option :: (preorder) preorder
 begin
 
 definition less_eq_option where
@@ -48,12 +47,63 @@
 lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
   by (simp add: less_option_def)
 
-instance by default
-  (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance proof
+qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
 
 end 
 
-instance option :: (linorder) linorder
-  by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance option :: (order) order proof
+qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instance option :: (linorder) linorder proof
+qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instantiation option :: (preorder) bot
+begin
+
+definition "bot = None"
+
+instance proof
+qed (simp add: bot_option_def)
+
+end
+
+instantiation option :: (top) top
+begin
+
+definition "top = Some top"
+
+instance proof
+qed (simp add: top_option_def less_eq_option_def split: option.split)
 
 end
+
+instance option :: (wellorder) wellorder proof
+  fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
+  assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  have "P None" by (rule H) simp
+  then have P_Some [case_names Some]:
+    "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
+  proof -
+    fix z
+    assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
+    with `P None` show "P z" by (cases z) simp_all
+  qed
+  show "P z" proof (cases z rule: P_Some)
+    case (Some w)
+    show "(P o Some) w" proof (induct rule: less_induct)
+      case (less x)
+      have "P (Some x)" proof (rule H)
+        fix y :: "'a option"
+        assume "y < Some x"
+        show "P y" proof (cases y rule: P_Some)
+          case (Some v) with `y < Some x` have "v < x" by simp
+          with less show "(P o Some) v" .
+        qed
+      qed
+      then show ?case by simp
+    qed
+  qed
+qed
+
+end
--- a/src/HOL/Library/OptionalSugar.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -4,7 +4,7 @@
 *)
 (*<*)
 theory OptionalSugar
-imports LaTeXsugar Complex_Main
+imports Complex_Main LaTeXsugar
 begin
 
 (* hiding set *)
--- a/src/HOL/Library/Order_Relation.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,6 +1,4 @@
-(*  ID          : $Id$
-    Author      : Tobias Nipkow
-*)
+(* Author: Tobias Nipkow *)
 
 header {* Orders as Relations *}
 
--- a/src/HOL/Library/Permutations.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Permutations.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -5,7 +5,7 @@
 header {* Permutations, both general and specifically on finite sets.*}
 
 theory Permutations
-imports Main Finite_Cartesian_Product Parity Fact
+imports Finite_Cartesian_Product Parity Fact Main
 begin
 
   (* Why should I import Main just to solve the Typerep problem! *)
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -6,10 +6,9 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-  imports SEQ Euclidean_Space
+imports SEQ Euclidean_Space
 begin
 
-
 declare fstcart_pastecart[simp] sndcart_pastecart[simp]
 
 subsection{* General notion of a topology *}
@@ -474,7 +473,7 @@
   have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
                ==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
   have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_sym]
-    by (auto simp add: dist_refl expand_set_eq Arith_Tools.less_divide_eq_number_of1)
+    by (auto simp add: dist_refl expand_set_eq less_divide_eq_number_of1)
   then show ?thesis by blast
 qed
 
@@ -662,7 +661,7 @@
 	have "?k/2 \<ge> 0" using kp by simp
 	then obtain w where w: "dist y w = ?k/ 2" by (metis vector_choose_dist)
 	from iT[unfolded expand_set_eq mem_interior]
-	have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+	have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: less_divide_eq_number_of1)
 	then obtain z where z: "dist w z < ?k/4" "z \<notin> T" by (auto simp add: subset_eq)
 	have "z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" using z apply simp
 	  using w e(1) d apply (auto simp only: dist_sym)
@@ -1323,7 +1322,7 @@
     assume "e>0"
     hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net"
             "eventually (\<lambda>x. dist (g x) m < e/2) net" using as
-      by (auto intro: tendstoD simp del: Arith_Tools.less_divide_eq_number_of1)
+      by (auto intro: tendstoD simp del: less_divide_eq_number_of1)
     hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net"
     proof(cases "trivial_limit net")
       case True
@@ -3956,7 +3955,7 @@
       hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto
       hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto
       from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto
-      have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: Arith_Tools.less_divide_eq_number_of1)
+      have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: less_divide_eq_number_of1)
       hence "\<bar>f x\<bar> * 2 * \<bar>l\<bar>  \<ge> \<bar>l\<bar> * \<bar>l\<bar>" unfolding mult_le_cancel_right by auto
       hence "\<bar>f x * l\<bar> * 2  \<ge> \<bar>l\<bar>^2" unfolding real_mult_commute and power2_eq_square by auto
       hence ***:"inverse \<bar>f x * l\<bar> \<le> inverse (l\<twosuperior> / 2)" using fxl0
@@ -4318,7 +4317,7 @@
       have "a$i < b$i" using as[THEN spec[where x=i]] by auto
       hence "a$i < ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i < b$i"
 	unfolding vector_smult_component and vector_add_component
-	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
+	by (auto simp add: less_divide_eq_number_of1)  }
     hence "{a <..< b} \<noteq> {}" using mem_interval(1)[of "?x" a b] by auto  }
   ultimately show ?th1 by blast
 
@@ -4333,7 +4332,7 @@
       have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
       hence "a$i \<le> ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i \<le> b$i"
 	unfolding vector_smult_component and vector_add_component
-	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
+	by (auto simp add: less_divide_eq_number_of1)  }
     hence "{a .. b} \<noteq> {}" using mem_interval(2)[of "?x" a b] by auto  }
   ultimately show ?th2 by blast
 qed
@@ -4397,13 +4396,13 @@
       { fix j
 	have "c $ j < ?x $ j \<and> ?x $ j < d $ j" unfolding Cart_lambda_beta
 	  apply(cases "j=i") using as(2)[THEN spec[where x=j]]
-	  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2)  }
+	  by (auto simp add: less_divide_eq_number_of1 as2)  }
       hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
       moreover
       have "?x\<notin>{a .. b}"
 	unfolding mem_interval apply auto apply(rule_tac x=i in exI)
 	using as(2)[THEN spec[where x=i]] and as2
-	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+	by (auto simp add: less_divide_eq_number_of1)
       ultimately have False using as by auto  }
     hence "a$i \<le> c$i" by(rule ccontr)auto
     moreover
@@ -4412,13 +4411,13 @@
       { fix j
 	have "d $ j > ?x $ j \<and> ?x $ j > c $ j" unfolding Cart_lambda_beta
 	  apply(cases "j=i") using as(2)[THEN spec[where x=j]]
-	  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2)  }
+	  by (auto simp add: less_divide_eq_number_of1 as2)  }
       hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
       moreover
       have "?x\<notin>{a .. b}"
 	unfolding mem_interval apply auto apply(rule_tac x=i in exI)
 	using as(2)[THEN spec[where x=i]] and as2
-	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+	by (auto simp add: less_divide_eq_number_of1)
       ultimately have False using as by auto  }
     hence "b$i \<ge> d$i" by(rule ccontr)auto
     ultimately
@@ -4449,7 +4448,7 @@
 lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows
  "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
   unfolding expand_set_eq and Int_iff and mem_interval
-  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 intro!: bexI)
+  by (auto simp add: less_divide_eq_number_of1 intro!: bexI)
 
 (* Moved interval_open_subset_closed a bit upwards *)
 
@@ -4564,7 +4563,7 @@
     have "a $ i < ((1 / 2) *s (a + b)) $ i \<and> ((1 / 2) *s (a + b)) $ i < b $ i"
       using assms[unfolded interval_ne_empty, THEN spec[where x=i]]
       unfolding vector_smult_component and vector_add_component
-      by(auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
+      by(auto simp add: less_divide_eq_number_of1)  }
   thus ?thesis unfolding mem_interval by auto
 qed
 
@@ -5632,7 +5631,7 @@
     { assume as:"dist a b > dist (f n x) (f n y)"
       then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
 	and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
-	using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: Arith_Tools.less_divide_eq_number_of1)
+	using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: less_divide_eq_number_of1)
       hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
 	apply(erule_tac x="Na+Nb+n" in allE)
 	apply(erule_tac x="Na+Nb+n" in allE) apply simp
--- a/src/HOL/Library/Zorn.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Library/Zorn.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -7,7 +7,7 @@
 header {* Zorn's Lemma *}
 
 theory Zorn
-imports "~~/src/HOL/Order_Relation"
+imports Order_Relation Main
 begin
 
 (* Define globally? In Set.thy? *)
--- a/src/HOL/NSA/hypreal_arith.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/NSA/hypreal_arith.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -30,10 +30,10 @@
     Simplifier.simproc (the_context ())
       "fast_hypreal_arith" 
       ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
-    (K LinArith.lin_arith_simproc);
+    (K Lin_Arith.lin_arith_simproc);
 
 val hypreal_arith_setup =
-  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = real_inj_thms @ inj_thms,
--- a/src/HOL/Nat.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Nat.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -63,9 +63,8 @@
 end
 
 lemma Suc_not_Zero: "Suc m \<noteq> 0"
-  apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
+  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
     Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
-  done
 
 lemma Zero_not_Suc: "0 \<noteq> Suc m"
   by (rule not_sym, rule Suc_not_Zero not_sym)
@@ -82,7 +81,7 @@
   done
 
 lemma nat_induct [case_names 0 Suc, induct type: nat]:
-  -- {* for backward compatibility -- naming of variables differs *}
+  -- {* for backward compatibility -- names of variables differ *}
   fixes n
   assumes "P 0"
     and "\<And>n. P n \<Longrightarrow> P (Suc n)"
@@ -1345,19 +1344,13 @@
   shows "u = s"
   using 2 1 by (rule trans)
 
+setup Arith_Data.setup
+
 use "Tools/nat_arith.ML"
 declaration {* K Nat_Arith.setup *}
 
-ML{*
-structure ArithFacts =
-  NamedThmsFun(val name = "arith"
-               val description = "arith facts - only ground formulas");
-*}
-
-setup ArithFacts.setup
-
 use "Tools/lin_arith.ML"
-declaration {* K LinArith.setup *}
+declaration {* K Lin_Arith.setup *}
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
--- a/src/HOL/NatBin.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/NatBin.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -7,6 +7,7 @@
 
 theory NatBin
 imports IntDiv
+uses ("Tools/nat_simprocs.ML")
 begin
 
 text {*
@@ -40,9 +41,7 @@
 
 subsection {* Predicate for negative binary numbers *}
 
-definition
-  neg  :: "int \<Rightarrow> bool"
-where
+definition neg  :: "int \<Rightarrow> bool" where
   "neg Z \<longleftrightarrow> Z < 0"
 
 lemma not_neg_int [simp]: "~ neg (of_nat n)"
@@ -652,7 +651,7 @@
 val numeral_ss = @{simpset} addsimps @{thms numerals};
 
 val nat_bin_arith_setup =
- LinArith.map_data
+ Lin_Arith.map_data
    (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
      {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
       inj_thms = inj_thms,
@@ -818,4 +817,159 @@
      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
 by (simp add: nat_mult_div_cancel1)
 
+
+subsection {* Simprocs for the Naturals *}
+
+use "Tools/nat_simprocs.ML"
+declaration {* K nat_simprocs_setup *}
+
+subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
+
+text{*Where K above is a literal*}
+
+lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
+by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
+
+text {*Now just instantiating @{text n} to @{text "number_of v"} does
+  the right simplification, but with some redundant inequality
+  tests.*}
+lemma neg_number_of_pred_iff_0:
+  "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
+apply (simp only: less_Suc_eq_le le_0_eq)
+apply (subst less_number_of_Suc, simp)
+done
+
+text{*No longer required as a simprule because of the @{text inverse_fold}
+   simproc*}
+lemma Suc_diff_number_of:
+     "Int.Pls < v ==>
+      Suc m - (number_of v) = m - (number_of (Int.pred v))"
+apply (subst Suc_diff_eq_diff_pred)
+apply simp
+apply (simp del: nat_numeral_1_eq_1)
+apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
+                        neg_number_of_pred_iff_0)
+done
+
+lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
+by (simp add: numerals split add: nat_diff_split)
+
+
+subsubsection{*For @{term nat_case} and @{term nat_rec}*}
+
+lemma nat_case_number_of [simp]:
+     "nat_case a f (number_of v) =
+        (let pv = number_of (Int.pred v) in
+         if neg pv then a else f (nat pv))"
+by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
+
+lemma nat_case_add_eq_if [simp]:
+     "nat_case a f ((number_of v) + n) =
+       (let pv = number_of (Int.pred v) in
+         if neg pv then nat_case a f n else f (nat pv + n))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+            del: nat_numeral_1_eq_1
+            add: nat_numeral_1_eq_1 [symmetric]
+                 numeral_1_eq_Suc_0 [symmetric]
+                 neg_number_of_pred_iff_0)
+done
+
+lemma nat_rec_number_of [simp]:
+     "nat_rec a f (number_of v) =
+        (let pv = number_of (Int.pred v) in
+         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
+apply (case_tac " (number_of v) ::nat")
+apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
+apply (simp split add: split_if_asm)
+done
+
+lemma nat_rec_add_eq_if [simp]:
+     "nat_rec a f (number_of v + n) =
+        (let pv = number_of (Int.pred v) in
+         if neg pv then nat_rec a f n
+                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+            del: nat_numeral_1_eq_1
+            add: nat_numeral_1_eq_1 [symmetric]
+                 numeral_1_eq_Suc_0 [symmetric]
+                 neg_number_of_pred_iff_0)
+done
+
+
+subsubsection{*Various Other Lemmas*}
+
+text {*Evens and Odds, for Mutilated Chess Board*}
+
+text{*Lemmas for specialist use, NOT as default simprules*}
+lemma nat_mult_2: "2 * z = (z+z::nat)"
+proof -
+  have "2*z = (1 + 1)*z" by simp
+  also have "... = z+z" by (simp add: left_distrib)
+  finally show ?thesis .
+qed
+
+lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
+by (subst mult_commute, rule nat_mult_2)
+
+text{*Case analysis on @{term "n<2"}*}
+lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
+by arith
+
+lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
+by arith
+
+lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
+by (simp add: nat_mult_2 [symmetric])
+
+lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
+apply (subgoal_tac "m mod 2 < 2")
+apply (erule less_2_cases [THEN disjE])
+apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
+done
+
+lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
+apply (subgoal_tac "m mod 2 < 2")
+apply (force simp del: mod_less_divisor, simp)
+done
+
+text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
+
+lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
+by simp
+
+lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
+by simp
+
+text{*Can be used to eliminate long strings of Sucs, but not by default*}
+lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
+by simp
+
+
+text{*These lemmas collapse some needless occurrences of Suc:
+    at least three Sucs, since two and fewer are rewritten back to Suc again!
+    We already have some rules to simplify operands smaller than 3.*}
+
+lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
+by (simp add: Suc3_eq_add_3)
+
+lemmas Suc_div_eq_add3_div_number_of =
+    Suc_div_eq_add3_div [of _ "number_of v", standard]
+declare Suc_div_eq_add3_div_number_of [simp]
+
+lemmas Suc_mod_eq_add3_mod_number_of =
+    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
+declare Suc_mod_eq_add3_mod_number_of [simp]
+
 end
--- a/src/HOL/OrderedGroup.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/OrderedGroup.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -466,7 +466,7 @@
   then show ?thesis by simp
 qed
 
-lemma add_neg_nonpos: 
+lemma add_neg_nonpos:
   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
 proof -
   have "a + b < 0 + 0"
@@ -494,6 +494,10 @@
   then show ?thesis by simp
 qed
 
+lemmas add_sign_intros =
+  add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
+  add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
+
 lemma add_nonneg_eq_0_iff:
   assumes x: "0 \<le> x" and y: "0 \<le> y"
   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
--- a/src/HOL/Presburger.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Presburger.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -7,6 +7,7 @@
 theory Presburger
 imports Groebner_Basis SetInterval
 uses
+  "Tools/Qelim/qelim.ML"
   "Tools/Qelim/cooper_data.ML"
   "Tools/Qelim/generated_cooper.ML"
   ("Tools/Qelim/cooper.ML")
@@ -438,12 +439,7 @@
 
 use "Tools/Qelim/presburger.ML"
 
-declaration {* fn _ =>
-  arith_tactic_add
-    (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st =>
-       (warning "Trying Presburger arithmetic ...";   
-    Presburger.cooper_tac true [] [] ctxt i st)))
-*}
+setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
 
 method_setup presburger = {*
 let
--- a/src/HOL/Ring_and_Field.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -729,11 +729,15 @@
 subclass pordered_semiring ..
 
 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
-by (drule mult_left_mono [of zero b], auto)
+using mult_left_mono [of zero b a] by simp
 
 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
-by (drule mult_left_mono [of b zero], auto)
-
+using mult_left_mono [of b zero a] by simp
+
+lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
+using mult_right_mono [of a zero b] by simp
+
+text {* Legacy - use @{text mult_nonpos_nonneg} *}
 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
 by (drule mult_right_mono [of b zero], auto)
 
@@ -786,31 +790,32 @@
   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
 by (force simp add: mult_strict_right_mono not_less [symmetric])
 
-lemma mult_pos_pos:
-  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
-by (drule mult_strict_left_mono [of zero b], auto)
-
-lemma mult_pos_neg:
-  "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
-by (drule mult_strict_left_mono [of b zero], auto)
-
-lemma mult_pos_neg2:
-  "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
+lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
+using mult_strict_left_mono [of zero b a] by simp
+
+lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
+using mult_strict_left_mono [of b zero a] by simp
+
+lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
+using mult_strict_right_mono [of a zero b] by simp
+
+text {* Legacy - use @{text mult_neg_pos} *}
+lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
 by (drule mult_strict_right_mono [of b zero], auto)
 
 lemma zero_less_mult_pos:
   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
-apply (cases "b\<le>0") 
+apply (cases "b\<le>0")
  apply (auto simp add: le_less not_less)
-apply (drule_tac mult_pos_neg [of a b]) 
+apply (drule_tac mult_pos_neg [of a b])
  apply (auto dest: less_not_sym)
 done
 
 lemma zero_less_mult_pos2:
   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
-apply (cases "b\<le>0") 
+apply (cases "b\<le>0")
  apply (auto simp add: le_less not_less)
-apply (drule_tac mult_pos_neg2 [of a b]) 
+apply (drule_tac mult_pos_neg2 [of a b])
  apply (auto dest: less_not_sym)
 done
 
@@ -819,9 +824,9 @@
   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   shows "a * c < b * d"
   using assms apply (cases "c=0")
-  apply (simp add: mult_pos_pos) 
+  apply (simp add: mult_pos_pos)
   apply (erule mult_strict_right_mono [THEN less_trans])
-  apply (force simp add: le_less) 
+  apply (force simp add: le_less)
   apply (erule mult_strict_left_mono, assumption)
   done
 
@@ -960,9 +965,8 @@
   apply (simp_all add: minus_mult_right [symmetric]) 
   done
 
-lemma mult_nonpos_nonpos:
-  "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
-by (drule mult_right_mono_neg [of a zero b]) auto
+lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
+using mult_right_mono_neg [of a zero b] by simp
 
 lemma split_mult_pos_le:
   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
@@ -1006,21 +1010,14 @@
 
 subclass ordered_ring ..
 
-lemma mult_strict_left_mono_neg:
-  "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
-  apply (drule mult_strict_left_mono [of _ _ "uminus c"])
-  apply (simp_all add: minus_mult_left [symmetric]) 
-  done
-
-lemma mult_strict_right_mono_neg:
-  "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
-  apply (drule mult_strict_right_mono [of _ _ "uminus c"])
-  apply (simp_all add: minus_mult_right [symmetric]) 
-  done
-
-lemma mult_neg_neg:
-  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
-by (drule mult_strict_right_mono_neg, auto)
+lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
+using mult_strict_left_mono [of b a "- c"] by simp
+
+lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
+using mult_strict_right_mono [of b a "- c"] by simp
+
+lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
+using mult_strict_right_mono_neg [of a zero b] by simp
 
 subclass ring_no_zero_divisors
 proof
@@ -1144,11 +1141,6 @@
   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
 by (auto simp: mult_le_cancel_left)
 
-end
-
-context ordered_ring_strict
-begin
-
 lemma mult_less_cancel_left_pos:
   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
 by (auto simp: mult_less_cancel_left)
@@ -1162,6 +1154,11 @@
 text{*Legacy - use @{text algebra_simps} *}
 lemmas ring_simps[noatp] = algebra_simps
 
+lemmas mult_sign_intros =
+  mult_nonneg_nonneg mult_nonneg_nonpos
+  mult_nonpos_nonneg mult_nonpos_nonpos
+  mult_pos_pos mult_pos_neg
+  mult_neg_pos mult_neg_neg
 
 class pordered_comm_ring = comm_ring + pordered_comm_semiring
 begin
--- a/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -172,7 +172,7 @@
 
     (* Canonical linear form for terms, formulae etc.. *)
 fun provelin ctxt t = Goal.prove ctxt [] [] t 
-  (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]);
+  (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
 fun linear_cmul 0 tm = zero 
   | linear_cmul n tm = case tm of  
       Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
--- a/src/HOL/Tools/Qelim/qelim.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/Qelim/qelim.ML
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 
 Generic quantifier elimination conversions for HOL formulae.
@@ -26,11 +25,12 @@
    case (term_of p) of
     Const(s,T)$_$_ => 
        if domain_type T = HOLogic.boolT
-          andalso s mem ["op &","op |","op -->","op ="]
+          andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
+            @{const_name "op -->"}, @{const_name "op ="}] s
        then binop_conv (conv env) p 
        else atcv env p
-  | Const("Not",_)$_ => arg_conv (conv env) p
-  | Const("Ex",_)$Abs(s,_,_) =>
+  | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p
+  | Const(@{const_name "Ex"},_)$Abs(s,_,_) =>
     let
      val (e,p0) = Thm.dest_comb p
      val (x,p') = Thm.dest_abs (SOME s) p0
@@ -41,8 +41,8 @@
      val (l,r) = Thm.dest_equals (cprop_of th')
     in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
        else Thm.transitive (Thm.transitive th th') (conv env r) end
-  | Const("Ex",_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
-  | Const("All",_)$_ =>
+  | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
+  | Const(@{const_name "All"},_)$_ =>
     let
      val p = Thm.dest_arg p
      val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
--- a/src/HOL/Tools/TFL/post.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -55,7 +55,7 @@
   Prim.postprocess strict
    {wf_tac     = REPEAT (ares_tac wfs 1),
     terminator = asm_simp_tac ss 1
-                 THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE
+                 THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE
                            fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1),
     simplifier = Rules.simpl_conv ss []};
 
--- a/src/HOL/Tools/arith_data.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -6,6 +6,11 @@
 
 signature ARITH_DATA =
 sig
+  val arith_tac: Proof.context -> int -> tactic
+  val verbose_arith_tac: Proof.context -> int -> tactic
+  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
+  val get_arith_facts: Proof.context -> thm list
+
   val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
@@ -14,11 +19,54 @@
   val trans_tac: thm option -> tactic
   val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
     -> simproc
+
+  val setup: theory -> theory
 end;
 
 structure Arith_Data: ARITH_DATA =
 struct
 
+(* slots for pluging in arithmetic facts and tactics *)
+
+structure Arith_Facts = NamedThmsFun(
+  val name = "arith"
+  val description = "arith facts - only ground formulas"
+);
+
+val get_arith_facts = Arith_Facts.get;
+
+structure Arith_Tactics = TheoryDataFun
+(
+  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
+  val empty = [];
+  val copy = I;
+  val extend = I;
+  fun merge _ = AList.merge (op =) (K true);
+);
+
+fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
+
+fun gen_arith_tac verbose ctxt =
+  let
+    val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
+    fun invoke (_, (name, tac)) k st = (if verbose
+      then warning ("Trying " ^ name ^ "...") else ();
+      tac verbose ctxt k st);
+  in FIRST' (map invoke (rev tactics)) end;
+
+val arith_tac = gen_arith_tac false;
+val verbose_arith_tac = gen_arith_tac true;
+
+val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
+  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+    THEN' verbose_arith_tac ctxt)));
+
+val setup = Arith_Facts.setup
+  #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
+
+
+(* various auxiliary and legacy *)
+
 fun prove_conv_nohyps tacs ctxt (t, u) =
   if t aconv u then NONE
   else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -197,7 +197,7 @@
               else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
           in
             rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
-            THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
+            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
           end
 
         fun steps_tac MAX strict lq lp =
--- a/src/HOL/Tools/int_arith.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -530,7 +530,7 @@
   :: Int_Numeral_Simprocs.cancel_numerals;
 
 val setup =
-  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
     inj_thms = nat_inj_thms @ inj_thms,
@@ -547,7 +547,7 @@
   "fast_int_arith" 
      ["(m::'a::{ordered_idom,number_ring}) < n",
       "(m::'a::{ordered_idom,number_ring}) <= n",
-      "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
+      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
 
 end;
 
--- a/src/HOL/Tools/int_factor_simprocs.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -232,7 +232,7 @@
       val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
       val pos = less $ zero $ t and neg = less $ t $ zero
       fun prove p =
-        Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
+        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
         handle THM _ => NONE
     in case prove pos of
          SOME th => SOME(th RS pos_th)
--- a/src/HOL/Tools/lin_arith.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -6,13 +6,9 @@
 
 signature BASIC_LIN_ARITH =
 sig
-  type arith_tactic
-  val mk_arith_tactic: string -> (Proof.context -> int -> tactic) -> arith_tactic
-  val eq_arith_tactic: arith_tactic * arith_tactic -> bool
   val arith_split_add: attribute
   val arith_discrete: string -> Context.generic -> Context.generic
   val arith_inj_const: string * typ -> Context.generic -> Context.generic
-  val arith_tactic_add: arith_tactic -> Context.generic -> Context.generic
   val fast_arith_split_limit: int Config.T
   val fast_arith_neq_limit: int Config.T
   val lin_arith_pre_tac: Proof.context -> int -> tactic
@@ -21,9 +17,7 @@
   val trace_arith: bool ref
   val lin_arith_simproc: simpset -> term -> thm option
   val fast_nat_arith_simproc: simproc
-  val simple_arith_tac: Proof.context -> int -> tactic
-  val arith_tac: Proof.context -> int -> tactic
-  val silent_arith_tac: Proof.context -> int -> tactic
+  val linear_arith_tac: Proof.context -> int -> tactic
 end;
 
 signature LIN_ARITH =
@@ -39,7 +33,7 @@
   val setup: Context.generic -> Context.generic
 end;
 
-structure LinArith: LIN_ARITH =
+structure Lin_Arith: LIN_ARITH =
 struct
 
 (* Parameters data for general linear arithmetic functor *)
@@ -72,7 +66,7 @@
   let val _ $ t = Thm.prop_of thm
   in t = Const("False",HOLogic.boolT) end;
 
-fun is_nat(t) = fastype_of1 t = HOLogic.natT;
+fun is_nat t = (fastype_of1 t = HOLogic.natT);
 
 fun mk_nat_thm sg t =
   let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
@@ -83,49 +77,35 @@
 
 (* arith context data *)
 
-datatype arith_tactic =
-  ArithTactic of {name: string, tactic: Proof.context -> int -> tactic, id: stamp};
-
-fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()};
-
-fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
-
 structure ArithContextData = GenericDataFun
 (
   type T = {splits: thm list,
             inj_consts: (string * typ) list,
-            discrete: string list,
-            tactics: arith_tactic list};
-  val empty = {splits = [], inj_consts = [], discrete = [], tactics = []};
+            discrete: string list};
+  val empty = {splits = [], inj_consts = [], discrete = []};
   val extend = I;
   fun merge _
-   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
-    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T =
+   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
+    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
    {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
     inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
-    discrete = Library.merge (op =) (discrete1, discrete2),
-    tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
+    discrete = Library.merge (op =) (discrete1, discrete2)};
 );
 
 val get_arith_data = ArithContextData.get o Context.Proof;
 
 val arith_split_add = Thm.declaration_attribute (fn thm =>
-  ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
+  ArithContextData.map (fn {splits, inj_consts, discrete} =>
     {splits = update Thm.eq_thm_prop thm splits,
-     inj_consts = inj_consts, discrete = discrete, tactics = tactics}));
-
-fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
-  {splits = splits, inj_consts = inj_consts,
-   discrete = update (op =) d discrete, tactics = tactics});
+     inj_consts = inj_consts, discrete = discrete}));
 
-fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
-  {splits = splits, inj_consts = update (op =) c inj_consts,
-   discrete = discrete, tactics= tactics});
+fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+  {splits = splits, inj_consts = inj_consts,
+   discrete = update (op =) d discrete});
 
-fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
-  {splits = splits, inj_consts = inj_consts, discrete = discrete,
-   tactics = update eq_arith_tactic tac tactics});
-
+fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+  {splits = splits, inj_consts = update (op =) c inj_consts,
+   discrete = discrete});
 
 val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9;
 val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9;
@@ -794,7 +774,7 @@
    Most of the work is done by the cancel tactics. *)
 
 val init_arith_data =
- Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
+ map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
    {add_mono_thms = add_mono_thms @
     @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
     mult_mono_thms = mult_mono_thms,
@@ -815,7 +795,7 @@
   arith_discrete "nat";
 
 fun add_arith_facts ss =
-  add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss;
+  add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
 
 val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
 
@@ -895,27 +875,16 @@
     (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
     (fast_ex_arith_tac ctxt ex);
 
-fun more_arith_tacs ctxt =
-  let val tactics = #tactics (get_arith_data ctxt)
-  in FIRST' (map (fn ArithTactic {tactic, ...} => tactic ctxt) tactics) end;
-
 in
 
-fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
-  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true];
-
-fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
-  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true,
-  more_arith_tacs ctxt];
+fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
+  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
 
-fun silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
-  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false,
-  more_arith_tacs ctxt];
+val linear_arith_tac = gen_linear_arith_tac true;
 
-val arith_method = Args.bang_facts >>
-  (fn prems => fn ctxt => METHOD (fn facts =>
-      HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
-      THEN' arith_tac ctxt)));
+val linarith_method = Args.bang_facts >> (fn prems => fn ctxt =>
+  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+    THEN' linear_arith_tac ctxt)));
 
 end;
 
@@ -929,11 +898,12 @@
       (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
   Context.mapping
    (setup_options #>
-    Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
+    Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
+    Method.setup @{binding linarith} linarith_method "linear arithmetic" #>
     Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
       "declaration of split rules for arithmetic procedure") I;
 
 end;
 
-structure BasicLinArith: BASIC_LIN_ARITH = LinArith;
-open BasicLinArith;
+structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
+open Basic_Lin_Arith;
--- a/src/HOL/Tools/nat_simprocs.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -565,7 +565,7 @@
 in
 
 val nat_simprocs_setup =
-  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms, lessD = lessD, neqE = neqE,
     simpset = simpset addsimps add_rules
--- a/src/HOL/Tools/rat_arith.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/rat_arith.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -35,7 +35,7 @@
 in
 
 val rat_arith_setup =
-  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
--- a/src/HOL/Tools/real_arith.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Tools/real_arith.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -29,7 +29,7 @@
 in
 
 val real_arith_setup =
-  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
--- a/src/HOL/Word/WordArith.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/Word/WordArith.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -512,7 +512,7 @@
 
 fun uint_arith_tacs ctxt = 
   let
-    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
+    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
     val cs = local_claset_of ctxt;
     val ss = local_simpset_of ctxt;
   in 
@@ -1075,7 +1075,7 @@
 
 fun unat_arith_tacs ctxt =   
   let
-    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
+    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
     val cs = local_claset_of ctxt;
     val ss = local_simpset_of ctxt;
   in 
--- a/src/HOL/ex/Arith_Examples.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/ex/Arith_Examples.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:  HOL/ex/Arith_Examples.thy
-    ID:     $Id$
     Author: Tjark Weber
 *)
 
@@ -14,13 +13,13 @@
 
   @{ML fast_arith_tac} is a very basic version of the tactic.  It performs no
   meta-to-object-logic conversion, and only some splitting of operators.
-  @{ML simple_arith_tac} performs meta-to-object-logic conversion, full
+  @{ML linear_arith_tac} performs meta-to-object-logic conversion, full
   splitting of operators, and NNF normalization of the goal.  The @{text arith}
   method combines them both, and tries other methods (e.g.~@{text presburger})
   as well.  This is the one that you should use in your proofs!
 
   An @{text arith}-based simproc is available as well (see @{ML
-  LinArith.lin_arith_simproc}), which---for performance
+  Lin_Arith.lin_arith_simproc}), which---for performance
   reasons---however does even less splitting than @{ML fast_arith_tac}
   at the moment (namely inequalities only).  (On the other hand, it
   does take apart conjunctions, which @{ML fast_arith_tac} currently
@@ -83,7 +82,7 @@
   by (tactic {* fast_arith_tac @{context} 1 *})
 
 lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
   by (tactic {* fast_arith_tac @{context} 1 *})
@@ -140,34 +139,34 @@
 subsection {* Meta-Logic *}
 
 lemma "x < Suc y == x <= y"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 
 subsection {* Various Other Examples *}
 
 lemma "(x < Suc y) = (x <= y)"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| (x::nat) < y; y < z |] ==> x < z"
   by (tactic {* fast_arith_tac @{context} 1 *})
 
 lemma "(x::nat) < y & y < z ==> x < z"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 text {* This example involves no arithmetic at all, but is solved by
   preprocessing (i.e. NNF normalization) alone. *}
 
 lemma "(P::bool) = Q ==> Q = P"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
   by (tactic {* fast_arith_tac @{context} 1 *})
@@ -185,7 +184,7 @@
   by (tactic {* fast_arith_tac @{context} 1 *})
 
 lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "(x - y) - (x::nat) = (x - x) - y"
   by (tactic {* fast_arith_tac @{context} 1 *})
@@ -207,7 +206,7 @@
 (*        preprocessing negates the goal and tries to compute its negation *)
 (*        normal form, which creates lots of separate cases for this       *)
 (*        disjunction of conjunctions                                      *)
-(* by (tactic {* simple_arith_tac 1 *}) *)
+(* by (tactic {* linear_arith_tac 1 *}) *)
 oops
 
 lemma "2 * (x::nat) ~= 1"
--- a/src/HOL/ex/ImperativeQuicksort.thy	Tue Mar 24 12:45:01 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,637 +0,0 @@
-theory ImperativeQuicksort
-imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
-begin
-
-text {* We prove QuickSort correct in the Relational Calculus. *}
-
-definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
-where
-  "swap arr i j = (
-     do
-       x \<leftarrow> nth arr i;
-       y \<leftarrow> nth arr j;
-       upd i y arr;
-       upd j x arr;
-       return ()
-     done)"
-
-lemma swap_permutes:
-  assumes "crel (swap a i j) h h' rs"
-  shows "multiset_of (get_array a h') 
-  = multiset_of (get_array a h)"
-  using assms
-  unfolding swap_def
-  by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
-
-function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
-where
-  "part1 a left right p = (
-     if (right \<le> left) then return right
-     else (do
-       v \<leftarrow> nth a left;
-       (if (v \<le> p) then (part1 a (left + 1) right p)
-                    else (do swap a left right;
-  part1 a left (right - 1) p done))
-     done))"
-by pat_completeness auto
-
-termination
-by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
-
-declare part1.simps[simp del]
-
-lemma part_permutes:
-  assumes "crel (part1 a l r p) h h' rs"
-  shows "multiset_of (get_array a h') 
-  = multiset_of (get_array a h)"
-  using assms
-proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
-  case (1 a l r p h h' rs)
-  thus ?case
-    unfolding part1.simps [of a l r p]
-    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
-qed
-
-lemma part_returns_index_in_bounds:
-  assumes "crel (part1 a l r p) h h' rs"
-  assumes "l \<le> r"
-  shows "l \<le> rs \<and> rs \<le> r"
-using assms
-proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
-  case (1 a l r p h h' rs)
-  note cr = `crel (part1 a l r p) h h' rs`
-  show ?case
-  proof (cases "r \<le> l")
-    case True (* Terminating case *)
-    with cr `l \<le> r` show ?thesis
-      unfolding part1.simps[of a l r p]
-      by (elim crelE crel_if crel_return crel_nth) auto
-  next
-    case False (* recursive case *)
-    note rec_condition = this
-    let ?v = "get_array a h ! l"
-    show ?thesis
-    proof (cases "?v \<le> p")
-      case True
-      with cr False
-      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
-        unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
-      from rec_condition have "l + 1 \<le> r" by arith
-      from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
-      show ?thesis by simp
-    next
-      case False
-      with rec_condition cr
-      obtain h1 where swp: "crel (swap a l r) h h1 ()"
-        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
-        unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
-      from rec_condition have "l \<le> r - 1" by arith
-      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
-    qed
-  qed
-qed
-
-lemma part_length_remains:
-  assumes "crel (part1 a l r p) h h' rs"
-  shows "Heap.length a h = Heap.length a h'"
-using assms
-proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
-  case (1 a l r p h h' rs)
-  note cr = `crel (part1 a l r p) h h' rs`
-  
-  show ?case
-  proof (cases "r \<le> l")
-    case True (* Terminating case *)
-    with cr show ?thesis
-      unfolding part1.simps[of a l r p]
-      by (elim crelE crel_if crel_return crel_nth) auto
-  next
-    case False (* recursive case *)
-    with cr 1 show ?thesis
-      unfolding part1.simps [of a l r p] swap_def
-      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
-  qed
-qed
-
-lemma part_outer_remains:
-  assumes "crel (part1 a l r p) h h' rs"
-  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
-  using assms
-proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
-  case (1 a l r p h h' rs)
-  note cr = `crel (part1 a l r p) h h' rs`
-  
-  show ?case
-  proof (cases "r \<le> l")
-    case True (* Terminating case *)
-    with cr show ?thesis
-      unfolding part1.simps[of a l r p]
-      by (elim crelE crel_if crel_return crel_nth) auto
-  next
-    case False (* recursive case *)
-    note rec_condition = this
-    let ?v = "get_array a h ! l"
-    show ?thesis
-    proof (cases "?v \<le> p")
-      case True
-      with cr False
-      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
-        unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
-      from 1(1)[OF rec_condition True rec1]
-      show ?thesis by fastsimp
-    next
-      case False
-      with rec_condition cr
-      obtain h1 where swp: "crel (swap a l r) h h1 ()"
-        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
-        unfolding part1.simps[of a l r p]
-        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"
-	unfolding swap_def
-	by (elim crelE crel_nth crel_upd crel_return) auto
-      with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
-    qed
-  qed
-qed
-
-
-lemma part_partitions:
-  assumes "crel (part1 a l r p) h h' rs"
-  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
-  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
-  using assms
-proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
-  case (1 a l r p h h' rs)
-  note cr = `crel (part1 a l r p) h h' rs`
-  
-  show ?case
-  proof (cases "r \<le> l")
-    case True (* Terminating case *)
-    with cr have "rs = r"
-      unfolding part1.simps[of a l r p]
-      by (elim crelE crel_if crel_return crel_nth) auto
-    with True
-    show ?thesis by auto
-  next
-    case False (* recursive case *)
-    note lr = this
-    let ?v = "get_array a h ! l"
-    show ?thesis
-    proof (cases "?v \<le> p")
-      case True
-      with lr cr
-      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
-        unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
-      from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
-	by fastsimp
-      have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
-      with 1(1)[OF False True rec1] a_l show ?thesis
-	by auto
-    next
-      case False
-      with lr cr
-      obtain h1 where swp: "crel (swap a l r) h h1 ()"
-        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
-        unfolding part1.simps[of a l r p]
-        by (elim crelE crel_nth crel_if crel_return) auto
-      from swp False have "get_array a h1 ! r \<ge> p"
-	unfolding swap_def
-	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
-      with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
-	by fastsimp
-      have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
-      with 1(2)[OF lr False rec2] a_r show ?thesis
-	by auto
-    qed
-  qed
-qed
-
-
-fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
-where
-  "partition a left right = (do
-     pivot \<leftarrow> nth a right;
-     middle \<leftarrow> part1 a left (right - 1) pivot;
-     v \<leftarrow> nth a middle;
-     m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
-     swap a m right;
-     return m
-   done)"
-
-declare partition.simps[simp del]
-
-lemma partition_permutes:
-  assumes "crel (partition a l r) h h' rs"
-  shows "multiset_of (get_array a h') 
-  = multiset_of (get_array a h)"
-proof -
-    from assms part_permutes swap_permutes show ?thesis
-      unfolding partition.simps
-      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
-qed
-
-lemma partition_length_remains:
-  assumes "crel (partition a l r) h h' rs"
-  shows "Heap.length a h = Heap.length a h'"
-proof -
-  from assms part_length_remains show ?thesis
-    unfolding partition.simps swap_def
-    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
-qed
-
-lemma partition_outer_remains:
-  assumes "crel (partition a l r) h h' rs"
-  assumes "l < r"
-  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
-proof -
-  from assms part_outer_remains part_returns_index_in_bounds show ?thesis
-    unfolding partition.simps swap_def
-    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
-qed
-
-lemma partition_returns_index_in_bounds:
-  assumes crel: "crel (partition a l r) h h' rs"
-  assumes "l < r"
-  shows "l \<le> rs \<and> rs \<le> r"
-proof -
-  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
-    and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
-         else middle)"
-    unfolding partition.simps
-    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
-  from `l < r` have "l \<le> r - 1" by arith
-  from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
-qed
-
-lemma partition_partitions:
-  assumes crel: "crel (partition a l r) h h' rs"
-  assumes "l < r"
-  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
-  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
-proof -
-  let ?pivot = "get_array a h ! r" 
-  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
-    and swap: "crel (swap a rs r) h1 h' ()"
-    and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
-         else middle)"
-    unfolding partition.simps
-    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
-  from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
-    (Heap.upd a rs (get_array a h1 ! r) h1)"
-    unfolding swap_def
-    by (elim crelE crel_return crel_nth crel_upd) simp
-  from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
-    unfolding swap_def
-    by (elim crelE crel_return crel_nth crel_upd) simp
-  from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
-    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
-  from `l < r` have "l \<le> r - 1" by simp 
-  note middle_in_bounds = part_returns_index_in_bounds[OF part this]
-  from part_outer_remains[OF part] `l < r`
-  have "get_array a h ! r = get_array a h1 ! r"
-    by fastsimp
-  with swap
-  have right_remains: "get_array a h ! r = get_array a h' ! rs"
-    unfolding swap_def
-    by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
-  from part_partitions [OF part]
-  show ?thesis
-  proof (cases "get_array a h1 ! middle \<le> ?pivot")
-    case True
-    with rs_equals have rs_equals: "rs = middle + 1" by simp
-    { 
-      fix i
-      assume i_is_left: "l \<le> i \<and> i < rs"
-      with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
-      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
-      from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
-      with part_partitions[OF part] right_remains True
-      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
-      with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
-	unfolding Heap.upd_def Heap.length_def by simp
-    }
-    moreover
-    {
-      fix i
-      assume "rs < i \<and> i \<le> r"
-
-      hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
-      hence "get_array a h' ! rs \<le> get_array a h' ! i"
-      proof
-	assume i_is: "rs < i \<and> i \<le> r - 1"
-	with swap_length_remains in_bounds middle_in_bounds rs_equals
-	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
-	from part_partitions[OF part] rs_equals right_remains i_is
-	have "get_array a h' ! rs \<le> get_array a h1 ! i"
-	  by fastsimp
-	with i_props h'_def show ?thesis by fastsimp
-      next
-	assume i_is: "rs < i \<and> i = r"
-	with rs_equals have "Suc middle \<noteq> r" by arith
-	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
-	with part_partitions[OF part] right_remains 
-	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
-	  by fastsimp
-	with i_is True rs_equals right_remains h'_def
-	show ?thesis using in_bounds
-	  unfolding Heap.upd_def Heap.length_def
-	  by auto
-      qed
-    }
-    ultimately show ?thesis by auto
-  next
-    case False
-    with rs_equals have rs_equals: "middle = rs" by simp
-    { 
-      fix i
-      assume i_is_left: "l \<le> i \<and> i < rs"
-      with swap_length_remains in_bounds middle_in_bounds rs_equals
-      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
-      from part_partitions[OF part] rs_equals right_remains i_is_left
-      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
-      with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
-	unfolding Heap.upd_def by simp
-    }
-    moreover
-    {
-      fix i
-      assume "rs < i \<and> i \<le> r"
-      hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
-      hence "get_array a h' ! rs \<le> get_array a h' ! i"
-      proof
-	assume i_is: "rs < i \<and> i \<le> r - 1"
-	with swap_length_remains in_bounds middle_in_bounds rs_equals
-	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
-	from part_partitions[OF part] rs_equals right_remains i_is
-	have "get_array a h' ! rs \<le> get_array a h1 ! i"
-	  by fastsimp
-	with i_props h'_def show ?thesis by fastsimp
-      next
-	assume i_is: "i = r"
-	from i_is False rs_equals right_remains h'_def
-	show ?thesis using in_bounds
-	  unfolding Heap.upd_def Heap.length_def
-	  by auto
-      qed
-    }
-    ultimately
-    show ?thesis by auto
-  qed
-qed
-
-
-function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
-where
-  "quicksort arr left right =
-     (if (right > left)  then
-        do
-          pivotNewIndex \<leftarrow> partition arr left right;
-          pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
-          quicksort arr left (pivotNewIndex - 1);
-          quicksort arr (pivotNewIndex + 1) right
-        done
-     else return ())"
-by pat_completeness auto
-
-(* For termination, we must show that the pivotNewIndex is between left and right *) 
-termination
-by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
-
-declare quicksort.simps[simp del]
-
-
-lemma quicksort_permutes:
-  assumes "crel (quicksort a l r) h h' rs"
-  shows "multiset_of (get_array a h') 
-  = multiset_of (get_array a h)"
-  using assms
-proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
-  case (1 a l r h h' rs)
-  with partition_permutes show ?case
-    unfolding quicksort.simps [of a l r]
-    by (elim crel_if crelE crel_assert crel_return) auto
-qed
-
-lemma length_remains:
-  assumes "crel (quicksort a l r) h h' rs"
-  shows "Heap.length a h = Heap.length a h'"
-using assms
-proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
-  case (1 a l r h h' rs)
-  with partition_length_remains show ?case
-    unfolding quicksort.simps [of a l r]
-    by (elim crel_if crelE crel_assert crel_return) auto
-qed
-
-lemma quicksort_outer_remains:
-  assumes "crel (quicksort a l r) h h' rs"
-   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
-  using assms
-proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
-  case (1 a l r h h' rs)
-  note cr = `crel (quicksort a l r) h h' rs`
-  thus ?case
-  proof (cases "r > l")
-    case False
-    with cr have "h' = h"
-      unfolding quicksort.simps [of a l r]
-      by (elim crel_if crel_return) auto
-    thus ?thesis by simp
-  next
-  case True
-   { 
-      fix h1 h2 p ret1 ret2 i
-      assume part: "crel (partition a l r) h h1 p"
-      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
-      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
-      assume pivot: "l \<le> p \<and> p \<le> r"
-      assume i_outer: "i < l \<or> r < i"
-      from  partition_outer_remains [OF part True] i_outer
-      have "get_array a h !i = get_array a h1 ! i" by fastsimp
-      moreover
-      with 1(1) [OF True pivot qs1] pivot i_outer
-      have "get_array a h1 ! i = get_array a h2 ! i" by auto
-      moreover
-      with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
-      have "get_array a h2 ! i = get_array a h' ! i" by auto
-      ultimately have "get_array a h ! i= get_array a h' ! i" by simp
-    }
-    with cr show ?thesis
-      unfolding quicksort.simps [of a l r]
-      by (elim crel_if crelE crel_assert crel_return) auto
-  qed
-qed
-
-lemma quicksort_is_skip:
-  assumes "crel (quicksort a l r) h h' rs"
-  shows "r \<le> l \<longrightarrow> h = h'"
-  using assms
-  unfolding quicksort.simps [of a l r]
-  by (elim crel_if crel_return) auto
- 
-lemma quicksort_sorts:
-  assumes "crel (quicksort a l r) h h' rs"
-  assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" 
-  shows "sorted (subarray l (r + 1) a h')"
-  using assms
-proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
-  case (1 a l r h h' rs)
-  note cr = `crel (quicksort a l r) h h' rs`
-  thus ?case
-  proof (cases "r > l")
-    case False
-    hence "l \<ge> r + 1 \<or> l = r" by arith 
-    with length_remains[OF cr] 1(5) show ?thesis
-      by (auto simp add: subarray_Nil subarray_single)
-  next
-    case True
-    { 
-      fix h1 h2 p
-      assume part: "crel (partition a l r) h h1 p"
-      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
-      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
-      from partition_returns_index_in_bounds [OF part True]
-      have pivot: "l\<le> p \<and> p \<le> r" .
-     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. *)
-      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
-      have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
-	by (simp add: subarray_eq_samelength_iff)
-      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. *)
-      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)
-      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"]
-      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> *)
-      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'"]
-      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
-      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. *)
-      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
-	unfolding subarray_def
-	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
-	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
-    }
-    with True cr show ?thesis
-      unfolding quicksort.simps [of a l r]
-      by (elim crel_if crel_return crelE crel_assert) auto
-  qed
-qed
-
-
-lemma quicksort_is_sort:
-  assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
-  shows "get_array a h' = sort (get_array a h)"
-proof (cases "get_array a h = []")
-  case True
-  with quicksort_is_skip[OF crel] show ?thesis
-  unfolding Heap.length_def by simp
-next
-  case False
-  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
-    unfolding Heap.length_def subarray_def by auto
-  with length_remains[OF crel] have "sorted (get_array a h')"
-    unfolding Heap.length_def by simp
-  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
-qed
-
-subsection {* No Errors in quicksort *}
-text {* We have proved that quicksort sorts (if no exceptions occur).
-We will now show that exceptions do not occur. *}
-
-lemma noError_part1: 
-  assumes "l < Heap.length a h" "r < Heap.length a h"
-  shows "noError (part1 a l r p) h"
-  using assms
-proof (induct a l r p arbitrary: h rule: part1.induct)
-  case (1 a l r p)
-  thus ?case
-    unfolding part1.simps [of a l r] swap_def
-    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
-qed
-
-lemma noError_partition:
-  assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
-  shows "noError (partition a l r) h"
-using assms
-unfolding partition.simps swap_def
-apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
-apply (frule part_length_remains)
-apply (frule part_returns_index_in_bounds)
-apply auto
-apply (frule part_length_remains)
-apply (frule part_returns_index_in_bounds)
-apply auto
-apply (frule part_length_remains)
-apply auto
-done
-
-lemma noError_quicksort:
-  assumes "l < Heap.length a h" "r < Heap.length a h"
-  shows "noError (quicksort a l r) h"
-using assms
-proof (induct a l r arbitrary: h rule: quicksort.induct)
-  case (1 a l ri h)
-  thus ?case
-    unfolding quicksort.simps [of a l ri]
-    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
-    apply (frule partition_returns_index_in_bounds)
-    apply auto
-    apply (frule partition_returns_index_in_bounds)
-    apply auto
-    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
-    apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
-    apply (erule disjE)
-    apply auto
-    unfolding quicksort.simps [of a "Suc ri" ri]
-    apply (auto intro!: noError_if noError_return)
-    done
-qed
-
-
-subsection {* Example *}
-
-definition "qsort a = do
-    k \<leftarrow> length a;
-    quicksort a 0 (k - 1);
-    return a
-  done"
-
-ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
-
-export_code qsort in SML_imp module_name QSort
-export_code qsort in OCaml module_name QSort file -
-export_code qsort in OCaml_imp module_name QSort file -
-export_code qsort in Haskell module_name QSort file -
-
-end
\ No newline at end of file
--- a/src/HOL/ex/MergeSort.thy	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/ex/MergeSort.thy	Tue Mar 24 12:45:23 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Merge.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2002 TU Muenchen
 *)
--- a/src/HOL/ex/ROOT.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/HOL/ex/ROOT.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -21,7 +21,6 @@
 
 use_thys [
   "Numeral",
-  "ImperativeQuicksort",
   "Higher_Order_Logic",
   "Abstract_NAT",
   "Guess",
--- a/src/HOL/ex/Subarray.thy	Tue Mar 24 12:45:01 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-theory Subarray
-imports Array Sublist
-begin
-
-definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
-where
-  "subarray n m a h \<equiv> sublist' n m (get_array a h)"
-
-lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
-apply (simp add: subarray_def Heap.upd_def)
-apply (simp add: sublist'_update1)
-done
-
-lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
-apply (simp add: subarray_def Heap.upd_def)
-apply (subst sublist'_update2)
-apply fastsimp
-apply simp
-done
-
-lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]"
-unfolding subarray_def Heap.upd_def
-by (simp add: sublist'_update3)
-
-lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
-by (simp add: subarray_def sublist'_Nil')
-
-lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]" 
-by (simp add: subarray_def Heap.length_def sublist'_single)
-
-lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
-by (simp add: subarray_def Heap.length_def length_sublist')
-
-lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
-by (simp add: length_subarray)
-
-lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
-unfolding Heap.length_def subarray_def
-by (simp add: sublist'_front)
-
-lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
-unfolding Heap.length_def subarray_def
-by (simp add: sublist'_back)
-
-lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
-unfolding subarray_def
-by (simp add: sublist'_append)
-
-lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
-unfolding Heap.length_def subarray_def
-by (simp add: sublist'_all)
-
-lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
-unfolding Heap.length_def subarray_def
-by (simp add: nth_sublist')
-
-lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
-unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
-
-lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
-unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
-
-lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
-unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
-
-end
\ No newline at end of file
--- a/src/HOL/ex/Sublist.thy	Tue Mar 24 12:45:01 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,505 +0,0 @@
-(* $Id$ *)
-
-header {* Slices of lists *}
-
-theory Sublist
-imports Multiset
-begin
-
-
-lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
-apply (induct xs arbitrary: i j k)
-apply simp
-apply (simp only: sublist_Cons)
-apply simp
-apply safe
-apply simp
-apply (erule_tac x="0" in meta_allE)
-apply (erule_tac x="j - 1" in meta_allE)
-apply (erule_tac x="k - 1" in meta_allE)
-apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
-apply simp
-apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
-apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
-apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
-apply simp
-apply fastsimp
-apply fastsimp
-apply fastsimp
-apply fastsimp
-apply (erule_tac x="i - 1" in meta_allE)
-apply (erule_tac x="j - 1" in meta_allE)
-apply (erule_tac x="k - 1" in meta_allE)
-apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
-apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
-apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
-apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
-apply simp
-apply fastsimp
-apply fastsimp
-apply fastsimp
-apply fastsimp
-done
-
-lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
-apply (induct xs arbitrary: i inds)
-apply simp
-apply (case_tac i)
-apply (simp add: sublist_Cons)
-apply (simp add: sublist_Cons)
-done
-
-lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
-proof (induct xs arbitrary: i inds)
-  case Nil thus ?case by simp
-next
-  case (Cons x xs)
-  thus ?case
-  proof (cases i)
-    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
-  next
-    case (Suc i')
-    with Cons show ?thesis
-      apply simp
-      apply (simp add: sublist_Cons)
-      apply auto
-      apply (auto simp add: nat.split)
-      apply (simp add: card_less_Suc[symmetric])
-      apply (simp add: card_less_Suc2)
-      done
-  qed
-qed
-
-lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
-by (simp add: sublist_update1 sublist_update2)
-
-lemma sublist_take: "sublist xs {j. j < m} = take m xs"
-apply (induct xs arbitrary: m)
-apply simp
-apply (case_tac m)
-apply simp
-apply (simp add: sublist_Cons)
-done
-
-lemma sublist_take': "sublist xs {0..<m} = take m xs"
-apply (induct xs arbitrary: m)
-apply simp
-apply (case_tac m)
-apply simp
-apply (simp add: sublist_Cons sublist_take)
-done
-
-lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
-apply (induct xs)
-apply simp
-apply (simp add: sublist_Cons)
-done
-
-lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
-apply (induct xs)
-apply simp
-apply (simp add: sublist_Cons)
-done
-
-lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
-apply (induct xs arbitrary: a)
-apply simp
-apply(case_tac aa)
-apply simp
-apply (simp add: sublist_Cons)
-apply simp
-apply (simp add: sublist_Cons)
-done
-
-lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
-apply (induct xs arbitrary: inds)
-apply simp
-apply (simp add: sublist_Cons)
-apply auto
-apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply auto
-done
-
-lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
-apply (induct xs arbitrary: inds)
-apply simp
-apply (simp add: sublist_Cons)
-apply (auto split: if_splits)
-apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply (case_tac x, auto)
-done
-
-lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
-apply (induct xs arbitrary: inds)
-apply simp
-apply (simp add: sublist_Cons)
-apply auto
-apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply (case_tac x, auto)
-done
-
-lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
-apply (induct xs arbitrary: ys inds inds')
-apply simp
-apply (drule sym, rule sym)
-apply (simp add: sublist_Nil, fastsimp)
-apply (case_tac ys)
-apply (simp add: sublist_Nil, fastsimp)
-apply (auto simp add: sublist_Cons)
-apply (erule_tac x="list" in meta_allE)
-apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
-apply fastsimp
-apply (erule_tac x="list" in meta_allE)
-apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
-apply fastsimp
-done
-
-lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
-apply (induct xs arbitrary: ys inds)
-apply simp
-apply (rule sym, simp add: sublist_Nil)
-apply (case_tac ys)
-apply (simp add: sublist_Nil)
-apply (auto simp add: sublist_Cons)
-apply (erule_tac x="list" in meta_allE)
-apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply fastsimp
-apply (erule_tac x="list" in meta_allE)
-apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply fastsimp
-done
-
-lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
-by (rule sublist_eq, auto)
-
-lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
-apply (induct xs arbitrary: ys inds)
-apply simp
-apply (rule sym, simp add: sublist_Nil)
-apply (case_tac ys)
-apply (simp add: sublist_Nil)
-apply (auto simp add: sublist_Cons)
-apply (case_tac i)
-apply auto
-apply (case_tac i)
-apply auto
-done
-
-section {* Another sublist function *}
-
-function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "sublist' n m [] = []"
-| "sublist' n 0 xs = []"
-| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
-| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
-by pat_completeness auto
-termination by lexicographic_order
-
-subsection {* Proving equivalence to the other sublist command *}
-
-lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
-apply (induct xs arbitrary: n m)
-apply simp
-apply (case_tac n)
-apply (case_tac m)
-apply simp
-apply (simp add: sublist_Cons)
-apply (case_tac m)
-apply simp
-apply (simp add: sublist_Cons)
-done
-
-
-lemma "sublist' n m xs = sublist xs {n..<m}"
-apply (induct xs arbitrary: n m)
-apply simp
-apply (case_tac n, case_tac m)
-apply simp
-apply simp
-apply (simp add: sublist_take')
-apply (case_tac m)
-apply simp
-apply (simp add: sublist_Cons sublist'_sublist)
-done
-
-
-subsection {* Showing equivalence to use of drop and take for definition *}
-
-lemma "sublist' n m xs = take (m - n) (drop n xs)"
-apply (induct xs arbitrary: n m)
-apply simp
-apply (case_tac m)
-apply simp
-apply (case_tac n)
-apply simp
-apply simp
-done
-
-subsection {* General lemma about sublist *}
-
-lemma sublist'_Nil[simp]: "sublist' i j [] = []"
-by simp
-
-lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow>  sublist' i' j xs)"
-by (cases i) auto
-
-lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
-apply (cases j)
-apply auto
-apply (cases i)
-apply auto
-done
-
-lemma sublist_n_0: "sublist' n 0 xs = []"
-by (induct xs, auto)
-
-lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
-apply (induct xs arbitrary: n m)
-apply simp
-apply (case_tac m)
-apply simp
-apply (case_tac n)
-apply simp
-apply simp
-done
-
-lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
-apply (induct xs arbitrary: n m)
-apply simp
-apply (case_tac m)
-apply simp
-apply (case_tac n)
-apply simp
-apply simp
-done
-
-lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
-apply (induct xs arbitrary: n m)
-apply simp
-apply (case_tac m)
-apply simp
-apply (case_tac n)
-apply simp
-apply simp
-done
-
-lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
-apply (induct xs arbitrary: n m)
-apply simp
-apply (case_tac m)
-apply simp
-apply (case_tac n)
-apply simp
-apply simp
-done
-
-lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
-apply (induct xs arbitrary: n)
-apply simp
-apply simp
-apply (case_tac n)
-apply (simp add: sublist_n_0)
-apply simp
-done
-
-lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
-apply (induct xs arbitrary: n m i)
-apply simp
-apply simp
-apply (case_tac i)
-apply simp
-apply simp
-done
-
-lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
-apply (induct xs arbitrary: n m i)
-apply simp
-apply simp
-apply (case_tac i)
-apply simp
-apply simp
-done
-
-lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
-proof (induct xs arbitrary: n m i)
-  case Nil thus ?case by auto
-next
-  case (Cons x xs)
-  thus ?case
-    apply -
-    apply auto
-    apply (cases i)
-    apply auto
-    apply (cases i)
-    apply auto
-    done
-qed
-
-lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
-proof (induct xs arbitrary: i j ys n m)
-  case Nil
-  thus ?case
-    apply -
-    apply (rule sym, drule sym)
-    apply (simp add: sublist'_Nil)
-    apply (simp add: sublist'_Nil3)
-    apply arith
-    done
-next
-  case (Cons x xs i j ys n m)
-  note c = this
-  thus ?case
-  proof (cases m)
-    case 0 thus ?thesis by (simp add: sublist_n_0)
-  next
-    case (Suc m')
-    note a = this
-    thus ?thesis
-    proof (cases n)
-      case 0 note b = this
-      show ?thesis
-      proof (cases ys)
-	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
-      next
-	case (Cons y ys)
-	show ?thesis
-	proof (cases j)
-	  case 0 with a b Cons.prems show ?thesis by simp
-	next
-	  case (Suc j') with a b Cons.prems Cons show ?thesis 
-	    apply -
-	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
-	    done
-	qed
-      qed
-    next
-      case (Suc n')
-      show ?thesis
-      proof (cases ys)
-	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
-      next
-	case (Cons y ys) with Suc a Cons.prems show ?thesis
-	  apply -
-	  apply simp
-	  apply (cases j)
-	  apply simp
-	  apply (cases i)
-	  apply simp
-	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
-	  apply simp
-	  apply simp
-	  apply simp
-	  apply simp
-	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
-	  apply simp
-	  apply simp
-	  apply simp
-	  done
-      qed
-    qed
-  qed
-qed
-
-lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
-by (induct xs arbitrary: i j, auto)
-
-lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
-apply (induct xs arbitrary: a i j)
-apply simp
-apply (case_tac j)
-apply simp
-apply (case_tac i)
-apply simp
-apply simp
-done
-
-lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
-apply (induct xs arbitrary: a i j)
-apply simp
-apply simp
-apply (case_tac j)
-apply simp
-apply auto
-apply (case_tac nat)
-apply auto
-done
-
-(* suffices that j \<le> length xs and length ys *) 
-lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs  = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
-proof (induct xs arbitrary: ys i j)
-  case Nil thus ?case by simp
-next
-  case (Cons x xs)
-  thus ?case
-    apply -
-    apply (cases ys)
-    apply simp
-    apply simp
-    apply auto
-    apply (case_tac i', auto)
-    apply (erule_tac x="Suc i'" in allE, auto)
-    apply (erule_tac x="i' - 1" in allE, auto)
-    apply (case_tac i', auto)
-    apply (erule_tac x="Suc i'" in allE, auto)
-    done
-qed
-
-lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
-by (induct xs, auto)
-
-lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
-by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
-
-lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
-by (induct xs arbitrary: i j k) auto
-
-lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
-apply (induct xs arbitrary: i j k)
-apply auto
-apply (case_tac k)
-apply auto
-apply (case_tac i)
-apply auto
-done
-
-lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
-apply (simp add: sublist'_sublist)
-apply (simp add: set_sublist)
-apply auto
-done
-
-lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
-unfolding set_sublist' by blast
-
-lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
-unfolding set_sublist' by blast
-
-
-lemma multiset_of_sublist:
-assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
-assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
-assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
-assumes multiset: "multiset_of xs = multiset_of ys"
-  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
-proof -
-  from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
-    by (simp add: sublist'_append)
-  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
-  with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
-    by (simp add: sublist'_append)
-  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
-  moreover
-  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
-    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
-  moreover
-  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
-    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
-  moreover
-  ultimately show ?thesis by (simp add: multiset_of_append)
-qed
-
-
-end
--- a/src/Provers/Arith/fast_lin_arith.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -466,7 +466,7 @@
                      NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
                                handle Option =>
                                (trace_thm "" thm1; trace_thm "" thm2;
-                                sys_error "Lin.arith. failed to add thms")
+                                sys_error "Linear arithmetic: failed to add thms")
                              )
                    | SOME thm => thm)
         | SOME thm => thm;
@@ -588,8 +588,8 @@
           handle NoEx => NONE
       in
         case ex of
-          SOME s => (warning "arith failed - see trace for a counterexample"; tracing s)
-        | NONE => warning "arith failed"
+          SOME s => (warning "Linear arithmetic failed - see trace for a counterexample."; tracing s)
+        | NONE => warning "Linear arithmetic failed"
       end;
 
 (* ------------------------------------------------------------------------- *)
--- a/src/Pure/Concurrent/future.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -212,7 +212,8 @@
     val _ = if continue then () else scheduler := NONE;
 
     val _ = notify_all ();
-    val _ = interruptible (fn () => wait_timeout (Time.fromSeconds 1)) ()
+    val _ = interruptible (fn () =>
+        wait_timeout (Time.fromMilliseconds (if null (! canceled) then 1000 else 50))) ()
       handle Exn.Interrupt => List.app do_cancel (Task_Queue.cancel_all (! queue));
   in continue end;
 
--- a/src/Pure/General/antiquote.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -11,11 +11,12 @@
     Antiq of Symbol_Pos.T list * Position.T |
     Open of Position.T |
     Close of Position.T
-  val is_antiq: 'a antiquote -> bool
+  val is_text: 'a antiquote -> bool
+  val report: ('a -> unit) -> 'a antiquote -> unit
+  val check_nesting: 'a antiquote list -> unit
   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
   val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
-  val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
-    Symbol_Pos.T list * Position.T -> 'a antiquote list
+  val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
 end;
 
 structure Antiquote: ANTIQUOTE =
@@ -29,8 +30,18 @@
   Open of Position.T |
   Close of Position.T;
 
-fun is_antiq (Text _) = false
-  | is_antiq _ = true;
+fun is_text (Text _) = true
+  | is_text _ = false;
+
+
+(* report *)
+
+val report_antiq = Position.report Markup.antiq;
+
+fun report report_text (Text x) = report_text x
+  | report _ (Antiq (_, pos)) = report_antiq pos
+  | report _ (Open pos) = report_antiq pos
+  | report _ (Close pos) = report_antiq pos;
 
 
 (* check_nesting *)
@@ -83,12 +94,9 @@
 
 (* read *)
 
-fun read _ _ ([], _) = []
-  | read report scanner (syms, pos) =
-      (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
-        SOME xs =>
-         (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
-          check_nesting xs; xs)
-      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
+fun read (syms, pos) =
+  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
+    SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
+  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
 end;
--- a/src/Pure/General/pretty.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/General/pretty.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -104,9 +104,9 @@
 (** printing items: compound phrases, strings, and breaks **)
 
 datatype T =
-  Block of Markup.T * T list * int * int |  (*markup, body, indentation, length*)
-  String of output * int |                  (*text, length*)
-  Break of bool * int;                      (*mandatory flag, width if not taken*)
+  Block of (output * output) * T list * int * int |  (*markup output, body, indentation, length*)
+  String of output * int |                           (*text, length*)
+  Break of bool * int;                               (*mandatory flag, width if not taken*)
 
 fun length (Block (_, _, _, len)) = len
   | length (String (_, len)) = len
@@ -124,12 +124,14 @@
 fun breaks prts = Library.separate (brk 1) prts;
 fun fbreaks prts = Library.separate fbrk prts;
 
-fun markup_block m (indent, es) =
+fun block_markup m (indent, es) =
   let
     fun sum [] k = k
       | sum (e :: es) k = sum es (length e + k);
   in Block (m, es, indent, sum es 0) end;
 
+fun markup_block m arg = block_markup (Markup.output m) arg;
+
 val blk = markup_block Markup.none;
 fun block prts = blk (2, prts);
 val strs = block o breaks o map str;
@@ -197,7 +199,7 @@
 local
   fun pruning dp (Block (m, bes, indent, wd)) =
         if dp > 0
-        then markup_block m (indent, map (pruning (dp - 1)) bes)
+        then block_markup m (indent, map (pruning (dp - 1)) bes)
         else str "..."
     | pruning dp e = e
 in
@@ -263,7 +265,7 @@
 fun format ([], _, _) text = text
   | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
       (case e of
-        Block (markup, bes, indent, wd) =>
+        Block ((bg, en), bes, indent, wd) =>
           let
             val {emergencypos, ...} = ! margin_info;
             val pos' = pos + indent;
@@ -271,7 +273,6 @@
             val block' =
               if pos' < emergencypos then (ind |> add_indent indent, pos')
               else (add_indent pos'' Buffer.empty, pos'');
-            val (bg, en) = Markup.output markup;
             val btext: text = text
               |> control bg
               |> format (bes, block', breakdist (es, after))
@@ -303,9 +304,9 @@
 (*symbolic markup -- no formatting*)
 fun symbolic prt =
   let
-    fun out (Block (m, [], _, _)) = Buffer.markup m I
-      | out (Block (m, prts, indent, _)) =
-          Buffer.markup m (Buffer.markup (Markup.block indent) (fold out prts))
+    fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
+      | out (Block ((bg, en), prts, indent, _)) =
+          Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
       | out (String (s, _)) = Buffer.add s
       | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
       | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
@@ -314,7 +315,7 @@
 (*unformatted output*)
 fun unformatted prt =
   let
-    fun fmt (Block (m, prts, _, _)) = Buffer.markup m (fold fmt prts)
+    fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
       | fmt (String (s, _)) = Buffer.add s
       | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
       | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
@@ -323,11 +324,11 @@
 
 (* ML toplevel pretty printing *)
 
-fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (Markup.output m, map to_ML prts, ind)
+fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
   | to_ML (String s) = ML_Pretty.String s
   | to_ML (Break b) = ML_Pretty.Break b;
 
-fun from_ML (ML_Pretty.Block (_, prts, ind)) = blk (ind, map from_ML prts)
+fun from_ML (ML_Pretty.Block (m, prts, ind)) = block_markup m (ind, map from_ML prts)
   | from_ML (ML_Pretty.String s) = String s
   | from_ML (ML_Pretty.Break b) = Break b;
 
--- a/src/Pure/IsaMakefile	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/IsaMakefile	Tue Mar 24 12:45:23 2009 +0100
@@ -69,7 +69,7 @@
   Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML	\
   Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML		\
   ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
-  ML/ml_thms.ML ML-Systems/install_pp_polyml.ML				\
+  ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
   ML-Systems/install_pp_polyml-experimental.ML Proof/extraction.ML	\
   Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
   Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML	\
--- a/src/Pure/Isar/code_unit.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/Isar/code_unit.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -218,7 +218,7 @@
     |> burrow_thms (canonical_tvars thy purify_tvar)
     |> map (canonical_vars thy purify_var)
     |> map (canonical_absvars purify_var)
-    |> map Drule.zero_var_indexes
+    |> Drule.zero_var_indexes_list
   end;
 
 
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -72,6 +72,10 @@
 
 (* toplevel pretty printing *)
 
+fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
+  | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
+  | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+
 fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
   | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
   | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
--- a/src/Pure/ML/ml_context.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -29,6 +29,8 @@
       (Proof.context -> string * string) * Proof.context
   val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
   val trace: bool ref
+  val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
+    Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
     Position.T -> Symbol_Pos.text -> unit
   val eval: bool -> Position.T -> Symbol_Pos.text -> unit
@@ -190,45 +192,44 @@
   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
 
 val struct_name = "Isabelle";
+val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n");
+val end_env = ML_Lex.tokenize "end;";
 
-fun eval_antiquotes (txt, pos) opt_context =
+in
+
+fun eval_antiquotes (ants, pos) opt_context =
   let
-    val syms = Symbol_Pos.explode (txt, pos);
-    val ants = Antiquote.read ML_Lex.report_token ML_Lex.scan_antiq (syms, pos);
     val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
     val ((ml_env, ml_body), opt_ctxt') =
-      if not (exists Antiquote.is_antiq ants)
-      then (("", Symbol.escape (Symbol_Pos.content syms)), opt_ctxt)
+      if forall Antiquote.is_text ants
+      then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
       else
         let
           val ctxt =
             (case opt_ctxt of
-              NONE => error ("Unknown context -- cannot expand ML antiquotations" ^
-                Position.str_of pos)
+              NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos)
             | SOME ctxt => Context.proof_of ctxt);
 
           val lex = #1 (OuterKeyword.get_lexicons ());
-          fun no_decl _ = ("", "");
+          fun no_decl _ = ([], []);
 
-          fun expand (Antiquote.Text tok) state =
-                (K ("", Symbol.escape (ML_Lex.content_of tok)), state)
+          fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
             | expand (Antiquote.Antiq x) (scope, background) =
                 let
                   val context = Stack.top scope;
                   val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
                   val (decl, background') = f {background = background, struct_name = struct_name};
-                in (decl, (Stack.map_top (K context') scope, background')) end
+                  val decl' = pairself ML_Lex.tokenize o decl;
+                in (decl', (Stack.map_top (K context') scope, background')) end
             | expand (Antiquote.Open _) (scope, background) =
                 (no_decl, (Stack.push scope, background))
             | expand (Antiquote.Close _) (scope, background) =
                 (no_decl, (Stack.pop scope, background));
 
           val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
-          val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself implode;
+          val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
         in (ml, SOME (Context.Proof ctxt')) end;
-  in (("structure " ^ struct_name ^ " =\nstruct\n" ^ ml_env ^ "end;", ml_body), opt_ctxt') end;
-
-in
+  in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
 
 val trace = ref false;
 
@@ -239,13 +240,15 @@
 
     (*prepare source text*)
     val _ = Position.report Markup.ML_source pos;
-    val ((env, body), env_ctxt) = eval_antiquotes (txt, pos) (Context.thread_data ());
+    val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
+    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ())
+      |>> pairself (implode o map ML_Lex.text_of);
     val _ = if ! trace then tracing (cat_lines [env, body]) else ();
 
     (*prepare static ML environment*)
     val _ = Context.setmp_thread_data env_ctxt
         (fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
-      |> (fn NONE => () | SOME context' => Context.>> (ML_Env.put (ML_Env.get context')));
+      |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
 
     (*eval ML*)
     val _ = eval_raw pos verbose body;
--- a/src/Pure/ML/ml_lex.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -13,17 +13,17 @@
   val stopper: token Scan.stopper
   val is_regular: token -> bool
   val is_improper: token -> bool
-  val pos_of: token -> string
+  val pos_of: token -> Position.T
   val kind_of: token -> token_kind
   val content_of: token -> string
-  val markup_of: token -> Markup.T
+  val text_of: token -> string
   val report_token: token -> unit
   val keywords: string list
-  val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
   val tokenize: string -> token list
+  val read_antiq: Symbol_Pos.T list * Position.T -> token Antiquote.antiquote list
 end;
 
 structure ML_Lex: ML_LEX =
@@ -42,10 +42,8 @@
 
 (* position *)
 
-fun position_of (Token ((pos, _), _)) = pos;
-fun end_position_of (Token ((_, pos), _)) = pos;
-
-val pos_of = Position.str_of o position_of;
+fun pos_of (Token ((pos, _), _)) = pos;
+fun end_pos_of (Token ((_, pos), _)) = pos;
 
 
 (* control tokens *)
@@ -57,7 +55,7 @@
   | is_eof _ = false;
 
 val stopper =
-  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* token content *)
@@ -67,6 +65,11 @@
 
 fun kind_of (Token (_, (k, _))) = k;
 
+fun text_of tok =
+  (case kind_of tok of
+    Error msg => error msg
+  | _ => Symbol.escape (content_of tok));
+
 fun is_regular (Token (_, (Error _, _))) = false
   | is_regular (Token (_, (EOF, _))) = false
   | is_regular _ = true;
@@ -78,22 +81,23 @@
 
 (* markup *)
 
-val markup_of = kind_of #>
-  (fn Keyword   => Markup.ML_keyword
-    | Ident     => Markup.ML_ident
-    | LongIdent => Markup.ML_ident
-    | TypeVar   => Markup.ML_tvar
-    | Word      => Markup.ML_numeral
-    | Int       => Markup.ML_numeral
-    | Real      => Markup.ML_numeral
-    | Char      => Markup.ML_char
-    | String    => Markup.ML_string
-    | Space     => Markup.none
-    | Comment   => Markup.ML_comment
-    | Error _   => Markup.ML_malformed
-    | EOF       => Markup.none);
+val token_kind_markup =
+ fn Keyword   => Markup.ML_keyword
+  | Ident     => Markup.ML_ident
+  | LongIdent => Markup.ML_ident
+  | TypeVar   => Markup.ML_tvar
+  | Word      => Markup.ML_numeral
+  | Int       => Markup.ML_numeral
+  | Real      => Markup.ML_numeral
+  | Char      => Markup.ML_char
+  | String    => Markup.ML_string
+  | Space     => Markup.none
+  | Comment   => Markup.ML_comment
+  | Error _   => Markup.ML_malformed
+  | EOF       => Markup.none;
 
-fun report_token tok = Position.report (markup_of tok) (position_of tok);
+fun report_token (Token ((pos, _), (kind, _))) =
+  Position.report (token_kind_markup kind) pos;
 
 
 
@@ -204,7 +208,7 @@
 end;
 
 
-(* token source *)
+(* scan tokens *)
 
 local
 
@@ -224,20 +228,31 @@
     scan_ident >> token Ident ||
     scan_typevar >> token TypeVar));
 
+val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
+
 fun recover msg =
   Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
   >> (fn cs => [token (Error msg) cs]);
 
 in
 
-val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
-
 fun source src =
   Symbol_Pos.source (Position.line 1) src
   |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
 
 val tokenize = Source.of_string #> source #> Source.exhaust;
 
+fun read_antiq (syms, pos) =
+  (Source.of_list syms
+    |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
+      (SOME (false, fn msg => recover msg >> map Antiquote.Text))
+    |> Source.exhaust
+    |> tap (List.app (Antiquote.report report_token))
+    |> tap Antiquote.check_nesting
+    |> tap (List.app (fn Antiquote.Text tok => ignore (text_of tok) | _ => ())))
+  handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
+
 end;
 
 end;
--- a/src/Pure/ML/ml_parse.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -20,7 +20,7 @@
 fun !!! scan =
   let
     fun get_pos [] = " (past end-of-file!)"
-      | get_pos (tok :: _) = T.pos_of tok;
+      | get_pos (tok :: _) = Position.str_of (T.pos_of tok);
 
     fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
       | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_test.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -0,0 +1,120 @@
+(*  Title:      Pure/ML/ml_test.ML
+    Author:     Makarius
+
+Test of advanced ML compiler invocation in Poly/ML 5.3.
+*)
+
+signature ML_TEST =
+sig
+  val get_result: Proof.context -> PolyML.parseTree list
+  val eval: bool -> bool -> Position.T -> ML_Lex.token list -> unit
+end
+
+structure ML_Test: ML_TEST =
+struct
+
+(* eval ML source tokens *)
+
+structure Result = GenericDataFun
+(
+  type T = PolyML.parseTree list;
+  val empty = [];
+  fun extend _ = [];
+  fun merge _ _ = [];
+);
+
+val get_result = Result.get o Context.Proof;
+
+fun eval do_run verbose pos toks =
+  let
+    val (print, err) = Output.ml_output;
+
+    val input = toks |> map (fn tok =>
+      (serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok)));
+    val index_pos = Inttab.lookup (Inttab.make (map (apsnd snd) input));
+
+    fun pos_of ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
+      (case (index_pos i, index_pos j) of
+        (SOME p, SOME q) => Position.encode_range (p, q)
+      | (SOME p, NONE) => p
+      | _ => Position.line_file line file);
+
+    val in_buffer = ref (map (apsnd fst) input);
+    val current_line = ref (the_default 1 (Position.line_of pos));
+    fun get () =
+      (case ! in_buffer of
+        [] => NONE
+      | (_, []) :: rest => (in_buffer := rest; get ())
+      | (i, c :: cs) :: rest =>
+          (in_buffer := (i, cs) :: rest;
+           if c = #"\n" then current_line := ! current_line + 1 else ();
+           SOME c));
+    fun get_index () = (case ! in_buffer of [] => 0 | (i, _) :: _ => i);
+
+    val out_buffer = ref ([]: string list);
+    fun put s = out_buffer := s :: ! out_buffer;
+    fun output () = implode (rev (! out_buffer));
+
+    fun put_message {message, hard, location, context = _} =
+     (put (if hard then "Error: " else "Warning: ");
+      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
+      put (Position.str_of (pos_of location) ^ "\n"));
+
+    fun result_fun (parse_tree, code) () =
+     (Context.>> (Result.map (append (the_list parse_tree)));
+      if is_none code then warning "Static Errors" else ());
+
+    val parameters =
+     [PolyML.Compiler.CPOutStream put,
+      PolyML.Compiler.CPNameSpace ML_Context.name_space,
+      PolyML.Compiler.CPErrorMessageProc put_message,
+      PolyML.Compiler.CPLineNo (fn () => ! current_line),
+      PolyML.Compiler.CPLineOffset get_index,
+      PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+     (if do_run then [] else [PolyML.Compiler.CPCompilerResultFun result_fun]);
+    val _ =
+      (while not (List.null (! in_buffer)) do
+        PolyML.compiler (get, parameters) ())
+      handle exn =>
+       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+        err (output ()); raise exn);
+  in if verbose then print (output ()) else () end;
+
+
+(* ML test command *)
+
+fun ML_test do_run (txt, pos) =
+  let
+    val _ = Position.report Markup.ML_source pos;
+    val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
+    val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
+
+    val _ = Context.setmp_thread_data env_ctxt
+        (fn () => (eval true false Position.none env; Context.thread_data ())) ()
+      |> (fn NONE => () | SOME context' => Context.>> (ML_Context.inherit_env context'));
+    val _ = eval do_run true pos body;
+    val _ = eval true false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
+  in () end;
+
+
+local structure P = OuterParse and K = OuterKeyword in
+
+fun inherit_env (context as Context.Proof lthy) =
+      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+  | inherit_env context = context;
+
+val _ =
+  OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
+    (P.ML_source >> (fn src =>
+      Toplevel.generic_theory (ML_Context.exec (fn () => ML_test true src) #> inherit_env)));
+
+val _ =
+  OuterSyntax.command "ML_parse" "advanced ML compiler test (parse only)" (K.tag_ml K.thy_decl)
+    (P.ML_source >> (fn src =>
+      Toplevel.generic_theory (ML_Context.exec (fn () => ML_test false src) #> inherit_env)));
+
+end;
+
+end;
+
--- a/src/Pure/ROOT.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -101,4 +101,6 @@
 (*configuration for Proof General*)
 cd "ProofGeneral"; use "ROOT.ML"; cd "..";
 
+if ml_system = "polyml-experimental" then use "ML/ml_test.ML" else ();
 use "pure_setup.ML";
+
--- a/src/Pure/Thy/latex.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -117,7 +117,7 @@
     else if T.is_kind T.Verbatim tok then
       let
         val (txt, pos) = T.source_position_of tok;
-        val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+        val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
         val out = implode (map output_syms_antiq ants);
       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
     else output_syms s
--- a/src/Pure/Thy/thy_output.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -156,9 +156,9 @@
           end
       | expand (Antiquote.Open _) = ""
       | expand (Antiquote.Close _) = "";
-    val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
   in
-    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
+    if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
       error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
     else implode (map expand ants)
   end;
--- a/src/Pure/Tools/find_theorems.ML	Tue Mar 24 12:45:01 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Tue Mar 24 12:45:23 2009 +0100
@@ -336,7 +336,9 @@
 
 fun find_theorems ctxt opt_goal rem_dups raw_criteria =
   let
-    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.all_prems_of ctxt) 1));
+    val assms = ProofContext.get_fact ctxt (Facts.named "local.assms")
+                handle ERROR _ => [];
+    val add_prems = Seq.hd o (TRY (Method.insert_tac assms 1));
     val opt_goal' = Option.map add_prems opt_goal;
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;