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