--- 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;