1 (* Generated from Cooper.thy; DO NOT EDIT! *) |
|
2 |
|
3 structure Generated_Cooper : sig |
|
4 type 'a eq |
|
5 val eq : 'a eq -> 'a -> 'a -> bool |
|
6 val eqa : 'a eq -> 'a -> 'a -> bool |
|
7 val leta : 'a -> ('a -> 'b) -> 'b |
|
8 val suc : IntInf.int -> IntInf.int |
|
9 datatype num = C of IntInf.int | Bound of IntInf.int | |
|
10 Cn of IntInf.int * IntInf.int * num | Neg of num | Add of num * num | |
|
11 Sub of num * num | Mul of IntInf.int * num |
|
12 datatype fm = T | F | Lt of num | Le of num | Gt of num | Ge of num | |
|
13 Eq of num | NEq of num | Dvd of IntInf.int * num | NDvd of IntInf.int * num |
|
14 | Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | |
|
15 Iff of fm * fm | E of fm | A of fm | Closed of IntInf.int | |
|
16 NClosed of IntInf.int |
|
17 val map : ('a -> 'b) -> 'a list -> 'b list |
|
18 val append : 'a list -> 'a list -> 'a list |
|
19 val disjuncts : fm -> fm list |
|
20 val fm_case : |
|
21 'a -> 'a -> (num -> 'a) -> |
|
22 (num -> 'a) -> |
|
23 (num -> 'a) -> |
|
24 (num -> 'a) -> |
|
25 (num -> 'a) -> |
|
26 (num -> 'a) -> |
|
27 (IntInf.int -> num -> 'a) -> |
|
28 (IntInf.int -> num -> 'a) -> |
|
29 (fm -> 'a) -> |
|
30 (fm -> fm -> 'a) -> |
|
31 (fm -> fm -> 'a) -> |
|
32 (fm -> fm -> 'a) -> |
|
33 (fm -> fm -> 'a) -> |
|
34 (fm -> 'a) -> |
|
35 (fm -> 'a) -> (IntInf.int -> 'a) -> (IntInf.int -> 'a) -> fm -> 'a |
|
36 val eq_num : num -> num -> bool |
|
37 val eq_fm : fm -> fm -> bool |
|
38 val djf : ('a -> fm) -> 'a -> fm -> fm |
|
39 val foldr : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b |
|
40 val evaldjf : ('a -> fm) -> 'a list -> fm |
|
41 val dj : (fm -> fm) -> fm -> fm |
|
42 val disj : fm -> fm -> fm |
|
43 val minus_nat : IntInf.int -> IntInf.int -> IntInf.int |
|
44 val decrnum : num -> num |
|
45 val decr : fm -> fm |
|
46 val concat_map : ('a -> 'b list) -> 'a list -> 'b list |
|
47 val numsubst0 : num -> num -> num |
|
48 val subst0 : num -> fm -> fm |
|
49 val minusinf : fm -> fm |
|
50 val eq_int : IntInf.int eq |
|
51 val zero_int : IntInf.int |
|
52 type 'a zero |
|
53 val zero : 'a zero -> 'a |
|
54 val zero_inta : IntInf.int zero |
|
55 type 'a times |
|
56 val times : 'a times -> 'a -> 'a -> 'a |
|
57 type 'a no_zero_divisors |
|
58 val times_no_zero_divisors : 'a no_zero_divisors -> 'a times |
|
59 val zero_no_zero_divisors : 'a no_zero_divisors -> 'a zero |
|
60 val times_int : IntInf.int times |
|
61 val no_zero_divisors_int : IntInf.int no_zero_divisors |
|
62 type 'a one |
|
63 val one : 'a one -> 'a |
|
64 type 'a zero_neq_one |
|
65 val one_zero_neq_one : 'a zero_neq_one -> 'a one |
|
66 val zero_zero_neq_one : 'a zero_neq_one -> 'a zero |
|
67 type 'a semigroup_mult |
|
68 val times_semigroup_mult : 'a semigroup_mult -> 'a times |
|
69 type 'a plus |
|
70 val plus : 'a plus -> 'a -> 'a -> 'a |
|
71 type 'a semigroup_add |
|
72 val plus_semigroup_add : 'a semigroup_add -> 'a plus |
|
73 type 'a ab_semigroup_add |
|
74 val semigroup_add_ab_semigroup_add : 'a ab_semigroup_add -> 'a semigroup_add |
|
75 type 'a semiring |
|
76 val ab_semigroup_add_semiring : 'a semiring -> 'a ab_semigroup_add |
|
77 val semigroup_mult_semiring : 'a semiring -> 'a semigroup_mult |
|
78 type 'a mult_zero |
|
79 val times_mult_zero : 'a mult_zero -> 'a times |
|
80 val zero_mult_zero : 'a mult_zero -> 'a zero |
|
81 type 'a monoid_add |
|
82 val semigroup_add_monoid_add : 'a monoid_add -> 'a semigroup_add |
|
83 val zero_monoid_add : 'a monoid_add -> 'a zero |
|
84 type 'a comm_monoid_add |
|
85 val ab_semigroup_add_comm_monoid_add : |
|
86 'a comm_monoid_add -> 'a ab_semigroup_add |
|
87 val monoid_add_comm_monoid_add : 'a comm_monoid_add -> 'a monoid_add |
|
88 type 'a semiring_0 |
|
89 val comm_monoid_add_semiring_0 : 'a semiring_0 -> 'a comm_monoid_add |
|
90 val mult_zero_semiring_0 : 'a semiring_0 -> 'a mult_zero |
|
91 val semiring_semiring_0 : 'a semiring_0 -> 'a semiring |
|
92 type 'a power |
|
93 val one_power : 'a power -> 'a one |
|
94 val times_power : 'a power -> 'a times |
|
95 type 'a monoid_mult |
|
96 val semigroup_mult_monoid_mult : 'a monoid_mult -> 'a semigroup_mult |
|
97 val power_monoid_mult : 'a monoid_mult -> 'a power |
|
98 type 'a semiring_1 |
|
99 val monoid_mult_semiring_1 : 'a semiring_1 -> 'a monoid_mult |
|
100 val semiring_0_semiring_1 : 'a semiring_1 -> 'a semiring_0 |
|
101 val zero_neq_one_semiring_1 : 'a semiring_1 -> 'a zero_neq_one |
|
102 type 'a cancel_semigroup_add |
|
103 val semigroup_add_cancel_semigroup_add : |
|
104 'a cancel_semigroup_add -> 'a semigroup_add |
|
105 type 'a cancel_ab_semigroup_add |
|
106 val ab_semigroup_add_cancel_ab_semigroup_add : |
|
107 'a cancel_ab_semigroup_add -> 'a ab_semigroup_add |
|
108 val cancel_semigroup_add_cancel_ab_semigroup_add : |
|
109 'a cancel_ab_semigroup_add -> 'a cancel_semigroup_add |
|
110 type 'a cancel_comm_monoid_add |
|
111 val cancel_ab_semigroup_add_cancel_comm_monoid_add : |
|
112 'a cancel_comm_monoid_add -> 'a cancel_ab_semigroup_add |
|
113 val comm_monoid_add_cancel_comm_monoid_add : |
|
114 'a cancel_comm_monoid_add -> 'a comm_monoid_add |
|
115 type 'a semiring_0_cancel |
|
116 val cancel_comm_monoid_add_semiring_0_cancel : |
|
117 'a semiring_0_cancel -> 'a cancel_comm_monoid_add |
|
118 val semiring_0_semiring_0_cancel : 'a semiring_0_cancel -> 'a semiring_0 |
|
119 type 'a semiring_1_cancel |
|
120 val semiring_0_cancel_semiring_1_cancel : |
|
121 'a semiring_1_cancel -> 'a semiring_0_cancel |
|
122 val semiring_1_semiring_1_cancel : 'a semiring_1_cancel -> 'a semiring_1 |
|
123 type 'a dvd |
|
124 val times_dvd : 'a dvd -> 'a times |
|
125 type 'a ab_semigroup_mult |
|
126 val semigroup_mult_ab_semigroup_mult : |
|
127 'a ab_semigroup_mult -> 'a semigroup_mult |
|
128 type 'a comm_semiring |
|
129 val ab_semigroup_mult_comm_semiring : 'a comm_semiring -> 'a ab_semigroup_mult |
|
130 val semiring_comm_semiring : 'a comm_semiring -> 'a semiring |
|
131 type 'a comm_semiring_0 |
|
132 val comm_semiring_comm_semiring_0 : 'a comm_semiring_0 -> 'a comm_semiring |
|
133 val semiring_0_comm_semiring_0 : 'a comm_semiring_0 -> 'a semiring_0 |
|
134 type 'a comm_monoid_mult |
|
135 val ab_semigroup_mult_comm_monoid_mult : |
|
136 'a comm_monoid_mult -> 'a ab_semigroup_mult |
|
137 val monoid_mult_comm_monoid_mult : 'a comm_monoid_mult -> 'a monoid_mult |
|
138 type 'a comm_semiring_1 |
|
139 val comm_monoid_mult_comm_semiring_1 : |
|
140 'a comm_semiring_1 -> 'a comm_monoid_mult |
|
141 val comm_semiring_0_comm_semiring_1 : 'a comm_semiring_1 -> 'a comm_semiring_0 |
|
142 val dvd_comm_semiring_1 : 'a comm_semiring_1 -> 'a dvd |
|
143 val semiring_1_comm_semiring_1 : 'a comm_semiring_1 -> 'a semiring_1 |
|
144 type 'a comm_semiring_0_cancel |
|
145 val comm_semiring_0_comm_semiring_0_cancel : |
|
146 'a comm_semiring_0_cancel -> 'a comm_semiring_0 |
|
147 val semiring_0_cancel_comm_semiring_0_cancel : |
|
148 'a comm_semiring_0_cancel -> 'a semiring_0_cancel |
|
149 type 'a comm_semiring_1_cancel |
|
150 val comm_semiring_0_cancel_comm_semiring_1_cancel : |
|
151 'a comm_semiring_1_cancel -> 'a comm_semiring_0_cancel |
|
152 val comm_semiring_1_comm_semiring_1_cancel : |
|
153 'a comm_semiring_1_cancel -> 'a comm_semiring_1 |
|
154 val semiring_1_cancel_comm_semiring_1_cancel : |
|
155 'a comm_semiring_1_cancel -> 'a semiring_1_cancel |
|
156 type 'a diva |
|
157 val dvd_div : 'a diva -> 'a dvd |
|
158 val diva : 'a diva -> 'a -> 'a -> 'a |
|
159 val moda : 'a diva -> 'a -> 'a -> 'a |
|
160 type 'a semiring_div |
|
161 val div_semiring_div : 'a semiring_div -> 'a diva |
|
162 val comm_semiring_1_cancel_semiring_div : |
|
163 'a semiring_div -> 'a comm_semiring_1_cancel |
|
164 val no_zero_divisors_semiring_div : 'a semiring_div -> 'a no_zero_divisors |
|
165 val one_int : IntInf.int |
|
166 val one_inta : IntInf.int one |
|
167 val zero_neq_one_int : IntInf.int zero_neq_one |
|
168 val semigroup_mult_int : IntInf.int semigroup_mult |
|
169 val plus_int : IntInf.int plus |
|
170 val semigroup_add_int : IntInf.int semigroup_add |
|
171 val ab_semigroup_add_int : IntInf.int ab_semigroup_add |
|
172 val semiring_int : IntInf.int semiring |
|
173 val mult_zero_int : IntInf.int mult_zero |
|
174 val monoid_add_int : IntInf.int monoid_add |
|
175 val comm_monoid_add_int : IntInf.int comm_monoid_add |
|
176 val semiring_0_int : IntInf.int semiring_0 |
|
177 val power_int : IntInf.int power |
|
178 val monoid_mult_int : IntInf.int monoid_mult |
|
179 val semiring_1_int : IntInf.int semiring_1 |
|
180 val cancel_semigroup_add_int : IntInf.int cancel_semigroup_add |
|
181 val cancel_ab_semigroup_add_int : IntInf.int cancel_ab_semigroup_add |
|
182 val cancel_comm_monoid_add_int : IntInf.int cancel_comm_monoid_add |
|
183 val semiring_0_cancel_int : IntInf.int semiring_0_cancel |
|
184 val semiring_1_cancel_int : IntInf.int semiring_1_cancel |
|
185 val dvd_int : IntInf.int dvd |
|
186 val ab_semigroup_mult_int : IntInf.int ab_semigroup_mult |
|
187 val comm_semiring_int : IntInf.int comm_semiring |
|
188 val comm_semiring_0_int : IntInf.int comm_semiring_0 |
|
189 val comm_monoid_mult_int : IntInf.int comm_monoid_mult |
|
190 val comm_semiring_1_int : IntInf.int comm_semiring_1 |
|
191 val comm_semiring_0_cancel_int : IntInf.int comm_semiring_0_cancel |
|
192 val comm_semiring_1_cancel_int : IntInf.int comm_semiring_1_cancel |
|
193 val abs_int : IntInf.int -> IntInf.int |
|
194 val split : ('a -> 'b -> 'c) -> 'a * 'b -> 'c |
|
195 val sgn_int : IntInf.int -> IntInf.int |
|
196 val apsnd : ('a -> 'b) -> 'c * 'a -> 'c * 'b |
|
197 val divmod_int : IntInf.int -> IntInf.int -> IntInf.int * IntInf.int |
|
198 val snd : 'a * 'b -> 'b |
|
199 val mod_int : IntInf.int -> IntInf.int -> IntInf.int |
|
200 val fst : 'a * 'b -> 'a |
|
201 val div_int : IntInf.int -> IntInf.int -> IntInf.int |
|
202 val div_inta : IntInf.int diva |
|
203 val semiring_div_int : IntInf.int semiring_div |
|
204 val dvd : 'a semiring_div * 'a eq -> 'a -> 'a -> bool |
|
205 val num_case : |
|
206 (IntInf.int -> 'a) -> |
|
207 (IntInf.int -> 'a) -> |
|
208 (IntInf.int -> IntInf.int -> num -> 'a) -> |
|
209 (num -> 'a) -> |
|
210 (num -> num -> 'a) -> |
|
211 (num -> num -> 'a) -> (IntInf.int -> num -> 'a) -> num -> 'a |
|
212 val nummul : IntInf.int -> num -> num |
|
213 val numneg : num -> num |
|
214 val numadd : num * num -> num |
|
215 val numsub : num -> num -> num |
|
216 val simpnum : num -> num |
|
217 val nota : fm -> fm |
|
218 val iffa : fm -> fm -> fm |
|
219 val impa : fm -> fm -> fm |
|
220 val conj : fm -> fm -> fm |
|
221 val simpfm : fm -> fm |
|
222 val iupt : IntInf.int -> IntInf.int -> IntInf.int list |
|
223 val mirror : fm -> fm |
|
224 val size_list : 'a list -> IntInf.int |
|
225 val alpha : fm -> num list |
|
226 val beta : fm -> num list |
|
227 val eq_numa : num eq |
|
228 val member : 'a eq -> 'a -> 'a list -> bool |
|
229 val remdups : 'a eq -> 'a list -> 'a list |
|
230 val gcd_int : IntInf.int -> IntInf.int -> IntInf.int |
|
231 val lcm_int : IntInf.int -> IntInf.int -> IntInf.int |
|
232 val delta : fm -> IntInf.int |
|
233 val a_beta : fm -> IntInf.int -> fm |
|
234 val zeta : fm -> IntInf.int |
|
235 val zsplit0 : num -> IntInf.int * num |
|
236 val zlfm : fm -> fm |
|
237 val unita : fm -> fm * (num list * IntInf.int) |
|
238 val cooper : fm -> fm |
|
239 val prep : fm -> fm |
|
240 val qelim : fm -> (fm -> fm) -> fm |
|
241 val pa : fm -> fm |
|
242 end = struct |
|
243 |
|
244 type 'a eq = {eq : 'a -> 'a -> bool}; |
|
245 val eq = #eq : 'a eq -> 'a -> 'a -> bool; |
|
246 |
|
247 fun eqa A_ a b = eq A_ a b; |
|
248 |
|
249 fun leta s f = f s; |
|
250 |
|
251 fun suc n = IntInf.+ (n, (1 : IntInf.int)); |
|
252 |
|
253 datatype num = C of IntInf.int | Bound of IntInf.int | |
|
254 Cn of IntInf.int * IntInf.int * num | Neg of num | Add of num * num | |
|
255 Sub of num * num | Mul of IntInf.int * num; |
|
256 |
|
257 datatype fm = T | F | Lt of num | Le of num | Gt of num | Ge of num | Eq of num |
|
258 | NEq of num | Dvd of IntInf.int * num | NDvd of IntInf.int * num | Not of fm |
|
259 | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm | E of fm | |
|
260 A of fm | Closed of IntInf.int | NClosed of IntInf.int; |
|
261 |
|
262 fun map f [] = [] |
|
263 | map f (x :: xs) = f x :: map f xs; |
|
264 |
|
265 fun append [] ys = ys |
|
266 | append (x :: xs) ys = x :: append xs ys; |
|
267 |
|
268 fun disjuncts (Or (p, q)) = append (disjuncts p) (disjuncts q) |
|
269 | disjuncts F = [] |
|
270 | disjuncts T = [T] |
|
271 | disjuncts (Lt u) = [Lt u] |
|
272 | disjuncts (Le v) = [Le v] |
|
273 | disjuncts (Gt w) = [Gt w] |
|
274 | disjuncts (Ge x) = [Ge x] |
|
275 | disjuncts (Eq y) = [Eq y] |
|
276 | disjuncts (NEq z) = [NEq z] |
|
277 | disjuncts (Dvd (aa, ab)) = [Dvd (aa, ab)] |
|
278 | disjuncts (NDvd (ac, ad)) = [NDvd (ac, ad)] |
|
279 | disjuncts (Not ae) = [Not ae] |
|
280 | disjuncts (And (af, ag)) = [And (af, ag)] |
|
281 | disjuncts (Imp (aj, ak)) = [Imp (aj, ak)] |
|
282 | disjuncts (Iff (al, am)) = [Iff (al, am)] |
|
283 | disjuncts (E an) = [E an] |
|
284 | disjuncts (A ao) = [A ao] |
|
285 | disjuncts (Closed ap) = [Closed ap] |
|
286 | disjuncts (NClosed aq) = [NClosed aq]; |
|
287 |
|
288 fun fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
289 (NClosed nat) = f19 nat |
|
290 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
291 (Closed nat) = f18 nat |
|
292 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
293 (A fm) = f17 fm |
|
294 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
295 (E fm) = f16 fm |
|
296 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
297 (Iff (fm1, fm2)) = f15 fm1 fm2 |
|
298 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
299 (Imp (fm1, fm2)) = f14 fm1 fm2 |
|
300 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
301 (Or (fm1, fm2)) = f13 fm1 fm2 |
|
302 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
303 (And (fm1, fm2)) = f12 fm1 fm2 |
|
304 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
305 (Not fm) = f11 fm |
|
306 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
307 (NDvd (inta, num)) = f10 inta num |
|
308 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
309 (Dvd (inta, num)) = f9 inta num |
|
310 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
311 (NEq num) = f8 num |
|
312 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
313 (Eq num) = f7 num |
|
314 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
315 (Ge num) = f6 num |
|
316 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
317 (Gt num) = f5 num |
|
318 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
319 (Le num) = f4 num |
|
320 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 |
|
321 (Lt num) = f3 num |
|
322 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F |
|
323 = f2 |
|
324 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T |
|
325 = f1; |
|
326 |
|
327 fun eq_num (C intaa) (C inta) = ((intaa : IntInf.int) = inta) |
|
328 | eq_num (Bound nata) (Bound nat) = ((nata : IntInf.int) = nat) |
|
329 | eq_num (Cn (nata, intaa, numa)) (Cn (nat, inta, num)) = |
|
330 ((nata : IntInf.int) = nat) andalso |
|
331 (((intaa : IntInf.int) = inta) andalso eq_num numa num) |
|
332 | eq_num (Neg numa) (Neg num) = eq_num numa num |
|
333 | eq_num (Add (num1a, num2a)) (Add (num1, num2)) = |
|
334 eq_num num1a num1 andalso eq_num num2a num2 |
|
335 | eq_num (Sub (num1a, num2a)) (Sub (num1, num2)) = |
|
336 eq_num num1a num1 andalso eq_num num2a num2 |
|
337 | eq_num (Mul (intaa, numa)) (Mul (inta, num)) = |
|
338 ((intaa : IntInf.int) = inta) andalso eq_num numa num |
|
339 | eq_num (C inta) (Bound nat) = false |
|
340 | eq_num (Bound nat) (C inta) = false |
|
341 | eq_num (C intaa) (Cn (nat, inta, num)) = false |
|
342 | eq_num (Cn (nat, intaa, num)) (C inta) = false |
|
343 | eq_num (C inta) (Neg num) = false |
|
344 | eq_num (Neg num) (C inta) = false |
|
345 | eq_num (C inta) (Add (num1, num2)) = false |
|
346 | eq_num (Add (num1, num2)) (C inta) = false |
|
347 | eq_num (C inta) (Sub (num1, num2)) = false |
|
348 | eq_num (Sub (num1, num2)) (C inta) = false |
|
349 | eq_num (C intaa) (Mul (inta, num)) = false |
|
350 | eq_num (Mul (intaa, num)) (C inta) = false |
|
351 | eq_num (Bound nata) (Cn (nat, inta, num)) = false |
|
352 | eq_num (Cn (nata, inta, num)) (Bound nat) = false |
|
353 | eq_num (Bound nat) (Neg num) = false |
|
354 | eq_num (Neg num) (Bound nat) = false |
|
355 | eq_num (Bound nat) (Add (num1, num2)) = false |
|
356 | eq_num (Add (num1, num2)) (Bound nat) = false |
|
357 | eq_num (Bound nat) (Sub (num1, num2)) = false |
|
358 | eq_num (Sub (num1, num2)) (Bound nat) = false |
|
359 | eq_num (Bound nat) (Mul (inta, num)) = false |
|
360 | eq_num (Mul (inta, num)) (Bound nat) = false |
|
361 | eq_num (Cn (nat, inta, numa)) (Neg num) = false |
|
362 | eq_num (Neg numa) (Cn (nat, inta, num)) = false |
|
363 | eq_num (Cn (nat, inta, num)) (Add (num1, num2)) = false |
|
364 | eq_num (Add (num1, num2)) (Cn (nat, inta, num)) = false |
|
365 | eq_num (Cn (nat, inta, num)) (Sub (num1, num2)) = false |
|
366 | eq_num (Sub (num1, num2)) (Cn (nat, inta, num)) = false |
|
367 | eq_num (Cn (nat, intaa, numa)) (Mul (inta, num)) = false |
|
368 | eq_num (Mul (intaa, numa)) (Cn (nat, inta, num)) = false |
|
369 | eq_num (Neg num) (Add (num1, num2)) = false |
|
370 | eq_num (Add (num1, num2)) (Neg num) = false |
|
371 | eq_num (Neg num) (Sub (num1, num2)) = false |
|
372 | eq_num (Sub (num1, num2)) (Neg num) = false |
|
373 | eq_num (Neg numa) (Mul (inta, num)) = false |
|
374 | eq_num (Mul (inta, numa)) (Neg num) = false |
|
375 | eq_num (Add (num1a, num2a)) (Sub (num1, num2)) = false |
|
376 | eq_num (Sub (num1a, num2a)) (Add (num1, num2)) = false |
|
377 | eq_num (Add (num1, num2)) (Mul (inta, num)) = false |
|
378 | eq_num (Mul (inta, num)) (Add (num1, num2)) = false |
|
379 | eq_num (Sub (num1, num2)) (Mul (inta, num)) = false |
|
380 | eq_num (Mul (inta, num)) (Sub (num1, num2)) = false; |
|
381 |
|
382 fun eq_fm T T = true |
|
383 | eq_fm F F = true |
|
384 | eq_fm (Lt numa) (Lt num) = eq_num numa num |
|
385 | eq_fm (Le numa) (Le num) = eq_num numa num |
|
386 | eq_fm (Gt numa) (Gt num) = eq_num numa num |
|
387 | eq_fm (Ge numa) (Ge num) = eq_num numa num |
|
388 | eq_fm (Eq numa) (Eq num) = eq_num numa num |
|
389 | eq_fm (NEq numa) (NEq num) = eq_num numa num |
|
390 | eq_fm (Dvd (intaa, numa)) (Dvd (inta, num)) = |
|
391 ((intaa : IntInf.int) = inta) andalso eq_num numa num |
|
392 | eq_fm (NDvd (intaa, numa)) (NDvd (inta, num)) = |
|
393 ((intaa : IntInf.int) = inta) andalso eq_num numa num |
|
394 | eq_fm (Not fma) (Not fm) = eq_fm fma fm |
|
395 | eq_fm (And (fm1a, fm2a)) (And (fm1, fm2)) = |
|
396 eq_fm fm1a fm1 andalso eq_fm fm2a fm2 |
|
397 | eq_fm (Or (fm1a, fm2a)) (Or (fm1, fm2)) = |
|
398 eq_fm fm1a fm1 andalso eq_fm fm2a fm2 |
|
399 | eq_fm (Imp (fm1a, fm2a)) (Imp (fm1, fm2)) = |
|
400 eq_fm fm1a fm1 andalso eq_fm fm2a fm2 |
|
401 | eq_fm (Iff (fm1a, fm2a)) (Iff (fm1, fm2)) = |
|
402 eq_fm fm1a fm1 andalso eq_fm fm2a fm2 |
|
403 | eq_fm (E fma) (E fm) = eq_fm fma fm |
|
404 | eq_fm (A fma) (A fm) = eq_fm fma fm |
|
405 | eq_fm (Closed nata) (Closed nat) = ((nata : IntInf.int) = nat) |
|
406 | eq_fm (NClosed nata) (NClosed nat) = ((nata : IntInf.int) = nat) |
|
407 | eq_fm T F = false |
|
408 | eq_fm F T = false |
|
409 | eq_fm T (Lt num) = false |
|
410 | eq_fm (Lt num) T = false |
|
411 | eq_fm T (Le num) = false |
|
412 | eq_fm (Le num) T = false |
|
413 | eq_fm T (Gt num) = false |
|
414 | eq_fm (Gt num) T = false |
|
415 | eq_fm T (Ge num) = false |
|
416 | eq_fm (Ge num) T = false |
|
417 | eq_fm T (Eq num) = false |
|
418 | eq_fm (Eq num) T = false |
|
419 | eq_fm T (NEq num) = false |
|
420 | eq_fm (NEq num) T = false |
|
421 | eq_fm T (Dvd (inta, num)) = false |
|
422 | eq_fm (Dvd (inta, num)) T = false |
|
423 | eq_fm T (NDvd (inta, num)) = false |
|
424 | eq_fm (NDvd (inta, num)) T = false |
|
425 | eq_fm T (Not fm) = false |
|
426 | eq_fm (Not fm) T = false |
|
427 | eq_fm T (And (fm1, fm2)) = false |
|
428 | eq_fm (And (fm1, fm2)) T = false |
|
429 | eq_fm T (Or (fm1, fm2)) = false |
|
430 | eq_fm (Or (fm1, fm2)) T = false |
|
431 | eq_fm T (Imp (fm1, fm2)) = false |
|
432 | eq_fm (Imp (fm1, fm2)) T = false |
|
433 | eq_fm T (Iff (fm1, fm2)) = false |
|
434 | eq_fm (Iff (fm1, fm2)) T = false |
|
435 | eq_fm T (E fm) = false |
|
436 | eq_fm (E fm) T = false |
|
437 | eq_fm T (A fm) = false |
|
438 | eq_fm (A fm) T = false |
|
439 | eq_fm T (Closed nat) = false |
|
440 | eq_fm (Closed nat) T = false |
|
441 | eq_fm T (NClosed nat) = false |
|
442 | eq_fm (NClosed nat) T = false |
|
443 | eq_fm F (Lt num) = false |
|
444 | eq_fm (Lt num) F = false |
|
445 | eq_fm F (Le num) = false |
|
446 | eq_fm (Le num) F = false |
|
447 | eq_fm F (Gt num) = false |
|
448 | eq_fm (Gt num) F = false |
|
449 | eq_fm F (Ge num) = false |
|
450 | eq_fm (Ge num) F = false |
|
451 | eq_fm F (Eq num) = false |
|
452 | eq_fm (Eq num) F = false |
|
453 | eq_fm F (NEq num) = false |
|
454 | eq_fm (NEq num) F = false |
|
455 | eq_fm F (Dvd (inta, num)) = false |
|
456 | eq_fm (Dvd (inta, num)) F = false |
|
457 | eq_fm F (NDvd (inta, num)) = false |
|
458 | eq_fm (NDvd (inta, num)) F = false |
|
459 | eq_fm F (Not fm) = false |
|
460 | eq_fm (Not fm) F = false |
|
461 | eq_fm F (And (fm1, fm2)) = false |
|
462 | eq_fm (And (fm1, fm2)) F = false |
|
463 | eq_fm F (Or (fm1, fm2)) = false |
|
464 | eq_fm (Or (fm1, fm2)) F = false |
|
465 | eq_fm F (Imp (fm1, fm2)) = false |
|
466 | eq_fm (Imp (fm1, fm2)) F = false |
|
467 | eq_fm F (Iff (fm1, fm2)) = false |
|
468 | eq_fm (Iff (fm1, fm2)) F = false |
|
469 | eq_fm F (E fm) = false |
|
470 | eq_fm (E fm) F = false |
|
471 | eq_fm F (A fm) = false |
|
472 | eq_fm (A fm) F = false |
|
473 | eq_fm F (Closed nat) = false |
|
474 | eq_fm (Closed nat) F = false |
|
475 | eq_fm F (NClosed nat) = false |
|
476 | eq_fm (NClosed nat) F = false |
|
477 | eq_fm (Lt numa) (Le num) = false |
|
478 | eq_fm (Le numa) (Lt num) = false |
|
479 | eq_fm (Lt numa) (Gt num) = false |
|
480 | eq_fm (Gt numa) (Lt num) = false |
|
481 | eq_fm (Lt numa) (Ge num) = false |
|
482 | eq_fm (Ge numa) (Lt num) = false |
|
483 | eq_fm (Lt numa) (Eq num) = false |
|
484 | eq_fm (Eq numa) (Lt num) = false |
|
485 | eq_fm (Lt numa) (NEq num) = false |
|
486 | eq_fm (NEq numa) (Lt num) = false |
|
487 | eq_fm (Lt numa) (Dvd (inta, num)) = false |
|
488 | eq_fm (Dvd (inta, numa)) (Lt num) = false |
|
489 | eq_fm (Lt numa) (NDvd (inta, num)) = false |
|
490 | eq_fm (NDvd (inta, numa)) (Lt num) = false |
|
491 | eq_fm (Lt num) (Not fm) = false |
|
492 | eq_fm (Not fm) (Lt num) = false |
|
493 | eq_fm (Lt num) (And (fm1, fm2)) = false |
|
494 | eq_fm (And (fm1, fm2)) (Lt num) = false |
|
495 | eq_fm (Lt num) (Or (fm1, fm2)) = false |
|
496 | eq_fm (Or (fm1, fm2)) (Lt num) = false |
|
497 | eq_fm (Lt num) (Imp (fm1, fm2)) = false |
|
498 | eq_fm (Imp (fm1, fm2)) (Lt num) = false |
|
499 | eq_fm (Lt num) (Iff (fm1, fm2)) = false |
|
500 | eq_fm (Iff (fm1, fm2)) (Lt num) = false |
|
501 | eq_fm (Lt num) (E fm) = false |
|
502 | eq_fm (E fm) (Lt num) = false |
|
503 | eq_fm (Lt num) (A fm) = false |
|
504 | eq_fm (A fm) (Lt num) = false |
|
505 | eq_fm (Lt num) (Closed nat) = false |
|
506 | eq_fm (Closed nat) (Lt num) = false |
|
507 | eq_fm (Lt num) (NClosed nat) = false |
|
508 | eq_fm (NClosed nat) (Lt num) = false |
|
509 | eq_fm (Le numa) (Gt num) = false |
|
510 | eq_fm (Gt numa) (Le num) = false |
|
511 | eq_fm (Le numa) (Ge num) = false |
|
512 | eq_fm (Ge numa) (Le num) = false |
|
513 | eq_fm (Le numa) (Eq num) = false |
|
514 | eq_fm (Eq numa) (Le num) = false |
|
515 | eq_fm (Le numa) (NEq num) = false |
|
516 | eq_fm (NEq numa) (Le num) = false |
|
517 | eq_fm (Le numa) (Dvd (inta, num)) = false |
|
518 | eq_fm (Dvd (inta, numa)) (Le num) = false |
|
519 | eq_fm (Le numa) (NDvd (inta, num)) = false |
|
520 | eq_fm (NDvd (inta, numa)) (Le num) = false |
|
521 | eq_fm (Le num) (Not fm) = false |
|
522 | eq_fm (Not fm) (Le num) = false |
|
523 | eq_fm (Le num) (And (fm1, fm2)) = false |
|
524 | eq_fm (And (fm1, fm2)) (Le num) = false |
|
525 | eq_fm (Le num) (Or (fm1, fm2)) = false |
|
526 | eq_fm (Or (fm1, fm2)) (Le num) = false |
|
527 | eq_fm (Le num) (Imp (fm1, fm2)) = false |
|
528 | eq_fm (Imp (fm1, fm2)) (Le num) = false |
|
529 | eq_fm (Le num) (Iff (fm1, fm2)) = false |
|
530 | eq_fm (Iff (fm1, fm2)) (Le num) = false |
|
531 | eq_fm (Le num) (E fm) = false |
|
532 | eq_fm (E fm) (Le num) = false |
|
533 | eq_fm (Le num) (A fm) = false |
|
534 | eq_fm (A fm) (Le num) = false |
|
535 | eq_fm (Le num) (Closed nat) = false |
|
536 | eq_fm (Closed nat) (Le num) = false |
|
537 | eq_fm (Le num) (NClosed nat) = false |
|
538 | eq_fm (NClosed nat) (Le num) = false |
|
539 | eq_fm (Gt numa) (Ge num) = false |
|
540 | eq_fm (Ge numa) (Gt num) = false |
|
541 | eq_fm (Gt numa) (Eq num) = false |
|
542 | eq_fm (Eq numa) (Gt num) = false |
|
543 | eq_fm (Gt numa) (NEq num) = false |
|
544 | eq_fm (NEq numa) (Gt num) = false |
|
545 | eq_fm (Gt numa) (Dvd (inta, num)) = false |
|
546 | eq_fm (Dvd (inta, numa)) (Gt num) = false |
|
547 | eq_fm (Gt numa) (NDvd (inta, num)) = false |
|
548 | eq_fm (NDvd (inta, numa)) (Gt num) = false |
|
549 | eq_fm (Gt num) (Not fm) = false |
|
550 | eq_fm (Not fm) (Gt num) = false |
|
551 | eq_fm (Gt num) (And (fm1, fm2)) = false |
|
552 | eq_fm (And (fm1, fm2)) (Gt num) = false |
|
553 | eq_fm (Gt num) (Or (fm1, fm2)) = false |
|
554 | eq_fm (Or (fm1, fm2)) (Gt num) = false |
|
555 | eq_fm (Gt num) (Imp (fm1, fm2)) = false |
|
556 | eq_fm (Imp (fm1, fm2)) (Gt num) = false |
|
557 | eq_fm (Gt num) (Iff (fm1, fm2)) = false |
|
558 | eq_fm (Iff (fm1, fm2)) (Gt num) = false |
|
559 | eq_fm (Gt num) (E fm) = false |
|
560 | eq_fm (E fm) (Gt num) = false |
|
561 | eq_fm (Gt num) (A fm) = false |
|
562 | eq_fm (A fm) (Gt num) = false |
|
563 | eq_fm (Gt num) (Closed nat) = false |
|
564 | eq_fm (Closed nat) (Gt num) = false |
|
565 | eq_fm (Gt num) (NClosed nat) = false |
|
566 | eq_fm (NClosed nat) (Gt num) = false |
|
567 | eq_fm (Ge numa) (Eq num) = false |
|
568 | eq_fm (Eq numa) (Ge num) = false |
|
569 | eq_fm (Ge numa) (NEq num) = false |
|
570 | eq_fm (NEq numa) (Ge num) = false |
|
571 | eq_fm (Ge numa) (Dvd (inta, num)) = false |
|
572 | eq_fm (Dvd (inta, numa)) (Ge num) = false |
|
573 | eq_fm (Ge numa) (NDvd (inta, num)) = false |
|
574 | eq_fm (NDvd (inta, numa)) (Ge num) = false |
|
575 | eq_fm (Ge num) (Not fm) = false |
|
576 | eq_fm (Not fm) (Ge num) = false |
|
577 | eq_fm (Ge num) (And (fm1, fm2)) = false |
|
578 | eq_fm (And (fm1, fm2)) (Ge num) = false |
|
579 | eq_fm (Ge num) (Or (fm1, fm2)) = false |
|
580 | eq_fm (Or (fm1, fm2)) (Ge num) = false |
|
581 | eq_fm (Ge num) (Imp (fm1, fm2)) = false |
|
582 | eq_fm (Imp (fm1, fm2)) (Ge num) = false |
|
583 | eq_fm (Ge num) (Iff (fm1, fm2)) = false |
|
584 | eq_fm (Iff (fm1, fm2)) (Ge num) = false |
|
585 | eq_fm (Ge num) (E fm) = false |
|
586 | eq_fm (E fm) (Ge num) = false |
|
587 | eq_fm (Ge num) (A fm) = false |
|
588 | eq_fm (A fm) (Ge num) = false |
|
589 | eq_fm (Ge num) (Closed nat) = false |
|
590 | eq_fm (Closed nat) (Ge num) = false |
|
591 | eq_fm (Ge num) (NClosed nat) = false |
|
592 | eq_fm (NClosed nat) (Ge num) = false |
|
593 | eq_fm (Eq numa) (NEq num) = false |
|
594 | eq_fm (NEq numa) (Eq num) = false |
|
595 | eq_fm (Eq numa) (Dvd (inta, num)) = false |
|
596 | eq_fm (Dvd (inta, numa)) (Eq num) = false |
|
597 | eq_fm (Eq numa) (NDvd (inta, num)) = false |
|
598 | eq_fm (NDvd (inta, numa)) (Eq num) = false |
|
599 | eq_fm (Eq num) (Not fm) = false |
|
600 | eq_fm (Not fm) (Eq num) = false |
|
601 | eq_fm (Eq num) (And (fm1, fm2)) = false |
|
602 | eq_fm (And (fm1, fm2)) (Eq num) = false |
|
603 | eq_fm (Eq num) (Or (fm1, fm2)) = false |
|
604 | eq_fm (Or (fm1, fm2)) (Eq num) = false |
|
605 | eq_fm (Eq num) (Imp (fm1, fm2)) = false |
|
606 | eq_fm (Imp (fm1, fm2)) (Eq num) = false |
|
607 | eq_fm (Eq num) (Iff (fm1, fm2)) = false |
|
608 | eq_fm (Iff (fm1, fm2)) (Eq num) = false |
|
609 | eq_fm (Eq num) (E fm) = false |
|
610 | eq_fm (E fm) (Eq num) = false |
|
611 | eq_fm (Eq num) (A fm) = false |
|
612 | eq_fm (A fm) (Eq num) = false |
|
613 | eq_fm (Eq num) (Closed nat) = false |
|
614 | eq_fm (Closed nat) (Eq num) = false |
|
615 | eq_fm (Eq num) (NClosed nat) = false |
|
616 | eq_fm (NClosed nat) (Eq num) = false |
|
617 | eq_fm (NEq numa) (Dvd (inta, num)) = false |
|
618 | eq_fm (Dvd (inta, numa)) (NEq num) = false |
|
619 | eq_fm (NEq numa) (NDvd (inta, num)) = false |
|
620 | eq_fm (NDvd (inta, numa)) (NEq num) = false |
|
621 | eq_fm (NEq num) (Not fm) = false |
|
622 | eq_fm (Not fm) (NEq num) = false |
|
623 | eq_fm (NEq num) (And (fm1, fm2)) = false |
|
624 | eq_fm (And (fm1, fm2)) (NEq num) = false |
|
625 | eq_fm (NEq num) (Or (fm1, fm2)) = false |
|
626 | eq_fm (Or (fm1, fm2)) (NEq num) = false |
|
627 | eq_fm (NEq num) (Imp (fm1, fm2)) = false |
|
628 | eq_fm (Imp (fm1, fm2)) (NEq num) = false |
|
629 | eq_fm (NEq num) (Iff (fm1, fm2)) = false |
|
630 | eq_fm (Iff (fm1, fm2)) (NEq num) = false |
|
631 | eq_fm (NEq num) (E fm) = false |
|
632 | eq_fm (E fm) (NEq num) = false |
|
633 | eq_fm (NEq num) (A fm) = false |
|
634 | eq_fm (A fm) (NEq num) = false |
|
635 | eq_fm (NEq num) (Closed nat) = false |
|
636 | eq_fm (Closed nat) (NEq num) = false |
|
637 | eq_fm (NEq num) (NClosed nat) = false |
|
638 | eq_fm (NClosed nat) (NEq num) = false |
|
639 | eq_fm (Dvd (intaa, numa)) (NDvd (inta, num)) = false |
|
640 | eq_fm (NDvd (intaa, numa)) (Dvd (inta, num)) = false |
|
641 | eq_fm (Dvd (inta, num)) (Not fm) = false |
|
642 | eq_fm (Not fm) (Dvd (inta, num)) = false |
|
643 | eq_fm (Dvd (inta, num)) (And (fm1, fm2)) = false |
|
644 | eq_fm (And (fm1, fm2)) (Dvd (inta, num)) = false |
|
645 | eq_fm (Dvd (inta, num)) (Or (fm1, fm2)) = false |
|
646 | eq_fm (Or (fm1, fm2)) (Dvd (inta, num)) = false |
|
647 | eq_fm (Dvd (inta, num)) (Imp (fm1, fm2)) = false |
|
648 | eq_fm (Imp (fm1, fm2)) (Dvd (inta, num)) = false |
|
649 | eq_fm (Dvd (inta, num)) (Iff (fm1, fm2)) = false |
|
650 | eq_fm (Iff (fm1, fm2)) (Dvd (inta, num)) = false |
|
651 | eq_fm (Dvd (inta, num)) (E fm) = false |
|
652 | eq_fm (E fm) (Dvd (inta, num)) = false |
|
653 | eq_fm (Dvd (inta, num)) (A fm) = false |
|
654 | eq_fm (A fm) (Dvd (inta, num)) = false |
|
655 | eq_fm (Dvd (inta, num)) (Closed nat) = false |
|
656 | eq_fm (Closed nat) (Dvd (inta, num)) = false |
|
657 | eq_fm (Dvd (inta, num)) (NClosed nat) = false |
|
658 | eq_fm (NClosed nat) (Dvd (inta, num)) = false |
|
659 | eq_fm (NDvd (inta, num)) (Not fm) = false |
|
660 | eq_fm (Not fm) (NDvd (inta, num)) = false |
|
661 | eq_fm (NDvd (inta, num)) (And (fm1, fm2)) = false |
|
662 | eq_fm (And (fm1, fm2)) (NDvd (inta, num)) = false |
|
663 | eq_fm (NDvd (inta, num)) (Or (fm1, fm2)) = false |
|
664 | eq_fm (Or (fm1, fm2)) (NDvd (inta, num)) = false |
|
665 | eq_fm (NDvd (inta, num)) (Imp (fm1, fm2)) = false |
|
666 | eq_fm (Imp (fm1, fm2)) (NDvd (inta, num)) = false |
|
667 | eq_fm (NDvd (inta, num)) (Iff (fm1, fm2)) = false |
|
668 | eq_fm (Iff (fm1, fm2)) (NDvd (inta, num)) = false |
|
669 | eq_fm (NDvd (inta, num)) (E fm) = false |
|
670 | eq_fm (E fm) (NDvd (inta, num)) = false |
|
671 | eq_fm (NDvd (inta, num)) (A fm) = false |
|
672 | eq_fm (A fm) (NDvd (inta, num)) = false |
|
673 | eq_fm (NDvd (inta, num)) (Closed nat) = false |
|
674 | eq_fm (Closed nat) (NDvd (inta, num)) = false |
|
675 | eq_fm (NDvd (inta, num)) (NClosed nat) = false |
|
676 | eq_fm (NClosed nat) (NDvd (inta, num)) = false |
|
677 | eq_fm (Not fm) (And (fm1, fm2)) = false |
|
678 | eq_fm (And (fm1, fm2)) (Not fm) = false |
|
679 | eq_fm (Not fm) (Or (fm1, fm2)) = false |
|
680 | eq_fm (Or (fm1, fm2)) (Not fm) = false |
|
681 | eq_fm (Not fm) (Imp (fm1, fm2)) = false |
|
682 | eq_fm (Imp (fm1, fm2)) (Not fm) = false |
|
683 | eq_fm (Not fm) (Iff (fm1, fm2)) = false |
|
684 | eq_fm (Iff (fm1, fm2)) (Not fm) = false |
|
685 | eq_fm (Not fma) (E fm) = false |
|
686 | eq_fm (E fma) (Not fm) = false |
|
687 | eq_fm (Not fma) (A fm) = false |
|
688 | eq_fm (A fma) (Not fm) = false |
|
689 | eq_fm (Not fm) (Closed nat) = false |
|
690 | eq_fm (Closed nat) (Not fm) = false |
|
691 | eq_fm (Not fm) (NClosed nat) = false |
|
692 | eq_fm (NClosed nat) (Not fm) = false |
|
693 | eq_fm (And (fm1a, fm2a)) (Or (fm1, fm2)) = false |
|
694 | eq_fm (Or (fm1a, fm2a)) (And (fm1, fm2)) = false |
|
695 | eq_fm (And (fm1a, fm2a)) (Imp (fm1, fm2)) = false |
|
696 | eq_fm (Imp (fm1a, fm2a)) (And (fm1, fm2)) = false |
|
697 | eq_fm (And (fm1a, fm2a)) (Iff (fm1, fm2)) = false |
|
698 | eq_fm (Iff (fm1a, fm2a)) (And (fm1, fm2)) = false |
|
699 | eq_fm (And (fm1, fm2)) (E fm) = false |
|
700 | eq_fm (E fm) (And (fm1, fm2)) = false |
|
701 | eq_fm (And (fm1, fm2)) (A fm) = false |
|
702 | eq_fm (A fm) (And (fm1, fm2)) = false |
|
703 | eq_fm (And (fm1, fm2)) (Closed nat) = false |
|
704 | eq_fm (Closed nat) (And (fm1, fm2)) = false |
|
705 | eq_fm (And (fm1, fm2)) (NClosed nat) = false |
|
706 | eq_fm (NClosed nat) (And (fm1, fm2)) = false |
|
707 | eq_fm (Or (fm1a, fm2a)) (Imp (fm1, fm2)) = false |
|
708 | eq_fm (Imp (fm1a, fm2a)) (Or (fm1, fm2)) = false |
|
709 | eq_fm (Or (fm1a, fm2a)) (Iff (fm1, fm2)) = false |
|
710 | eq_fm (Iff (fm1a, fm2a)) (Or (fm1, fm2)) = false |
|
711 | eq_fm (Or (fm1, fm2)) (E fm) = false |
|
712 | eq_fm (E fm) (Or (fm1, fm2)) = false |
|
713 | eq_fm (Or (fm1, fm2)) (A fm) = false |
|
714 | eq_fm (A fm) (Or (fm1, fm2)) = false |
|
715 | eq_fm (Or (fm1, fm2)) (Closed nat) = false |
|
716 | eq_fm (Closed nat) (Or (fm1, fm2)) = false |
|
717 | eq_fm (Or (fm1, fm2)) (NClosed nat) = false |
|
718 | eq_fm (NClosed nat) (Or (fm1, fm2)) = false |
|
719 | eq_fm (Imp (fm1a, fm2a)) (Iff (fm1, fm2)) = false |
|
720 | eq_fm (Iff (fm1a, fm2a)) (Imp (fm1, fm2)) = false |
|
721 | eq_fm (Imp (fm1, fm2)) (E fm) = false |
|
722 | eq_fm (E fm) (Imp (fm1, fm2)) = false |
|
723 | eq_fm (Imp (fm1, fm2)) (A fm) = false |
|
724 | eq_fm (A fm) (Imp (fm1, fm2)) = false |
|
725 | eq_fm (Imp (fm1, fm2)) (Closed nat) = false |
|
726 | eq_fm (Closed nat) (Imp (fm1, fm2)) = false |
|
727 | eq_fm (Imp (fm1, fm2)) (NClosed nat) = false |
|
728 | eq_fm (NClosed nat) (Imp (fm1, fm2)) = false |
|
729 | eq_fm (Iff (fm1, fm2)) (E fm) = false |
|
730 | eq_fm (E fm) (Iff (fm1, fm2)) = false |
|
731 | eq_fm (Iff (fm1, fm2)) (A fm) = false |
|
732 | eq_fm (A fm) (Iff (fm1, fm2)) = false |
|
733 | eq_fm (Iff (fm1, fm2)) (Closed nat) = false |
|
734 | eq_fm (Closed nat) (Iff (fm1, fm2)) = false |
|
735 | eq_fm (Iff (fm1, fm2)) (NClosed nat) = false |
|
736 | eq_fm (NClosed nat) (Iff (fm1, fm2)) = false |
|
737 | eq_fm (E fma) (A fm) = false |
|
738 | eq_fm (A fma) (E fm) = false |
|
739 | eq_fm (E fm) (Closed nat) = false |
|
740 | eq_fm (Closed nat) (E fm) = false |
|
741 | eq_fm (E fm) (NClosed nat) = false |
|
742 | eq_fm (NClosed nat) (E fm) = false |
|
743 | eq_fm (A fm) (Closed nat) = false |
|
744 | eq_fm (Closed nat) (A fm) = false |
|
745 | eq_fm (A fm) (NClosed nat) = false |
|
746 | eq_fm (NClosed nat) (A fm) = false |
|
747 | eq_fm (Closed nata) (NClosed nat) = false |
|
748 | eq_fm (NClosed nata) (Closed nat) = false; |
|
749 |
|
750 fun djf f p q = |
|
751 (if eq_fm q T then T |
|
752 else (if eq_fm q F then f p |
|
753 else (case f p of T => T | F => q | Lt _ => Or (f p, q) |
|
754 | Le _ => Or (f p, q) | Gt _ => Or (f p, q) |
|
755 | Ge _ => Or (f p, q) | Eq _ => Or (f p, q) |
|
756 | NEq _ => Or (f p, q) | Dvd (_, _) => Or (f p, q) |
|
757 | NDvd (_, _) => Or (f p, q) | Not _ => Or (f p, q) |
|
758 | And (_, _) => Or (f p, q) | Or (_, _) => Or (f p, q) |
|
759 | Imp (_, _) => Or (f p, q) | Iff (_, _) => Or (f p, q) |
|
760 | E _ => Or (f p, q) | A _ => Or (f p, q) |
|
761 | Closed _ => Or (f p, q) | NClosed _ => Or (f p, q)))); |
|
762 |
|
763 fun foldr f [] a = a |
|
764 | foldr f (x :: xs) a = f x (foldr f xs a); |
|
765 |
|
766 fun evaldjf f ps = foldr (djf f) ps F; |
|
767 |
|
768 fun dj f p = evaldjf f (disjuncts p); |
|
769 |
|
770 fun disj p q = |
|
771 (if eq_fm p T orelse eq_fm q T then T |
|
772 else (if eq_fm p F then q else (if eq_fm q F then p else Or (p, q)))); |
|
773 |
|
774 fun minus_nat n m = IntInf.max (0, (IntInf.- (n, m))); |
|
775 |
|
776 fun decrnum (Bound n) = Bound (minus_nat n (1 : IntInf.int)) |
|
777 | decrnum (Neg a) = Neg (decrnum a) |
|
778 | decrnum (Add (a, b)) = Add (decrnum a, decrnum b) |
|
779 | decrnum (Sub (a, b)) = Sub (decrnum a, decrnum b) |
|
780 | decrnum (Mul (c, a)) = Mul (c, decrnum a) |
|
781 | decrnum (Cn (n, i, a)) = Cn (minus_nat n (1 : IntInf.int), i, decrnum a) |
|
782 | decrnum (C u) = C u; |
|
783 |
|
784 fun decr (Lt a) = Lt (decrnum a) |
|
785 | decr (Le a) = Le (decrnum a) |
|
786 | decr (Gt a) = Gt (decrnum a) |
|
787 | decr (Ge a) = Ge (decrnum a) |
|
788 | decr (Eq a) = Eq (decrnum a) |
|
789 | decr (NEq a) = NEq (decrnum a) |
|
790 | decr (Dvd (i, a)) = Dvd (i, decrnum a) |
|
791 | decr (NDvd (i, a)) = NDvd (i, decrnum a) |
|
792 | decr (Not p) = Not (decr p) |
|
793 | decr (And (p, q)) = And (decr p, decr q) |
|
794 | decr (Or (p, q)) = Or (decr p, decr q) |
|
795 | decr (Imp (p, q)) = Imp (decr p, decr q) |
|
796 | decr (Iff (p, q)) = Iff (decr p, decr q) |
|
797 | decr T = T |
|
798 | decr F = F |
|
799 | decr (E ao) = E ao |
|
800 | decr (A ap) = A ap |
|
801 | decr (Closed aq) = Closed aq |
|
802 | decr (NClosed ar) = NClosed ar; |
|
803 |
|
804 fun concat_map f [] = [] |
|
805 | concat_map f (x :: xs) = append (f x) (concat_map f xs); |
|
806 |
|
807 fun numsubst0 t (C c) = C c |
|
808 | numsubst0 t (Bound n) = |
|
809 (if ((n : IntInf.int) = (0 : IntInf.int)) then t else Bound n) |
|
810 | numsubst0 t (Neg a) = Neg (numsubst0 t a) |
|
811 | numsubst0 t (Add (a, b)) = Add (numsubst0 t a, numsubst0 t b) |
|
812 | numsubst0 t (Sub (a, b)) = Sub (numsubst0 t a, numsubst0 t b) |
|
813 | numsubst0 t (Mul (i, a)) = Mul (i, numsubst0 t a) |
|
814 | numsubst0 t (Cn (v, i, a)) = |
|
815 (if ((v : IntInf.int) = (0 : IntInf.int)) |
|
816 then Add (Mul (i, t), numsubst0 t a) |
|
817 else Cn (suc (minus_nat v (1 : IntInf.int)), i, numsubst0 t a)); |
|
818 |
|
819 fun subst0 t T = T |
|
820 | subst0 t F = F |
|
821 | subst0 t (Lt a) = Lt (numsubst0 t a) |
|
822 | subst0 t (Le a) = Le (numsubst0 t a) |
|
823 | subst0 t (Gt a) = Gt (numsubst0 t a) |
|
824 | subst0 t (Ge a) = Ge (numsubst0 t a) |
|
825 | subst0 t (Eq a) = Eq (numsubst0 t a) |
|
826 | subst0 t (NEq a) = NEq (numsubst0 t a) |
|
827 | subst0 t (Dvd (i, a)) = Dvd (i, numsubst0 t a) |
|
828 | subst0 t (NDvd (i, a)) = NDvd (i, numsubst0 t a) |
|
829 | subst0 t (Not p) = Not (subst0 t p) |
|
830 | subst0 t (And (p, q)) = And (subst0 t p, subst0 t q) |
|
831 | subst0 t (Or (p, q)) = Or (subst0 t p, subst0 t q) |
|
832 | subst0 t (Imp (p, q)) = Imp (subst0 t p, subst0 t q) |
|
833 | subst0 t (Iff (p, q)) = Iff (subst0 t p, subst0 t q) |
|
834 | subst0 t (Closed p) = Closed p |
|
835 | subst0 t (NClosed p) = NClosed p; |
|
836 |
|
837 fun minusinf (And (p, q)) = And (minusinf p, minusinf q) |
|
838 | minusinf (Or (p, q)) = Or (minusinf p, minusinf q) |
|
839 | minusinf T = T |
|
840 | minusinf F = F |
|
841 | minusinf (Lt (C bo)) = Lt (C bo) |
|
842 | minusinf (Lt (Bound bp)) = Lt (Bound bp) |
|
843 | minusinf (Lt (Neg bt)) = Lt (Neg bt) |
|
844 | minusinf (Lt (Add (bu, bv))) = Lt (Add (bu, bv)) |
|
845 | minusinf (Lt (Sub (bw, bx))) = Lt (Sub (bw, bx)) |
|
846 | minusinf (Lt (Mul (by, bz))) = Lt (Mul (by, bz)) |
|
847 | minusinf (Le (C co)) = Le (C co) |
|
848 | minusinf (Le (Bound cp)) = Le (Bound cp) |
|
849 | minusinf (Le (Neg ct)) = Le (Neg ct) |
|
850 | minusinf (Le (Add (cu, cv))) = Le (Add (cu, cv)) |
|
851 | minusinf (Le (Sub (cw, cx))) = Le (Sub (cw, cx)) |
|
852 | minusinf (Le (Mul (cy, cz))) = Le (Mul (cy, cz)) |
|
853 | minusinf (Gt (C doa)) = Gt (C doa) |
|
854 | minusinf (Gt (Bound dp)) = Gt (Bound dp) |
|
855 | minusinf (Gt (Neg dt)) = Gt (Neg dt) |
|
856 | minusinf (Gt (Add (du, dv))) = Gt (Add (du, dv)) |
|
857 | minusinf (Gt (Sub (dw, dx))) = Gt (Sub (dw, dx)) |
|
858 | minusinf (Gt (Mul (dy, dz))) = Gt (Mul (dy, dz)) |
|
859 | minusinf (Ge (C eo)) = Ge (C eo) |
|
860 | minusinf (Ge (Bound ep)) = Ge (Bound ep) |
|
861 | minusinf (Ge (Neg et)) = Ge (Neg et) |
|
862 | minusinf (Ge (Add (eu, ev))) = Ge (Add (eu, ev)) |
|
863 | minusinf (Ge (Sub (ew, ex))) = Ge (Sub (ew, ex)) |
|
864 | minusinf (Ge (Mul (ey, ez))) = Ge (Mul (ey, ez)) |
|
865 | minusinf (Eq (C fo)) = Eq (C fo) |
|
866 | minusinf (Eq (Bound fp)) = Eq (Bound fp) |
|
867 | minusinf (Eq (Neg ft)) = Eq (Neg ft) |
|
868 | minusinf (Eq (Add (fu, fv))) = Eq (Add (fu, fv)) |
|
869 | minusinf (Eq (Sub (fw, fx))) = Eq (Sub (fw, fx)) |
|
870 | minusinf (Eq (Mul (fy, fz))) = Eq (Mul (fy, fz)) |
|
871 | minusinf (NEq (C go)) = NEq (C go) |
|
872 | minusinf (NEq (Bound gp)) = NEq (Bound gp) |
|
873 | minusinf (NEq (Neg gt)) = NEq (Neg gt) |
|
874 | minusinf (NEq (Add (gu, gv))) = NEq (Add (gu, gv)) |
|
875 | minusinf (NEq (Sub (gw, gx))) = NEq (Sub (gw, gx)) |
|
876 | minusinf (NEq (Mul (gy, gz))) = NEq (Mul (gy, gz)) |
|
877 | minusinf (Dvd (aa, ab)) = Dvd (aa, ab) |
|
878 | minusinf (NDvd (ac, ad)) = NDvd (ac, ad) |
|
879 | minusinf (Not ae) = Not ae |
|
880 | minusinf (Imp (aj, ak)) = Imp (aj, ak) |
|
881 | minusinf (Iff (al, am)) = Iff (al, am) |
|
882 | minusinf (E an) = E an |
|
883 | minusinf (A ao) = A ao |
|
884 | minusinf (Closed ap) = Closed ap |
|
885 | minusinf (NClosed aq) = NClosed aq |
|
886 | minusinf (Lt (Cn (cm, c, e))) = |
|
887 (if ((cm : IntInf.int) = (0 : IntInf.int)) then T |
|
888 else Lt (Cn (suc (minus_nat cm (1 : IntInf.int)), c, e))) |
|
889 | minusinf (Le (Cn (dm, c, e))) = |
|
890 (if ((dm : IntInf.int) = (0 : IntInf.int)) then T |
|
891 else Le (Cn (suc (minus_nat dm (1 : IntInf.int)), c, e))) |
|
892 | minusinf (Gt (Cn (em, c, e))) = |
|
893 (if ((em : IntInf.int) = (0 : IntInf.int)) then F |
|
894 else Gt (Cn (suc (minus_nat em (1 : IntInf.int)), c, e))) |
|
895 | minusinf (Ge (Cn (fm, c, e))) = |
|
896 (if ((fm : IntInf.int) = (0 : IntInf.int)) then F |
|
897 else Ge (Cn (suc (minus_nat fm (1 : IntInf.int)), c, e))) |
|
898 | minusinf (Eq (Cn (gm, c, e))) = |
|
899 (if ((gm : IntInf.int) = (0 : IntInf.int)) then F |
|
900 else Eq (Cn (suc (minus_nat gm (1 : IntInf.int)), c, e))) |
|
901 | minusinf (NEq (Cn (hm, c, e))) = |
|
902 (if ((hm : IntInf.int) = (0 : IntInf.int)) then T |
|
903 else NEq (Cn (suc (minus_nat hm (1 : IntInf.int)), c, e))); |
|
904 |
|
905 val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq; |
|
906 |
|
907 val zero_int : IntInf.int = (0 : IntInf.int); |
|
908 |
|
909 type 'a zero = {zero : 'a}; |
|
910 val zero = #zero : 'a zero -> 'a; |
|
911 |
|
912 val zero_inta = {zero = zero_int} : IntInf.int zero; |
|
913 |
|
914 type 'a times = {times : 'a -> 'a -> 'a}; |
|
915 val times = #times : 'a times -> 'a -> 'a -> 'a; |
|
916 |
|
917 type 'a no_zero_divisors = |
|
918 {times_no_zero_divisors : 'a times, zero_no_zero_divisors : 'a zero}; |
|
919 val times_no_zero_divisors = #times_no_zero_divisors : |
|
920 'a no_zero_divisors -> 'a times; |
|
921 val zero_no_zero_divisors = #zero_no_zero_divisors : |
|
922 'a no_zero_divisors -> 'a zero; |
|
923 |
|
924 val times_int = {times = (fn a => fn b => IntInf.* (a, b))} : IntInf.int times; |
|
925 |
|
926 val no_zero_divisors_int = |
|
927 {times_no_zero_divisors = times_int, zero_no_zero_divisors = zero_inta} : |
|
928 IntInf.int no_zero_divisors; |
|
929 |
|
930 type 'a one = {one : 'a}; |
|
931 val one = #one : 'a one -> 'a; |
|
932 |
|
933 type 'a zero_neq_one = {one_zero_neq_one : 'a one, zero_zero_neq_one : 'a zero}; |
|
934 val one_zero_neq_one = #one_zero_neq_one : 'a zero_neq_one -> 'a one; |
|
935 val zero_zero_neq_one = #zero_zero_neq_one : 'a zero_neq_one -> 'a zero; |
|
936 |
|
937 type 'a semigroup_mult = {times_semigroup_mult : 'a times}; |
|
938 val times_semigroup_mult = #times_semigroup_mult : |
|
939 'a semigroup_mult -> 'a times; |
|
940 |
|
941 type 'a plus = {plus : 'a -> 'a -> 'a}; |
|
942 val plus = #plus : 'a plus -> 'a -> 'a -> 'a; |
|
943 |
|
944 type 'a semigroup_add = {plus_semigroup_add : 'a plus}; |
|
945 val plus_semigroup_add = #plus_semigroup_add : 'a semigroup_add -> 'a plus; |
|
946 |
|
947 type 'a ab_semigroup_add = {semigroup_add_ab_semigroup_add : 'a semigroup_add}; |
|
948 val semigroup_add_ab_semigroup_add = #semigroup_add_ab_semigroup_add : |
|
949 'a ab_semigroup_add -> 'a semigroup_add; |
|
950 |
|
951 type 'a semiring = |
|
952 {ab_semigroup_add_semiring : 'a ab_semigroup_add, |
|
953 semigroup_mult_semiring : 'a semigroup_mult}; |
|
954 val ab_semigroup_add_semiring = #ab_semigroup_add_semiring : |
|
955 'a semiring -> 'a ab_semigroup_add; |
|
956 val semigroup_mult_semiring = #semigroup_mult_semiring : |
|
957 'a semiring -> 'a semigroup_mult; |
|
958 |
|
959 type 'a mult_zero = {times_mult_zero : 'a times, zero_mult_zero : 'a zero}; |
|
960 val times_mult_zero = #times_mult_zero : 'a mult_zero -> 'a times; |
|
961 val zero_mult_zero = #zero_mult_zero : 'a mult_zero -> 'a zero; |
|
962 |
|
963 type 'a monoid_add = |
|
964 {semigroup_add_monoid_add : 'a semigroup_add, zero_monoid_add : 'a zero}; |
|
965 val semigroup_add_monoid_add = #semigroup_add_monoid_add : |
|
966 'a monoid_add -> 'a semigroup_add; |
|
967 val zero_monoid_add = #zero_monoid_add : 'a monoid_add -> 'a zero; |
|
968 |
|
969 type 'a comm_monoid_add = |
|
970 {ab_semigroup_add_comm_monoid_add : 'a ab_semigroup_add, |
|
971 monoid_add_comm_monoid_add : 'a monoid_add}; |
|
972 val ab_semigroup_add_comm_monoid_add = #ab_semigroup_add_comm_monoid_add : |
|
973 'a comm_monoid_add -> 'a ab_semigroup_add; |
|
974 val monoid_add_comm_monoid_add = #monoid_add_comm_monoid_add : |
|
975 'a comm_monoid_add -> 'a monoid_add; |
|
976 |
|
977 type 'a semiring_0 = |
|
978 {comm_monoid_add_semiring_0 : 'a comm_monoid_add, |
|
979 mult_zero_semiring_0 : 'a mult_zero, semiring_semiring_0 : 'a semiring}; |
|
980 val comm_monoid_add_semiring_0 = #comm_monoid_add_semiring_0 : |
|
981 'a semiring_0 -> 'a comm_monoid_add; |
|
982 val mult_zero_semiring_0 = #mult_zero_semiring_0 : |
|
983 'a semiring_0 -> 'a mult_zero; |
|
984 val semiring_semiring_0 = #semiring_semiring_0 : 'a semiring_0 -> 'a semiring; |
|
985 |
|
986 type 'a power = {one_power : 'a one, times_power : 'a times}; |
|
987 val one_power = #one_power : 'a power -> 'a one; |
|
988 val times_power = #times_power : 'a power -> 'a times; |
|
989 |
|
990 type 'a monoid_mult = |
|
991 {semigroup_mult_monoid_mult : 'a semigroup_mult, |
|
992 power_monoid_mult : 'a power}; |
|
993 val semigroup_mult_monoid_mult = #semigroup_mult_monoid_mult : |
|
994 'a monoid_mult -> 'a semigroup_mult; |
|
995 val power_monoid_mult = #power_monoid_mult : 'a monoid_mult -> 'a power; |
|
996 |
|
997 type 'a semiring_1 = |
|
998 {monoid_mult_semiring_1 : 'a monoid_mult, |
|
999 semiring_0_semiring_1 : 'a semiring_0, |
|
1000 zero_neq_one_semiring_1 : 'a zero_neq_one}; |
|
1001 val monoid_mult_semiring_1 = #monoid_mult_semiring_1 : |
|
1002 'a semiring_1 -> 'a monoid_mult; |
|
1003 val semiring_0_semiring_1 = #semiring_0_semiring_1 : |
|
1004 'a semiring_1 -> 'a semiring_0; |
|
1005 val zero_neq_one_semiring_1 = #zero_neq_one_semiring_1 : |
|
1006 'a semiring_1 -> 'a zero_neq_one; |
|
1007 |
|
1008 type 'a cancel_semigroup_add = |
|
1009 {semigroup_add_cancel_semigroup_add : 'a semigroup_add}; |
|
1010 val semigroup_add_cancel_semigroup_add = #semigroup_add_cancel_semigroup_add : |
|
1011 'a cancel_semigroup_add -> 'a semigroup_add; |
|
1012 |
|
1013 type 'a cancel_ab_semigroup_add = |
|
1014 {ab_semigroup_add_cancel_ab_semigroup_add : 'a ab_semigroup_add, |
|
1015 cancel_semigroup_add_cancel_ab_semigroup_add : 'a cancel_semigroup_add}; |
|
1016 val ab_semigroup_add_cancel_ab_semigroup_add = |
|
1017 #ab_semigroup_add_cancel_ab_semigroup_add : |
|
1018 'a cancel_ab_semigroup_add -> 'a ab_semigroup_add; |
|
1019 val cancel_semigroup_add_cancel_ab_semigroup_add = |
|
1020 #cancel_semigroup_add_cancel_ab_semigroup_add : |
|
1021 'a cancel_ab_semigroup_add -> 'a cancel_semigroup_add; |
|
1022 |
|
1023 type 'a cancel_comm_monoid_add = |
|
1024 {cancel_ab_semigroup_add_cancel_comm_monoid_add : 'a cancel_ab_semigroup_add, |
|
1025 comm_monoid_add_cancel_comm_monoid_add : 'a comm_monoid_add}; |
|
1026 val cancel_ab_semigroup_add_cancel_comm_monoid_add = |
|
1027 #cancel_ab_semigroup_add_cancel_comm_monoid_add : |
|
1028 'a cancel_comm_monoid_add -> 'a cancel_ab_semigroup_add; |
|
1029 val comm_monoid_add_cancel_comm_monoid_add = |
|
1030 #comm_monoid_add_cancel_comm_monoid_add : |
|
1031 'a cancel_comm_monoid_add -> 'a comm_monoid_add; |
|
1032 |
|
1033 type 'a semiring_0_cancel = |
|
1034 {cancel_comm_monoid_add_semiring_0_cancel : 'a cancel_comm_monoid_add, |
|
1035 semiring_0_semiring_0_cancel : 'a semiring_0}; |
|
1036 val cancel_comm_monoid_add_semiring_0_cancel = |
|
1037 #cancel_comm_monoid_add_semiring_0_cancel : |
|
1038 'a semiring_0_cancel -> 'a cancel_comm_monoid_add; |
|
1039 val semiring_0_semiring_0_cancel = #semiring_0_semiring_0_cancel : |
|
1040 'a semiring_0_cancel -> 'a semiring_0; |
|
1041 |
|
1042 type 'a semiring_1_cancel = |
|
1043 {semiring_0_cancel_semiring_1_cancel : 'a semiring_0_cancel, |
|
1044 semiring_1_semiring_1_cancel : 'a semiring_1}; |
|
1045 val semiring_0_cancel_semiring_1_cancel = #semiring_0_cancel_semiring_1_cancel : |
|
1046 'a semiring_1_cancel -> 'a semiring_0_cancel; |
|
1047 val semiring_1_semiring_1_cancel = #semiring_1_semiring_1_cancel : |
|
1048 'a semiring_1_cancel -> 'a semiring_1; |
|
1049 |
|
1050 type 'a dvd = {times_dvd : 'a times}; |
|
1051 val times_dvd = #times_dvd : 'a dvd -> 'a times; |
|
1052 |
|
1053 type 'a ab_semigroup_mult = |
|
1054 {semigroup_mult_ab_semigroup_mult : 'a semigroup_mult}; |
|
1055 val semigroup_mult_ab_semigroup_mult = #semigroup_mult_ab_semigroup_mult : |
|
1056 'a ab_semigroup_mult -> 'a semigroup_mult; |
|
1057 |
|
1058 type 'a comm_semiring = |
|
1059 {ab_semigroup_mult_comm_semiring : 'a ab_semigroup_mult, |
|
1060 semiring_comm_semiring : 'a semiring}; |
|
1061 val ab_semigroup_mult_comm_semiring = #ab_semigroup_mult_comm_semiring : |
|
1062 'a comm_semiring -> 'a ab_semigroup_mult; |
|
1063 val semiring_comm_semiring = #semiring_comm_semiring : |
|
1064 'a comm_semiring -> 'a semiring; |
|
1065 |
|
1066 type 'a comm_semiring_0 = |
|
1067 {comm_semiring_comm_semiring_0 : 'a comm_semiring, |
|
1068 semiring_0_comm_semiring_0 : 'a semiring_0}; |
|
1069 val comm_semiring_comm_semiring_0 = #comm_semiring_comm_semiring_0 : |
|
1070 'a comm_semiring_0 -> 'a comm_semiring; |
|
1071 val semiring_0_comm_semiring_0 = #semiring_0_comm_semiring_0 : |
|
1072 'a comm_semiring_0 -> 'a semiring_0; |
|
1073 |
|
1074 type 'a comm_monoid_mult = |
|
1075 {ab_semigroup_mult_comm_monoid_mult : 'a ab_semigroup_mult, |
|
1076 monoid_mult_comm_monoid_mult : 'a monoid_mult}; |
|
1077 val ab_semigroup_mult_comm_monoid_mult = #ab_semigroup_mult_comm_monoid_mult : |
|
1078 'a comm_monoid_mult -> 'a ab_semigroup_mult; |
|
1079 val monoid_mult_comm_monoid_mult = #monoid_mult_comm_monoid_mult : |
|
1080 'a comm_monoid_mult -> 'a monoid_mult; |
|
1081 |
|
1082 type 'a comm_semiring_1 = |
|
1083 {comm_monoid_mult_comm_semiring_1 : 'a comm_monoid_mult, |
|
1084 comm_semiring_0_comm_semiring_1 : 'a comm_semiring_0, |
|
1085 dvd_comm_semiring_1 : 'a dvd, semiring_1_comm_semiring_1 : 'a semiring_1}; |
|
1086 val comm_monoid_mult_comm_semiring_1 = #comm_monoid_mult_comm_semiring_1 : |
|
1087 'a comm_semiring_1 -> 'a comm_monoid_mult; |
|
1088 val comm_semiring_0_comm_semiring_1 = #comm_semiring_0_comm_semiring_1 : |
|
1089 'a comm_semiring_1 -> 'a comm_semiring_0; |
|
1090 val dvd_comm_semiring_1 = #dvd_comm_semiring_1 : 'a comm_semiring_1 -> 'a dvd; |
|
1091 val semiring_1_comm_semiring_1 = #semiring_1_comm_semiring_1 : |
|
1092 'a comm_semiring_1 -> 'a semiring_1; |
|
1093 |
|
1094 type 'a comm_semiring_0_cancel = |
|
1095 {comm_semiring_0_comm_semiring_0_cancel : 'a comm_semiring_0, |
|
1096 semiring_0_cancel_comm_semiring_0_cancel : 'a semiring_0_cancel}; |
|
1097 val comm_semiring_0_comm_semiring_0_cancel = |
|
1098 #comm_semiring_0_comm_semiring_0_cancel : |
|
1099 'a comm_semiring_0_cancel -> 'a comm_semiring_0; |
|
1100 val semiring_0_cancel_comm_semiring_0_cancel = |
|
1101 #semiring_0_cancel_comm_semiring_0_cancel : |
|
1102 'a comm_semiring_0_cancel -> 'a semiring_0_cancel; |
|
1103 |
|
1104 type 'a comm_semiring_1_cancel = |
|
1105 {comm_semiring_0_cancel_comm_semiring_1_cancel : 'a comm_semiring_0_cancel, |
|
1106 comm_semiring_1_comm_semiring_1_cancel : 'a comm_semiring_1, |
|
1107 semiring_1_cancel_comm_semiring_1_cancel : 'a semiring_1_cancel}; |
|
1108 val comm_semiring_0_cancel_comm_semiring_1_cancel = |
|
1109 #comm_semiring_0_cancel_comm_semiring_1_cancel : |
|
1110 'a comm_semiring_1_cancel -> 'a comm_semiring_0_cancel; |
|
1111 val comm_semiring_1_comm_semiring_1_cancel = |
|
1112 #comm_semiring_1_comm_semiring_1_cancel : |
|
1113 'a comm_semiring_1_cancel -> 'a comm_semiring_1; |
|
1114 val semiring_1_cancel_comm_semiring_1_cancel = |
|
1115 #semiring_1_cancel_comm_semiring_1_cancel : |
|
1116 'a comm_semiring_1_cancel -> 'a semiring_1_cancel; |
|
1117 |
|
1118 type 'a diva = {dvd_div : 'a dvd, diva : 'a -> 'a -> 'a, moda : 'a -> 'a -> 'a}; |
|
1119 val dvd_div = #dvd_div : 'a diva -> 'a dvd; |
|
1120 val diva = #diva : 'a diva -> 'a -> 'a -> 'a; |
|
1121 val moda = #moda : 'a diva -> 'a -> 'a -> 'a; |
|
1122 |
|
1123 type 'a semiring_div = |
|
1124 {div_semiring_div : 'a diva, |
|
1125 comm_semiring_1_cancel_semiring_div : 'a comm_semiring_1_cancel, |
|
1126 no_zero_divisors_semiring_div : 'a no_zero_divisors}; |
|
1127 val div_semiring_div = #div_semiring_div : 'a semiring_div -> 'a diva; |
|
1128 val comm_semiring_1_cancel_semiring_div = #comm_semiring_1_cancel_semiring_div : |
|
1129 'a semiring_div -> 'a comm_semiring_1_cancel; |
|
1130 val no_zero_divisors_semiring_div = #no_zero_divisors_semiring_div : |
|
1131 'a semiring_div -> 'a no_zero_divisors; |
|
1132 |
|
1133 val one_int : IntInf.int = (1 : IntInf.int); |
|
1134 |
|
1135 val one_inta = {one = one_int} : IntInf.int one; |
|
1136 |
|
1137 val zero_neq_one_int = |
|
1138 {one_zero_neq_one = one_inta, zero_zero_neq_one = zero_inta} : |
|
1139 IntInf.int zero_neq_one; |
|
1140 |
|
1141 val semigroup_mult_int = {times_semigroup_mult = times_int} : |
|
1142 IntInf.int semigroup_mult; |
|
1143 |
|
1144 val plus_int = {plus = (fn a => fn b => IntInf.+ (a, b))} : IntInf.int plus; |
|
1145 |
|
1146 val semigroup_add_int = {plus_semigroup_add = plus_int} : |
|
1147 IntInf.int semigroup_add; |
|
1148 |
|
1149 val ab_semigroup_add_int = {semigroup_add_ab_semigroup_add = semigroup_add_int} |
|
1150 : IntInf.int ab_semigroup_add; |
|
1151 |
|
1152 val semiring_int = |
|
1153 {ab_semigroup_add_semiring = ab_semigroup_add_int, |
|
1154 semigroup_mult_semiring = semigroup_mult_int} |
|
1155 : IntInf.int semiring; |
|
1156 |
|
1157 val mult_zero_int = {times_mult_zero = times_int, zero_mult_zero = zero_inta} : |
|
1158 IntInf.int mult_zero; |
|
1159 |
|
1160 val monoid_add_int = |
|
1161 {semigroup_add_monoid_add = semigroup_add_int, zero_monoid_add = zero_inta} : |
|
1162 IntInf.int monoid_add; |
|
1163 |
|
1164 val comm_monoid_add_int = |
|
1165 {ab_semigroup_add_comm_monoid_add = ab_semigroup_add_int, |
|
1166 monoid_add_comm_monoid_add = monoid_add_int} |
|
1167 : IntInf.int comm_monoid_add; |
|
1168 |
|
1169 val semiring_0_int = |
|
1170 {comm_monoid_add_semiring_0 = comm_monoid_add_int, |
|
1171 mult_zero_semiring_0 = mult_zero_int, semiring_semiring_0 = semiring_int} |
|
1172 : IntInf.int semiring_0; |
|
1173 |
|
1174 val power_int = {one_power = one_inta, times_power = times_int} : |
|
1175 IntInf.int power; |
|
1176 |
|
1177 val monoid_mult_int = |
|
1178 {semigroup_mult_monoid_mult = semigroup_mult_int, |
|
1179 power_monoid_mult = power_int} |
|
1180 : IntInf.int monoid_mult; |
|
1181 |
|
1182 val semiring_1_int = |
|
1183 {monoid_mult_semiring_1 = monoid_mult_int, |
|
1184 semiring_0_semiring_1 = semiring_0_int, |
|
1185 zero_neq_one_semiring_1 = zero_neq_one_int} |
|
1186 : IntInf.int semiring_1; |
|
1187 |
|
1188 val cancel_semigroup_add_int = |
|
1189 {semigroup_add_cancel_semigroup_add = semigroup_add_int} : |
|
1190 IntInf.int cancel_semigroup_add; |
|
1191 |
|
1192 val cancel_ab_semigroup_add_int = |
|
1193 {ab_semigroup_add_cancel_ab_semigroup_add = ab_semigroup_add_int, |
|
1194 cancel_semigroup_add_cancel_ab_semigroup_add = cancel_semigroup_add_int} |
|
1195 : IntInf.int cancel_ab_semigroup_add; |
|
1196 |
|
1197 val cancel_comm_monoid_add_int = |
|
1198 {cancel_ab_semigroup_add_cancel_comm_monoid_add = cancel_ab_semigroup_add_int, |
|
1199 comm_monoid_add_cancel_comm_monoid_add = comm_monoid_add_int} |
|
1200 : IntInf.int cancel_comm_monoid_add; |
|
1201 |
|
1202 val semiring_0_cancel_int = |
|
1203 {cancel_comm_monoid_add_semiring_0_cancel = cancel_comm_monoid_add_int, |
|
1204 semiring_0_semiring_0_cancel = semiring_0_int} |
|
1205 : IntInf.int semiring_0_cancel; |
|
1206 |
|
1207 val semiring_1_cancel_int = |
|
1208 {semiring_0_cancel_semiring_1_cancel = semiring_0_cancel_int, |
|
1209 semiring_1_semiring_1_cancel = semiring_1_int} |
|
1210 : IntInf.int semiring_1_cancel; |
|
1211 |
|
1212 val dvd_int = {times_dvd = times_int} : IntInf.int dvd; |
|
1213 |
|
1214 val ab_semigroup_mult_int = |
|
1215 {semigroup_mult_ab_semigroup_mult = semigroup_mult_int} : |
|
1216 IntInf.int ab_semigroup_mult; |
|
1217 |
|
1218 val comm_semiring_int = |
|
1219 {ab_semigroup_mult_comm_semiring = ab_semigroup_mult_int, |
|
1220 semiring_comm_semiring = semiring_int} |
|
1221 : IntInf.int comm_semiring; |
|
1222 |
|
1223 val comm_semiring_0_int = |
|
1224 {comm_semiring_comm_semiring_0 = comm_semiring_int, |
|
1225 semiring_0_comm_semiring_0 = semiring_0_int} |
|
1226 : IntInf.int comm_semiring_0; |
|
1227 |
|
1228 val comm_monoid_mult_int = |
|
1229 {ab_semigroup_mult_comm_monoid_mult = ab_semigroup_mult_int, |
|
1230 monoid_mult_comm_monoid_mult = monoid_mult_int} |
|
1231 : IntInf.int comm_monoid_mult; |
|
1232 |
|
1233 val comm_semiring_1_int = |
|
1234 {comm_monoid_mult_comm_semiring_1 = comm_monoid_mult_int, |
|
1235 comm_semiring_0_comm_semiring_1 = comm_semiring_0_int, |
|
1236 dvd_comm_semiring_1 = dvd_int, semiring_1_comm_semiring_1 = semiring_1_int} |
|
1237 : IntInf.int comm_semiring_1; |
|
1238 |
|
1239 val comm_semiring_0_cancel_int = |
|
1240 {comm_semiring_0_comm_semiring_0_cancel = comm_semiring_0_int, |
|
1241 semiring_0_cancel_comm_semiring_0_cancel = semiring_0_cancel_int} |
|
1242 : IntInf.int comm_semiring_0_cancel; |
|
1243 |
|
1244 val comm_semiring_1_cancel_int = |
|
1245 {comm_semiring_0_cancel_comm_semiring_1_cancel = comm_semiring_0_cancel_int, |
|
1246 comm_semiring_1_comm_semiring_1_cancel = comm_semiring_1_int, |
|
1247 semiring_1_cancel_comm_semiring_1_cancel = semiring_1_cancel_int} |
|
1248 : IntInf.int comm_semiring_1_cancel; |
|
1249 |
|
1250 fun abs_int i = (if IntInf.< (i, (0 : IntInf.int)) then IntInf.~ i else i); |
|
1251 |
|
1252 fun split f (a, b) = f a b; |
|
1253 |
|
1254 fun sgn_int i = |
|
1255 (if ((i : IntInf.int) = (0 : IntInf.int)) then (0 : IntInf.int) |
|
1256 else (if IntInf.< ((0 : IntInf.int), i) then (1 : IntInf.int) |
|
1257 else IntInf.~ (1 : IntInf.int))); |
|
1258 |
|
1259 fun apsnd f (x, y) = (x, f y); |
|
1260 |
|
1261 fun divmod_int k l = |
|
1262 (if ((k : IntInf.int) = (0 : IntInf.int)) |
|
1263 then ((0 : IntInf.int), (0 : IntInf.int)) |
|
1264 else (if ((l : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), k) |
|
1265 else apsnd (fn a => IntInf.* (sgn_int l, a)) |
|
1266 (if (((sgn_int k) : IntInf.int) = (sgn_int l)) |
|
1267 then IntInf.divMod (IntInf.abs k, IntInf.abs l) |
|
1268 else let |
|
1269 val (r, s) = |
|
1270 IntInf.divMod (IntInf.abs k, IntInf.abs l); |
|
1271 in |
|
1272 (if ((s : IntInf.int) = (0 : IntInf.int)) |
|
1273 then (IntInf.~ r, (0 : IntInf.int)) |
|
1274 else (IntInf.- (IntInf.~ r, (1 : IntInf.int)), |
|
1275 IntInf.- (abs_int l, s))) |
|
1276 end))); |
|
1277 |
|
1278 fun snd (a, b) = b; |
|
1279 |
|
1280 fun mod_int a b = snd (divmod_int a b); |
|
1281 |
|
1282 fun fst (a, b) = a; |
|
1283 |
|
1284 fun div_int a b = fst (divmod_int a b); |
|
1285 |
|
1286 val div_inta = {dvd_div = dvd_int, diva = div_int, moda = mod_int} : |
|
1287 IntInf.int diva; |
|
1288 |
|
1289 val semiring_div_int = |
|
1290 {div_semiring_div = div_inta, |
|
1291 comm_semiring_1_cancel_semiring_div = comm_semiring_1_cancel_int, |
|
1292 no_zero_divisors_semiring_div = no_zero_divisors_int} |
|
1293 : IntInf.int semiring_div; |
|
1294 |
|
1295 fun dvd (A1_, A2_) a b = |
|
1296 eqa A2_ (moda (div_semiring_div A1_) b a) |
|
1297 (zero ((zero_no_zero_divisors o no_zero_divisors_semiring_div) A1_)); |
|
1298 |
|
1299 fun num_case f1 f2 f3 f4 f5 f6 f7 (Mul (inta, num)) = f7 inta num |
|
1300 | num_case f1 f2 f3 f4 f5 f6 f7 (Sub (num1, num2)) = f6 num1 num2 |
|
1301 | num_case f1 f2 f3 f4 f5 f6 f7 (Add (num1, num2)) = f5 num1 num2 |
|
1302 | num_case f1 f2 f3 f4 f5 f6 f7 (Neg num) = f4 num |
|
1303 | num_case f1 f2 f3 f4 f5 f6 f7 (Cn (nat, inta, num)) = f3 nat inta num |
|
1304 | num_case f1 f2 f3 f4 f5 f6 f7 (Bound nat) = f2 nat |
|
1305 | num_case f1 f2 f3 f4 f5 f6 f7 (C inta) = f1 inta; |
|
1306 |
|
1307 fun nummul i (C j) = C (IntInf.* (i, j)) |
|
1308 | nummul i (Cn (n, c, t)) = Cn (n, IntInf.* (c, i), nummul i t) |
|
1309 | nummul i (Bound v) = Mul (i, Bound v) |
|
1310 | nummul i (Neg v) = Mul (i, Neg v) |
|
1311 | nummul i (Add (v, va)) = Mul (i, Add (v, va)) |
|
1312 | nummul i (Sub (v, va)) = Mul (i, Sub (v, va)) |
|
1313 | nummul i (Mul (v, va)) = Mul (i, Mul (v, va)); |
|
1314 |
|
1315 fun numneg t = nummul (IntInf.~ (1 : IntInf.int)) t; |
|
1316 |
|
1317 fun numadd (Cn (n1, c1, r1), Cn (n2, c2, r2)) = |
|
1318 (if ((n1 : IntInf.int) = n2) |
|
1319 then let |
|
1320 val c = IntInf.+ (c1, c2); |
|
1321 in |
|
1322 (if ((c : IntInf.int) = (0 : IntInf.int)) then numadd (r1, r2) |
|
1323 else Cn (n1, c, numadd (r1, r2))) |
|
1324 end |
|
1325 else (if IntInf.<= (n1, n2) |
|
1326 then Cn (n1, c1, numadd (r1, Add (Mul (c2, Bound n2), r2))) |
|
1327 else Cn (n2, c2, numadd (Add (Mul (c1, Bound n1), r1), r2)))) |
|
1328 | numadd (Cn (n1, c1, r1), C dd) = Cn (n1, c1, numadd (r1, C dd)) |
|
1329 | numadd (Cn (n1, c1, r1), Bound de) = Cn (n1, c1, numadd (r1, Bound de)) |
|
1330 | numadd (Cn (n1, c1, r1), Neg di) = Cn (n1, c1, numadd (r1, Neg di)) |
|
1331 | numadd (Cn (n1, c1, r1), Add (dj, dk)) = |
|
1332 Cn (n1, c1, numadd (r1, Add (dj, dk))) |
|
1333 | numadd (Cn (n1, c1, r1), Sub (dl, dm)) = |
|
1334 Cn (n1, c1, numadd (r1, Sub (dl, dm))) |
|
1335 | numadd (Cn (n1, c1, r1), Mul (dn, doa)) = |
|
1336 Cn (n1, c1, numadd (r1, Mul (dn, doa))) |
|
1337 | numadd (C w, Cn (n2, c2, r2)) = Cn (n2, c2, numadd (C w, r2)) |
|
1338 | numadd (Bound x, Cn (n2, c2, r2)) = Cn (n2, c2, numadd (Bound x, r2)) |
|
1339 | numadd (Neg ac, Cn (n2, c2, r2)) = Cn (n2, c2, numadd (Neg ac, r2)) |
|
1340 | numadd (Add (ad, ae), Cn (n2, c2, r2)) = |
|
1341 Cn (n2, c2, numadd (Add (ad, ae), r2)) |
|
1342 | numadd (Sub (af, ag), Cn (n2, c2, r2)) = |
|
1343 Cn (n2, c2, numadd (Sub (af, ag), r2)) |
|
1344 | numadd (Mul (ah, ai), Cn (n2, c2, r2)) = |
|
1345 Cn (n2, c2, numadd (Mul (ah, ai), r2)) |
|
1346 | numadd (C b1, C b2) = C (IntInf.+ (b1, b2)) |
|
1347 | numadd (C aj, Bound bi) = Add (C aj, Bound bi) |
|
1348 | numadd (C aj, Neg bm) = Add (C aj, Neg bm) |
|
1349 | numadd (C aj, Add (bn, bo)) = Add (C aj, Add (bn, bo)) |
|
1350 | numadd (C aj, Sub (bp, bq)) = Add (C aj, Sub (bp, bq)) |
|
1351 | numadd (C aj, Mul (br, bs)) = Add (C aj, Mul (br, bs)) |
|
1352 | numadd (Bound ak, C cf) = Add (Bound ak, C cf) |
|
1353 | numadd (Bound ak, Bound cg) = Add (Bound ak, Bound cg) |
|
1354 | numadd (Bound ak, Neg ck) = Add (Bound ak, Neg ck) |
|
1355 | numadd (Bound ak, Add (cl, cm)) = Add (Bound ak, Add (cl, cm)) |
|
1356 | numadd (Bound ak, Sub (cn, co)) = Add (Bound ak, Sub (cn, co)) |
|
1357 | numadd (Bound ak, Mul (cp, cq)) = Add (Bound ak, Mul (cp, cq)) |
|
1358 | numadd (Neg ao, C en) = Add (Neg ao, C en) |
|
1359 | numadd (Neg ao, Bound eo) = Add (Neg ao, Bound eo) |
|
1360 | numadd (Neg ao, Neg es) = Add (Neg ao, Neg es) |
|
1361 | numadd (Neg ao, Add (et, eu)) = Add (Neg ao, Add (et, eu)) |
|
1362 | numadd (Neg ao, Sub (ev, ew)) = Add (Neg ao, Sub (ev, ew)) |
|
1363 | numadd (Neg ao, Mul (ex, ey)) = Add (Neg ao, Mul (ex, ey)) |
|
1364 | numadd (Add (ap, aq), C fl) = Add (Add (ap, aq), C fl) |
|
1365 | numadd (Add (ap, aq), Bound fm) = Add (Add (ap, aq), Bound fm) |
|
1366 | numadd (Add (ap, aq), Neg fq) = Add (Add (ap, aq), Neg fq) |
|
1367 | numadd (Add (ap, aq), Add (fr, fs)) = Add (Add (ap, aq), Add (fr, fs)) |
|
1368 | numadd (Add (ap, aq), Sub (ft, fu)) = Add (Add (ap, aq), Sub (ft, fu)) |
|
1369 | numadd (Add (ap, aq), Mul (fv, fw)) = Add (Add (ap, aq), Mul (fv, fw)) |
|
1370 | numadd (Sub (ar, asa), C gj) = Add (Sub (ar, asa), C gj) |
|
1371 | numadd (Sub (ar, asa), Bound gk) = Add (Sub (ar, asa), Bound gk) |
|
1372 | numadd (Sub (ar, asa), Neg go) = Add (Sub (ar, asa), Neg go) |
|
1373 | numadd (Sub (ar, asa), Add (gp, gq)) = Add (Sub (ar, asa), Add (gp, gq)) |
|
1374 | numadd (Sub (ar, asa), Sub (gr, gs)) = Add (Sub (ar, asa), Sub (gr, gs)) |
|
1375 | numadd (Sub (ar, asa), Mul (gt, gu)) = Add (Sub (ar, asa), Mul (gt, gu)) |
|
1376 | numadd (Mul (at, au), C hh) = Add (Mul (at, au), C hh) |
|
1377 | numadd (Mul (at, au), Bound hi) = Add (Mul (at, au), Bound hi) |
|
1378 | numadd (Mul (at, au), Neg hm) = Add (Mul (at, au), Neg hm) |
|
1379 | numadd (Mul (at, au), Add (hn, ho)) = Add (Mul (at, au), Add (hn, ho)) |
|
1380 | numadd (Mul (at, au), Sub (hp, hq)) = Add (Mul (at, au), Sub (hp, hq)) |
|
1381 | numadd (Mul (at, au), Mul (hr, hs)) = Add (Mul (at, au), Mul (hr, hs)); |
|
1382 |
|
1383 fun numsub s t = |
|
1384 (if eq_num s t then C (0 : IntInf.int) else numadd (s, numneg t)); |
|
1385 |
|
1386 fun simpnum (C j) = C j |
|
1387 | simpnum (Bound n) = Cn (n, (1 : IntInf.int), C (0 : IntInf.int)) |
|
1388 | simpnum (Neg t) = numneg (simpnum t) |
|
1389 | simpnum (Add (t, s)) = numadd (simpnum t, simpnum s) |
|
1390 | simpnum (Sub (t, s)) = numsub (simpnum t) (simpnum s) |
|
1391 | simpnum (Mul (i, t)) = |
|
1392 (if ((i : IntInf.int) = (0 : IntInf.int)) then C (0 : IntInf.int) |
|
1393 else nummul i (simpnum t)) |
|
1394 | simpnum (Cn (v, va, vb)) = Cn (v, va, vb); |
|
1395 |
|
1396 fun nota (Not p) = p |
|
1397 | nota T = F |
|
1398 | nota F = T |
|
1399 | nota (Lt v) = Not (Lt v) |
|
1400 | nota (Le v) = Not (Le v) |
|
1401 | nota (Gt v) = Not (Gt v) |
|
1402 | nota (Ge v) = Not (Ge v) |
|
1403 | nota (Eq v) = Not (Eq v) |
|
1404 | nota (NEq v) = Not (NEq v) |
|
1405 | nota (Dvd (v, va)) = Not (Dvd (v, va)) |
|
1406 | nota (NDvd (v, va)) = Not (NDvd (v, va)) |
|
1407 | nota (And (v, va)) = Not (And (v, va)) |
|
1408 | nota (Or (v, va)) = Not (Or (v, va)) |
|
1409 | nota (Imp (v, va)) = Not (Imp (v, va)) |
|
1410 | nota (Iff (v, va)) = Not (Iff (v, va)) |
|
1411 | nota (E v) = Not (E v) |
|
1412 | nota (A v) = Not (A v) |
|
1413 | nota (Closed v) = Not (Closed v) |
|
1414 | nota (NClosed v) = Not (NClosed v); |
|
1415 |
|
1416 fun iffa p q = |
|
1417 (if eq_fm p q then T |
|
1418 else (if eq_fm p (nota q) orelse eq_fm (nota p) q then F |
|
1419 else (if eq_fm p F then nota q |
|
1420 else (if eq_fm q F then nota p |
|
1421 else (if eq_fm p T then q |
|
1422 else (if eq_fm q T then p else Iff (p, q))))))); |
|
1423 |
|
1424 fun impa p q = |
|
1425 (if eq_fm p F orelse eq_fm q T then T |
|
1426 else (if eq_fm p T then q else (if eq_fm q F then nota p else Imp (p, q)))); |
|
1427 |
|
1428 fun conj p q = |
|
1429 (if eq_fm p F orelse eq_fm q F then F |
|
1430 else (if eq_fm p T then q else (if eq_fm q T then p else And (p, q)))); |
|
1431 |
|
1432 fun simpfm (And (p, q)) = conj (simpfm p) (simpfm q) |
|
1433 | simpfm (Or (p, q)) = disj (simpfm p) (simpfm q) |
|
1434 | simpfm (Imp (p, q)) = impa (simpfm p) (simpfm q) |
|
1435 | simpfm (Iff (p, q)) = iffa (simpfm p) (simpfm q) |
|
1436 | simpfm (Not p) = nota (simpfm p) |
|
1437 | simpfm (Lt a) = |
|
1438 let |
|
1439 val aa = simpnum a; |
|
1440 in |
|
1441 (case aa of C v => (if IntInf.< (v, (0 : IntInf.int)) then T else F) |
|
1442 | Bound _ => Lt aa | Cn (_, _, _) => Lt aa | Neg _ => Lt aa |
|
1443 | Add (_, _) => Lt aa | Sub (_, _) => Lt aa | Mul (_, _) => Lt aa) |
|
1444 end |
|
1445 | simpfm (Le a) = |
|
1446 let |
|
1447 val aa = simpnum a; |
|
1448 in |
|
1449 (case aa of C v => (if IntInf.<= (v, (0 : IntInf.int)) then T else F) |
|
1450 | Bound _ => Le aa | Cn (_, _, _) => Le aa | Neg _ => Le aa |
|
1451 | Add (_, _) => Le aa | Sub (_, _) => Le aa | Mul (_, _) => Le aa) |
|
1452 end |
|
1453 | simpfm (Gt a) = |
|
1454 let |
|
1455 val aa = simpnum a; |
|
1456 in |
|
1457 (case aa of C v => (if IntInf.< ((0 : IntInf.int), v) then T else F) |
|
1458 | Bound _ => Gt aa | Cn (_, _, _) => Gt aa | Neg _ => Gt aa |
|
1459 | Add (_, _) => Gt aa | Sub (_, _) => Gt aa | Mul (_, _) => Gt aa) |
|
1460 end |
|
1461 | simpfm (Ge a) = |
|
1462 let |
|
1463 val aa = simpnum a; |
|
1464 in |
|
1465 (case aa of C v => (if IntInf.<= ((0 : IntInf.int), v) then T else F) |
|
1466 | Bound _ => Ge aa | Cn (_, _, _) => Ge aa | Neg _ => Ge aa |
|
1467 | Add (_, _) => Ge aa | Sub (_, _) => Ge aa | Mul (_, _) => Ge aa) |
|
1468 end |
|
1469 | simpfm (Eq a) = |
|
1470 let |
|
1471 val aa = simpnum a; |
|
1472 in |
|
1473 (case aa |
|
1474 of C v => (if ((v : IntInf.int) = (0 : IntInf.int)) then T else F) |
|
1475 | Bound _ => Eq aa | Cn (_, _, _) => Eq aa | Neg _ => Eq aa |
|
1476 | Add (_, _) => Eq aa | Sub (_, _) => Eq aa | Mul (_, _) => Eq aa) |
|
1477 end |
|
1478 | simpfm (NEq a) = |
|
1479 let |
|
1480 val aa = simpnum a; |
|
1481 in |
|
1482 (case aa |
|
1483 of C v => (if not ((v : IntInf.int) = (0 : IntInf.int)) then T else F) |
|
1484 | Bound _ => NEq aa | Cn (_, _, _) => NEq aa | Neg _ => NEq aa |
|
1485 | Add (_, _) => NEq aa | Sub (_, _) => NEq aa | Mul (_, _) => NEq aa) |
|
1486 end |
|
1487 | simpfm (Dvd (i, a)) = |
|
1488 (if ((i : IntInf.int) = (0 : IntInf.int)) then simpfm (Eq a) |
|
1489 else (if (((abs_int i) : IntInf.int) = (1 : IntInf.int)) then T |
|
1490 else let |
|
1491 val aa = simpnum a; |
|
1492 in |
|
1493 (case aa |
|
1494 of C v => |
|
1495 (if dvd (semiring_div_int, eq_int) i v then T else F) |
|
1496 | Bound _ => Dvd (i, aa) | Cn (_, _, _) => Dvd (i, aa) |
|
1497 | Neg _ => Dvd (i, aa) | Add (_, _) => Dvd (i, aa) |
|
1498 | Sub (_, _) => Dvd (i, aa) | Mul (_, _) => Dvd (i, aa)) |
|
1499 end)) |
|
1500 | simpfm (NDvd (i, a)) = |
|
1501 (if ((i : IntInf.int) = (0 : IntInf.int)) then simpfm (NEq a) |
|
1502 else (if (((abs_int i) : IntInf.int) = (1 : IntInf.int)) then F |
|
1503 else let |
|
1504 val aa = simpnum a; |
|
1505 in |
|
1506 (case aa |
|
1507 of C v => |
|
1508 (if not (dvd (semiring_div_int, eq_int) i v) then T |
|
1509 else F) |
|
1510 | Bound _ => NDvd (i, aa) | Cn (_, _, _) => NDvd (i, aa) |
|
1511 | Neg _ => NDvd (i, aa) | Add (_, _) => NDvd (i, aa) |
|
1512 | Sub (_, _) => NDvd (i, aa) | Mul (_, _) => NDvd (i, aa)) |
|
1513 end)) |
|
1514 | simpfm T = T |
|
1515 | simpfm F = F |
|
1516 | simpfm (E v) = E v |
|
1517 | simpfm (A v) = A v |
|
1518 | simpfm (Closed v) = Closed v |
|
1519 | simpfm (NClosed v) = NClosed v; |
|
1520 |
|
1521 fun iupt i j = |
|
1522 (if IntInf.< (j, i) then [] |
|
1523 else i :: iupt (IntInf.+ (i, (1 : IntInf.int))) j); |
|
1524 |
|
1525 fun mirror (And (p, q)) = And (mirror p, mirror q) |
|
1526 | mirror (Or (p, q)) = Or (mirror p, mirror q) |
|
1527 | mirror T = T |
|
1528 | mirror F = F |
|
1529 | mirror (Lt (C bo)) = Lt (C bo) |
|
1530 | mirror (Lt (Bound bp)) = Lt (Bound bp) |
|
1531 | mirror (Lt (Neg bt)) = Lt (Neg bt) |
|
1532 | mirror (Lt (Add (bu, bv))) = Lt (Add (bu, bv)) |
|
1533 | mirror (Lt (Sub (bw, bx))) = Lt (Sub (bw, bx)) |
|
1534 | mirror (Lt (Mul (by, bz))) = Lt (Mul (by, bz)) |
|
1535 | mirror (Le (C co)) = Le (C co) |
|
1536 | mirror (Le (Bound cp)) = Le (Bound cp) |
|
1537 | mirror (Le (Neg ct)) = Le (Neg ct) |
|
1538 | mirror (Le (Add (cu, cv))) = Le (Add (cu, cv)) |
|
1539 | mirror (Le (Sub (cw, cx))) = Le (Sub (cw, cx)) |
|
1540 | mirror (Le (Mul (cy, cz))) = Le (Mul (cy, cz)) |
|
1541 | mirror (Gt (C doa)) = Gt (C doa) |
|
1542 | mirror (Gt (Bound dp)) = Gt (Bound dp) |
|
1543 | mirror (Gt (Neg dt)) = Gt (Neg dt) |
|
1544 | mirror (Gt (Add (du, dv))) = Gt (Add (du, dv)) |
|
1545 | mirror (Gt (Sub (dw, dx))) = Gt (Sub (dw, dx)) |
|
1546 | mirror (Gt (Mul (dy, dz))) = Gt (Mul (dy, dz)) |
|
1547 | mirror (Ge (C eo)) = Ge (C eo) |
|
1548 | mirror (Ge (Bound ep)) = Ge (Bound ep) |
|
1549 | mirror (Ge (Neg et)) = Ge (Neg et) |
|
1550 | mirror (Ge (Add (eu, ev))) = Ge (Add (eu, ev)) |
|
1551 | mirror (Ge (Sub (ew, ex))) = Ge (Sub (ew, ex)) |
|
1552 | mirror (Ge (Mul (ey, ez))) = Ge (Mul (ey, ez)) |
|
1553 | mirror (Eq (C fo)) = Eq (C fo) |
|
1554 | mirror (Eq (Bound fp)) = Eq (Bound fp) |
|
1555 | mirror (Eq (Neg ft)) = Eq (Neg ft) |
|
1556 | mirror (Eq (Add (fu, fv))) = Eq (Add (fu, fv)) |
|
1557 | mirror (Eq (Sub (fw, fx))) = Eq (Sub (fw, fx)) |
|
1558 | mirror (Eq (Mul (fy, fz))) = Eq (Mul (fy, fz)) |
|
1559 | mirror (NEq (C go)) = NEq (C go) |
|
1560 | mirror (NEq (Bound gp)) = NEq (Bound gp) |
|
1561 | mirror (NEq (Neg gt)) = NEq (Neg gt) |
|
1562 | mirror (NEq (Add (gu, gv))) = NEq (Add (gu, gv)) |
|
1563 | mirror (NEq (Sub (gw, gx))) = NEq (Sub (gw, gx)) |
|
1564 | mirror (NEq (Mul (gy, gz))) = NEq (Mul (gy, gz)) |
|
1565 | mirror (Dvd (aa, C ho)) = Dvd (aa, C ho) |
|
1566 | mirror (Dvd (aa, Bound hp)) = Dvd (aa, Bound hp) |
|
1567 | mirror (Dvd (aa, Neg ht)) = Dvd (aa, Neg ht) |
|
1568 | mirror (Dvd (aa, Add (hu, hv))) = Dvd (aa, Add (hu, hv)) |
|
1569 | mirror (Dvd (aa, Sub (hw, hx))) = Dvd (aa, Sub (hw, hx)) |
|
1570 | mirror (Dvd (aa, Mul (hy, hz))) = Dvd (aa, Mul (hy, hz)) |
|
1571 | mirror (NDvd (ac, C io)) = NDvd (ac, C io) |
|
1572 | mirror (NDvd (ac, Bound ip)) = NDvd (ac, Bound ip) |
|
1573 | mirror (NDvd (ac, Neg it)) = NDvd (ac, Neg it) |
|
1574 | mirror (NDvd (ac, Add (iu, iv))) = NDvd (ac, Add (iu, iv)) |
|
1575 | mirror (NDvd (ac, Sub (iw, ix))) = NDvd (ac, Sub (iw, ix)) |
|
1576 | mirror (NDvd (ac, Mul (iy, iz))) = NDvd (ac, Mul (iy, iz)) |
|
1577 | mirror (Not ae) = Not ae |
|
1578 | mirror (Imp (aj, ak)) = Imp (aj, ak) |
|
1579 | mirror (Iff (al, am)) = Iff (al, am) |
|
1580 | mirror (E an) = E an |
|
1581 | mirror (A ao) = A ao |
|
1582 | mirror (Closed ap) = Closed ap |
|
1583 | mirror (NClosed aq) = NClosed aq |
|
1584 | mirror (Lt (Cn (cm, c, e))) = |
|
1585 (if ((cm : IntInf.int) = (0 : IntInf.int)) |
|
1586 then Gt (Cn ((0 : IntInf.int), c, Neg e)) |
|
1587 else Lt (Cn (suc (minus_nat cm (1 : IntInf.int)), c, e))) |
|
1588 | mirror (Le (Cn (dm, c, e))) = |
|
1589 (if ((dm : IntInf.int) = (0 : IntInf.int)) |
|
1590 then Ge (Cn ((0 : IntInf.int), c, Neg e)) |
|
1591 else Le (Cn (suc (minus_nat dm (1 : IntInf.int)), c, e))) |
|
1592 | mirror (Gt (Cn (em, c, e))) = |
|
1593 (if ((em : IntInf.int) = (0 : IntInf.int)) |
|
1594 then Lt (Cn ((0 : IntInf.int), c, Neg e)) |
|
1595 else Gt (Cn (suc (minus_nat em (1 : IntInf.int)), c, e))) |
|
1596 | mirror (Ge (Cn (fm, c, e))) = |
|
1597 (if ((fm : IntInf.int) = (0 : IntInf.int)) |
|
1598 then Le (Cn ((0 : IntInf.int), c, Neg e)) |
|
1599 else Ge (Cn (suc (minus_nat fm (1 : IntInf.int)), c, e))) |
|
1600 | mirror (Eq (Cn (gm, c, e))) = |
|
1601 (if ((gm : IntInf.int) = (0 : IntInf.int)) |
|
1602 then Eq (Cn ((0 : IntInf.int), c, Neg e)) |
|
1603 else Eq (Cn (suc (minus_nat gm (1 : IntInf.int)), c, e))) |
|
1604 | mirror (NEq (Cn (hm, c, e))) = |
|
1605 (if ((hm : IntInf.int) = (0 : IntInf.int)) |
|
1606 then NEq (Cn ((0 : IntInf.int), c, Neg e)) |
|
1607 else NEq (Cn (suc (minus_nat hm (1 : IntInf.int)), c, e))) |
|
1608 | mirror (Dvd (i, Cn (im, c, e))) = |
|
1609 (if ((im : IntInf.int) = (0 : IntInf.int)) |
|
1610 then Dvd (i, Cn ((0 : IntInf.int), c, Neg e)) |
|
1611 else Dvd (i, Cn (suc (minus_nat im (1 : IntInf.int)), c, e))) |
|
1612 | mirror (NDvd (i, Cn (jm, c, e))) = |
|
1613 (if ((jm : IntInf.int) = (0 : IntInf.int)) |
|
1614 then NDvd (i, Cn ((0 : IntInf.int), c, Neg e)) |
|
1615 else NDvd (i, Cn (suc (minus_nat jm (1 : IntInf.int)), c, e))); |
|
1616 |
|
1617 fun size_list [] = (0 : IntInf.int) |
|
1618 | size_list (a :: lista) = IntInf.+ (size_list lista, suc (0 : IntInf.int)); |
|
1619 |
|
1620 fun alpha (And (p, q)) = append (alpha p) (alpha q) |
|
1621 | alpha (Or (p, q)) = append (alpha p) (alpha q) |
|
1622 | alpha T = [] |
|
1623 | alpha F = [] |
|
1624 | alpha (Lt (C bo)) = [] |
|
1625 | alpha (Lt (Bound bp)) = [] |
|
1626 | alpha (Lt (Neg bt)) = [] |
|
1627 | alpha (Lt (Add (bu, bv))) = [] |
|
1628 | alpha (Lt (Sub (bw, bx))) = [] |
|
1629 | alpha (Lt (Mul (by, bz))) = [] |
|
1630 | alpha (Le (C co)) = [] |
|
1631 | alpha (Le (Bound cp)) = [] |
|
1632 | alpha (Le (Neg ct)) = [] |
|
1633 | alpha (Le (Add (cu, cv))) = [] |
|
1634 | alpha (Le (Sub (cw, cx))) = [] |
|
1635 | alpha (Le (Mul (cy, cz))) = [] |
|
1636 | alpha (Gt (C doa)) = [] |
|
1637 | alpha (Gt (Bound dp)) = [] |
|
1638 | alpha (Gt (Neg dt)) = [] |
|
1639 | alpha (Gt (Add (du, dv))) = [] |
|
1640 | alpha (Gt (Sub (dw, dx))) = [] |
|
1641 | alpha (Gt (Mul (dy, dz))) = [] |
|
1642 | alpha (Ge (C eo)) = [] |
|
1643 | alpha (Ge (Bound ep)) = [] |
|
1644 | alpha (Ge (Neg et)) = [] |
|
1645 | alpha (Ge (Add (eu, ev))) = [] |
|
1646 | alpha (Ge (Sub (ew, ex))) = [] |
|
1647 | alpha (Ge (Mul (ey, ez))) = [] |
|
1648 | alpha (Eq (C fo)) = [] |
|
1649 | alpha (Eq (Bound fp)) = [] |
|
1650 | alpha (Eq (Neg ft)) = [] |
|
1651 | alpha (Eq (Add (fu, fv))) = [] |
|
1652 | alpha (Eq (Sub (fw, fx))) = [] |
|
1653 | alpha (Eq (Mul (fy, fz))) = [] |
|
1654 | alpha (NEq (C go)) = [] |
|
1655 | alpha (NEq (Bound gp)) = [] |
|
1656 | alpha (NEq (Neg gt)) = [] |
|
1657 | alpha (NEq (Add (gu, gv))) = [] |
|
1658 | alpha (NEq (Sub (gw, gx))) = [] |
|
1659 | alpha (NEq (Mul (gy, gz))) = [] |
|
1660 | alpha (Dvd (aa, ab)) = [] |
|
1661 | alpha (NDvd (ac, ad)) = [] |
|
1662 | alpha (Not ae) = [] |
|
1663 | alpha (Imp (aj, ak)) = [] |
|
1664 | alpha (Iff (al, am)) = [] |
|
1665 | alpha (E an) = [] |
|
1666 | alpha (A ao) = [] |
|
1667 | alpha (Closed ap) = [] |
|
1668 | alpha (NClosed aq) = [] |
|
1669 | alpha (Lt (Cn (cm, c, e))) = |
|
1670 (if ((cm : IntInf.int) = (0 : IntInf.int)) then [e] else []) |
|
1671 | alpha (Le (Cn (dm, c, e))) = |
|
1672 (if ((dm : IntInf.int) = (0 : IntInf.int)) |
|
1673 then [Add (C (~1 : IntInf.int), e)] else []) |
|
1674 | alpha (Gt (Cn (em, c, e))) = |
|
1675 (if ((em : IntInf.int) = (0 : IntInf.int)) then [] else []) |
|
1676 | alpha (Ge (Cn (fm, c, e))) = |
|
1677 (if ((fm : IntInf.int) = (0 : IntInf.int)) then [] else []) |
|
1678 | alpha (Eq (Cn (gm, c, e))) = |
|
1679 (if ((gm : IntInf.int) = (0 : IntInf.int)) |
|
1680 then [Add (C (~1 : IntInf.int), e)] else []) |
|
1681 | alpha (NEq (Cn (hm, c, e))) = |
|
1682 (if ((hm : IntInf.int) = (0 : IntInf.int)) then [e] else []); |
|
1683 |
|
1684 fun beta (And (p, q)) = append (beta p) (beta q) |
|
1685 | beta (Or (p, q)) = append (beta p) (beta q) |
|
1686 | beta T = [] |
|
1687 | beta F = [] |
|
1688 | beta (Lt (C bo)) = [] |
|
1689 | beta (Lt (Bound bp)) = [] |
|
1690 | beta (Lt (Neg bt)) = [] |
|
1691 | beta (Lt (Add (bu, bv))) = [] |
|
1692 | beta (Lt (Sub (bw, bx))) = [] |
|
1693 | beta (Lt (Mul (by, bz))) = [] |
|
1694 | beta (Le (C co)) = [] |
|
1695 | beta (Le (Bound cp)) = [] |
|
1696 | beta (Le (Neg ct)) = [] |
|
1697 | beta (Le (Add (cu, cv))) = [] |
|
1698 | beta (Le (Sub (cw, cx))) = [] |
|
1699 | beta (Le (Mul (cy, cz))) = [] |
|
1700 | beta (Gt (C doa)) = [] |
|
1701 | beta (Gt (Bound dp)) = [] |
|
1702 | beta (Gt (Neg dt)) = [] |
|
1703 | beta (Gt (Add (du, dv))) = [] |
|
1704 | beta (Gt (Sub (dw, dx))) = [] |
|
1705 | beta (Gt (Mul (dy, dz))) = [] |
|
1706 | beta (Ge (C eo)) = [] |
|
1707 | beta (Ge (Bound ep)) = [] |
|
1708 | beta (Ge (Neg et)) = [] |
|
1709 | beta (Ge (Add (eu, ev))) = [] |
|
1710 | beta (Ge (Sub (ew, ex))) = [] |
|
1711 | beta (Ge (Mul (ey, ez))) = [] |
|
1712 | beta (Eq (C fo)) = [] |
|
1713 | beta (Eq (Bound fp)) = [] |
|
1714 | beta (Eq (Neg ft)) = [] |
|
1715 | beta (Eq (Add (fu, fv))) = [] |
|
1716 | beta (Eq (Sub (fw, fx))) = [] |
|
1717 | beta (Eq (Mul (fy, fz))) = [] |
|
1718 | beta (NEq (C go)) = [] |
|
1719 | beta (NEq (Bound gp)) = [] |
|
1720 | beta (NEq (Neg gt)) = [] |
|
1721 | beta (NEq (Add (gu, gv))) = [] |
|
1722 | beta (NEq (Sub (gw, gx))) = [] |
|
1723 | beta (NEq (Mul (gy, gz))) = [] |
|
1724 | beta (Dvd (aa, ab)) = [] |
|
1725 | beta (NDvd (ac, ad)) = [] |
|
1726 | beta (Not ae) = [] |
|
1727 | beta (Imp (aj, ak)) = [] |
|
1728 | beta (Iff (al, am)) = [] |
|
1729 | beta (E an) = [] |
|
1730 | beta (A ao) = [] |
|
1731 | beta (Closed ap) = [] |
|
1732 | beta (NClosed aq) = [] |
|
1733 | beta (Lt (Cn (cm, c, e))) = |
|
1734 (if ((cm : IntInf.int) = (0 : IntInf.int)) then [] else []) |
|
1735 | beta (Le (Cn (dm, c, e))) = |
|
1736 (if ((dm : IntInf.int) = (0 : IntInf.int)) then [] else []) |
|
1737 | beta (Gt (Cn (em, c, e))) = |
|
1738 (if ((em : IntInf.int) = (0 : IntInf.int)) then [Neg e] else []) |
|
1739 | beta (Ge (Cn (fm, c, e))) = |
|
1740 (if ((fm : IntInf.int) = (0 : IntInf.int)) |
|
1741 then [Sub (C (~1 : IntInf.int), e)] else []) |
|
1742 | beta (Eq (Cn (gm, c, e))) = |
|
1743 (if ((gm : IntInf.int) = (0 : IntInf.int)) |
|
1744 then [Sub (C (~1 : IntInf.int), e)] else []) |
|
1745 | beta (NEq (Cn (hm, c, e))) = |
|
1746 (if ((hm : IntInf.int) = (0 : IntInf.int)) then [Neg e] else []); |
|
1747 |
|
1748 val eq_numa = {eq = eq_num} : num eq; |
|
1749 |
|
1750 fun member A_ x [] = false |
|
1751 | member A_ x (y :: ys) = eqa A_ x y orelse member A_ x ys; |
|
1752 |
|
1753 fun remdups A_ [] = [] |
|
1754 | remdups A_ (x :: xs) = |
|
1755 (if member A_ x xs then remdups A_ xs else x :: remdups A_ xs); |
|
1756 |
|
1757 fun gcd_int k l = |
|
1758 abs_int |
|
1759 (if ((l : IntInf.int) = (0 : IntInf.int)) then k |
|
1760 else gcd_int l (mod_int (abs_int k) (abs_int l))); |
|
1761 |
|
1762 fun lcm_int a b = div_int (IntInf.* (abs_int a, abs_int b)) (gcd_int a b); |
|
1763 |
|
1764 fun delta (And (p, q)) = lcm_int (delta p) (delta q) |
|
1765 | delta (Or (p, q)) = lcm_int (delta p) (delta q) |
|
1766 | delta T = (1 : IntInf.int) |
|
1767 | delta F = (1 : IntInf.int) |
|
1768 | delta (Lt u) = (1 : IntInf.int) |
|
1769 | delta (Le v) = (1 : IntInf.int) |
|
1770 | delta (Gt w) = (1 : IntInf.int) |
|
1771 | delta (Ge x) = (1 : IntInf.int) |
|
1772 | delta (Eq y) = (1 : IntInf.int) |
|
1773 | delta (NEq z) = (1 : IntInf.int) |
|
1774 | delta (Dvd (aa, C bo)) = (1 : IntInf.int) |
|
1775 | delta (Dvd (aa, Bound bp)) = (1 : IntInf.int) |
|
1776 | delta (Dvd (aa, Neg bt)) = (1 : IntInf.int) |
|
1777 | delta (Dvd (aa, Add (bu, bv))) = (1 : IntInf.int) |
|
1778 | delta (Dvd (aa, Sub (bw, bx))) = (1 : IntInf.int) |
|
1779 | delta (Dvd (aa, Mul (by, bz))) = (1 : IntInf.int) |
|
1780 | delta (NDvd (ac, C co)) = (1 : IntInf.int) |
|
1781 | delta (NDvd (ac, Bound cp)) = (1 : IntInf.int) |
|
1782 | delta (NDvd (ac, Neg ct)) = (1 : IntInf.int) |
|
1783 | delta (NDvd (ac, Add (cu, cv))) = (1 : IntInf.int) |
|
1784 | delta (NDvd (ac, Sub (cw, cx))) = (1 : IntInf.int) |
|
1785 | delta (NDvd (ac, Mul (cy, cz))) = (1 : IntInf.int) |
|
1786 | delta (Not ae) = (1 : IntInf.int) |
|
1787 | delta (Imp (aj, ak)) = (1 : IntInf.int) |
|
1788 | delta (Iff (al, am)) = (1 : IntInf.int) |
|
1789 | delta (E an) = (1 : IntInf.int) |
|
1790 | delta (A ao) = (1 : IntInf.int) |
|
1791 | delta (Closed ap) = (1 : IntInf.int) |
|
1792 | delta (NClosed aq) = (1 : IntInf.int) |
|
1793 | delta (Dvd (i, Cn (cm, c, e))) = |
|
1794 (if ((cm : IntInf.int) = (0 : IntInf.int)) then i else (1 : IntInf.int)) |
|
1795 | delta (NDvd (i, Cn (dm, c, e))) = |
|
1796 (if ((dm : IntInf.int) = (0 : IntInf.int)) then i else (1 : IntInf.int)); |
|
1797 |
|
1798 fun a_beta (And (p, q)) = (fn k => And (a_beta p k, a_beta q k)) |
|
1799 | a_beta (Or (p, q)) = (fn k => Or (a_beta p k, a_beta q k)) |
|
1800 | a_beta T = (fn _ => T) |
|
1801 | a_beta F = (fn _ => F) |
|
1802 | a_beta (Lt (C bo)) = (fn _ => Lt (C bo)) |
|
1803 | a_beta (Lt (Bound bp)) = (fn _ => Lt (Bound bp)) |
|
1804 | a_beta (Lt (Neg bt)) = (fn _ => Lt (Neg bt)) |
|
1805 | a_beta (Lt (Add (bu, bv))) = (fn _ => Lt (Add (bu, bv))) |
|
1806 | a_beta (Lt (Sub (bw, bx))) = (fn _ => Lt (Sub (bw, bx))) |
|
1807 | a_beta (Lt (Mul (by, bz))) = (fn _ => Lt (Mul (by, bz))) |
|
1808 | a_beta (Le (C co)) = (fn _ => Le (C co)) |
|
1809 | a_beta (Le (Bound cp)) = (fn _ => Le (Bound cp)) |
|
1810 | a_beta (Le (Neg ct)) = (fn _ => Le (Neg ct)) |
|
1811 | a_beta (Le (Add (cu, cv))) = (fn _ => Le (Add (cu, cv))) |
|
1812 | a_beta (Le (Sub (cw, cx))) = (fn _ => Le (Sub (cw, cx))) |
|
1813 | a_beta (Le (Mul (cy, cz))) = (fn _ => Le (Mul (cy, cz))) |
|
1814 | a_beta (Gt (C doa)) = (fn _ => Gt (C doa)) |
|
1815 | a_beta (Gt (Bound dp)) = (fn _ => Gt (Bound dp)) |
|
1816 | a_beta (Gt (Neg dt)) = (fn _ => Gt (Neg dt)) |
|
1817 | a_beta (Gt (Add (du, dv))) = (fn _ => Gt (Add (du, dv))) |
|
1818 | a_beta (Gt (Sub (dw, dx))) = (fn _ => Gt (Sub (dw, dx))) |
|
1819 | a_beta (Gt (Mul (dy, dz))) = (fn _ => Gt (Mul (dy, dz))) |
|
1820 | a_beta (Ge (C eo)) = (fn _ => Ge (C eo)) |
|
1821 | a_beta (Ge (Bound ep)) = (fn _ => Ge (Bound ep)) |
|
1822 | a_beta (Ge (Neg et)) = (fn _ => Ge (Neg et)) |
|
1823 | a_beta (Ge (Add (eu, ev))) = (fn _ => Ge (Add (eu, ev))) |
|
1824 | a_beta (Ge (Sub (ew, ex))) = (fn _ => Ge (Sub (ew, ex))) |
|
1825 | a_beta (Ge (Mul (ey, ez))) = (fn _ => Ge (Mul (ey, ez))) |
|
1826 | a_beta (Eq (C fo)) = (fn _ => Eq (C fo)) |
|
1827 | a_beta (Eq (Bound fp)) = (fn _ => Eq (Bound fp)) |
|
1828 | a_beta (Eq (Neg ft)) = (fn _ => Eq (Neg ft)) |
|
1829 | a_beta (Eq (Add (fu, fv))) = (fn _ => Eq (Add (fu, fv))) |
|
1830 | a_beta (Eq (Sub (fw, fx))) = (fn _ => Eq (Sub (fw, fx))) |
|
1831 | a_beta (Eq (Mul (fy, fz))) = (fn _ => Eq (Mul (fy, fz))) |
|
1832 | a_beta (NEq (C go)) = (fn _ => NEq (C go)) |
|
1833 | a_beta (NEq (Bound gp)) = (fn _ => NEq (Bound gp)) |
|
1834 | a_beta (NEq (Neg gt)) = (fn _ => NEq (Neg gt)) |
|
1835 | a_beta (NEq (Add (gu, gv))) = (fn _ => NEq (Add (gu, gv))) |
|
1836 | a_beta (NEq (Sub (gw, gx))) = (fn _ => NEq (Sub (gw, gx))) |
|
1837 | a_beta (NEq (Mul (gy, gz))) = (fn _ => NEq (Mul (gy, gz))) |
|
1838 | a_beta (Dvd (aa, C ho)) = (fn _ => Dvd (aa, C ho)) |
|
1839 | a_beta (Dvd (aa, Bound hp)) = (fn _ => Dvd (aa, Bound hp)) |
|
1840 | a_beta (Dvd (aa, Neg ht)) = (fn _ => Dvd (aa, Neg ht)) |
|
1841 | a_beta (Dvd (aa, Add (hu, hv))) = (fn _ => Dvd (aa, Add (hu, hv))) |
|
1842 | a_beta (Dvd (aa, Sub (hw, hx))) = (fn _ => Dvd (aa, Sub (hw, hx))) |
|
1843 | a_beta (Dvd (aa, Mul (hy, hz))) = (fn _ => Dvd (aa, Mul (hy, hz))) |
|
1844 | a_beta (NDvd (ac, C io)) = (fn _ => NDvd (ac, C io)) |
|
1845 | a_beta (NDvd (ac, Bound ip)) = (fn _ => NDvd (ac, Bound ip)) |
|
1846 | a_beta (NDvd (ac, Neg it)) = (fn _ => NDvd (ac, Neg it)) |
|
1847 | a_beta (NDvd (ac, Add (iu, iv))) = (fn _ => NDvd (ac, Add (iu, iv))) |
|
1848 | a_beta (NDvd (ac, Sub (iw, ix))) = (fn _ => NDvd (ac, Sub (iw, ix))) |
|
1849 | a_beta (NDvd (ac, Mul (iy, iz))) = (fn _ => NDvd (ac, Mul (iy, iz))) |
|
1850 | a_beta (Not ae) = (fn _ => Not ae) |
|
1851 | a_beta (Imp (aj, ak)) = (fn _ => Imp (aj, ak)) |
|
1852 | a_beta (Iff (al, am)) = (fn _ => Iff (al, am)) |
|
1853 | a_beta (E an) = (fn _ => E an) |
|
1854 | a_beta (A ao) = (fn _ => A ao) |
|
1855 | a_beta (Closed ap) = (fn _ => Closed ap) |
|
1856 | a_beta (NClosed aq) = (fn _ => NClosed aq) |
|
1857 | a_beta (Lt (Cn (cm, c, e))) = |
|
1858 (if ((cm : IntInf.int) = (0 : IntInf.int)) |
|
1859 then (fn k => |
|
1860 Lt (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e)))) |
|
1861 else (fn _ => Lt (Cn (suc (minus_nat cm (1 : IntInf.int)), c, e)))) |
|
1862 | a_beta (Le (Cn (dm, c, e))) = |
|
1863 (if ((dm : IntInf.int) = (0 : IntInf.int)) |
|
1864 then (fn k => |
|
1865 Le (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e)))) |
|
1866 else (fn _ => Le (Cn (suc (minus_nat dm (1 : IntInf.int)), c, e)))) |
|
1867 | a_beta (Gt (Cn (em, c, e))) = |
|
1868 (if ((em : IntInf.int) = (0 : IntInf.int)) |
|
1869 then (fn k => |
|
1870 Gt (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e)))) |
|
1871 else (fn _ => Gt (Cn (suc (minus_nat em (1 : IntInf.int)), c, e)))) |
|
1872 | a_beta (Ge (Cn (fm, c, e))) = |
|
1873 (if ((fm : IntInf.int) = (0 : IntInf.int)) |
|
1874 then (fn k => |
|
1875 Ge (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e)))) |
|
1876 else (fn _ => Ge (Cn (suc (minus_nat fm (1 : IntInf.int)), c, e)))) |
|
1877 | a_beta (Eq (Cn (gm, c, e))) = |
|
1878 (if ((gm : IntInf.int) = (0 : IntInf.int)) |
|
1879 then (fn k => |
|
1880 Eq (Cn ((0 : IntInf.int), (1 : IntInf.int), Mul (div_int k c, e)))) |
|
1881 else (fn _ => Eq (Cn (suc (minus_nat gm (1 : IntInf.int)), c, e)))) |
|
1882 | a_beta (NEq (Cn (hm, c, e))) = |
|
1883 (if ((hm : IntInf.int) = (0 : IntInf.int)) |
|
1884 then (fn k => |
|
1885 NEq (Cn ((0 : IntInf.int), (1 : IntInf.int), |
|
1886 Mul (div_int k c, e)))) |
|
1887 else (fn _ => NEq (Cn (suc (minus_nat hm (1 : IntInf.int)), c, e)))) |
|
1888 | a_beta (Dvd (i, Cn (im, c, e))) = |
|
1889 (if ((im : IntInf.int) = (0 : IntInf.int)) |
|
1890 then (fn k => |
|
1891 Dvd (IntInf.* (div_int k c, i), |
|
1892 Cn ((0 : IntInf.int), (1 : IntInf.int), |
|
1893 Mul (div_int k c, e)))) |
|
1894 else (fn _ => Dvd (i, Cn (suc (minus_nat im (1 : IntInf.int)), c, e)))) |
|
1895 | a_beta (NDvd (i, Cn (jm, c, e))) = |
|
1896 (if ((jm : IntInf.int) = (0 : IntInf.int)) |
|
1897 then (fn k => |
|
1898 NDvd (IntInf.* (div_int k c, i), |
|
1899 Cn ((0 : IntInf.int), (1 : IntInf.int), |
|
1900 Mul (div_int k c, e)))) |
|
1901 else (fn _ => NDvd (i, Cn (suc (minus_nat jm (1 : IntInf.int)), c, e)))); |
|
1902 |
|
1903 fun zeta (And (p, q)) = lcm_int (zeta p) (zeta q) |
|
1904 | zeta (Or (p, q)) = lcm_int (zeta p) (zeta q) |
|
1905 | zeta T = (1 : IntInf.int) |
|
1906 | zeta F = (1 : IntInf.int) |
|
1907 | zeta (Lt (C bo)) = (1 : IntInf.int) |
|
1908 | zeta (Lt (Bound bp)) = (1 : IntInf.int) |
|
1909 | zeta (Lt (Neg bt)) = (1 : IntInf.int) |
|
1910 | zeta (Lt (Add (bu, bv))) = (1 : IntInf.int) |
|
1911 | zeta (Lt (Sub (bw, bx))) = (1 : IntInf.int) |
|
1912 | zeta (Lt (Mul (by, bz))) = (1 : IntInf.int) |
|
1913 | zeta (Le (C co)) = (1 : IntInf.int) |
|
1914 | zeta (Le (Bound cp)) = (1 : IntInf.int) |
|
1915 | zeta (Le (Neg ct)) = (1 : IntInf.int) |
|
1916 | zeta (Le (Add (cu, cv))) = (1 : IntInf.int) |
|
1917 | zeta (Le (Sub (cw, cx))) = (1 : IntInf.int) |
|
1918 | zeta (Le (Mul (cy, cz))) = (1 : IntInf.int) |
|
1919 | zeta (Gt (C doa)) = (1 : IntInf.int) |
|
1920 | zeta (Gt (Bound dp)) = (1 : IntInf.int) |
|
1921 | zeta (Gt (Neg dt)) = (1 : IntInf.int) |
|
1922 | zeta (Gt (Add (du, dv))) = (1 : IntInf.int) |
|
1923 | zeta (Gt (Sub (dw, dx))) = (1 : IntInf.int) |
|
1924 | zeta (Gt (Mul (dy, dz))) = (1 : IntInf.int) |
|
1925 | zeta (Ge (C eo)) = (1 : IntInf.int) |
|
1926 | zeta (Ge (Bound ep)) = (1 : IntInf.int) |
|
1927 | zeta (Ge (Neg et)) = (1 : IntInf.int) |
|
1928 | zeta (Ge (Add (eu, ev))) = (1 : IntInf.int) |
|
1929 | zeta (Ge (Sub (ew, ex))) = (1 : IntInf.int) |
|
1930 | zeta (Ge (Mul (ey, ez))) = (1 : IntInf.int) |
|
1931 | zeta (Eq (C fo)) = (1 : IntInf.int) |
|
1932 | zeta (Eq (Bound fp)) = (1 : IntInf.int) |
|
1933 | zeta (Eq (Neg ft)) = (1 : IntInf.int) |
|
1934 | zeta (Eq (Add (fu, fv))) = (1 : IntInf.int) |
|
1935 | zeta (Eq (Sub (fw, fx))) = (1 : IntInf.int) |
|
1936 | zeta (Eq (Mul (fy, fz))) = (1 : IntInf.int) |
|
1937 | zeta (NEq (C go)) = (1 : IntInf.int) |
|
1938 | zeta (NEq (Bound gp)) = (1 : IntInf.int) |
|
1939 | zeta (NEq (Neg gt)) = (1 : IntInf.int) |
|
1940 | zeta (NEq (Add (gu, gv))) = (1 : IntInf.int) |
|
1941 | zeta (NEq (Sub (gw, gx))) = (1 : IntInf.int) |
|
1942 | zeta (NEq (Mul (gy, gz))) = (1 : IntInf.int) |
|
1943 | zeta (Dvd (aa, C ho)) = (1 : IntInf.int) |
|
1944 | zeta (Dvd (aa, Bound hp)) = (1 : IntInf.int) |
|
1945 | zeta (Dvd (aa, Neg ht)) = (1 : IntInf.int) |
|
1946 | zeta (Dvd (aa, Add (hu, hv))) = (1 : IntInf.int) |
|
1947 | zeta (Dvd (aa, Sub (hw, hx))) = (1 : IntInf.int) |
|
1948 | zeta (Dvd (aa, Mul (hy, hz))) = (1 : IntInf.int) |
|
1949 | zeta (NDvd (ac, C io)) = (1 : IntInf.int) |
|
1950 | zeta (NDvd (ac, Bound ip)) = (1 : IntInf.int) |
|
1951 | zeta (NDvd (ac, Neg it)) = (1 : IntInf.int) |
|
1952 | zeta (NDvd (ac, Add (iu, iv))) = (1 : IntInf.int) |
|
1953 | zeta (NDvd (ac, Sub (iw, ix))) = (1 : IntInf.int) |
|
1954 | zeta (NDvd (ac, Mul (iy, iz))) = (1 : IntInf.int) |
|
1955 | zeta (Not ae) = (1 : IntInf.int) |
|
1956 | zeta (Imp (aj, ak)) = (1 : IntInf.int) |
|
1957 | zeta (Iff (al, am)) = (1 : IntInf.int) |
|
1958 | zeta (E an) = (1 : IntInf.int) |
|
1959 | zeta (A ao) = (1 : IntInf.int) |
|
1960 | zeta (Closed ap) = (1 : IntInf.int) |
|
1961 | zeta (NClosed aq) = (1 : IntInf.int) |
|
1962 | zeta (Lt (Cn (cm, c, e))) = |
|
1963 (if ((cm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int)) |
|
1964 | zeta (Le (Cn (dm, c, e))) = |
|
1965 (if ((dm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int)) |
|
1966 | zeta (Gt (Cn (em, c, e))) = |
|
1967 (if ((em : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int)) |
|
1968 | zeta (Ge (Cn (fm, c, e))) = |
|
1969 (if ((fm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int)) |
|
1970 | zeta (Eq (Cn (gm, c, e))) = |
|
1971 (if ((gm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int)) |
|
1972 | zeta (NEq (Cn (hm, c, e))) = |
|
1973 (if ((hm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int)) |
|
1974 | zeta (Dvd (i, Cn (im, c, e))) = |
|
1975 (if ((im : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int)) |
|
1976 | zeta (NDvd (i, Cn (jm, c, e))) = |
|
1977 (if ((jm : IntInf.int) = (0 : IntInf.int)) then c else (1 : IntInf.int)); |
|
1978 |
|
1979 fun zsplit0 (C c) = ((0 : IntInf.int), C c) |
|
1980 | zsplit0 (Bound n) = |
|
1981 (if ((n : IntInf.int) = (0 : IntInf.int)) |
|
1982 then ((1 : IntInf.int), C (0 : IntInf.int)) |
|
1983 else ((0 : IntInf.int), Bound n)) |
|
1984 | zsplit0 (Cn (n, i, a)) = |
|
1985 let |
|
1986 val (ia, aa) = zsplit0 a; |
|
1987 in |
|
1988 (if ((n : IntInf.int) = (0 : IntInf.int)) then (IntInf.+ (i, ia), aa) |
|
1989 else (ia, Cn (n, i, aa))) |
|
1990 end |
|
1991 | zsplit0 (Neg a) = |
|
1992 let |
|
1993 val (i, aa) = zsplit0 a; |
|
1994 in |
|
1995 (IntInf.~ i, Neg aa) |
|
1996 end |
|
1997 | zsplit0 (Add (a, b)) = |
|
1998 let |
|
1999 val (ia, aa) = zsplit0 a; |
|
2000 val (ib, ba) = zsplit0 b; |
|
2001 in |
|
2002 (IntInf.+ (ia, ib), Add (aa, ba)) |
|
2003 end |
|
2004 | zsplit0 (Sub (a, b)) = |
|
2005 let |
|
2006 val (ia, aa) = zsplit0 a; |
|
2007 val (ib, ba) = zsplit0 b; |
|
2008 in |
|
2009 (IntInf.- (ia, ib), Sub (aa, ba)) |
|
2010 end |
|
2011 | zsplit0 (Mul (i, a)) = |
|
2012 let |
|
2013 val (ia, aa) = zsplit0 a; |
|
2014 in |
|
2015 (IntInf.* (i, ia), Mul (i, aa)) |
|
2016 end; |
|
2017 |
|
2018 fun zlfm (And (p, q)) = And (zlfm p, zlfm q) |
|
2019 | zlfm (Or (p, q)) = Or (zlfm p, zlfm q) |
|
2020 | zlfm (Imp (p, q)) = Or (zlfm (Not p), zlfm q) |
|
2021 | zlfm (Iff (p, q)) = |
|
2022 Or (And (zlfm p, zlfm q), And (zlfm (Not p), zlfm (Not q))) |
|
2023 | zlfm (Lt a) = |
|
2024 let |
|
2025 val (c, r) = zsplit0 a; |
|
2026 in |
|
2027 (if ((c : IntInf.int) = (0 : IntInf.int)) then Lt r |
|
2028 else (if IntInf.< ((0 : IntInf.int), c) |
|
2029 then Lt (Cn ((0 : IntInf.int), c, r)) |
|
2030 else Gt (Cn ((0 : IntInf.int), IntInf.~ c, Neg r)))) |
|
2031 end |
|
2032 | zlfm (Le a) = |
|
2033 let |
|
2034 val (c, r) = zsplit0 a; |
|
2035 in |
|
2036 (if ((c : IntInf.int) = (0 : IntInf.int)) then Le r |
|
2037 else (if IntInf.< ((0 : IntInf.int), c) |
|
2038 then Le (Cn ((0 : IntInf.int), c, r)) |
|
2039 else Ge (Cn ((0 : IntInf.int), IntInf.~ c, Neg r)))) |
|
2040 end |
|
2041 | zlfm (Gt a) = |
|
2042 let |
|
2043 val (c, r) = zsplit0 a; |
|
2044 in |
|
2045 (if ((c : IntInf.int) = (0 : IntInf.int)) then Gt r |
|
2046 else (if IntInf.< ((0 : IntInf.int), c) |
|
2047 then Gt (Cn ((0 : IntInf.int), c, r)) |
|
2048 else Lt (Cn ((0 : IntInf.int), IntInf.~ c, Neg r)))) |
|
2049 end |
|
2050 | zlfm (Ge a) = |
|
2051 let |
|
2052 val (c, r) = zsplit0 a; |
|
2053 in |
|
2054 (if ((c : IntInf.int) = (0 : IntInf.int)) then Ge r |
|
2055 else (if IntInf.< ((0 : IntInf.int), c) |
|
2056 then Ge (Cn ((0 : IntInf.int), c, r)) |
|
2057 else Le (Cn ((0 : IntInf.int), IntInf.~ c, Neg r)))) |
|
2058 end |
|
2059 | zlfm (Eq a) = |
|
2060 let |
|
2061 val (c, r) = zsplit0 a; |
|
2062 in |
|
2063 (if ((c : IntInf.int) = (0 : IntInf.int)) then Eq r |
|
2064 else (if IntInf.< ((0 : IntInf.int), c) |
|
2065 then Eq (Cn ((0 : IntInf.int), c, r)) |
|
2066 else Eq (Cn ((0 : IntInf.int), IntInf.~ c, Neg r)))) |
|
2067 end |
|
2068 | zlfm (NEq a) = |
|
2069 let |
|
2070 val (c, r) = zsplit0 a; |
|
2071 in |
|
2072 (if ((c : IntInf.int) = (0 : IntInf.int)) then NEq r |
|
2073 else (if IntInf.< ((0 : IntInf.int), c) |
|
2074 then NEq (Cn ((0 : IntInf.int), c, r)) |
|
2075 else NEq (Cn ((0 : IntInf.int), IntInf.~ c, Neg r)))) |
|
2076 end |
|
2077 | zlfm (Dvd (i, a)) = |
|
2078 (if ((i : IntInf.int) = (0 : IntInf.int)) then zlfm (Eq a) |
|
2079 else let |
|
2080 val (c, r) = zsplit0 a; |
|
2081 in |
|
2082 (if ((c : IntInf.int) = (0 : IntInf.int)) then Dvd (abs_int i, r) |
|
2083 else (if IntInf.< ((0 : IntInf.int), c) |
|
2084 then Dvd (abs_int i, Cn ((0 : IntInf.int), c, r)) |
|
2085 else Dvd (abs_int i, |
|
2086 Cn ((0 : IntInf.int), IntInf.~ c, Neg r)))) |
|
2087 end) |
|
2088 | zlfm (NDvd (i, a)) = |
|
2089 (if ((i : IntInf.int) = (0 : IntInf.int)) then zlfm (NEq a) |
|
2090 else let |
|
2091 val (c, r) = zsplit0 a; |
|
2092 in |
|
2093 (if ((c : IntInf.int) = (0 : IntInf.int)) then NDvd (abs_int i, r) |
|
2094 else (if IntInf.< ((0 : IntInf.int), c) |
|
2095 then NDvd (abs_int i, Cn ((0 : IntInf.int), c, r)) |
|
2096 else NDvd (abs_int i, |
|
2097 Cn ((0 : IntInf.int), IntInf.~ c, Neg r)))) |
|
2098 end) |
|
2099 | zlfm (Not (And (p, q))) = Or (zlfm (Not p), zlfm (Not q)) |
|
2100 | zlfm (Not (Or (p, q))) = And (zlfm (Not p), zlfm (Not q)) |
|
2101 | zlfm (Not (Imp (p, q))) = And (zlfm p, zlfm (Not q)) |
|
2102 | zlfm (Not (Iff (p, q))) = |
|
2103 Or (And (zlfm p, zlfm (Not q)), And (zlfm (Not p), zlfm q)) |
|
2104 | zlfm (Not (Not p)) = zlfm p |
|
2105 | zlfm (Not T) = F |
|
2106 | zlfm (Not F) = T |
|
2107 | zlfm (Not (Lt a)) = zlfm (Ge a) |
|
2108 | zlfm (Not (Le a)) = zlfm (Gt a) |
|
2109 | zlfm (Not (Gt a)) = zlfm (Le a) |
|
2110 | zlfm (Not (Ge a)) = zlfm (Lt a) |
|
2111 | zlfm (Not (Eq a)) = zlfm (NEq a) |
|
2112 | zlfm (Not (NEq a)) = zlfm (Eq a) |
|
2113 | zlfm (Not (Dvd (i, a))) = zlfm (NDvd (i, a)) |
|
2114 | zlfm (Not (NDvd (i, a))) = zlfm (Dvd (i, a)) |
|
2115 | zlfm (Not (Closed p)) = NClosed p |
|
2116 | zlfm (Not (NClosed p)) = Closed p |
|
2117 | zlfm T = T |
|
2118 | zlfm F = F |
|
2119 | zlfm (Not (E ci)) = Not (E ci) |
|
2120 | zlfm (Not (A cj)) = Not (A cj) |
|
2121 | zlfm (E ao) = E ao |
|
2122 | zlfm (A ap) = A ap |
|
2123 | zlfm (Closed aq) = Closed aq |
|
2124 | zlfm (NClosed ar) = NClosed ar; |
|
2125 |
|
2126 fun unita p = |
|
2127 let |
|
2128 val pa = zlfm p; |
|
2129 val l = zeta pa; |
|
2130 val q = |
|
2131 And (Dvd (l, Cn ((0 : IntInf.int), (1 : IntInf.int), C (0 : IntInf.int))), |
|
2132 a_beta pa l); |
|
2133 val d = delta q; |
|
2134 val b = remdups eq_numa (map simpnum (beta q)); |
|
2135 val a = remdups eq_numa (map simpnum (alpha q)); |
|
2136 in |
|
2137 (if IntInf.<= (size_list b, size_list a) then (q, (b, d)) |
|
2138 else (mirror q, (a, d))) |
|
2139 end; |
|
2140 |
|
2141 fun cooper p = |
|
2142 let |
|
2143 val (q, (b, d)) = unita p; |
|
2144 val js = iupt (1 : IntInf.int) d; |
|
2145 val mq = simpfm (minusinf q); |
|
2146 val md = evaldjf (fn j => simpfm (subst0 (C j) mq)) js; |
|
2147 in |
|
2148 (if eq_fm md T then T |
|
2149 else let |
|
2150 val qd = |
|
2151 evaldjf (fn (ba, j) => simpfm (subst0 (Add (ba, C j)) q)) |
|
2152 (concat_map (fn ba => map (fn a => (ba, a)) js) b); |
|
2153 in |
|
2154 decr (disj md qd) |
|
2155 end) |
|
2156 end; |
|
2157 |
|
2158 fun prep (E T) = T |
|
2159 | prep (E F) = F |
|
2160 | prep (E (Or (p, q))) = Or (prep (E p), prep (E q)) |
|
2161 | prep (E (Imp (p, q))) = Or (prep (E (Not p)), prep (E q)) |
|
2162 | prep (E (Iff (p, q))) = |
|
2163 Or (prep (E (And (p, q))), prep (E (And (Not p, Not q)))) |
|
2164 | prep (E (Not (And (p, q)))) = Or (prep (E (Not p)), prep (E (Not q))) |
|
2165 | prep (E (Not (Imp (p, q)))) = prep (E (And (p, Not q))) |
|
2166 | prep (E (Not (Iff (p, q)))) = |
|
2167 Or (prep (E (And (p, Not q))), prep (E (And (Not p, q)))) |
|
2168 | prep (E (Lt ef)) = E (prep (Lt ef)) |
|
2169 | prep (E (Le eg)) = E (prep (Le eg)) |
|
2170 | prep (E (Gt eh)) = E (prep (Gt eh)) |
|
2171 | prep (E (Ge ei)) = E (prep (Ge ei)) |
|
2172 | prep (E (Eq ej)) = E (prep (Eq ej)) |
|
2173 | prep (E (NEq ek)) = E (prep (NEq ek)) |
|
2174 | prep (E (Dvd (el, em))) = E (prep (Dvd (el, em))) |
|
2175 | prep (E (NDvd (en, eo))) = E (prep (NDvd (en, eo))) |
|
2176 | prep (E (Not T)) = E (prep (Not T)) |
|
2177 | prep (E (Not F)) = E (prep (Not F)) |
|
2178 | prep (E (Not (Lt gw))) = E (prep (Not (Lt gw))) |
|
2179 | prep (E (Not (Le gx))) = E (prep (Not (Le gx))) |
|
2180 | prep (E (Not (Gt gy))) = E (prep (Not (Gt gy))) |
|
2181 | prep (E (Not (Ge gz))) = E (prep (Not (Ge gz))) |
|
2182 | prep (E (Not (Eq ha))) = E (prep (Not (Eq ha))) |
|
2183 | prep (E (Not (NEq hb))) = E (prep (Not (NEq hb))) |
|
2184 | prep (E (Not (Dvd (hc, hd)))) = E (prep (Not (Dvd (hc, hd)))) |
|
2185 | prep (E (Not (NDvd (he, hf)))) = E (prep (Not (NDvd (he, hf)))) |
|
2186 | prep (E (Not (Not hg))) = E (prep (Not (Not hg))) |
|
2187 | prep (E (Not (Or (hj, hk)))) = E (prep (Not (Or (hj, hk)))) |
|
2188 | prep (E (Not (E hp))) = E (prep (Not (E hp))) |
|
2189 | prep (E (Not (A hq))) = E (prep (Not (A hq))) |
|
2190 | prep (E (Not (Closed hr))) = E (prep (Not (Closed hr))) |
|
2191 | prep (E (Not (NClosed hs))) = E (prep (Not (NClosed hs))) |
|
2192 | prep (E (And (eq, er))) = E (prep (And (eq, er))) |
|
2193 | prep (E (E ey)) = E (prep (E ey)) |
|
2194 | prep (E (A ez)) = E (prep (A ez)) |
|
2195 | prep (E (Closed fa)) = E (prep (Closed fa)) |
|
2196 | prep (E (NClosed fb)) = E (prep (NClosed fb)) |
|
2197 | prep (A (And (p, q))) = And (prep (A p), prep (A q)) |
|
2198 | prep (A T) = prep (Not (E (Not T))) |
|
2199 | prep (A F) = prep (Not (E (Not F))) |
|
2200 | prep (A (Lt jn)) = prep (Not (E (Not (Lt jn)))) |
|
2201 | prep (A (Le jo)) = prep (Not (E (Not (Le jo)))) |
|
2202 | prep (A (Gt jp)) = prep (Not (E (Not (Gt jp)))) |
|
2203 | prep (A (Ge jq)) = prep (Not (E (Not (Ge jq)))) |
|
2204 | prep (A (Eq jr)) = prep (Not (E (Not (Eq jr)))) |
|
2205 | prep (A (NEq js)) = prep (Not (E (Not (NEq js)))) |
|
2206 | prep (A (Dvd (jt, ju))) = prep (Not (E (Not (Dvd (jt, ju))))) |
|
2207 | prep (A (NDvd (jv, jw))) = prep (Not (E (Not (NDvd (jv, jw))))) |
|
2208 | prep (A (Not jx)) = prep (Not (E (Not (Not jx)))) |
|
2209 | prep (A (Or (ka, kb))) = prep (Not (E (Not (Or (ka, kb))))) |
|
2210 | prep (A (Imp (kc, kd))) = prep (Not (E (Not (Imp (kc, kd))))) |
|
2211 | prep (A (Iff (ke, kf))) = prep (Not (E (Not (Iff (ke, kf))))) |
|
2212 | prep (A (E kg)) = prep (Not (E (Not (E kg)))) |
|
2213 | prep (A (A kh)) = prep (Not (E (Not (A kh)))) |
|
2214 | prep (A (Closed ki)) = prep (Not (E (Not (Closed ki)))) |
|
2215 | prep (A (NClosed kj)) = prep (Not (E (Not (NClosed kj)))) |
|
2216 | prep (Not (Not p)) = prep p |
|
2217 | prep (Not (And (p, q))) = Or (prep (Not p), prep (Not q)) |
|
2218 | prep (Not (A p)) = prep (E (Not p)) |
|
2219 | prep (Not (Or (p, q))) = And (prep (Not p), prep (Not q)) |
|
2220 | prep (Not (Imp (p, q))) = And (prep p, prep (Not q)) |
|
2221 | prep (Not (Iff (p, q))) = Or (prep (And (p, Not q)), prep (And (Not p, q))) |
|
2222 | prep (Not T) = Not (prep T) |
|
2223 | prep (Not F) = Not (prep F) |
|
2224 | prep (Not (Lt bo)) = Not (prep (Lt bo)) |
|
2225 | prep (Not (Le bp)) = Not (prep (Le bp)) |
|
2226 | prep (Not (Gt bq)) = Not (prep (Gt bq)) |
|
2227 | prep (Not (Ge br)) = Not (prep (Ge br)) |
|
2228 | prep (Not (Eq bs)) = Not (prep (Eq bs)) |
|
2229 | prep (Not (NEq bt)) = Not (prep (NEq bt)) |
|
2230 | prep (Not (Dvd (bu, bv))) = Not (prep (Dvd (bu, bv))) |
|
2231 | prep (Not (NDvd (bw, bx))) = Not (prep (NDvd (bw, bx))) |
|
2232 | prep (Not (E ch)) = Not (prep (E ch)) |
|
2233 | prep (Not (Closed cj)) = Not (prep (Closed cj)) |
|
2234 | prep (Not (NClosed ck)) = Not (prep (NClosed ck)) |
|
2235 | prep (Or (p, q)) = Or (prep p, prep q) |
|
2236 | prep (And (p, q)) = And (prep p, prep q) |
|
2237 | prep (Imp (p, q)) = prep (Or (Not p, q)) |
|
2238 | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (Not p, Not q))) |
|
2239 | prep T = T |
|
2240 | prep F = F |
|
2241 | prep (Lt u) = Lt u |
|
2242 | prep (Le v) = Le v |
|
2243 | prep (Gt w) = Gt w |
|
2244 | prep (Ge x) = Ge x |
|
2245 | prep (Eq y) = Eq y |
|
2246 | prep (NEq z) = NEq z |
|
2247 | prep (Dvd (aa, ab)) = Dvd (aa, ab) |
|
2248 | prep (NDvd (ac, ad)) = NDvd (ac, ad) |
|
2249 | prep (Closed ap) = Closed ap |
|
2250 | prep (NClosed aq) = NClosed aq; |
|
2251 |
|
2252 fun qelim (E p) = (fn qe => dj qe (qelim p qe)) |
|
2253 | qelim (A p) = (fn qe => nota (qe (qelim (Not p) qe))) |
|
2254 | qelim (Not p) = (fn qe => nota (qelim p qe)) |
|
2255 | qelim (And (p, q)) = (fn qe => conj (qelim p qe) (qelim q qe)) |
|
2256 | qelim (Or (p, q)) = (fn qe => disj (qelim p qe) (qelim q qe)) |
|
2257 | qelim (Imp (p, q)) = (fn qe => impa (qelim p qe) (qelim q qe)) |
|
2258 | qelim (Iff (p, q)) = (fn qe => iffa (qelim p qe) (qelim q qe)) |
|
2259 | qelim T = (fn _ => simpfm T) |
|
2260 | qelim F = (fn _ => simpfm F) |
|
2261 | qelim (Lt u) = (fn _ => simpfm (Lt u)) |
|
2262 | qelim (Le v) = (fn _ => simpfm (Le v)) |
|
2263 | qelim (Gt w) = (fn _ => simpfm (Gt w)) |
|
2264 | qelim (Ge x) = (fn _ => simpfm (Ge x)) |
|
2265 | qelim (Eq y) = (fn _ => simpfm (Eq y)) |
|
2266 | qelim (NEq z) = (fn _ => simpfm (NEq z)) |
|
2267 | qelim (Dvd (aa, ab)) = (fn _ => simpfm (Dvd (aa, ab))) |
|
2268 | qelim (NDvd (ac, ad)) = (fn _ => simpfm (NDvd (ac, ad))) |
|
2269 | qelim (Closed ap) = (fn _ => simpfm (Closed ap)) |
|
2270 | qelim (NClosed aq) = (fn _ => simpfm (NClosed aq)); |
|
2271 |
|
2272 fun pa p = qelim (prep p) cooper; |
|
2273 |
|
2274 end; (*struct Generated_Cooper*) |
|