1369 fun gen_length n (x :: xs) = gen_length (suc n) xs |
1386 fun gen_length n (x :: xs) = gen_length (suc n) xs |
1370 | gen_length n [] = n; |
1387 | gen_length n [] = n; |
1371 |
1388 |
1372 fun size_list x = gen_length zero_nat x; |
1389 fun size_list x = gen_length zero_nat x; |
1373 |
1390 |
1374 fun a_beta (And (p, q)) = (fn k => And (a_beta p k, a_beta q k)) |
1391 fun a_beta (And (p, q)) k = And (a_beta p k, a_beta q k) |
1375 | a_beta (Or (p, q)) = (fn k => Or (a_beta p k, a_beta q k)) |
1392 | a_beta (Or (p, q)) k = Or (a_beta p k, a_beta q k) |
1376 | a_beta T = (fn _ => T) |
1393 | a_beta T k = T |
1377 | a_beta F = (fn _ => F) |
1394 | a_beta F k = F |
1378 | a_beta (Lt (C bo)) = (fn _ => Lt (C bo)) |
1395 | a_beta (Lt (C va)) k = Lt (C va) |
1379 | a_beta (Lt (Bound bp)) = (fn _ => Lt (Bound bp)) |
1396 | a_beta (Lt (Bound va)) k = Lt (Bound va) |
1380 | a_beta (Lt (Neg bt)) = (fn _ => Lt (Neg bt)) |
1397 | a_beta (Lt (Neg va)) k = Lt (Neg va) |
1381 | a_beta (Lt (Add (bu, bv))) = (fn _ => Lt (Add (bu, bv))) |
1398 | a_beta (Lt (Add (va, vb))) k = Lt (Add (va, vb)) |
1382 | a_beta (Lt (Sub (bw, bx))) = (fn _ => Lt (Sub (bw, bx))) |
1399 | a_beta (Lt (Sub (va, vb))) k = Lt (Sub (va, vb)) |
1383 | a_beta (Lt (Mul (by, bz))) = (fn _ => Lt (Mul (by, bz))) |
1400 | a_beta (Lt (Mul (va, vb))) k = Lt (Mul (va, vb)) |
1384 | a_beta (Le (C co)) = (fn _ => Le (C co)) |
1401 | a_beta (Le (C va)) k = Le (C va) |
1385 | a_beta (Le (Bound cp)) = (fn _ => Le (Bound cp)) |
1402 | a_beta (Le (Bound va)) k = Le (Bound va) |
1386 | a_beta (Le (Neg ct)) = (fn _ => Le (Neg ct)) |
1403 | a_beta (Le (Neg va)) k = Le (Neg va) |
1387 | a_beta (Le (Add (cu, cv))) = (fn _ => Le (Add (cu, cv))) |
1404 | a_beta (Le (Add (va, vb))) k = Le (Add (va, vb)) |
1388 | a_beta (Le (Sub (cw, cx))) = (fn _ => Le (Sub (cw, cx))) |
1405 | a_beta (Le (Sub (va, vb))) k = Le (Sub (va, vb)) |
1389 | a_beta (Le (Mul (cy, cz))) = (fn _ => Le (Mul (cy, cz))) |
1406 | a_beta (Le (Mul (va, vb))) k = Le (Mul (va, vb)) |
1390 | a_beta (Gt (C doa)) = (fn _ => Gt (C doa)) |
1407 | a_beta (Gt (C va)) k = Gt (C va) |
1391 | a_beta (Gt (Bound dp)) = (fn _ => Gt (Bound dp)) |
1408 | a_beta (Gt (Bound va)) k = Gt (Bound va) |
1392 | a_beta (Gt (Neg dt)) = (fn _ => Gt (Neg dt)) |
1409 | a_beta (Gt (Neg va)) k = Gt (Neg va) |
1393 | a_beta (Gt (Add (du, dv))) = (fn _ => Gt (Add (du, dv))) |
1410 | a_beta (Gt (Add (va, vb))) k = Gt (Add (va, vb)) |
1394 | a_beta (Gt (Sub (dw, dx))) = (fn _ => Gt (Sub (dw, dx))) |
1411 | a_beta (Gt (Sub (va, vb))) k = Gt (Sub (va, vb)) |
1395 | a_beta (Gt (Mul (dy, dz))) = (fn _ => Gt (Mul (dy, dz))) |
1412 | a_beta (Gt (Mul (va, vb))) k = Gt (Mul (va, vb)) |
1396 | a_beta (Ge (C eo)) = (fn _ => Ge (C eo)) |
1413 | a_beta (Ge (C va)) k = Ge (C va) |
1397 | a_beta (Ge (Bound ep)) = (fn _ => Ge (Bound ep)) |
1414 | a_beta (Ge (Bound va)) k = Ge (Bound va) |
1398 | a_beta (Ge (Neg et)) = (fn _ => Ge (Neg et)) |
1415 | a_beta (Ge (Neg va)) k = Ge (Neg va) |
1399 | a_beta (Ge (Add (eu, ev))) = (fn _ => Ge (Add (eu, ev))) |
1416 | a_beta (Ge (Add (va, vb))) k = Ge (Add (va, vb)) |
1400 | a_beta (Ge (Sub (ew, ex))) = (fn _ => Ge (Sub (ew, ex))) |
1417 | a_beta (Ge (Sub (va, vb))) k = Ge (Sub (va, vb)) |
1401 | a_beta (Ge (Mul (ey, ez))) = (fn _ => Ge (Mul (ey, ez))) |
1418 | a_beta (Ge (Mul (va, vb))) k = Ge (Mul (va, vb)) |
1402 | a_beta (Eq (C fo)) = (fn _ => Eq (C fo)) |
1419 | a_beta (Eq (C va)) k = Eq (C va) |
1403 | a_beta (Eq (Bound fp)) = (fn _ => Eq (Bound fp)) |
1420 | a_beta (Eq (Bound va)) k = Eq (Bound va) |
1404 | a_beta (Eq (Neg ft)) = (fn _ => Eq (Neg ft)) |
1421 | a_beta (Eq (Neg va)) k = Eq (Neg va) |
1405 | a_beta (Eq (Add (fu, fv))) = (fn _ => Eq (Add (fu, fv))) |
1422 | a_beta (Eq (Add (va, vb))) k = Eq (Add (va, vb)) |
1406 | a_beta (Eq (Sub (fw, fx))) = (fn _ => Eq (Sub (fw, fx))) |
1423 | a_beta (Eq (Sub (va, vb))) k = Eq (Sub (va, vb)) |
1407 | a_beta (Eq (Mul (fy, fz))) = (fn _ => Eq (Mul (fy, fz))) |
1424 | a_beta (Eq (Mul (va, vb))) k = Eq (Mul (va, vb)) |
1408 | a_beta (NEq (C go)) = (fn _ => NEq (C go)) |
1425 | a_beta (NEq (C va)) k = NEq (C va) |
1409 | a_beta (NEq (Bound gp)) = (fn _ => NEq (Bound gp)) |
1426 | a_beta (NEq (Bound va)) k = NEq (Bound va) |
1410 | a_beta (NEq (Neg gt)) = (fn _ => NEq (Neg gt)) |
1427 | a_beta (NEq (Neg va)) k = NEq (Neg va) |
1411 | a_beta (NEq (Add (gu, gv))) = (fn _ => NEq (Add (gu, gv))) |
1428 | a_beta (NEq (Add (va, vb))) k = NEq (Add (va, vb)) |
1412 | a_beta (NEq (Sub (gw, gx))) = (fn _ => NEq (Sub (gw, gx))) |
1429 | a_beta (NEq (Sub (va, vb))) k = NEq (Sub (va, vb)) |
1413 | a_beta (NEq (Mul (gy, gz))) = (fn _ => NEq (Mul (gy, gz))) |
1430 | a_beta (NEq (Mul (va, vb))) k = NEq (Mul (va, vb)) |
1414 | a_beta (Dvd (aa, C ho)) = (fn _ => Dvd (aa, C ho)) |
1431 | a_beta (Dvd (v, C vb)) k = Dvd (v, C vb) |
1415 | a_beta (Dvd (aa, Bound hp)) = (fn _ => Dvd (aa, Bound hp)) |
1432 | a_beta (Dvd (v, Bound vb)) k = Dvd (v, Bound vb) |
1416 | a_beta (Dvd (aa, Neg ht)) = (fn _ => Dvd (aa, Neg ht)) |
1433 | a_beta (Dvd (v, Neg vb)) k = Dvd (v, Neg vb) |
1417 | a_beta (Dvd (aa, Add (hu, hv))) = (fn _ => Dvd (aa, Add (hu, hv))) |
1434 | a_beta (Dvd (v, Add (vb, vc))) k = Dvd (v, Add (vb, vc)) |
1418 | a_beta (Dvd (aa, Sub (hw, hx))) = (fn _ => Dvd (aa, Sub (hw, hx))) |
1435 | a_beta (Dvd (v, Sub (vb, vc))) k = Dvd (v, Sub (vb, vc)) |
1419 | a_beta (Dvd (aa, Mul (hy, hz))) = (fn _ => Dvd (aa, Mul (hy, hz))) |
1436 | a_beta (Dvd (v, Mul (vb, vc))) k = Dvd (v, Mul (vb, vc)) |
1420 | a_beta (NDvd (ac, C io)) = (fn _ => NDvd (ac, C io)) |
1437 | a_beta (NDvd (v, C vb)) k = NDvd (v, C vb) |
1421 | a_beta (NDvd (ac, Bound ip)) = (fn _ => NDvd (ac, Bound ip)) |
1438 | a_beta (NDvd (v, Bound vb)) k = NDvd (v, Bound vb) |
1422 | a_beta (NDvd (ac, Neg it)) = (fn _ => NDvd (ac, Neg it)) |
1439 | a_beta (NDvd (v, Neg vb)) k = NDvd (v, Neg vb) |
1423 | a_beta (NDvd (ac, Add (iu, iv))) = (fn _ => NDvd (ac, Add (iu, iv))) |
1440 | a_beta (NDvd (v, Add (vb, vc))) k = NDvd (v, Add (vb, vc)) |
1424 | a_beta (NDvd (ac, Sub (iw, ix))) = (fn _ => NDvd (ac, Sub (iw, ix))) |
1441 | a_beta (NDvd (v, Sub (vb, vc))) k = NDvd (v, Sub (vb, vc)) |
1425 | a_beta (NDvd (ac, Mul (iy, iz))) = (fn _ => NDvd (ac, Mul (iy, iz))) |
1442 | a_beta (NDvd (v, Mul (vb, vc))) k = NDvd (v, Mul (vb, vc)) |
1426 | a_beta (NOT ae) = (fn _ => NOT ae) |
1443 | a_beta (NOT v) k = NOT v |
1427 | a_beta (Imp (aj, ak)) = (fn _ => Imp (aj, ak)) |
1444 | a_beta (Imp (v, va)) k = Imp (v, va) |
1428 | a_beta (Iff (al, am)) = (fn _ => Iff (al, am)) |
1445 | a_beta (Iff (v, va)) k = Iff (v, va) |
1429 | a_beta (E an) = (fn _ => E an) |
1446 | a_beta (E v) k = E v |
1430 | a_beta (A ao) = (fn _ => A ao) |
1447 | a_beta (A v) k = A v |
1431 | a_beta (Closed ap) = (fn _ => Closed ap) |
1448 | a_beta (Closed v) k = Closed v |
1432 | a_beta (NClosed aq) = (fn _ => NClosed aq) |
1449 | a_beta (NClosed v) k = NClosed v |
1433 | a_beta (Lt (CN (cm, c, e))) = |
1450 | a_beta (Lt (CN (vd, c, e))) k = |
1434 (if equal_nat cm zero_nat |
1451 (if equal_nat vd zero_nat |
1435 then (fn k => |
1452 then Lt (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) |
1436 Lt (CN (zero_nat, Int_of_integer (1 : IntInf.int), |
1453 else Lt (CN (suc (minus_nat vd one_nat), c, e))) |
1437 Mul (divide_inta k c, e)))) |
1454 | a_beta (Le (CN (vd, c, e))) k = |
1438 else (fn _ => Lt (CN (suc (minus_nat cm one_nat), c, e)))) |
1455 (if equal_nat vd zero_nat |
1439 | a_beta (Le (CN (dm, c, e))) = |
1456 then Le (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) |
1440 (if equal_nat dm zero_nat |
1457 else Le (CN (suc (minus_nat vd one_nat), c, e))) |
1441 then (fn k => |
1458 | a_beta (Gt (CN (vd, c, e))) k = |
1442 Le (CN (zero_nat, Int_of_integer (1 : IntInf.int), |
1459 (if equal_nat vd zero_nat |
1443 Mul (divide_inta k c, e)))) |
1460 then Gt (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) |
1444 else (fn _ => Le (CN (suc (minus_nat dm one_nat), c, e)))) |
1461 else Gt (CN (suc (minus_nat vd one_nat), c, e))) |
1445 | a_beta (Gt (CN (em, c, e))) = |
1462 | a_beta (Ge (CN (vd, c, e))) k = |
1446 (if equal_nat em zero_nat |
1463 (if equal_nat vd zero_nat |
1447 then (fn k => |
1464 then Ge (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) |
1448 Gt (CN (zero_nat, Int_of_integer (1 : IntInf.int), |
1465 else Ge (CN (suc (minus_nat vd one_nat), c, e))) |
1449 Mul (divide_inta k c, e)))) |
1466 | a_beta (Eq (CN (vd, c, e))) k = |
1450 else (fn _ => Gt (CN (suc (minus_nat em one_nat), c, e)))) |
1467 (if equal_nat vd zero_nat |
1451 | a_beta (Ge (CN (fm, c, e))) = |
1468 then Eq (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) |
1452 (if equal_nat fm zero_nat |
1469 else Eq (CN (suc (minus_nat vd one_nat), c, e))) |
1453 then (fn k => |
1470 | a_beta (NEq (CN (vd, c, e))) k = |
1454 Ge (CN (zero_nat, Int_of_integer (1 : IntInf.int), |
1471 (if equal_nat vd zero_nat |
1455 Mul (divide_inta k c, e)))) |
1472 then NEq (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) |
1456 else (fn _ => Ge (CN (suc (minus_nat fm one_nat), c, e)))) |
1473 else NEq (CN (suc (minus_nat vd one_nat), c, e))) |
1457 | a_beta (Eq (CN (gm, c, e))) = |
1474 | a_beta (Dvd (i, CN (ve, c, e))) k = |
1458 (if equal_nat gm zero_nat |
1475 (if equal_nat ve zero_nat |
1459 then (fn k => |
1476 then Dvd (times_inta (divide_inta k c) i, |
1460 Eq (CN (zero_nat, Int_of_integer (1 : IntInf.int), |
1477 CN (zero_nat, one_inta, Mul (divide_inta k c, e))) |
1461 Mul (divide_inta k c, e)))) |
1478 else Dvd (i, CN (suc (minus_nat ve one_nat), c, e))) |
1462 else (fn _ => Eq (CN (suc (minus_nat gm one_nat), c, e)))) |
1479 | a_beta (NDvd (i, CN (ve, c, e))) k = |
1463 | a_beta (NEq (CN (hm, c, e))) = |
1480 (if equal_nat ve zero_nat |
1464 (if equal_nat hm zero_nat |
1481 then NDvd (times_inta (divide_inta k c) i, |
1465 then (fn k => |
1482 CN (zero_nat, one_inta, Mul (divide_inta k c, e))) |
1466 NEq (CN (zero_nat, Int_of_integer (1 : IntInf.int), |
1483 else NDvd (i, CN (suc (minus_nat ve one_nat), c, e))); |
1467 Mul (divide_inta k c, e)))) |
1484 |
1468 else (fn _ => NEq (CN (suc (minus_nat hm one_nat), c, e)))) |
1485 fun gcd_integer k l = |
1469 | a_beta (Dvd (i, CN (im, c, e))) = |
1486 abs (if l = (0 : IntInf.int) then k |
1470 (if equal_nat im zero_nat |
1487 else gcd_integer l (modulo_integer (abs k) (abs l))); |
1471 then (fn k => |
1488 |
1472 Dvd (times_inta (divide_inta k c) i, |
1489 fun lcm_integer a b = divide_integer (abs a * abs b) (gcd_integer a b); |
1473 CN (zero_nat, Int_of_integer (1 : IntInf.int), |
1490 |
1474 Mul (divide_inta k c, e)))) |
1491 fun lcm_int (Int_of_integer x) (Int_of_integer y) = |
1475 else (fn _ => Dvd (i, CN (suc (minus_nat im one_nat), c, e)))) |
1492 Int_of_integer (lcm_integer x y); |
1476 | a_beta (NDvd (i, CN (jm, c, e))) = |
|
1477 (if equal_nat jm zero_nat |
|
1478 then (fn k => |
|
1479 NDvd (times_inta (divide_inta k c) i, |
|
1480 CN (zero_nat, Int_of_integer (1 : IntInf.int), |
|
1481 Mul (divide_inta k c, e)))) |
|
1482 else (fn _ => NDvd (i, CN (suc (minus_nat jm one_nat), c, e)))); |
|
1483 |
|
1484 fun gcd_int k l = |
|
1485 abs_int |
|
1486 (if equal_inta l zero_inta then k |
|
1487 else gcd_int l (mod_int (abs_int k) (abs_int l))); |
|
1488 |
|
1489 fun lcm_int a b = |
|
1490 divide_inta (times_inta (abs_int a) (abs_int b)) (gcd_int a b); |
|
1491 |
1493 |
1492 fun delta (And (p, q)) = lcm_int (delta p) (delta q) |
1494 fun delta (And (p, q)) = lcm_int (delta p) (delta q) |
1493 | delta (Or (p, q)) = lcm_int (delta p) (delta q) |
1495 | delta (Or (p, q)) = lcm_int (delta p) (delta q) |
1494 | delta T = Int_of_integer (1 : IntInf.int) |
1496 | delta T = one_inta |
1495 | delta F = Int_of_integer (1 : IntInf.int) |
1497 | delta F = one_inta |
1496 | delta (Lt u) = Int_of_integer (1 : IntInf.int) |
1498 | delta (Lt v) = one_inta |
1497 | delta (Le v) = Int_of_integer (1 : IntInf.int) |
1499 | delta (Le v) = one_inta |
1498 | delta (Gt w) = Int_of_integer (1 : IntInf.int) |
1500 | delta (Gt v) = one_inta |
1499 | delta (Ge x) = Int_of_integer (1 : IntInf.int) |
1501 | delta (Ge v) = one_inta |
1500 | delta (Eq y) = Int_of_integer (1 : IntInf.int) |
1502 | delta (Eq v) = one_inta |
1501 | delta (NEq z) = Int_of_integer (1 : IntInf.int) |
1503 | delta (NEq v) = one_inta |
1502 | delta (Dvd (aa, C bo)) = Int_of_integer (1 : IntInf.int) |
1504 | delta (Dvd (v, C vb)) = one_inta |
1503 | delta (Dvd (aa, Bound bp)) = Int_of_integer (1 : IntInf.int) |
1505 | delta (Dvd (v, Bound vb)) = one_inta |
1504 | delta (Dvd (aa, Neg bt)) = Int_of_integer (1 : IntInf.int) |
1506 | delta (Dvd (v, Neg vb)) = one_inta |
1505 | delta (Dvd (aa, Add (bu, bv))) = Int_of_integer (1 : IntInf.int) |
1507 | delta (Dvd (v, Add (vb, vc))) = one_inta |
1506 | delta (Dvd (aa, Sub (bw, bx))) = Int_of_integer (1 : IntInf.int) |
1508 | delta (Dvd (v, Sub (vb, vc))) = one_inta |
1507 | delta (Dvd (aa, Mul (by, bz))) = Int_of_integer (1 : IntInf.int) |
1509 | delta (Dvd (v, Mul (vb, vc))) = one_inta |
1508 | delta (NDvd (ac, C co)) = Int_of_integer (1 : IntInf.int) |
1510 | delta (NDvd (v, C vb)) = one_inta |
1509 | delta (NDvd (ac, Bound cp)) = Int_of_integer (1 : IntInf.int) |
1511 | delta (NDvd (v, Bound vb)) = one_inta |
1510 | delta (NDvd (ac, Neg ct)) = Int_of_integer (1 : IntInf.int) |
1512 | delta (NDvd (v, Neg vb)) = one_inta |
1511 | delta (NDvd (ac, Add (cu, cv))) = Int_of_integer (1 : IntInf.int) |
1513 | delta (NDvd (v, Add (vb, vc))) = one_inta |
1512 | delta (NDvd (ac, Sub (cw, cx))) = Int_of_integer (1 : IntInf.int) |
1514 | delta (NDvd (v, Sub (vb, vc))) = one_inta |
1513 | delta (NDvd (ac, Mul (cy, cz))) = Int_of_integer (1 : IntInf.int) |
1515 | delta (NDvd (v, Mul (vb, vc))) = one_inta |
1514 | delta (NOT ae) = Int_of_integer (1 : IntInf.int) |
1516 | delta (NOT v) = one_inta |
1515 | delta (Imp (aj, ak)) = Int_of_integer (1 : IntInf.int) |
1517 | delta (Imp (v, va)) = one_inta |
1516 | delta (Iff (al, am)) = Int_of_integer (1 : IntInf.int) |
1518 | delta (Iff (v, va)) = one_inta |
1517 | delta (E an) = Int_of_integer (1 : IntInf.int) |
1519 | delta (E v) = one_inta |
1518 | delta (A ao) = Int_of_integer (1 : IntInf.int) |
1520 | delta (A v) = one_inta |
1519 | delta (Closed ap) = Int_of_integer (1 : IntInf.int) |
1521 | delta (Closed v) = one_inta |
1520 | delta (NClosed aq) = Int_of_integer (1 : IntInf.int) |
1522 | delta (NClosed v) = one_inta |
1521 | delta (Dvd (i, CN (cm, c, e))) = |
1523 | delta (Dvd (i, CN (ve, c, e))) = |
1522 (if equal_nat cm zero_nat then i else Int_of_integer (1 : IntInf.int)) |
1524 (if equal_nat ve zero_nat then i else one_inta) |
1523 | delta (NDvd (i, CN (dm, c, e))) = |
1525 | delta (NDvd (i, CN (ve, c, e))) = |
1524 (if equal_nat dm zero_nat then i else Int_of_integer (1 : IntInf.int)); |
1526 (if equal_nat ve zero_nat then i else one_inta); |
1525 |
1527 |
1526 fun alpha (And (p, q)) = alpha p @ alpha q |
1528 fun alpha (And (p, q)) = alpha p @ alpha q |
1527 | alpha (Or (p, q)) = alpha p @ alpha q |
1529 | alpha (Or (p, q)) = alpha p @ alpha q |
1528 | alpha T = [] |
1530 | alpha T = [] |
1529 | alpha F = [] |
1531 | alpha F = [] |
1530 | alpha (Lt (C bo)) = [] |
1532 | alpha (Lt (C va)) = [] |
1531 | alpha (Lt (Bound bp)) = [] |
1533 | alpha (Lt (Bound va)) = [] |
1532 | alpha (Lt (Neg bt)) = [] |
1534 | alpha (Lt (Neg va)) = [] |
1533 | alpha (Lt (Add (bu, bv))) = [] |
1535 | alpha (Lt (Add (va, vb))) = [] |
1534 | alpha (Lt (Sub (bw, bx))) = [] |
1536 | alpha (Lt (Sub (va, vb))) = [] |
1535 | alpha (Lt (Mul (by, bz))) = [] |
1537 | alpha (Lt (Mul (va, vb))) = [] |
1536 | alpha (Le (C co)) = [] |
1538 | alpha (Le (C va)) = [] |
1537 | alpha (Le (Bound cp)) = [] |
1539 | alpha (Le (Bound va)) = [] |
1538 | alpha (Le (Neg ct)) = [] |
1540 | alpha (Le (Neg va)) = [] |
1539 | alpha (Le (Add (cu, cv))) = [] |
1541 | alpha (Le (Add (va, vb))) = [] |
1540 | alpha (Le (Sub (cw, cx))) = [] |
1542 | alpha (Le (Sub (va, vb))) = [] |
1541 | alpha (Le (Mul (cy, cz))) = [] |
1543 | alpha (Le (Mul (va, vb))) = [] |
1542 | alpha (Gt (C doa)) = [] |
1544 | alpha (Gt (C va)) = [] |
1543 | alpha (Gt (Bound dp)) = [] |
1545 | alpha (Gt (Bound va)) = [] |
1544 | alpha (Gt (Neg dt)) = [] |
1546 | alpha (Gt (Neg va)) = [] |
1545 | alpha (Gt (Add (du, dv))) = [] |
1547 | alpha (Gt (Add (va, vb))) = [] |
1546 | alpha (Gt (Sub (dw, dx))) = [] |
1548 | alpha (Gt (Sub (va, vb))) = [] |
1547 | alpha (Gt (Mul (dy, dz))) = [] |
1549 | alpha (Gt (Mul (va, vb))) = [] |
1548 | alpha (Ge (C eo)) = [] |
1550 | alpha (Ge (C va)) = [] |
1549 | alpha (Ge (Bound ep)) = [] |
1551 | alpha (Ge (Bound va)) = [] |
1550 | alpha (Ge (Neg et)) = [] |
1552 | alpha (Ge (Neg va)) = [] |
1551 | alpha (Ge (Add (eu, ev))) = [] |
1553 | alpha (Ge (Add (va, vb))) = [] |
1552 | alpha (Ge (Sub (ew, ex))) = [] |
1554 | alpha (Ge (Sub (va, vb))) = [] |
1553 | alpha (Ge (Mul (ey, ez))) = [] |
1555 | alpha (Ge (Mul (va, vb))) = [] |
1554 | alpha (Eq (C fo)) = [] |
1556 | alpha (Eq (C va)) = [] |
1555 | alpha (Eq (Bound fp)) = [] |
1557 | alpha (Eq (Bound va)) = [] |
1556 | alpha (Eq (Neg ft)) = [] |
1558 | alpha (Eq (Neg va)) = [] |
1557 | alpha (Eq (Add (fu, fv))) = [] |
1559 | alpha (Eq (Add (va, vb))) = [] |
1558 | alpha (Eq (Sub (fw, fx))) = [] |
1560 | alpha (Eq (Sub (va, vb))) = [] |
1559 | alpha (Eq (Mul (fy, fz))) = [] |
1561 | alpha (Eq (Mul (va, vb))) = [] |
1560 | alpha (NEq (C go)) = [] |
1562 | alpha (NEq (C va)) = [] |
1561 | alpha (NEq (Bound gp)) = [] |
1563 | alpha (NEq (Bound va)) = [] |
1562 | alpha (NEq (Neg gt)) = [] |
1564 | alpha (NEq (Neg va)) = [] |
1563 | alpha (NEq (Add (gu, gv))) = [] |
1565 | alpha (NEq (Add (va, vb))) = [] |
1564 | alpha (NEq (Sub (gw, gx))) = [] |
1566 | alpha (NEq (Sub (va, vb))) = [] |
1565 | alpha (NEq (Mul (gy, gz))) = [] |
1567 | alpha (NEq (Mul (va, vb))) = [] |
1566 | alpha (Dvd (aa, ab)) = [] |
1568 | alpha (Dvd (v, va)) = [] |
1567 | alpha (NDvd (ac, ad)) = [] |
1569 | alpha (NDvd (v, va)) = [] |
1568 | alpha (NOT ae) = [] |
1570 | alpha (NOT v) = [] |
1569 | alpha (Imp (aj, ak)) = [] |
1571 | alpha (Imp (v, va)) = [] |
1570 | alpha (Iff (al, am)) = [] |
1572 | alpha (Iff (v, va)) = [] |
1571 | alpha (E an) = [] |
1573 | alpha (E v) = [] |
1572 | alpha (A ao) = [] |
1574 | alpha (A v) = [] |
1573 | alpha (Closed ap) = [] |
1575 | alpha (Closed v) = [] |
1574 | alpha (NClosed aq) = [] |
1576 | alpha (NClosed v) = [] |
1575 | alpha (Lt (CN (cm, c, e))) = (if equal_nat cm zero_nat then [e] else []) |
1577 | alpha (Lt (CN (vd, c, e))) = (if equal_nat vd zero_nat then [e] else []) |
1576 | alpha (Le (CN (dm, c, e))) = |
1578 | alpha (Le (CN (vd, c, e))) = |
1577 (if equal_nat dm zero_nat |
1579 (if equal_nat vd zero_nat then [Add (C (uminus_int one_inta), e)] else []) |
1578 then [Add (C (uminus_int (Int_of_integer (1 : IntInf.int))), e)] else []) |
1580 | alpha (Gt (CN (vd, c, e))) = (if equal_nat vd zero_nat then [] else []) |
1579 | alpha (Gt (CN (em, c, e))) = (if equal_nat em zero_nat then [] else []) |
1581 | alpha (Ge (CN (vd, c, e))) = (if equal_nat vd zero_nat then [] else []) |
1580 | alpha (Ge (CN (fm, c, e))) = (if equal_nat fm zero_nat then [] else []) |
1582 | alpha (Eq (CN (vd, c, e))) = |
1581 | alpha (Eq (CN (gm, c, e))) = |
1583 (if equal_nat vd zero_nat then [Add (C (uminus_int one_inta), e)] else []) |
1582 (if equal_nat gm zero_nat |
1584 | alpha (NEq (CN (vd, c, e))) = (if equal_nat vd zero_nat then [e] else []); |
1583 then [Add (C (uminus_int (Int_of_integer (1 : IntInf.int))), e)] else []) |
|
1584 | alpha (NEq (CN (hm, c, e))) = (if equal_nat hm zero_nat then [e] else []); |
|
1585 |
1585 |
1586 fun zeta (And (p, q)) = lcm_int (zeta p) (zeta q) |
1586 fun zeta (And (p, q)) = lcm_int (zeta p) (zeta q) |
1587 | zeta (Or (p, q)) = lcm_int (zeta p) (zeta q) |
1587 | zeta (Or (p, q)) = lcm_int (zeta p) (zeta q) |
1588 | zeta T = Int_of_integer (1 : IntInf.int) |
1588 | zeta T = one_inta |
1589 | zeta F = Int_of_integer (1 : IntInf.int) |
1589 | zeta F = one_inta |
1590 | zeta (Lt (C bo)) = Int_of_integer (1 : IntInf.int) |
1590 | zeta (Lt (C va)) = one_inta |
1591 | zeta (Lt (Bound bp)) = Int_of_integer (1 : IntInf.int) |
1591 | zeta (Lt (Bound va)) = one_inta |
1592 | zeta (Lt (Neg bt)) = Int_of_integer (1 : IntInf.int) |
1592 | zeta (Lt (Neg va)) = one_inta |
1593 | zeta (Lt (Add (bu, bv))) = Int_of_integer (1 : IntInf.int) |
1593 | zeta (Lt (Add (va, vb))) = one_inta |
1594 | zeta (Lt (Sub (bw, bx))) = Int_of_integer (1 : IntInf.int) |
1594 | zeta (Lt (Sub (va, vb))) = one_inta |
1595 | zeta (Lt (Mul (by, bz))) = Int_of_integer (1 : IntInf.int) |
1595 | zeta (Lt (Mul (va, vb))) = one_inta |
1596 | zeta (Le (C co)) = Int_of_integer (1 : IntInf.int) |
1596 | zeta (Le (C va)) = one_inta |
1597 | zeta (Le (Bound cp)) = Int_of_integer (1 : IntInf.int) |
1597 | zeta (Le (Bound va)) = one_inta |
1598 | zeta (Le (Neg ct)) = Int_of_integer (1 : IntInf.int) |
1598 | zeta (Le (Neg va)) = one_inta |
1599 | zeta (Le (Add (cu, cv))) = Int_of_integer (1 : IntInf.int) |
1599 | zeta (Le (Add (va, vb))) = one_inta |
1600 | zeta (Le (Sub (cw, cx))) = Int_of_integer (1 : IntInf.int) |
1600 | zeta (Le (Sub (va, vb))) = one_inta |
1601 | zeta (Le (Mul (cy, cz))) = Int_of_integer (1 : IntInf.int) |
1601 | zeta (Le (Mul (va, vb))) = one_inta |
1602 | zeta (Gt (C doa)) = Int_of_integer (1 : IntInf.int) |
1602 | zeta (Gt (C va)) = one_inta |
1603 | zeta (Gt (Bound dp)) = Int_of_integer (1 : IntInf.int) |
1603 | zeta (Gt (Bound va)) = one_inta |
1604 | zeta (Gt (Neg dt)) = Int_of_integer (1 : IntInf.int) |
1604 | zeta (Gt (Neg va)) = one_inta |
1605 | zeta (Gt (Add (du, dv))) = Int_of_integer (1 : IntInf.int) |
1605 | zeta (Gt (Add (va, vb))) = one_inta |
1606 | zeta (Gt (Sub (dw, dx))) = Int_of_integer (1 : IntInf.int) |
1606 | zeta (Gt (Sub (va, vb))) = one_inta |
1607 | zeta (Gt (Mul (dy, dz))) = Int_of_integer (1 : IntInf.int) |
1607 | zeta (Gt (Mul (va, vb))) = one_inta |
1608 | zeta (Ge (C eo)) = Int_of_integer (1 : IntInf.int) |
1608 | zeta (Ge (C va)) = one_inta |
1609 | zeta (Ge (Bound ep)) = Int_of_integer (1 : IntInf.int) |
1609 | zeta (Ge (Bound va)) = one_inta |
1610 | zeta (Ge (Neg et)) = Int_of_integer (1 : IntInf.int) |
1610 | zeta (Ge (Neg va)) = one_inta |
1611 | zeta (Ge (Add (eu, ev))) = Int_of_integer (1 : IntInf.int) |
1611 | zeta (Ge (Add (va, vb))) = one_inta |
1612 | zeta (Ge (Sub (ew, ex))) = Int_of_integer (1 : IntInf.int) |
1612 | zeta (Ge (Sub (va, vb))) = one_inta |
1613 | zeta (Ge (Mul (ey, ez))) = Int_of_integer (1 : IntInf.int) |
1613 | zeta (Ge (Mul (va, vb))) = one_inta |
1614 | zeta (Eq (C fo)) = Int_of_integer (1 : IntInf.int) |
1614 | zeta (Eq (C va)) = one_inta |
1615 | zeta (Eq (Bound fp)) = Int_of_integer (1 : IntInf.int) |
1615 | zeta (Eq (Bound va)) = one_inta |
1616 | zeta (Eq (Neg ft)) = Int_of_integer (1 : IntInf.int) |
1616 | zeta (Eq (Neg va)) = one_inta |
1617 | zeta (Eq (Add (fu, fv))) = Int_of_integer (1 : IntInf.int) |
1617 | zeta (Eq (Add (va, vb))) = one_inta |
1618 | zeta (Eq (Sub (fw, fx))) = Int_of_integer (1 : IntInf.int) |
1618 | zeta (Eq (Sub (va, vb))) = one_inta |
1619 | zeta (Eq (Mul (fy, fz))) = Int_of_integer (1 : IntInf.int) |
1619 | zeta (Eq (Mul (va, vb))) = one_inta |
1620 | zeta (NEq (C go)) = Int_of_integer (1 : IntInf.int) |
1620 | zeta (NEq (C va)) = one_inta |
1621 | zeta (NEq (Bound gp)) = Int_of_integer (1 : IntInf.int) |
1621 | zeta (NEq (Bound va)) = one_inta |
1622 | zeta (NEq (Neg gt)) = Int_of_integer (1 : IntInf.int) |
1622 | zeta (NEq (Neg va)) = one_inta |
1623 | zeta (NEq (Add (gu, gv))) = Int_of_integer (1 : IntInf.int) |
1623 | zeta (NEq (Add (va, vb))) = one_inta |
1624 | zeta (NEq (Sub (gw, gx))) = Int_of_integer (1 : IntInf.int) |
1624 | zeta (NEq (Sub (va, vb))) = one_inta |
1625 | zeta (NEq (Mul (gy, gz))) = Int_of_integer (1 : IntInf.int) |
1625 | zeta (NEq (Mul (va, vb))) = one_inta |
1626 | zeta (Dvd (aa, C ho)) = Int_of_integer (1 : IntInf.int) |
1626 | zeta (Dvd (v, C vb)) = one_inta |
1627 | zeta (Dvd (aa, Bound hp)) = Int_of_integer (1 : IntInf.int) |
1627 | zeta (Dvd (v, Bound vb)) = one_inta |
1628 | zeta (Dvd (aa, Neg ht)) = Int_of_integer (1 : IntInf.int) |
1628 | zeta (Dvd (v, Neg vb)) = one_inta |
1629 | zeta (Dvd (aa, Add (hu, hv))) = Int_of_integer (1 : IntInf.int) |
1629 | zeta (Dvd (v, Add (vb, vc))) = one_inta |
1630 | zeta (Dvd (aa, Sub (hw, hx))) = Int_of_integer (1 : IntInf.int) |
1630 | zeta (Dvd (v, Sub (vb, vc))) = one_inta |
1631 | zeta (Dvd (aa, Mul (hy, hz))) = Int_of_integer (1 : IntInf.int) |
1631 | zeta (Dvd (v, Mul (vb, vc))) = one_inta |
1632 | zeta (NDvd (ac, C io)) = Int_of_integer (1 : IntInf.int) |
1632 | zeta (NDvd (v, C vb)) = one_inta |
1633 | zeta (NDvd (ac, Bound ip)) = Int_of_integer (1 : IntInf.int) |
1633 | zeta (NDvd (v, Bound vb)) = one_inta |
1634 | zeta (NDvd (ac, Neg it)) = Int_of_integer (1 : IntInf.int) |
1634 | zeta (NDvd (v, Neg vb)) = one_inta |
1635 | zeta (NDvd (ac, Add (iu, iv))) = Int_of_integer (1 : IntInf.int) |
1635 | zeta (NDvd (v, Add (vb, vc))) = one_inta |
1636 | zeta (NDvd (ac, Sub (iw, ix))) = Int_of_integer (1 : IntInf.int) |
1636 | zeta (NDvd (v, Sub (vb, vc))) = one_inta |
1637 | zeta (NDvd (ac, Mul (iy, iz))) = Int_of_integer (1 : IntInf.int) |
1637 | zeta (NDvd (v, Mul (vb, vc))) = one_inta |
1638 | zeta (NOT ae) = Int_of_integer (1 : IntInf.int) |
1638 | zeta (NOT v) = one_inta |
1639 | zeta (Imp (aj, ak)) = Int_of_integer (1 : IntInf.int) |
1639 | zeta (Imp (v, va)) = one_inta |
1640 | zeta (Iff (al, am)) = Int_of_integer (1 : IntInf.int) |
1640 | zeta (Iff (v, va)) = one_inta |
1641 | zeta (E an) = Int_of_integer (1 : IntInf.int) |
1641 | zeta (E v) = one_inta |
1642 | zeta (A ao) = Int_of_integer (1 : IntInf.int) |
1642 | zeta (A v) = one_inta |
1643 | zeta (Closed ap) = Int_of_integer (1 : IntInf.int) |
1643 | zeta (Closed v) = one_inta |
1644 | zeta (NClosed aq) = Int_of_integer (1 : IntInf.int) |
1644 | zeta (NClosed v) = one_inta |
1645 | zeta (Lt (CN (cm, c, e))) = |
1645 | zeta (Lt (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) |
1646 (if equal_nat cm zero_nat then c else Int_of_integer (1 : IntInf.int)) |
1646 | zeta (Le (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) |
1647 | zeta (Le (CN (dm, c, e))) = |
1647 | zeta (Gt (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) |
1648 (if equal_nat dm zero_nat then c else Int_of_integer (1 : IntInf.int)) |
1648 | zeta (Ge (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) |
1649 | zeta (Gt (CN (em, c, e))) = |
1649 | zeta (Eq (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) |
1650 (if equal_nat em zero_nat then c else Int_of_integer (1 : IntInf.int)) |
1650 | zeta (NEq (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) |
1651 | zeta (Ge (CN (fm, c, e))) = |
1651 | zeta (Dvd (i, CN (ve, c, e))) = |
1652 (if equal_nat fm zero_nat then c else Int_of_integer (1 : IntInf.int)) |
1652 (if equal_nat ve zero_nat then c else one_inta) |
1653 | zeta (Eq (CN (gm, c, e))) = |
1653 | zeta (NDvd (i, CN (ve, c, e))) = |
1654 (if equal_nat gm zero_nat then c else Int_of_integer (1 : IntInf.int)) |
1654 (if equal_nat ve zero_nat then c else one_inta); |
1655 | zeta (NEq (CN (hm, c, e))) = |
|
1656 (if equal_nat hm zero_nat then c else Int_of_integer (1 : IntInf.int)) |
|
1657 | zeta (Dvd (i, CN (im, c, e))) = |
|
1658 (if equal_nat im zero_nat then c else Int_of_integer (1 : IntInf.int)) |
|
1659 | zeta (NDvd (i, CN (jm, c, e))) = |
|
1660 (if equal_nat jm zero_nat then c else Int_of_integer (1 : IntInf.int)); |
|
1661 |
1655 |
1662 fun beta (And (p, q)) = beta p @ beta q |
1656 fun beta (And (p, q)) = beta p @ beta q |
1663 | beta (Or (p, q)) = beta p @ beta q |
1657 | beta (Or (p, q)) = beta p @ beta q |
1664 | beta T = [] |
1658 | beta T = [] |
1665 | beta F = [] |
1659 | beta F = [] |
1666 | beta (Lt (C bo)) = [] |
1660 | beta (Lt (C va)) = [] |
1667 | beta (Lt (Bound bp)) = [] |
1661 | beta (Lt (Bound va)) = [] |
1668 | beta (Lt (Neg bt)) = [] |
1662 | beta (Lt (Neg va)) = [] |
1669 | beta (Lt (Add (bu, bv))) = [] |
1663 | beta (Lt (Add (va, vb))) = [] |
1670 | beta (Lt (Sub (bw, bx))) = [] |
1664 | beta (Lt (Sub (va, vb))) = [] |
1671 | beta (Lt (Mul (by, bz))) = [] |
1665 | beta (Lt (Mul (va, vb))) = [] |
1672 | beta (Le (C co)) = [] |
1666 | beta (Le (C va)) = [] |
1673 | beta (Le (Bound cp)) = [] |
1667 | beta (Le (Bound va)) = [] |
1674 | beta (Le (Neg ct)) = [] |
1668 | beta (Le (Neg va)) = [] |
1675 | beta (Le (Add (cu, cv))) = [] |
1669 | beta (Le (Add (va, vb))) = [] |
1676 | beta (Le (Sub (cw, cx))) = [] |
1670 | beta (Le (Sub (va, vb))) = [] |
1677 | beta (Le (Mul (cy, cz))) = [] |
1671 | beta (Le (Mul (va, vb))) = [] |
1678 | beta (Gt (C doa)) = [] |
1672 | beta (Gt (C va)) = [] |
1679 | beta (Gt (Bound dp)) = [] |
1673 | beta (Gt (Bound va)) = [] |
1680 | beta (Gt (Neg dt)) = [] |
1674 | beta (Gt (Neg va)) = [] |
1681 | beta (Gt (Add (du, dv))) = [] |
1675 | beta (Gt (Add (va, vb))) = [] |
1682 | beta (Gt (Sub (dw, dx))) = [] |
1676 | beta (Gt (Sub (va, vb))) = [] |
1683 | beta (Gt (Mul (dy, dz))) = [] |
1677 | beta (Gt (Mul (va, vb))) = [] |
1684 | beta (Ge (C eo)) = [] |
1678 | beta (Ge (C va)) = [] |
1685 | beta (Ge (Bound ep)) = [] |
1679 | beta (Ge (Bound va)) = [] |
1686 | beta (Ge (Neg et)) = [] |
1680 | beta (Ge (Neg va)) = [] |
1687 | beta (Ge (Add (eu, ev))) = [] |
1681 | beta (Ge (Add (va, vb))) = [] |
1688 | beta (Ge (Sub (ew, ex))) = [] |
1682 | beta (Ge (Sub (va, vb))) = [] |
1689 | beta (Ge (Mul (ey, ez))) = [] |
1683 | beta (Ge (Mul (va, vb))) = [] |
1690 | beta (Eq (C fo)) = [] |
1684 | beta (Eq (C va)) = [] |
1691 | beta (Eq (Bound fp)) = [] |
1685 | beta (Eq (Bound va)) = [] |
1692 | beta (Eq (Neg ft)) = [] |
1686 | beta (Eq (Neg va)) = [] |
1693 | beta (Eq (Add (fu, fv))) = [] |
1687 | beta (Eq (Add (va, vb))) = [] |
1694 | beta (Eq (Sub (fw, fx))) = [] |
1688 | beta (Eq (Sub (va, vb))) = [] |
1695 | beta (Eq (Mul (fy, fz))) = [] |
1689 | beta (Eq (Mul (va, vb))) = [] |
1696 | beta (NEq (C go)) = [] |
1690 | beta (NEq (C va)) = [] |
1697 | beta (NEq (Bound gp)) = [] |
1691 | beta (NEq (Bound va)) = [] |
1698 | beta (NEq (Neg gt)) = [] |
1692 | beta (NEq (Neg va)) = [] |
1699 | beta (NEq (Add (gu, gv))) = [] |
1693 | beta (NEq (Add (va, vb))) = [] |
1700 | beta (NEq (Sub (gw, gx))) = [] |
1694 | beta (NEq (Sub (va, vb))) = [] |
1701 | beta (NEq (Mul (gy, gz))) = [] |
1695 | beta (NEq (Mul (va, vb))) = [] |
1702 | beta (Dvd (aa, ab)) = [] |
1696 | beta (Dvd (v, va)) = [] |
1703 | beta (NDvd (ac, ad)) = [] |
1697 | beta (NDvd (v, va)) = [] |
1704 | beta (NOT ae) = [] |
1698 | beta (NOT v) = [] |
1705 | beta (Imp (aj, ak)) = [] |
1699 | beta (Imp (v, va)) = [] |
1706 | beta (Iff (al, am)) = [] |
1700 | beta (Iff (v, va)) = [] |
1707 | beta (E an) = [] |
1701 | beta (E v) = [] |
1708 | beta (A ao) = [] |
1702 | beta (A v) = [] |
1709 | beta (Closed ap) = [] |
1703 | beta (Closed v) = [] |
1710 | beta (NClosed aq) = [] |
1704 | beta (NClosed v) = [] |
1711 | beta (Lt (CN (cm, c, e))) = (if equal_nat cm zero_nat then [] else []) |
1705 | beta (Lt (CN (vd, c, e))) = (if equal_nat vd zero_nat then [] else []) |
1712 | beta (Le (CN (dm, c, e))) = (if equal_nat dm zero_nat then [] else []) |
1706 | beta (Le (CN (vd, c, e))) = (if equal_nat vd zero_nat then [] else []) |
1713 | beta (Gt (CN (em, c, e))) = (if equal_nat em zero_nat then [Neg e] else []) |
1707 | beta (Gt (CN (vd, c, e))) = (if equal_nat vd zero_nat then [Neg e] else []) |
1714 | beta (Ge (CN (fm, c, e))) = |
1708 | beta (Ge (CN (vd, c, e))) = |
1715 (if equal_nat fm zero_nat |
1709 (if equal_nat vd zero_nat then [Sub (C (uminus_int one_inta), e)] else []) |
1716 then [Sub (C (uminus_int (Int_of_integer (1 : IntInf.int))), e)] else []) |
1710 | beta (Eq (CN (vd, c, e))) = |
1717 | beta (Eq (CN (gm, c, e))) = |
1711 (if equal_nat vd zero_nat then [Sub (C (uminus_int one_inta), e)] else []) |
1718 (if equal_nat gm zero_nat |
1712 | beta (NEq (CN (vd, c, e))) = |
1719 then [Sub (C (uminus_int (Int_of_integer (1 : IntInf.int))), e)] else []) |
1713 (if equal_nat vd zero_nat then [Neg e] else []); |
1720 | beta (NEq (CN (hm, c, e))) = |
|
1721 (if equal_nat hm zero_nat then [Neg e] else []); |
|
1722 |
1714 |
1723 fun mirror (And (p, q)) = And (mirror p, mirror q) |
1715 fun mirror (And (p, q)) = And (mirror p, mirror q) |
1724 | mirror (Or (p, q)) = Or (mirror p, mirror q) |
1716 | mirror (Or (p, q)) = Or (mirror p, mirror q) |
1725 | mirror T = T |
1717 | mirror T = T |
1726 | mirror F = F |
1718 | mirror F = F |
1727 | mirror (Lt (C bo)) = Lt (C bo) |
1719 | mirror (Lt (C va)) = Lt (C va) |
1728 | mirror (Lt (Bound bp)) = Lt (Bound bp) |
1720 | mirror (Lt (Bound va)) = Lt (Bound va) |
1729 | mirror (Lt (Neg bt)) = Lt (Neg bt) |
1721 | mirror (Lt (Neg va)) = Lt (Neg va) |
1730 | mirror (Lt (Add (bu, bv))) = Lt (Add (bu, bv)) |
1722 | mirror (Lt (Add (va, vb))) = Lt (Add (va, vb)) |
1731 | mirror (Lt (Sub (bw, bx))) = Lt (Sub (bw, bx)) |
1723 | mirror (Lt (Sub (va, vb))) = Lt (Sub (va, vb)) |
1732 | mirror (Lt (Mul (by, bz))) = Lt (Mul (by, bz)) |
1724 | mirror (Lt (Mul (va, vb))) = Lt (Mul (va, vb)) |
1733 | mirror (Le (C co)) = Le (C co) |
1725 | mirror (Le (C va)) = Le (C va) |
1734 | mirror (Le (Bound cp)) = Le (Bound cp) |
1726 | mirror (Le (Bound va)) = Le (Bound va) |
1735 | mirror (Le (Neg ct)) = Le (Neg ct) |
1727 | mirror (Le (Neg va)) = Le (Neg va) |
1736 | mirror (Le (Add (cu, cv))) = Le (Add (cu, cv)) |
1728 | mirror (Le (Add (va, vb))) = Le (Add (va, vb)) |
1737 | mirror (Le (Sub (cw, cx))) = Le (Sub (cw, cx)) |
1729 | mirror (Le (Sub (va, vb))) = Le (Sub (va, vb)) |
1738 | mirror (Le (Mul (cy, cz))) = Le (Mul (cy, cz)) |
1730 | mirror (Le (Mul (va, vb))) = Le (Mul (va, vb)) |
1739 | mirror (Gt (C doa)) = Gt (C doa) |
1731 | mirror (Gt (C va)) = Gt (C va) |
1740 | mirror (Gt (Bound dp)) = Gt (Bound dp) |
1732 | mirror (Gt (Bound va)) = Gt (Bound va) |
1741 | mirror (Gt (Neg dt)) = Gt (Neg dt) |
1733 | mirror (Gt (Neg va)) = Gt (Neg va) |
1742 | mirror (Gt (Add (du, dv))) = Gt (Add (du, dv)) |
1734 | mirror (Gt (Add (va, vb))) = Gt (Add (va, vb)) |
1743 | mirror (Gt (Sub (dw, dx))) = Gt (Sub (dw, dx)) |
1735 | mirror (Gt (Sub (va, vb))) = Gt (Sub (va, vb)) |
1744 | mirror (Gt (Mul (dy, dz))) = Gt (Mul (dy, dz)) |
1736 | mirror (Gt (Mul (va, vb))) = Gt (Mul (va, vb)) |
1745 | mirror (Ge (C eo)) = Ge (C eo) |
1737 | mirror (Ge (C va)) = Ge (C va) |
1746 | mirror (Ge (Bound ep)) = Ge (Bound ep) |
1738 | mirror (Ge (Bound va)) = Ge (Bound va) |
1747 | mirror (Ge (Neg et)) = Ge (Neg et) |
1739 | mirror (Ge (Neg va)) = Ge (Neg va) |
1748 | mirror (Ge (Add (eu, ev))) = Ge (Add (eu, ev)) |
1740 | mirror (Ge (Add (va, vb))) = Ge (Add (va, vb)) |
1749 | mirror (Ge (Sub (ew, ex))) = Ge (Sub (ew, ex)) |
1741 | mirror (Ge (Sub (va, vb))) = Ge (Sub (va, vb)) |
1750 | mirror (Ge (Mul (ey, ez))) = Ge (Mul (ey, ez)) |
1742 | mirror (Ge (Mul (va, vb))) = Ge (Mul (va, vb)) |
1751 | mirror (Eq (C fo)) = Eq (C fo) |
1743 | mirror (Eq (C va)) = Eq (C va) |
1752 | mirror (Eq (Bound fp)) = Eq (Bound fp) |
1744 | mirror (Eq (Bound va)) = Eq (Bound va) |
1753 | mirror (Eq (Neg ft)) = Eq (Neg ft) |
1745 | mirror (Eq (Neg va)) = Eq (Neg va) |
1754 | mirror (Eq (Add (fu, fv))) = Eq (Add (fu, fv)) |
1746 | mirror (Eq (Add (va, vb))) = Eq (Add (va, vb)) |
1755 | mirror (Eq (Sub (fw, fx))) = Eq (Sub (fw, fx)) |
1747 | mirror (Eq (Sub (va, vb))) = Eq (Sub (va, vb)) |
1756 | mirror (Eq (Mul (fy, fz))) = Eq (Mul (fy, fz)) |
1748 | mirror (Eq (Mul (va, vb))) = Eq (Mul (va, vb)) |
1757 | mirror (NEq (C go)) = NEq (C go) |
1749 | mirror (NEq (C va)) = NEq (C va) |
1758 | mirror (NEq (Bound gp)) = NEq (Bound gp) |
1750 | mirror (NEq (Bound va)) = NEq (Bound va) |
1759 | mirror (NEq (Neg gt)) = NEq (Neg gt) |
1751 | mirror (NEq (Neg va)) = NEq (Neg va) |
1760 | mirror (NEq (Add (gu, gv))) = NEq (Add (gu, gv)) |
1752 | mirror (NEq (Add (va, vb))) = NEq (Add (va, vb)) |
1761 | mirror (NEq (Sub (gw, gx))) = NEq (Sub (gw, gx)) |
1753 | mirror (NEq (Sub (va, vb))) = NEq (Sub (va, vb)) |
1762 | mirror (NEq (Mul (gy, gz))) = NEq (Mul (gy, gz)) |
1754 | mirror (NEq (Mul (va, vb))) = NEq (Mul (va, vb)) |
1763 | mirror (Dvd (aa, C ho)) = Dvd (aa, C ho) |
1755 | mirror (Dvd (v, C vb)) = Dvd (v, C vb) |
1764 | mirror (Dvd (aa, Bound hp)) = Dvd (aa, Bound hp) |
1756 | mirror (Dvd (v, Bound vb)) = Dvd (v, Bound vb) |
1765 | mirror (Dvd (aa, Neg ht)) = Dvd (aa, Neg ht) |
1757 | mirror (Dvd (v, Neg vb)) = Dvd (v, Neg vb) |
1766 | mirror (Dvd (aa, Add (hu, hv))) = Dvd (aa, Add (hu, hv)) |
1758 | mirror (Dvd (v, Add (vb, vc))) = Dvd (v, Add (vb, vc)) |
1767 | mirror (Dvd (aa, Sub (hw, hx))) = Dvd (aa, Sub (hw, hx)) |
1759 | mirror (Dvd (v, Sub (vb, vc))) = Dvd (v, Sub (vb, vc)) |
1768 | mirror (Dvd (aa, Mul (hy, hz))) = Dvd (aa, Mul (hy, hz)) |
1760 | mirror (Dvd (v, Mul (vb, vc))) = Dvd (v, Mul (vb, vc)) |
1769 | mirror (NDvd (ac, C io)) = NDvd (ac, C io) |
1761 | mirror (NDvd (v, C vb)) = NDvd (v, C vb) |
1770 | mirror (NDvd (ac, Bound ip)) = NDvd (ac, Bound ip) |
1762 | mirror (NDvd (v, Bound vb)) = NDvd (v, Bound vb) |
1771 | mirror (NDvd (ac, Neg it)) = NDvd (ac, Neg it) |
1763 | mirror (NDvd (v, Neg vb)) = NDvd (v, Neg vb) |
1772 | mirror (NDvd (ac, Add (iu, iv))) = NDvd (ac, Add (iu, iv)) |
1764 | mirror (NDvd (v, Add (vb, vc))) = NDvd (v, Add (vb, vc)) |
1773 | mirror (NDvd (ac, Sub (iw, ix))) = NDvd (ac, Sub (iw, ix)) |
1765 | mirror (NDvd (v, Sub (vb, vc))) = NDvd (v, Sub (vb, vc)) |
1774 | mirror (NDvd (ac, Mul (iy, iz))) = NDvd (ac, Mul (iy, iz)) |
1766 | mirror (NDvd (v, Mul (vb, vc))) = NDvd (v, Mul (vb, vc)) |
1775 | mirror (NOT ae) = NOT ae |
1767 | mirror (NOT v) = NOT v |
1776 | mirror (Imp (aj, ak)) = Imp (aj, ak) |
1768 | mirror (Imp (v, va)) = Imp (v, va) |
1777 | mirror (Iff (al, am)) = Iff (al, am) |
1769 | mirror (Iff (v, va)) = Iff (v, va) |
1778 | mirror (E an) = E an |
1770 | mirror (E v) = E v |
1779 | mirror (A ao) = A ao |
1771 | mirror (A v) = A v |
1780 | mirror (Closed ap) = Closed ap |
1772 | mirror (Closed v) = Closed v |
1781 | mirror (NClosed aq) = NClosed aq |
1773 | mirror (NClosed v) = NClosed v |
1782 | mirror (Lt (CN (cm, c, e))) = |
1774 | mirror (Lt (CN (vd, c, e))) = |
1783 (if equal_nat cm zero_nat then Gt (CN (zero_nat, c, Neg e)) |
1775 (if equal_nat vd zero_nat then Gt (CN (zero_nat, c, Neg e)) |
1784 else Lt (CN (suc (minus_nat cm one_nat), c, e))) |
1776 else Lt (CN (suc (minus_nat vd one_nat), c, e))) |
1785 | mirror (Le (CN (dm, c, e))) = |
1777 | mirror (Le (CN (vd, c, e))) = |
1786 (if equal_nat dm zero_nat then Ge (CN (zero_nat, c, Neg e)) |
1778 (if equal_nat vd zero_nat then Ge (CN (zero_nat, c, Neg e)) |
1787 else Le (CN (suc (minus_nat dm one_nat), c, e))) |
1779 else Le (CN (suc (minus_nat vd one_nat), c, e))) |
1788 | mirror (Gt (CN (em, c, e))) = |
1780 | mirror (Gt (CN (vd, c, e))) = |
1789 (if equal_nat em zero_nat then Lt (CN (zero_nat, c, Neg e)) |
1781 (if equal_nat vd zero_nat then Lt (CN (zero_nat, c, Neg e)) |
1790 else Gt (CN (suc (minus_nat em one_nat), c, e))) |
1782 else Gt (CN (suc (minus_nat vd one_nat), c, e))) |
1791 | mirror (Ge (CN (fm, c, e))) = |
1783 | mirror (Ge (CN (vd, c, e))) = |
1792 (if equal_nat fm zero_nat then Le (CN (zero_nat, c, Neg e)) |
1784 (if equal_nat vd zero_nat then Le (CN (zero_nat, c, Neg e)) |
1793 else Ge (CN (suc (minus_nat fm one_nat), c, e))) |
1785 else Ge (CN (suc (minus_nat vd one_nat), c, e))) |
1794 | mirror (Eq (CN (gm, c, e))) = |
1786 | mirror (Eq (CN (vd, c, e))) = |
1795 (if equal_nat gm zero_nat then Eq (CN (zero_nat, c, Neg e)) |
1787 (if equal_nat vd zero_nat then Eq (CN (zero_nat, c, Neg e)) |
1796 else Eq (CN (suc (minus_nat gm one_nat), c, e))) |
1788 else Eq (CN (suc (minus_nat vd one_nat), c, e))) |
1797 | mirror (NEq (CN (hm, c, e))) = |
1789 | mirror (NEq (CN (vd, c, e))) = |
1798 (if equal_nat hm zero_nat then NEq (CN (zero_nat, c, Neg e)) |
1790 (if equal_nat vd zero_nat then NEq (CN (zero_nat, c, Neg e)) |
1799 else NEq (CN (suc (minus_nat hm one_nat), c, e))) |
1791 else NEq (CN (suc (minus_nat vd one_nat), c, e))) |
1800 | mirror (Dvd (i, CN (im, c, e))) = |
1792 | mirror (Dvd (i, CN (ve, c, e))) = |
1801 (if equal_nat im zero_nat then Dvd (i, CN (zero_nat, c, Neg e)) |
1793 (if equal_nat ve zero_nat then Dvd (i, CN (zero_nat, c, Neg e)) |
1802 else Dvd (i, CN (suc (minus_nat im one_nat), c, e))) |
1794 else Dvd (i, CN (suc (minus_nat ve one_nat), c, e))) |
1803 | mirror (NDvd (i, CN (jm, c, e))) = |
1795 | mirror (NDvd (i, CN (ve, c, e))) = |
1804 (if equal_nat jm zero_nat then NDvd (i, CN (zero_nat, c, Neg e)) |
1796 (if equal_nat ve zero_nat then NDvd (i, CN (zero_nat, c, Neg e)) |
1805 else NDvd (i, CN (suc (minus_nat jm one_nat), c, e))); |
1797 else NDvd (i, CN (suc (minus_nat ve one_nat), c, e))); |
1806 |
1798 |
1807 fun member A_ [] y = false |
1799 fun member A_ [] y = false |
1808 | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y; |
1800 | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y; |
1809 |
1801 |
1810 fun remdups A_ [] = [] |
1802 fun remdups A_ [] = [] |
1811 | remdups A_ (x :: xs) = |
1803 | remdups A_ (x :: xs) = |
1812 (if member A_ xs x then remdups A_ xs else x :: remdups A_ xs); |
1804 (if member A_ xs x then remdups A_ xs else x :: remdups A_ xs); |
1813 |
1805 |
1814 fun zsplit0 (C c) = (zero_inta, C c) |
1806 fun zsplit0 (C c) = (zero_inta, C c) |
1815 | zsplit0 (Bound n) = |
1807 | zsplit0 (Bound n) = |
1816 (if equal_nat n zero_nat then (Int_of_integer (1 : IntInf.int), C zero_inta) |
1808 (if equal_nat n zero_nat then (one_inta, C zero_inta) |
1817 else (zero_inta, Bound n)) |
1809 else (zero_inta, Bound n)) |
1818 | zsplit0 (CN (n, i, a)) = |
1810 | zsplit0 (CN (n, i, a)) = |
1819 let |
1811 let |
1820 val aa = zsplit0 a; |
1812 val aa = zsplit0 a; |
1821 val (ia, ab) = aa; |
1813 val (ia, ab) = aa; |
1822 in |
1814 in |
1823 (if equal_nat n zero_nat then (plus_inta i ia, ab) |
1815 (if equal_nat n zero_nat then (plus_inta i ia, ab) |
1824 else (ia, CN (n, i, ab))) |
1816 else (ia, CN (n, i, ab))) |
1825 end |
1817 end |
1826 | zsplit0 (Neg a) = |
1818 | zsplit0 (Neg a) = let |
1827 let |
1819 val aa = zsplit0 a; |
1828 val aa = zsplit0 a; |
1820 val (i, ab) = aa; |
1829 val (i, ab) = aa; |
1821 in |
1830 in |
1822 (uminus_int i, Neg ab) |
1831 (uminus_int i, Neg ab) |
1823 end |
1832 end |
1824 | zsplit0 (Add (a, b)) = let |
1833 | zsplit0 (Add (a, b)) = |
1825 val aa = zsplit0 a; |
1834 let |
1826 val (ia, ab) = aa; |
1835 val aa = zsplit0 a; |
1827 val ba = zsplit0 b; |
1836 val (ia, ab) = aa; |
1828 val (ib, bb) = ba; |
1837 val ba = zsplit0 b; |
1829 in |
1838 val (ib, bb) = ba; |
1830 (plus_inta ia ib, Add (ab, bb)) |
1839 in |
1831 end |
1840 (plus_inta ia ib, Add (ab, bb)) |
1832 | zsplit0 (Sub (a, b)) = let |
1841 end |
1833 val aa = zsplit0 a; |
1842 | zsplit0 (Sub (a, b)) = |
1834 val (ia, ab) = aa; |
1843 let |
1835 val ba = zsplit0 b; |
1844 val aa = zsplit0 a; |
1836 val (ib, bb) = ba; |
1845 val (ia, ab) = aa; |
1837 in |
1846 val ba = zsplit0 b; |
1838 (minus_inta ia ib, Sub (ab, bb)) |
1847 val (ib, bb) = ba; |
1839 end |
1848 in |
1840 | zsplit0 (Mul (i, a)) = let |
1849 (minus_inta ia ib, Sub (ab, bb)) |
1841 val aa = zsplit0 a; |
1850 end |
1842 val (ia, ab) = aa; |
1851 | zsplit0 (Mul (i, a)) = |
1843 in |
1852 let |
1844 (times_inta i ia, Mul (i, ab)) |
1853 val aa = zsplit0 a; |
1845 end; |
1854 val (ia, ab) = aa; |
|
1855 in |
|
1856 (times_inta i ia, Mul (i, ab)) |
|
1857 end; |
|
1858 |
1846 |
1859 fun zlfm (And (p, q)) = And (zlfm p, zlfm q) |
1847 fun zlfm (And (p, q)) = And (zlfm p, zlfm q) |
1860 | zlfm (Or (p, q)) = Or (zlfm p, zlfm q) |
1848 | zlfm (Or (p, q)) = Or (zlfm p, zlfm q) |
1861 | zlfm (Imp (p, q)) = Or (zlfm (NOT p), zlfm q) |
1849 | zlfm (Imp (p, q)) = Or (zlfm (NOT p), zlfm q) |
1862 | zlfm (Iff (p, q)) = |
1850 | zlfm (Iff (p, q)) = |