--- 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<n ==> R; n<m ==> R|] ==> R *)
- val [lessimp1,lessimp2] = prems_of casethm
- val less1 = fst(Logic.dest_implies lessimp1) (* m<n *)
- and less2 = fst(Logic.dest_implies lessimp2) (* n<m *)
- val cless1 = cterm_of sg less1 and cless2 = cterm_of sg less2
- val thm1 = mkthm sg (thms @ [assume cless1]) just1
- and thm2 = mkthm sg (thms @ [assume cless2]) just2
- val dthm1 = implies_intr cless1 thm1 and dthm2 = implies_intr cless2 thm2
- val thm = dthm2 COMP (dthm1 COMP casethm)
-in Some(LA_Logic.mk_Eq ((implies_intr cnconcl thm) COMP LA_Logic.ccontr)) end
-handle _ => 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;