--- 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 *)
--- 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