75 lessD: thm list, simpset: Simplifier.simpset} |
75 lessD: thm list, simpset: Simplifier.simpset} |
76 -> {add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list, |
76 -> {add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list, |
77 lessD: thm list, simpset: Simplifier.simpset}) |
77 lessD: thm list, simpset: Simplifier.simpset}) |
78 -> theory -> theory |
78 -> theory -> theory |
79 val trace : bool ref |
79 val trace : bool ref |
|
80 val fast_arith_neq_limit: int ref |
80 val lin_arith_prover: Sign.sg -> thm list -> term -> thm option |
81 val lin_arith_prover: Sign.sg -> thm list -> term -> thm option |
81 val lin_arith_tac: bool -> int -> tactic |
82 val lin_arith_tac: bool -> int -> tactic |
82 val cut_lin_arith_tac: thm list -> int -> tactic |
83 val cut_lin_arith_tac: thm list -> int -> tactic |
83 end; |
84 end; |
84 |
85 |
618 in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN |
619 in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN |
619 EVERY(map just1 justs) |
620 EVERY(map just1 justs) |
620 end |
621 end |
621 state; |
622 state; |
622 |
623 |
|
624 fun count P xs = length(filter P xs); |
|
625 |
|
626 (* The limit on the number of ~= allowed. |
|
627 Because each ~= is split into two cases, this can lead to an explosion. |
|
628 *) |
|
629 val fast_arith_neq_limit = ref 9; |
|
630 |
623 fun prove sg ps ex Hs concl = |
631 fun prove sg ps ex Hs concl = |
624 let val Hitems = map (LA_Data.decomp sg) Hs |
632 let val Hitems = map (LA_Data.decomp sg) Hs |
625 in case LA_Data.decomp sg concl of |
633 in if count (fn None => false | Some(_,_,r,_,_,_) => r = "~=") Hitems |
|
634 > !fast_arith_neq_limit then None |
|
635 else |
|
636 case LA_Data.decomp sg concl of |
626 None => refute sg ps ex (Hitems@[None]) |
637 None => refute sg ps ex (Hitems@[None]) |
627 | Some(citem as (r,i,rel,l,j,d)) => |
638 | Some(citem as (r,i,rel,l,j,d)) => |
628 let val neg::rel0 = explode rel |
639 let val neg::rel0 = explode rel |
629 val nrel = if neg = "~" then implode rel0 else "~"^rel |
640 val nrel = if neg = "~" then implode rel0 else "~"^rel |
630 in refute sg ps ex (Hitems @ [Some(r,i,nrel,l,j,d)]) end |
641 in refute sg ps ex (Hitems @ [Some(r,i,nrel,l,j,d)]) end |