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