# HG changeset patch # User nipkow # Date 1022746331 -7200 # Node ID ef8ed6adcb383626eb6114a01a3cc939147d6397 # Parent da61bfa0a391bbc0f58411967cef91c95b6f92b7 Big update. Allows case splitting on ~= now (trying both < and >). diff -r da61bfa0a391 -r ef8ed6adcb38 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue May 28 11:07:36 2002 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Thu May 30 10:12:11 2002 +0200 @@ -242,7 +242,7 @@ let val dummy = print_ineqs ineqs; val (triv,nontriv) = partition is_trivial ineqs in if not(null triv) - then case find_first is_answer triv of + then case Library.find_first is_answer triv of None => elim nontriv | some => some else if null nontriv then None else @@ -347,7 +347,14 @@ in trace_msg "mkthm"; let val thm = trace_thm "Final thm:" (mk just) in let val fls = simplify simpset thm - in trace_thm "After simplification:" fls; fls + in trace_thm "After simplification:" fls; + if LA_Logic.is_False fls then fls + else + (tracing "Assumptions:"; seq print_thm asms; + tracing "Proved:"; print_thm fls; + warning "Linear arithmetic should have refuted the assumptions.\n\ + \Please inform Tobias Nipkow (nipkow@in.tum.de)."; + fls) end end handle FalseE thm => (trace_thm "False reached early:" thm; thm) end @@ -372,7 +379,7 @@ val diff = map2 (op -) (rhsa,lhsa) val c = i-j val just = Asm k - fun lineq(c,le,cs,j) = Some(Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j))) + fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j)) in case rel of "<=" => lineq(c,Le,diff,just) | "~<=" => if discrete @@ -383,7 +390,6 @@ else lineq(c,Lt,diff,just) | "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just)) | "=" => lineq(c,Eq,diff,just) - | "~=" => None | _ => sys_error("mklineq" ^ rel) end end; @@ -394,115 +400,145 @@ in Some(Lineq(0,Le,l,Nat(i))) end else None -fun abstract pTs items = - let val atoms = foldl (fn (ats,((lhs,_,_,rhs,_,_),_)) => - (map fst lhs) union ((map fst rhs) union ats)) - ([],items) +(* This code is tricky. It takes a list of premises in the order they occur +in the subgoal. Numerical premises are coded as Some(tuple), non-numerical +ones as None. Going through the premises, each numeric one is converted into +a Lineq. The tricky bit is to convert ~= which is split into two cases < and +>. Thus mklineqss returns a list of equation systems. This may blow up if +there are many ~=, but in practice it does not seem to happen. The really +tricky bit is to arrange the order of the cases such that they coincide with +the order in which the cases are in the end generated by the tactic that +applies the generated refutation thms (see function 'refute_tac'). + +For variables n of type nat, a constraint 0 <= n is added. +*) +fun mklineqss(pTs,items) = + let fun add(ats,None) = ats + | add(ats,Some(lhs,_,_,rhs,_,_)) = + (map fst lhs) union ((map fst rhs) union ats) + val atoms = foldl add ([],items) + val mkleq = mklineq atoms val ixs = 0 upto (length(atoms)-1) val iatoms = atoms ~~ ixs - in mapfilter (mklineq atoms) items @ mapfilter (mknat pTs ixs) iatoms end; + val natlineqs = mapfilter (mknat pTs ixs) iatoms + + fun elim_neq front _ [] = [front] + | elim_neq front n (None::ineqs) = elim_neq front (n+1) ineqs + | elim_neq front n (Some(ineq as (l,i,rel,r,j,d))::ineqs) = + if rel = "~=" then elim_neq front n (ineqs @ [Some(l,i,"<",r,j,d)]) @ + elim_neq front n (ineqs @ [Some(r,j,"<",l,i,d)]) + else elim_neq (mkleq(ineq,n) :: front) (n+1) ineqs -(* Ordinary refutation *) -fun refute1(pTs,items) = - (case elim (abstract pTs items) of - None => [] - | Some(Lineq(_,_,_,j)) => [j]); + in elim_neq natlineqs 0 items end; -fun refute1_tac(i,just) = +fun elim_all (ineqs::ineqss) js = + (case elim ineqs of None => None + | Some(Lineq(_,_,_,j)) => elim_all ineqss (js@[j])) + | elim_all [] js = Some js + +fun refute(pTsitems) = elim_all (mklineqss pTsitems) []; + +fun refute_tac(i,justs) = fn state => let val sg = #sign(rep_thm state) - in resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i THEN - METAHYPS (fn asms => rtac (mkthm sg asms just) 1) i - end - state; - -(* Double refutation caused by equality in conclusion *) -fun refute2(pTs,items, (rhs,i,_,lhs,j,d), nHs) = - (case elim (abstract pTs (items@[((rhs,i,"<",lhs,j,d),nHs)])) of - None => [] - | Some(Lineq(_,_,_,j1)) => - (case elim (abstract pTs (items@[((lhs,j,"<",rhs,i,d),nHs)])) of - None => [] - | Some(Lineq(_,_,_,j2)) => [j1,j2])); - -fun refute2_tac(i,just1,just2) = - fn state => - let val sg = #sign(rep_thm state) - in rtac LA_Logic.ccontr i THEN rotate_tac ~1 i THEN etac LA_Logic.neqE i THEN - METAHYPS (fn asms => rtac (mkthm sg asms just1) 1) i THEN - METAHYPS (fn asms => rtac (mkthm sg asms just2) 1) i + fun just1 j = REPEAT_DETERM(etac LA_Logic.neqE i) THEN + METAHYPS (fn asms => rtac (mkthm sg asms j) 1) i + in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN + EVERY(map just1 justs) end state; fun prove sg (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 sg h of - None => None | Some(it) => Some(it,i)) ixHs +let val Hitems = map (LA_Data.decomp sg) Hs in case LA_Data.decomp sg concl of - None => if null Hitems then [] else refute1(pTs,Hitems) + None => refute(pTs,Hitems@[None]) | Some(citem as (r,i,rel,l,j,d)) => - 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,d),nHs)]) end + let val neg::rel0 = explode rel + val nrel = if neg = "~" then implode rel0 else "~"^rel + in refute(pTs, Hitems @ [Some(r,i,nrel,l,j,d)]) end end; (* Fast but very incomplete decider. Only premises and conclusions that are already (negated) (in)equations are taken into account. *) -fun lin_arith_tac i st = SUBGOAL (fn (A,n) => +fun lin_arith_tac i st = SUBGOAL (fn (A,_) => let val pTs = rev(map snd (Logic.strip_params A)) 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) (pTs,Hs,concl) of - [j] => refute1_tac(n,j) - | [j1,j2] => refute2_tac(n,j1,j2) - | _ => no_tac + None => no_tac + | Some js => refute_tac(i,js) end) i st; fun cut_lin_arith_tac thms i = cut_facts_tac thms i THEN lin_arith_tac i; -fun prover1(just,sg,thms,concl,pos) = -let val nconcl = LA_Logic.neg_prop concl - val cnconcl = cterm_of sg nconcl - val Fthm = mkthm sg (thms @ [assume cnconcl]) just - val contr = if pos then LA_Logic.ccontr else LA_Logic.notI -in Some(LA_Logic.mk_Eq ((implies_intr cnconcl Fthm) COMP contr)) end -handle _ => None; +(** 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 mklineqss. *) + +datatype splittree = Tip of thm list + | Spl of thm * cterm * splittree * cterm * splittree + +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; -(* handle thm with equality conclusion *) -fun prover2(just1,just2,sg,thms,concl) = -let val nconcl = LA_Logic.neg_prop concl (* m ~= n *) - val cnconcl = cterm_of sg nconcl - val neqthm = assume cnconcl - val casethm = neqthm COMP LA_Logic.neqE (* [|m R; n R|] ==> R *) - val [lessimp1,lessimp2] = prems_of casethm - val less1 = fst(Logic.dest_implies lessimp1) (* m None; +fun splitasms asms = +let fun split(asms',[]) = Tip(rev asms') + | split(asms',asm::asms) = + let val spl = asm COMP LA_Logic.neqE + val (ct1,ct2) = extract(cprop_of spl) + val thm1 = assume ct1 and thm2 = assume ct2 + in Spl(spl,ct1,split(asms',asms@[thm1]),ct2,split(asms',asms@[thm2])) end + handle THM _ => split(asm::asms', asms) +in split([],asms) end; -(* PRE: concl is not negated! *) +fun fwdproof sg (Tip asms) (j::js) = (mkthm sg asms j, js) + | fwdproof sg (Spl(thm,ct1,tree1,ct2,tree2)) js = + let val (thm1,js1) = fwdproof sg tree1 js + val (thm2,js2) = fwdproof sg tree2 js1 + val thm1' = implies_intr ct1 thm1 + val thm2' = implies_intr ct2 thm2 + in (thm2' COMP (thm1' COMP thm), js2) end; +(* needs handle _ => None ? *) + +fun prover sg thms Tconcl js pos = +let val nTconcl = LA_Logic.neg_prop Tconcl + val cnTconcl = cterm_of sg nTconcl + val nTconclthm = assume cnTconcl + val tree = splitasms (thms @ [nTconclthm]) + val (thm,_) = fwdproof sg tree js + val contr = if pos then LA_Logic.ccontr else LA_Logic.notI +in Some(LA_Logic.mk_Eq((implies_intr cnTconcl thm) COMP contr)) end +(* in case concl contains ?-var, which makes assume fail: *) +handle THM _ => None; + +(* PRE: concl is not negated! + This assumption is OK because + 1. lin_arith_prover tries both to prove and disprove concl and + 2. lin_arith_prover is applied by the simplifier which + dives into terms and will thus try the non-negated concl anyway. +*) fun lin_arith_prover sg thms concl = let val Hs = map (#prop o rep_thm) thms val Tconcl = LA_Logic.mk_Trueprop concl -in case prove sg ([],Hs,Tconcl) of - [j] => prover1(j,sg,thms,Tconcl,true) - | [j1,j2] => prover2(j1,j2,sg,thms,Tconcl) - | _ => let val nTconcl = LA_Logic.neg_prop Tconcl - in case prove sg ([],Hs,nTconcl) of - [j] => prover1(j,sg,thms,nTconcl,false) - (* [_,_] impossible because of negation *) - | _ => None +in case prove sg ([],Hs,Tconcl) of (* concl provable? *) + Some js => prover sg thms Tconcl js true + | None => let val nTconcl = LA_Logic.neg_prop Tconcl + in case prove sg ([],Hs,nTconcl) of (* ~concl provable? *) + Some js => prover sg thms nTconcl js false + | None => None end end;