src/Provers/Arith/fast_lin_arith.ML

 
 fun elim ineqs =
   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
   let val (eqs,noneqs) = partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
   if not(null eqs) then

         | mk(Multiplied2(n,j)) = simp (trace_msg("**"^string_of_int n); trace_thm "**" (multn2(n,mk j)))
 
   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 ([e-mail]).";
+             fls)
         end
      end handle FalseE thm => (trace_thm "False reached early:" thm; thm)
   end
 end;
 

         val lhsa = map (coeff lhs) atoms
         and rhsa = map (coeff rhs) atoms
         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
                   then lineq(1-c,Le,map (op ~) diff,NotLeDD(just))
                   else lineq(~c,Lt,map (op ~) diff,NotLeD(just))
        | "<"   => if discrete
                   then lineq(c+1,Le,diff,LessD(just))
                   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;
 
 fun mknat pTs ixs (atom,i) =
   if LA_Logic.is_nat(pTs,atom)
   then let val l = map (fn j => if j=i then 1 else 0) ixs
        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;
-
-(* Ordinary refutation *)
-fun refute1(pTs,items) =
-  (case elim (abstract pTs items) of
-       None => []
-     | Some(Lineq(_,_,_,j)) => [j]);
-
-fun refute1_tac(i,just) =
+      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
+
+  in elim_neq natlineqs 0 items end;
+
+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
+        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;
 
-(* 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
-    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
+(** 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;
+
+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;
+
+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 cnconcl Fthm) COMP contr)) end
-handle _ => None;
-
-(* 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;
-
-(* PRE: concl is not negated! *)
+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;
 
 end;