# HG changeset patch # User webertj # Date 1154171712 -7200 # Node ID 58b71535ed0089c928739c10ec457ed353961f08 # Parent 636ac45d100fae4e8400558dc34184639e8c402c lin_arith_prover splits certain operators (e.g. min, max, abs) diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Divides.thy Sat Jul 29 13:15:12 2006 +0200 @@ -710,7 +710,7 @@ apply (rule iffI) apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient) prefer 3; apply assumption - apply (simp_all add: quorem_def) apply arith + apply (simp_all add: quorem_def) apply (rule conjI) apply (rule_tac P="%x. n * (m div n) \ x" in subst [OF mod_div_equality [of _ n]]) diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Hyperreal/HyperArith.thy --- a/src/HOL/Hyperreal/HyperArith.thy Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Hyperreal/HyperArith.thy Sat Jul 29 13:15:12 2006 +0200 @@ -11,12 +11,6 @@ uses ("hypreal_arith.ML") begin -subsection{*Numerals and Arithmetic*} - -use "hypreal_arith.ML" - -setup hypreal_arith_setup - subsection{*Absolute Value Function for the Hyperreals*} lemma hrabs_add_less: @@ -109,4 +103,32 @@ Addsimps [symmetric hypreal_diff_def] *) + +subsection{*Numerals and Arithmetic*} + +lemma star_of_zero: "star_of 0 = 0" + by simp + +lemma star_of_one: "star_of 1 = 1" + by simp + +lemma star_of_add: "star_of (x + y) = star_of x + star_of y" + by simp + +lemma star_of_minus: "star_of (- x) = - star_of x" + by simp + +lemma star_of_diff: "star_of (x - y) = star_of x - star_of y" + by simp + +lemma star_of_mult: "star_of (x * y) = star_of x * star_of y" + by simp + +lemma star_of_number_of: "star_of (number_of v) = number_of v" + by simp + +use "hypreal_arith.ML" + +setup hypreal_arith_setup + end diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Hyperreal/Lim.thy Sat Jul 29 13:15:12 2006 +0200 @@ -1259,10 +1259,11 @@ apply (drule_tac x = "f n + - lim f" in spec, safe) apply (drule_tac P = "%na. no\na --> ?Q na" and x = "no + n" in spec, auto) apply (subgoal_tac "lim f \ f (no + n) ") -apply (induct_tac [2] "no") -apply (auto intro: order_trans simp add: diff_minus abs_if) apply (drule_tac no=no and m=n in lemma_f_mono_add) apply (auto simp add: add_commute) +apply (induct_tac "no") +apply simp +apply (auto intro: order_trans simp add: diff_minus abs_if) done lemma lim_uminus: "convergent g ==> lim (%x. - g x) = - (lim g)" diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Hyperreal/NSA.thy --- a/src/HOL/Hyperreal/NSA.thy Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Hyperreal/NSA.thy Sat Jul 29 13:15:12 2006 +0200 @@ -1349,8 +1349,7 @@ ==> hypreal_of_real x + u < hypreal_of_real y" apply (simp add: Infinitesimal_def) apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp) -(* FIXME: arith simproc bug with apply (simp add: abs_less_iff) *) -apply simp +apply (simp add: abs_less_iff) done lemma Infinitesimal_add_hrabs_hypreal_of_real_less: diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Hyperreal/Series.thy --- a/src/HOL/Hyperreal/Series.thy Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Hyperreal/Series.thy Sat Jul 29 13:15:12 2006 +0200 @@ -323,6 +323,8 @@ lemmas sumr_geometric = geometric_sum [where 'a = real] +ML {* fast_arith_split_limit := 0; *} (* FIXME: needed because otherwise a premise gets simplified away *) + lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))" apply (case_tac "x = 1") apply (auto dest!: LIMSEQ_rabs_realpow_zero2 @@ -333,6 +335,8 @@ apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2) done +ML {* fast_arith_split_limit := 9; *} (* FIXME *) + text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*} lemma summable_convergent_sumr_iff: diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Hyperreal/hypreal_arith.ML --- a/src/HOL/Hyperreal/hypreal_arith.ML Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Hyperreal/hypreal_arith.ML Sat Jul 29 13:15:12 2006 +0200 @@ -8,21 +8,26 @@ Instantiation of the generic linear arithmetic package for type hypreal. *) -(****Instantiation of the generic linear arithmetic package****) - - local -val real_inj_thms = [thm "star_of_le" RS iffD2, +val simps = [thm "star_of_zero", + thm "star_of_one", + thm "star_of_number_of", + thm "star_of_add", + thm "star_of_minus", + thm "star_of_diff", + thm "star_of_mult"] + +val real_inj_thms = [thm "star_of_le" RS iffD2, thm "star_of_less" RS iffD2, - thm "star_of_eq" RS iffD2]; + thm "star_of_eq" RS iffD2] in -val hyprealT = Type("StarDef.star", [HOLogic.realT]); +val hyprealT = Type ("StarDef.star", [HOLogic.realT]); val fast_hypreal_arith_simproc = - Simplifier.simproc (Theory.sign_of (the_context ())) + Simplifier.simproc (the_context ()) "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] Fast_Arith.lin_arith_prover; @@ -31,14 +36,11 @@ Fast_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 @ real_inj_thms, + inj_thms = real_inj_thms @ inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*) neqE = neqE, - simpset = simpset}) #> + simpset = simpset addsimps simps}) #> arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #> (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy)); end; - - - diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Integ/IntDef.thy Sat Jul 29 13:15:12 2006 +0200 @@ -387,7 +387,7 @@ lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" proof - have "(\(x,y). {x-y}) respects intrel" - by (simp add: congruent_def, arith) + by (simp add: congruent_def) thus ?thesis by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) qed diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Integ/int_arith1.ML Sat Jul 29 13:15:12 2006 +0200 @@ -510,10 +510,13 @@ minus_mult_left RS sym, minus_mult_right RS sym, minus_add_distrib, minus_minus, mult_assoc, of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult, - of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat]; + of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat] + +val nat_inj_thms = [zle_int RS iffD2, + int_int_eq RS iffD2] val simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@ - Int_Numeral_Simprocs.cancel_numerals; + Int_Numeral_Simprocs.cancel_numerals in @@ -521,15 +524,15 @@ Fast_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_strict_left_mono,mult_left_mono] @ mult_mono_thms, - inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms, + inj_thms = nat_inj_thms @ inj_thms, lessD = lessD @ [zless_imp_add1_zle], neqE = neqE, simpset = simpset addsimps add_rules addsimprocs simprocs addcongs [if_weak_cong]}) #> - arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT) #> + arith_inj_const ("NatArith.of_nat", HOLogic.natT --> HOLogic.intT) #> arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #> - arith_discrete "IntDef.int"; + arith_discrete "IntDef.int" end; @@ -540,7 +543,7 @@ "(m::'a::{ordered_idom,number_ring}) <= n", "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover; -Addsimprocs [fast_int_arith_simproc] +Addsimprocs [fast_int_arith_simproc]; (* Some test data diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Real/rat_arith.ML --- a/src/HOL/Real/rat_arith.ML Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Real/rat_arith.ML Sat Jul 29 13:15:12 2006 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Real/rat_arith0.ML +(* Title: HOL/Real/rat_arith.ML ID: $Id$ Author: Lawrence C Paulson Copyright 2004 University of Cambridge @@ -8,8 +8,6 @@ Instantiation of the generic linear arithmetic package for type rat. *) -(****Instantiation of the generic linear arithmetic package for fields****) - local val simprocs = field_cancel_numeral_factors @@ -19,35 +17,39 @@ divide_1, divide_zero_left, times_divide_eq_right, times_divide_eq_left, minus_divide_left RS sym, minus_divide_right RS sym, - of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff, - of_int_mult, of_int_of_nat_eq]; + of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff, + of_int_mult, of_int_of_nat_eq] + +val nat_inj_thms = [of_nat_le_iff RS iffD2, + of_nat_eq_iff RS iffD2] +(* not needed because x < (y::nat) can be rewritten as Suc x <= y: + of_nat_less_iff RS iffD2 *) + +val int_inj_thms = [of_int_le_iff RS iffD2, + of_int_eq_iff RS iffD2] +(* not needed because x < (y::int) can be rewritten as x + 1 <= y: + of_int_less_iff RS iffD2 *) in -val fast_rat_arith_simproc = - Simplifier.simproc (Theory.sign_of(the_context())) +val fast_rat_arith_simproc = + Simplifier.simproc (the_context ()) "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"] - Fast_Arith.lin_arith_prover; + Fast_Arith.lin_arith_prover -val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2, - of_nat_eq_iff RS iffD2]; - -val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2, - of_int_eq_iff RS iffD2]; - -val ratT = Type("Rational.rat", []); +val ratT = Type ("Rational.rat", []) val rat_arith_setup = Fast_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 @ inj_thms, + inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*) neqE = neqE, simpset = simpset addsimps simps addsimprocs simprocs}) #> - arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT) #> - arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT) #> - (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy)); + arith_inj_const ("NatArith.of_nat", HOLogic.natT --> ratT) #> + arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT) #> + (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy)) end; diff -r 636ac45d100f -r 58b71535ed00 src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/Real/real_arith.ML Sat Jul 29 13:15:12 2006 +0200 @@ -102,18 +102,22 @@ real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add, real_of_int_minus, real_of_int_diff, real_of_int_mult, real_of_int_of_nat_eq, - real_of_nat_number_of, real_number_of]; + real_of_nat_number_of, real_number_of] -val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2, - real_of_int_inject RS iffD2]; +val nat_inj_thms = [real_of_nat_le_iff RS iffD2, + real_of_nat_inject RS iffD2] +(* not needed because x < (y::nat) can be rewritten as Suc x <= y: + real_of_nat_less_iff RS iffD2 *) -val nat_inj_thms = [real_of_nat_le_iff RS iffD2, real_of_nat_less_iff RS iffD2, - real_of_nat_inject RS iffD2]; +val int_inj_thms = [real_of_int_le_iff RS iffD2, + real_of_int_inject RS iffD2] +(* not needed because x < (y::int) can be rewritten as x + 1 <= y: + real_of_int_less_iff RS iffD2 *) in val fast_real_arith_simproc = - Simplifier.simproc (Theory.sign_of (the_context ())) + Simplifier.simproc (the_context ()) "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] Fast_Arith.lin_arith_prover; @@ -129,11 +133,6 @@ arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT) #> (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)); -(* some thms for injection nat => real: -real_of_nat_zero -real_of_nat_add -*) - end; diff -r 636ac45d100f -r 58b71535ed00 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Sat Jul 29 00:51:36 2006 +0200 +++ b/src/HOL/arith_data.ML Sat Jul 29 13:15:12 2006 +0200 @@ -241,17 +241,24 @@ (* Decomposition of terms *) -fun nT (Type("fun",[N,_])) = N = HOLogic.natT - | nT _ = false; +(* typ -> bool *) -fun add_atom(t,m,(p,i)) = (case AList.lookup (op =) p t of NONE => ((t, m) :: p, i) - | SOME n => (AList.update (op =) (t, Rat.add (n, m)) p, i)); +fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT) + | nT _ = false; + +fun add_atom (t, m, (p, i)) = + case AList.lookup (op =) p t of NONE => ((t, m) :: p, i) + | SOME n => (AList.update (op =) (t, Rat.add (n, m)) p, i); exception Zero; -fun rat_of_term (numt,dent) = - let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent - in if den = 0 then raise Zero else Rat.rat_of_quotient (num,den) end; +fun rat_of_term (numt, dent) = +let + val num = HOLogic.dest_binum numt + val den = HOLogic.dest_binum dent +in + if den = 0 then raise Zero else Rat.rat_of_quotient (num, den) +end; (* Warning: in rare cases number_of encloses a non-numeral, in which case dest_binum raises TERM; hence all the handles below. @@ -267,91 +274,104 @@ their coefficients *) +(* (string * Term.typ) list -> ... *) + fun demult inj_consts = let -fun demult((mC as Const("HOL.times",_)) $ s $ t,m) = ((case s of - Const("Numeral.number_of",_)$n - => demult(t,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n))) - | Const("HOL.uminus",_)$(Const("Numeral.number_of",_)$n) - => demult(t,Rat.mult(m,Rat.rat_of_intinf(~(HOLogic.dest_binum n)))) - | Const("Suc",_) $ _ - => demult(t,Rat.mult(m,Rat.rat_of_int(number_of_Sucs s))) - | Const("HOL.times",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m) - | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) => - let val den = HOLogic.dest_binum dent - in if den = 0 then raise Zero - else demult(mC $ numt $ t,Rat.mult(m, Rat.inv(Rat.rat_of_intinf den))) + fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = ( + (case s of + Const ("Numeral.number_of", _) $ n => + demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n))) + | Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) => + demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_binum n)))) + | Const("Suc", _) $ _ => + demult (t, Rat.mult (m, Rat.rat_of_int (number_of_Sucs s))) + | Const ("HOL.times", _) $ s1 $ s2 => + demult (mC $ s1 $ (mC $ s2 $ t), m) + | Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) => + let + val den = HOLogic.dest_binum dent + in + if den = 0 then raise Zero else demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den))) end - | _ => atomult(mC,s,t,m) - ) handle TERM _ => atomult(mC,s,t,m)) - | demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) = - (let val den = HOLogic.dest_binum dent - in if den = 0 then raise Zero else demult(t,Rat.mult(m, Rat.inv(Rat.rat_of_intinf den))) end - handle TERM _ => (SOME atom,m)) - | demult(Const("0",_),m) = (NONE, Rat.rat_of_int 0) - | demult(Const("1",_),m) = (NONE, m) - | demult(t as Const("Numeral.number_of",_)$n,m) = - ((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n))) - handle TERM _ => (SOME t,m)) - | demult(Const("HOL.uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1))) - | demult(t as Const f $ x, m) = - (if f mem inj_consts then SOME x else SOME t,m) - | demult(atom,m) = (SOME atom,m) - -and atomult(mC,atom,t,m) = (case demult(t,m) of (NONE,m') => (SOME atom,m') - | (SOME t',m') => (SOME(mC $ atom $ t'),m')) + | _ => + atomult (mC, s, t, m) + ) handle TERM _ => atomult (mC, s, t, m) + ) + | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) = ( + let + val den = HOLogic.dest_binum dent + in + if den = 0 then raise Zero else demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den))) + end + handle TERM _ => (SOME atom, m) + ) + | demult(Const("0",_),m) = (NONE, Rat.rat_of_int 0) + | demult(Const("1",_),m) = (NONE, m) + | demult(t as Const("Numeral.number_of",_)$n,m) = + ((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n))) + handle TERM _ => (SOME t,m)) + | demult(Const("HOL.uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1))) + | demult(t as Const f $ x, m) = + (if f mem inj_consts then SOME x else SOME t,m) + | demult(atom,m) = (SOME atom,m) +and + atomult (mC, atom, t, m) = ( + case demult (t, m) of (NONE, m') => (SOME atom, m') + | (SOME t', m') => (SOME (mC $ atom $ t'), m') + ) in demult end; -fun decomp2 inj_consts (rel,lhs,rhs) = +fun decomp2 inj_consts (rel, lhs, rhs) = let -(* Turn term into list of summand * multiplicity plus a constant *) -fun poly(Const("HOL.plus",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) - | poly(all as Const("HOL.minus",T) $ s $ t, m, pi) = - if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi)) - | poly(all as Const("HOL.uminus",T) $ t, m, pi) = - if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi) - | poly(Const("0",_), _, pi) = pi - | poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m)) - | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m))) - | poly(t as Const("HOL.times",_) $ _ $ _, m, pi as (p,i)) = - (case demult inj_consts (t,m) of - (NONE,m') => (p,Rat.add(i,m)) - | (SOME u,m') => add_atom(u,m',pi)) - | poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) = - (case demult inj_consts (t,m) of - (NONE,m') => (p,Rat.add(i,m')) - | (SOME u,m') => add_atom(u,m',pi)) - | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) = - ((p,Rat.add(i,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum t)))) - handle TERM _ => add_atom all) - | poly(all as Const f $ x, m, pi) = - if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi) - | poly x = add_atom x; + (* Turn term into list of summand * multiplicity plus a constant *) + fun poly(Const("HOL.plus",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) + | poly(all as Const("HOL.minus",T) $ s $ t, m, pi) = + if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi)) + | poly(all as Const("HOL.uminus",T) $ t, m, pi) = + if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi) + | poly(Const("0",_), _, pi) = pi + | poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m)) + | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m))) + | poly(t as Const("HOL.times",_) $ _ $ _, m, pi as (p,i)) = + (case demult inj_consts (t,m) of + (NONE,m') => (p,Rat.add(i,m)) + | (SOME u,m') => add_atom(u,m',pi)) + | poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) = + (case demult inj_consts (t,m) of + (NONE,m') => (p,Rat.add(i,m')) + | (SOME u,m') => add_atom(u,m',pi)) + | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) = + ((p,Rat.add(i,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum t)))) + handle TERM _ => add_atom all) + | poly(all as Const f $ x, m, pi) = + if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi) + | poly x = add_atom x + val (p, i) = poly (lhs, Rat.rat_of_int 1, ([], Rat.rat_of_int 0)) + val (q, j) = poly (rhs, Rat.rat_of_int 1, ([], Rat.rat_of_int 0)) +in + case rel of + "Orderings.less" => SOME (p, i, "<", q, j) + | "Orderings.less_eq" => SOME (p, i, "<=", q, j) + | "op =" => SOME (p, i, "=", q, j) + | _ => NONE +end handle Zero => NONE; -val (p,i) = poly(lhs,Rat.rat_of_int 1,([],Rat.rat_of_int 0)) -and (q,j) = poly(rhs,Rat.rat_of_int 1,([],Rat.rat_of_int 0)) - - in case rel of - "Orderings.less" => SOME(p,i,"<",q,j) - | "Orderings.less_eq" => SOME(p,i,"<=",q,j) - | "op =" => SOME(p,i,"=",q,j) - | _ => NONE - end handle Zero => NONE; - -fun negate(SOME(x,i,rel,y,j,d)) = SOME(x,i,"~"^rel,y,j,d) - | negate NONE = NONE; +fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d) + | negate NONE = NONE; fun of_lin_arith_sort sg U = - Type.of_sort (Sign.tsig_of sg) (U,["Ring_and_Field.ordered_idom"]) + Type.of_sort (Sign.tsig_of sg) (U, ["Ring_and_Field.ordered_idom"]) -fun allows_lin_arith sg discrete (U as Type(D,[])) = - if of_lin_arith_sort sg U - then (true, D mem discrete) - else (* special cases *) - if D mem discrete then (true,true) else (false,false) - | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false); +fun allows_lin_arith sg discrete (U as Type (D, [])) = + if of_lin_arith_sort sg U then + (true, D mem discrete) + else (* special cases *) + if D mem discrete then (true, true) else (false, false) + | allows_lin_arith sg discrete U = + (of_lin_arith_sort sg U, false); -fun decomp1 (sg,discrete,inj_consts) (T,xxx) = +fun decomp1 (sg, discrete, inj_consts) (T, xxx) = (case T of Type("fun",[U,_]) => (case allows_lin_arith sg discrete U of @@ -366,10 +386,13 @@ | decomp2 data _ = NONE fun decomp sg = - let val {discrete, inj_consts, ...} = ArithTheoryData.get sg - in decomp2 (sg,discrete,inj_consts) end +let + val {discrete, inj_consts, ...} = ArithTheoryData.get sg +in + decomp2 (sg,discrete,inj_consts) +end; -fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n) +fun number_of (n, T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n); (*---------------------------------------------------------------------------*) (* code that performs certain goal transformations for linear arithmetic *) diff -r 636ac45d100f -r 58b71535ed00 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sat Jul 29 00:51:36 2006 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat Jul 29 13:15:12 2006 +0200 @@ -466,15 +466,15 @@ let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm) in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end - fun mk (Asm i) = trace_thm "Asm" (nth asms i) - | mk (Nat i) = trace_thm "Nat" (LA_Logic.mk_nat_thm sg (nth atoms i)) - | mk (LessD(j)) = trace_thm "L" (hd([mk j] RL lessD)) - | mk (NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) - | mk (NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD)) - | mk (NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) - | mk (Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) - | mk (Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j))) - | mk (Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j))) + fun mk (Asm i) = trace_thm "Asm" (nth asms i) + | mk (Nat i) = trace_thm "Nat" (LA_Logic.mk_nat_thm sg (nth atoms i)) + | mk (LessD j) = trace_thm "L" (hd ([mk j] RL lessD)) + | mk (NotLeD j) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) + | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) + | mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) + | mk (Added (j1, j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) + | mk (Multiplied (n, j)) = (trace_msg ("*" ^ IntInf.toString n); trace_thm "*" (multn (n, mk j))) + | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ IntInf.toString n); trace_thm "**" (multn2 (n, mk j))) in trace_msg "mkthm"; let val thm = trace_thm "Final thm:" (mk just) @@ -590,14 +590,13 @@ (* failure as soon as a case could not be refuted; i.e. delay further *) (* splitting until after a refutation for other cases has been found. *) -(* Theory.theory -> bool -> typ list * term list -> (typ list * (decompT * int) list) list *) +(* Theory.theory -> typ list * term list -> (typ list * (decompT * int) list) list *) -fun split_items sg do_pre (Ts, terms) = +fun split_items sg (Ts, terms) = let (* - val _ = trace_msg ("split_items: do_pre is " ^ Bool.toString do_pre ^ "\n" ^ - " Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^ - " terms = " ^ string_of_list (Sign.string_of_term sg) terms) + val _ = trace_msg ("split_items: Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^ + " terms = " ^ string_of_list (Sign.string_of_term sg) terms) *) (* splits inequalities '~=' into '<' and '>'; this corresponds to *) (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *) @@ -616,7 +615,7 @@ val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *) (* (typ list * term list) list *) - (if do_pre then LA_Data.pre_decomp sg else Library.single) + LA_Data.pre_decomp sg |> (* compute the internal encoding of (in-)equalities *) (* (typ list * decompT option list) list *) map (apsnd (map (LA_Data.decomp sg))) @@ -695,8 +694,38 @@ (* Theory.theory -> (string * Term.typ) list -> bool -> bool -> term list -> injust list option *) -fun refute sg params show_ex do_pre terms = - refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) []; +fun refute sg params show_ex terms = + refutes sg params show_ex (split_items sg (map snd params, terms)) []; + +(* ('a -> bool) -> 'a list -> int *) + +fun count P xs = length (List.filter P xs); + +(* The limit on the number of ~= allowed. + Because each ~= is split into two cases, this can lead to an explosion. +*) +val fast_arith_neq_limit = ref 9; + +(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> Term.term list -> Term.term -> injust list option *) + +fun prove sg params show_ex Hs concl = + let + (* append the negated conclusion to 'Hs' -- this corresponds to *) + (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *) + (* theorem/tactic level *) + val Hs' = Hs @ [LA_Logic.neg_prop concl] + (* decompT option -> bool *) + fun is_neq NONE = false + | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") + in + trace_msg "prove"; + if count is_neq (map (LA_Data.decomp sg) Hs') + > !fast_arith_neq_limit then ( + trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ string_of_int (!fast_arith_neq_limit) ^ ")"); + NONE + ) else + refute sg params show_ex Hs' + end; (* MetaSimplifier.simpset -> int * injust list -> Tactical.tactic *) @@ -714,36 +743,6 @@ EVERY (map just1 justs) (* prove every resulting subgoal, using its justification *) end state; -(* ('a -> bool) -> 'a list -> int *) - -fun count P xs = length (List.filter P xs); - -(* The limit on the number of ~= allowed. - Because each ~= is split into two cases, this can lead to an explosion. -*) -val fast_arith_neq_limit = ref 9; - -(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> Term.term list -> Term.term -> injust list option *) - -fun prove sg params show_ex do_pre Hs concl = - let - (* append the negated conclusion to 'Hs' -- this corresponds to *) - (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *) - (* theorem/tactic level *) - val Hs' = Hs @ [LA_Logic.neg_prop concl] - (* decompT option -> bool *) - fun is_neq NONE = false - | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") - in - trace_msg "prove"; - if count is_neq (map (LA_Data.decomp sg) Hs') - > !fast_arith_neq_limit then ( - trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ string_of_int (!fast_arith_neq_limit) ^ ")"); - NONE - ) else - refute sg params show_ex do_pre Hs' - end; - (* Fast but very incomplete decider. Only premises and conclusions that are already (negated) (in)equations are taken into account. @@ -753,7 +752,7 @@ val Hs = Logic.strip_assums_hyp A val concl = Logic.strip_assums_concl A in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st; - case prove (Thm.sign_of_thm st) params show_ex true Hs concl of + case prove (Thm.sign_of_thm st) params show_ex Hs concl of NONE => (trace_msg "Refutation failed."; no_tac) | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js)) end) i st; @@ -768,65 +767,13 @@ (** Forward proof from theorems **) -(* More tricky code. Needs to arrange the proofs of the multiple cases (due -to splits of ~= premises) such that it coincides with the order of the cases -generated by function split_items. *) - -datatype splittree = Tip of thm list - | Spl of thm * cterm * splittree * cterm * splittree - -(* the cterm "(ct1 ==> ?R) ==> (ct2 ==> ?R) ==> ?R" is taken to (ct1, ct2) *) - -(* Thm.cterm -> Thm.cterm * Thm.cterm *) - -fun extract imp = -let val (Il, r) = Thm.dest_comb imp - val (_, imp1) = Thm.dest_comb Il - val (Ict1, _) = Thm.dest_comb imp1 - val (_, ct1) = Thm.dest_comb Ict1 - val (Ir, _) = Thm.dest_comb r - val (_, Ict2r) = Thm.dest_comb Ir - val (Ict2, _) = Thm.dest_comb Ict2r - val (_, ct2) = Thm.dest_comb Ict2 -in (ct1, ct2) end; - -(* Theory.theory -> Thm.thm list -> splittree *) - -fun splitasms sg asms = -let val {neqE, ...} = Data.get sg - fun elim_neq (asms', []) = Tip (rev asms') - | elim_neq (asms', asm::asms) = - (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of - SOME spl => - let val (ct1, ct2) = extract (cprop_of spl) - val thm1 = assume ct1 - val thm2 = assume ct2 - in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2])) - end - | NONE => elim_neq (asm::asms', asms)) -in elim_neq ([], asms) end; - -(* Theory.theory * MetaSimplifier.simpset -> splittree -> injust list -> (Thm.thm, injust list) *) - -fun fwdproof ctxt (Tip asms) (j::js) = (mkthm ctxt asms j, js) - | fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js = - let val (thm1, js1) = fwdproof ctxt tree1 js - val (thm2, js2) = fwdproof ctxt tree2 js1 - val thm1' = implies_intr ct1 thm1 - val thm2' = implies_intr ct2 thm2 - in (thm2' COMP (thm1' COMP thm), js2) end; -(* needs handle THM _ => NONE ? *) - (* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> Term.term -> injust list -> bool -> Thm.thm option *) fun prover (ctxt as (sg, ss)) thms Tconcl js pos = -let -(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *) -(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *) +let (* There is no "forward version" of 'pre_tac'. Therefore we combine the *) (* available theorems into a single proof state and perform "backward proof" *) (* using 'refute_tac'. *) -(* val Hs = map prop_of thms val Prop = fold (curry Logic.mk_implies) (rev Hs) Tconcl val cProp = cterm_of sg Prop @@ -835,15 +782,6 @@ |> Seq.hd |> Goal.finish |> fold (fn thA => fn thAB => implies_elim thAB thA) thms -*) -(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) - val nTconcl = LA_Logic.neg_prop Tconcl - val cnTconcl = cterm_of sg nTconcl - val nTconclthm = assume cnTconcl - val tree = splitasms sg (thms @ [nTconclthm]) - val (Falsethm, _) = fwdproof ctxt tree js - val contr = if pos then LA_Logic.ccontr else LA_Logic.notI - val concl = implies_intr cnTconcl Falsethm COMP contr in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end (* in case concl contains ?-var, which makes assume fail: *) @@ -867,10 +805,10 @@ val _ = map (trace_thm "thms:") thms val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl) *) -in case prove sg [] false false Hs Tconcl of (* concl provable? *) +in case prove sg [] false Hs Tconcl of (* concl provable? *) SOME js => prover (sg, ss) thms Tconcl js true | NONE => let val nTconcl = LA_Logic.neg_prop Tconcl - in case prove sg [] false false Hs nTconcl of (* ~concl provable? *) + in case prove sg [] false Hs nTconcl of (* ~concl provable? *) SOME js => prover (sg, ss) thms nTconcl js false | NONE => NONE end