# HG changeset patch # User wenzelm # Date 1634330947 -7200 # Node ID b4660c388e724b13e16ce0f4115fdb10c94d4262 # Parent 823ccd84b8795c785912b8797084fad6fbba3034 isabelle regenerate_cooper; diff -r 823ccd84b879 -r b4660c388e72 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri Oct 15 22:00:28 2021 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Oct 15 22:49:07 2021 +0200 @@ -640,7 +640,7 @@ | fm_of_term ps vs (\<^term>\(=) :: bool => _ \ $ t1 $ t2) = Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (Const (\<^const_name>\Not\, _) $ t') = - Proc.NOT (fm_of_term ps vs t') + Proc.Not (fm_of_term ps vs t') | fm_of_term ps vs (Const (\<^const_name>\Ex\, _) $ Abs abs) = Proc.E (uncurry (fm_of_term ps) (descend vs abs)) | fm_of_term ps vs (Const (\<^const_name>\All\, _) $ Abs abs) = @@ -677,18 +677,18 @@ | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (Proc.Iff (t1, t2)) = \<^term>\(=) :: bool => _\ $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 - | term_of_fm ps vs (Proc.NOT t') = HOLogic.Not $ term_of_fm ps vs t' + | term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t' | term_of_fm ps vs (Proc.Eq t') = \<^term>\(=) :: int => _ \ $ term_of_num vs t'$ \<^term>\0::int\ - | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.NOT (Proc.Eq t')) + | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t')) | term_of_fm ps vs (Proc.Lt t') = \<^term>\(<) :: int => _ \ $ term_of_num vs t' $ \<^term>\0::int\ | term_of_fm ps vs (Proc.Le t') = \<^term>\(<=) :: int => _ \ $ term_of_num vs t' $ \<^term>\0::int\ | term_of_fm ps vs (Proc.Gt t') = \<^term>\(<) :: int => _ \ $ \<^term>\0::int\ $ term_of_num vs t' | term_of_fm ps vs (Proc.Ge t') = \<^term>\(<=) :: int => _ \ $ \<^term>\0::int\ $ term_of_num vs t' | term_of_fm ps vs (Proc.Dvd (i, t')) = \<^term>\(dvd) :: int => _ \ $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t' - | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.NOT (Proc.Dvd (i, t'))) + | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t'))) | term_of_fm ps vs (Proc.Closed n) = nth ps (Proc.integer_of_nat n) - | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.NOT (Proc.Closed n)); + | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n)); fun procedure t = let diff -r 823ccd84b879 -r b4660c388e72 src/HOL/Tools/Qelim/cooper_procedure.ML --- a/src/HOL/Tools/Qelim/cooper_procedure.ML Fri Oct 15 22:00:28 2021 +0200 +++ b/src/HOL/Tools/Qelim/cooper_procedure.ML Fri Oct 15 22:49:07 2021 +0200 @@ -7,7 +7,7 @@ Neg of numa | Add of numa * numa | Sub of numa * numa | Mul of inta * numa datatype fm = T | F | Lt of numa | Le of numa | Gt of numa | Ge of numa | Eq of numa | NEq of numa | Dvd of inta * numa | NDvd of inta * numa | - NOT of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm + Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm | E of fm | A of fm | Closed of nat | NClosed of nat val pa : fm -> fm val nat_of_integer : int -> nat @@ -619,7 +619,7 @@ datatype fm = T | F | Lt of numa | Le of numa | Gt of numa | Ge of numa | Eq of numa | NEq of numa | Dvd of inta * numa | NDvd of inta * numa | - NOT of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm | + Not of fm | And of fm * fm | Or of fm * fm | Imp of fm * fm | Iff of fm * fm | E of fm | A of fm | Closed of nat | NClosed of nat; fun id x = (fn xa => xa) x; @@ -643,7 +643,7 @@ | disjuncts (NEq v) = [NEq v] | disjuncts (Dvd (v, va)) = [Dvd (v, va)] | disjuncts (NDvd (v, va)) = [NDvd (v, va)] - | disjuncts (NOT v) = [NOT v] + | disjuncts (Not v) = [Not v] | disjuncts (And (v, va)) = [And (v, va)] | disjuncts (Imp (v, va)) = [Imp (v, va)] | disjuncts (Iff (v, va)) = [Iff (v, va)] @@ -711,22 +711,22 @@ | equal_fm (Imp (x141, x142)) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (Or (x131, x132)) = false | equal_fm (Or (x131, x132)) (And (x121, x122)) = false - | equal_fm (NOT x11) (NClosed x19) = false - | equal_fm (NClosed x19) (NOT x11) = false - | equal_fm (NOT x11) (Closed x18) = false - | equal_fm (Closed x18) (NOT x11) = false - | equal_fm (NOT x11) (A x17) = false - | equal_fm (A x17) (NOT x11) = false - | equal_fm (NOT x11) (E x16) = false - | equal_fm (E x16) (NOT x11) = false - | equal_fm (NOT x11) (Iff (x151, x152)) = false - | equal_fm (Iff (x151, x152)) (NOT x11) = false - | equal_fm (NOT x11) (Imp (x141, x142)) = false - | equal_fm (Imp (x141, x142)) (NOT x11) = false - | equal_fm (NOT x11) (Or (x131, x132)) = false - | equal_fm (Or (x131, x132)) (NOT x11) = false - | equal_fm (NOT x11) (And (x121, x122)) = false - | equal_fm (And (x121, x122)) (NOT x11) = false + | equal_fm (Not x11) (NClosed x19) = false + | equal_fm (NClosed x19) (Not x11) = false + | equal_fm (Not x11) (Closed x18) = false + | equal_fm (Closed x18) (Not x11) = false + | equal_fm (Not x11) (A x17) = false + | equal_fm (A x17) (Not x11) = false + | equal_fm (Not x11) (E x16) = false + | equal_fm (E x16) (Not x11) = false + | equal_fm (Not x11) (Iff (x151, x152)) = false + | equal_fm (Iff (x151, x152)) (Not x11) = false + | equal_fm (Not x11) (Imp (x141, x142)) = false + | equal_fm (Imp (x141, x142)) (Not x11) = false + | equal_fm (Not x11) (Or (x131, x132)) = false + | equal_fm (Or (x131, x132)) (Not x11) = false + | equal_fm (Not x11) (And (x121, x122)) = false + | equal_fm (And (x121, x122)) (Not x11) = false | equal_fm (NDvd (x101, x102)) (NClosed x19) = false | equal_fm (NClosed x19) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (Closed x18) = false @@ -743,8 +743,8 @@ | equal_fm (Or (x131, x132)) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (NDvd (x101, x102)) = false - | equal_fm (NDvd (x101, x102)) (NOT x11) = false - | equal_fm (NOT x11) (NDvd (x101, x102)) = false + | equal_fm (NDvd (x101, x102)) (Not x11) = false + | equal_fm (Not x11) (NDvd (x101, x102)) = false | equal_fm (Dvd (x91, x92)) (NClosed x19) = false | equal_fm (NClosed x19) (Dvd (x91, x92)) = false | equal_fm (Dvd (x91, x92)) (Closed x18) = false @@ -761,8 +761,8 @@ | equal_fm (Or (x131, x132)) (Dvd (x91, x92)) = false | equal_fm (Dvd (x91, x92)) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (Dvd (x91, x92)) = false - | equal_fm (Dvd (x91, x92)) (NOT x11) = false - | equal_fm (NOT x11) (Dvd (x91, x92)) = false + | equal_fm (Dvd (x91, x92)) (Not x11) = false + | equal_fm (Not x11) (Dvd (x91, x92)) = false | equal_fm (Dvd (x91, x92)) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (Dvd (x91, x92)) = false | equal_fm (NEq x8) (NClosed x19) = false @@ -781,8 +781,8 @@ | equal_fm (Or (x131, x132)) (NEq x8) = false | equal_fm (NEq x8) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (NEq x8) = false - | equal_fm (NEq x8) (NOT x11) = false - | equal_fm (NOT x11) (NEq x8) = false + | equal_fm (NEq x8) (Not x11) = false + | equal_fm (Not x11) (NEq x8) = false | equal_fm (NEq x8) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (NEq x8) = false | equal_fm (NEq x8) (Dvd (x91, x92)) = false @@ -803,8 +803,8 @@ | equal_fm (Or (x131, x132)) (Eq x7) = false | equal_fm (Eq x7) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (Eq x7) = false - | equal_fm (Eq x7) (NOT x11) = false - | equal_fm (NOT x11) (Eq x7) = false + | equal_fm (Eq x7) (Not x11) = false + | equal_fm (Not x11) (Eq x7) = false | equal_fm (Eq x7) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (Eq x7) = false | equal_fm (Eq x7) (Dvd (x91, x92)) = false @@ -827,8 +827,8 @@ | equal_fm (Or (x131, x132)) (Ge x6) = false | equal_fm (Ge x6) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (Ge x6) = false - | equal_fm (Ge x6) (NOT x11) = false - | equal_fm (NOT x11) (Ge x6) = false + | equal_fm (Ge x6) (Not x11) = false + | equal_fm (Not x11) (Ge x6) = false | equal_fm (Ge x6) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (Ge x6) = false | equal_fm (Ge x6) (Dvd (x91, x92)) = false @@ -853,8 +853,8 @@ | equal_fm (Or (x131, x132)) (Gt x5) = false | equal_fm (Gt x5) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (Gt x5) = false - | equal_fm (Gt x5) (NOT x11) = false - | equal_fm (NOT x11) (Gt x5) = false + | equal_fm (Gt x5) (Not x11) = false + | equal_fm (Not x11) (Gt x5) = false | equal_fm (Gt x5) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (Gt x5) = false | equal_fm (Gt x5) (Dvd (x91, x92)) = false @@ -881,8 +881,8 @@ | equal_fm (Or (x131, x132)) (Le x4) = false | equal_fm (Le x4) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (Le x4) = false - | equal_fm (Le x4) (NOT x11) = false - | equal_fm (NOT x11) (Le x4) = false + | equal_fm (Le x4) (Not x11) = false + | equal_fm (Not x11) (Le x4) = false | equal_fm (Le x4) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (Le x4) = false | equal_fm (Le x4) (Dvd (x91, x92)) = false @@ -911,8 +911,8 @@ | equal_fm (Or (x131, x132)) (Lt x3) = false | equal_fm (Lt x3) (And (x121, x122)) = false | equal_fm (And (x121, x122)) (Lt x3) = false - | equal_fm (Lt x3) (NOT x11) = false - | equal_fm (NOT x11) (Lt x3) = false + | equal_fm (Lt x3) (Not x11) = false + | equal_fm (Not x11) (Lt x3) = false | equal_fm (Lt x3) (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) (Lt x3) = false | equal_fm (Lt x3) (Dvd (x91, x92)) = false @@ -943,8 +943,8 @@ | equal_fm (Or (x131, x132)) F = false | equal_fm F (And (x121, x122)) = false | equal_fm (And (x121, x122)) F = false - | equal_fm F (NOT x11) = false - | equal_fm (NOT x11) F = false + | equal_fm F (Not x11) = false + | equal_fm (Not x11) F = false | equal_fm F (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) F = false | equal_fm F (Dvd (x91, x92)) = false @@ -977,8 +977,8 @@ | equal_fm (Or (x131, x132)) T = false | equal_fm T (And (x121, x122)) = false | equal_fm (And (x121, x122)) T = false - | equal_fm T (NOT x11) = false - | equal_fm (NOT x11) T = false + | equal_fm T (Not x11) = false + | equal_fm (Not x11) T = false | equal_fm T (NDvd (x101, x102)) = false | equal_fm (NDvd (x101, x102)) T = false | equal_fm T (Dvd (x91, x92)) = false @@ -1009,7 +1009,7 @@ equal_fm x131 y131 andalso equal_fm x132 y132 | equal_fm (And (x121, x122)) (And (y121, y122)) = equal_fm x121 y121 andalso equal_fm x122 y122 - | equal_fm (NOT x11) (NOT y11) = equal_fm x11 y11 + | equal_fm (Not x11) (Not y11) = equal_fm x11 y11 | equal_fm (NDvd (x101, x102)) (NDvd (y101, y102)) = equal_inta x101 y101 andalso equal_numa x102 y102 | equal_fm (Dvd (x91, x92)) (Dvd (y91, y92)) = @@ -1030,7 +1030,7 @@ | Le _ => Or (f p, q) | Gt _ => Or (f p, q) | Ge _ => Or (f p, q) | Eq _ => Or (f p, q) | NEq _ => Or (f p, q) | Dvd (_, _) => Or (f p, q) - | NDvd (_, _) => Or (f p, q) | NOT _ => Or (f p, q) + | NDvd (_, _) => Or (f p, q) | Not _ => Or (f p, q) | And (_, _) => Or (f p, q) | Or (_, _) => Or (f p, q) | Imp (_, _) => Or (f p, q) | Iff (_, _) => Or (f p, q) | E _ => Or (f p, q) | A _ => Or (f p, q) @@ -1089,7 +1089,7 @@ | minusinf (NEq (Mul (va, vb))) = NEq (Mul (va, vb)) | minusinf (Dvd (v, va)) = Dvd (v, va) | minusinf (NDvd (v, va)) = NDvd (v, va) - | minusinf (NOT v) = NOT v + | minusinf (Not v) = Not v | minusinf (Imp (v, va)) = Imp (v, va) | minusinf (Iff (v, va)) = Iff (v, va) | minusinf (E v) = E v @@ -1138,7 +1138,7 @@ | subst0 t (NEq a) = NEq (numsubst0 t a) | subst0 t (Dvd (i, a)) = Dvd (i, numsubst0 t a) | subst0 t (NDvd (i, a)) = NDvd (i, numsubst0 t a) - | subst0 t (NOT p) = NOT (subst0 t p) + | subst0 t (Not p) = Not (subst0 t p) | subst0 t (And (p, q)) = And (subst0 t p, subst0 t q) | subst0 t (Or (p, q)) = Or (subst0 t p, subst0 t q) | subst0 t (Imp (p, q)) = Imp (subst0 t p, subst0 t q) @@ -1263,25 +1263,25 @@ else (if equal_fm p T then q else (if equal_fm q T then p else And (p, q)))); -fun nota (NOT p) = p +fun nota (Not p) = p | nota T = F | nota F = T - | nota (Lt v) = NOT (Lt v) - | nota (Le v) = NOT (Le v) - | nota (Gt v) = NOT (Gt v) - | nota (Ge v) = NOT (Ge v) - | nota (Eq v) = NOT (Eq v) - | nota (NEq v) = NOT (NEq v) - | nota (Dvd (v, va)) = NOT (Dvd (v, va)) - | nota (NDvd (v, va)) = NOT (NDvd (v, va)) - | nota (And (v, va)) = NOT (And (v, va)) - | nota (Or (v, va)) = NOT (Or (v, va)) - | nota (Imp (v, va)) = NOT (Imp (v, va)) - | nota (Iff (v, va)) = NOT (Iff (v, va)) - | nota (E v) = NOT (E v) - | nota (A v) = NOT (A v) - | nota (Closed v) = NOT (Closed v) - | nota (NClosed v) = NOT (NClosed v); + | nota (Lt v) = Not (Lt v) + | nota (Le v) = Not (Le v) + | nota (Gt v) = Not (Gt v) + | nota (Ge v) = Not (Ge v) + | nota (Eq v) = Not (Eq v) + | nota (NEq v) = Not (NEq v) + | nota (Dvd (v, va)) = Not (Dvd (v, va)) + | nota (NDvd (v, va)) = Not (NDvd (v, va)) + | nota (And (v, va)) = Not (And (v, va)) + | nota (Or (v, va)) = Not (Or (v, va)) + | nota (Imp (v, va)) = Not (Imp (v, va)) + | nota (Iff (v, va)) = Not (Iff (v, va)) + | nota (E v) = Not (E v) + | nota (A v) = Not (A v) + | nota (Closed v) = Not (Closed v) + | nota (NClosed v) = Not (NClosed v); fun imp p q = (if equal_fm p F orelse equal_fm q T then T @@ -1301,7 +1301,7 @@ | simpfm (Or (p, q)) = disj (simpfm p) (simpfm q) | simpfm (Imp (p, q)) = imp (simpfm p) (simpfm q) | simpfm (Iff (p, q)) = iff (simpfm p) (simpfm q) - | simpfm (NOT p) = nota (simpfm p) + | simpfm (Not p) = nota (simpfm p) | simpfm (Lt a) = let val aa = simpnum a; @@ -1442,7 +1442,7 @@ | a_beta (NDvd (v, Add (vb, vc))) k = NDvd (v, Add (vb, vc)) | a_beta (NDvd (v, Sub (vb, vc))) k = NDvd (v, Sub (vb, vc)) | a_beta (NDvd (v, Mul (vb, vc))) k = NDvd (v, Mul (vb, vc)) - | a_beta (NOT v) k = NOT v + | a_beta (Not v) k = Not v | a_beta (Imp (v, va)) k = Imp (v, va) | a_beta (Iff (v, va)) k = Iff (v, va) | a_beta (E v) k = E v @@ -1515,7 +1515,7 @@ | delta (NDvd (v, Add (vb, vc))) = one_inta | delta (NDvd (v, Sub (vb, vc))) = one_inta | delta (NDvd (v, Mul (vb, vc))) = one_inta - | delta (NOT v) = one_inta + | delta (Not v) = one_inta | delta (Imp (v, va)) = one_inta | delta (Iff (v, va)) = one_inta | delta (E v) = one_inta @@ -1569,7 +1569,7 @@ | alpha (NEq (Mul (va, vb))) = [] | alpha (Dvd (v, va)) = [] | alpha (NDvd (v, va)) = [] - | alpha (NOT v) = [] + | alpha (Not v) = [] | alpha (Imp (v, va)) = [] | alpha (Iff (v, va)) = [] | alpha (E v) = [] @@ -1637,7 +1637,7 @@ | zeta (NDvd (v, Add (vb, vc))) = one_inta | zeta (NDvd (v, Sub (vb, vc))) = one_inta | zeta (NDvd (v, Mul (vb, vc))) = one_inta - | zeta (NOT v) = one_inta + | zeta (Not v) = one_inta | zeta (Imp (v, va)) = one_inta | zeta (Iff (v, va)) = one_inta | zeta (E v) = one_inta @@ -1697,7 +1697,7 @@ | beta (NEq (Mul (va, vb))) = [] | beta (Dvd (v, va)) = [] | beta (NDvd (v, va)) = [] - | beta (NOT v) = [] + | beta (Not v) = [] | beta (Imp (v, va)) = [] | beta (Iff (v, va)) = [] | beta (E v) = [] @@ -1766,7 +1766,7 @@ | mirror (NDvd (v, Add (vb, vc))) = NDvd (v, Add (vb, vc)) | mirror (NDvd (v, Sub (vb, vc))) = NDvd (v, Sub (vb, vc)) | mirror (NDvd (v, Mul (vb, vc))) = NDvd (v, Mul (vb, vc)) - | mirror (NOT v) = NOT v + | mirror (Not v) = Not v | mirror (Imp (v, va)) = Imp (v, va) | mirror (Iff (v, va)) = Iff (v, va) | mirror (E v) = E v @@ -1848,9 +1848,9 @@ fun zlfm (And (p, q)) = And (zlfm p, zlfm q) | zlfm (Or (p, q)) = Or (zlfm p, zlfm q) - | zlfm (Imp (p, q)) = Or (zlfm (NOT p), zlfm q) + | zlfm (Imp (p, q)) = Or (zlfm (Not p), zlfm q) | zlfm (Iff (p, q)) = - Or (And (zlfm p, zlfm q), And (zlfm (NOT p), zlfm (NOT q))) + Or (And (zlfm p, zlfm q), And (zlfm (Not p), zlfm (Not q))) | zlfm (Lt a) = let val (c, r) = zsplit0 a; @@ -1920,28 +1920,28 @@ else NDvd (abs_int i, CN (zero_nat, uminus_int c, Neg r)))) end) - | zlfm (NOT (And (p, q))) = Or (zlfm (NOT p), zlfm (NOT q)) - | zlfm (NOT (Or (p, q))) = And (zlfm (NOT p), zlfm (NOT q)) - | zlfm (NOT (Imp (p, q))) = And (zlfm p, zlfm (NOT q)) - | zlfm (NOT (Iff (p, q))) = - Or (And (zlfm p, zlfm (NOT q)), And (zlfm (NOT p), zlfm q)) - | zlfm (NOT (NOT p)) = zlfm p - | zlfm (NOT T) = F - | zlfm (NOT F) = T - | zlfm (NOT (Lt a)) = zlfm (Ge a) - | zlfm (NOT (Le a)) = zlfm (Gt a) - | zlfm (NOT (Gt a)) = zlfm (Le a) - | zlfm (NOT (Ge a)) = zlfm (Lt a) - | zlfm (NOT (Eq a)) = zlfm (NEq a) - | zlfm (NOT (NEq a)) = zlfm (Eq a) - | zlfm (NOT (Dvd (i, a))) = zlfm (NDvd (i, a)) - | zlfm (NOT (NDvd (i, a))) = zlfm (Dvd (i, a)) - | zlfm (NOT (Closed p)) = NClosed p - | zlfm (NOT (NClosed p)) = Closed p + | zlfm (Not (And (p, q))) = Or (zlfm (Not p), zlfm (Not q)) + | zlfm (Not (Or (p, q))) = And (zlfm (Not p), zlfm (Not q)) + | zlfm (Not (Imp (p, q))) = And (zlfm p, zlfm (Not q)) + | zlfm (Not (Iff (p, q))) = + Or (And (zlfm p, zlfm (Not q)), And (zlfm (Not p), zlfm q)) + | zlfm (Not (Not p)) = zlfm p + | zlfm (Not T) = F + | zlfm (Not F) = T + | zlfm (Not (Lt a)) = zlfm (Ge a) + | zlfm (Not (Le a)) = zlfm (Gt a) + | zlfm (Not (Gt a)) = zlfm (Le a) + | zlfm (Not (Ge a)) = zlfm (Lt a) + | zlfm (Not (Eq a)) = zlfm (NEq a) + | zlfm (Not (NEq a)) = zlfm (Eq a) + | zlfm (Not (Dvd (i, a))) = zlfm (NDvd (i, a)) + | zlfm (Not (NDvd (i, a))) = zlfm (Dvd (i, a)) + | zlfm (Not (Closed p)) = NClosed p + | zlfm (Not (NClosed p)) = Closed p | zlfm T = T | zlfm F = F - | zlfm (NOT (E va)) = NOT (E va) - | zlfm (NOT (A va)) = NOT (A va) + | zlfm (Not (E va)) = Not (E va) + | zlfm (Not (A va)) = Not (A va) | zlfm (E v) = E v | zlfm (A v) = A v | zlfm (Closed v) = Closed v @@ -1976,7 +1976,7 @@ | decr (NEq a) = NEq (decrnum a) | decr (Dvd (i, a)) = Dvd (i, decrnum a) | decr (NDvd (i, a)) = NDvd (i, decrnum a) - | decr (NOT p) = NOT (decr p) + | decr (Not p) = Not (decr p) | decr (And (p, q)) = And (decr p, decr q) | decr (Or (p, q)) = Or (decr p, decr q) | decr (Imp (p, q)) = Imp (decr p, decr q) @@ -2014,8 +2014,8 @@ end; fun qelim (E p) = (fn qe => dj qe (qelim p qe)) - | qelim (A p) = (fn qe => nota (qe (qelim (NOT p) qe))) - | qelim (NOT p) = (fn qe => nota (qelim p qe)) + | qelim (A p) = (fn qe => nota (qe (qelim (Not p) qe))) + | qelim (Not p) = (fn qe => nota (qelim p qe)) | qelim (And (p, q)) = (fn qe => conj (qelim p qe) (qelim q qe)) | qelim (Or (p, q)) = (fn qe => disj (qelim p qe) (qelim q qe)) | qelim (Imp (p, q)) = (fn qe => imp (qelim p qe) (qelim q qe)) @@ -2036,13 +2036,13 @@ fun prep (E T) = T | prep (E F) = F | prep (E (Or (p, q))) = Or (prep (E p), prep (E q)) - | prep (E (Imp (p, q))) = Or (prep (E (NOT p)), prep (E q)) + | prep (E (Imp (p, q))) = Or (prep (E (Not p)), prep (E q)) | prep (E (Iff (p, q))) = - Or (prep (E (And (p, q))), prep (E (And (NOT p, NOT q)))) - | prep (E (NOT (And (p, q)))) = Or (prep (E (NOT p)), prep (E (NOT q))) - | prep (E (NOT (Imp (p, q)))) = prep (E (And (p, NOT q))) - | prep (E (NOT (Iff (p, q)))) = - Or (prep (E (And (p, NOT q))), prep (E (And (NOT p, q)))) + Or (prep (E (And (p, q))), prep (E (And (Not p, Not q)))) + | prep (E (Not (And (p, q)))) = Or (prep (E (Not p)), prep (E (Not q))) + | prep (E (Not (Imp (p, q)))) = prep (E (And (p, Not q))) + | prep (E (Not (Iff (p, q)))) = + Or (prep (E (And (p, Not q))), prep (E (And (Not p, q)))) | prep (E (Lt v)) = E (prep (Lt v)) | prep (E (Le v)) = E (prep (Le v)) | prep (E (Gt v)) = E (prep (Gt v)) @@ -2051,69 +2051,69 @@ | prep (E (NEq v)) = E (prep (NEq v)) | prep (E (Dvd (v, va))) = E (prep (Dvd (v, va))) | prep (E (NDvd (v, va))) = E (prep (NDvd (v, va))) - | prep (E (NOT T)) = E (prep (NOT T)) - | prep (E (NOT F)) = E (prep (NOT F)) - | prep (E (NOT (Lt va))) = E (prep (NOT (Lt va))) - | prep (E (NOT (Le va))) = E (prep (NOT (Le va))) - | prep (E (NOT (Gt va))) = E (prep (NOT (Gt va))) - | prep (E (NOT (Ge va))) = E (prep (NOT (Ge va))) - | prep (E (NOT (Eq va))) = E (prep (NOT (Eq va))) - | prep (E (NOT (NEq va))) = E (prep (NOT (NEq va))) - | prep (E (NOT (Dvd (va, vb)))) = E (prep (NOT (Dvd (va, vb)))) - | prep (E (NOT (NDvd (va, vb)))) = E (prep (NOT (NDvd (va, vb)))) - | prep (E (NOT (NOT va))) = E (prep (NOT (NOT va))) - | prep (E (NOT (Or (va, vb)))) = E (prep (NOT (Or (va, vb)))) - | prep (E (NOT (E va))) = E (prep (NOT (E va))) - | prep (E (NOT (A va))) = E (prep (NOT (A va))) - | prep (E (NOT (Closed va))) = E (prep (NOT (Closed va))) - | prep (E (NOT (NClosed va))) = E (prep (NOT (NClosed va))) + | prep (E (Not T)) = E (prep (Not T)) + | prep (E (Not F)) = E (prep (Not F)) + | prep (E (Not (Lt va))) = E (prep (Not (Lt va))) + | prep (E (Not (Le va))) = E (prep (Not (Le va))) + | prep (E (Not (Gt va))) = E (prep (Not (Gt va))) + | prep (E (Not (Ge va))) = E (prep (Not (Ge va))) + | prep (E (Not (Eq va))) = E (prep (Not (Eq va))) + | prep (E (Not (NEq va))) = E (prep (Not (NEq va))) + | prep (E (Not (Dvd (va, vb)))) = E (prep (Not (Dvd (va, vb)))) + | prep (E (Not (NDvd (va, vb)))) = E (prep (Not (NDvd (va, vb)))) + | prep (E (Not (Not va))) = E (prep (Not (Not va))) + | prep (E (Not (Or (va, vb)))) = E (prep (Not (Or (va, vb)))) + | prep (E (Not (E va))) = E (prep (Not (E va))) + | prep (E (Not (A va))) = E (prep (Not (A va))) + | prep (E (Not (Closed va))) = E (prep (Not (Closed va))) + | prep (E (Not (NClosed va))) = E (prep (Not (NClosed va))) | prep (E (And (v, va))) = E (prep (And (v, va))) | prep (E (E v)) = E (prep (E v)) | prep (E (A v)) = E (prep (A v)) | prep (E (Closed v)) = E (prep (Closed v)) | prep (E (NClosed v)) = E (prep (NClosed v)) | prep (A (And (p, q))) = And (prep (A p), prep (A q)) - | prep (A T) = prep (NOT (E (NOT T))) - | prep (A F) = prep (NOT (E (NOT F))) - | prep (A (Lt v)) = prep (NOT (E (NOT (Lt v)))) - | prep (A (Le v)) = prep (NOT (E (NOT (Le v)))) - | prep (A (Gt v)) = prep (NOT (E (NOT (Gt v)))) - | prep (A (Ge v)) = prep (NOT (E (NOT (Ge v)))) - | prep (A (Eq v)) = prep (NOT (E (NOT (Eq v)))) - | prep (A (NEq v)) = prep (NOT (E (NOT (NEq v)))) - | prep (A (Dvd (v, va))) = prep (NOT (E (NOT (Dvd (v, va))))) - | prep (A (NDvd (v, va))) = prep (NOT (E (NOT (NDvd (v, va))))) - | prep (A (NOT v)) = prep (NOT (E (NOT (NOT v)))) - | prep (A (Or (v, va))) = prep (NOT (E (NOT (Or (v, va))))) - | prep (A (Imp (v, va))) = prep (NOT (E (NOT (Imp (v, va))))) - | prep (A (Iff (v, va))) = prep (NOT (E (NOT (Iff (v, va))))) - | prep (A (E v)) = prep (NOT (E (NOT (E v)))) - | prep (A (A v)) = prep (NOT (E (NOT (A v)))) - | prep (A (Closed v)) = prep (NOT (E (NOT (Closed v)))) - | prep (A (NClosed v)) = prep (NOT (E (NOT (NClosed v)))) - | prep (NOT (NOT p)) = prep p - | prep (NOT (And (p, q))) = Or (prep (NOT p), prep (NOT q)) - | prep (NOT (A p)) = prep (E (NOT p)) - | prep (NOT (Or (p, q))) = And (prep (NOT p), prep (NOT q)) - | prep (NOT (Imp (p, q))) = And (prep p, prep (NOT q)) - | prep (NOT (Iff (p, q))) = Or (prep (And (p, NOT q)), prep (And (NOT p, q))) - | prep (NOT T) = NOT (prep T) - | prep (NOT F) = NOT (prep F) - | prep (NOT (Lt v)) = NOT (prep (Lt v)) - | prep (NOT (Le v)) = NOT (prep (Le v)) - | prep (NOT (Gt v)) = NOT (prep (Gt v)) - | prep (NOT (Ge v)) = NOT (prep (Ge v)) - | prep (NOT (Eq v)) = NOT (prep (Eq v)) - | prep (NOT (NEq v)) = NOT (prep (NEq v)) - | prep (NOT (Dvd (v, va))) = NOT (prep (Dvd (v, va))) - | prep (NOT (NDvd (v, va))) = NOT (prep (NDvd (v, va))) - | prep (NOT (E v)) = NOT (prep (E v)) - | prep (NOT (Closed v)) = NOT (prep (Closed v)) - | prep (NOT (NClosed v)) = NOT (prep (NClosed v)) + | prep (A T) = prep (Not (E (Not T))) + | prep (A F) = prep (Not (E (Not F))) + | prep (A (Lt v)) = prep (Not (E (Not (Lt v)))) + | prep (A (Le v)) = prep (Not (E (Not (Le v)))) + | prep (A (Gt v)) = prep (Not (E (Not (Gt v)))) + | prep (A (Ge v)) = prep (Not (E (Not (Ge v)))) + | prep (A (Eq v)) = prep (Not (E (Not (Eq v)))) + | prep (A (NEq v)) = prep (Not (E (Not (NEq v)))) + | prep (A (Dvd (v, va))) = prep (Not (E (Not (Dvd (v, va))))) + | prep (A (NDvd (v, va))) = prep (Not (E (Not (NDvd (v, va))))) + | prep (A (Not v)) = prep (Not (E (Not (Not v)))) + | prep (A (Or (v, va))) = prep (Not (E (Not (Or (v, va))))) + | prep (A (Imp (v, va))) = prep (Not (E (Not (Imp (v, va))))) + | prep (A (Iff (v, va))) = prep (Not (E (Not (Iff (v, va))))) + | prep (A (E v)) = prep (Not (E (Not (E v)))) + | prep (A (A v)) = prep (Not (E (Not (A v)))) + | prep (A (Closed v)) = prep (Not (E (Not (Closed v)))) + | prep (A (NClosed v)) = prep (Not (E (Not (NClosed v)))) + | prep (Not (Not p)) = prep p + | prep (Not (And (p, q))) = Or (prep (Not p), prep (Not q)) + | prep (Not (A p)) = prep (E (Not p)) + | prep (Not (Or (p, q))) = And (prep (Not p), prep (Not q)) + | prep (Not (Imp (p, q))) = And (prep p, prep (Not q)) + | prep (Not (Iff (p, q))) = Or (prep (And (p, Not q)), prep (And (Not p, q))) + | prep (Not T) = Not (prep T) + | prep (Not F) = Not (prep F) + | prep (Not (Lt v)) = Not (prep (Lt v)) + | prep (Not (Le v)) = Not (prep (Le v)) + | prep (Not (Gt v)) = Not (prep (Gt v)) + | prep (Not (Ge v)) = Not (prep (Ge v)) + | prep (Not (Eq v)) = Not (prep (Eq v)) + | prep (Not (NEq v)) = Not (prep (NEq v)) + | prep (Not (Dvd (v, va))) = Not (prep (Dvd (v, va))) + | prep (Not (NDvd (v, va))) = Not (prep (NDvd (v, va))) + | prep (Not (E v)) = Not (prep (E v)) + | prep (Not (Closed v)) = Not (prep (Closed v)) + | prep (Not (NClosed v)) = Not (prep (NClosed v)) | prep (Or (p, q)) = Or (prep p, prep q) | prep (And (p, q)) = And (prep p, prep q) - | prep (Imp (p, q)) = prep (Or (NOT p, q)) - | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (NOT p, NOT q))) + | prep (Imp (p, q)) = prep (Or (Not p, q)) + | prep (Iff (p, q)) = Or (prep (And (p, q)), prep (And (Not p, Not q))) | prep T = T | prep F = F | prep (Lt v) = Lt v