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