# HG changeset patch # User nipkow # Date 1237895123 -3600 # Node ID 7b09a2d9bcfcc3b62f37d1cf9480430d3577101d # Parent 182fb8d27b48656f56083e85ca27fa44d4354033# Parent 48f5a5524e1180ef65d85e684f528bcd16fc7aeb merged diff -r 48f5a5524e11 -r 7b09a2d9bcfc doc-src/HOL/HOL.tex --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Arith_Tools.thy --- 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 \ - b) = (b \ -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 \ 1) = (-1 \ 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 "\"}) *} - -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 "\"} 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 |] ==> \ n dvd (m::nat)" - by (unfold dvd_def) auto - -ML {* -val divide_minus1 = @{thm divide_minus1}; -val minus1_divide = @{thm minus1_divide}; -*} - -end diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Decision_Procs/Ferrack.thy --- 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 = {* diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Divides.thy --- 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 \ m < n \ \ n dvd m" +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) + end diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Groebner_Basis.thy --- 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" diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/HoareParallel/OG_Examples.thy --- 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) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- /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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Imperative_HOL/ROOT.ML --- 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"; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- /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 \ nat \ nat \ unit Heap" +where + "swap arr i j = ( + do + x \ nth arr i; + y \ 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 \ nat \ nat \ nat \ nat Heap" +where + "part1 a left right p = ( + if (right \ left) then return right + else (do + v \ nth a left; + (if (v \ 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 (\(_,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 \ r" + shows "l \ rs \ rs \ 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 \ l") + case True (* Terminating case *) + with cr `l \ 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 \ 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 \ r" by arith + from 1(1)[OF rec_condition True rec1 `l + 1 \ 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 \ r - 1" by arith + from 1(2) [OF rec_condition False rec2 `l \ 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 \ 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 "\i. i < l \ r < i \ 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 \ 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 \ 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 + "\i. i < l \ r < i \ 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 "(\i. l \ i \ i < rs \ get_array (a::nat array) h' ! i \ p) + \ (\i. rs < i \ i \ r \ get_array a h' ! i \ 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 \ 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 \ 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 \ p" + by fastsimp + have "\i. (l \ i = (l = i \ Suc l \ 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 \ 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 \ p" + by fastsimp + have "\i. (i \ r = (i = r \ i \ r - 1))" by arith + with 1(2)[OF lr False rec2] a_r show ?thesis + by auto + qed + qed +qed + + +fun partition :: "nat array \ nat \ nat \ nat Heap" +where + "partition a left right = (do + pivot \ nth a right; + middle \ part1 a left (right - 1) pivot; + v \ nth a middle; + m \ return (if (v \ 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 "\i. i < l \ r < i \ 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 \ rs \ rs \ 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 \ 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 \ 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 "(\i. l \ i \ i < rs \ get_array (a::nat array) h' ! i \ get_array a h' ! rs) \ + (\i. rs < i \ i \ r \ get_array a h' ! rs \ 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 \ ?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 \ 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 \ 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 \ ?pivot") + case True + with rs_equals have rs_equals: "rs = middle + 1" by simp + { + fix i + assume i_is_left: "l \ i \ i < rs" + with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r` + have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto + from i_is_left rs_equals have "l \ i \ i < middle \ i = middle" by arith + with part_partitions[OF part] right_remains True + have "get_array a h1 ! i \ get_array a h' ! rs" by fastsimp + with i_props h'_def in_bounds have "get_array a h' ! i \ get_array a h' ! rs" + unfolding Heap.upd_def Heap.length_def by simp + } + moreover + { + fix i + assume "rs < i \ i \ r" + + hence "(rs < i \ i \ r - 1) \ (rs < i \ i = r)" by arith + hence "get_array a h' ! rs \ get_array a h' ! i" + proof + assume i_is: "rs < i \ i \ r - 1" + with swap_length_remains in_bounds middle_in_bounds rs_equals + have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto + from part_partitions[OF part] rs_equals right_remains i_is + have "get_array a h' ! rs \ get_array a h1 ! i" + by fastsimp + with i_props h'_def show ?thesis by fastsimp + next + assume i_is: "rs < i \ i = r" + with rs_equals have "Suc middle \ r" by arith + with middle_in_bounds `l < r` have "Suc middle \ r - 1" by arith + with part_partitions[OF part] right_remains + have "get_array a h' ! rs \ 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 \ i \ i < rs" + with swap_length_remains in_bounds middle_in_bounds rs_equals + have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto + from part_partitions[OF part] rs_equals right_remains i_is_left + have "get_array a h1 ! i \ get_array a h' ! rs" by fastsimp + with i_props h'_def have "get_array a h' ! i \ get_array a h' ! rs" + unfolding Heap.upd_def by simp + } + moreover + { + fix i + assume "rs < i \ i \ r" + hence "(rs < i \ i \ r - 1) \ i = r" by arith + hence "get_array a h' ! rs \ get_array a h' ! i" + proof + assume i_is: "rs < i \ i \ r - 1" + with swap_length_remains in_bounds middle_in_bounds rs_equals + have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto + from part_partitions[OF part] rs_equals right_remains i_is + have "get_array a h' ! rs \ 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 \ nat \ nat \ unit Heap" +where + "quicksort arr left right = + (if (right > left) then + do + pivotNewIndex \ partition arr left right; + pivotNewIndex \ assert (\x. left \ x \ x \ 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 (\(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 "\i. i < l \ r < i \ 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 \ p \ p \ r" + assume i_outer: "i < l \ 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 \ l \ 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 \ r + 1 \ 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\ p \ p \ 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 \ r", auto simp add: subarray_Nil) + (* -- Secondly, both sublists remain partitioned. *) + from partition_partitions[OF part True] + have part_conds1: "\j. j \ set (subarray l p a h1) \ j \ get_array a h1 ! p " + and part_conds2: "\j. j \ set (subarray (p + 1) (r + 1) a h1) \ get_array a h1 ! p \ 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': "\j. j \ set (subarray l p a h') \ j \ get_array a h' ! p" + by (simp, subst set_of_multiset_of[symmetric], simp) + (* -- These steps are the analogous for the right sublist \ *) + 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': "\j. j \ set (subarray (p + 1) (r + 1) a h') \ get_array a h' ! p \ 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 \ ri \ 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 \ 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Imperative_HOL/ex/Subarray.thy --- /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 \ nat \ ('a::heap) array \ heap \ 'a list" +where + "subarray n m a h \ sublist' n m (get_array a h)" + +lemma subarray_upd: "i \ m \ 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 \ 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: "\ n \ i; i < m\ \ 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 \ m \ subarray n m a h = []" +by (simp add: subarray_def sublist'_Nil') + +lemma subarray_single: "\ n < Heap.length a h \ \ 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 \ Heap.length a h \ List.length (subarray n m a h) = m - n" +by (simp add: subarray_def Heap.length_def length_sublist') + +lemma length_subarray_0: "m \ Heap.length a h \ List.length (subarray 0 m a h) = m" +by (simp add: length_subarray) + +lemma subarray_nth_array_Cons: "\ i < Heap.length a h; i < j \ \ (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: "\ i < j; j \ Heap.length a h\ \ 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: "\ i < j; j < k \ \ 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: "\ k < j - i; j \ Heap.length a h \ \ 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' \ (subarray i j a h = subarray i j a h') = (\i'. i \ i' \ i' < j \ 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: "(\j. j \ set (subarray l r a h) \ P j) = (\k. l \ k \ k < r \ k < Heap.length a h \ 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: "(\j \ set (subarray l r a h). P j) = (\k. l \ k \ k < r \ k < Heap.length a h \ 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Imperative_HOL/ex/Sublist.thy --- /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 \ j \ j \ k \ sublist xs {i.. j - 1 \ j - 1 \ k - 1") +apply simp +apply (subgoal_tac "{ja. Suc ja < j} = {0.. Suc ja \ Suc ja < k} = {j - Suc 0.. Suc ja \ Suc ja < j} = {i - 1 .. Suc ja \ Suc ja < k} = {j - 1.. Suc j \ Suc j < k} = {i - 1.. j - 1 \ j - 1 \ k - 1") +apply simp +apply fastsimp +apply fastsimp +apply fastsimp +apply fastsimp +done + +lemma sublist_update1: "i \ inds \ 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 \ inds \ sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \ 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 \ inds then (sublist xs inds)[(card {k \ 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.. 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: "\i \ inds. i \ length xs \ sublist xs inds = []" +apply (induct xs arbitrary: inds) +apply simp +apply (simp add: sublist_Cons) +apply auto +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply auto +done + +lemma sublist_Nil': "sublist xs inds = [] \ \i \ inds. i \ 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 \ inds}" in meta_allE) +apply (case_tac x, auto) +done + +lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\i \ inds. i \ length xs)" +apply (induct xs arbitrary: inds) +apply simp +apply (simp add: sublist_Cons) +apply auto +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply (case_tac x, auto) +done + +lemma sublist_eq_subseteq: " \ inds' \ inds; sublist xs inds = sublist ys inds \ \ 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 \ inds}" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) +apply fastsimp +apply (erule_tac x="list" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) +apply fastsimp +done + +lemma sublist_eq: "\ \i \ inds. ((i < length xs) \ (i < length ys)) \ ((i \ length xs ) \ (i \ length ys)); \i \ inds. xs ! i = ys ! i \ \ 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 \ inds}" in meta_allE) +apply fastsimp +apply (erule_tac x="list" in meta_allE) +apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) +apply fastsimp +done + +lemma sublist_eq_samelength: "\ length xs = length ys; \i \ inds. xs ! i = ys ! i \ \ sublist xs inds = sublist ys inds" +by (rule sublist_eq, auto) + +lemma sublist_eq_samelength_iff: "length xs = length ys \ (sublist xs inds = sublist ys inds) = (\i \ 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 \ nat \ 'a list \ '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 \ j \ 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.. (x # sublist' 0 j xs) | Suc i' \ 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 \ m \ 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 \ length xs \ 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 \ m) \ (n \ 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: "\ n < length xs; n < m \ \ 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'_single: "n < length xs \ 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 \ m \ 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 \ 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: "\n \ i; i < m\ \ 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 "\ sublist' i j xs = sublist' i j ys; n \ i; m \ j \ \ 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 \ length xs \ length (sublist' i j xs) = j - i" +by (induct xs arbitrary: i j, auto) + +lemma sublist'_front: "\ i < j; i < length xs \ \ 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: "\ i < j; j \ length xs \ \ 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 \ length xs and length ys *) +lemma sublist'_eq_samelength_iff: "length xs = length ys \ (sublist' i j xs = sublist' i j ys) = (\i'. i \ i' \ i' < j \ 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: "\ i \ j; j \ k \ \(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs" +by (induct xs arbitrary: i j k) auto + +lemma nth_sublist': "\ k < j - i; j \ length xs \ \ (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. \k. i \ k \ k < j \ k < List.length xs \ x = xs ! k}" +apply (simp add: sublist'_sublist) +apply (simp add: set_sublist) +apply auto +done + +lemma all_in_set_sublist'_conv: "(\j. j \ set (sublist' l r xs) \ P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" +unfolding set_sublist' by blast + +lemma ball_in_set_sublist'_conv: "(\j \ set (sublist' l r xs). P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" +unfolding set_sublist' by blast + + +lemma multiset_of_sublist: +assumes l_r: "l \ r \ r \ List.length xs" +assumes left: "\ i. i < l \ (xs::'a list) ! i = ys ! i" +assumes right: "\ i. i \ r \ (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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Import/HOL4Compat.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Int.thy --- 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 \ - b) = (b \ -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 \ 1) = (-1 \ 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 "\"}) *} + +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 "\"} 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 \ int \ int" diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/IntDiv.thy --- 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 \ int \ int \ int \ bool" where @@ -920,9 +924,10 @@ next assume "a\0" and le_a: "0\a" hence a_pos: "1 \ 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) \ 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 \ b mod a" by simp hence le_addm: "0 \ 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 \ int \ int \ int" where diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/IsaMakefile --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Abstract_Rat.thy --- 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 \ int" diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/AssocList.thy --- 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 {* diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Binomial.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Boolean_Algebra.thy --- 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 = diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Char_nat.thy --- 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]. *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Char_ord.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Code_Char.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Code_Char_chr.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Code_Index.thy --- 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 {* diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Code_Integer.thy --- 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 {* diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Coinductive_List.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Commutative_Ring.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/ContNotDenum.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Continuity.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Countable.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Determinants.thy --- 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*} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Efficient_Nat.thy --- 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 {* diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Enum.thy --- 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} *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Euclidean_Space.thy --- 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.*} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Eval_Witness.thy --- 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 {* diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Executable_Set.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Finite_Cartesian_Product.thy --- 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 \ card S = n)" diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Formal_Power_Series.thy --- 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*} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/FrechetDeriv.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/FuncSet.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Glbs.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Infinite_Set.thy --- 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 {* diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Inner_Product.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/LaTeXsugar.thy --- 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 *) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/ListVector.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/List_Prefix.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/List_lexord.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Mapping.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Multiset.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Nat_Infinity.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Nat_Int_Bij.thy --- 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 "\"} and @{text "\\"} *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Nested_Environment.thy --- 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 {* diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Numeral_Type.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Option_ord.thy --- 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 \ 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 \ bool" and z :: "'a option" + assume H: "\x. (\y. y < x \ P y) \ P x" + have "P None" by (rule H) simp + then have P_Some [case_names Some]: + "\z. (\x. z = Some x \ (P o Some) x) \ P z" + proof - + fix z + assume "\x. z = Some x \ (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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/OptionalSugar.thy --- 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 *) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Order_Relation.thy --- 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 *} diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Permutations.thy --- 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! *) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Topology_Euclidean_Space.thy --- 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: "\d x y z. (d x z :: real) <= d x y + d y z \ d y z = d z y ==> ~(d x y * 2 < d x z \ 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 \ 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 "\ ball w (?k/4) \ T" using kp by (auto simp add: Arith_Tools.less_divide_eq_number_of1) + have "\ ball w (?k/4) \ T" using kp by (auto simp add: less_divide_eq_number_of1) then obtain z where z: "dist w z < ?k/4" "z \ T" by (auto simp add: subset_eq) have "z \ T \ z\ y \ dist z y < d \ 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 (\x. dist (f x) l < e/2) net" "eventually (\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 (\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 \ 0" using `l \ 0` by auto hence fxl0: "(f x) * l \ 0" using `l \ 0` by auto from * have **:"\f x - l\ < l\ * e / 2" by auto - have "\f x\ * 2 \ \l\" using * by (auto simp del: Arith_Tools.less_divide_eq_number_of1) + have "\f x\ * 2 \ \l\" using * by (auto simp del: less_divide_eq_number_of1) hence "\f x\ * 2 * \l\ \ \l\ * \l\" unfolding mult_le_cancel_right by auto hence "\f x * l\ * 2 \ \l\^2" unfolding real_mult_commute and power2_eq_square by auto hence ***:"inverse \f x * l\ \ inverse (l\ / 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} \ {}" using mem_interval(1)[of "?x" a b] by auto } ultimately show ?th1 by blast @@ -4333,7 +4332,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} \ {}" 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 \ ?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\{c<..{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 \ c$i" by(rule ccontr)auto moreover @@ -4412,13 +4411,13 @@ { fix j have "d $ j > ?x $ j \ ?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\{c<..{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 \ d$i" by(rule ccontr)auto ultimately @@ -4449,7 +4448,7 @@ lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows "{a .. b} \ {c .. d} = {(\ i. max (a$i) (c$i)) .. (\ 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 \ ((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 "\m\Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2" and "\m\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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Library/Zorn.thy --- 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? *) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/NSA/hypreal_arith.ML --- 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, diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Nat.thy --- 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 \ 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 \ 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 "\n. P n \ 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/NatBin.thy --- 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 \ bool" -where +definition neg :: "int \ bool" where "neg Z \ 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/OrderedGroup.thy --- 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 \ 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 \ x" and y: "0 \ y" shows "x + y = 0 \ x = 0 \ y = 0" diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Presburger.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Ring_and_Field.thy --- 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 \ a \ 0 \ b \ 0 \ 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 \ a \ b \ 0 \ a * b \ 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 \ 0 \ 0 \ b \ a * b \ 0" +using mult_right_mono [of a zero b] by simp + +text {* Legacy - use @{text mult_nonpos_nonneg} *} lemma mult_nonneg_nonpos2: "0 \ a \ b \ 0 \ b * a \ 0" by (drule mult_right_mono [of b zero], auto) @@ -786,31 +790,32 @@ "a * c \ b * c \ 0 < c \ a \ b" by (force simp add: mult_strict_right_mono not_less [symmetric]) -lemma mult_pos_pos: - "0 < a \ 0 < b \ 0 < a * b" -by (drule mult_strict_left_mono [of zero b], auto) - -lemma mult_pos_neg: - "0 < a \ b < 0 \ a * b < 0" -by (drule mult_strict_left_mono [of b zero], auto) - -lemma mult_pos_neg2: - "0 < a \ b < 0 \ b * a < 0" +lemma mult_pos_pos: "0 < a \ 0 < b \ 0 < a * b" +using mult_strict_left_mono [of zero b a] by simp + +lemma mult_pos_neg: "0 < a \ b < 0 \ a * b < 0" +using mult_strict_left_mono [of b zero a] by simp + +lemma mult_neg_pos: "a < 0 \ 0 < b \ 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 \ b < 0 \ b * a < 0" by (drule mult_strict_right_mono [of b zero], auto) lemma zero_less_mult_pos: "0 < a * b \ 0 < a \ 0 < b" -apply (cases "b\0") +apply (cases "b\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 \ 0 < a \ 0 < b" -apply (cases "b\0") +apply (cases "b\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 \ 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 \ 0 \ b \ 0 \ 0 \ a * b" -by (drule mult_right_mono_neg [of a zero b]) auto +lemma mult_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a * b" +using mult_right_mono_neg [of a zero b] by simp lemma split_mult_pos_le: "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a * b" @@ -1006,21 +1010,14 @@ subclass ordered_ring .. -lemma mult_strict_left_mono_neg: - "b < a \ c < 0 \ 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 \ c < 0 \ 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 \ b < 0 \ 0 < a * b" -by (drule mult_strict_right_mono_neg, auto) +lemma mult_strict_left_mono_neg: "b < a \ c < 0 \ c * a < c * b" +using mult_strict_left_mono [of b a "- c"] by simp + +lemma mult_strict_right_mono_neg: "b < a \ c < 0 \ a * c < b * c" +using mult_strict_right_mono [of b a "- c"] by simp + +lemma mult_neg_neg: "a < 0 \ b < 0 \ 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 \ c * a \ c * b \ b \ a" by (auto simp: mult_le_cancel_left) -end - -context ordered_ring_strict -begin - lemma mult_less_cancel_left_pos: "0 < c \ c * a < c * b \ 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/Qelim/qelim.ML --- 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) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/TFL/post.ML --- 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 []}; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/arith_data.ML --- 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)) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/function_package/scnp_reconstruct.ML --- 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 = diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/int_arith.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/int_factor_simprocs.ML --- 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) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/lin_arith.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/nat_simprocs.ML --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/rat_arith.ML --- 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, diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Tools/real_arith.ML --- 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, diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/Word/WordArith.thy --- 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/ex/Arith_Examples.thy --- 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" diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/ex/ImperativeQuicksort.thy --- 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 \ nat \ nat \ unit Heap" -where - "swap arr i j = ( - do - x \ nth arr i; - y \ 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 \ nat \ nat \ nat \ nat Heap" -where - "part1 a left right p = ( - if (right \ left) then return right - else (do - v \ nth a left; - (if (v \ 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 (\(_,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 \ r" - shows "l \ rs \ rs \ 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 \ l") - case True (* Terminating case *) - with cr `l \ 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 \ 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 \ r" by arith - from 1(1)[OF rec_condition True rec1 `l + 1 \ 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 \ r - 1" by arith - from 1(2) [OF rec_condition False rec2 `l \ 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 \ 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 "\i. i < l \ r < i \ 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 \ 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 \ 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 - "\i. i < l \ r < i \ 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 "(\i. l \ i \ i < rs \ get_array (a::nat array) h' ! i \ p) - \ (\i. rs < i \ i \ r \ get_array a h' ! i \ 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 \ 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 \ 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 \ p" - by fastsimp - have "\i. (l \ i = (l = i \ Suc l \ 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 \ 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 \ p" - by fastsimp - have "\i. (i \ r = (i = r \ i \ r - 1))" by arith - with 1(2)[OF lr False rec2] a_r show ?thesis - by auto - qed - qed -qed - - -fun partition :: "nat array \ nat \ nat \ nat Heap" -where - "partition a left right = (do - pivot \ nth a right; - middle \ part1 a left (right - 1) pivot; - v \ nth a middle; - m \ return (if (v \ 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 "\i. i < l \ r < i \ 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 \ rs \ rs \ 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 \ 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 \ 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 "(\i. l \ i \ i < rs \ get_array (a::nat array) h' ! i \ get_array a h' ! rs) \ - (\i. rs < i \ i \ r \ get_array a h' ! rs \ 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 \ ?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 \ 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 \ 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 \ ?pivot") - case True - with rs_equals have rs_equals: "rs = middle + 1" by simp - { - fix i - assume i_is_left: "l \ i \ i < rs" - with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r` - have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto - from i_is_left rs_equals have "l \ i \ i < middle \ i = middle" by arith - with part_partitions[OF part] right_remains True - have "get_array a h1 ! i \ get_array a h' ! rs" by fastsimp - with i_props h'_def in_bounds have "get_array a h' ! i \ get_array a h' ! rs" - unfolding Heap.upd_def Heap.length_def by simp - } - moreover - { - fix i - assume "rs < i \ i \ r" - - hence "(rs < i \ i \ r - 1) \ (rs < i \ i = r)" by arith - hence "get_array a h' ! rs \ get_array a h' ! i" - proof - assume i_is: "rs < i \ i \ r - 1" - with swap_length_remains in_bounds middle_in_bounds rs_equals - have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto - from part_partitions[OF part] rs_equals right_remains i_is - have "get_array a h' ! rs \ get_array a h1 ! i" - by fastsimp - with i_props h'_def show ?thesis by fastsimp - next - assume i_is: "rs < i \ i = r" - with rs_equals have "Suc middle \ r" by arith - with middle_in_bounds `l < r` have "Suc middle \ r - 1" by arith - with part_partitions[OF part] right_remains - have "get_array a h' ! rs \ 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 \ i \ i < rs" - with swap_length_remains in_bounds middle_in_bounds rs_equals - have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto - from part_partitions[OF part] rs_equals right_remains i_is_left - have "get_array a h1 ! i \ get_array a h' ! rs" by fastsimp - with i_props h'_def have "get_array a h' ! i \ get_array a h' ! rs" - unfolding Heap.upd_def by simp - } - moreover - { - fix i - assume "rs < i \ i \ r" - hence "(rs < i \ i \ r - 1) \ i = r" by arith - hence "get_array a h' ! rs \ get_array a h' ! i" - proof - assume i_is: "rs < i \ i \ r - 1" - with swap_length_remains in_bounds middle_in_bounds rs_equals - have i_props: "i < Heap.length a h'" "i \ r" "i \ rs" by auto - from part_partitions[OF part] rs_equals right_remains i_is - have "get_array a h' ! rs \ 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 \ nat \ nat \ unit Heap" -where - "quicksort arr left right = - (if (right > left) then - do - pivotNewIndex \ partition arr left right; - pivotNewIndex \ assert (\x. left \ x \ x \ 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 (\(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 "\i. i < l \ r < i \ 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 \ p \ p \ r" - assume i_outer: "i < l \ 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 \ l \ 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 \ r + 1 \ 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\ p \ p \ 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 \ r", auto simp add: subarray_Nil) - (* -- Secondly, both sublists remain partitioned. *) - from partition_partitions[OF part True] - have part_conds1: "\j. j \ set (subarray l p a h1) \ j \ get_array a h1 ! p " - and part_conds2: "\j. j \ set (subarray (p + 1) (r + 1) a h1) \ get_array a h1 ! p \ 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': "\j. j \ set (subarray l p a h') \ j \ get_array a h' ! p" - by (simp, subst set_of_multiset_of[symmetric], simp) - (* -- These steps are the analogous for the right sublist \ *) - 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': "\j. j \ set (subarray (p + 1) (r + 1) a h') \ get_array a h' ! p \ 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 \ ri \ 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 \ 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/ex/MergeSort.thy --- 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 *) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/ex/ROOT.ML --- 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", diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/ex/Subarray.thy --- 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 \ nat \ ('a::heap) array \ heap \ 'a list" -where - "subarray n m a h \ sublist' n m (get_array a h)" - -lemma subarray_upd: "i \ m \ 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 \ 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: "\ n \ i; i < m\ \ 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 \ m \ subarray n m a h = []" -by (simp add: subarray_def sublist'_Nil') - -lemma subarray_single: "\ n < Heap.length a h \ \ 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 \ Heap.length a h \ List.length (subarray n m a h) = m - n" -by (simp add: subarray_def Heap.length_def length_sublist') - -lemma length_subarray_0: "m \ Heap.length a h \ List.length (subarray 0 m a h) = m" -by (simp add: length_subarray) - -lemma subarray_nth_array_Cons: "\ i < Heap.length a h; i < j \ \ (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: "\ i < j; j \ Heap.length a h\ \ 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: "\ i < j; j < k \ \ 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: "\ k < j - i; j \ Heap.length a h \ \ 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' \ (subarray i j a h = subarray i j a h') = (\i'. i \ i' \ i' < j \ 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: "(\j. j \ set (subarray l r a h) \ P j) = (\k. l \ k \ k < r \ k < Heap.length a h \ 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: "(\j \ set (subarray l r a h). P j) = (\k. l \ k \ k < r \ k < Heap.length a h \ 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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/HOL/ex/Sublist.thy --- 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 \ j \ j \ k \ sublist xs {i.. j - 1 \ j - 1 \ k - 1") -apply simp -apply (subgoal_tac "{ja. Suc ja < j} = {0.. Suc ja \ Suc ja < k} = {j - Suc 0.. Suc ja \ Suc ja < j} = {i - 1 .. Suc ja \ Suc ja < k} = {j - 1.. Suc j \ Suc j < k} = {i - 1.. j - 1 \ j - 1 \ k - 1") -apply simp -apply fastsimp -apply fastsimp -apply fastsimp -apply fastsimp -done - -lemma sublist_update1: "i \ inds \ 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 \ inds \ sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \ 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 \ inds then (sublist xs inds)[(card {k \ 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.. 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: "\i \ inds. i \ length xs \ sublist xs inds = []" -apply (induct xs arbitrary: inds) -apply simp -apply (simp add: sublist_Cons) -apply auto -apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) -apply auto -done - -lemma sublist_Nil': "sublist xs inds = [] \ \i \ inds. i \ 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 \ inds}" in meta_allE) -apply (case_tac x, auto) -done - -lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\i \ inds. i \ length xs)" -apply (induct xs arbitrary: inds) -apply simp -apply (simp add: sublist_Cons) -apply auto -apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) -apply (case_tac x, auto) -done - -lemma sublist_eq_subseteq: " \ inds' \ inds; sublist xs inds = sublist ys inds \ \ 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 \ inds}" in meta_allE) -apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) -apply fastsimp -apply (erule_tac x="list" in meta_allE) -apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) -apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) -apply fastsimp -done - -lemma sublist_eq: "\ \i \ inds. ((i < length xs) \ (i < length ys)) \ ((i \ length xs ) \ (i \ length ys)); \i \ inds. xs ! i = ys ! i \ \ 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 \ inds}" in meta_allE) -apply fastsimp -apply (erule_tac x="list" in meta_allE) -apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) -apply fastsimp -done - -lemma sublist_eq_samelength: "\ length xs = length ys; \i \ inds. xs ! i = ys ! i \ \ sublist xs inds = sublist ys inds" -by (rule sublist_eq, auto) - -lemma sublist_eq_samelength_iff: "length xs = length ys \ (sublist xs inds = sublist ys inds) = (\i \ 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 \ nat \ 'a list \ '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 \ j \ 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.. (x # sublist' 0 j xs) | Suc i' \ 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 \ m \ 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 \ length xs \ 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 \ m) \ (n \ 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: "\ n < length xs; n < m \ \ 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'_single: "n < length xs \ 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 \ m \ 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 \ 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: "\n \ i; i < m\ \ 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 "\ sublist' i j xs = sublist' i j ys; n \ i; m \ j \ \ 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 \ length xs \ length (sublist' i j xs) = j - i" -by (induct xs arbitrary: i j, auto) - -lemma sublist'_front: "\ i < j; i < length xs \ \ 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: "\ i < j; j \ length xs \ \ 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 \ length xs and length ys *) -lemma sublist'_eq_samelength_iff: "length xs = length ys \ (sublist' i j xs = sublist' i j ys) = (\i'. i \ i' \ i' < j \ 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: "\ i \ j; j \ k \ \(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs" -by (induct xs arbitrary: i j k) auto - -lemma nth_sublist': "\ k < j - i; j \ length xs \ \ (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. \k. i \ k \ k < j \ k < List.length xs \ x = xs ! k}" -apply (simp add: sublist'_sublist) -apply (simp add: set_sublist) -apply auto -done - -lemma all_in_set_sublist'_conv: "(\j. j \ set (sublist' l r xs) \ P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" -unfolding set_sublist' by blast - -lemma ball_in_set_sublist'_conv: "(\j \ set (sublist' l r xs). P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" -unfolding set_sublist' by blast - - -lemma multiset_of_sublist: -assumes l_r: "l \ r \ r \ List.length xs" -assumes left: "\ i. i < l \ (xs::'a list) ! i = ys ! i" -assumes right: "\ i. i \ r \ (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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Provers/Arith/fast_lin_arith.ML --- 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; (* ------------------------------------------------------------------------- *) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/Concurrent/future.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/General/antiquote.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/General/pretty.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/IsaMakefile --- 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 \ diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/Isar/code_unit.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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/ML-Systems/polyml-experimental.ML --- 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) diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/ML/ml_context.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/ML/ml_lex.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/ML/ml_parse.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/ML/ml_test.ML --- /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; + diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/ROOT.ML --- 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"; + diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/Thy/latex.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 diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/Thy/thy_output.ML --- 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; diff -r 48f5a5524e11 -r 7b09a2d9bcfc src/Pure/Tools/find_theorems.ML --- 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;