1(*****************************************************************************) 2(* FILE : solve.sml *) 3(* DESCRIPTION : Functions for solving arithmetic formulae. *) 4(* *) 5(* READS FILES : <none> *) 6(* WRITES FILES : <none> *) 7(* *) 8(* AUTHOR : R.J.Boulton, University of Cambridge *) 9(* DATE : 19th April 1991 *) 10(* *) 11(* TRANSLATOR : R.J.Boulton, University of Cambridge *) 12(* DATE : 15th February 1993 *) 13(* *) 14(* LAST MODIFIED : R.J.Boulton *) 15(* DATE : 16th November 1995 *) 16(*****************************************************************************) 17 18structure Solve :> Solve = 19struct 20 open Arbint HolKernel boolLib; 21 open Arith_cons Term_coeffs RJBConv Theorems Thm_convs 22 Norm_arith Norm_ineqs Solve_ineqs; 23 24infix THENC; 25 26fun failwith function = raise (mk_HOL_ERR "Solve" function "") 27 28 29(*---------------------------------------------------------------------------*) 30(* INEQS_FALSE_CONV : conv *) 31(* *) 32(* Proves a conjunction of normalized inequalities is false, provided they *) 33(* are unsatisfiable. Checks for any inequalities that can immediately be *) 34(* shown to be false before calling VAR_ELIM. *) 35(* *) 36(* Example: *) 37(* *) 38(* INEQS_FALSE_CONV *) 39(* `((2 + (2 * n)) <= (1 * m)) /\ *) 40(* ((1 * m) <= (1 * n)) /\ *) 41(* (0 <= (1 * n)) /\ *) 42(* (0 <= (1 * m))` *) 43(* ---> *) 44(* |- (2 + (2 * n)) <= (1 * m) /\ *) 45(* (1 * m) <= (1 * n) /\ *) 46(* 0 <= (1 * n) /\ *) 47(* 0 <= (1 * m) = *) 48(* F *) 49(*---------------------------------------------------------------------------*) 50 51fun INEQS_FALSE_CONV tm = 52 let val ineqs = strip_conj tm 53 val rev_ineqs = rev ineqs 54 val coeffsl = map coeffs_of_leq ineqs 55 val falses = 56 filter (fn (const,bind) => (null bind) andalso (const < zero)) coeffsl 57 val th = 58 if null falses 59 then let val var_names = Lib.mk_set(map fst(flatten(map snd coeffsl))) 60 val coeffsl' = 61 (map (fn v => (zero, [(v,one)])) var_names) @ coeffsl 62 val (_,f) = VAR_ELIM coeffsl' 63 val axioms = 64 map (fn v => SPEC (mk_num_var v) ZERO_LESS_EQ_ONE_TIMES) 65 var_names 66 in itlist PROVE_HYP axioms (f ()) 67 end 68 else ASSUME (build_leq (hd falses)) 69 val th' = CONV_RULE LEQ_CONV th 70 val th'' = DISCH (hd rev_ineqs) th' 71 fun conj_disch tm th = CONV_RULE IMP_IMP_CONJ_IMP_CONV (DISCH tm th) 72 val th''' = itlist conj_disch (rev (tl rev_ineqs)) th'' 73 in 74 CONV_RULE IMP_F_EQ_F_CONV th''' 75 end 76 handle HOL_ERR _ => failwith "INEQS_FALSE_CONV"; 77 78(*---------------------------------------------------------------------------*) 79(* DISJ_INEQS_FALSE_CONV : conv *) 80(* *) 81(* Proves a disjunction of conjunctions of normalized inequalities is false, *) 82(* provided each conjunction is unsatisfiable. *) 83(*---------------------------------------------------------------------------*) 84 85fun DISJ_INEQS_FALSE_CONV tm = 86 (if is_disj tm 87 then ((RATOR_CONV (RAND_CONV INEQS_FALSE_CONV)) THENC 88 OR_F_CONV THENC 89 DISJ_INEQS_FALSE_CONV) tm 90 else INEQS_FALSE_CONV tm 91 ) handle (HOL_ERR _) => failwith "DISJ_INEQS_FALSE_CONV"; 92 93(*---------------------------------------------------------------------------*) 94(* NOT_NOT_INTRO_CONV : conv *) 95(* *) 96(* `b` ---> |- b = ~~b provided b is of type ":bool". *) 97(*---------------------------------------------------------------------------*) 98 99fun NOT_NOT_INTRO_CONV tm = 100 (SYM ((NOT_NOT_NORM_CONV o mk_neg o mk_neg) tm) 101 ) handle (HOL_ERR _) => failwith "NOT_NOT_INTRO_CONV"; 102 103(*---------------------------------------------------------------------------*) 104(* Discriminator functions for T (true) and F (false) *) 105(*---------------------------------------------------------------------------*) 106 107val is_T = equal T 108and is_F = equal F 109 110(*---------------------------------------------------------------------------*) 111(* NEGATE_CONV : conv -> conv *) 112(* *) 113(* Function for negating the operation of a conversion that proves a formula *) 114(* to be either true or false. For example if `conv' proves `0 <= n` to be *) 115(* equal to `T` then `NEGATE_CONV conv' will prove `~(0 <= n)` to be `F`. *) 116(* The function fails if the application of `conv' to the negation of the *) 117(* formula does not yield either `T` or `F`. *) 118(* *) 119(* If use of this function succeeds then the input term will necessarily *) 120(* have been changed. Hence it does not need to be a CONV. It can however *) 121(* take a CONV as its argument. *) 122(*---------------------------------------------------------------------------*) 123 124val neg_tm = boolSyntax.negation 125 126fun NEGATE_CONV conv tm = 127 let val neg = is_neg tm 128 val th = RULE_OF_CONV conv (if neg then (dest_neg tm) else (mk_neg tm)) 129 val r = rhs (concl th) 130 val truth_th = 131 if is_T r then NOT_T_F else 132 if is_F r then NOT_F_T else failwith "NEGATE_CONV" 133 val neg_fn = if neg then I else TRANS (NOT_NOT_INTRO_CONV tm) 134 in neg_fn (TRANS (AP_TERM neg_tm th) truth_th) 135 end; 136 137(*---------------------------------------------------------------------------*) 138(* DEPTH_FORALL_CONV : conv -> conv *) 139(* *) 140(* DEPTH_FORALL_CONV conv `!x1 ... xn. body` applies conv to `body` and *) 141(* returns a theorem of the form: *) 142(* *) 143(* |- (!x1 ... xn. body) = (!x1 ... xn. body') *) 144(*---------------------------------------------------------------------------*) 145 146fun DEPTH_FORALL_CONV conv tm = 147 if is_forall tm 148 then RAND_CONV (ABS_CONV (DEPTH_FORALL_CONV conv)) tm 149 else conv tm; 150 151(*---------------------------------------------------------------------------*) 152(* FORALL_ARITH_CONV : conv *) 153(* *) 154(* Proof procedure for non-existential Presburger natural arithmetic *) 155(* (+, * by a constant, numeric constants, numeric variables, <, <=, =, >=, *) 156(* >, ~, /\, \/, ==>, = (iff), ! (when in prenex normal form). *) 157(* Expects formula in prenex normal form. *) 158(* Subtraction, PRE and conditionals must have been eliminated. *) 159(* SUC is allowed. *) 160(* Boolean variables and constants are not allowed. *) 161(* *) 162(* The procedure will prove most formulae in the subset of arithmetic *) 163(* specified above, but there is some incompleteness. However, this rarely *) 164(* manifests itself in practice. It is therefore likely that if the *) 165(* procedure cannot prove a formula in the subset, the formula is not valid. *) 166(*---------------------------------------------------------------------------*) 167 168fun FORALL_ARITH_CONV tm = 169 (reset_multiplication_theorems (); 170 RULE_OF_CONV 171 (DEPTH_FORALL_CONV 172 (NEGATE_CONV 173 ((fn tm => ARITH_FORM_NORM_CONV tm 174 handle HOL_ERR _ => 175 raise HOL_ERR{origin_structure = "Solve", 176 origin_function = "FORALL_ARITH_CONV", 177 message = "formula not in the allowed subset"} 178 ) THENC 179 (fn tm => DISJ_INEQS_FALSE_CONV tm 180 handle HOL_ERR _ => 181 raise HOL_ERR{origin_structure = "Solve", 182 origin_function = "FORALL_ARITH_CONV", 183 message = "cannot prove formula"} 184 ))) THENC 185 REPEATC FORALL_SIMP_CONV) 186 tm 187 ); 188 189end 190