# HG changeset patch # User nipkow # Date 915891944 -3600 # Node ID 34242451bc9104d47a152584ecc1d1d76fcd8beb # Parent fba734ba6894ef46eaa7ff6cc636a2570c87eb2a Added simproc. diff -r fba734ba6894 -r 34242451bc91 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sat Jan 09 15:24:11 1999 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat Jan 09 15:25:44 1999 +0100 @@ -27,6 +27,9 @@ val sym: thm (* x = y ==> y = x *) val decomp: term -> ((term * int)list * int * string * (term * int)list * int)option + val mkEqTrue: thm -> thm + val mk_Trueprop: term -> term + val neg_prop: term -> term * bool val simp: thm -> thm val is_False: thm -> bool val is_nat: typ list * term -> bool @@ -38,6 +41,13 @@ p/q is the decomposition of the sum terms x/y into a list of summand * multiplicity pairs and a constant summand. +mkEqTrue(P) = `P == True' + +neg_prop(t) = (nt,neg) if t is wrapped up in Trueprop and + nt is the (logically) negated version of t, where the negation + of a negative term is the term itself (no double negation!); + neg = `t is already negated'. + simp must reduce contradictory <= to False. It should also cancel common summands to keep <= reduced; otherwise <= can grow to massive proportions. @@ -48,6 +58,7 @@ signature FAST_LIN_ARITH = sig + val lin_arith_prover: Sign.sg -> thm list -> term -> thm option val lin_arith_tac: int -> tactic val cut_lin_arith_tac: thm list -> int -> tactic end; @@ -223,7 +234,7 @@ local exception FalseE of thm in -fun mkproof sg asms just = +fun mkthm sg asms just = let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_)) => map fst lhs union (map fst rhs union ats)) ([], mapfilter (LA_Data.decomp o concl_of) asms) @@ -287,32 +298,51 @@ in mapfilter (mklineq atoms) items @ mapfilter (mknat pTs ixs) iatoms end; (* Ordinary refutation *) -fun refute1_tac pTs items = - let val lineqs = abstract pTs items - in case elim lineqs of - None => K no_tac - | Some(Lineq(_,_,_,j)) => - fn i => fn state => - let val sg = #sign(rep_thm state) - in resolve_tac [LA_Data.notI,LA_Data.ccontr] i THEN - METAHYPS (fn asms => rtac (mkproof sg asms j) 1) i - end state - end; +fun refute1(pTs,items) = + (case elim (abstract pTs items) of + None => [] + | Some(Lineq(_,_,_,j)) => [j]); + +fun refute1_tac(i,just) = + fn state => + let val sg = #sign(rep_thm state) + in resolve_tac [LA_Data.notI,LA_Data.ccontr] i THEN + METAHYPS (fn asms => rtac (mkthm sg asms just) 1) i + end + state; (* Double refutation caused by equality in conclusion *) -fun refute2_tac pTs items (rhs,i,_,lhs,j) nHs = +fun refute2(pTs,items, (rhs,i,_,lhs,j), nHs) = (case elim (abstract pTs (items@[((rhs,i,"<",lhs,j),nHs)])) of - None => K no_tac + None => [] | Some(Lineq(_,_,_,j1)) => (case elim (abstract pTs (items@[((lhs,j,"<",rhs,i),nHs)])) of - None => K no_tac - | Some(Lineq(_,_,_,j2)) => - fn i => fn state => - let val sg = #sign(rep_thm state) - in rtac LA_Data.ccontr i THEN etac LA_Data.neqE i THEN - METAHYPS (fn asms => rtac (mkproof sg asms j1) 1) i THEN - METAHYPS (fn asms => rtac (mkproof sg asms j2) 1) i - end state)); + None => [] + | Some(Lineq(_,_,_,j2)) => [j1,j2])); + +fun refute2_tac(i,just1,just2) = + fn state => + let val sg = #sign(rep_thm state) + in rtac LA_Data.ccontr i THEN rotate_tac ~1 i THEN etac LA_Data.neqE i THEN + METAHYPS (fn asms => rtac (mkthm sg asms just1) 1) i THEN + METAHYPS (fn asms => rtac (mkthm sg asms just2) 1) i + end + state; + +fun prove(pTs,Hs,concl) = +let val nHs = length Hs + val ixHs = Hs ~~ (0 upto (nHs-1)) + val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of + None => None | Some(it) => Some(it,i)) ixHs +in case LA_Data.decomp concl of + None => if null Hitems then [] else refute1(pTs,Hitems) + | Some(citem as (r,i,rel,l,j)) => + if rel = "=" + then refute2(pTs,Hitems,citem,nHs) + else let val neg::rel0 = explode rel + val nrel = if neg = "~" then implode rel0 else "~"^rel + in refute1(pTs, Hitems@[((r,i,nrel,l,j),nHs)]) end +end; (* Fast but very incomplete decider. Only premises and conclusions @@ -321,20 +351,48 @@ val lin_arith_tac = SUBGOAL (fn (A,n) => let val pTs = rev(map snd (Logic.strip_params A)) val Hs = Logic.strip_assums_hyp A - val nHs = length Hs - val His = Hs ~~ (0 upto (nHs-1)) - val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of - None => None | Some(it) => Some(it,i)) His - in case LA_Data.decomp(Logic.strip_assums_concl A) of - None => if null Hitems then no_tac else refute1_tac pTs Hitems n - | Some(citem as (r,i,rel,l,j)) => - if rel = "=" - then refute2_tac pTs Hitems citem nHs n - else let val neg::rel0 = explode rel - val nrel = if neg = "~" then implode rel0 else "~"^rel - in refute1_tac pTs (Hitems@[((r,i,nrel,l,j),nHs)]) n end + val concl = Logic.strip_assums_concl A + in case prove(pTs,Hs,concl) of + [j] => refute1_tac(n,j) + | [j1,j2] => refute2_tac(n,j1,j2) + | _ => no_tac end); fun cut_lin_arith_tac thms i = cut_facts_tac thms i THEN lin_arith_tac i; +fun prover1(just,sg,thms,concl) = +let val (nconcl,neg) = LA_Data.neg_prop concl + val cnconcl = cterm_of sg nconcl + val Fthm = mkthm sg (thms @ [assume cnconcl]) just + val contr = if neg then LA_Data.notI else LA_Data.ccontr +in Some(LA_Data.mkEqTrue ((implies_intr cnconcl Fthm) COMP contr)) end +handle _ => None; + +(* handle thm with equality conclusion *) +fun prover2(just1,just2,sg,thms,concl) = +let val (nconcl,_) = LA_Data.neg_prop concl (* m ~= n *) + val cnconcl = cterm_of sg nconcl + val neqthm = assume cnconcl + val casethm = neqthm COMP LA_Data.neqE (* [|m R; n R|] ==> R *) + val [lessimp1,lessimp2] = prems_of casethm + val less1 = fst(Logic.dest_implies lessimp1) (* m None; + +(* FIXME: forward proof of equalities missing! *) +fun lin_arith_prover sg thms concl = +let val Hs = map (#prop o rep_thm) thms + val Tconcl = LA_Data.mk_Trueprop concl +in case prove([],Hs,Tconcl) of + [j] => prover1(j,sg,thms,Tconcl) + | [j1,j2] => prover2(j1,j2,sg,thms,Tconcl) + | _ => None end; + +end;