src/Provers/Arith/fast_lin_arith.ML
 author haftmann Mon May 11 15:57:30 2009 +0200 (2009-05-11) changeset 31102 f1e3100e6c49 parent 30687 16f6efd4e599 child 31510 e0f2bb4b0021 permissions -rw-r--r--
mk_number replaces number_of
 nipkow@5982 ` 1` ```(* Title: Provers/Arith/fast_lin_arith.ML ``` nipkow@5982 ` 2` ``` ID: \$Id\$ ``` wenzelm@24076 ` 3` ``` Author: Tobias Nipkow and Tjark Weber ``` nipkow@6102 ` 4` wenzelm@24076 ` 5` ```A generic linear arithmetic package. It provides two tactics ``` wenzelm@24076 ` 6` ```(cut_lin_arith_tac, lin_arith_tac) and a simplification procedure ``` wenzelm@24076 ` 7` ```(lin_arith_simproc). ``` nipkow@6102 ` 8` wenzelm@24076 ` 9` ```Only take premises and conclusions into account that are already ``` wenzelm@24076 ` 10` ```(negated) (in)equations. lin_arith_simproc tries to prove or disprove ``` wenzelm@24076 ` 11` ```the term. ``` nipkow@5982 ` 12` ```*) ``` nipkow@5982 ` 13` nipkow@5982 ` 14` ```(*** Data needed for setting up the linear arithmetic package ***) ``` nipkow@5982 ` 15` nipkow@6102 ` 16` ```signature LIN_ARITH_LOGIC = ``` nipkow@6102 ` 17` ```sig ``` webertj@20276 ` 18` ``` val conjI : thm (* P ==> Q ==> P & Q *) ``` webertj@20276 ` 19` ``` val ccontr : thm (* (~ P ==> False) ==> P *) ``` webertj@20276 ` 20` ``` val notI : thm (* (P ==> False) ==> ~ P *) ``` webertj@20276 ` 21` ``` val not_lessD : thm (* ~(m < n) ==> n <= m *) ``` webertj@20276 ` 22` ``` val not_leD : thm (* ~(m <= n) ==> n < m *) ``` webertj@20276 ` 23` ``` val sym : thm (* x = y ==> y = x *) ``` webertj@20276 ` 24` ``` val mk_Eq : thm -> thm ``` webertj@20276 ` 25` ``` val atomize : thm -> thm list ``` webertj@20276 ` 26` ``` val mk_Trueprop : term -> term ``` webertj@20276 ` 27` ``` val neg_prop : term -> term ``` webertj@20276 ` 28` ``` val is_False : thm -> bool ``` webertj@20276 ` 29` ``` val is_nat : typ list * term -> bool ``` webertj@20276 ` 30` ``` val mk_nat_thm : theory -> term -> thm ``` nipkow@6102 ` 31` ```end; ``` nipkow@6102 ` 32` ```(* ``` nipkow@6102 ` 33` ```mk_Eq(~in) = `in == False' ``` nipkow@6102 ` 34` ```mk_Eq(in) = `in == True' ``` nipkow@6102 ` 35` ```where `in' is an (in)equality. ``` nipkow@6102 ` 36` webertj@23190 ` 37` ```neg_prop(t) = neg if t is wrapped up in Trueprop and neg is the ``` webertj@23190 ` 38` ``` (logically) negated version of t (again wrapped up in Trueprop), ``` webertj@23190 ` 39` ``` where the negation of a negative term is the term itself (no ``` webertj@23190 ` 40` ``` double negation!); raises TERM ("neg_prop", [t]) if t is not of ``` webertj@23190 ` 41` ``` the form 'Trueprop \$ _' ``` nipkow@6128 ` 42` nipkow@6128 ` 43` ```is_nat(parameter-types,t) = t:nat ``` nipkow@6128 ` 44` ```mk_nat_thm(t) = "0 <= t" ``` nipkow@6102 ` 45` ```*) ``` nipkow@6102 ` 46` nipkow@5982 ` 47` ```signature LIN_ARITH_DATA = ``` nipkow@5982 ` 48` ```sig ``` wenzelm@24076 ` 49` ``` (*internal representation of linear (in-)equations:*) ``` wenzelm@26945 ` 50` ``` type decomp = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool ``` wenzelm@26945 ` 51` ``` val decomp: Proof.context -> term -> decomp option ``` wenzelm@24076 ` 52` ``` val domain_is_nat: term -> bool ``` wenzelm@24076 ` 53` wenzelm@24076 ` 54` ``` (*preprocessing, performed on a representation of subgoals as list of premises:*) ``` wenzelm@24076 ` 55` ``` val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list ``` wenzelm@24076 ` 56` wenzelm@24076 ` 57` ``` (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*) ``` wenzelm@24076 ` 58` ``` val pre_tac: Proof.context -> int -> tactic ``` haftmann@31102 ` 59` ``` val mk_number: typ -> int -> term ``` wenzelm@24076 ` 60` wenzelm@24076 ` 61` ``` (*the limit on the number of ~= allowed; because each ~= is split ``` wenzelm@24076 ` 62` ``` into two cases, this can lead to an explosion*) ``` wenzelm@24112 ` 63` ``` val fast_arith_neq_limit: int Config.T ``` nipkow@5982 ` 64` ```end; ``` nipkow@5982 ` 65` ```(* ``` nipkow@7551 ` 66` ```decomp(`x Rel y') should yield (p,i,Rel,q,j,d) ``` nipkow@5982 ` 67` ``` where Rel is one of "<", "~<", "<=", "~<=" and "=" and ``` webertj@20217 ` 68` ``` p (q, respectively) is the decomposition of the sum term x ``` webertj@20217 ` 69` ``` (y, respectively) into a list of summand * multiplicity ``` webertj@20217 ` 70` ``` pairs and a constant summand and d indicates if the domain ``` webertj@20217 ` 71` ``` is discrete. ``` webertj@20217 ` 72` webertj@20276 ` 73` ```domain_is_nat(`x Rel y') t should yield true iff x is of type "nat". ``` webertj@20276 ` 74` webertj@20217 ` 75` ```The relationship between pre_decomp and pre_tac is somewhat tricky. The ``` webertj@20217 ` 76` ```internal representation of a subgoal and the corresponding theorem must ``` webertj@20217 ` 77` ```be modified by pre_decomp (pre_tac, resp.) in a corresponding way. See ``` webertj@20217 ` 78` ```the comment for split_items below. (This is even necessary for eta- and ``` webertj@20217 ` 79` ```beta-equivalent modifications, as some of the lin. arith. code is not ``` webertj@20217 ` 80` ```insensitive to them.) ``` nipkow@5982 ` 81` wenzelm@9420 ` 82` ```ss must reduce contradictory <= to False. ``` nipkow@5982 ` 83` ``` It should also cancel common summands to keep <= reduced; ``` nipkow@5982 ` 84` ``` otherwise <= can grow to massive proportions. ``` nipkow@5982 ` 85` ```*) ``` nipkow@5982 ` 86` nipkow@6062 ` 87` ```signature FAST_LIN_ARITH = ``` nipkow@6062 ` 88` ```sig ``` haftmann@31102 ` 89` ``` val cut_lin_arith_tac: simpset -> int -> tactic ``` haftmann@31102 ` 90` ``` val lin_arith_tac: Proof.context -> bool -> int -> tactic ``` haftmann@31102 ` 91` ``` val lin_arith_simproc: simpset -> term -> thm option ``` nipkow@15184 ` 92` ``` val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, ``` nipkow@15922 ` 93` ``` lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} ``` nipkow@15184 ` 94` ``` -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, ``` nipkow@15922 ` 95` ``` lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) ``` wenzelm@24076 ` 96` ``` -> Context.generic -> Context.generic ``` webertj@19314 ` 97` ``` val trace: bool ref ``` wenzelm@27020 ` 98` ``` val warning_count: int ref; ``` nipkow@6062 ` 99` ```end; ``` nipkow@6062 ` 100` wenzelm@24076 ` 101` ```functor Fast_Lin_Arith ``` wenzelm@24076 ` 102` ``` (structure LA_Logic: LIN_ARITH_LOGIC and LA_Data: LIN_ARITH_DATA): FAST_LIN_ARITH = ``` nipkow@5982 ` 103` ```struct ``` nipkow@5982 ` 104` wenzelm@9420 ` 105` wenzelm@9420 ` 106` ```(** theory data **) ``` wenzelm@9420 ` 107` wenzelm@24076 ` 108` ```structure Data = GenericDataFun ``` wenzelm@22846 ` 109` ```( ``` wenzelm@24076 ` 110` ``` type T = ``` wenzelm@24076 ` 111` ``` {add_mono_thms: thm list, ``` wenzelm@24076 ` 112` ``` mult_mono_thms: thm list, ``` wenzelm@24076 ` 113` ``` inj_thms: thm list, ``` wenzelm@24076 ` 114` ``` lessD: thm list, ``` wenzelm@24076 ` 115` ``` neqE: thm list, ``` wenzelm@24076 ` 116` ``` simpset: Simplifier.simpset}; ``` wenzelm@9420 ` 117` nipkow@10691 ` 118` ``` val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], ``` nipkow@15922 ` 119` ``` lessD = [], neqE = [], simpset = Simplifier.empty_ss}; ``` wenzelm@16458 ` 120` ``` val extend = I; ``` wenzelm@16458 ` 121` ``` fun merge _ ``` wenzelm@16458 ` 122` ``` ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, ``` wenzelm@16458 ` 123` ``` lessD = lessD1, neqE=neqE1, simpset = simpset1}, ``` wenzelm@16458 ` 124` ``` {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, ``` wenzelm@16458 ` 125` ``` lessD = lessD2, neqE=neqE2, simpset = simpset2}) = ``` wenzelm@24039 ` 126` ``` {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2), ``` wenzelm@24039 ` 127` ``` mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2), ``` wenzelm@24039 ` 128` ``` inj_thms = Thm.merge_thms (inj_thms1, inj_thms2), ``` wenzelm@24039 ` 129` ``` lessD = Thm.merge_thms (lessD1, lessD2), ``` wenzelm@24039 ` 130` ``` neqE = Thm.merge_thms (neqE1, neqE2), ``` nipkow@10575 ` 131` ``` simpset = Simplifier.merge_ss (simpset1, simpset2)}; ``` wenzelm@22846 ` 132` ```); ``` wenzelm@9420 ` 133` wenzelm@9420 ` 134` ```val map_data = Data.map; ``` wenzelm@24076 ` 135` ```val get_data = Data.get o Context.Proof; ``` wenzelm@9420 ` 136` wenzelm@9420 ` 137` wenzelm@9420 ` 138` nipkow@5982 ` 139` ```(*** A fast decision procedure ***) ``` nipkow@5982 ` 140` ```(*** Code ported from HOL Light ***) ``` nipkow@6056 ` 141` ```(* possible optimizations: ``` nipkow@6056 ` 142` ``` use (var,coeff) rep or vector rep tp save space; ``` nipkow@6056 ` 143` ``` treat non-negative atoms separately rather than adding 0 <= atom ``` nipkow@6056 ` 144` ```*) ``` nipkow@5982 ` 145` paulson@9073 ` 146` ```val trace = ref false; ``` paulson@9073 ` 147` nipkow@5982 ` 148` ```datatype lineq_type = Eq | Le | Lt; ``` nipkow@5982 ` 149` nipkow@6056 ` 150` ```datatype injust = Asm of int ``` nipkow@6056 ` 151` ``` | Nat of int (* index of atom *) ``` nipkow@6128 ` 152` ``` | LessD of injust ``` nipkow@6128 ` 153` ``` | NotLessD of injust ``` nipkow@6128 ` 154` ``` | NotLeD of injust ``` nipkow@7551 ` 155` ``` | NotLeDD of injust ``` wenzelm@24630 ` 156` ``` | Multiplied of int * injust ``` wenzelm@24630 ` 157` ``` | Multiplied2 of int * injust ``` nipkow@5982 ` 158` ``` | Added of injust * injust; ``` nipkow@5982 ` 159` wenzelm@24630 ` 160` ```datatype lineq = Lineq of int * lineq_type * int list * injust; ``` nipkow@5982 ` 161` nipkow@13498 ` 162` ```(* ------------------------------------------------------------------------- *) ``` nipkow@13498 ` 163` ```(* Finding a (counter) example from the trace of a failed elimination *) ``` nipkow@13498 ` 164` ```(* ------------------------------------------------------------------------- *) ``` nipkow@13498 ` 165` ```(* Examples are represented as rational numbers, *) ``` nipkow@13498 ` 166` ```(* Dont blame John Harrison for this code - it is entirely mine. TN *) ``` nipkow@13498 ` 167` nipkow@13498 ` 168` ```exception NoEx; ``` nipkow@13498 ` 169` nipkow@14372 ` 170` ```(* Coding: (i,true,cs) means i <= cs and (i,false,cs) means i < cs. ``` nipkow@14372 ` 171` ``` In general, true means the bound is included, false means it is excluded. ``` nipkow@14372 ` 172` ``` Need to know if it is a lower or upper bound for unambiguous interpretation! ``` nipkow@14372 ` 173` ```*) ``` nipkow@14372 ` 174` haftmann@22950 ` 175` ```fun elim_eqns (Lineq (i, Le, cs, _)) = [(i, true, cs)] ``` haftmann@22950 ` 176` ``` | elim_eqns (Lineq (i, Eq, cs, _)) = [(i, true, cs),(~i, true, map ~ cs)] ``` haftmann@22950 ` 177` ``` | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)]; ``` nipkow@13498 ` 178` nipkow@13498 ` 179` ```(* PRE: ex[v] must be 0! *) ``` wenzelm@24630 ` 180` ```fun eval ex v (a, le, cs) = ``` haftmann@22950 ` 181` ``` let ``` haftmann@22950 ` 182` ``` val rs = map Rat.rat_of_int cs; ``` haftmann@22950 ` 183` ``` val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero; ``` haftmann@23063 ` 184` ``` in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (nth rs v)), le) end; ``` haftmann@23063 ` 185` ```(* If nth rs v < 0, le should be negated. ``` nipkow@14372 ` 186` ``` Instead this swap is taken into account in ratrelmin2. ``` nipkow@14372 ` 187` ```*) ``` nipkow@13498 ` 188` haftmann@22950 ` 189` ```fun ratrelmin2 (x as (r, ler), y as (s, les)) = ``` haftmann@23520 ` 190` ``` case Rat.ord (r, s) ``` haftmann@22950 ` 191` ``` of EQUAL => (r, (not ler) andalso (not les)) ``` haftmann@22950 ` 192` ``` | LESS => x ``` haftmann@22950 ` 193` ``` | GREATER => y; ``` haftmann@22950 ` 194` haftmann@22950 ` 195` ```fun ratrelmax2 (x as (r, ler), y as (s, les)) = ``` haftmann@23520 ` 196` ``` case Rat.ord (r, s) ``` haftmann@22950 ` 197` ``` of EQUAL => (r, ler andalso les) ``` haftmann@22950 ` 198` ``` | LESS => y ``` haftmann@22950 ` 199` ``` | GREATER => x; ``` nipkow@13498 ` 200` nipkow@14372 ` 201` ```val ratrelmin = foldr1 ratrelmin2; ``` nipkow@14372 ` 202` ```val ratrelmax = foldr1 ratrelmax2; ``` nipkow@13498 ` 203` haftmann@22950 ` 204` ```fun ratexact up (r, exact) = ``` nipkow@14372 ` 205` ``` if exact then r else ``` haftmann@22950 ` 206` ``` let ``` haftmann@22950 ` 207` ``` val (p, q) = Rat.quotient_of_rat r; ``` haftmann@22950 ` 208` ``` val nth = Rat.inv (Rat.rat_of_int q); ``` haftmann@22950 ` 209` ``` in Rat.add r (if up then nth else Rat.neg nth) end; ``` nipkow@14372 ` 210` haftmann@22950 ` 211` ```fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two); ``` nipkow@14372 ` 212` webertj@20217 ` 213` ```fun choose2 d ((lb, exactl), (ub, exactu)) = ``` haftmann@23520 ` 214` ``` let val ord = Rat.sign lb in ``` haftmann@22950 ` 215` ``` if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu) ``` haftmann@22950 ` 216` ``` then Rat.zero ``` haftmann@22950 ` 217` ``` else if not d then ``` haftmann@22950 ` 218` ``` if ord = GREATER ``` webertj@20217 ` 219` ``` then if exactl then lb else ratmiddle (lb, ub) ``` haftmann@22950 ` 220` ``` else if exactu then ub else ratmiddle (lb, ub) ``` haftmann@22950 ` 221` ``` else (*discrete domain, both bounds must be exact*) ``` haftmann@23025 ` 222` ``` if ord = GREATER ``` haftmann@22950 ` 223` ``` then let val lb' = Rat.roundup lb in ``` haftmann@22950 ` 224` ``` if Rat.le lb' ub then lb' else raise NoEx end ``` haftmann@22950 ` 225` ``` else let val ub' = Rat.rounddown ub in ``` haftmann@22950 ` 226` ``` if Rat.le lb ub' then ub' else raise NoEx end ``` haftmann@22950 ` 227` ``` end; ``` nipkow@13498 ` 228` haftmann@22950 ` 229` ```fun findex1 discr (v, lineqs) ex = ``` haftmann@22950 ` 230` ``` let ``` haftmann@23063 ` 231` ``` val nz = filter (fn (Lineq (_, _, cs, _)) => nth cs v <> 0) lineqs; ``` haftmann@22950 ` 232` ``` val ineqs = maps elim_eqns nz; ``` haftmann@23063 ` 233` ``` val (ge, le) = List.partition (fn (_,_,cs) => nth cs v > 0) ineqs ``` haftmann@22950 ` 234` ``` val lb = ratrelmax (map (eval ex v) ge) ``` haftmann@22950 ` 235` ``` val ub = ratrelmin (map (eval ex v) le) ``` haftmann@21109 ` 236` ``` in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end; ``` nipkow@13498 ` 237` nipkow@13498 ` 238` ```fun elim1 v x = ``` haftmann@23063 ` 239` ``` map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le, ``` haftmann@21109 ` 240` ``` nth_map v (K Rat.zero) bs)); ``` nipkow@13498 ` 241` haftmann@23520 ` 242` ```fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.sign) cs ``` haftmann@23063 ` 243` ``` of [x] => x =/ nth cs v ``` haftmann@23063 ` 244` ``` | _ => false; ``` nipkow@13498 ` 245` nipkow@13498 ` 246` ```(* The base case: ``` nipkow@13498 ` 247` ``` all variables occur only with positive or only with negative coefficients *) ``` nipkow@13498 ` 248` ```fun pick_vars discr (ineqs,ex) = ``` haftmann@23520 ` 249` ``` let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.sign) cs) ineqs ``` nipkow@14372 ` 250` ``` in case nz of [] => ex ``` nipkow@14372 ` 251` ``` | (_,_,cs) :: _ => ``` haftmann@23520 ` 252` ``` let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs ``` haftmann@22950 ` 253` ``` val d = nth discr v; ``` haftmann@23520 ` 254` ``` val pos = not (Rat.sign (nth cs v) = LESS); ``` haftmann@22950 ` 255` ``` val sv = filter (single_var v) nz; ``` nipkow@14372 ` 256` ``` val minmax = ``` haftmann@17951 ` 257` ``` if pos then if d then Rat.roundup o fst o ratrelmax ``` nipkow@14372 ` 258` ``` else ratexact true o ratrelmax ``` haftmann@17951 ` 259` ``` else if d then Rat.rounddown o fst o ratrelmin ``` nipkow@14372 ` 260` ``` else ratexact false o ratrelmin ``` haftmann@23063 ` 261` ``` val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (nth bs v)), le)) sv ``` haftmann@17951 ` 262` ``` val x = minmax((Rat.zero,if pos then true else false)::bnds) ``` nipkow@14372 ` 263` ``` val ineqs' = elim1 v x nz ``` haftmann@21109 ` 264` ``` val ex' = nth_map v (K x) ex ``` nipkow@14372 ` 265` ``` in pick_vars discr (ineqs',ex') end ``` nipkow@13498 ` 266` ``` end; ``` nipkow@13498 ` 267` nipkow@13498 ` 268` ```fun findex0 discr n lineqs = ``` haftmann@22950 ` 269` ``` let val ineqs = maps elim_eqns lineqs ``` haftmann@22950 ` 270` ``` val rineqs = map (fn (a,le,cs) => (Rat.rat_of_int a, le, map Rat.rat_of_int cs)) ``` nipkow@14372 ` 271` ``` ineqs ``` haftmann@17951 ` 272` ``` in pick_vars discr (rineqs,replicate n Rat.zero) end; ``` nipkow@13498 ` 273` nipkow@13498 ` 274` ```(* ------------------------------------------------------------------------- *) ``` webertj@23197 ` 275` ```(* End of counterexample finder. The actual decision procedure starts here. *) ``` nipkow@13498 ` 276` ```(* ------------------------------------------------------------------------- *) ``` nipkow@13498 ` 277` nipkow@5982 ` 278` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 279` ```(* Calculate new (in)equality type after addition. *) ``` nipkow@5982 ` 280` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 281` nipkow@5982 ` 282` ```fun find_add_type(Eq,x) = x ``` nipkow@5982 ` 283` ``` | find_add_type(x,Eq) = x ``` nipkow@5982 ` 284` ``` | find_add_type(_,Lt) = Lt ``` nipkow@5982 ` 285` ``` | find_add_type(Lt,_) = Lt ``` nipkow@5982 ` 286` ``` | find_add_type(Le,Le) = Le; ``` nipkow@5982 ` 287` nipkow@5982 ` 288` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 289` ```(* Multiply out an (in)equation. *) ``` nipkow@5982 ` 290` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 291` nipkow@5982 ` 292` ```fun multiply_ineq n (i as Lineq(k,ty,l,just)) = ``` nipkow@5982 ` 293` ``` if n = 1 then i ``` nipkow@5982 ` 294` ``` else if n = 0 andalso ty = Lt then sys_error "multiply_ineq" ``` nipkow@5982 ` 295` ``` else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq" ``` paulson@17524 ` 296` ``` else Lineq (n * k, ty, map (curry op* n) l, Multiplied (n, just)); ``` nipkow@5982 ` 297` nipkow@5982 ` 298` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 299` ```(* Add together (in)equations. *) ``` nipkow@5982 ` 300` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 301` nipkow@5982 ` 302` ```fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = ``` haftmann@18330 ` 303` ``` let val l = map2 (curry (op +)) l1 l2 ``` nipkow@5982 ` 304` ``` in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end; ``` nipkow@5982 ` 305` nipkow@5982 ` 306` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 307` ```(* Elimination of variable between a single pair of (in)equations. *) ``` nipkow@5982 ` 308` ```(* If they're both inequalities, 1st coefficient must be +ve, 2nd -ve. *) ``` nipkow@5982 ` 309` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 310` nipkow@5982 ` 311` ```fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = ``` haftmann@23063 ` 312` ``` let val c1 = nth l1 v and c2 = nth l2 v ``` haftmann@23261 ` 313` ``` val m = Integer.lcm (abs c1) (abs c2) ``` nipkow@5982 ` 314` ``` val m1 = m div (abs c1) and m2 = m div (abs c2) ``` nipkow@5982 ` 315` ``` val (n1,n2) = ``` nipkow@5982 ` 316` ``` if (c1 >= 0) = (c2 >= 0) ``` nipkow@5982 ` 317` ``` then if ty1 = Eq then (~m1,m2) ``` nipkow@5982 ` 318` ``` else if ty2 = Eq then (m1,~m2) ``` nipkow@5982 ` 319` ``` else sys_error "elim_var" ``` nipkow@5982 ` 320` ``` else (m1,m2) ``` nipkow@5982 ` 321` ``` val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1) ``` nipkow@5982 ` 322` ``` then (~n1,~n2) else (n1,n2) ``` nipkow@5982 ` 323` ``` in add_ineq (multiply_ineq n1 i1) (multiply_ineq n2 i2) end; ``` nipkow@5982 ` 324` nipkow@5982 ` 325` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 326` ```(* The main refutation-finding code. *) ``` nipkow@5982 ` 327` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 328` nipkow@5982 ` 329` ```fun is_trivial (Lineq(_,_,l,_)) = forall (fn i => i=0) l; ``` nipkow@5982 ` 330` nipkow@5982 ` 331` ```fun is_answer (ans as Lineq(k,ty,l,_)) = ``` nipkow@5982 ` 332` ``` case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0; ``` nipkow@5982 ` 333` wenzelm@24630 ` 334` ```fun calc_blowup l = ``` haftmann@17496 ` 335` ``` let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l) ``` wenzelm@24630 ` 336` ``` in length p * length n end; ``` nipkow@5982 ` 337` nipkow@5982 ` 338` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 339` ```(* Main elimination code: *) ``` nipkow@5982 ` 340` ```(* *) ``` nipkow@5982 ` 341` ```(* (1) Looks for immediate solutions (false assertions with no variables). *) ``` nipkow@5982 ` 342` ```(* *) ``` nipkow@5982 ` 343` ```(* (2) If there are any equations, picks a variable with the lowest absolute *) ``` nipkow@5982 ` 344` ```(* coefficient in any of them, and uses it to eliminate. *) ``` nipkow@5982 ` 345` ```(* *) ``` nipkow@5982 ` 346` ```(* (3) Otherwise, chooses a variable in the inequality to minimize the *) ``` nipkow@5982 ` 347` ```(* blowup (number of consequences generated) and eliminates it. *) ``` nipkow@5982 ` 348` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 349` nipkow@5982 ` 350` ```fun allpairs f xs ys = ``` wenzelm@26945 ` 351` ``` maps (fn x => map (fn y => f x y) ys) xs; ``` nipkow@5982 ` 352` nipkow@5982 ` 353` ```fun extract_first p = ``` skalberg@15531 ` 354` ``` let fun extract xs (y::ys) = if p y then (SOME y,xs@ys) ``` nipkow@5982 ` 355` ``` else extract (y::xs) ys ``` skalberg@15531 ` 356` ``` | extract xs [] = (NONE,xs) ``` nipkow@5982 ` 357` ``` in extract [] end; ``` nipkow@5982 ` 358` nipkow@6056 ` 359` ```fun print_ineqs ineqs = ``` paulson@9073 ` 360` ``` if !trace then ``` wenzelm@12262 ` 361` ``` tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => ``` wenzelm@24630 ` 362` ``` string_of_int c ^ ``` paulson@9073 ` 363` ``` (case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ ``` wenzelm@24630 ` 364` ``` commas(map string_of_int l)) ineqs)) ``` paulson@9073 ` 365` ``` else (); ``` nipkow@6056 ` 366` nipkow@13498 ` 367` ```type history = (int * lineq list) list; ``` nipkow@13498 ` 368` ```datatype result = Success of injust | Failure of history; ``` nipkow@13498 ` 369` webertj@20217 ` 370` ```fun elim (ineqs, hist) = ``` webertj@20217 ` 371` ``` let val dummy = print_ineqs ineqs ``` webertj@20217 ` 372` ``` val (triv, nontriv) = List.partition is_trivial ineqs in ``` webertj@20217 ` 373` ``` if not (null triv) ``` nipkow@13186 ` 374` ``` then case Library.find_first is_answer triv of ``` webertj@20217 ` 375` ``` NONE => elim (nontriv, hist) ``` skalberg@15531 ` 376` ``` | SOME(Lineq(_,_,_,j)) => Success j ``` nipkow@5982 ` 377` ``` else ``` webertj@20217 ` 378` ``` if null nontriv then Failure hist ``` nipkow@13498 ` 379` ``` else ``` webertj@20217 ` 380` ``` let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in ``` webertj@20217 ` 381` ``` if not (null eqs) then ``` skalberg@15570 ` 382` ``` let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) ``` wenzelm@24630 ` 383` ``` val sclist = sort (fn (x,y) => int_ord (abs x, abs y)) ``` skalberg@15570 ` 384` ``` (List.filter (fn i => i<>0) clist) ``` nipkow@5982 ` 385` ``` val c = hd sclist ``` skalberg@15531 ` 386` ``` val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) = ``` nipkow@5982 ` 387` ``` extract_first (fn Lineq(_,_,l,_) => c mem l) eqs ``` webertj@20217 ` 388` ``` val v = find_index_eq c ceq ``` haftmann@23063 ` 389` ``` val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ``` nipkow@5982 ` 390` ``` (othereqs @ noneqs) ``` nipkow@5982 ` 391` ``` val others = map (elim_var v eq) roth @ ioth ``` nipkow@13498 ` 392` ``` in elim(others,(v,nontriv)::hist) end ``` nipkow@5982 ` 393` ``` else ``` nipkow@5982 ` 394` ``` let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs ``` haftmann@23063 ` 395` ``` val numlist = 0 upto (length (hd lists) - 1) ``` haftmann@23063 ` 396` ``` val coeffs = map (fn i => map (fn xs => nth xs i) lists) numlist ``` nipkow@5982 ` 397` ``` val blows = map calc_blowup coeffs ``` nipkow@5982 ` 398` ``` val iblows = blows ~~ numlist ``` haftmann@23063 ` 399` ``` val nziblows = filter_out (fn (i, _) => i = 0) iblows ``` nipkow@13498 ` 400` ``` in if null nziblows then Failure((~1,nontriv)::hist) ``` nipkow@13498 ` 401` ``` else ``` nipkow@5982 ` 402` ``` let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) ``` haftmann@23063 ` 403` ``` val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs ``` haftmann@23063 ` 404` ``` val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes ``` nipkow@13498 ` 405` ``` in elim(no @ allpairs (elim_var v) pos neg, (v,nontriv)::hist) end ``` nipkow@5982 ` 406` ``` end ``` nipkow@5982 ` 407` ``` end ``` nipkow@5982 ` 408` ``` end; ``` nipkow@5982 ` 409` nipkow@5982 ` 410` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 411` ```(* Translate back a proof. *) ``` nipkow@5982 ` 412` ```(* ------------------------------------------------------------------------- *) ``` nipkow@5982 ` 413` wenzelm@24076 ` 414` ```fun trace_thm msg th = ``` wenzelm@24076 ` 415` ``` (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th); ``` paulson@9073 ` 416` wenzelm@24076 ` 417` ```fun trace_term ctxt msg t = ``` wenzelm@24920 ` 418` ``` (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t) ``` wenzelm@24076 ` 419` wenzelm@24076 ` 420` ```fun trace_msg msg = ``` wenzelm@24076 ` 421` ``` if !trace then tracing msg else (); ``` paulson@9073 ` 422` wenzelm@27020 ` 423` ```val warning_count = ref 0; ``` wenzelm@27020 ` 424` ```val warning_count_max = 10; ``` wenzelm@27020 ` 425` berghofe@26835 ` 426` ```val union_term = curry (gen_union Pattern.aeconv); ``` berghofe@26835 ` 427` ```val union_bterm = curry (gen_union ``` berghofe@26835 ` 428` ``` (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'))); ``` berghofe@26835 ` 429` nipkow@13498 ` 430` ```(* FIXME OPTIMIZE!!!! (partly done already) ``` nipkow@6056 ` 431` ``` Addition/Multiplication need i*t representation rather than t+t+... ``` haftmann@31102 ` 432` ``` Get rid of Mulitplied(2). For Nat LA_Data.mk_number should return Suc^n ``` nipkow@10691 ` 433` ``` because Numerals are not known early enough. ``` nipkow@6056 ` 434` nipkow@6056 ` 435` ```Simplification may detect a contradiction 'prematurely' due to type ``` nipkow@6056 ` 436` ```information: n+1 <= 0 is simplified to False and does not need to be crossed ``` nipkow@6056 ` 437` ```with 0 <= n. ``` nipkow@6056 ` 438` ```*) ``` nipkow@6056 ` 439` ```local ``` wenzelm@24076 ` 440` ``` exception FalseE of thm ``` nipkow@6056 ` 441` ```in ``` wenzelm@27020 ` 442` wenzelm@24076 ` 443` ```fun mkthm ss asms (just: injust) = ``` wenzelm@24076 ` 444` ``` let ``` wenzelm@24076 ` 445` ``` val ctxt = Simplifier.the_context ss; ``` wenzelm@24076 ` 446` ``` val thy = ProofContext.theory_of ctxt; ``` wenzelm@24076 ` 447` ``` val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt; ``` wenzelm@24076 ` 448` ``` val simpset' = Simplifier.inherit_context ss simpset; ``` wenzelm@24076 ` 449` ``` val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) => ``` berghofe@26835 ` 450` ``` union_term (map fst lhs) (union_term (map fst rhs) ats)) ``` webertj@20217 ` 451` ``` ([], List.mapPartial (fn thm => if Thm.no_prems thm ``` wenzelm@24076 ` 452` ``` then LA_Data.decomp ctxt (Thm.concl_of thm) ``` webertj@20217 ` 453` ``` else NONE) asms) ``` nipkow@6056 ` 454` nipkow@10575 ` 455` ``` fun add2 thm1 thm2 = ``` nipkow@6102 ` 456` ``` let val conj = thm1 RS (thm2 RS LA_Logic.conjI) ``` skalberg@15531 ` 457` ``` in get_first (fn th => SOME(conj RS th) handle THM _ => NONE) add_mono_thms ``` nipkow@5982 ` 458` ``` end; ``` skalberg@15531 ` 459` ``` fun try_add [] _ = NONE ``` nipkow@10575 ` 460` ``` | try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of ``` skalberg@15531 ` 461` ``` NONE => try_add thm1s thm2 | some => some; ``` nipkow@10575 ` 462` nipkow@10575 ` 463` ``` fun addthms thm1 thm2 = ``` nipkow@10575 ` 464` ``` case add2 thm1 thm2 of ``` skalberg@15531 ` 465` ``` NONE => (case try_add ([thm1] RL inj_thms) thm2 of ``` webertj@20217 ` 466` ``` NONE => ( the (try_add ([thm2] RL inj_thms) thm1) ``` wenzelm@15660 ` 467` ``` handle Option => ``` nipkow@14360 ` 468` ``` (trace_thm "" thm1; trace_thm "" thm2; ``` haftmann@30687 ` 469` ``` sys_error "Linear arithmetic: failed to add thms") ``` webertj@20217 ` 470` ``` ) ``` skalberg@15531 ` 471` ``` | SOME thm => thm) ``` skalberg@15531 ` 472` ``` | SOME thm => thm; ``` nipkow@10575 ` 473` nipkow@5982 ` 474` ``` fun multn(n,thm) = ``` nipkow@5982 ` 475` ``` let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th) ``` nipkow@6102 ` 476` ``` in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end; ``` webertj@20217 ` 477` nipkow@15184 ` 478` ``` fun multn2(n,thm) = ``` skalberg@15531 ` 479` ``` let val SOME(mth) = ``` skalberg@15531 ` 480` ``` get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms ``` wenzelm@22596 ` 481` ``` fun cvar(th,_ \$ (_ \$ _ \$ var)) = cterm_of (Thm.theory_of_thm th) var; ``` nipkow@15184 ` 482` ``` val cv = cvar(mth, hd(prems_of mth)); ``` haftmann@31102 ` 483` ``` val ct = cterm_of thy (LA_Data.mk_number (#T (rep_cterm cv)) n) ``` nipkow@15184 ` 484` ``` in instantiate ([],[(cv,ct)]) mth end ``` nipkow@10691 ` 485` nipkow@6056 ` 486` ``` fun simp thm = ``` wenzelm@17515 ` 487` ``` let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm) ``` nipkow@6102 ` 488` ``` in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end ``` nipkow@6056 ` 489` wenzelm@24076 ` 490` ``` fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i) ``` wenzelm@24076 ` 491` ``` | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i)) ``` webertj@20254 ` 492` ``` | mk (LessD j) = trace_thm "L" (hd ([mk j] RL lessD)) ``` webertj@20254 ` 493` ``` | mk (NotLeD j) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) ``` webertj@20254 ` 494` ``` | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) ``` webertj@20254 ` 495` ``` | mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) ``` webertj@20254 ` 496` ``` | mk (Added (j1, j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) ``` wenzelm@24630 ` 497` ``` | mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j))) ``` wenzelm@24630 ` 498` ``` | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j))) ``` nipkow@5982 ` 499` wenzelm@27020 ` 500` ``` in ``` wenzelm@27020 ` 501` ``` let ``` wenzelm@27020 ` 502` ``` val _ = trace_msg "mkthm"; ``` wenzelm@27020 ` 503` ``` val thm = trace_thm "Final thm:" (mk just); ``` wenzelm@27020 ` 504` ``` val fls = simplify simpset' thm; ``` wenzelm@27020 ` 505` ``` val _ = trace_thm "After simplification:" fls; ``` wenzelm@27020 ` 506` ``` val _ = ``` wenzelm@27020 ` 507` ``` if LA_Logic.is_False fls then () ``` wenzelm@27020 ` 508` ``` else ``` wenzelm@27020 ` 509` ``` let val count = CRITICAL (fn () => inc warning_count) in ``` wenzelm@27020 ` 510` ``` if count > warning_count_max then () ``` wenzelm@27020 ` 511` ``` else ``` wenzelm@27020 ` 512` ``` (tracing (cat_lines ``` wenzelm@27020 ` 513` ``` (["Assumptions:"] @ map Display.string_of_thm asms @ [""] @ ``` wenzelm@27020 ` 514` ``` ["Proved:", Display.string_of_thm fls, ""] @ ``` wenzelm@27020 ` 515` ``` (if count <> warning_count_max then [] ``` wenzelm@27020 ` 516` ``` else ["\n(Reached maximal message count -- disabling future warnings)"]))); ``` wenzelm@27020 ` 517` ``` warning "Linear arithmetic should have refuted the assumptions.\n\ ``` wenzelm@27020 ` 518` ``` \Please inform Tobias Nipkow (nipkow@in.tum.de).") ``` wenzelm@27020 ` 519` ``` end; ``` wenzelm@27020 ` 520` ``` in fls end ``` wenzelm@27020 ` 521` ``` handle FalseE thm => trace_thm "False reached early:" thm ``` wenzelm@27020 ` 522` ``` end; ``` wenzelm@27020 ` 523` nipkow@6056 ` 524` ```end; ``` nipkow@5982 ` 525` haftmann@23261 ` 526` ```fun coeff poly atom = ``` berghofe@26835 ` 527` ``` AList.lookup Pattern.aeconv poly atom |> the_default 0; ``` nipkow@10691 ` 528` nipkow@10691 ` 529` ```fun integ(rlhs,r,rel,rrhs,s,d) = ``` haftmann@17951 ` 530` ```let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s ``` wenzelm@24630 ` 531` ``` val m = Integer.lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs)) ``` wenzelm@22846 ` 532` ``` fun mult(t,r) = ``` haftmann@17951 ` 533` ``` let val (i,j) = Rat.quotient_of_rat r ``` paulson@15965 ` 534` ``` in (t,i * (m div j)) end ``` nipkow@12932 ` 535` ```in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end ``` nipkow@10691 ` 536` nipkow@13498 ` 537` ```fun mklineq n atoms = ``` webertj@20217 ` 538` ``` fn (item, k) => ``` webertj@20217 ` 539` ``` let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item ``` nipkow@13498 ` 540` ``` val lhsa = map (coeff lhs) atoms ``` nipkow@13498 ` 541` ``` and rhsa = map (coeff rhs) atoms ``` haftmann@18330 ` 542` ``` val diff = map2 (curry (op -)) rhsa lhsa ``` nipkow@13498 ` 543` ``` val c = i-j ``` nipkow@13498 ` 544` ``` val just = Asm k ``` nipkow@13498 ` 545` ``` fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j)) ``` nipkow@13498 ` 546` ``` in case rel of ``` nipkow@13498 ` 547` ``` "<=" => lineq(c,Le,diff,just) ``` nipkow@13498 ` 548` ``` | "~<=" => if discrete ``` nipkow@13498 ` 549` ``` then lineq(1-c,Le,map (op ~) diff,NotLeDD(just)) ``` nipkow@13498 ` 550` ``` else lineq(~c,Lt,map (op ~) diff,NotLeD(just)) ``` nipkow@13498 ` 551` ``` | "<" => if discrete ``` nipkow@13498 ` 552` ``` then lineq(c+1,Le,diff,LessD(just)) ``` nipkow@13498 ` 553` ``` else lineq(c,Lt,diff,just) ``` nipkow@13498 ` 554` ``` | "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just)) ``` nipkow@13498 ` 555` ``` | "=" => lineq(c,Eq,diff,just) ``` wenzelm@22846 ` 556` ``` | _ => sys_error("mklineq" ^ rel) ``` nipkow@5982 ` 557` ``` end; ``` nipkow@5982 ` 558` nipkow@13498 ` 559` ```(* ------------------------------------------------------------------------- *) ``` nipkow@13498 ` 560` ```(* Print (counter) example *) ``` nipkow@13498 ` 561` ```(* ------------------------------------------------------------------------- *) ``` nipkow@13498 ` 562` nipkow@13498 ` 563` ```fun print_atom((a,d),r) = ``` haftmann@17951 ` 564` ``` let val (p,q) = Rat.quotient_of_rat r ``` wenzelm@24630 ` 565` ``` val s = if d then string_of_int p else ``` nipkow@13498 ` 566` ``` if p = 0 then "0" ``` wenzelm@24630 ` 567` ``` else string_of_int p ^ "/" ^ string_of_int q ``` nipkow@13498 ` 568` ``` in a ^ " = " ^ s end; ``` nipkow@13498 ` 569` wenzelm@19049 ` 570` ```fun produce_ex sds = ``` haftmann@17496 ` 571` ``` curry (op ~~) sds ``` haftmann@17496 ` 572` ``` #> map print_atom ``` haftmann@17496 ` 573` ``` #> commas ``` webertj@23197 ` 574` ``` #> curry (op ^) "Counterexample (possibly spurious):\n"; ``` nipkow@13498 ` 575` wenzelm@24076 ` 576` ```fun trace_ex ctxt params atoms discr n (hist: history) = ``` webertj@20217 ` 577` ``` case hist of ``` webertj@20217 ` 578` ``` [] => () ``` webertj@20217 ` 579` ``` | (v, lineqs) :: hist' => ``` wenzelm@24076 ` 580` ``` let ``` wenzelm@24076 ` 581` ``` val frees = map Free params ``` wenzelm@24920 ` 582` ``` fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t)) ``` wenzelm@24076 ` 583` ``` val start = ``` wenzelm@24076 ` 584` ``` if v = ~1 then (hist', findex0 discr n lineqs) ``` haftmann@22950 ` 585` ``` else (hist, replicate n Rat.zero) ``` wenzelm@24076 ` 586` ``` val ex = SOME (produce_ex (map show_term atoms ~~ discr) ``` wenzelm@24076 ` 587` ``` (uncurry (fold (findex1 discr)) start)) ``` webertj@20217 ` 588` ``` handle NoEx => NONE ``` wenzelm@24076 ` 589` ``` in ``` wenzelm@24076 ` 590` ``` case ex of ``` haftmann@30687 ` 591` ``` SOME s => (warning "Linear arithmetic failed - see trace for a counterexample."; tracing s) ``` haftmann@30687 ` 592` ``` | NONE => warning "Linear arithmetic failed" ``` wenzelm@24076 ` 593` ``` end; ``` nipkow@13498 ` 594` webertj@20217 ` 595` ```(* ------------------------------------------------------------------------- *) ``` webertj@20217 ` 596` webertj@20268 ` 597` ```fun mknat (pTs : typ list) (ixs : int list) (atom : term, i : int) : lineq option = ``` webertj@20217 ` 598` ``` if LA_Logic.is_nat (pTs, atom) ``` nipkow@6056 ` 599` ``` then let val l = map (fn j => if j=i then 1 else 0) ixs ``` webertj@20217 ` 600` ``` in SOME (Lineq (0, Le, l, Nat i)) end ``` webertj@20217 ` 601` ``` else NONE; ``` nipkow@6056 ` 602` nipkow@13186 ` 603` ```(* This code is tricky. It takes a list of premises in the order they occur ``` skalberg@15531 ` 604` ```in the subgoal. Numerical premises are coded as SOME(tuple), non-numerical ``` skalberg@15531 ` 605` ```ones as NONE. Going through the premises, each numeric one is converted into ``` nipkow@13186 ` 606` ```a Lineq. The tricky bit is to convert ~= which is split into two cases < and ``` nipkow@13498 ` 607` ```>. Thus split_items returns a list of equation systems. This may blow up if ``` nipkow@13186 ` 608` ```there are many ~=, but in practice it does not seem to happen. The really ``` nipkow@13186 ` 609` ```tricky bit is to arrange the order of the cases such that they coincide with ``` nipkow@13186 ` 610` ```the order in which the cases are in the end generated by the tactic that ``` nipkow@13186 ` 611` ```applies the generated refutation thms (see function 'refute_tac'). ``` nipkow@13186 ` 612` nipkow@13186 ` 613` ```For variables n of type nat, a constraint 0 <= n is added. ``` nipkow@13186 ` 614` ```*) ``` webertj@20217 ` 615` webertj@20217 ` 616` ```(* FIXME: To optimize, the splitting of cases and the search for refutations *) ``` webertj@20276 ` 617` ```(* could be intertwined: separate the first (fully split) case, *) ``` webertj@20217 ` 618` ```(* refute it, continue with splitting and refuting. Terminate with *) ``` webertj@20217 ` 619` ```(* failure as soon as a case could not be refuted; i.e. delay further *) ``` webertj@20217 ` 620` ```(* splitting until after a refutation for other cases has been found. *) ``` webertj@20217 ` 621` webertj@30406 ` 622` ```fun split_items ctxt do_pre split_neq (Ts, terms) : (typ list * (LA_Data.decomp * int) list) list = ``` webertj@20276 ` 623` ```let ``` webertj@20276 ` 624` ``` (* splits inequalities '~=' into '<' and '>'; this corresponds to *) ``` webertj@20276 ` 625` ``` (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *) ``` webertj@20276 ` 626` ``` (* level *) ``` webertj@20276 ` 627` ``` (* FIXME: this is currently sensitive to the order of theorems in *) ``` webertj@20276 ` 628` ``` (* neqE: The theorem for type "nat" must come first. A *) ``` webertj@20276 ` 629` ``` (* better (i.e. less likely to break when neqE changes) *) ``` webertj@20276 ` 630` ``` (* implementation should *test* which theorem from neqE *) ``` webertj@20276 ` 631` ``` (* can be applied, and split the premise accordingly. *) ``` wenzelm@26945 ` 632` ``` fun elim_neq (ineqs : (LA_Data.decomp option * bool) list) : ``` wenzelm@26945 ` 633` ``` (LA_Data.decomp option * bool) list list = ``` webertj@20276 ` 634` ``` let ``` wenzelm@26945 ` 635` ``` fun elim_neq' nat_only ([] : (LA_Data.decomp option * bool) list) : ``` wenzelm@26945 ` 636` ``` (LA_Data.decomp option * bool) list list = ``` webertj@20276 ` 637` ``` [[]] ``` webertj@20276 ` 638` ``` | elim_neq' nat_only ((NONE, is_nat) :: ineqs) = ``` webertj@20276 ` 639` ``` map (cons (NONE, is_nat)) (elim_neq' nat_only ineqs) ``` webertj@20276 ` 640` ``` | elim_neq' nat_only ((ineq as (SOME (l, i, rel, r, j, d), is_nat)) :: ineqs) = ``` webertj@20276 ` 641` ``` if rel = "~=" andalso (not nat_only orelse is_nat) then ``` webertj@20276 ` 642` ``` (* [| ?l ~= ?r; ?l < ?r ==> ?R; ?r < ?l ==> ?R |] ==> ?R *) ``` webertj@20276 ` 643` ``` elim_neq' nat_only (ineqs @ [(SOME (l, i, "<", r, j, d), is_nat)]) @ ``` webertj@20276 ` 644` ``` elim_neq' nat_only (ineqs @ [(SOME (r, j, "<", l, i, d), is_nat)]) ``` webertj@20276 ` 645` ``` else ``` webertj@20276 ` 646` ``` map (cons ineq) (elim_neq' nat_only ineqs) ``` webertj@20276 ` 647` ``` in ``` webertj@20276 ` 648` ``` ineqs |> elim_neq' true ``` wenzelm@26945 ` 649` ``` |> maps (elim_neq' false) ``` webertj@20276 ` 650` ``` end ``` nipkow@13464 ` 651` webertj@30406 ` 652` ``` fun ignore_neq (NONE, bool) = (NONE, bool) ``` webertj@30406 ` 653` ``` | ignore_neq (ineq as SOME (_, _, rel, _, _, _), bool) = ``` webertj@30406 ` 654` ``` if rel = "~=" then (NONE, bool) else (ineq, bool) ``` webertj@30406 ` 655` webertj@20276 ` 656` ``` fun number_hyps _ [] = [] ``` webertj@20276 ` 657` ``` | number_hyps n (NONE::xs) = number_hyps (n+1) xs ``` webertj@20276 ` 658` ``` | number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs ``` webertj@20276 ` 659` webertj@20276 ` 660` ``` val result = (Ts, terms) ``` webertj@20276 ` 661` ``` |> (* user-defined preprocessing of the subgoal *) ``` wenzelm@24076 ` 662` ``` (if do_pre then LA_Data.pre_decomp ctxt else Library.single) ``` webertj@23195 ` 663` ``` |> tap (fn subgoals => trace_msg ("Preprocessing yields " ^ ``` webertj@23195 ` 664` ``` string_of_int (length subgoals) ^ " subgoal(s) total.")) ``` wenzelm@22846 ` 665` ``` |> (* produce the internal encoding of (in-)equalities *) ``` wenzelm@24076 ` 666` ``` map (apsnd (map (fn t => (LA_Data.decomp ctxt t, LA_Data.domain_is_nat t)))) ``` webertj@20276 ` 667` ``` |> (* splitting of inequalities *) ``` webertj@30406 ` 668` ``` map (apsnd (if split_neq then elim_neq else ``` webertj@30406 ` 669` ``` Library.single o map ignore_neq)) ``` wenzelm@22846 ` 670` ``` |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals) ``` webertj@20276 ` 671` ``` |> (* numbering of hypotheses, ignoring irrelevant ones *) ``` webertj@20276 ` 672` ``` map (apsnd (number_hyps 0)) ``` webertj@23195 ` 673` ```in ``` webertj@23195 ` 674` ``` trace_msg ("Splitting of inequalities yields " ^ ``` webertj@23195 ` 675` ``` string_of_int (length result) ^ " subgoal(s) total."); ``` webertj@23195 ` 676` ``` result ``` webertj@23195 ` 677` ```end; ``` nipkow@13464 ` 678` wenzelm@26945 ` 679` ```fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decomp, _)) : term list = ``` berghofe@26835 ` 680` ``` union_term (map fst lhs) (union_term (map fst rhs) ats); ``` webertj@20217 ` 681` wenzelm@26945 ` 682` ```fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _)) : ``` webertj@20268 ` 683` ``` (bool * term) list = ``` berghofe@26835 ` 684` ``` union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats); ``` nipkow@13498 ` 685` wenzelm@26945 ` 686` ```fun discr (initems : (LA_Data.decomp * int) list) : bool list = ``` webertj@20268 ` 687` ``` map fst (Library.foldl add_datoms ([],initems)); ``` webertj@20217 ` 688` wenzelm@24076 ` 689` ```fun refutes ctxt params show_ex : ``` wenzelm@26945 ` 690` ``` (typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option = ``` wenzelm@26945 ` 691` ``` let ``` wenzelm@26945 ` 692` ``` fun refute ((Ts, initems : (LA_Data.decomp * int) list) :: initemss) (js: injust list) = ``` wenzelm@26945 ` 693` ``` let ``` wenzelm@26945 ` 694` ``` val atoms = Library.foldl add_atoms ([], initems) ``` wenzelm@26945 ` 695` ``` val n = length atoms ``` wenzelm@26945 ` 696` ``` val mkleq = mklineq n atoms ``` wenzelm@26945 ` 697` ``` val ixs = 0 upto (n - 1) ``` wenzelm@26945 ` 698` ``` val iatoms = atoms ~~ ixs ``` wenzelm@26945 ` 699` ``` val natlineqs = List.mapPartial (mknat Ts ixs) iatoms ``` wenzelm@26945 ` 700` ``` val ineqs = map mkleq initems @ natlineqs ``` wenzelm@26945 ` 701` ``` in case elim (ineqs, []) of ``` wenzelm@26945 ` 702` ``` Success j => ``` wenzelm@26945 ` 703` ``` (trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); ``` wenzelm@26945 ` 704` ``` refute initemss (js @ [j])) ``` wenzelm@26945 ` 705` ``` | Failure hist => ``` wenzelm@26945 ` 706` ``` (if not show_ex then () ``` wenzelm@26945 ` 707` ``` else ``` wenzelm@26945 ` 708` ``` let ``` wenzelm@26945 ` 709` ``` val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params) ``` wenzelm@26945 ` 710` ``` val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes ``` wenzelm@26945 ` 711` ``` (Name.invents (Variable.names_of ctxt') Name.uu (length Ts - length params)) ``` wenzelm@26945 ` 712` ``` val params' = (more_names @ param_names) ~~ Ts ``` wenzelm@26945 ` 713` ``` in ``` wenzelm@26945 ` 714` ``` trace_ex ctxt'' params' atoms (discr initems) n hist ``` wenzelm@26945 ` 715` ``` end; NONE) ``` wenzelm@26945 ` 716` ``` end ``` wenzelm@26945 ` 717` ``` | refute [] js = SOME js ``` wenzelm@26945 ` 718` ``` in refute end; ``` nipkow@5982 ` 719` webertj@30406 ` 720` ```fun refute ctxt params show_ex do_pre split_neq terms : injust list option = ``` webertj@30406 ` 721` ``` refutes ctxt params show_ex (split_items ctxt do_pre split_neq ``` webertj@30406 ` 722` ``` (map snd params, terms)) []; ``` webertj@20254 ` 723` haftmann@22950 ` 724` ```fun count P xs = length (filter P xs); ``` webertj@20254 ` 725` webertj@30406 ` 726` ```fun prove ctxt params show_ex do_pre Hs concl : bool * injust list option = ``` webertj@20254 ` 727` ``` let ``` webertj@23190 ` 728` ``` val _ = trace_msg "prove:" ``` webertj@20254 ` 729` ``` (* append the negated conclusion to 'Hs' -- this corresponds to *) ``` webertj@20254 ` 730` ``` (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *) ``` webertj@20254 ` 731` ``` (* theorem/tactic level *) ``` webertj@20254 ` 732` ``` val Hs' = Hs @ [LA_Logic.neg_prop concl] ``` webertj@20254 ` 733` ``` fun is_neq NONE = false ``` webertj@20254 ` 734` ``` | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") ``` webertj@30406 ` 735` ``` val neq_limit = Config.get ctxt LA_Data.fast_arith_neq_limit ``` webertj@30406 ` 736` ``` val split_neq = count is_neq (map (LA_Data.decomp ctxt) Hs') <= neq_limit ``` webertj@20254 ` 737` ``` in ``` webertj@30406 ` 738` ``` if split_neq then () ``` wenzelm@24076 ` 739` ``` else ``` webertj@30406 ` 740` ``` trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ ``` webertj@30406 ` 741` ``` string_of_int neq_limit ^ "), ignoring all inequalities"); ``` webertj@30406 ` 742` ``` (split_neq, refute ctxt params show_ex do_pre split_neq Hs') ``` webertj@23190 ` 743` ``` end handle TERM ("neg_prop", _) => ``` webertj@23190 ` 744` ``` (* since no meta-logic negation is available, we can only fail if *) ``` webertj@23190 ` 745` ``` (* the conclusion is not of the form 'Trueprop \$ _' (simply *) ``` webertj@23190 ` 746` ``` (* dropping the conclusion doesn't work either, because even *) ``` webertj@23190 ` 747` ``` (* 'False' does not imply arbitrary 'concl::prop') *) ``` webertj@30406 ` 748` ``` (trace_msg "prove failed (cannot negate conclusion)."; ``` webertj@30406 ` 749` ``` (false, NONE)); ``` webertj@20217 ` 750` webertj@30406 ` 751` ```fun refute_tac ss (i, split_neq, justs) = ``` nipkow@6074 ` 752` ``` fn state => ``` wenzelm@24076 ` 753` ``` let ``` wenzelm@24076 ` 754` ``` val ctxt = Simplifier.the_context ss; ``` wenzelm@24076 ` 755` ``` val _ = trace_thm ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^ ``` wenzelm@24076 ` 756` ``` string_of_int (length justs) ^ " justification(s)):") state ``` wenzelm@24076 ` 757` ``` val {neqE, ...} = get_data ctxt; ``` wenzelm@24076 ` 758` ``` fun just1 j = ``` wenzelm@24076 ` 759` ``` (* eliminate inequalities *) ``` webertj@30406 ` 760` ``` (if split_neq then ``` webertj@30406 ` 761` ``` REPEAT_DETERM (eresolve_tac neqE i) ``` webertj@30406 ` 762` ``` else ``` webertj@30406 ` 763` ``` all_tac) THEN ``` wenzelm@24076 ` 764` ``` PRIMITIVE (trace_thm "State after neqE:") THEN ``` wenzelm@24076 ` 765` ``` (* use theorems generated from the actual justifications *) ``` wenzelm@24076 ` 766` ``` METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i ``` wenzelm@24076 ` 767` ``` in ``` wenzelm@24076 ` 768` ``` (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *) ``` wenzelm@24076 ` 769` ``` DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN ``` wenzelm@24076 ` 770` ``` (* user-defined preprocessing of the subgoal *) ``` wenzelm@24076 ` 771` ``` DETERM (LA_Data.pre_tac ctxt i) THEN ``` wenzelm@24076 ` 772` ``` PRIMITIVE (trace_thm "State after pre_tac:") THEN ``` wenzelm@24076 ` 773` ``` (* prove every resulting subgoal, using its justification *) ``` wenzelm@24076 ` 774` ``` EVERY (map just1 justs) ``` webertj@20217 ` 775` ``` end state; ``` nipkow@6074 ` 776` nipkow@5982 ` 777` ```(* ``` nipkow@5982 ` 778` ```Fast but very incomplete decider. Only premises and conclusions ``` nipkow@5982 ` 779` ```that are already (negated) (in)equations are taken into account. ``` nipkow@5982 ` 780` ```*) ``` wenzelm@24076 ` 781` ```fun simpset_lin_arith_tac ss show_ex = SUBGOAL (fn (A, i) => ``` wenzelm@24076 ` 782` ``` let ``` wenzelm@24076 ` 783` ``` val ctxt = Simplifier.the_context ss ``` wenzelm@24076 ` 784` ``` val params = rev (Logic.strip_params A) ``` wenzelm@24076 ` 785` ``` val Hs = Logic.strip_assums_hyp A ``` wenzelm@24076 ` 786` ``` val concl = Logic.strip_assums_concl A ``` wenzelm@24076 ` 787` ``` val _ = trace_term ctxt ("Trying to refute subgoal " ^ string_of_int i) A ``` wenzelm@24076 ` 788` ``` in ``` wenzelm@24076 ` 789` ``` case prove ctxt params show_ex true Hs concl of ``` webertj@30406 ` 790` ``` (_, NONE) => (trace_msg "Refutation failed."; no_tac) ``` webertj@30406 ` 791` ``` | (split_neq, SOME js) => (trace_msg "Refutation succeeded."; ``` webertj@30406 ` 792` ``` refute_tac ss (i, split_neq, js)) ``` wenzelm@24076 ` 793` ``` end); ``` nipkow@5982 ` 794` wenzelm@24076 ` 795` ```fun cut_lin_arith_tac ss = ``` wenzelm@24076 ` 796` ``` cut_facts_tac (Simplifier.prems_of_ss ss) THEN' ``` wenzelm@24076 ` 797` ``` simpset_lin_arith_tac ss false; ``` wenzelm@17613 ` 798` wenzelm@24076 ` 799` ```fun lin_arith_tac ctxt = ``` wenzelm@24076 ` 800` ``` simpset_lin_arith_tac (Simplifier.context ctxt Simplifier.empty_ss); ``` wenzelm@24076 ` 801` wenzelm@24076 ` 802` nipkow@5982 ` 803` nipkow@13186 ` 804` ```(** Forward proof from theorems **) ``` nipkow@13186 ` 805` webertj@20433 ` 806` ```(* More tricky code. Needs to arrange the proofs of the multiple cases (due ``` webertj@20433 ` 807` ```to splits of ~= premises) such that it coincides with the order of the cases ``` webertj@20433 ` 808` ```generated by function split_items. *) ``` webertj@20433 ` 809` webertj@20433 ` 810` ```datatype splittree = Tip of thm list ``` webertj@20433 ` 811` ``` | Spl of thm * cterm * splittree * cterm * splittree; ``` webertj@20433 ` 812` webertj@20433 ` 813` ```(* "(ct1 ==> ?R) ==> (ct2 ==> ?R) ==> ?R" is taken to (ct1, ct2) *) ``` webertj@20433 ` 814` webertj@20433 ` 815` ```fun extract (imp : cterm) : cterm * cterm = ``` webertj@20433 ` 816` ```let val (Il, r) = Thm.dest_comb imp ``` webertj@20433 ` 817` ``` val (_, imp1) = Thm.dest_comb Il ``` webertj@20433 ` 818` ``` val (Ict1, _) = Thm.dest_comb imp1 ``` webertj@20433 ` 819` ``` val (_, ct1) = Thm.dest_comb Ict1 ``` webertj@20433 ` 820` ``` val (Ir, _) = Thm.dest_comb r ``` webertj@20433 ` 821` ``` val (_, Ict2r) = Thm.dest_comb Ir ``` webertj@20433 ` 822` ``` val (Ict2, _) = Thm.dest_comb Ict2r ``` webertj@20433 ` 823` ``` val (_, ct2) = Thm.dest_comb Ict2 ``` webertj@20433 ` 824` ```in (ct1, ct2) end; ``` webertj@20433 ` 825` wenzelm@24076 ` 826` ```fun splitasms ctxt (asms : thm list) : splittree = ``` wenzelm@24076 ` 827` ```let val {neqE, ...} = get_data ctxt ``` webertj@20433 ` 828` ``` fun elim_neq (asms', []) = Tip (rev asms') ``` webertj@20433 ` 829` ``` | elim_neq (asms', asm::asms) = ``` webertj@20433 ` 830` ``` (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of ``` webertj@20433 ` 831` ``` SOME spl => ``` webertj@20433 ` 832` ``` let val (ct1, ct2) = extract (cprop_of spl) ``` webertj@20433 ` 833` ``` val thm1 = assume ct1 ``` webertj@20433 ` 834` ``` val thm2 = assume ct2 ``` webertj@20433 ` 835` ``` in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2])) ``` webertj@20433 ` 836` ``` end ``` webertj@20433 ` 837` ``` | NONE => elim_neq (asm::asms', asms)) ``` webertj@20433 ` 838` ```in elim_neq ([], asms) end; ``` webertj@20433 ` 839` wenzelm@24076 ` 840` ```fun fwdproof ss (Tip asms : splittree) (j::js : injust list) = (mkthm ss asms j, js) ``` wenzelm@24076 ` 841` ``` | fwdproof ss (Spl (thm, ct1, tree1, ct2, tree2)) js = ``` wenzelm@24076 ` 842` ``` let ``` wenzelm@24076 ` 843` ``` val (thm1, js1) = fwdproof ss tree1 js ``` wenzelm@24076 ` 844` ``` val (thm2, js2) = fwdproof ss tree2 js1 ``` webertj@20433 ` 845` ``` val thm1' = implies_intr ct1 thm1 ``` webertj@20433 ` 846` ``` val thm2' = implies_intr ct2 thm2 ``` wenzelm@24076 ` 847` ``` in (thm2' COMP (thm1' COMP thm), js2) end; ``` wenzelm@24076 ` 848` ``` (* FIXME needs handle THM _ => NONE ? *) ``` webertj@20433 ` 849` webertj@30406 ` 850` ```fun prover ss thms Tconcl (js : injust list) split_neq pos : thm option = ``` wenzelm@24076 ` 851` ``` let ``` wenzelm@24076 ` 852` ``` val ctxt = Simplifier.the_context ss ``` wenzelm@24076 ` 853` ``` val thy = ProofContext.theory_of ctxt ``` wenzelm@24076 ` 854` ``` val nTconcl = LA_Logic.neg_prop Tconcl ``` wenzelm@24076 ` 855` ``` val cnTconcl = cterm_of thy nTconcl ``` wenzelm@24076 ` 856` ``` val nTconclthm = assume cnTconcl ``` webertj@30406 ` 857` ``` val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm]) ``` wenzelm@24076 ` 858` ``` val (Falsethm, _) = fwdproof ss tree js ``` wenzelm@24076 ` 859` ``` val contr = if pos then LA_Logic.ccontr else LA_Logic.notI ``` wenzelm@24076 ` 860` ``` val concl = implies_intr cnTconcl Falsethm COMP contr ``` wenzelm@24076 ` 861` ``` in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end ``` wenzelm@24076 ` 862` ``` (*in case concl contains ?-var, which makes assume fail:*) (* FIXME Variable.import_terms *) ``` wenzelm@24076 ` 863` ``` handle THM _ => NONE; ``` nipkow@13186 ` 864` nipkow@13186 ` 865` ```(* PRE: concl is not negated! ``` nipkow@13186 ` 866` ``` This assumption is OK because ``` wenzelm@24076 ` 867` ``` 1. lin_arith_simproc tries both to prove and disprove concl and ``` wenzelm@24076 ` 868` ``` 2. lin_arith_simproc is applied by the Simplifier which ``` nipkow@13186 ` 869` ``` dives into terms and will thus try the non-negated concl anyway. ``` nipkow@13186 ` 870` ```*) ``` wenzelm@24076 ` 871` ```fun lin_arith_simproc ss concl = ``` wenzelm@24076 ` 872` ``` let ``` wenzelm@24076 ` 873` ``` val ctxt = Simplifier.the_context ss ``` wenzelm@26945 ` 874` ``` val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss) ``` wenzelm@24076 ` 875` ``` val Hs = map Thm.prop_of thms ``` nipkow@6102 ` 876` ``` val Tconcl = LA_Logic.mk_Trueprop concl ``` wenzelm@24076 ` 877` ``` in ``` wenzelm@24076 ` 878` ``` case prove ctxt [] false false Hs Tconcl of (* concl provable? *) ``` webertj@30406 ` 879` ``` (split_neq, SOME js) => prover ss thms Tconcl js split_neq true ``` webertj@30406 ` 880` ``` | (_, NONE) => ``` wenzelm@24076 ` 881` ``` let val nTconcl = LA_Logic.neg_prop Tconcl in ``` wenzelm@24076 ` 882` ``` case prove ctxt [] false false Hs nTconcl of (* ~concl provable? *) ``` webertj@30406 ` 883` ``` (split_neq, SOME js) => prover ss thms nTconcl js split_neq false ``` webertj@30406 ` 884` ``` | (_, NONE) => NONE ``` wenzelm@24076 ` 885` ``` end ``` wenzelm@24076 ` 886` ``` end; ``` nipkow@6074 ` 887` nipkow@6074 ` 888` ```end; ```