equal
deleted
inserted
replaced
21 |
21 |
22 (*** Data needed for setting up the linear arithmetic package ***) |
22 (*** Data needed for setting up the linear arithmetic package ***) |
23 |
23 |
24 signature LIN_ARITH_LOGIC = |
24 signature LIN_ARITH_LOGIC = |
25 sig |
25 sig |
26 val conjI: thm |
26 val conjI: thm (* P ==> Q ==> P & Q *) |
27 val ccontr: thm (* (~ P ==> False) ==> P *) |
27 val ccontr: thm (* (~ P ==> False) ==> P *) |
28 val notI: thm (* (P ==> False) ==> ~ P *) |
28 val notI: thm (* (P ==> False) ==> ~ P *) |
29 val not_lessD: thm (* ~(m < n) ==> n <= m *) |
29 val not_lessD: thm (* ~(m < n) ==> n <= m *) |
30 val not_leD: thm (* ~(m <= n) ==> n < m *) |
30 val not_leD: thm (* ~(m <= n) ==> n < m *) |
31 val sym: thm (* x = y ==> y = x *) |
31 val sym: thm (* x = y ==> y = x *) |
74 val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
74 val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
75 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} |
75 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} |
76 -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
76 -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
77 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) |
77 lessD: thm list, neqE: 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 fast_arith_neq_limit: int ref |
81 val lin_arith_prover: theory -> simpset -> term -> thm option |
81 val lin_arith_prover: theory -> simpset -> term -> thm option |
82 val lin_arith_tac: bool -> int -> tactic |
82 val lin_arith_tac: bool -> int -> tactic |
83 val cut_lin_arith_tac: simpset -> int -> tactic |
83 val cut_lin_arith_tac: simpset -> int -> tactic |
84 end; |
84 end; |
589 fun discr initems = map fst (Library.foldl add_datoms ([],initems)); |
589 fun discr initems = map fst (Library.foldl add_datoms ([],initems)); |
590 |
590 |
591 fun refutes sg (pTs,params) ex = |
591 fun refutes sg (pTs,params) ex = |
592 let |
592 let |
593 fun refute (initems::initemss) js = |
593 fun refute (initems::initemss) js = |
594 let val atoms = Library.foldl add_atoms ([],initems) |
594 let val _ = trace_msg ("initems: " ^ makestring initems) (* TODO *) |
|
595 val atoms = Library.foldl add_atoms ([],initems) |
595 val n = length atoms |
596 val n = length atoms |
596 val mkleq = mklineq n atoms |
597 val mkleq = mklineq n atoms |
597 val ixs = 0 upto (n-1) |
598 val ixs = 0 upto (n-1) |
598 val iatoms = atoms ~~ ixs |
599 val iatoms = atoms ~~ ixs |
599 val natlineqs = List.mapPartial (mknat pTs ixs) iatoms |
600 val natlineqs = List.mapPartial (mknat pTs ixs) iatoms |
629 *) |
630 *) |
630 val fast_arith_neq_limit = ref 9; |
631 val fast_arith_neq_limit = ref 9; |
631 |
632 |
632 fun prove sg ps ex Hs concl = |
633 fun prove sg ps ex Hs concl = |
633 let val Hitems = map (LA_Data.decomp sg) Hs |
634 let val Hitems = map (LA_Data.decomp sg) Hs |
|
635 val _ = trace_msg ("Hitems: " ^ makestring Hitems) (* TODO *) |
634 in if count (fn NONE => false | SOME(_,_,r,_,_,_) => r = "~=") Hitems |
636 in if count (fn NONE => false | SOME(_,_,r,_,_,_) => r = "~=") Hitems |
635 > !fast_arith_neq_limit then NONE |
637 > !fast_arith_neq_limit then NONE |
636 else |
638 else |
637 case LA_Data.decomp sg concl of |
639 case LA_Data.decomp sg concl of |
638 NONE => refute sg ps ex (Hitems@[NONE]) |
640 NONE => refute sg ps ex (Hitems@[NONE]) |