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