1(* ---------------------------------------------------------------------- 2 FILE : gen_arith.sml 3 DESCRIPTION : Generalised arithmetic proof procedure. 4 5 AUTHOR : R.J.Boulton, University of Cambridge 6 DATE : 30th January 1992 7 ---------------------------------------------------------------------- *) 8 9structure Gen_arith :> Gen_arith = 10struct 11 12open Arbint HolKernel boolLib Rsyntax 13 Arith_cons Solve Exists_arith 14 Sub_and_cond Prenex Instance RJBConv; 15 16infix THENC; 17 18val REWRITE_CONV = Rewrite.REWRITE_CONV; 19 20fun failwith function = raise (mk_HOL_ERR "Gen_arith" function ""); 21 22val op << = String.<; 23 24 25(*---------------------------------------------------------------------------*) 26(* contains_var : term -> bool *) 27(* *) 28(* Returns true if an expression possibly involving SUC, +, *, numeric *) 29(* constants and variables does contain a variable. Also returns true if any *) 30(* subterm does not conform to this specification of expressions. *) 31(* *) 32(* The internal function uses failure to denote that the expression *) 33(* evaluates to zero. This is used because, when normalised, zero multiplied *) 34(* by an expression is zero and hence any variables in the expression can be *) 35(* ignored. *) 36(*---------------------------------------------------------------------------*) 37 38fun contains_var tm = 39 let fun contains_var' tm = 40 if (is_var tm) then true 41 else if (is_const tm orelse is_num_const tm) then 42 (if (is_zero tm) then failwith "fail" else not (is_num_const tm)) 43 else if (is_suc tm) then (contains_var' (rand tm) handle _ => false) 44 else if (is_plus tm) then 45 ((let val b = contains_var' (arg1 tm) 46 in b orelse (contains_var' (arg2 tm) handle _ => false) 47 end) 48 handle _ => contains_var' (arg2 tm) 49 ) 50 else if (is_mult tm) then 51 ((contains_var' (arg1 tm)) orelse (contains_var' (arg2 tm))) 52 else true 53 in contains_var' tm handle _ => false 54 end; 55 56(*---------------------------------------------------------------------------*) 57(* is_linear_mult : term -> bool *) 58(* *) 59(* Returns true if the term is a linear multiplication, i.e. at least one of *) 60(* the arguments is a constant expression. Fails if the term is not a *) 61(* multiplication. *) 62(*---------------------------------------------------------------------------*) 63 64fun is_linear_mult tm = 65 (let val (l,r) = dest_mult tm 66 in if (contains_var l) then (not (contains_var r)) else true 67 end 68 ) handle _ => failwith "is_linear_mult"; 69 70(*---------------------------------------------------------------------------*) 71(* non_presburger_subterms : term -> term list *) 72(* *) 73(* Computes the subterms of a term that are not in the Presburger subset of *) 74(* arithmetic. All variables are included. *) 75(* *) 76(* The function detects multiplications in which both of the arguments are *) 77(* non-constant expressions and returns the multiplication in the list of *) 78(* non-presburger terms. This allows a formula such as: *) 79(* *) 80(* m < (n * p) /\ (n * p) < q ==> m < q *) 81(* *) 82(* to be proved by the arithmetic procedure. *) 83(*---------------------------------------------------------------------------*) 84 85fun non_presburger_subterms tm = 86 (non_presburger_subterms (#Body (dest_forall tm))) handle _ => 87 (non_presburger_subterms (#Body (dest_exists tm))) handle _ => 88 (non_presburger_subterms (dest_neg tm)) handle _ => 89 (non_presburger_subterms (dest_suc tm)) handle _ => 90 (non_presburger_subterms (dest_pre tm)) handle _ => 91 (if (is_conj tm) orelse (is_disj tm) orelse (is_imp tm) orelse 92 (is_eq tm) orelse 93 (is_less tm) orelse (is_leq tm) orelse 94 (is_great tm) orelse (is_geq tm) orelse 95 (is_plus tm) orelse (is_minus tm) orelse 96 (is_linear_mult tm handle _ => false) 97 then Lib.union (non_presburger_subterms (arg1 tm)) 98 (non_presburger_subterms (arg2 tm)) 99 else if (is_num_const tm) then [] 100 else [tm]); 101 102(*---------------------------------------------------------------------------*) 103(* is_presburger : term -> bool *) 104(* *) 105(* Returns true if the term is a formula in the Presburger subset of natural *) 106(* number arithmetic. *) 107(*---------------------------------------------------------------------------*) 108 109val num_ty = Arith_cons.num_ty 110fun is_num_var tm = is_var tm andalso type_of tm = num_ty 111val is_presburger = (all is_num_var) o non_presburger_subterms; 112 113 114(* ---------------------------------------------------------------------- 115 EXPAND_NORM_MULTS_CONV : term -> thm 116 117 expands multiplications over additions (e.g., x * (y + z) becomes 118 x * y + x * z), and then normalises multiplications so that 119 non-numeral multiplicands always appear in the same order, and 120 grouped together, possibly with an isolated numeral coefficient. 121 ---------------------------------------------------------------------- *) 122 123fun EXPAND_NORM_MULTS_CONV tm = let 124 open arithmeticTheory numSyntax Psyntax 125 fun norm_mult t = let 126 val ms = strip_mult t 127 val _ = Int.>(length ms, 1) orelse failwith "not a mult" 128 val (nums, others) = partition is_numeral ms 129 val sorted_others = Listsort.sort Term.compare others 130 val AC = EQT_ELIM o AC_CONV(MULT_ASSOC, MULT_COMM) 131 in 132 if null others then reduceLib.REDUCE_CONV 133 else if null nums then 134 K (AC (mk_eq(t, list_mk_mult sorted_others))) 135 else 136 K (AC (mk_eq(t, mk_mult(list_mk_mult nums, 137 list_mk_mult sorted_others)))) THENC 138 LAND_CONV reduceLib.REDUCE_CONV 139 end t 140in 141 PURE_REWRITE_CONV [LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB] THENC 142 ONCE_DEPTH_CONV norm_mult 143end tm 144 145 146(*---------------------------------------------------------------------------*) 147(* ARITH_CONV : conv *) 148(* *) 149(* Proof procedure for purely universal and purely existential Presburger *) 150(* natural arithmetic (only one kind of quantifier allowed when in prenex *) 151(* normal form, i.e., only `forall' or only `exists', not a mixture). *) 152(* *) 153(* The subset consists of +, * by a constant, numeric constants, numeric *) 154(* variables, <, <=, =, >=, >, ~, /\, \/, ==>, = (iff). *) 155(* Subtraction and conditionals are allowed. *) 156(* SUC and PRE are allowed. *) 157(* Boolean variables are not allowed. *) 158(* Existential formulae must have all variables quantified because any free *) 159(* variables will be taken as universally quantified which violates the *) 160(* constraint that mixed quantifiers are not allowed. *) 161(* Substitution instances of universal formulae are also allowed. *) 162(* *) 163(* The procedure will prove many formulae in the subset of arithmetic *) 164(* specified above, but there is some incompleteness. *) 165(*---------------------------------------------------------------------------*) 166 167 168val ARITH_CONV = 169 let val BOOL_SIMP_CONV = REWRITE_CONV [] 170 fun GEN_ARITH_CONV tm = 171 (if is_exists tm 172 then EXISTS_ARITH_CONV tm 173 else (EXPAND_NORM_MULTS_CONV THENC 174 INSTANCE_T_CONV non_presburger_subterms FORALL_ARITH_CONV) tm) 175 handle e => raise (wrap_exn "Gen_arith" "ARITH_CONV" e) 176 in 177 SUB_AND_COND_ELIM_CONV THENC BOOL_SIMP_CONV THENC 178 (fn tm => if (is_T tm) orelse (is_F tm) then ALL_CONV tm 179 else (PRENEX_CONV THENC GEN_ARITH_CONV) tm) 180 end; 181 182end 183