# HG changeset patch # User chaieb # Date 1181553004 -7200 # Node ID 156db04f8af0bbf169e0d1737a946a155e6f1357 # Parent e36fc1bcb8c681754578a08ca1a0d2cd274b98b4 Removed from CVS, since obselete in the new Presburger Method; diff -r e36fc1bcb8c6 -r 156db04f8af0 src/HOL/Tools/Presburger/cooper_dec.ML --- a/src/HOL/Tools/Presburger/cooper_dec.ML Mon Jun 11 11:07:18 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,917 +0,0 @@ -(* Title: HOL/Tools/Presburger/cooper_dec.ML - ID: $Id$ - Author: Amine Chaieb and Tobias Nipkow, TU Muenchen - -The Cooper Algorithm decision procedure (intensively inspired by -J. Harrison). *) - -signature COOPER_DEC = -sig - exception COOPER - val mk_number : IntInf.int -> term - val zero : term - val one : term - val dest_number : term -> IntInf.int - val is_number : term -> bool - val is_arith_rel : term -> bool - val linear_cmul : IntInf.int -> term -> term - val linear_add : string list -> term -> term -> term - val linear_sub : string list -> term -> term -> term - val linear_neg : term -> term - val lint : string list -> term -> term - val linform : string list -> term -> term - val formlcm : term -> term -> IntInf.int - val adjustcoeff : term -> IntInf.int -> term -> term - val unitycoeff : term -> term -> term - val divlcm : term -> term -> IntInf.int - val bset : term -> term -> term list - val aset : term -> term -> term list - val linrep : string list -> term -> term -> term -> term - val list_disj : term list -> term - val list_conj : term list -> term - val simpl : term -> term - val fv : term -> string list - val negate : term -> term - val operations : (string * (IntInf.int * IntInf.int -> bool)) list - val conjuncts : term -> term list - val disjuncts : term -> term list - val has_bound : term -> bool - val minusinf : term -> term -> term - val plusinf : term -> term -> term - val onatoms : (term -> term) -> term -> term - val evalc : term -> term - val cooper_w : string list -> term -> (term option * term) - val integer_qelim : Term.term -> Term.term -end; - -structure CooperDec : COOPER_DEC = -struct - -(* ========================================================================= *) -(* Cooper's algorithm for Presburger arithmetic. *) -(* ========================================================================= *) -exception COOPER; - - -(* ------------------------------------------------------------------------- *) -(* Lift operations up to numerals. *) -(* ------------------------------------------------------------------------- *) - -(*Assumption : The construction of atomar formulas in linearl arithmetic is based on -relation operations of Type : [IntInf.int,IntInf.int]---> bool *) - -(* ------------------------------------------------------------------------- *) - -(*Function is_arith_rel returns true if and only if the term is an atomar presburger -formula *) -fun is_arith_rel tm = case tm - of Const(p, Type ("fun", [Type ("IntDef.int", []), Type ("fun", [Type ("IntDef.int", []), - Type ("bool", [])])])) $ _ $_ => true - | _ => false; - -(*Function is_arith_rel returns true if and only if the term is an operation of the -form [int,int]---> int*) - -val mk_number = HOLogic.mk_number HOLogic.intT; -val zero = mk_number 0; -val one = mk_number 1; -fun dest_number t = let - val (T, n) = HOLogic.dest_number t - in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end; -val is_number = can dest_number; - -(*maps a unary natural function on a term containing an natural number*) -fun numeral1 f n = mk_number (f (dest_number n)); - -(*maps a binary natural function on 2 term containing natural numbers*) -fun numeral2 f m n = mk_number (f (dest_number m) (dest_number n)); - -(* ------------------------------------------------------------------------- *) -(* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *) -(* *) -(* Note that we're quite strict: the ci must be present even if 1 *) -(* (but if 0 we expect the monomial to be omitted) and k must be there *) -(* even if it's zero. Thus, it's a constant iff not an addition term. *) -(* ------------------------------------------------------------------------- *) - - -fun linear_cmul n tm = if n = 0 then zero else let fun times n k = n*k in - ( case tm of - (Const(@{const_name HOL.plus},T) $ (Const (@{const_name HOL.times},T1 ) $c1 $ x1) $ rest) => - Const(@{const_name HOL.plus},T) $ ((Const(@{const_name HOL.times},T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) - |_ => numeral1 (times n) tm) - end ; - - - - -(* Whether the first of two items comes earlier in the list *) -fun earlier [] x y = false - |earlier (h::t) x y =if h = y then false - else if h = x then true - else earlier t x y ; - -fun earlierv vars (Bound i) (Bound j) = i < j - |earlierv vars (Bound _) _ = true - |earlierv vars _ (Bound _) = false - |earlierv vars (Free (x,_)) (Free (y,_)) = earlier vars x y; - - -fun linear_add vars tm1 tm2 = - let fun addwith x y = x + y in - (case (tm1,tm2) of - ((Const (@{const_name HOL.plus},T1) $ ( Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1),(Const - (@{const_name HOL.plus},T3)$( Const(@{const_name HOL.times},T4) $ c2 $ x2) $ rest2)) => - if x1 = x2 then - let val c = (numeral2 (addwith) c1 c2) - in - if c = zero then (linear_add vars rest1 rest2) - else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c $ x1) $ (linear_add vars rest1 rest2)) - end - else - if earlierv vars x1 x2 then (Const(@{const_name HOL.plus},T1) $ - (Const(@{const_name HOL.times},T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) - else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) - |((Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1) ,_) => - (Const(@{const_name HOL.plus},T1)$ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ (linear_add vars - rest1 tm2)) - |(_, (Const(@{const_name HOL.plus},T1) $(Const(@{const_name HOL.times},T2) $ c2 $ x2) $ rest2)) => - (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 - rest2)) - | (_,_) => numeral2 (addwith) tm1 tm2) - - end; - -(*To obtain the unary - applyed on a formula*) - -fun linear_neg tm = linear_cmul (0 - 1) tm; - -(*Substraction of two terms *) - -fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); - - -(* ------------------------------------------------------------------------- *) -(* Linearize a term. *) -(* ------------------------------------------------------------------------- *) - -(* linearises a term from the point of view of Variable Free (x,T). -After this fuction the all expressions containig ths variable will have the form - c*Free(x,T) + t where c is a constant ant t is a Term which is not containing - Free(x,T)*) - -fun lint vars tm = if is_number tm then tm else case tm of - (Free (x,T)) => (HOLogic.mk_binop @{const_name HOL.plus} ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1),Free (x,T))), zero)) - |(Bound i) => (Const(@{const_name HOL.plus},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ - (Const(@{const_name HOL.times},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) - |(Const(@{const_name HOL.uminus},_) $ t ) => (linear_neg (lint vars t)) - |(Const(@{const_name HOL.plus},_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) - |(Const(@{const_name HOL.minus},_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) - |(Const (@{const_name HOL.times},_) $ s $ t) => - let val s' = lint vars s - val t' = lint vars t - in - if is_number s' then (linear_cmul (dest_number s') t') - else if is_number t' then (linear_cmul (dest_number t') s') - - else raise COOPER - end - |_ => raise COOPER; - - - -(* ------------------------------------------------------------------------- *) -(* Linearize the atoms in a formula, and eliminate non-strict inequalities. *) -(* ------------------------------------------------------------------------- *) - -fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); - -fun linform vars (Const ("Divides.dvd",_) $ c $ t) = - if is_number c then - let val c' = (mk_number(abs(dest_number c))) - in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) - end - else (warning "Nonlinear term --- Non numeral leftside at dvd" - ;raise COOPER) - |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) - |linform vars (Const(@{const_name Orderings.less},_)$ s $t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s)) - |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) - |linform vars (Const(@{const_name Orderings.less_eq},_)$ s $ t ) = - (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) - |linform vars (Const("op >=",_)$ s $ t ) = - (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> - HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> - HOLogic.intT) $s $(mk_number 1)) $ t)) - - |linform vars fm = fm; - -(* ------------------------------------------------------------------------- *) -(* Post-NNF transformation eliminating negated inequalities. *) -(* ------------------------------------------------------------------------- *) - -fun posineq fm = case fm of - (Const ("Not",_)$(Const(@{const_name Orderings.less},_)$ c $ t)) => - (HOLogic.mk_binrel @{const_name Orderings.less} (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) - | ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q) - | ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q) - | _ => fm; - - -(* ------------------------------------------------------------------------- *) -(* Find the LCM of the coefficients of x. *) -(* ------------------------------------------------------------------------- *) -(*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) - -fun gcd (a:IntInf.int) b = if a=0 then b else gcd (b mod a) a ; -fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); - -fun formlcm x fm = case fm of - (Const (p,_)$ _ $(Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_)$ c $ y ) $z ) ) => if - (is_arith_rel fm) andalso (x = y) then (abs(dest_number c)) else 1 - | ( Const ("Not", _) $p) => formlcm x p - | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) - | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) - | _ => 1; - -(* ------------------------------------------------------------------------- *) -(* Adjust all coefficients of x in formula; fold in reduction to +/- 1. *) -(* ------------------------------------------------------------------------- *) - -fun adjustcoeff x l fm = - case fm of - (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ - c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then - let val m = l div (dest_number c) - val n = (if p = @{const_name Orderings.less} then abs(m) else m) - val xtm = HOLogic.mk_binop @{const_name HOL.times} ((mk_number (m div n)), x) - in - (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) - end - else fm - |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) - |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeff x l p) $(adjustcoeff x l q) - |( Const ("op |",_) $ p $ q) => HOLogic.disj $(adjustcoeff x l p)$ (adjustcoeff x l q) - |_ => fm; - -(* ------------------------------------------------------------------------- *) -(* Hence make coefficient of x one in existential formula. *) -(* ------------------------------------------------------------------------- *) - -fun unitycoeff x fm = - let val l = formlcm x fm - val fm' = adjustcoeff x l fm in - if l = 1 then fm' - else - let val xp = (HOLogic.mk_binop @{const_name HOL.plus} - ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1), x )), zero)) - in - HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm) - end - end; - -(* adjustcoeffeq l fm adjusts the coeffitients c_i of x overall in fm to l*) -(* Here l must be a multiple of all c_i otherwise the obtained formula is not equivalent*) -(* -fun adjustcoeffeq x l fm = - case fm of - (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ - c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then - let val m = l div (dest_number c) - val n = (if p = @{const_name Orderings.less} then abs(m) else m) - val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x)) - in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) - end - else fm - |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) - |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeffeq x l p) $(adjustcoeffeq x l q) - |( Const ("op |",_) $ p $ q) => HOLogic.disj $(adjustcoeffeq x l p)$ (adjustcoeffeq x l q) - |_ => fm; - - -*) - -(* ------------------------------------------------------------------------- *) -(* The "minus infinity" version. *) -(* ------------------------------------------------------------------------- *) - -fun minusinf x fm = case fm of - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => - if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const - else fm - - |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z - )) => if (x = y) - then if (pm1 = one) andalso (c = zero) then HOLogic.false_const - else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const - else error "minusinf : term not in normal form!!!" - else fm - - |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) - |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) - |(Const ("op |",_) $ p $ q) => HOLogic.disj $ (minusinf x p) $ (minusinf x q) - |_ => fm; - -(* ------------------------------------------------------------------------- *) -(* The "Plus infinity" version. *) -(* ------------------------------------------------------------------------- *) - -fun plusinf x fm = case fm of - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => - if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const - else fm - - |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z - )) => if (x = y) - then if (pm1 = one) andalso (c = zero) then HOLogic.true_const - else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const - else error "plusinf : term not in normal form!!!" - else fm - - |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p) - |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q) - |(Const ("op |",_) $ p $ q) => HOLogic.disj $ (plusinf x p) $ (plusinf x q) - |_ => fm; - -(* ------------------------------------------------------------------------- *) -(* The LCM of all the divisors that involve x. *) -(* ------------------------------------------------------------------------- *) - -fun divlcm x (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z ) ) = - if x = y then abs(dest_number d) else 1 - |divlcm x ( Const ("Not", _) $ p) = divlcm x p - |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) - |divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q) - |divlcm x _ = 1; - -(* ------------------------------------------------------------------------- *) -(* Construct the B-set. *) -(* ------------------------------------------------------------------------- *) - -fun bset x fm = case fm of - (Const ("Not", _) $ p) => if (is_arith_rel p) then - (case p of - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) ) - => if (is_arith_rel p) andalso (x= y) andalso (c2 = one) andalso (c1 = zero) - then [linear_neg a] - else bset x p - |_ =>[]) - - else bset x p - |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))] else [] - |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] - |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) - |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) - |_ => []; - -(* ------------------------------------------------------------------------- *) -(* Construct the A-set. *) -(* ------------------------------------------------------------------------- *) - -fun aset x fm = case fm of - (Const ("Not", _) $ p) => if (is_arith_rel p) then - (case p of - (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) ) - => if (x= y) andalso (c2 = one) andalso (c1 = zero) - then [linear_neg a] - else [] - |_ =>[]) - - else aset x p - |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a] else [] - |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else [] - |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q) - |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q) - |_ => []; - - -(* ------------------------------------------------------------------------- *) -(* Replace top variable with another linear form, retaining canonicality. *) -(* ------------------------------------------------------------------------- *) - -fun linrep vars x t fm = case fm of - ((Const(p,_)$ d $ (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$ c $ y) $ z))) => - if (x = y) andalso (is_arith_rel fm) - then - let val ct = linear_cmul (dest_number c) t - in (HOLogic.mk_binrel p (d, linear_add vars ct z)) - end - else fm - |(Const ("Not", _) $ p) => HOLogic.Not $ (linrep vars x t p) - |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (linrep vars x t p) $ (linrep vars x t q) - |(Const ("op |",_) $ p $ q) => HOLogic.disj $ (linrep vars x t p) $ (linrep vars x t q) - |_ => fm; - -(* ------------------------------------------------------------------------- *) -(* Evaluation of constant expressions. *) -(* ------------------------------------------------------------------------- *) - -(* An other implementation of divides, that covers more cases*) - -exception DVD_UNKNOWN - -fun dvd_op (d, t) = - if not(is_number d) then raise DVD_UNKNOWN - else let - val dn = dest_number d - fun coeffs_of x = case x of - Const(p,_) $ tl $ tr => - if p = @{const_name HOL.plus} then (coeffs_of tl) union (coeffs_of tr) - else if p = @{const_name HOL.times} - then if (is_number tr) - then [(dest_number tr) * (dest_number tl)] - else [dest_number tl] - else [] - |_ => if (is_number t) then [dest_number t] else [] - val ts = coeffs_of t - in case ts of - [] => raise DVD_UNKNOWN - |_ => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true - end; - - -val operations = - [("op =",op=), (@{const_name Orderings.less},IntInf.<), ("op >",IntInf.>), (@{const_name Orderings.less_eq},IntInf.<=) , - ("op >=",IntInf.>=), - ("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; - -fun applyoperation (SOME f) (a,b) = f (a, b) - |applyoperation _ (_, _) = false; - -(*Evaluation of constant atomic formulas*) - (*FIXME : This is an optimation but still incorrect !! *) -(* -fun evalc_atom at = case at of - (Const (p,_) $ s $ t) => - (if p="Divides.dvd" then - ((if dvd_op(s,t) then HOLogic.true_const - else HOLogic.false_const) - handle _ => at) - else - case AList.lookup (op =) operations p of - SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const else HOLogic.false_const) - handle _ => at) - | _ => at) - |Const("Not",_)$(Const (p,_) $ s $ t) =>( - case AList.lookup (op =) operations p of - SOME f => ((if (f ((dest_number s),(dest_number t))) then - HOLogic.false_const else HOLogic.true_const) - handle _ => at) - | _ => at) - | _ => at; - -*) - -fun evalc_atom at = case at of - (Const (p,_) $ s $ t) => - ( case AList.lookup (op =) operations p of - SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const - else HOLogic.false_const) - handle _ => at) - | _ => at) - |Const("Not",_)$(Const (p,_) $ s $ t) =>( - case AList.lookup (op =) operations p of - SOME f => ((if (f ((dest_number s),(dest_number t))) - then HOLogic.false_const else HOLogic.true_const) - handle _ => at) - | _ => at) - | _ => at; - - (*Function onatoms apllys function f on the atomic formulas involved in a.*) - -fun onatoms f a = if (is_arith_rel a) then f a else case a of - - (Const ("Not",_) $ p) => if is_arith_rel p then HOLogic.Not $ (f p) - - else HOLogic.Not $ (onatoms f p) - |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (onatoms f p) $ (onatoms f q) - |(Const ("op |",_) $ p $ q) => HOLogic.disj $ (onatoms f p) $ (onatoms f q) - |(Const ("op -->",_) $ p $ q) => HOLogic.imp $ (onatoms f p) $ (onatoms f q) - |((Const ("op =", Type ("fun",[Type ("bool", []),_]))) $ p $ q) => (Const ("op =", [HOLogic.boolT, HOLogic.boolT] ---> HOLogic.boolT)) $ (onatoms f p) $ (onatoms f q) - |(Const("All",_) $ Abs(x,T,p)) => Const("All", [HOLogic.intT --> - HOLogic.boolT] ---> HOLogic.boolT)$ Abs (x ,T, (onatoms f p)) - |(Const("Ex",_) $ Abs(x,T,p)) => Const("Ex", [HOLogic.intT --> HOLogic.boolT]---> HOLogic.boolT) $ Abs( x ,T, (onatoms f p)) - |_ => a; - -val evalc = onatoms evalc_atom; - -(* ------------------------------------------------------------------------- *) -(* Hence overall quantifier elimination. *) -(* ------------------------------------------------------------------------- *) - - -(*list_disj[conj] makes a disj[conj] of a given list. used with conjucts or disjuncts -it liearises iterated conj[disj]unctions. *) - -fun list_disj [] = HOLogic.false_const - | list_disj ps = foldr1 (fn (p, q) => HOLogic.disj $ p $ q) ps; - -fun list_conj [] = HOLogic.true_const - | list_conj ps = foldr1 (fn (p, q) => HOLogic.conj $ p $ q) ps; - - -(*Simplification of Formulas *) - -(*Function q_bnd_chk checks if a quantified Formula makes sens : Means if in -the body of the existential quantifier there are bound variables to the -existential quantifier.*) - -fun has_bound fm =let fun has_boundh fm i = case fm of - Bound n => (i = n) - |Abs (_,_,p) => has_boundh p (i+1) - |t1 $ t2 => (has_boundh t1 i) orelse (has_boundh t2 i) - |_ =>false - -in case fm of - Bound _ => true - |Abs (_,_,p) => has_boundh p 0 - |t1 $ t2 => (has_bound t1 ) orelse (has_bound t2 ) - |_ =>false -end; - -(*has_sub_abs checks if in a given Formula there are subformulas which are quantifed -too. Is no used no more.*) - -fun has_sub_abs fm = case fm of - Abs (_,_,_) => true - |t1 $ t2 => (has_bound t1 ) orelse (has_bound t2 ) - |_ =>false ; - -(*update_bounds called with i=0 udates the numeration of bounded variables because the -formula will not be quantified any more.*) - -fun update_bounds fm i = case fm of - Bound n => if n >= i then Bound (n-1) else fm - |Abs (x,T,p) => Abs(x,T,(update_bounds p (i+1))) - |t1 $ t2 => (update_bounds t1 i) $ (update_bounds t2 i) - |_ => fm ; - -(*psimpl : Simplification of propositions (general purpose)*) -fun psimpl1 fm = case fm of - Const("Not",_) $ Const ("False",_) => HOLogic.true_const - | Const("Not",_) $ Const ("True",_) => HOLogic.false_const - | Const("op &",_) $ Const ("False",_) $ q => HOLogic.false_const - | Const("op &",_) $ p $ Const ("False",_) => HOLogic.false_const - | Const("op &",_) $ Const ("True",_) $ q => q - | Const("op &",_) $ p $ Const ("True",_) => p - | Const("op |",_) $ Const ("False",_) $ q => q - | Const("op |",_) $ p $ Const ("False",_) => p - | Const("op |",_) $ Const ("True",_) $ q => HOLogic.true_const - | Const("op |",_) $ p $ Const ("True",_) => HOLogic.true_const - | Const("op -->",_) $ Const ("False",_) $ q => HOLogic.true_const - | Const("op -->",_) $ Const ("True",_) $ q => q - | Const("op -->",_) $ p $ Const ("True",_) => HOLogic.true_const - | Const("op -->",_) $ p $ Const ("False",_) => HOLogic.Not $ p - | Const("op =", Type ("fun",[Type ("bool", []),_])) $ Const ("True",_) $ q => q - | Const("op =", Type ("fun",[Type ("bool", []),_])) $ p $ Const ("True",_) => p - | Const("op =", Type ("fun",[Type ("bool", []),_])) $ Const ("False",_) $ q => HOLogic.Not $ q - | Const("op =", Type ("fun",[Type ("bool", []),_])) $ p $ Const ("False",_) => HOLogic.Not $ p - | _ => fm; - -fun psimpl fm = case fm of - Const ("Not",_) $ p => psimpl1 (HOLogic.Not $ (psimpl p)) - | Const("op &",_) $ p $ q => psimpl1 (HOLogic.mk_conj (psimpl p,psimpl q)) - | Const("op |",_) $ p $ q => psimpl1 (HOLogic.mk_disj (psimpl p,psimpl q)) - | Const("op -->",_) $ p $ q => psimpl1 (HOLogic.mk_imp(psimpl p,psimpl q)) - | Const("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q => psimpl1 (HOLogic.mk_eq(psimpl p,psimpl q)) - | _ => fm; - - -(*simpl : Simplification of Terms involving quantifiers too. - This function is able to drop out some quantified expressions where there are no - bound varaibles.*) - -fun simpl1 fm = - case fm of - Const("All",_) $Abs(x,_,p) => if (has_bound fm ) then fm - else (update_bounds p 0) - | Const("Ex",_) $ Abs (x,_,p) => if has_bound fm then fm - else (update_bounds p 0) - | _ => psimpl fm; - -fun simpl fm = case fm of - Const ("Not",_) $ p => simpl1 (HOLogic.Not $(simpl p)) - | Const ("op &",_) $ p $ q => simpl1 (HOLogic.mk_conj (simpl p ,simpl q)) - | Const ("op |",_) $ p $ q => simpl1 (HOLogic.mk_disj (simpl p ,simpl q )) - | Const ("op -->",_) $ p $ q => simpl1 (HOLogic.mk_imp(simpl p ,simpl q )) - | Const("op =", Type ("fun",[Type ("bool", []),_]))$ p $ q => simpl1 - (HOLogic.mk_eq(simpl p ,simpl q )) -(* | Const ("All",Ta) $ Abs(Vn,VT,p) => simpl1(Const("All",Ta) $ - Abs(Vn,VT,simpl p )) - | Const ("Ex",Ta) $ Abs(Vn,VT,p) => simpl1(Const("Ex",Ta) $ - Abs(Vn,VT,simpl p )) -*) - | _ => fm; - -(* ------------------------------------------------------------------------- *) - -(* Puts fm into NNF*) - -fun nnf fm = if (is_arith_rel fm) then fm -else (case fm of - ( Const ("op &",_) $ p $ q) => HOLogic.conj $ (nnf p) $(nnf q) - | (Const("op |",_) $ p $q) => HOLogic.disj $ (nnf p)$(nnf q) - | (Const ("op -->",_) $ p $ q) => HOLogic.disj $ (nnf (HOLogic.Not $ p)) $ (nnf q) - | ((Const ("op =", Type ("fun",[Type ("bool", []),_]))) $ p $ q) =>(HOLogic.disj $ (HOLogic.conj $ (nnf p) $ (nnf q)) $ (HOLogic.conj $ (nnf (HOLogic.Not $ p) ) $ (nnf(HOLogic.Not $ q)))) - | (Const ("Not",_)) $ ((Const ("Not",_)) $ p) => (nnf p) - | (Const ("Not",_)) $ (( Const ("op &",_)) $ p $ q) =>HOLogic.disj $ (nnf(HOLogic.Not $ p)) $ (nnf(HOLogic.Not $q)) - | (Const ("Not",_)) $ (( Const ("op |",_)) $ p $ q) =>HOLogic.conj $ (nnf(HOLogic.Not $ p)) $ (nnf(HOLogic.Not $ q)) - | (Const ("Not",_)) $ (( Const ("op -->",_)) $ p $ q ) =>HOLogic.conj $ (nnf p) $(nnf(HOLogic.Not $ q)) - | (Const ("Not",_)) $ ((Const ("op =", Type ("fun",[Type ("bool", []),_]))) $ p $ q ) =>(HOLogic.disj $ (HOLogic.conj $(nnf p) $ (nnf(HOLogic.Not $ q))) $ (HOLogic.conj $(nnf(HOLogic.Not $ p)) $ (nnf q))) - | _ => fm); - - -(* Function remred to remove redundancy in a list while keeping the order of appearance of the -elements. but VERY INEFFICIENT!! *) - -fun remred1 el [] = [] - |remred1 el (h::t) = if el=h then (remred1 el t) else h::(remred1 el t); - -fun remred [] = [] - |remred (x::l) = x::(remred1 x (remred l)); - -(*Makes sure that all free Variables are of the type integer but this function is only -used temporarily, this job must be done by the parser later on.*) - -fun mk_uni_vars T (node $ rest) = (case node of - Free (name,_) => Free (name,T) $ (mk_uni_vars T rest) - |_=> (mk_uni_vars T node) $ (mk_uni_vars T rest ) ) - |mk_uni_vars T (Free (v,_)) = Free (v,T) - |mk_uni_vars T tm = tm; - -fun mk_uni_int T (Const (@{const_name HOL.zero},T2)) = if T = T2 then (mk_number 0) else (Const (@{const_name HOL.zero},T2)) - |mk_uni_int T (Const (@{const_name HOL.one},T2)) = if T = T2 then (mk_number 1) else (Const (@{const_name HOL.one},T2)) - |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest ) - |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) - |mk_uni_int T tm = tm; - - -(* Minusinfinity Version*) -fun myupto (m:IntInf.int) n = if m > n then [] else m::(myupto (m+1) n) - -fun coopermi vars1 fm = - case fm of - Const ("Ex",_) $ Abs(x0,T,p0) => - let - val (xn,p1) = Syntax.variant_abs (x0,T,p0) - val x = Free (xn,T) - val vars = (xn::vars1) - val p = unitycoeff x (posineq (simpl p1)) - val p_inf = simpl (minusinf x p) - val bset = bset x p - val js = myupto 1 (divlcm x p) - fun p_element j b = linrep vars x (linear_add vars b (mk_number j)) p - fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) bset) - in (list_disj (map stage js)) - end - | _ => error "cooper: not an existential formula"; - - - -(* The plusinfinity version of cooper*) -fun cooperpi vars1 fm = - case fm of - Const ("Ex",_) $ Abs(x0,T,p0) => let - val (xn,p1) = Syntax.variant_abs (x0,T,p0) - val x = Free (xn,T) - val vars = (xn::vars1) - val p = unitycoeff x (posineq (simpl p1)) - val p_inf = simpl (plusinf x p) - val aset = aset x p - val js = myupto 1 (divlcm x p) - fun p_element j a = linrep vars x (linear_sub vars a (mk_number j)) p - fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) aset) - in (list_disj (map stage js)) - end - | _ => error "cooper: not an existential formula"; - - -(* Try to find a withness for the formula *) - -fun inf_w mi d vars x p = - let val f = if mi then minusinf else plusinf in - case (simpl (minusinf x p)) of - Const("True",_) => (SOME (mk_number 1), HOLogic.true_const) - |Const("False",_) => (NONE,HOLogic.false_const) - |F => - let - fun h n = - case ((simpl o evalc) (linrep vars x (mk_number n) F)) of - Const("True",_) => (SOME (mk_number n),HOLogic.true_const) - |F' => if n=1 then (NONE,F') - else let val (rw,rf) = h (n-1) in - (rw,HOLogic.mk_disj(F',rf)) - end - - in (h d) - end - end; - -fun set_w d b st vars x p = let - fun h ns = case ns of - [] => (NONE,HOLogic.false_const) - |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of - Const("True",_) => (SOME n,HOLogic.true_const) - |F' => let val (rw,rf) = h nl - in (rw,HOLogic.mk_disj(F',rf)) - end) - val f = if b then linear_add else linear_sub - val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_number i)) st)) (myupto 1 d) [] - in h p_elements - end; - -fun withness d b st vars x p = case (inf_w b d vars x p) of - (SOME n,_) => (SOME n,HOLogic.true_const) - |(NONE,Pinf) => (case (set_w d b st vars x p) of - (SOME n,_) => (SOME n,HOLogic.true_const) - |(_,Pst) => (NONE,HOLogic.mk_disj(Pinf,Pst))); - - - - -(*Cooper main procedure*) - -exception STAGE_TRUE; - - -fun cooper vars1 fm = - case fm of - Const ("Ex",_) $ Abs(x0,T,p0) => let - val (xn,p1) = Syntax.variant_abs (x0,T,p0) - val x = Free (xn,T) - val vars = (xn::vars1) -(* val p = unitycoeff x (posineq (simpl p1)) *) - val p = unitycoeff x p1 - val ast = aset x p - val bst = bset x p - val js = myupto 1 (divlcm x p) - val (p_inf,f,S ) = - if (length bst) <= (length ast) - then (simpl (minusinf x p),linear_add,bst) - else (simpl (plusinf x p), linear_sub,ast) - fun p_element j a = linrep vars x (f vars a (mk_number j)) p - fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S) - fun stageh n = ((if n = 0 then [] - else - let - val nth_stage = simpl (evalc (stage n)) - in - if (nth_stage = HOLogic.true_const) - then raise STAGE_TRUE - else if (nth_stage = HOLogic.false_const) then stageh (n-1) - else nth_stage::(stageh (n-1)) - end ) - handle STAGE_TRUE => [HOLogic.true_const]) - val slist = stageh (divlcm x p) - in (list_disj slist) - end - | _ => error "cooper: not an existential formula"; - - -(* A Version of cooper that returns a withness *) -fun cooper_w vars1 fm = - case fm of - Const ("Ex",_) $ Abs(x0,T,p0) => let - val (xn,p1) = Syntax.variant_abs (x0,T,p0) - val x = Free (xn,T) - val vars = (xn::vars1) -(* val p = unitycoeff x (posineq (simpl p1)) *) - val p = unitycoeff x p1 - val ast = aset x p - val bst = bset x p - val d = divlcm x p - val (p_inf,S ) = - if (length bst) <= (length ast) - then (true,bst) - else (false,ast) - in withness d p_inf S vars x p -(* fun p_element j a = linrep vars x (f vars a (mk_number j)) p - fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S) - in (list_disj (map stage js)) -*) - end - | _ => error "cooper: not an existential formula"; - - -(* ------------------------------------------------------------------------- *) -(* Free variables in terms and formulas. *) -(* ------------------------------------------------------------------------- *) - -fun fvt tml = case tml of - [] => [] - | Free(x,_)::r => x::(fvt r) - -fun fv fm = fvt (term_frees fm); - - -(* ========================================================================= *) -(* Quantifier elimination. *) -(* ========================================================================= *) -(*conj[/disj]uncts lists iterated conj[disj]unctions*) - -fun disjuncts fm = case fm of - Const ("op |",_) $ p $ q => (disjuncts p) @ (disjuncts q) - | _ => [fm]; - -fun conjuncts fm = case fm of - Const ("op &",_) $p $ q => (conjuncts p) @ (conjuncts q) - | _ => [fm]; - - - -(* ------------------------------------------------------------------------- *) -(* Lift procedure given literal modifier, formula normalizer & basic quelim. *) -(* ------------------------------------------------------------------------- *) - -fun lift_qelim afn nfn qfn isat = -let -fun qelift vars fm = if (isat fm) then afn vars fm -else -case fm of - Const ("Not",_) $ p => HOLogic.Not $ (qelift vars p) - | Const ("op &",_) $ p $q => HOLogic.conj $ (qelift vars p) $ (qelift vars q) - | Const ("op |",_) $ p $ q => HOLogic.disj $ (qelift vars p) $ (qelift vars q) - | Const ("op -->",_) $ p $ q => HOLogic.imp $ (qelift vars p) $ (qelift vars q) - | Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q => HOLogic.mk_eq ((qelift vars p),(qelift vars q)) - | Const ("All",QT) $ Abs(x,T,p) => HOLogic.Not $(qelift vars (Const ("Ex",QT) $ Abs(x,T,(HOLogic.Not $ p)))) - | (e as Const ("Ex",_)) $ Abs (x,T,p) => qfn vars (e$Abs (x,T,(nfn(qelift (x::vars) p)))) - | _ => fm - -in (fn fm => qelift (fv fm) fm) -end; - - -(* -fun lift_qelim afn nfn qfn isat = - let fun qelim x vars p = - let val cjs = conjuncts p - val (ycjs,ncjs) = List.partition (has_bound) cjs in - (if ycjs = [] then p else - let val q = (qfn vars ((HOLogic.exists_const HOLogic.intT - ) $ Abs(x,HOLogic.intT,(list_conj ycjs)))) in - (fold_rev conj_help ncjs q) - end) - end - - fun qelift vars fm = if (isat fm) then afn vars fm - else - case fm of - Const ("Not",_) $ p => HOLogic.Not $ (qelift vars p) - | Const ("op &",_) $ p $q => HOLogic.conj $ (qelift vars p) $ (qelift vars q) - | Const ("op |",_) $ p $ q => HOLogic.disj $ (qelift vars p) $ (qelift vars q) - | Const ("op -->",_) $ p $ q => HOLogic.imp $ (qelift vars p) $ (qelift vars q) - | Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q => HOLogic.mk_eq ((qelift vars p),(qelift vars q)) - | Const ("All",QT) $ Abs(x,T,p) => HOLogic.Not $(qelift vars (Const ("Ex",QT) $ Abs(x,T,(HOLogic.Not $ p)))) - | Const ("Ex",_) $ Abs (x,T,p) => let val djs = disjuncts(nfn(qelift (x::vars) p)) in - list_disj(map (qelim x vars) djs) end - | _ => fm - - in (fn fm => simpl(qelift (fv fm) fm)) - end; -*) - -(* ------------------------------------------------------------------------- *) -(* Cleverer (proposisional) NNF with conditional and literal modification. *) -(* ------------------------------------------------------------------------- *) - -(*Function Negate used by cnnf, negates a formula p*) - -fun negate (Const ("Not",_) $ p) = p - |negate p = (HOLogic.Not $ p); - -fun cnnf lfn = - let fun cnnfh fm = case fm of - (Const ("op &",_) $ p $ q) => HOLogic.mk_conj(cnnfh p,cnnfh q) - | (Const ("op |",_) $ p $ q) => HOLogic.mk_disj(cnnfh p,cnnfh q) - | (Const ("op -->",_) $ p $q) => HOLogic.mk_disj(cnnfh(HOLogic.Not $ p),cnnfh q) - | (Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q) => HOLogic.mk_disj( - HOLogic.mk_conj(cnnfh p,cnnfh q), - HOLogic.mk_conj(cnnfh(HOLogic.Not $ p),cnnfh(HOLogic.Not $q))) - - | (Const ("Not",_) $ (Const("Not",_) $ p)) => cnnfh p - | (Const ("Not",_) $ (Const ("op &",_) $ p $ q)) => HOLogic.mk_disj(cnnfh(HOLogic.Not $ p),cnnfh(HOLogic.Not $ q)) - | (Const ("Not",_) $(Const ("op |",_) $ (Const ("op &",_) $ p $ q) $ - (Const ("op &",_) $ p1 $ r))) => if p1 = negate p then - HOLogic.mk_disj( - cnnfh (HOLogic.mk_conj(p,cnnfh(HOLogic.Not $ q))), - cnnfh (HOLogic.mk_conj(p1,cnnfh(HOLogic.Not $ r)))) - else HOLogic.mk_conj( - cnnfh (HOLogic.mk_disj(cnnfh (HOLogic.Not $ p),cnnfh(HOLogic.Not $ q))), - cnnfh (HOLogic.mk_disj(cnnfh (HOLogic.Not $ p1),cnnfh(HOLogic.Not $ r))) - ) - | (Const ("Not",_) $ (Const ("op |",_) $ p $ q)) => HOLogic.mk_conj(cnnfh(HOLogic.Not $ p),cnnfh(HOLogic.Not $ q)) - | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) => HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not $ q)) - | (Const ("Not",_) $ (Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q)) => HOLogic.mk_disj(HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not $ q)),HOLogic.mk_conj(cnnfh(HOLogic.Not $ p),cnnfh q)) - | _ => lfn fm -in cnnfh - end; - -(*End- function the quantifierelimination an decion procedure of presburger formulas.*) - -(* -val integer_qelim = simpl o evalc o (lift_qelim linform (simpl o (cnnf posineq o evalc)) cooper is_arith_rel) ; -*) - - -val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; - -end; diff -r e36fc1bcb8c6 -r 156db04f8af0 src/HOL/Tools/Presburger/cooper_proof.ML --- a/src/HOL/Tools/Presburger/cooper_proof.ML Mon Jun 11 11:07:18 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,988 +0,0 @@ -(* Title: HOL/Tools/Presburger/cooper_proof.ML - ID: $Id$ - Author: Amine Chaieb and Tobias Nipkow, TU Muenchen - -File containing the implementation of the proof -generation for Cooper Algorithm -*) - - -signature COOPER_PROOF = -sig - val qe_Not : thm - val qe_conjI : thm - val qe_disjI : thm - val qe_impI : thm - val qe_eqI : thm - val qe_exI : thm - val list_to_set : typ -> term list -> term - val qe_get_terms : thm -> term * term - val cooper_prv : theory -> term -> term -> thm - val proof_of_evalc : theory -> term -> thm - val proof_of_cnnf : theory -> term -> (term -> thm) -> thm - val proof_of_linform : theory -> string list -> term -> thm - val proof_of_adjustcoeffeq : theory -> term -> IntInf.int -> term -> thm - val prove_elementar : theory -> string -> term -> thm - val thm_of : theory -> (term -> (term list * (thm list -> thm))) -> term -> thm -end; - -structure CooperProof : COOPER_PROOF = -struct -open CooperDec; - -val presburger_ss = simpset () - addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"]; - -val cboolT = ctyp_of HOL.thy HOLogic.boolT; - -(*Theorems that will be used later for the proofgeneration*) - -val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0"; -val unity_coeff_ex = thm "unity_coeff_ex"; - -(* Theorems for proving the adjustment of the coefficients*) - -val ac_lt_eq = thm "ac_lt_eq"; -val ac_eq_eq = thm "ac_eq_eq"; -val ac_dvd_eq = thm "ac_dvd_eq"; -val ac_pi_eq = thm "ac_pi_eq"; - -(* The logical compination of the sythetised properties*) -val qe_Not = thm "qe_Not"; -val qe_conjI = thm "qe_conjI"; -val qe_disjI = thm "qe_disjI"; -val qe_impI = thm "qe_impI"; -val qe_eqI = thm "qe_eqI"; -val qe_exI = thm "qe_exI"; -val qe_ALLI = thm "qe_ALLI"; - -(*Modulo D property for Pminusinf an Plusinf *) -val fm_modd_minf = thm "fm_modd_minf"; -val not_dvd_modd_minf = thm "not_dvd_modd_minf"; -val dvd_modd_minf = thm "dvd_modd_minf"; - -val fm_modd_pinf = thm "fm_modd_pinf"; -val not_dvd_modd_pinf = thm "not_dvd_modd_pinf"; -val dvd_modd_pinf = thm "dvd_modd_pinf"; - -(* the minusinfinity proprty*) - -val fm_eq_minf = thm "fm_eq_minf"; -val neq_eq_minf = thm "neq_eq_minf"; -val eq_eq_minf = thm "eq_eq_minf"; -val le_eq_minf = thm "le_eq_minf"; -val len_eq_minf = thm "len_eq_minf"; -val not_dvd_eq_minf = thm "not_dvd_eq_minf"; -val dvd_eq_minf = thm "dvd_eq_minf"; - -(* the Plusinfinity proprty*) - -val fm_eq_pinf = thm "fm_eq_pinf"; -val neq_eq_pinf = thm "neq_eq_pinf"; -val eq_eq_pinf = thm "eq_eq_pinf"; -val le_eq_pinf = thm "le_eq_pinf"; -val len_eq_pinf = thm "len_eq_pinf"; -val not_dvd_eq_pinf = thm "not_dvd_eq_pinf"; -val dvd_eq_pinf = thm "dvd_eq_pinf"; - -(*Logical construction of the Property*) -val eq_minf_conjI = thm "eq_minf_conjI"; -val eq_minf_disjI = thm "eq_minf_disjI"; -val modd_minf_disjI = thm "modd_minf_disjI"; -val modd_minf_conjI = thm "modd_minf_conjI"; - -val eq_pinf_conjI = thm "eq_pinf_conjI"; -val eq_pinf_disjI = thm "eq_pinf_disjI"; -val modd_pinf_disjI = thm "modd_pinf_disjI"; -val modd_pinf_conjI = thm "modd_pinf_conjI"; - -(*Cooper Backwards...*) -(*Bset*) -val not_bst_p_fm = thm "not_bst_p_fm"; -val not_bst_p_ne = thm "not_bst_p_ne"; -val not_bst_p_eq = thm "not_bst_p_eq"; -val not_bst_p_gt = thm "not_bst_p_gt"; -val not_bst_p_lt = thm "not_bst_p_lt"; -val not_bst_p_ndvd = thm "not_bst_p_ndvd"; -val not_bst_p_dvd = thm "not_bst_p_dvd"; - -(*Aset*) -val not_ast_p_fm = thm "not_ast_p_fm"; -val not_ast_p_ne = thm "not_ast_p_ne"; -val not_ast_p_eq = thm "not_ast_p_eq"; -val not_ast_p_gt = thm "not_ast_p_gt"; -val not_ast_p_lt = thm "not_ast_p_lt"; -val not_ast_p_ndvd = thm "not_ast_p_ndvd"; -val not_ast_p_dvd = thm "not_ast_p_dvd"; - -(*Logical construction of the prop*) -(*Bset*) -val not_bst_p_conjI = thm "not_bst_p_conjI"; -val not_bst_p_disjI = thm "not_bst_p_disjI"; -val not_bst_p_Q_elim = thm "not_bst_p_Q_elim"; - -(*Aset*) -val not_ast_p_conjI = thm "not_ast_p_conjI"; -val not_ast_p_disjI = thm "not_ast_p_disjI"; -val not_ast_p_Q_elim = thm "not_ast_p_Q_elim"; - -(*Cooper*) -val cppi_eq = thm "cppi_eq"; -val cpmi_eq = thm "cpmi_eq"; - -(*Others*) -val simp_from_to = thm "simp_from_to"; -val P_eqtrue = thm "P_eqtrue"; -val P_eqfalse = thm "P_eqfalse"; - -(*For Proving NNF*) - -val nnf_nn = thm "nnf_nn"; -val nnf_im = thm "nnf_im"; -val nnf_eq = thm "nnf_eq"; -val nnf_sdj = thm "nnf_sdj"; -val nnf_ncj = thm "nnf_ncj"; -val nnf_nim = thm "nnf_nim"; -val nnf_neq = thm "nnf_neq"; -val nnf_ndj = thm "nnf_ndj"; - -(*For Proving term linearizition*) -val linearize_dvd = thm "linearize_dvd"; -val lf_lt = thm "lf_lt"; -val lf_eq = thm "lf_eq"; -val lf_dvd = thm "lf_dvd"; - - -(* ------------------------------------------------------------------------- *) -(*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*) -(*Respectively by their abstract representation Const(@{const_name HOL.one},..) and Const(@{const_name HOL.zero},..)*) -(*this is necessary because the theorems use this representation.*) -(* This function should be elminated in next versions...*) -(* ------------------------------------------------------------------------- *) - -fun norm_zero_one fm = case fm of - (Const (@{const_name HOL.times},_) $ c $ t) => - if c = one then (norm_zero_one t) - else if (dest_number c = ~1) - then (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t)) - else (HOLogic.mk_binop @{const_name HOL.times} (norm_zero_one c,norm_zero_one t)) - |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest)) - |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p))) - |_ => fm; - -(* ------------------------------------------------------------------------- *) -(*function list to Set, constructs a set containing all elements of a given list.*) -(* ------------------------------------------------------------------------- *) -fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in - case l of - [] => Const ("{}",T) - |(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t) - end; - -(* ------------------------------------------------------------------------- *) -(* Returns both sides of an equvalence in the theorem*) -(* ------------------------------------------------------------------------- *) -fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end; - -(* ------------------------------------------------------------------------- *) -(*This function proove elementar will be used to generate proofs at - runtime*) (*It is thought to prove properties such as a dvd b - (essentially) that are only to make at runtime.*) -(* ------------------------------------------------------------------------- *) -fun prove_elementar thy s fm2 = - Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY - (case s of - (*"ss" like simplification with simpset*) - "ss" => - let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex] - in [simp_tac ss 1, TRY (simple_arith_tac 1)] end - - (*"bl" like blast tactic*) - (* Is only used in the harrisons like proof procedure *) - | "bl" => [blast_tac HOL_cs 1] - - (*"ed" like Existence disjunctions ...*) - (* Is only used in the harrisons like proof procedure *) - | "ed" => - let - val ex_disj_tacs = - let - val tac1 = EVERY[REPEAT(resolve_tac [disjI1,disjI2] 1), etac exI 1] - val tac2 = EVERY[etac exE 1, rtac exI 1, - REPEAT(resolve_tac [disjI1,disjI2] 1), assumption 1] - in [rtac iffI 1, - etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1, - REPEAT(EVERY[etac disjE 1, tac2]), tac2] - end - in ex_disj_tacs end - - | "fa" => [simple_arith_tac 1] - - | "sa" => - let val ss = presburger_ss addsimps zadd_ac - in [simp_tac ss 1, TRY (simple_arith_tac 1)] end - - (* like Existance Conjunction *) - | "ec" => - let val ss = presburger_ss addsimps zadd_ac - in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end - - | "ac" => - let val ss = HOL_basic_ss addsimps zadd_ac - in [simp_tac ss 1] end - - | "lf" => - let val ss = presburger_ss addsimps zadd_ac - in [simp_tac ss 1, TRY (simple_arith_tac 1)] end)); - -(*=============================================================*) -(*-------------------------------------------------------------*) -(* The new compact model *) -(*-------------------------------------------------------------*) -(*=============================================================*) - -fun thm_of sg decomp t = - let val (ts,recomb) = decomp t - in recomb (map (thm_of sg decomp) ts) - end; - -(*==================================================*) -(* Compact Version for adjustcoeffeq *) -(*==================================================*) - -fun decomp_adjustcoeffeq sg x l fm = case fm of - (Const("Not",_)$(Const(@{const_name Orderings.less},_) $ zero $(rt as (Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ c $ y ) $z )))) => - let - val m = l div (dest_number c) - val n = if (x = y) then abs (m) else 1 - val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x)) - val rs = if (x = y) - then (HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) - else HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] one rt ) - val ck = cterm_of sg (mk_number n) - val cc = cterm_of sg c - val ct = cterm_of sg z - val cx = cterm_of sg y - val pre = prove_elementar sg "lf" - (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number n)) - val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq))) - in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) - end - - |(Const(p,_) $a $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ - c $ y ) $t )) => - if (is_arith_rel fm) andalso (x = y) - then - let val m = l div (dest_number c) - val k = (if p = @{const_name Orderings.less} then abs(m) else m) - val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div k)*l) ), x)) - val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul k t) )))) - - val ck = cterm_of sg (mk_number k) - val cc = cterm_of sg c - val ct = cterm_of sg t - val cx = cterm_of sg x - val ca = cterm_of sg a - - in - case p of - @{const_name Orderings.less} => - let val pre = prove_elementar sg "lf" - (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number k)) - val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq))) - in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) - end - - |"op =" => - let val pre = prove_elementar sg "lf" - (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k))) - val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq))) - in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) - end - - |"Divides.dvd" => - let val pre = prove_elementar sg "lf" - (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k))) - val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq)) - in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) - - end - end - else ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl) - - |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not) - |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI) - |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI) - - |_ => ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl); - -fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l); - - - -(*==================================================*) -(* Finding rho for modd_minusinfinity *) -(*==================================================*) -fun rho_for_modd_minf x dlcm sg fm1 = -let - (*Some certified Terms*) - - val ctrue = cterm_of sg HOLogic.true_const - val cfalse = cterm_of sg HOLogic.false_const - val fm = norm_zero_one fm1 - in case fm1 of - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => - if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) - - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => - if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) - then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) - - |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => - if (y=x) andalso (c1 = zero) then - if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else - (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) - - |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then let val cz = cterm_of sg (norm_zero_one z) - val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero) - in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf))) - end - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) - |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ - c $ y ) $ z))) => - if y=x then let val cz = cterm_of sg (norm_zero_one z) - val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero) - in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf))) - end - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) - - - |_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf) - end; -(*=========================================================================*) -(*=========================================================================*) -fun rho_for_eq_minf x dlcm sg fm1 = - let - val fm = norm_zero_one fm1 - in case fm1 of - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => - if (x=y) andalso (c1=zero) andalso (c2=one) - then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) - - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => - if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one)) - then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) - - |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => - if (y=x) andalso (c1 =zero) then - if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else - (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) - |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then let val cd = cterm_of sg (norm_zero_one d) - val cz = cterm_of sg (norm_zero_one z) - in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf)) - end - - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) - - |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then let val cd = cterm_of sg (norm_zero_one d) - val cz = cterm_of sg (norm_zero_one z) - in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf)) - end - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) - - - |_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) - end; - -(*=====================================================*) -(*=====================================================*) -(*=========== minf proofs with the compact version==========*) -fun decomp_minf_eq x dlcm sg t = case t of - Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI) - |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI) - |_ => ([],fn [] => rho_for_eq_minf x dlcm sg t); - -fun decomp_minf_modd x dlcm sg t = case t of - Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI) - |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI) - |_ => ([],fn [] => rho_for_modd_minf x dlcm sg t); - -(* -------------------------------------------------------------*) -(* Finding rho for pinf_modd *) -(* -------------------------------------------------------------*) -fun rho_for_modd_pinf x dlcm sg fm1 = -let - (*Some certified Terms*) - - val ctrue = cterm_of sg HOLogic.true_const - val cfalse = cterm_of sg HOLogic.false_const - val fm = norm_zero_one fm1 - in case fm1 of - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => - if ((x=y) andalso (c1= zero) andalso (c2= one)) - then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) - - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => - if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero) andalso (c2 = one)) - then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) - - |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => - if ((y=x) andalso (c1 = zero)) then - if (pm1 = one) - then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) - else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) - - |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then let val cz = cterm_of sg (norm_zero_one z) - val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero) - in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf))) - end - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) - |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ - c $ y ) $ z))) => - if y=x then let val cz = cterm_of sg (norm_zero_one z) - val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero) - in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf))) - end - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) - - - |_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf) - end; -(* -------------------------------------------------------------*) -(* Finding rho for pinf_eq *) -(* -------------------------------------------------------------*) -fun rho_for_eq_pinf x dlcm sg fm1 = - let - val fm = norm_zero_one fm1 - in case fm1 of - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => - if (x=y) andalso (c1=zero) andalso (c2=one) - then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) - - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => - if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one)) - then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) - - |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => - if (y=x) andalso (c1 =zero) then - if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else - (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf)) - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) - |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then let val cd = cterm_of sg (norm_zero_one d) - val cz = cterm_of sg (norm_zero_one z) - in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf)) - end - - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) - - |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then let val cd = cterm_of sg (norm_zero_one d) - val cz = cterm_of sg (norm_zero_one z) - in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf)) - end - else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) - - - |_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) - end; - - - -fun minf_proof_of_c sg x dlcm t = - let val minf_eqth = thm_of sg (decomp_minf_eq x dlcm sg) t - val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t - in (minf_eqth, minf_moddth) -end; - -(*=========== pinf proofs with the compact version==========*) -fun decomp_pinf_eq x dlcm sg t = case t of - Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI) - |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI) - |_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ; - -fun decomp_pinf_modd x dlcm sg t = case t of - Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI) - |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI) - |_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t); - -fun pinf_proof_of_c sg x dlcm t = - let val pinf_eqth = thm_of sg (decomp_pinf_eq x dlcm sg) t - val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t - in (pinf_eqth,pinf_moddth) -end; - - -(* ------------------------------------------------------------------------- *) -(* Here we generate the theorem for the Bset Property in the simple direction*) -(* It is just an instantiation*) -(* ------------------------------------------------------------------------- *) -(* -fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm = - let - val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) - val cdlcm = cterm_of sg dlcm - val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs)) - in instantiate' [] [SOME cdlcm,SOME cB, SOME cp] (bst_thm) -end; - -fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm = - let - val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) - val cdlcm = cterm_of sg dlcm - val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast)) - in instantiate' [] [SOME cdlcm,SOME cA, SOME cp] (ast_thm) -end; -*) - -(* For the generation of atomic Theorems*) -(* Prove the premisses on runtime and then make RS*) -(* ------------------------------------------------------------------------- *) - -(*========= this is rho ============*) -fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at = - let - val cdlcm = cterm_of sg dlcm - val cB = cterm_of sg B - val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) - val cat = cterm_of sg (norm_zero_one at) - in - case at of - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => - if (x=y) andalso (c1=zero) andalso (c2=one) - then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B) - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) - val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero ,dlcm)) - in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) - - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => - if (is_arith_rel at) andalso (x=y) - then let - val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1))) - in - let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B) - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const(@{const_name HOL.minus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ norm_zero_one z) $ HOLogic.mk_number HOLogic.intT 1)) - val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) - in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq))) - end - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) - - |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => - if (y=x) andalso (c1 =zero) then - if pm1 = one then - let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B) - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) - in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt))) - end - else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) - in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) - - |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then - let val cz = cterm_of sg (norm_zero_one z) - val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) - in (instantiate' [] [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) - - |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then - let val cz = cterm_of sg (norm_zero_one z) - val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) - in (instantiate' [] [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) - - |_ => (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) - - end; - - -(* ------------------------------------------------------------------------- *) -(* Main interpretation function for this backwards dirction*) -(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*) -(*Help Function*) -(* ------------------------------------------------------------------------- *) - -(*==================== Proof with the compact version *) - -fun decomp_nbstp sg x dlcm B fm t = case t of - Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI ) - |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI) - |_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t); - -fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t = - let - val th = thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t - val fma = absfree (xn,xT, norm_zero_one fm) - in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma)) - in [th,th1] MRS (not_bst_p_Q_elim) - end - end; - - -(* ------------------------------------------------------------------------- *) -(* Protokol interpretation function for the backwards direction for cooper's Theorem*) - -(* For the generation of atomic Theorems*) -(* Prove the premisses on runtime and then make RS*) -(* ------------------------------------------------------------------------- *) -(*========= this is rho ============*) -fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at = - let - val cdlcm = cterm_of sg dlcm - val cA = cterm_of sg A - val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) - val cat = cterm_of sg (norm_zero_one at) - in - case at of - (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => - if (x=y) andalso (c1=zero) andalso (c2=one) - then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A) - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) - val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) - in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) - - |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => - if (is_arith_rel at) andalso (x=y) - then let val ast_z = norm_zero_one (linear_sub [] one z ) - val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A) - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const(@{const_name HOL.plus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ one)) - val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) - in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) - - |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) => - if (y=x) andalso (c1 =zero) then - if pm1 = (mk_number ~1) then - let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A) - val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm)) - in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt))) - end - else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm)) - in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) - - |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then - let val cz = cterm_of sg (norm_zero_one z) - val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) - in (instantiate' [] [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) - - |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => - if y=x then - let val cz = cterm_of sg (norm_zero_one z) - val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) - in (instantiate' [] [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd))) - end - else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) - - |_ => (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) - - end; - -(* ------------------------------------------------------------------------ *) -(* Main interpretation function for this backwards dirction*) -(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*) -(*Help Function*) -(* ------------------------------------------------------------------------- *) - -fun decomp_nastp sg x dlcm A fm t = case t of - Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI ) - |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI) - |_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t); - -fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t = - let - val th = thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t - val fma = absfree (xn,xT, norm_zero_one fm) - in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma)) - in [th,th1] MRS (not_ast_p_Q_elim) - end - end; - - -(* -------------------------------*) -(* Finding rho and beta for evalc *) -(* -------------------------------*) - -fun rho_for_evalc sg at = case at of - (Const (p,_) $ s $ t) =>( - case AList.lookup (op =) operations p of - SOME f => - ((if (f ((dest_number s),(dest_number t))) - then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) - else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))) - handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) - | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl ) - |Const("Not",_)$(Const (p,_) $ s $ t) =>( - case AList.lookup (op =) operations p of - SOME f => - ((if (f ((dest_number s),(dest_number t))) - then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)) - else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))) - handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) - | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl ) - | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl; - - -(*=========================================================*) -fun decomp_evalc sg t = case t of - (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI) - |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI) - |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI) - |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI) - |_ => ([], fn [] => rho_for_evalc sg t); - - -fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm; - -(*==================================================*) -(* Proof of linform with the compact model *) -(*==================================================*) - - -fun decomp_linform sg vars t = case t of - (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI) - |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI) - |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI) - |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI) - |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not) - |(Const("Divides.dvd",_)$d$r) => - if is_number d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd))) - else (warning "Nonlinear Term --- Non numeral leftside at dvd"; - raise COOPER) - |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t))); - -fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f; - -(* ------------------------------------------------------------------------- *) -(* Interpretaion of Protocols of the cooper procedure : minusinfinity version*) -(* ------------------------------------------------------------------------- *) -fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm = - (* Get the Bset thm*) - let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm - val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm)); - val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm - in (dpos,minf_eqth,nbstpthm,minf_moddth) -end; - -(* ------------------------------------------------------------------------- *) -(* Interpretaion of Protocols of the cooper procedure : plusinfinity version *) -(* ------------------------------------------------------------------------- *) -fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm = - let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm - val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm)); - val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm - in (dpos,pinf_eqth,nastpthm,pinf_moddth) -end; - -(* ------------------------------------------------------------------------- *) -(* Interpretaion of Protocols of the cooper procedure : full version*) -(* ------------------------------------------------------------------------- *) -fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of - "pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm - in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq) - end - |"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm - in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq) - end - |_ => error "parameter error"; - -(* ------------------------------------------------------------------------- *) -(* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*) -(* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*) -(* ------------------------------------------------------------------------- *) - -(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*) -(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *) - -fun cooper_prv sg (x as Free(xn,xT)) efm = let - (* lfm_thm : efm = linearized form of efm*) - val lfm_thm = proof_of_linform sg [xn] efm - (*efm2 is the linearized form of efm *) - val efm2 = snd(qe_get_terms lfm_thm) - (* l is the lcm of all coefficients of x *) - val l = formlcm x efm2 - (*ac_thm: efm = efm2 with adjusted coefficients of x *) - val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans - (* fm is efm2 with adjusted coefficients of x *) - val fm = snd (qe_get_terms ac_thm) - (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) - val cfm = unitycoeff x fm - (*afm is fm where c*x is replaced by 1*x or -1*x *) - val afm = adjustcoeff x l fm - (* P = %x.afm*) - val P = absfree(xn,xT,afm) - (* This simpset allows the elimination of the sets in bex {1..d} *) - val ss = presburger_ss addsimps - [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] - (* uth : EX x.P(l*x) = EX x. l dvd x & P x*) - val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex) - (* e_ac_thm : Ex x. efm = EX x. fm*) - val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) - (* A and B set of the formula*) - val A = aset x cfm - val B = bset x cfm - (* the divlcm (delta) of the formula*) - val dlcm = mk_number (divlcm x cfm) - (* Which set is smaller to generate the (hoepfully) shorter proof*) - val cms = if ((length A) < (length B )) then "pi" else "mi" -(* val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*) - (* synthesize the proof of cooper's theorem*) - (* cp_thm: EX x. cfm = Q*) - val cp_thm = cooper_thm sg cms x cfm dlcm A B - (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) - (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) -(* - val _ = prth cp_thm - val _ = writeln "Expanding the bounded EX..." -*) - val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans))) -(* - val _ = writeln "Expanded" *) - (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) - val (lsuth,rsuth) = qe_get_terms (uth) - (* lseacth = EX x. efm; rseacth = EX x. fm*) - val (lseacth,rseacth) = qe_get_terms(e_ac_thm) - (* lscth = EX x. cfm; rscth = Q' *) - val (lscth,rscth) = qe_get_terms (exp_cp_thm) - (* u_c_thm: EX x. P(l*x) = Q'*) - val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans - (* result: EX x. efm = Q'*) - in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) - end -|cooper_prv _ _ _ = error "Parameters format"; - -(* **************************************** *) -(* An Other Version of cooper proving *) -(* by giving a withness for EX *) -(* **************************************** *) - - - -fun cooper_prv_w sg (x as Free(xn,xT)) efm = let - (* lfm_thm : efm = linearized form of efm*) - val lfm_thm = proof_of_linform sg [xn] efm - (*efm2 is the linearized form of efm *) - val efm2 = snd(qe_get_terms lfm_thm) - (* l is the lcm of all coefficients of x *) - val l = formlcm x efm2 - (*ac_thm: efm = efm2 with adjusted coefficients of x *) - val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans - (* fm is efm2 with adjusted coefficients of x *) - val fm = snd (qe_get_terms ac_thm) - (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) - val cfm = unitycoeff x fm - (*afm is fm where c*x is replaced by 1*x or -1*x *) - val afm = adjustcoeff x l fm - (* P = %x.afm*) - val P = absfree(xn,xT,afm) - (* This simpset allows the elimination of the sets in bex {1..d} *) - val ss = presburger_ss addsimps - [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] - (* uth : EX x.P(l*x) = EX x. l dvd x & P x*) - val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex) - (* e_ac_thm : Ex x. efm = EX x. fm*) - val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) - (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) - val (lsuth,rsuth) = qe_get_terms (uth) - (* lseacth = EX x. efm; rseacth = EX x. fm*) - val (lseacth,rseacth) = qe_get_terms(e_ac_thm) - - val (w,rs) = cooper_w [] cfm - val exp_cp_thm = case w of - (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*) - SOME n => e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*) - |_ => let - (* A and B set of the formula*) - val A = aset x cfm - val B = bset x cfm - (* the divlcm (delta) of the formula*) - val dlcm = mk_number (divlcm x cfm) - (* Which set is smaller to generate the (hoepfully) shorter proof*) - val cms = if ((length A) < (length B )) then "pi" else "mi" - (* synthesize the proof of cooper's theorem*) - (* cp_thm: EX x. cfm = Q*) - val cp_thm = cooper_thm sg cms x cfm dlcm A B - (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) - (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) - in refl RS (simplify ss (cp_thm RSN (2,trans))) - end - (* lscth = EX x. cfm; rscth = Q' *) - val (lscth,rscth) = qe_get_terms (exp_cp_thm) - (* u_c_thm: EX x. P(l*x) = Q'*) - val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans - (* result: EX x. efm = Q'*) - in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) - end -|cooper_prv_w _ _ _ = error "Parameters format"; - - - -fun decomp_cnnf sg lfnp P = case P of - Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI ) - |Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_disjI) - |Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn) - |Const("Not",_) $ (Const(opn,T) $ p $ q) => - if opn = "op |" - then case (p,q) of - (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) => - if r1 = negate r - then ([r,HOLogic.Not$s,r1,HOLogic.Not$t],fn [th1_1,th1_2,th2_1,th2_2] => [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj) - - else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj) - |(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj) - else ( - case (opn,T) of - ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj ) - |("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim ) - |("op =",Type ("fun",[Type ("bool", []),_])) => - ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq) - |(_,_) => ([], fn [] => lfnp P) -) - - |(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im) - - |(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) => - ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq ) - |_ => ([], fn [] => lfnp P); - - - - -fun proof_of_cnnf sg p lfnp = - let val th1 = thm_of sg (decomp_cnnf sg lfnp) p - val rs = snd(qe_get_terms th1) - val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs)) - in [th1,th2] MRS trans - end; - -end; - diff -r e36fc1bcb8c6 -r 156db04f8af0 src/HOL/Tools/Presburger/reflected_cooper.ML --- a/src/HOL/Tools/Presburger/reflected_cooper.ML Mon Jun 11 11:07:18 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,119 +0,0 @@ -(* $Id$ *) -(* The oracle for Presburger arithmetic based on the verified Code *) - (* in HOL/ex/Reflected_Presburger.thy *) - -structure ReflectedCooper = -struct - -open Generated; -(* pseudo reification : term -> intterm *) - -fun i_of_term vs t = case t of - Free(xn,xT) => (case AList.lookup (op =) vs t of - NONE => error "Variable not found in the list!!" - | SOME n => Var n) - | Const(@{const_name HOL.zero},iT) => Cst 0 - | Const(@{const_name HOL.one},iT) => Cst 1 - | Bound i => Var (nat (IntInf.fromInt i)) - | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t') - | Const (@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) - | Const (@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) - | Const (@{const_name HOL.times},_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2) - | Const (@{const_name Numeral.number_of},_)$t' => Cst (HOLogic.dest_numeral t') - | _ => error "i_of_term: unknown term"; - -(* pseudo reification : term -> QF *) -fun qf_of_term vs t = case t of - Const("True",_) => T - | Const("False",_) => F - | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2) - | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2) - | Const ("Divides.dvd",_)$t1$t2 => - Divides(i_of_term vs t1,i_of_term vs t2) - | Const("op =",eqT)$t1$t2 => - if (domain_type eqT = HOLogic.intT) - then let val i1 = i_of_term vs t1 - val i2 = i_of_term vs t2 - in Eq (i1,i2) - end - else Equ(qf_of_term vs t1,qf_of_term vs t2) - | Const("op &",_)$t1$t2 => And(qf_of_term vs t1,qf_of_term vs t2) - | Const("op |",_)$t1$t2 => Or(qf_of_term vs t1,qf_of_term vs t2) - | Const("op -->",_)$t1$t2 => Imp(qf_of_term vs t1,qf_of_term vs t2) - | Const("Not",_)$t' => NOT(qf_of_term vs t') - | Const("Ex",_)$Abs(xn,xT,p) => - QEx(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p) - | Const("All",_)$Abs(xn,xT,p) => - QAll(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p) - | _ => error "qf_of_term : unknown term!"; - -(* -fun parse thy s = term_of (Thm.read_cterm thy (s, HOLogic.boolT)); - -val t = parse "ALL (i::int) (j::int). i < 8* j --> (i - 1 = j + 3 + 2*j) & (j <= -i + k ) | 4 = i | 5 dvd i"; -*) -fun zip [] [] = [] - | zip (x::xs) (y::ys) = (x,y)::(zip xs ys); - - -fun start_vs t = - let val fs = term_frees t - in zip fs (map (nat o IntInf.fromInt) (0 upto (length fs - 1))) - end ; - -(* transform intterm and QF back to terms *) -val iT = HOLogic.intT; -val bT = HOLogic.boolT; -fun myassoc2 l v = - case l of - [] => NONE - | (x,v')::xs => if v = v' then SOME x - else myassoc2 xs v; - -fun term_of_i vs t = - case t of - Cst i => CooperDec.mk_number i - | Var n => valOf (myassoc2 vs n) - | Neg t' => Const(@{const_name HOL.uminus},iT --> iT)$(term_of_i vs t') - | Add(t1,t2) => Const(@{const_name HOL.plus},[iT,iT] ---> iT)$ - (term_of_i vs t1)$(term_of_i vs t2) - | Sub(t1,t2) => Const(@{const_name HOL.minus},[iT,iT] ---> iT)$ - (term_of_i vs t1)$(term_of_i vs t2) - | Mult(t1,t2) => Const(@{const_name HOL.times},[iT,iT] ---> iT)$ - (term_of_i vs t1)$(term_of_i vs t2); - -fun term_of_qf vs t = - case t of - T => HOLogic.true_const - | F => HOLogic.false_const - | Lt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$ - (term_of_i vs t1)$(term_of_i vs t2) - | Le(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$ - (term_of_i vs t1)$(term_of_i vs t2) - | Gt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$ - (term_of_i vs t2)$(term_of_i vs t1) - | Ge(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$ - (term_of_i vs t2)$(term_of_i vs t1) - | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$ - (term_of_i vs t1)$(term_of_i vs t2) - | Divides(t1,t2) => Const("Divides.dvd",[iT,iT] ---> bT)$ - (term_of_i vs t1)$(term_of_i vs t2) - | NOT t' => HOLogic.Not$(term_of_qf vs t') - | And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2) - | Or(t1,t2) => HOLogic.disj$(term_of_qf vs t1)$(term_of_qf vs t2) - | Imp(t1,t2) => HOLogic.imp$(term_of_qf vs t1)$(term_of_qf vs t2) - | Equ(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf vs t1)$ - (term_of_qf vs t2) - | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; - -(* The oracle *) -fun presburger_oracle thy t = - let val vs = start_vs t - val result = lift_un (term_of_qf vs) (pa (qf_of_term vs t)) - in - case result of - None => raise CooperDec.COOPER - | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t')) - end ; - -end; diff -r e36fc1bcb8c6 -r 156db04f8af0 src/HOL/Tools/Presburger/reflected_presburger.ML --- a/src/HOL/Tools/Presburger/reflected_presburger.ML Mon Jun 11 11:07:18 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2172 +0,0 @@ -(* $Id$ *) - - (* Caution: This file should not be modified. *) - (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *) -fun nat (i:IntInf.int) = if i < 0 then 0 else i : IntInf.int; -structure Generated = -struct - -datatype intterm = Cst of IntInf.int | Var of IntInf.int | Neg of intterm - | Add of intterm * intterm | Sub of intterm * intterm - | Mult of intterm * intterm; - -datatype QF = Lt of intterm * intterm | Gt of intterm * intterm - | Le of intterm * intterm | Ge of intterm * intterm | Eq of intterm * intterm - | Divides of intterm * intterm | T | F | NOT of QF | And of QF * QF - | Or of QF * QF | Imp of QF * QF | Equ of QF * QF | QAll of QF | QEx of QF; - -datatype 'a option = None | Some of 'a; - -fun lift_un c None = None - | lift_un c (Some p) = Some (c p); - -fun lift_bin (c, (Some a, Some b)) = Some (c a b) - | lift_bin (c, (None, y)) = None - | lift_bin (c, (Some y, None)) = None; - -fun lift_qe qe None = None - | lift_qe qe (Some p) = qe p; - -fun qelim (qe, QAll p) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe, p)))) - | qelim (qe, QEx p) = lift_qe qe (qelim (qe, p)) - | qelim (qe, And (p, q)) = - lift_bin ((fn x => fn xa => And (x, xa)), (qelim (qe, p), qelim (qe, q))) - | qelim (qe, Or (p, q)) = - lift_bin ((fn x => fn xa => Or (x, xa)), (qelim (qe, p), qelim (qe, q))) - | qelim (qe, Imp (p, q)) = - lift_bin ((fn x => fn xa => Imp (x, xa)), (qelim (qe, p), qelim (qe, q))) - | qelim (qe, Equ (p, q)) = - lift_bin ((fn x => fn xa => Equ (x, xa)), (qelim (qe, p), qelim (qe, q))) - | qelim (qe, NOT p) = lift_un NOT (qelim (qe, p)) - | qelim (qe, Lt (w, x)) = Some (Lt (w, x)) - | qelim (qe, Gt (y, z)) = Some (Gt (y, z)) - | qelim (qe, Le (aa, ab)) = Some (Le (aa, ab)) - | qelim (qe, Ge (ac, ad)) = Some (Ge (ac, ad)) - | qelim (qe, Eq (ae, af)) = Some (Eq (ae, af)) - | qelim (qe, Divides (ag, ah)) = Some (Divides (ag, ah)) - | qelim (qe, T) = Some T - | qelim (qe, F) = Some F; - -fun lin_mul (c, Cst i) = Cst (c * i) - | lin_mul (c, Add (Mult (Cst c', Var n), r)) = - (if (c = 0) then Cst 0 - else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r))); - -fun op_60_def0 m n = IntInf.< (m,n); - -fun op_60_61_def0 m n = not (op_60_def0 n m); - -fun lin_add (Add (Mult (Cst c1, Var n1), r1), Add (Mult (Cst c2, Var n2), r2)) = - (if (n1 = n2) - then let val c = Cst (c1 + c2) - in (if ((c1 + c2) = 0) then lin_add (r1, r2) - else Add (Mult (c, Var n1), lin_add (r1, r2))) - end - else (if op_60_61_def0 n1 n2 - then Add (Mult (Cst c1, Var n1), - lin_add (r1, Add (Mult (Cst c2, Var n2), r2))) - else Add (Mult (Cst c2, Var n2), - lin_add (Add (Mult (Cst c1, Var n1), r1), r2)))) - | lin_add (Add (Mult (Cst c1, Var n1), r1), Cst b) = - Add (Mult (Cst c1, Var n1), lin_add (r1, Cst b)) - | lin_add (Cst x, Add (Mult (Cst c2, Var n2), r2)) = - Add (Mult (Cst c2, Var n2), lin_add (Cst x, r2)) - | lin_add (Cst b1, Cst b2) = Cst (b1 + b2); - -fun lin_neg i = lin_mul (~1, i); - -fun linearize (Cst b) = Some (Cst b) - | linearize (Var n) = Some (Add (Mult (Cst 1, Var n), Cst 0)) - | linearize (Neg i) = lift_un lin_neg (linearize i) - | linearize (Add (i, j)) = - lift_bin ((fn x => fn y => lin_add (x, y)), (linearize i, linearize j)) - | linearize (Sub (i, j)) = - lift_bin - ((fn x => fn y => lin_add (x, lin_neg y)), (linearize i, linearize j)) - | linearize (Mult (i, j)) = - (case linearize i of None => None - | Some x => - (case x of - Cst xa => - (case linearize j of None => None - | Some x => Some (lin_mul (xa, x))) - | Var xa => - (case linearize j of None => None - | Some xa => - (case xa of Cst xa => Some (lin_mul (xa, x)) - | Var xa => None | Neg xa => None | Add (xa, xb) => None - | Sub (xa, xb) => None | Mult (xa, xb) => None)) - | Neg xa => - (case linearize j of None => None - | Some xa => - (case xa of Cst xa => Some (lin_mul (xa, x)) - | Var xa => None | Neg xa => None | Add (xa, xb) => None - | Sub (xa, xb) => None | Mult (xa, xb) => None)) - | Add (xa, xb) => - (case linearize j of None => None - | Some xa => - (case xa of Cst xa => Some (lin_mul (xa, x)) - | Var xa => None | Neg xa => None | Add (xa, xb) => None - | Sub (xa, xb) => None | Mult (xa, xb) => None)) - | Sub (xa, xb) => - (case linearize j of None => None - | Some xa => - (case xa of Cst xa => Some (lin_mul (xa, x)) - | Var xa => None | Neg xa => None | Add (xa, xb) => None - | Sub (xa, xb) => None | Mult (xa, xb) => None)) - | Mult (xa, xb) => - (case linearize j of None => None - | Some xa => - (case xa of Cst xa => Some (lin_mul (xa, x)) - | Var xa => None | Neg xa => None | Add (xa, xb) => None - | Sub (xa, xb) => None | Mult (xa, xb) => None)))); - -fun linform (Le (it1, it2)) = - lift_bin - ((fn x => fn y => Le (lin_add (x, lin_neg y), Cst 0)), - (linearize it1, linearize it2)) - | linform (Eq (it1, it2)) = - lift_bin - ((fn x => fn y => Eq (lin_add (x, lin_neg y), Cst 0)), - (linearize it1, linearize it2)) - | linform (Divides (d, t)) = - (case linearize d of None => None - | Some x => - (case x of - Cst xa => - (if (xa = 0) then None - else (case linearize t of None => None - | Some xa => Some (Divides (x, xa)))) - | Var xa => None | Neg xa => None | Add (xa, xb) => None - | Sub (xa, xb) => None | Mult (xa, xb) => None)) - | linform T = Some T - | linform F = Some F - | linform (NOT p) = lift_un NOT (linform p) - | linform (And (p, q)) = - lift_bin ((fn f => fn g => And (f, g)), (linform p, linform q)) - | linform (Or (p, q)) = - lift_bin ((fn f => fn g => Or (f, g)), (linform p, linform q)); - -fun nnf (Lt (it1, it2)) = Le (Sub (it1, it2), Cst (~ 1)) - | nnf (Gt (it1, it2)) = Le (Sub (it2, it1), Cst (~ 1)) - | nnf (Le (it1, it2)) = Le (it1, it2) - | nnf (Ge (it1, it2)) = Le (it2, it1) - | nnf (Eq (it1, it2)) = Eq (it2, it1) - | nnf (Divides (d, t)) = Divides (d, t) - | nnf T = T - | nnf F = F - | nnf (And (p, q)) = And (nnf p, nnf q) - | nnf (Or (p, q)) = Or (nnf p, nnf q) - | nnf (Imp (p, q)) = Or (nnf (NOT p), nnf q) - | nnf (Equ (p, q)) = Or (And (nnf p, nnf q), And (nnf (NOT p), nnf (NOT q))) - | nnf (NOT (Lt (it1, it2))) = Le (it2, it1) - | nnf (NOT (Gt (it1, it2))) = Le (it1, it2) - | nnf (NOT (Le (it1, it2))) = Le (Sub (it2, it1), Cst (~ 1)) - | nnf (NOT (Ge (it1, it2))) = Le (Sub (it1, it2), Cst (~ 1)) - | nnf (NOT (Eq (it1, it2))) = NOT (Eq (it1, it2)) - | nnf (NOT (Divides (d, t))) = NOT (Divides (d, t)) - | nnf (NOT T) = F - | nnf (NOT F) = T - | nnf (NOT (NOT p)) = nnf p - | nnf (NOT (And (p, q))) = Or (nnf (NOT p), nnf (NOT q)) - | nnf (NOT (Or (p, q))) = And (nnf (NOT p), nnf (NOT q)) - | nnf (NOT (Imp (p, q))) = And (nnf p, nnf (NOT q)) - | nnf (NOT (Equ (p, q))) = - Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q)); - -fun op_45_def2 z w = IntInf.+ (z,~ w); - -fun op_45_def0 m n = nat (op_45_def2 (m) (n)); - -val id_1_def0 : IntInf.int = (0 + 1); - -fun decrvarsI (Cst i) = Cst i - | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0) - | decrvarsI (Neg a) = Neg (decrvarsI a) - | decrvarsI (Add (a, b)) = Add (decrvarsI a, decrvarsI b) - | decrvarsI (Sub (a, b)) = Sub (decrvarsI a, decrvarsI b) - | decrvarsI (Mult (a, b)) = Mult (decrvarsI a, decrvarsI b); - -fun decrvars (Lt (a, b)) = Lt (decrvarsI a, decrvarsI b) - | decrvars (Gt (a, b)) = Gt (decrvarsI a, decrvarsI b) - | decrvars (Le (a, b)) = Le (decrvarsI a, decrvarsI b) - | decrvars (Ge (a, b)) = Ge (decrvarsI a, decrvarsI b) - | decrvars (Eq (a, b)) = Eq (decrvarsI a, decrvarsI b) - | decrvars (Divides (a, b)) = Divides (decrvarsI a, decrvarsI b) - | decrvars T = T - | decrvars F = F - | decrvars (NOT p) = NOT (decrvars p) - | decrvars (And (p, q)) = And (decrvars p, decrvars q) - | decrvars (Or (p, q)) = Or (decrvars p, decrvars q) - | decrvars (Imp (p, q)) = Imp (decrvars p, decrvars q) - | decrvars (Equ (p, q)) = Equ (decrvars p, decrvars q); - -fun op_64 [] ys = ys - | op_64 (x :: xs) ys = (x :: op_64 xs ys); - -fun map f [] = [] - | map f (x :: xs) = (f x :: map f xs); - -fun iupto (i:IntInf.int, j:IntInf.int) = (if (j < i) then [] else (i :: iupto ((i + 1), j))); - -fun all_sums (j:IntInf.int, []) = [] - | all_sums (j, (i :: is)) = - op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is)); - -fun split x = (fn p => x (fst p) (snd p)); - -fun negateSnd x = split (fn q => fn r => (q, IntInf.~ r)) x; - -fun adjust b = - (fn (q:IntInf.int, r:IntInf.int) => - (if (0 <= op_45_def2 r b) then ((((2:IntInf.int) * q) + (1:IntInf.int)), op_45_def2 r b) - else (((2:IntInf.int) * q), r))); - -fun negDivAlg (a:IntInf.int, b:IntInf.int) = - (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b)) - else adjust b (negDivAlg (a, (2 * b)))); - -fun posDivAlg (a:IntInf.int, b:IntInf.int) = - (if ((a < b) orelse (b <= 0)) then (0, a) - else adjust b (posDivAlg (a, (2 * b)))); - -fun divAlg x = - split (fn a:IntInf.int => fn b:IntInf.int => - (if (0 <= a) - then (if (0 <= b) then posDivAlg (a, b) - else (if (a = 0) then (0, 0) - else negateSnd (negDivAlg (~ a, ~ b)))) - else (if (0 < b) then negDivAlg (a, b) - else negateSnd (posDivAlg (~ a, ~ b))))) - x; - -fun op_mod_def1 a b = snd (divAlg (a, b)); - -fun op_dvd m n = (op_mod_def1 n m = 0); - -fun psimpl (Le (l, r)) = - (case lift_bin - ((fn x => fn y => lin_add (x, lin_neg y)), - (linearize l, linearize r)) of - None => Le (l, r) - | Some x => - (case x of Cst xa => (if (xa <= 0) then T else F) - | Var xa => Le (x, Cst 0) | Neg xa => Le (x, Cst 0) - | Add (xa, xb) => Le (x, Cst 0) | Sub (xa, xb) => Le (x, Cst 0) - | Mult (xa, xb) => Le (x, Cst 0))) - | psimpl (Eq (l, r)) = - (case lift_bin - ((fn x => fn y => lin_add (x, lin_neg y)), - (linearize l, linearize r)) of - None => Eq (l, r) - | Some x => - (case x of Cst xa => (if (xa = 0) then T else F) - | Var xa => Eq (x, Cst 0) | Neg xa => Eq (x, Cst 0) - | Add (xa, xb) => Eq (x, Cst 0) | Sub (xa, xb) => Eq (x, Cst 0) - | Mult (xa, xb) => Eq (x, Cst 0))) - | psimpl (Divides (Cst d, t)) = - (case linearize t of None => Divides (Cst d, t) - | Some x => - (case x of Cst xa => (if op_dvd d xa then T else F) - | Var xa => Divides (Cst d, x) | Neg xa => Divides (Cst d, x) - | Add (xa, xb) => Divides (Cst d, x) - | Sub (xa, xb) => Divides (Cst d, x) - | Mult (xa, xb) => Divides (Cst d, x))) - | psimpl (Equ (p, q)) = - let val p' = psimpl p; val q' = psimpl q - in (case p' of - Lt (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | Gt (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | Le (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | Ge (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | Eq (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | Divides (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | T => q' - | F => (case q' of Lt (x, xa) => NOT q' | Gt (x, xa) => NOT q' - | Le (x, xa) => NOT q' | Ge (x, xa) => NOT q' - | Eq (x, xa) => NOT q' | Divides (x, xa) => NOT q' | T => F - | F => T | NOT x => x | And (x, xa) => NOT q' - | Or (x, xa) => NOT q' | Imp (x, xa) => NOT q' - | Equ (x, xa) => NOT q' | QAll x => NOT q' | QEx x => NOT q') - | NOT x => - (case q' of Lt (xa, xb) => Equ (p', q') - | Gt (xa, xb) => Equ (p', q') | Le (xa, xb) => Equ (p', q') - | Ge (xa, xb) => Equ (p', q') | Eq (xa, xb) => Equ (p', q') - | Divides (xa, xb) => Equ (p', q') | T => p' | F => x - | NOT xa => Equ (x, xa) | And (xa, xb) => Equ (p', q') - | Or (xa, xb) => Equ (p', q') | Imp (xa, xb) => Equ (p', q') - | Equ (xa, xb) => Equ (p', q') | QAll xa => Equ (p', q') - | QEx xa => Equ (p', q')) - | And (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | Or (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | Imp (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | Equ (x, xa) => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | QAll x => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q')) - | QEx x => - (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q') - | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q') - | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q') - | T => p' | F => NOT p' | NOT x => Equ (p', q') - | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q') - | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q') - | QAll x => Equ (p', q') | QEx x => Equ (p', q'))) - end - | psimpl (NOT p) = - let val p' = psimpl p - in (case p' of Lt (x, xa) => NOT p' | Gt (x, xa) => NOT p' - | Le (x, xa) => NOT p' | Ge (x, xa) => NOT p' | Eq (x, xa) => NOT p' - | Divides (x, xa) => NOT p' | T => F | F => T | NOT x => x - | And (x, xa) => NOT p' | Or (x, xa) => NOT p' | Imp (x, xa) => NOT p' - | Equ (x, xa) => NOT p' | QAll x => NOT p' | QEx x => NOT p') - end - | psimpl (Lt (u, v)) = Lt (u, v) - | psimpl (Gt (w, x)) = Gt (w, x) - | psimpl (Ge (aa, ab)) = Ge (aa, ab) - | psimpl (Divides (Var bp, af)) = Divides (Var bp, af) - | psimpl (Divides (Neg bq, af)) = Divides (Neg bq, af) - | psimpl (Divides (Add (br, bs), af)) = Divides (Add (br, bs), af) - | psimpl (Divides (Sub (bt, bu), af)) = Divides (Sub (bt, bu), af) - | psimpl (Divides (Mult (bv, bw), af)) = Divides (Mult (bv, bw), af) - | psimpl T = T - | psimpl F = F - | psimpl (QAll ap) = QAll ap - | psimpl (QEx aq) = QEx aq - | psimpl (And (p, q)) = - let val p' = psimpl p - in (case p' of - Lt (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | Gt (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | Le (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | Ge (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | Eq (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | Divides (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | T => psimpl q | F => F - | NOT x => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | And (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | Or (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | Imp (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | Equ (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | QAll x => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end - | QEx x => - let val q' = psimpl q - in (case q' of Lt (x, xa) => And (p', q') - | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q') - | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q') - | Divides (x, xa) => And (p', q') | T => p' | F => F - | NOT x => And (p', q') | And (x, xa) => And (p', q') - | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q') - | Equ (x, xa) => And (p', q') | QAll x => And (p', q') - | QEx x => And (p', q')) - end) - end - | psimpl (Or (p, q)) = - let val p' = psimpl p - in (case p' of - Lt (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') | Gt (x, xa) => Or (p', q') - | Le (x, xa) => Or (p', q') | Ge (x, xa) => Or (p', q') - | Eq (x, xa) => Or (p', q') | Divides (x, xa) => Or (p', q') - | T => T | F => p' | NOT x => Or (p', q') - | And (x, xa) => Or (p', q') | Or (x, xa) => Or (p', q') - | Imp (x, xa) => Or (p', q') | Equ (x, xa) => Or (p', q') - | QAll x => Or (p', q') | QEx x => Or (p', q')) - end - | Gt (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | Le (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | Ge (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | Eq (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | Divides (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | T => T | F => psimpl q - | NOT x => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | And (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | Or (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | Imp (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | Equ (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | QAll x => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end - | QEx x => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Or (p', q') - | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q') - | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q') - | Divides (x, xa) => Or (p', q') | T => T | F => p' - | NOT x => Or (p', q') | And (x, xa) => Or (p', q') - | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q') - | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q') - | QEx x => Or (p', q')) - end) - end - | psimpl (Imp (p, q)) = - let val p' = psimpl p - in (case p' of - Lt (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | Gt (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | Le (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | Ge (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | Eq (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | Divides (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | T => psimpl q | F => T - | NOT x => - let val q' = psimpl q - in (case q' of Lt (xa, xb) => Or (x, q') - | Gt (xa, xb) => Or (x, q') | Le (xa, xb) => Or (x, q') - | Ge (xa, xb) => Or (x, q') | Eq (xa, xb) => Or (x, q') - | Divides (xa, xb) => Or (x, q') | T => T | F => x - | NOT xa => Or (x, q') | And (xa, xb) => Or (x, q') - | Or (xa, xb) => Or (x, q') | Imp (xa, xb) => Or (x, q') - | Equ (xa, xb) => Or (x, q') | QAll xa => Or (x, q') - | QEx xa => Or (x, q')) - end - | And (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | Or (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | Imp (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | Equ (x, xa) => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | QAll x => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end - | QEx x => - let val q' = psimpl q - in (case q' of Lt (x, xa) => Imp (p', q') - | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q') - | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q') - | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p' - | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q') - | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q') - | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q') - | QEx x => Imp (p', q')) - end) - end; - -fun subst_it i (Cst b) = Cst b - | subst_it i (Var n) = (if (n = 0) then i else Var n) - | subst_it i (Neg it) = Neg (subst_it i it) - | subst_it i (Add (it1, it2)) = Add (subst_it i it1, subst_it i it2) - | subst_it i (Sub (it1, it2)) = Sub (subst_it i it1, subst_it i it2) - | subst_it i (Mult (it1, it2)) = Mult (subst_it i it1, subst_it i it2); - -fun subst_p i (Le (it1, it2)) = Le (subst_it i it1, subst_it i it2) - | subst_p i (Lt (it1, it2)) = Lt (subst_it i it1, subst_it i it2) - | subst_p i (Ge (it1, it2)) = Ge (subst_it i it1, subst_it i it2) - | subst_p i (Gt (it1, it2)) = Gt (subst_it i it1, subst_it i it2) - | subst_p i (Eq (it1, it2)) = Eq (subst_it i it1, subst_it i it2) - | subst_p i (Divides (d, t)) = Divides (subst_it i d, subst_it i t) - | subst_p i T = T - | subst_p i F = F - | subst_p i (And (p, q)) = And (subst_p i p, subst_p i q) - | subst_p i (Or (p, q)) = Or (subst_p i p, subst_p i q) - | subst_p i (Imp (p, q)) = Imp (subst_p i p, subst_p i q) - | subst_p i (Equ (p, q)) = Equ (subst_p i p, subst_p i q) - | subst_p i (NOT p) = NOT (subst_p i p); - -fun explode_disj ([], p) = F - | explode_disj ((i :: is), p) = - let val pi = psimpl (subst_p i p) - in (case pi of - Lt (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | Gt (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | Le (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | Ge (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | Eq (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | Divides (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | T => T | F => explode_disj (is, p) - | NOT x => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | And (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | Or (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | Imp (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | Equ (x, xa) => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | QAll x => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end - | QEx x => - let val r = explode_disj (is, p) - in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r) - | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r) - | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r) - | T => T | F => pi | NOT x => Or (pi, r) - | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r) - | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r) - | QAll x => Or (pi, r) | QEx x => Or (pi, r)) - end) - end; - -fun minusinf (And (p, q)) = And (minusinf p, minusinf q) - | minusinf (Or (p, q)) = Or (minusinf p, minusinf q) - | minusinf (Lt (u, v)) = Lt (u, v) - | minusinf (Gt (w, x)) = Gt (w, x) - | minusinf (Le (Cst bo, z)) = Le (Cst bo, z) - | minusinf (Le (Var bp, z)) = Le (Var bp, z) - | minusinf (Le (Neg bq, z)) = Le (Neg bq, z) - | minusinf (Le (Add (Cst cg, bs), z)) = Le (Add (Cst cg, bs), z) - | minusinf (Le (Add (Var ch, bs), z)) = Le (Add (Var ch, bs), z) - | minusinf (Le (Add (Neg ci, bs), z)) = Le (Add (Neg ci, bs), z) - | minusinf (Le (Add (Add (cj, ck), bs), z)) = Le (Add (Add (cj, ck), bs), z) - | minusinf (Le (Add (Sub (cl, cm), bs), z)) = Le (Add (Sub (cl, cm), bs), z) - | minusinf (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = - Le (Add (Mult (Cst cy, Cst dq), bs), z) - | minusinf (Le (Add (Mult (Cst cy, Var ei), bs), z)) = - (if (ei = 0) then (if (cy < 0) then F else T) - else Le (Add (Mult (Cst cy, Var (op_45_def0 ei id_1_def0 + 1)), bs), z)) - | minusinf (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = - Le (Add (Mult (Cst cy, Neg ds), bs), z) - | minusinf (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = - Le (Add (Mult (Cst cy, Add (dt, du)), bs), z) - | minusinf (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = - Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z) - | minusinf (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = - Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z) - | minusinf (Le (Add (Mult (Var cz, co), bs), z)) = - Le (Add (Mult (Var cz, co), bs), z) - | minusinf (Le (Add (Mult (Neg da, co), bs), z)) = - Le (Add (Mult (Neg da, co), bs), z) - | minusinf (Le (Add (Mult (Add (db, dc), co), bs), z)) = - Le (Add (Mult (Add (db, dc), co), bs), z) - | minusinf (Le (Add (Mult (Sub (dd, de), co), bs), z)) = - Le (Add (Mult (Sub (dd, de), co), bs), z) - | minusinf (Le (Add (Mult (Mult (df, dg), co), bs), z)) = - Le (Add (Mult (Mult (df, dg), co), bs), z) - | minusinf (Le (Sub (bt, bu), z)) = Le (Sub (bt, bu), z) - | minusinf (Le (Mult (bv, bw), z)) = Le (Mult (bv, bw), z) - | minusinf (Ge (aa, ab)) = Ge (aa, ab) - | minusinf (Eq (Cst ek, ad)) = Eq (Cst ek, ad) - | minusinf (Eq (Var el, ad)) = Eq (Var el, ad) - | minusinf (Eq (Neg em, ad)) = Eq (Neg em, ad) - | minusinf (Eq (Add (Cst fc, eo), ad)) = Eq (Add (Cst fc, eo), ad) - | minusinf (Eq (Add (Var fd, eo), ad)) = Eq (Add (Var fd, eo), ad) - | minusinf (Eq (Add (Neg fe, eo), ad)) = Eq (Add (Neg fe, eo), ad) - | minusinf (Eq (Add (Add (ff, fg), eo), ad)) = Eq (Add (Add (ff, fg), eo), ad) - | minusinf (Eq (Add (Sub (fh, fi), eo), ad)) = Eq (Add (Sub (fh, fi), eo), ad) - | minusinf (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = - Eq (Add (Mult (Cst fu, Cst gm), eo), ad) - | minusinf (Eq (Add (Mult (Cst fu, Var he), eo), ad)) = - (if (he = 0) then F - else Eq (Add (Mult (Cst fu, Var (op_45_def0 he id_1_def0 + 1)), eo), ad)) - | minusinf (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = - Eq (Add (Mult (Cst fu, Neg go), eo), ad) - | minusinf (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = - Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad) - | minusinf (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = - Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad) - | minusinf (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = - Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad) - | minusinf (Eq (Add (Mult (Var fv, fk), eo), ad)) = - Eq (Add (Mult (Var fv, fk), eo), ad) - | minusinf (Eq (Add (Mult (Neg fw, fk), eo), ad)) = - Eq (Add (Mult (Neg fw, fk), eo), ad) - | minusinf (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = - Eq (Add (Mult (Add (fx, fy), fk), eo), ad) - | minusinf (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = - Eq (Add (Mult (Sub (fz, ga), fk), eo), ad) - | minusinf (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = - Eq (Add (Mult (Mult (gb, gc), fk), eo), ad) - | minusinf (Eq (Sub (ep, eq), ad)) = Eq (Sub (ep, eq), ad) - | minusinf (Eq (Mult (er, es), ad)) = Eq (Mult (er, es), ad) - | minusinf (Divides (ae, af)) = Divides (ae, af) - | minusinf T = T - | minusinf F = F - | minusinf (NOT (Lt (hg, hh))) = NOT (Lt (hg, hh)) - | minusinf (NOT (Gt (hi, hj))) = NOT (Gt (hi, hj)) - | minusinf (NOT (Le (hk, hl))) = NOT (Le (hk, hl)) - | minusinf (NOT (Ge (hm, hn))) = NOT (Ge (hm, hn)) - | minusinf (NOT (Eq (Cst ja, hp))) = NOT (Eq (Cst ja, hp)) - | minusinf (NOT (Eq (Var jb, hp))) = NOT (Eq (Var jb, hp)) - | minusinf (NOT (Eq (Neg jc, hp))) = NOT (Eq (Neg jc, hp)) - | minusinf (NOT (Eq (Add (Cst js, je), hp))) = NOT (Eq (Add (Cst js, je), hp)) - | minusinf (NOT (Eq (Add (Var jt, je), hp))) = NOT (Eq (Add (Var jt, je), hp)) - | minusinf (NOT (Eq (Add (Neg ju, je), hp))) = NOT (Eq (Add (Neg ju, je), hp)) - | minusinf (NOT (Eq (Add (Add (jv, jw), je), hp))) = - NOT (Eq (Add (Add (jv, jw), je), hp)) - | minusinf (NOT (Eq (Add (Sub (jx, jy), je), hp))) = - NOT (Eq (Add (Sub (jx, jy), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = - NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) = - (if (lu = 0) then T - else NOT (Eq (Add (Mult (Cst kk, Var (op_45_def0 lu id_1_def0 + 1)), je), - hp))) - | minusinf (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = - NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = - NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = - NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = - NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = - NOT (Eq (Add (Mult (Var kl, ka), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = - NOT (Eq (Add (Mult (Neg km, ka), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = - NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = - NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp)) - | minusinf (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = - NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp)) - | minusinf (NOT (Eq (Sub (jf, jg), hp))) = NOT (Eq (Sub (jf, jg), hp)) - | minusinf (NOT (Eq (Mult (jh, ji), hp))) = NOT (Eq (Mult (jh, ji), hp)) - | minusinf (NOT (Divides (hq, hr))) = NOT (Divides (hq, hr)) - | minusinf (NOT T) = NOT T - | minusinf (NOT F) = NOT F - | minusinf (NOT (NOT hs)) = NOT (NOT hs) - | minusinf (NOT (And (ht, hu))) = NOT (And (ht, hu)) - | minusinf (NOT (Or (hv, hw))) = NOT (Or (hv, hw)) - | minusinf (NOT (Imp (hx, hy))) = NOT (Imp (hx, hy)) - | minusinf (NOT (Equ (hz, ia))) = NOT (Equ (hz, ia)) - | minusinf (NOT (QAll ib)) = NOT (QAll ib) - | minusinf (NOT (QEx ic)) = NOT (QEx ic) - | minusinf (Imp (al, am)) = Imp (al, am) - | minusinf (Equ (an, ao)) = Equ (an, ao) - | minusinf (QAll ap) = QAll ap - | minusinf (QEx aq) = QEx aq; - -fun abs (i:IntInf.int) = (if (i < 0) then IntInf.~ i else i); - -fun op_div_def1 a b = fst (divAlg (a, b)); - -fun op_mod_def0 m n = nat (op_mod_def1 (m) (n)); - -fun ngcd (m:IntInf.int, n:IntInf.int) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n)); - -fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x; - -fun ilcm (a:IntInf.int) (b:IntInf.int) = op_div_def1 (a * b) (igcd (a, b)); - -fun divlcm (NOT p) = divlcm p - | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q) - | divlcm (Or (p, q)) = ilcm (divlcm p) (divlcm q) - | divlcm (Lt (u, v)) = 1 - | divlcm (Gt (w, x)) = 1 - | divlcm (Le (y, z)) = 1 - | divlcm (Ge (aa, ab)) = 1 - | divlcm (Eq (ac, ad)) = 1 - | divlcm (Divides (Cst bo, Cst cg)) = 1 - | divlcm (Divides (Cst bo, Var ch)) = 1 - | divlcm (Divides (Cst bo, Neg ci)) = 1 - | divlcm (Divides (Cst bo, Add (Cst cy, ck))) = 1 - | divlcm (Divides (Cst bo, Add (Var cz, ck))) = 1 - | divlcm (Divides (Cst bo, Add (Neg da, ck))) = 1 - | divlcm (Divides (Cst bo, Add (Add (db, dc), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Sub (dd, de), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Cst ei), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Var fa), ck))) = - (if (fa = 0) then abs bo else 1) - | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Neg ek), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Add (el, em)), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Sub (en, eo)), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Mult (ep, eq)), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Var dr, dg), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Neg ds, dg), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Add (dt, du), dg), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Sub (dv, dw), dg), ck))) = 1 - | divlcm (Divides (Cst bo, Add (Mult (Mult (dx, dy), dg), ck))) = 1 - | divlcm (Divides (Cst bo, Sub (cl, cm))) = 1 - | divlcm (Divides (Cst bo, Mult (cn, co))) = 1 - | divlcm (Divides (Var bp, af)) = 1 - | divlcm (Divides (Neg bq, af)) = 1 - | divlcm (Divides (Add (br, bs), af)) = 1 - | divlcm (Divides (Sub (bt, bu), af)) = 1 - | divlcm (Divides (Mult (bv, bw), af)) = 1 - | divlcm T = 1 - | divlcm F = 1 - | divlcm (Imp (al, am)) = 1 - | divlcm (Equ (an, ao)) = 1 - | divlcm (QAll ap) = 1 - | divlcm (QEx aq) = 1; - -fun explode_minf (q, B) = - let val d = divlcm q; val pm = minusinf q; - val dj1 = explode_disj (map (fn x => Cst x) (iupto (1, d)), pm) - in (case dj1 of - Lt (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | Gt (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | Le (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | Ge (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | Eq (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | Divides (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | T => T | F => explode_disj (all_sums (d, B), q) - | NOT x => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | And (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | Or (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | Imp (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | Equ (x, xa) => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | QAll x => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end - | QEx x => - let val dj2 = explode_disj (all_sums (d, B), q) - in (case dj2 of Lt (x, xa) => Or (dj1, dj2) - | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2) - | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2) - | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1 - | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2) - | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2) - | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2) - | QEx x => Or (dj1, dj2)) - end) - end; - -fun mirror (And (p, q)) = And (mirror p, mirror q) - | mirror (Or (p, q)) = Or (mirror p, mirror q) - | mirror (Lt (u, v)) = Lt (u, v) - | mirror (Gt (w, x)) = Gt (w, x) - | mirror (Le (Cst bp, aa)) = Le (Cst bp, aa) - | mirror (Le (Var bq, aa)) = Le (Var bq, aa) - | mirror (Le (Neg br, aa)) = Le (Neg br, aa) - | mirror (Le (Add (Cst ch, bt), aa)) = Le (Add (Cst ch, bt), aa) - | mirror (Le (Add (Var ci, bt), aa)) = Le (Add (Var ci, bt), aa) - | mirror (Le (Add (Neg cj, bt), aa)) = Le (Add (Neg cj, bt), aa) - | mirror (Le (Add (Add (ck, cl), bt), aa)) = Le (Add (Add (ck, cl), bt), aa) - | mirror (Le (Add (Sub (cm, cn), bt), aa)) = Le (Add (Sub (cm, cn), bt), aa) - | mirror (Le (Add (Mult (Cst cz, Cst dr), bt), aa)) = - Le (Add (Mult (Cst cz, Cst dr), bt), aa) - | mirror (Le (Add (Mult (Cst cz, Var ej), bt), aa)) = - (if (ej = 0) then Le (Add (Mult (Cst (~ cz), Var 0), bt), aa) - else Le (Add (Mult (Cst cz, Var (op_45_def0 ej id_1_def0 + 1)), bt), aa)) - | mirror (Le (Add (Mult (Cst cz, Neg dt), bt), aa)) = - Le (Add (Mult (Cst cz, Neg dt), bt), aa) - | mirror (Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)) = - Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa) - | mirror (Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)) = - Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa) - | mirror (Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)) = - Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa) - | mirror (Le (Add (Mult (Var da, cp), bt), aa)) = - Le (Add (Mult (Var da, cp), bt), aa) - | mirror (Le (Add (Mult (Neg db, cp), bt), aa)) = - Le (Add (Mult (Neg db, cp), bt), aa) - | mirror (Le (Add (Mult (Add (dc, dd), cp), bt), aa)) = - Le (Add (Mult (Add (dc, dd), cp), bt), aa) - | mirror (Le (Add (Mult (Sub (de, df), cp), bt), aa)) = - Le (Add (Mult (Sub (de, df), cp), bt), aa) - | mirror (Le (Add (Mult (Mult (dg, dh), cp), bt), aa)) = - Le (Add (Mult (Mult (dg, dh), cp), bt), aa) - | mirror (Le (Sub (bu, bv), aa)) = Le (Sub (bu, bv), aa) - | mirror (Le (Mult (bw, bx), aa)) = Le (Mult (bw, bx), aa) - | mirror (Ge (ab, ac)) = Ge (ab, ac) - | mirror (Eq (Cst el, ae)) = Eq (Cst el, ae) - | mirror (Eq (Var em, ae)) = Eq (Var em, ae) - | mirror (Eq (Neg en, ae)) = Eq (Neg en, ae) - | mirror (Eq (Add (Cst fd, ep), ae)) = Eq (Add (Cst fd, ep), ae) - | mirror (Eq (Add (Var fe, ep), ae)) = Eq (Add (Var fe, ep), ae) - | mirror (Eq (Add (Neg ff, ep), ae)) = Eq (Add (Neg ff, ep), ae) - | mirror (Eq (Add (Add (fg, fh), ep), ae)) = Eq (Add (Add (fg, fh), ep), ae) - | mirror (Eq (Add (Sub (fi, fj), ep), ae)) = Eq (Add (Sub (fi, fj), ep), ae) - | mirror (Eq (Add (Mult (Cst fv, Cst gn), ep), ae)) = - Eq (Add (Mult (Cst fv, Cst gn), ep), ae) - | mirror (Eq (Add (Mult (Cst fv, Var hf), ep), ae)) = - (if (hf = 0) then Eq (Add (Mult (Cst (~ fv), Var 0), ep), ae) - else Eq (Add (Mult (Cst fv, Var (op_45_def0 hf id_1_def0 + 1)), ep), ae)) - | mirror (Eq (Add (Mult (Cst fv, Neg gp), ep), ae)) = - Eq (Add (Mult (Cst fv, Neg gp), ep), ae) - | mirror (Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)) = - Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae) - | mirror (Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)) = - Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae) - | mirror (Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)) = - Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae) - | mirror (Eq (Add (Mult (Var fw, fl), ep), ae)) = - Eq (Add (Mult (Var fw, fl), ep), ae) - | mirror (Eq (Add (Mult (Neg fx, fl), ep), ae)) = - Eq (Add (Mult (Neg fx, fl), ep), ae) - | mirror (Eq (Add (Mult (Add (fy, fz), fl), ep), ae)) = - Eq (Add (Mult (Add (fy, fz), fl), ep), ae) - | mirror (Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)) = - Eq (Add (Mult (Sub (ga, gb), fl), ep), ae) - | mirror (Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)) = - Eq (Add (Mult (Mult (gc, gd), fl), ep), ae) - | mirror (Eq (Sub (eq, er), ae)) = Eq (Sub (eq, er), ae) - | mirror (Eq (Mult (es, et), ae)) = Eq (Mult (es, et), ae) - | mirror (Divides (Cst hh, Cst hz)) = Divides (Cst hh, Cst hz) - | mirror (Divides (Cst hh, Var ia)) = Divides (Cst hh, Var ia) - | mirror (Divides (Cst hh, Neg ib)) = Divides (Cst hh, Neg ib) - | mirror (Divides (Cst hh, Add (Cst ir, id))) = - Divides (Cst hh, Add (Cst ir, id)) - | mirror (Divides (Cst hh, Add (Var is, id))) = - Divides (Cst hh, Add (Var is, id)) - | mirror (Divides (Cst hh, Add (Neg it, id))) = - Divides (Cst hh, Add (Neg it, id)) - | mirror (Divides (Cst hh, Add (Add (iu, iv), id))) = - Divides (Cst hh, Add (Add (iu, iv), id)) - | mirror (Divides (Cst hh, Add (Sub (iw, ix), id))) = - Divides (Cst hh, Add (Sub (iw, ix), id)) - | mirror (Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))) = - Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id)) - | mirror (Divides (Cst hh, Add (Mult (Cst jj, Var kt), id))) = - (if (kt = 0) then Divides (Cst hh, Add (Mult (Cst (~ jj), Var 0), id)) - else Divides - (Cst hh, - Add (Mult (Cst jj, Var (op_45_def0 kt id_1_def0 + 1)), id))) - | mirror (Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))) = - Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id)) - | mirror (Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))) = - Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id)) - | mirror (Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))) = - Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id)) - | mirror (Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))) = - Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id)) - | mirror (Divides (Cst hh, Add (Mult (Var jk, iz), id))) = - Divides (Cst hh, Add (Mult (Var jk, iz), id)) - | mirror (Divides (Cst hh, Add (Mult (Neg jl, iz), id))) = - Divides (Cst hh, Add (Mult (Neg jl, iz), id)) - | mirror (Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))) = - Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id)) - | mirror (Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))) = - Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id)) - | mirror (Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))) = - Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id)) - | mirror (Divides (Cst hh, Sub (ie, if'))) = Divides (Cst hh, Sub (ie, if')) - | mirror (Divides (Cst hh, Mult (ig, ih))) = Divides (Cst hh, Mult (ig, ih)) - | mirror (Divides (Var hi, ag)) = Divides (Var hi, ag) - | mirror (Divides (Neg hj, ag)) = Divides (Neg hj, ag) - | mirror (Divides (Add (hk, hl), ag)) = Divides (Add (hk, hl), ag) - | mirror (Divides (Sub (hm, hn), ag)) = Divides (Sub (hm, hn), ag) - | mirror (Divides (Mult (ho, hp), ag)) = Divides (Mult (ho, hp), ag) - | mirror T = T - | mirror F = F - | mirror (NOT (Lt (kv, kw))) = NOT (Lt (kv, kw)) - | mirror (NOT (Gt (kx, ky))) = NOT (Gt (kx, ky)) - | mirror (NOT (Le (kz, la))) = NOT (Le (kz, la)) - | mirror (NOT (Ge (lb, lc))) = NOT (Ge (lb, lc)) - | mirror (NOT (Eq (Cst mp, le))) = NOT (Eq (Cst mp, le)) - | mirror (NOT (Eq (Var mq, le))) = NOT (Eq (Var mq, le)) - | mirror (NOT (Eq (Neg mr, le))) = NOT (Eq (Neg mr, le)) - | mirror (NOT (Eq (Add (Cst nh, mt), le))) = NOT (Eq (Add (Cst nh, mt), le)) - | mirror (NOT (Eq (Add (Var ni, mt), le))) = NOT (Eq (Add (Var ni, mt), le)) - | mirror (NOT (Eq (Add (Neg nj, mt), le))) = NOT (Eq (Add (Neg nj, mt), le)) - | mirror (NOT (Eq (Add (Add (nk, nl), mt), le))) = - NOT (Eq (Add (Add (nk, nl), mt), le)) - | mirror (NOT (Eq (Add (Sub (nm, nn), mt), le))) = - NOT (Eq (Add (Sub (nm, nn), mt), le)) - | mirror (NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))) = - NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le)) - | mirror (NOT (Eq (Add (Mult (Cst nz, Var pj), mt), le))) = - (if (pj = 0) then NOT (Eq (Add (Mult (Cst (~ nz), Var 0), mt), le)) - else NOT (Eq (Add (Mult (Cst nz, Var (op_45_def0 pj id_1_def0 + 1)), mt), - le))) - | mirror (NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))) = - NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le)) - | mirror (NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))) = - NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le)) - | mirror (NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))) = - NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le)) - | mirror (NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))) = - NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le)) - | mirror (NOT (Eq (Add (Mult (Var oa, np), mt), le))) = - NOT (Eq (Add (Mult (Var oa, np), mt), le)) - | mirror (NOT (Eq (Add (Mult (Neg ob, np), mt), le))) = - NOT (Eq (Add (Mult (Neg ob, np), mt), le)) - | mirror (NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))) = - NOT (Eq (Add (Mult (Add (oc, od), np), mt), le)) - | mirror (NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))) = - NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le)) - | mirror (NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))) = - NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le)) - | mirror (NOT (Eq (Sub (mu, mv), le))) = NOT (Eq (Sub (mu, mv), le)) - | mirror (NOT (Eq (Mult (mw, mx), le))) = NOT (Eq (Mult (mw, mx), le)) - | mirror (NOT (Divides (Cst pl, Cst qd))) = NOT (Divides (Cst pl, Cst qd)) - | mirror (NOT (Divides (Cst pl, Var qe))) = NOT (Divides (Cst pl, Var qe)) - | mirror (NOT (Divides (Cst pl, Neg qf))) = NOT (Divides (Cst pl, Neg qf)) - | mirror (NOT (Divides (Cst pl, Add (Cst qv, qh)))) = - NOT (Divides (Cst pl, Add (Cst qv, qh))) - | mirror (NOT (Divides (Cst pl, Add (Var qw, qh)))) = - NOT (Divides (Cst pl, Add (Var qw, qh))) - | mirror (NOT (Divides (Cst pl, Add (Neg qx, qh)))) = - NOT (Divides (Cst pl, Add (Neg qx, qh))) - | mirror (NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))) = - NOT (Divides (Cst pl, Add (Add (qy, qz), qh))) - | mirror (NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))) = - NOT (Divides (Cst pl, Add (Sub (ra, rb), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Var sx), qh)))) = - (if (sx = 0) - then NOT (Divides (Cst pl, Add (Mult (Cst (~ rn), Var 0), qh))) - else NOT (Divides - (Cst pl, - Add (Mult (Cst rn, Var (op_45_def0 sx id_1_def0 + 1)), - qh)))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh))) - | mirror (NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))) = - NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh))) - | mirror (NOT (Divides (Cst pl, Sub (qi, qj)))) = - NOT (Divides (Cst pl, Sub (qi, qj))) - | mirror (NOT (Divides (Cst pl, Mult (qk, ql)))) = - NOT (Divides (Cst pl, Mult (qk, ql))) - | mirror (NOT (Divides (Var pm, lg))) = NOT (Divides (Var pm, lg)) - | mirror (NOT (Divides (Neg pn, lg))) = NOT (Divides (Neg pn, lg)) - | mirror (NOT (Divides (Add (po, pp), lg))) = NOT (Divides (Add (po, pp), lg)) - | mirror (NOT (Divides (Sub (pq, pr), lg))) = NOT (Divides (Sub (pq, pr), lg)) - | mirror (NOT (Divides (Mult (ps, pt), lg))) = - NOT (Divides (Mult (ps, pt), lg)) - | mirror (NOT T) = NOT T - | mirror (NOT F) = NOT F - | mirror (NOT (NOT lh)) = NOT (NOT lh) - | mirror (NOT (And (li, lj))) = NOT (And (li, lj)) - | mirror (NOT (Or (lk, ll))) = NOT (Or (lk, ll)) - | mirror (NOT (Imp (lm, ln))) = NOT (Imp (lm, ln)) - | mirror (NOT (Equ (lo, lp))) = NOT (Equ (lo, lp)) - | mirror (NOT (QAll lq)) = NOT (QAll lq) - | mirror (NOT (QEx lr)) = NOT (QEx lr) - | mirror (Imp (am, an)) = Imp (am, an) - | mirror (Equ (ao, ap)) = Equ (ao, ap) - | mirror (QAll aq) = QAll aq - | mirror (QEx ar) = QEx ar; - -fun op_43_def0 m n = nat ((m) + (n)); - -fun size_def1 [] = (0:IntInf.int) - | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1); - -fun aset (And (p, q)) = op_64 (aset p) (aset q) - | aset (Or (p, q)) = op_64 (aset p) (aset q) - | aset (Lt (u, v)) = [] - | aset (Gt (w, x)) = [] - | aset (Le (Cst bo, z)) = [] - | aset (Le (Var bp, z)) = [] - | aset (Le (Neg bq, z)) = [] - | aset (Le (Add (Cst cg, bs), z)) = [] - | aset (Le (Add (Var ch, bs), z)) = [] - | aset (Le (Add (Neg ci, bs), z)) = [] - | aset (Le (Add (Add (cj, ck), bs), z)) = [] - | aset (Le (Add (Sub (cl, cm), bs), z)) = [] - | aset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = [] - | aset (Le (Add (Mult (Cst cy, Var ei), bs), z)) = - (if (ei = 0) - then (if (cy < 0) then [lin_add (bs, Cst 1)] - else [lin_neg bs, lin_add (lin_neg bs, Cst 1)]) - else []) - | aset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = [] - | aset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = [] - | aset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = [] - | aset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = [] - | aset (Le (Add (Mult (Var cz, co), bs), z)) = [] - | aset (Le (Add (Mult (Neg da, co), bs), z)) = [] - | aset (Le (Add (Mult (Add (db, dc), co), bs), z)) = [] - | aset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = [] - | aset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = [] - | aset (Le (Sub (bt, bu), z)) = [] - | aset (Le (Mult (bv, bw), z)) = [] - | aset (Ge (aa, ab)) = [] - | aset (Eq (Cst ek, ad)) = [] - | aset (Eq (Var el, ad)) = [] - | aset (Eq (Neg em, ad)) = [] - | aset (Eq (Add (Cst fc, eo), ad)) = [] - | aset (Eq (Add (Var fd, eo), ad)) = [] - | aset (Eq (Add (Neg fe, eo), ad)) = [] - | aset (Eq (Add (Add (ff, fg), eo), ad)) = [] - | aset (Eq (Add (Sub (fh, fi), eo), ad)) = [] - | aset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = [] - | aset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) = - (if (he = 0) - then (if (fu < 0) then [lin_add (eo, Cst 1)] - else [lin_add (lin_neg eo, Cst 1)]) - else []) - | aset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = [] - | aset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = [] - | aset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = [] - | aset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = [] - | aset (Eq (Add (Mult (Var fv, fk), eo), ad)) = [] - | aset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = [] - | aset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = [] - | aset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = [] - | aset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = [] - | aset (Eq (Sub (ep, eq), ad)) = [] - | aset (Eq (Mult (er, es), ad)) = [] - | aset (Divides (ae, af)) = [] - | aset T = [] - | aset F = [] - | aset (NOT (Lt (hg, hh))) = [] - | aset (NOT (Gt (hi, hj))) = [] - | aset (NOT (Le (hk, hl))) = [] - | aset (NOT (Ge (hm, hn))) = [] - | aset (NOT (Eq (Cst ja, hp))) = [] - | aset (NOT (Eq (Var jb, hp))) = [] - | aset (NOT (Eq (Neg jc, hp))) = [] - | aset (NOT (Eq (Add (Cst js, je), hp))) = [] - | aset (NOT (Eq (Add (Var jt, je), hp))) = [] - | aset (NOT (Eq (Add (Neg ju, je), hp))) = [] - | aset (NOT (Eq (Add (Add (jv, jw), je), hp))) = [] - | aset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) = - (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else []) - | aset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = [] - | aset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = [] - | aset (NOT (Eq (Sub (jf, jg), hp))) = [] - | aset (NOT (Eq (Mult (jh, ji), hp))) = [] - | aset (NOT (Divides (hq, hr))) = [] - | aset (NOT T) = [] - | aset (NOT F) = [] - | aset (NOT (NOT hs)) = [] - | aset (NOT (And (ht, hu))) = [] - | aset (NOT (Or (hv, hw))) = [] - | aset (NOT (Imp (hx, hy))) = [] - | aset (NOT (Equ (hz, ia))) = [] - | aset (NOT (QAll ib)) = [] - | aset (NOT (QEx ic)) = [] - | aset (Imp (al, am)) = [] - | aset (Equ (an, ao)) = [] - | aset (QAll ap) = [] - | aset (QEx aq) = []; - -fun op_mem x [] = false - | op_mem x (y :: ys) = (if (y = x) then true else op_mem x ys); - -fun list_insert x xs = (if op_mem x xs then xs else (x :: xs)); - -fun list_set [] = [] - | list_set (x :: xs) = list_insert x (list_set xs); - -fun bset (And (p, q)) = op_64 (bset p) (bset q) - | bset (Or (p, q)) = op_64 (bset p) (bset q) - | bset (Lt (u, v)) = [] - | bset (Gt (w, x)) = [] - | bset (Le (Cst bo, z)) = [] - | bset (Le (Var bp, z)) = [] - | bset (Le (Neg bq, z)) = [] - | bset (Le (Add (Cst cg, bs), z)) = [] - | bset (Le (Add (Var ch, bs), z)) = [] - | bset (Le (Add (Neg ci, bs), z)) = [] - | bset (Le (Add (Add (cj, ck), bs), z)) = [] - | bset (Le (Add (Sub (cl, cm), bs), z)) = [] - | bset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = [] - | bset (Le (Add (Mult (Cst cy, Var ei), bs), z)) = - (if (ei = 0) - then (if (cy < 0) then [lin_add (bs, Cst ~1), bs] - else [lin_add (lin_neg bs, Cst ~1)]) - else []) - | bset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = [] - | bset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = [] - | bset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = [] - | bset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = [] - | bset (Le (Add (Mult (Var cz, co), bs), z)) = [] - | bset (Le (Add (Mult (Neg da, co), bs), z)) = [] - | bset (Le (Add (Mult (Add (db, dc), co), bs), z)) = [] - | bset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = [] - | bset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = [] - | bset (Le (Sub (bt, bu), z)) = [] - | bset (Le (Mult (bv, bw), z)) = [] - | bset (Ge (aa, ab)) = [] - | bset (Eq (Cst ek, ad)) = [] - | bset (Eq (Var el, ad)) = [] - | bset (Eq (Neg em, ad)) = [] - | bset (Eq (Add (Cst fc, eo), ad)) = [] - | bset (Eq (Add (Var fd, eo), ad)) = [] - | bset (Eq (Add (Neg fe, eo), ad)) = [] - | bset (Eq (Add (Add (ff, fg), eo), ad)) = [] - | bset (Eq (Add (Sub (fh, fi), eo), ad)) = [] - | bset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = [] - | bset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) = - (if (he = 0) - then (if (fu < 0) then [lin_add (eo, Cst ~1)] - else [lin_add (lin_neg eo, Cst ~1)]) - else []) - | bset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = [] - | bset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = [] - | bset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = [] - | bset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = [] - | bset (Eq (Add (Mult (Var fv, fk), eo), ad)) = [] - | bset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = [] - | bset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = [] - | bset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = [] - | bset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = [] - | bset (Eq (Sub (ep, eq), ad)) = [] - | bset (Eq (Mult (er, es), ad)) = [] - | bset (Divides (ae, af)) = [] - | bset T = [] - | bset F = [] - | bset (NOT (Lt (hg, hh))) = [] - | bset (NOT (Gt (hi, hj))) = [] - | bset (NOT (Le (hk, hl))) = [] - | bset (NOT (Ge (hm, hn))) = [] - | bset (NOT (Eq (Cst ja, hp))) = [] - | bset (NOT (Eq (Var jb, hp))) = [] - | bset (NOT (Eq (Neg jc, hp))) = [] - | bset (NOT (Eq (Add (Cst js, je), hp))) = [] - | bset (NOT (Eq (Add (Var jt, je), hp))) = [] - | bset (NOT (Eq (Add (Neg ju, je), hp))) = [] - | bset (NOT (Eq (Add (Add (jv, jw), je), hp))) = [] - | bset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) = - (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else []) - | bset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = [] - | bset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = [] - | bset (NOT (Eq (Sub (jf, jg), hp))) = [] - | bset (NOT (Eq (Mult (jh, ji), hp))) = [] - | bset (NOT (Divides (hq, hr))) = [] - | bset (NOT T) = [] - | bset (NOT F) = [] - | bset (NOT (NOT hs)) = [] - | bset (NOT (And (ht, hu))) = [] - | bset (NOT (Or (hv, hw))) = [] - | bset (NOT (Imp (hx, hy))) = [] - | bset (NOT (Equ (hz, ia))) = [] - | bset (NOT (QAll ib)) = [] - | bset (NOT (QEx ic)) = [] - | bset (Imp (al, am)) = [] - | bset (Equ (an, ao)) = [] - | bset (QAll ap) = [] - | bset (QEx aq) = []; - -fun adjustcoeff (l:IntInf.int, Le (Add (Mult (Cst c, Var 0), r), Cst i)) = - (if (c <= 0) - then Le (Add (Mult (Cst ~1, Var 0), lin_mul (~ (op_div_def1 l c), r)), - Cst 0) - else Le (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0)) - | adjustcoeff (l, Eq (Add (Mult (Cst c, Var 0), r), Cst i)) = - Eq (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst c, Var 0), r), Cst i))) = - NOT (Eq (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0)) - | adjustcoeff (l, And (p, q)) = And (adjustcoeff (l, p), adjustcoeff (l, q)) - | adjustcoeff (l, Or (p, q)) = Or (adjustcoeff (l, p), adjustcoeff (l, q)) - | adjustcoeff (l, Lt (w, x)) = Lt (w, x) - | adjustcoeff (l, Gt (y, z)) = Gt (y, z) - | adjustcoeff (l, Le (Cst bq, ab)) = Le (Cst bq, ab) - | adjustcoeff (l, Le (Var br, ab)) = Le (Var br, ab) - | adjustcoeff (l, Le (Neg bs, ab)) = Le (Neg bs, ab) - | adjustcoeff (l, Le (Add (Cst ci, bu), ab)) = Le (Add (Cst ci, bu), ab) - | adjustcoeff (l, Le (Add (Var cj, bu), ab)) = Le (Add (Var cj, bu), ab) - | adjustcoeff (l, Le (Add (Neg ck, bu), ab)) = Le (Add (Neg ck, bu), ab) - | adjustcoeff (l, Le (Add (Add (cl, cm), bu), ab)) = - Le (Add (Add (cl, cm), bu), ab) - | adjustcoeff (l, Le (Add (Sub (cn, co), bu), ab)) = - Le (Add (Sub (cn, co), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Cst da, Cst ds), bu), ab)) = - Le (Add (Mult (Cst da, Cst ds), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Var en)) = - Le (Add (Mult (Cst da, Var 0), bu), Var en) - | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Neg eo)) = - Le (Add (Mult (Cst da, Var 0), bu), Neg eo) - | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Add (ep, eq))) = - Le (Add (Mult (Cst da, Var 0), bu), Add (ep, eq)) - | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Sub (er, es))) = - Le (Add (Mult (Cst da, Var 0), bu), Sub (er, es)) - | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Mult (et, eu))) = - Le (Add (Mult (Cst da, Var 0), bu), Mult (et, eu)) - | adjustcoeff (l, Le (Add (Mult (Cst da, Var ek), bu), ab)) = - Le (Add (Mult (Cst da, Var ek), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Cst da, Neg du), bu), ab)) = - Le (Add (Mult (Cst da, Neg du), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Cst da, Add (dv, dw)), bu), ab)) = - Le (Add (Mult (Cst da, Add (dv, dw)), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Cst da, Sub (dx, dy)), bu), ab)) = - Le (Add (Mult (Cst da, Sub (dx, dy)), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Cst da, Mult (dz, ea)), bu), ab)) = - Le (Add (Mult (Cst da, Mult (dz, ea)), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Var db, cq), bu), ab)) = - Le (Add (Mult (Var db, cq), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Neg dc, cq), bu), ab)) = - Le (Add (Mult (Neg dc, cq), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Add (dd, de), cq), bu), ab)) = - Le (Add (Mult (Add (dd, de), cq), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Sub (df, dg), cq), bu), ab)) = - Le (Add (Mult (Sub (df, dg), cq), bu), ab) - | adjustcoeff (l, Le (Add (Mult (Mult (dh, di), cq), bu), ab)) = - Le (Add (Mult (Mult (dh, di), cq), bu), ab) - | adjustcoeff (l, Le (Sub (bv, bw), ab)) = Le (Sub (bv, bw), ab) - | adjustcoeff (l, Le (Mult (bx, by), ab)) = Le (Mult (bx, by), ab) - | adjustcoeff (l, Ge (ac, ad)) = Ge (ac, ad) - | adjustcoeff (l, Eq (Cst fe, af)) = Eq (Cst fe, af) - | adjustcoeff (l, Eq (Var ff, af)) = Eq (Var ff, af) - | adjustcoeff (l, Eq (Neg fg, af)) = Eq (Neg fg, af) - | adjustcoeff (l, Eq (Add (Cst fw, fi), af)) = Eq (Add (Cst fw, fi), af) - | adjustcoeff (l, Eq (Add (Var fx, fi), af)) = Eq (Add (Var fx, fi), af) - | adjustcoeff (l, Eq (Add (Neg fy, fi), af)) = Eq (Add (Neg fy, fi), af) - | adjustcoeff (l, Eq (Add (Add (fz, ga), fi), af)) = - Eq (Add (Add (fz, ga), fi), af) - | adjustcoeff (l, Eq (Add (Sub (gb, gc), fi), af)) = - Eq (Add (Sub (gb, gc), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Cst hg), fi), af)) = - Eq (Add (Mult (Cst go, Cst hg), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Var ib)) = - Eq (Add (Mult (Cst go, Var 0), fi), Var ib) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Neg ic)) = - Eq (Add (Mult (Cst go, Var 0), fi), Neg ic) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Add (id, ie))) = - Eq (Add (Mult (Cst go, Var 0), fi), Add (id, ie)) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Sub (if', ig))) = - Eq (Add (Mult (Cst go, Var 0), fi), Sub (if', ig)) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Mult (ih, ii))) = - Eq (Add (Mult (Cst go, Var 0), fi), Mult (ih, ii)) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Var hy), fi), af)) = - Eq (Add (Mult (Cst go, Var hy), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Neg hi), fi), af)) = - Eq (Add (Mult (Cst go, Neg hi), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Add (hj, hk)), fi), af)) = - Eq (Add (Mult (Cst go, Add (hj, hk)), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Sub (hl, hm)), fi), af)) = - Eq (Add (Mult (Cst go, Sub (hl, hm)), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Cst go, Mult (hn, ho)), fi), af)) = - Eq (Add (Mult (Cst go, Mult (hn, ho)), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Var gp, ge), fi), af)) = - Eq (Add (Mult (Var gp, ge), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Neg gq, ge), fi), af)) = - Eq (Add (Mult (Neg gq, ge), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Add (gr, gs), ge), fi), af)) = - Eq (Add (Mult (Add (gr, gs), ge), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Sub (gt, gu), ge), fi), af)) = - Eq (Add (Mult (Sub (gt, gu), ge), fi), af) - | adjustcoeff (l, Eq (Add (Mult (Mult (gv, gw), ge), fi), af)) = - Eq (Add (Mult (Mult (gv, gw), ge), fi), af) - | adjustcoeff (l, Eq (Sub (fj, fk), af)) = Eq (Sub (fj, fk), af) - | adjustcoeff (l, Eq (Mult (fl, fm), af)) = Eq (Mult (fl, fm), af) - | adjustcoeff (l, Divides (Cst is, Cst jk)) = Divides (Cst is, Cst jk) - | adjustcoeff (l, Divides (Cst is, Var jl)) = Divides (Cst is, Var jl) - | adjustcoeff (l, Divides (Cst is, Neg jm)) = Divides (Cst is, Neg jm) - | adjustcoeff (l, Divides (Cst is, Add (Cst kc, jo))) = - Divides (Cst is, Add (Cst kc, jo)) - | adjustcoeff (l, Divides (Cst is, Add (Var kd, jo))) = - Divides (Cst is, Add (Var kd, jo)) - | adjustcoeff (l, Divides (Cst is, Add (Neg ke, jo))) = - Divides (Cst is, Add (Neg ke, jo)) - | adjustcoeff (l, Divides (Cst is, Add (Add (kf, kg), jo))) = - Divides (Cst is, Add (Add (kf, kg), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Sub (kh, ki), jo))) = - Divides (Cst is, Add (Sub (kh, ki), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Cst lm), jo))) = - Divides (Cst is, Add (Mult (Cst ku, Cst lm), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Var me), jo))) = - (if (me = 0) - then Divides - (Cst (op_div_def1 l ku * is), - Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l ku, jo))) - else Divides - (Cst is, - Add (Mult (Cst ku, Var (op_45_def0 me id_1_def0 + 1)), jo))) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Neg lo), jo))) = - Divides (Cst is, Add (Mult (Cst ku, Neg lo), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Add (lp, lq)), jo))) = - Divides (Cst is, Add (Mult (Cst ku, Add (lp, lq)), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Sub (lr, ls)), jo))) = - Divides (Cst is, Add (Mult (Cst ku, Sub (lr, ls)), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Mult (lt, lu)), jo))) = - Divides (Cst is, Add (Mult (Cst ku, Mult (lt, lu)), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Var kv, kk), jo))) = - Divides (Cst is, Add (Mult (Var kv, kk), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Neg kw, kk), jo))) = - Divides (Cst is, Add (Mult (Neg kw, kk), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Add (kx, ky), kk), jo))) = - Divides (Cst is, Add (Mult (Add (kx, ky), kk), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Sub (kz, la), kk), jo))) = - Divides (Cst is, Add (Mult (Sub (kz, la), kk), jo)) - | adjustcoeff (l, Divides (Cst is, Add (Mult (Mult (lb, lc), kk), jo))) = - Divides (Cst is, Add (Mult (Mult (lb, lc), kk), jo)) - | adjustcoeff (l, Divides (Cst is, Sub (jp, jq))) = - Divides (Cst is, Sub (jp, jq)) - | adjustcoeff (l, Divides (Cst is, Mult (jr, js))) = - Divides (Cst is, Mult (jr, js)) - | adjustcoeff (l, Divides (Var it, ah)) = Divides (Var it, ah) - | adjustcoeff (l, Divides (Neg iu, ah)) = Divides (Neg iu, ah) - | adjustcoeff (l, Divides (Add (iv, iw), ah)) = Divides (Add (iv, iw), ah) - | adjustcoeff (l, Divides (Sub (ix, iy), ah)) = Divides (Sub (ix, iy), ah) - | adjustcoeff (l, Divides (Mult (iz, ja), ah)) = Divides (Mult (iz, ja), ah) - | adjustcoeff (l, T) = T - | adjustcoeff (l, F) = F - | adjustcoeff (l, NOT (Lt (mg, mh))) = NOT (Lt (mg, mh)) - | adjustcoeff (l, NOT (Gt (mi, mj))) = NOT (Gt (mi, mj)) - | adjustcoeff (l, NOT (Le (mk, ml))) = NOT (Le (mk, ml)) - | adjustcoeff (l, NOT (Ge (mm, mn))) = NOT (Ge (mm, mn)) - | adjustcoeff (l, NOT (Eq (Cst oa, mp))) = NOT (Eq (Cst oa, mp)) - | adjustcoeff (l, NOT (Eq (Var ob, mp))) = NOT (Eq (Var ob, mp)) - | adjustcoeff (l, NOT (Eq (Neg oc, mp))) = NOT (Eq (Neg oc, mp)) - | adjustcoeff (l, NOT (Eq (Add (Cst os, oe), mp))) = - NOT (Eq (Add (Cst os, oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Var ot, oe), mp))) = - NOT (Eq (Add (Var ot, oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Neg ou, oe), mp))) = - NOT (Eq (Add (Neg ou, oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Add (ov, ow), oe), mp))) = - NOT (Eq (Add (Add (ov, ow), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Sub (ox, oy), oe), mp))) = - NOT (Eq (Add (Sub (ox, oy), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Cst qc), oe), mp))) = - NOT (Eq (Add (Mult (Cst pk, Cst qc), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Var qx))) = - NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Var qx)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Neg qy))) = - NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Neg qy)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Add (qz, ra)))) = - NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Add (qz, ra))) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Sub (rb, rc)))) = - NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Sub (rb, rc))) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Mult (rd, re)))) = - NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Mult (rd, re))) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var qu), oe), mp))) = - NOT (Eq (Add (Mult (Cst pk, Var qu), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Neg qe), oe), mp))) = - NOT (Eq (Add (Mult (Cst pk, Neg qe), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Add (qf, qg)), oe), mp))) = - NOT (Eq (Add (Mult (Cst pk, Add (qf, qg)), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Sub (qh, qi)), oe), mp))) = - NOT (Eq (Add (Mult (Cst pk, Sub (qh, qi)), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Mult (qj, qk)), oe), mp))) = - NOT (Eq (Add (Mult (Cst pk, Mult (qj, qk)), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Var pl, pa), oe), mp))) = - NOT (Eq (Add (Mult (Var pl, pa), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Neg pm, pa), oe), mp))) = - NOT (Eq (Add (Mult (Neg pm, pa), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Add (pn, po), pa), oe), mp))) = - NOT (Eq (Add (Mult (Add (pn, po), pa), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Sub (pp, pq), pa), oe), mp))) = - NOT (Eq (Add (Mult (Sub (pp, pq), pa), oe), mp)) - | adjustcoeff (l, NOT (Eq (Add (Mult (Mult (pr, ps), pa), oe), mp))) = - NOT (Eq (Add (Mult (Mult (pr, ps), pa), oe), mp)) - | adjustcoeff (l, NOT (Eq (Sub (of', og), mp))) = NOT (Eq (Sub (of', og), mp)) - | adjustcoeff (l, NOT (Eq (Mult (oh, oi), mp))) = NOT (Eq (Mult (oh, oi), mp)) - | adjustcoeff (l, NOT (Divides (Cst ro, Cst sg))) = - NOT (Divides (Cst ro, Cst sg)) - | adjustcoeff (l, NOT (Divides (Cst ro, Var sh))) = - NOT (Divides (Cst ro, Var sh)) - | adjustcoeff (l, NOT (Divides (Cst ro, Neg si))) = - NOT (Divides (Cst ro, Neg si)) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Cst sy, sk)))) = - NOT (Divides (Cst ro, Add (Cst sy, sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Var sz, sk)))) = - NOT (Divides (Cst ro, Add (Var sz, sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Neg ta, sk)))) = - NOT (Divides (Cst ro, Add (Neg ta, sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Add (tb, tc), sk)))) = - NOT (Divides (Cst ro, Add (Add (tb, tc), sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Sub (td, te), sk)))) = - NOT (Divides (Cst ro, Add (Sub (td, te), sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Cst ui), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Cst tq, Cst ui), sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Var va), sk)))) = - (if (va = 0) - then NOT (Divides - (Cst (op_div_def1 l tq * ro), - Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l tq, sk)))) - else NOT (Divides - (Cst ro, - Add (Mult (Cst tq, Var (op_45_def0 va id_1_def0 + 1)), - sk)))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Neg uk), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Cst tq, Neg uk), sk))) - | adjustcoeff - (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Add (ul, um)), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Cst tq, Add (ul, um)), sk))) - | adjustcoeff - (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Sub (un, uo)), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Cst tq, Sub (un, uo)), sk))) - | adjustcoeff - (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Mult (up, uq)), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Cst tq, Mult (up, uq)), sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Var tr, tg), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Var tr, tg), sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Neg ts, tg), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Neg ts, tg), sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Add (tt, tu), tg), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Add (tt, tu), tg), sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Sub (tv, tw), tg), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Sub (tv, tw), tg), sk))) - | adjustcoeff - (l, NOT (Divides (Cst ro, Add (Mult (Mult (tx, ty), tg), sk)))) = - NOT (Divides (Cst ro, Add (Mult (Mult (tx, ty), tg), sk))) - | adjustcoeff (l, NOT (Divides (Cst ro, Sub (sl, sm)))) = - NOT (Divides (Cst ro, Sub (sl, sm))) - | adjustcoeff (l, NOT (Divides (Cst ro, Mult (sn, so)))) = - NOT (Divides (Cst ro, Mult (sn, so))) - | adjustcoeff (l, NOT (Divides (Var rp, mr))) = NOT (Divides (Var rp, mr)) - | adjustcoeff (l, NOT (Divides (Neg rq, mr))) = NOT (Divides (Neg rq, mr)) - | adjustcoeff (l, NOT (Divides (Add (rr, rs), mr))) = - NOT (Divides (Add (rr, rs), mr)) - | adjustcoeff (l, NOT (Divides (Sub (rt, ru), mr))) = - NOT (Divides (Sub (rt, ru), mr)) - | adjustcoeff (l, NOT (Divides (Mult (rv, rw), mr))) = - NOT (Divides (Mult (rv, rw), mr)) - | adjustcoeff (l, NOT T) = NOT T - | adjustcoeff (l, NOT F) = NOT F - | adjustcoeff (l, NOT (NOT ms)) = NOT (NOT ms) - | adjustcoeff (l, NOT (And (mt, mu))) = NOT (And (mt, mu)) - | adjustcoeff (l, NOT (Or (mv, mw))) = NOT (Or (mv, mw)) - | adjustcoeff (l, NOT (Imp (mx, my))) = NOT (Imp (mx, my)) - | adjustcoeff (l, NOT (Equ (mz, na))) = NOT (Equ (mz, na)) - | adjustcoeff (l, NOT (QAll nb)) = NOT (QAll nb) - | adjustcoeff (l, NOT (QEx nc)) = NOT (QEx nc) - | adjustcoeff (l, Imp (an, ao)) = Imp (an, ao) - | adjustcoeff (l, Equ (ap, aq)) = Equ (ap, aq) - | adjustcoeff (l, QAll ar) = QAll ar - | adjustcoeff (l, QEx as') = QEx as'; - -fun formlcm (Le (Add (Mult (Cst c, Var 0), r), Cst i)) = abs c - | formlcm (Eq (Add (Mult (Cst c, Var 0), r), Cst i)) = abs c - | formlcm (NOT p) = formlcm p - | formlcm (And (p, q)) = ilcm (formlcm p) (formlcm q) - | formlcm (Or (p, q)) = ilcm (formlcm p) (formlcm q) - | formlcm (Lt (u, v)) = 1 - | formlcm (Gt (w, x)) = 1 - | formlcm (Le (Cst bo, z)) = 1 - | formlcm (Le (Var bp, z)) = 1 - | formlcm (Le (Neg bq, z)) = 1 - | formlcm (Le (Add (Cst cg, bs), z)) = 1 - | formlcm (Le (Add (Var ch, bs), z)) = 1 - | formlcm (Le (Add (Neg ci, bs), z)) = 1 - | formlcm (Le (Add (Add (cj, ck), bs), z)) = 1 - | formlcm (Le (Add (Sub (cl, cm), bs), z)) = 1 - | formlcm (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = 1 - | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Var el)) = 1 - | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Neg em)) = 1 - | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Add (en, eo))) = 1 - | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Sub (ep, eq))) = 1 - | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Mult (er, es))) = 1 - | formlcm (Le (Add (Mult (Cst cy, Var ei ), bs), z)) = 1 - | formlcm (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = 1 - | formlcm (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = 1 - | formlcm (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = 1 - | formlcm (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = 1 - | formlcm (Le (Add (Mult (Var cz, co), bs), z)) = 1 - | formlcm (Le (Add (Mult (Neg da, co), bs), z)) = 1 - | formlcm (Le (Add (Mult (Add (db, dc), co), bs), z)) = 1 - | formlcm (Le (Add (Mult (Sub (dd, de), co), bs), z)) = 1 - | formlcm (Le (Add (Mult (Mult (df, dg), co), bs), z)) = 1 - | formlcm (Le (Sub (bt, bu), z)) = 1 - | formlcm (Le (Mult (bv, bw), z)) = 1 - | formlcm (Ge (aa, ab)) = 1 - | formlcm (Eq (Cst fc, ad)) = 1 - | formlcm (Eq (Var fd, ad)) = 1 - | formlcm (Eq (Neg fe, ad)) = 1 - | formlcm (Eq (Add (Cst fu, fg), ad)) = 1 - | formlcm (Eq (Add (Var fv, fg), ad)) = 1 - | formlcm (Eq (Add (Neg fw, fg), ad)) = 1 - | formlcm (Eq (Add (Add (fx, fy), fg), ad)) = 1 - | formlcm (Eq (Add (Sub (fz, ga), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Cst he), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Var hz)) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Neg ia)) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Add (ib, ic))) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Sub (id, ie))) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Mult (if', ig))) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Var hw), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Neg hg), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Add (hh, hi)), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Sub (hj, hk)), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Cst gm, Mult (hl, hm)), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Var gn, gc), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Neg go, gc), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Add (gp, gq), gc), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Sub (gr, gs), gc), fg), ad)) = 1 - | formlcm (Eq (Add (Mult (Mult (gt, gu), gc), fg), ad)) = 1 - | formlcm (Eq (Sub (fh, fi), ad)) = 1 - | formlcm (Eq (Mult (fj, fk), ad)) = 1 - | formlcm (Divides (Cst iq, Cst ji)) = 1 - | formlcm (Divides (Cst iq, Var jj)) = 1 - | formlcm (Divides (Cst iq, Neg jk)) = 1 - | formlcm (Divides (Cst iq, Add (Cst ka, jm))) = 1 - | formlcm (Divides (Cst iq, Add (Var kb, jm))) = 1 - | formlcm (Divides (Cst iq, Add (Neg kc, jm))) = 1 - | formlcm (Divides (Cst iq, Add (Add (kd, ke), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Sub (kf, kg), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Cst lk), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Var mc), jm))) = - (if (mc = 0) then abs ks else 1) - | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Neg lm), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Add (ln, lo)), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Sub (lp, lq)), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Mult (lr, ls)), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Var kt, ki), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Neg ku, ki), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Add (kv, kw), ki), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Sub (kx, ky), ki), jm))) = 1 - | formlcm (Divides (Cst iq, Add (Mult (Mult (kz, la), ki), jm))) = 1 - | formlcm (Divides (Cst iq, Sub (jn, jo))) = 1 - | formlcm (Divides (Cst iq, Mult (jp, jq))) = 1 - | formlcm (Divides (Var ir, af)) = 1 - | formlcm (Divides (Neg is, af)) = 1 - | formlcm (Divides (Add (it, iu), af)) = 1 - | formlcm (Divides (Sub (iv, iw), af)) = 1 - | formlcm (Divides (Mult (ix, iy), af)) = 1 - | formlcm T = 1 - | formlcm F = 1 - | formlcm (Imp (al, am)) = 1 - | formlcm (Equ (an, ao)) = 1 - | formlcm (QAll ap) = 1 - | formlcm (QEx aq) = 1; - -fun unitycoeff p = - let val l = formlcm p; val p' = adjustcoeff (l, p) - in (if (l = 1) then p' - else And (Divides (Cst l, Add (Mult (Cst 1, Var 0), Cst 0)), p')) - end; - -fun unify p = - let val q = unitycoeff p; val B = list_set (bset q); val A = list_set (aset q) - in (if op_60_61_def0 (size_def1 B) (size_def1 A) then (q, B) - else (mirror q, map lin_neg A)) - end; - -fun cooper p = - lift_un (fn q => decrvars (explode_minf (unify q))) (linform (nnf p)); - -fun pa p = lift_un psimpl (qelim (cooper, p)); - -val test = pa; - -end;