# HG changeset patch # User haftmann # Date 1486850011 -3600 # Node ID 3cb8013913538527ca44e44376b2d9f4c6a7f5c0 # Parent e383fad30b2582c23236b8e778512fec92ecaa8d more fun without recdef diff -r e383fad30b25 -r 3cb801391353 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Fri Feb 10 11:39:23 2017 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Sat Feb 11 22:53:31 2017 +0100 @@ -82,32 +82,35 @@ | "Ifm bbs bs (Closed n) \ bbs!n" | "Ifm bbs bs (NClosed n) \ \ bbs!n" -consts prep :: "fm \ fm" -recdef prep "measure fmsize" +function (sequential) prep :: "fm \ fm" +where "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 (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)))" - "prep (E p) = E (prep p)" - "prep (A (And p q)) = And (prep (A p)) (prep (A q))" - "prep (A p) = prep (NOT (E (NOT p)))" - "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 p) = NOT (prep p)" - "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 p = p" - (hints simp add: fmsize_pos) +| "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 (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)))" +| "prep (E p) = E (prep p)" +| "prep (A (And p q)) = And (prep (A p)) (prep (A q))" +| "prep (A p) = prep (NOT (E (NOT p)))" +| "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 p) = NOT (prep p)" +| "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 p = p" + by pat_completeness auto + +termination + by (relation "measure fmsize") (simp_all add: fmsize_pos) lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p" by (induct p arbitrary: bs rule: prep.induct) auto @@ -434,25 +437,6 @@ "numadd (C b1, C b2) = C (b1 + b2)" "numadd (a, b) = Add a b" -(*function (sequential) - numadd :: "num \ num \ num" -where - "numadd (Add (Mul c1 (Bound n1)) r1) (Add (Mul c2 (Bound n2)) r2) = - (if n1 = n2 then (let c = c1 + c2 - in (if c = 0 then numadd r1 r2 else - Add (Mul c (Bound n1)) (numadd r1 r2))) - else if n1 \ n2 then - Add (Mul c1 (Bound n1)) (numadd r1 (Add (Mul c2 (Bound n2)) r2)) - else - Add (Mul c2 (Bound n2)) (numadd (Add (Mul c1 (Bound n1)) r1) r2))" - | "numadd (Add (Mul c1 (Bound n1)) r1) t = - Add (Mul c1 (Bound n1)) (numadd r1 t)" - | "numadd t (Add (Mul c2 (Bound n2)) r2) = - Add (Mul c2 (Bound n2)) (numadd t r2)" - | "numadd (C b1) (C b2) = C (b1 + b2)" - | "numadd a b = Add a b" -apply pat_completeness apply auto*) - lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" apply (induct t s rule: numadd.induct) apply (simp_all add: Let_def) @@ -989,91 +973,95 @@ by simp qed -consts iszlfm :: "fm \ bool" \ \Linearity test for fm\ -recdef iszlfm "measure size" +fun iszlfm :: "fm \ bool" \ \Linearity test for fm\ +where "iszlfm (And p q) \ iszlfm p \ iszlfm q" - "iszlfm (Or p q) \ iszlfm p \ iszlfm q" - "iszlfm (Eq (CN 0 c e)) \ c > 0 \ numbound0 e" - "iszlfm (NEq (CN 0 c e)) \ c > 0 \ numbound0 e" - "iszlfm (Lt (CN 0 c e)) \ c > 0 \ numbound0 e" - "iszlfm (Le (CN 0 c e)) \ c > 0 \ numbound0 e" - "iszlfm (Gt (CN 0 c e)) \ c > 0 \ numbound0 e" - "iszlfm (Ge (CN 0 c e)) \ c > 0 \ numbound0 e" - "iszlfm (Dvd i (CN 0 c e)) \ c > 0 \ i > 0 \ numbound0 e" - "iszlfm (NDvd i (CN 0 c e)) \ c > 0 \ i > 0 \ numbound0 e" - "iszlfm p \ isatom p \ bound0 p" +| "iszlfm (Or p q) \ iszlfm p \ iszlfm q" +| "iszlfm (Eq (CN 0 c e)) \ c > 0 \ numbound0 e" +| "iszlfm (NEq (CN 0 c e)) \ c > 0 \ numbound0 e" +| "iszlfm (Lt (CN 0 c e)) \ c > 0 \ numbound0 e" +| "iszlfm (Le (CN 0 c e)) \ c > 0 \ numbound0 e" +| "iszlfm (Gt (CN 0 c e)) \ c > 0 \ numbound0 e" +| "iszlfm (Ge (CN 0 c e)) \ c > 0 \ numbound0 e" +| "iszlfm (Dvd i (CN 0 c e)) \ c > 0 \ i > 0 \ numbound0 e" +| "iszlfm (NDvd i (CN 0 c e)) \ c > 0 \ i > 0 \ numbound0 e" +| "iszlfm p \ isatom p \ bound0 p" lemma zlin_qfree: "iszlfm p \ qfree p" by (induct p rule: iszlfm.induct) auto -consts zlfm :: "fm \ fm" \ \Linearity transformation for fm\ -recdef zlfm "measure fmsize" +function (sequential) zlfm :: "fm \ fm" \ \Linearity transformation for fm\ +where "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 (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))" - "zlfm (Lt a) = +| "zlfm (Or p q) = Or (zlfm 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)))" +| "zlfm (Lt a) = (let (c, r) = zsplit0 a in if c = 0 then Lt r else if c > 0 then (Lt (CN 0 c r)) else Gt (CN 0 (- c) (Neg r)))" - "zlfm (Le a) = +| "zlfm (Le a) = (let (c, r) = zsplit0 a in if c = 0 then Le r else if c > 0 then Le (CN 0 c r) else Ge (CN 0 (- c) (Neg r)))" - "zlfm (Gt a) = +| "zlfm (Gt a) = (let (c, r) = zsplit0 a in if c = 0 then Gt r else if c > 0 then Gt (CN 0 c r) else Lt (CN 0 (- c) (Neg r)))" - "zlfm (Ge a) = +| "zlfm (Ge a) = (let (c, r) = zsplit0 a in if c = 0 then Ge r else if c > 0 then Ge (CN 0 c r) else Le (CN 0 (- c) (Neg r)))" - "zlfm (Eq a) = +| "zlfm (Eq a) = (let (c, r) = zsplit0 a in if c = 0 then Eq r else if c > 0 then Eq (CN 0 c r) else Eq (CN 0 (- c) (Neg r)))" - "zlfm (NEq a) = +| "zlfm (NEq a) = (let (c, r) = zsplit0 a in if c = 0 then NEq r else if c > 0 then NEq (CN 0 c r) else NEq (CN 0 (- c) (Neg r)))" - "zlfm (Dvd i a) = +| "zlfm (Dvd i a) = (if i = 0 then zlfm (Eq a) else let (c, r) = zsplit0 a in if c = 0 then Dvd \i\ r else if c > 0 then Dvd \i\ (CN 0 c r) else Dvd \i\ (CN 0 (- c) (Neg r)))" - "zlfm (NDvd i a) = +| "zlfm (NDvd i a) = (if i = 0 then zlfm (NEq a) else let (c, r) = zsplit0 a in if c = 0 then NDvd \i\ r else if c > 0 then NDvd \i\ (CN 0 c r) else NDvd \i\ (CN 0 (- c) (Neg r)))" - "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 p = p" (hints simp add: fmsize_pos) +| "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 p = p" + by pat_completeness auto + +termination + by (relation "measure fmsize") (simp_all add: fmsize_pos) lemma zlfm_I: assumes qfp: "qfree p" @@ -1258,48 +1246,48 @@ qed qed auto -consts minusinf :: "fm \ fm" \ \Virtual substitution of \-\\\ -recdef minusinf "measure size" +fun minusinf :: "fm \ fm" \ \Virtual substitution of \-\\\ +where "minusinf (And p q) = And (minusinf p) (minusinf q)" - "minusinf (Or p q) = Or (minusinf p) (minusinf q)" - "minusinf (Eq (CN 0 c e)) = F" - "minusinf (NEq (CN 0 c e)) = T" - "minusinf (Lt (CN 0 c e)) = T" - "minusinf (Le (CN 0 c e)) = T" - "minusinf (Gt (CN 0 c e)) = F" - "minusinf (Ge (CN 0 c e)) = F" - "minusinf p = p" +| "minusinf (Or p q) = Or (minusinf p) (minusinf q)" +| "minusinf (Eq (CN 0 c e)) = F" +| "minusinf (NEq (CN 0 c e)) = T" +| "minusinf (Lt (CN 0 c e)) = T" +| "minusinf (Le (CN 0 c e)) = T" +| "minusinf (Gt (CN 0 c e)) = F" +| "minusinf (Ge (CN 0 c e)) = F" +| "minusinf p = p" lemma minusinf_qfree: "qfree p \ qfree (minusinf p)" by (induct p rule: minusinf.induct) auto -consts plusinf :: "fm \ fm" \ \Virtual substitution of \+\\\ -recdef plusinf "measure size" +fun plusinf :: "fm \ fm" \ \Virtual substitution of \+\\\ +where "plusinf (And p q) = And (plusinf p) (plusinf q)" - "plusinf (Or p q) = Or (plusinf p) (plusinf q)" - "plusinf (Eq (CN 0 c e)) = F" - "plusinf (NEq (CN 0 c e)) = T" - "plusinf (Lt (CN 0 c e)) = F" - "plusinf (Le (CN 0 c e)) = F" - "plusinf (Gt (CN 0 c e)) = T" - "plusinf (Ge (CN 0 c e)) = T" - "plusinf p = p" +| "plusinf (Or p q) = Or (plusinf p) (plusinf q)" +| "plusinf (Eq (CN 0 c e)) = F" +| "plusinf (NEq (CN 0 c e)) = T" +| "plusinf (Lt (CN 0 c e)) = F" +| "plusinf (Le (CN 0 c e)) = F" +| "plusinf (Gt (CN 0 c e)) = T" +| "plusinf (Ge (CN 0 c e)) = T" +| "plusinf p = p" -consts \ :: "fm \ int" \ \Compute \lcm {d| N\<^sup>? Dvd c*x+t \ p}\\ -recdef \ "measure size" +fun \ :: "fm \ int" \ \Compute \lcm {d| N\<^sup>? Dvd c*x+t \ p}\\ +where "\ (And p q) = lcm (\ p) (\ q)" - "\ (Or p q) = lcm (\ p) (\ q)" - "\ (Dvd i (CN 0 c e)) = i" - "\ (NDvd i (CN 0 c e)) = i" - "\ p = 1" +| "\ (Or p q) = lcm (\ p) (\ q)" +| "\ (Dvd i (CN 0 c e)) = i" +| "\ (NDvd i (CN 0 c e)) = i" +| "\ p = 1" -consts d_\ :: "fm \ int \ bool" \ \check if a given l divides all the ds above\ -recdef d_\ "measure size" - "d_\ (And p q) = (\d. d_\ p d \ d_\ q d)" - "d_\ (Or p q) = (\d. d_\ p d \ d_\ q d)" - "d_\ (Dvd i (CN 0 c e)) = (\d. i dvd d)" - "d_\ (NDvd i (CN 0 c e)) = (\d. i dvd d)" - "d_\ p = (\d. True)" +fun d_\ :: "fm \ int \ bool" \ \check if a given l divides all the ds above\ +where + "d_\ (And p q) d \ d_\ p d \ d_\ q d" +| "d_\ (Or p q) d \ d_\ p d \ d_\ q d" +| "d_\ (Dvd i (CN 0 c e)) d \ i dvd d" +| "d_\ (NDvd i (CN 0 c e)) d \ i dvd d" +| "d_\ p d \ True" lemma delta_mono: assumes lin: "iszlfm p" @@ -1321,118 +1309,87 @@ assumes lin: "iszlfm p" shows "d_\ p (\ p) \ \ p >0" using lin -proof (induct p rule: iszlfm.induct) - case (1 p q) - let ?d = "\ (And p q)" - from 1 lcm_pos_int have dp: "?d > 0" - by simp - have d1: "\ p dvd \ (And p q)" - using 1 by simp - then have th: "d_\ p ?d" - using delta_mono 1(2,3) by (simp only: iszlfm.simps) - have "\ q dvd \ (And p q)" - using 1 by simp - then have th': "d_\ q ?d" - using delta_mono 1 by (simp only: iszlfm.simps) - from th th' dp show ?case - by simp -next - case (2 p q) - let ?d = "\ (And p q)" - from 2 lcm_pos_int have dp: "?d > 0" - by simp - have "\ p dvd \ (And p q)" - using 2 by simp - then have th: "d_\ p ?d" - using delta_mono 2 by (simp only: iszlfm.simps) - have "\ q dvd \ (And p q)" - using 2 by simp - then have th': "d_\ q ?d" - using delta_mono 2 by (simp only: iszlfm.simps) - from th th' dp show ?case - by simp -qed simp_all + by (induct p rule: iszlfm.induct) (auto intro: delta_mono simp add: lcm_pos_int) +fun a_\ :: "fm \ int \ fm" \ \adjust the coefficients of a formula\ +where + "a_\ (And p q) k = And (a_\ p k) (a_\ q k)" +| "a_\ (Or p q) k = Or (a_\ p k) (a_\ q k)" +| "a_\ (Eq (CN 0 c e)) k = Eq (CN 0 1 (Mul (k div c) e))" +| "a_\ (NEq (CN 0 c e)) k = NEq (CN 0 1 (Mul (k div c) e))" +| "a_\ (Lt (CN 0 c e)) k = Lt (CN 0 1 (Mul (k div c) e))" +| "a_\ (Le (CN 0 c e)) k = Le (CN 0 1 (Mul (k div c) e))" +| "a_\ (Gt (CN 0 c e)) k = Gt (CN 0 1 (Mul (k div c) e))" +| "a_\ (Ge (CN 0 c e)) k = Ge (CN 0 1 (Mul (k div c) e))" +| "a_\ (Dvd i (CN 0 c e)) k = Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e))" +| "a_\ (NDvd i (CN 0 c e)) k = NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e))" +| "a_\ p k = p" -consts a_\ :: "fm \ int \ fm" \ \adjust the coefficients of a formula\ -recdef a_\ "measure size" - "a_\ (And p q) = (\k. And (a_\ p k) (a_\ q k))" - "a_\ (Or p q) = (\k. Or (a_\ p k) (a_\ q k))" - "a_\ (Eq (CN 0 c e)) = (\k. Eq (CN 0 1 (Mul (k div c) e)))" - "a_\ (NEq (CN 0 c e)) = (\k. NEq (CN 0 1 (Mul (k div c) e)))" - "a_\ (Lt (CN 0 c e)) = (\k. Lt (CN 0 1 (Mul (k div c) e)))" - "a_\ (Le (CN 0 c e)) = (\k. Le (CN 0 1 (Mul (k div c) e)))" - "a_\ (Gt (CN 0 c e)) = (\k. Gt (CN 0 1 (Mul (k div c) e)))" - "a_\ (Ge (CN 0 c e)) = (\k. Ge (CN 0 1 (Mul (k div c) e)))" - "a_\ (Dvd i (CN 0 c e)) =(\k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" - "a_\ (NDvd i (CN 0 c e))=(\k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" - "a_\ p = (\k. p)" +fun d_\ :: "fm \ int \ bool" \ \test if all coeffs c of c divide a given l\ +where + "d_\ (And p q) k \ d_\ p k \ d_\ q k" +| "d_\ (Or p q) k \ d_\ p k \ d_\ q k" +| "d_\ (Eq (CN 0 c e)) k \ c dvd k" +| "d_\ (NEq (CN 0 c e)) k \ c dvd k" +| "d_\ (Lt (CN 0 c e)) k \ c dvd k" +| "d_\ (Le (CN 0 c e)) k \ c dvd k" +| "d_\ (Gt (CN 0 c e)) k \ c dvd k" +| "d_\ (Ge (CN 0 c e)) k \ c dvd k" +| "d_\ (Dvd i (CN 0 c e)) k \ c dvd k" +| "d_\ (NDvd i (CN 0 c e)) k \ c dvd k" +| "d_\ p k \ True" -consts d_\ :: "fm \ int \ bool" \ \test if all coeffs c of c divide a given l\ -recdef d_\ "measure size" - "d_\ (And p q) = (\k. (d_\ p k) \ (d_\ q k))" - "d_\ (Or p q) = (\k. (d_\ p k) \ (d_\ q k))" - "d_\ (Eq (CN 0 c e)) = (\k. c dvd k)" - "d_\ (NEq (CN 0 c e)) = (\k. c dvd k)" - "d_\ (Lt (CN 0 c e)) = (\k. c dvd k)" - "d_\ (Le (CN 0 c e)) = (\k. c dvd k)" - "d_\ (Gt (CN 0 c e)) = (\k. c dvd k)" - "d_\ (Ge (CN 0 c e)) = (\k. c dvd k)" - "d_\ (Dvd i (CN 0 c e)) =(\k. c dvd k)" - "d_\ (NDvd i (CN 0 c e))=(\k. c dvd k)" - "d_\ p = (\k. True)" +fun \ :: "fm \ int" \ \computes the lcm of all coefficients of x\ +where + "\ (And p q) = lcm (\ p) (\ q)" +| "\ (Or p q) = lcm (\ p) (\ q)" +| "\ (Eq (CN 0 c e)) = c" +| "\ (NEq (CN 0 c e)) = c" +| "\ (Lt (CN 0 c e)) = c" +| "\ (Le (CN 0 c e)) = c" +| "\ (Gt (CN 0 c e)) = c" +| "\ (Ge (CN 0 c e)) = c" +| "\ (Dvd i (CN 0 c e)) = c" +| "\ (NDvd i (CN 0 c e))= c" +| "\ p = 1" -consts \ :: "fm \ int" \ \computes the lcm of all coefficients of x\ -recdef \ "measure size" - "\ (And p q) = lcm (\ p) (\ q)" - "\ (Or p q) = lcm (\ p) (\ q)" - "\ (Eq (CN 0 c e)) = c" - "\ (NEq (CN 0 c e)) = c" - "\ (Lt (CN 0 c e)) = c" - "\ (Le (CN 0 c e)) = c" - "\ (Gt (CN 0 c e)) = c" - "\ (Ge (CN 0 c e)) = c" - "\ (Dvd i (CN 0 c e)) = c" - "\ (NDvd i (CN 0 c e))= c" - "\ p = 1" - -consts \ :: "fm \ num list" -recdef \ "measure size" +fun \ :: "fm \ num list" +where "\ (And p q) = (\ p @ \ q)" - "\ (Or p q) = (\ p @ \ q)" - "\ (Eq (CN 0 c e)) = [Sub (C (- 1)) e]" - "\ (NEq (CN 0 c e)) = [Neg e]" - "\ (Lt (CN 0 c e)) = []" - "\ (Le (CN 0 c e)) = []" - "\ (Gt (CN 0 c e)) = [Neg e]" - "\ (Ge (CN 0 c e)) = [Sub (C (- 1)) e]" - "\ p = []" +| "\ (Or p q) = (\ p @ \ q)" +| "\ (Eq (CN 0 c e)) = [Sub (C (- 1)) e]" +| "\ (NEq (CN 0 c e)) = [Neg e]" +| "\ (Lt (CN 0 c e)) = []" +| "\ (Le (CN 0 c e)) = []" +| "\ (Gt (CN 0 c e)) = [Neg e]" +| "\ (Ge (CN 0 c e)) = [Sub (C (- 1)) e]" +| "\ p = []" -consts \ :: "fm \ num list" -recdef \ "measure size" +fun \ :: "fm \ num list" +where "\ (And p q) = \ p @ \ q" - "\ (Or p q) = \ p @ \ q" - "\ (Eq (CN 0 c e)) = [Add (C (- 1)) e]" - "\ (NEq (CN 0 c e)) = [e]" - "\ (Lt (CN 0 c e)) = [e]" - "\ (Le (CN 0 c e)) = [Add (C (- 1)) e]" - "\ (Gt (CN 0 c e)) = []" - "\ (Ge (CN 0 c e)) = []" - "\ p = []" +| "\ (Or p q) = \ p @ \ q" +| "\ (Eq (CN 0 c e)) = [Add (C (- 1)) e]" +| "\ (NEq (CN 0 c e)) = [e]" +| "\ (Lt (CN 0 c e)) = [e]" +| "\ (Le (CN 0 c e)) = [Add (C (- 1)) e]" +| "\ (Gt (CN 0 c e)) = []" +| "\ (Ge (CN 0 c e)) = []" +| "\ p = []" -consts mirror :: "fm \ fm" -recdef mirror "measure size" +fun mirror :: "fm \ fm" +where "mirror (And p q) = And (mirror p) (mirror q)" - "mirror (Or p q) = Or (mirror p) (mirror q)" - "mirror (Eq (CN 0 c e)) = Eq (CN 0 c (Neg e))" - "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))" - "mirror (Lt (CN 0 c e)) = Gt (CN 0 c (Neg e))" - "mirror (Le (CN 0 c e)) = Ge (CN 0 c (Neg e))" - "mirror (Gt (CN 0 c e)) = Lt (CN 0 c (Neg e))" - "mirror (Ge (CN 0 c e)) = Le (CN 0 c (Neg e))" - "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))" - "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))" - "mirror p = p" +| "mirror (Or p q) = Or (mirror p) (mirror q)" +| "mirror (Eq (CN 0 c e)) = Eq (CN 0 c (Neg e))" +| "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))" +| "mirror (Lt (CN 0 c e)) = Gt (CN 0 c (Neg e))" +| "mirror (Le (CN 0 c e)) = Ge (CN 0 c (Neg e))" +| "mirror (Gt (CN 0 c e)) = Lt (CN 0 c (Neg e))" +| "mirror (Ge (CN 0 c e)) = Le (CN 0 c (Neg e))" +| "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))" +| "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))" +| "mirror p = p" text \Lemmas for the correctness of \\_\\\ diff -r e383fad30b25 -r 3cb801391353 src/HOL/Tools/Qelim/cooper_procedure.ML --- a/src/HOL/Tools/Qelim/cooper_procedure.ML Fri Feb 10 11:39:23 2017 +0100 +++ b/src/HOL/Tools/Qelim/cooper_procedure.ML Sat Feb 11 22:53:31 2017 +0100 @@ -47,56 +47,6 @@ val one_int = {one = one_inta} : inta one; -fun sgn_integer k = - (if k = (0 : IntInf.int) then (0 : IntInf.int) - else (if k < (0 : IntInf.int) then (~1 : IntInf.int) - else (1 : IntInf.int))); - -fun abs_integer k = (if k < (0 : IntInf.int) then ~ k else k); - -fun apsnd f (x, y) = (x, f y); - -fun divmod_integer k l = - (if k = (0 : IntInf.int) then ((0 : IntInf.int), (0 : IntInf.int)) - else (if l = (0 : IntInf.int) then ((0 : IntInf.int), k) - else (apsnd o (fn a => fn b => a * b) o sgn_integer) l - (if sgn_integer k = sgn_integer l - then Integer.div_mod (abs k) (abs l) - else let - val (r, s) = Integer.div_mod (abs k) (abs l); - in - (if s = (0 : IntInf.int) then (~ r, (0 : IntInf.int)) - else (~ r - (1 : IntInf.int), abs_integer l - s)) - end))); - -fun fst (x1, x2) = x1; - -fun divide_integer k l = fst (divmod_integer k l); - -fun divide_inta k l = - Int_of_integer (divide_integer (integer_of_int k) (integer_of_int l)); - -fun snd (x1, x2) = x2; - -fun mod_integer k l = snd (divmod_integer k l); - -fun mod_int k l = - Int_of_integer (mod_integer (integer_of_int k) (integer_of_int l)); - -type 'a divide = {divide : 'a -> 'a -> 'a}; -val divide = #divide : 'a divide -> 'a -> 'a -> 'a; - -type 'a diva = - {divide_div : 'a divide, dvd_div : 'a dvd, moda : 'a -> 'a -> 'a}; -val divide_div = #divide_div : 'a diva -> 'a divide; -val dvd_div = #dvd_div : 'a diva -> 'a dvd; -val moda = #moda : 'a diva -> 'a -> 'a -> 'a; - -val divide_int = {divide = divide_inta} : inta divide; - -val div_int = {divide_div = divide_int, dvd_div = dvd_int, moda = mod_int} : - inta diva; - fun plus_inta k l = Int_of_integer (integer_of_int k + integer_of_int l); type 'a plus = {plus : 'a -> 'a -> 'a}; @@ -139,6 +89,55 @@ val minus_int = {minus = minus_inta} : inta minus; +fun sgn_integer k = + (if k = (0 : IntInf.int) then (0 : IntInf.int) + else (if k < (0 : IntInf.int) then (~1 : IntInf.int) + else (1 : IntInf.int))); + +fun apsnd f (x, y) = (x, f y); + +fun divmod_integer k l = + (if k = (0 : IntInf.int) then ((0 : IntInf.int), (0 : IntInf.int)) + else (if l = (0 : IntInf.int) then ((0 : IntInf.int), k) + else (apsnd o (fn a => fn b => a * b) o sgn_integer) l + (if sgn_integer k = sgn_integer l + then Integer.div_mod (abs k) (abs l) + else let + val (r, s) = Integer.div_mod (abs k) (abs l); + in + (if s = (0 : IntInf.int) then (~ r, (0 : IntInf.int)) + else (~ r - (1 : IntInf.int), abs l - s)) + end))); + +fun fst (x1, x2) = x1; + +fun divide_integer k l = fst (divmod_integer k l); + +fun divide_inta k l = + Int_of_integer (divide_integer (integer_of_int k) (integer_of_int l)); + +type 'a divide = {divide : 'a -> 'a -> 'a}; +val divide = #divide : 'a divide -> 'a -> 'a -> 'a; + +val divide_int = {divide = divide_inta} : inta divide; + +fun snd (x1, x2) = x2; + +fun modulo_integer k l = snd (divmod_integer k l); + +fun modulo_inta k l = + Int_of_integer (modulo_integer (integer_of_int k) (integer_of_int l)); + +type 'a modulo = + {divide_modulo : 'a divide, dvd_modulo : 'a dvd, modulo : 'a -> 'a -> 'a}; +val divide_modulo = #divide_modulo : 'a modulo -> 'a divide; +val dvd_modulo = #dvd_modulo : 'a modulo -> 'a dvd; +val modulo = #modulo : 'a modulo -> 'a -> 'a -> 'a; + +val modulo_int = + {divide_modulo = divide_int, dvd_modulo = dvd_int, modulo = modulo_inta} : + inta modulo; + type 'a ab_semigroup_add = {semigroup_add_ab_semigroup_add : 'a semigroup_add}; val semigroup_add_ab_semigroup_add = #semigroup_add_ab_semigroup_add : 'a ab_semigroup_add -> 'a semigroup_add; @@ -344,12 +343,12 @@ 'a comm_semiring_1_cancel -> 'a semiring_1_cancel; type 'a semidom = - {semiring_1_no_zero_divisors_semidom : 'a semiring_1_no_zero_divisors, - comm_semiring_1_cancel_semidom : 'a comm_semiring_1_cancel}; + {comm_semiring_1_cancel_semidom : 'a comm_semiring_1_cancel, + semiring_1_no_zero_divisors_semidom : 'a semiring_1_no_zero_divisors}; +val comm_semiring_1_cancel_semidom = #comm_semiring_1_cancel_semidom : + 'a semidom -> 'a comm_semiring_1_cancel; val semiring_1_no_zero_divisors_semidom = #semiring_1_no_zero_divisors_semidom : 'a semidom -> 'a semiring_1_no_zero_divisors; -val comm_semiring_1_cancel_semidom = #comm_semiring_1_cancel_semidom : - 'a semidom -> 'a comm_semiring_1_cancel; val ab_semigroup_add_int = {semigroup_add_ab_semigroup_add = semigroup_add_int} : inta ab_semigroup_add; @@ -473,8 +472,8 @@ : inta comm_semiring_1_cancel; val semidom_int = - {semiring_1_no_zero_divisors_semidom = semiring_1_no_zero_divisors_int, - comm_semiring_1_cancel_semidom = comm_semiring_1_cancel_int} + {comm_semiring_1_cancel_semidom = comm_semiring_1_cancel_int, + semiring_1_no_zero_divisors_semidom = semiring_1_no_zero_divisors_int} : inta semidom; type 'a semiring_no_zero_divisors_cancel = @@ -496,18 +495,6 @@ #semiring_no_zero_divisors_cancel_semidom_divide : 'a semidom_divide -> 'a semiring_no_zero_divisors_cancel; -type 'a algebraic_semidom = - {semidom_divide_algebraic_semidom : 'a semidom_divide}; -val semidom_divide_algebraic_semidom = #semidom_divide_algebraic_semidom : - 'a algebraic_semidom -> 'a semidom_divide; - -type 'a semiring_div = - {div_semiring_div : 'a diva, - algebraic_semidom_semiring_div : 'a algebraic_semidom}; -val div_semiring_div = #div_semiring_div : 'a semiring_div -> 'a diva; -val algebraic_semidom_semiring_div = #algebraic_semidom_semiring_div : - 'a semiring_div -> 'a algebraic_semidom; - val semiring_no_zero_divisors_cancel_int = {semiring_no_zero_divisors_semiring_no_zero_divisors_cancel = semiring_no_zero_divisors_int} @@ -519,14 +506,41 @@ semiring_no_zero_divisors_cancel_int} : inta semidom_divide; +type 'a semiring_modulo = + {comm_semiring_1_cancel_semiring_modulo : 'a comm_semiring_1_cancel, + modulo_semiring_modulo : 'a modulo}; +val comm_semiring_1_cancel_semiring_modulo = + #comm_semiring_1_cancel_semiring_modulo : + 'a semiring_modulo -> 'a comm_semiring_1_cancel; +val modulo_semiring_modulo = #modulo_semiring_modulo : + 'a semiring_modulo -> 'a modulo; + +val semiring_modulo_int = + {comm_semiring_1_cancel_semiring_modulo = comm_semiring_1_cancel_int, + modulo_semiring_modulo = modulo_int} + : inta semiring_modulo; + +type 'a algebraic_semidom = + {semidom_divide_algebraic_semidom : 'a semidom_divide}; +val semidom_divide_algebraic_semidom = #semidom_divide_algebraic_semidom : + 'a algebraic_semidom -> 'a semidom_divide; + val algebraic_semidom_int = {semidom_divide_algebraic_semidom = semidom_divide_int} : inta algebraic_semidom; -val semiring_div_int = - {div_semiring_div = div_int, - algebraic_semidom_semiring_div = algebraic_semidom_int} - : inta semiring_div; +type 'a semidom_modulo = + {algebraic_semidom_semidom_modulo : 'a algebraic_semidom, + semiring_modulo_semidom_modulo : 'a semiring_modulo}; +val algebraic_semidom_semidom_modulo = #algebraic_semidom_semidom_modulo : + 'a semidom_modulo -> 'a algebraic_semidom; +val semiring_modulo_semidom_modulo = #semiring_modulo_semidom_modulo : + 'a semidom_modulo -> 'a semiring_modulo; + +val semidom_modulo_int = + {algebraic_semidom_semidom_modulo = algebraic_semidom_int, + semiring_modulo_semidom_modulo = semiring_modulo_int} + : inta semidom_modulo; datatype nat = Nat of int; @@ -1035,69 +1049,69 @@ | minusinf (Or (p, q)) = Or (minusinf p, minusinf q) | minusinf T = T | minusinf F = F - | minusinf (Lt (C bo)) = Lt (C bo) - | minusinf (Lt (Bound bp)) = Lt (Bound bp) - | minusinf (Lt (Neg bt)) = Lt (Neg bt) - | minusinf (Lt (Add (bu, bv))) = Lt (Add (bu, bv)) - | minusinf (Lt (Sub (bw, bx))) = Lt (Sub (bw, bx)) - | minusinf (Lt (Mul (by, bz))) = Lt (Mul (by, bz)) - | minusinf (Le (C co)) = Le (C co) - | minusinf (Le (Bound cp)) = Le (Bound cp) - | minusinf (Le (Neg ct)) = Le (Neg ct) - | minusinf (Le (Add (cu, cv))) = Le (Add (cu, cv)) - | minusinf (Le (Sub (cw, cx))) = Le (Sub (cw, cx)) - | minusinf (Le (Mul (cy, cz))) = Le (Mul (cy, cz)) - | minusinf (Gt (C doa)) = Gt (C doa) - | minusinf (Gt (Bound dp)) = Gt (Bound dp) - | minusinf (Gt (Neg dt)) = Gt (Neg dt) - | minusinf (Gt (Add (du, dv))) = Gt (Add (du, dv)) - | minusinf (Gt (Sub (dw, dx))) = Gt (Sub (dw, dx)) - | minusinf (Gt (Mul (dy, dz))) = Gt (Mul (dy, dz)) - | minusinf (Ge (C eo)) = Ge (C eo) - | minusinf (Ge (Bound ep)) = Ge (Bound ep) - | minusinf (Ge (Neg et)) = Ge (Neg et) - | minusinf (Ge (Add (eu, ev))) = Ge (Add (eu, ev)) - | minusinf (Ge (Sub (ew, ex))) = Ge (Sub (ew, ex)) - | minusinf (Ge (Mul (ey, ez))) = Ge (Mul (ey, ez)) - | minusinf (Eq (C fo)) = Eq (C fo) - | minusinf (Eq (Bound fp)) = Eq (Bound fp) - | minusinf (Eq (Neg ft)) = Eq (Neg ft) - | minusinf (Eq (Add (fu, fv))) = Eq (Add (fu, fv)) - | minusinf (Eq (Sub (fw, fx))) = Eq (Sub (fw, fx)) - | minusinf (Eq (Mul (fy, fz))) = Eq (Mul (fy, fz)) - | minusinf (NEq (C go)) = NEq (C go) - | minusinf (NEq (Bound gp)) = NEq (Bound gp) - | minusinf (NEq (Neg gt)) = NEq (Neg gt) - | minusinf (NEq (Add (gu, gv))) = NEq (Add (gu, gv)) - | minusinf (NEq (Sub (gw, gx))) = NEq (Sub (gw, gx)) - | minusinf (NEq (Mul (gy, gz))) = NEq (Mul (gy, gz)) - | minusinf (Dvd (aa, ab)) = Dvd (aa, ab) - | minusinf (NDvd (ac, ad)) = NDvd (ac, ad) - | minusinf (NOT ae) = NOT ae - | minusinf (Imp (aj, ak)) = Imp (aj, ak) - | minusinf (Iff (al, am)) = Iff (al, am) - | minusinf (E an) = E an - | minusinf (A ao) = A ao - | minusinf (Closed ap) = Closed ap - | minusinf (NClosed aq) = NClosed aq - | minusinf (Lt (CN (cm, c, e))) = - (if equal_nat cm zero_nat then T - else Lt (CN (suc (minus_nat cm one_nat), c, e))) - | minusinf (Le (CN (dm, c, e))) = - (if equal_nat dm zero_nat then T - else Le (CN (suc (minus_nat dm one_nat), c, e))) - | minusinf (Gt (CN (em, c, e))) = - (if equal_nat em zero_nat then F - else Gt (CN (suc (minus_nat em one_nat), c, e))) - | minusinf (Ge (CN (fm, c, e))) = - (if equal_nat fm zero_nat then F - else Ge (CN (suc (minus_nat fm one_nat), c, e))) - | minusinf (Eq (CN (gm, c, e))) = - (if equal_nat gm zero_nat then F - else Eq (CN (suc (minus_nat gm one_nat), c, e))) - | minusinf (NEq (CN (hm, c, e))) = - (if equal_nat hm zero_nat then T - else NEq (CN (suc (minus_nat hm one_nat), c, e))); + | minusinf (Lt (C va)) = Lt (C va) + | minusinf (Lt (Bound va)) = Lt (Bound va) + | minusinf (Lt (Neg va)) = Lt (Neg va) + | minusinf (Lt (Add (va, vb))) = Lt (Add (va, vb)) + | minusinf (Lt (Sub (va, vb))) = Lt (Sub (va, vb)) + | minusinf (Lt (Mul (va, vb))) = Lt (Mul (va, vb)) + | minusinf (Le (C va)) = Le (C va) + | minusinf (Le (Bound va)) = Le (Bound va) + | minusinf (Le (Neg va)) = Le (Neg va) + | minusinf (Le (Add (va, vb))) = Le (Add (va, vb)) + | minusinf (Le (Sub (va, vb))) = Le (Sub (va, vb)) + | minusinf (Le (Mul (va, vb))) = Le (Mul (va, vb)) + | minusinf (Gt (C va)) = Gt (C va) + | minusinf (Gt (Bound va)) = Gt (Bound va) + | minusinf (Gt (Neg va)) = Gt (Neg va) + | minusinf (Gt (Add (va, vb))) = Gt (Add (va, vb)) + | minusinf (Gt (Sub (va, vb))) = Gt (Sub (va, vb)) + | minusinf (Gt (Mul (va, vb))) = Gt (Mul (va, vb)) + | minusinf (Ge (C va)) = Ge (C va) + | minusinf (Ge (Bound va)) = Ge (Bound va) + | minusinf (Ge (Neg va)) = Ge (Neg va) + | minusinf (Ge (Add (va, vb))) = Ge (Add (va, vb)) + | minusinf (Ge (Sub (va, vb))) = Ge (Sub (va, vb)) + | minusinf (Ge (Mul (va, vb))) = Ge (Mul (va, vb)) + | minusinf (Eq (C va)) = Eq (C va) + | minusinf (Eq (Bound va)) = Eq (Bound va) + | minusinf (Eq (Neg va)) = Eq (Neg va) + | minusinf (Eq (Add (va, vb))) = Eq (Add (va, vb)) + | minusinf (Eq (Sub (va, vb))) = Eq (Sub (va, vb)) + | minusinf (Eq (Mul (va, vb))) = Eq (Mul (va, vb)) + | minusinf (NEq (C va)) = NEq (C va) + | minusinf (NEq (Bound va)) = NEq (Bound va) + | minusinf (NEq (Neg va)) = NEq (Neg va) + | minusinf (NEq (Add (va, vb))) = NEq (Add (va, vb)) + | minusinf (NEq (Sub (va, vb))) = NEq (Sub (va, vb)) + | 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 (Imp (v, va)) = Imp (v, va) + | minusinf (Iff (v, va)) = Iff (v, va) + | minusinf (E v) = E v + | minusinf (A v) = A v + | minusinf (Closed v) = Closed v + | minusinf (NClosed v) = NClosed v + | minusinf (Lt (CN (vd, c, e))) = + (if equal_nat vd zero_nat then T + else Lt (CN (suc (minus_nat vd one_nat), c, e))) + | minusinf (Le (CN (vd, c, e))) = + (if equal_nat vd zero_nat then T + else Le (CN (suc (minus_nat vd one_nat), c, e))) + | minusinf (Gt (CN (vd, c, e))) = + (if equal_nat vd zero_nat then F + else Gt (CN (suc (minus_nat vd one_nat), c, e))) + | minusinf (Ge (CN (vd, c, e))) = + (if equal_nat vd zero_nat then F + else Ge (CN (suc (minus_nat vd one_nat), c, e))) + | minusinf (Eq (CN (vd, c, e))) = + (if equal_nat vd zero_nat then F + else Eq (CN (suc (minus_nat vd one_nat), c, e))) + | minusinf (NEq (CN (vd, c, e))) = + (if equal_nat vd zero_nat then T + else NEq (CN (suc (minus_nat vd one_nat), c, e))); fun map f [] = [] | map f (x21 :: x22) = f x21 :: map f x22; @@ -1139,12 +1153,14 @@ fun abs_int i = (if less_int i zero_inta then uminus_int i else i); fun dvd (A1_, A2_) a b = - eq A2_ (moda (div_semiring_div A1_) b a) + eq A2_ + (modulo ((modulo_semiring_modulo o semiring_modulo_semidom_modulo) A1_) b a) (zero ((zero_mult_zero o mult_zero_semiring_0 o semiring_0_semiring_1 o semiring_1_comm_semiring_1 o comm_semiring_1_comm_semiring_1_cancel o comm_semiring_1_cancel_semidom o semidom_semidom_divide o - semidom_divide_algebraic_semidom o algebraic_semidom_semiring_div) + semidom_divide_algebraic_semidom o + algebraic_semidom_semidom_modulo) A1_)); fun nummul i (C j) = C (times_inta i j) @@ -1155,7 +1171,7 @@ | nummul i (Sub (v, va)) = Mul (i, Sub (v, va)) | nummul i (Mul (v, va)) = Mul (i, Mul (v, va)); -fun numneg t = nummul (uminus_int (Int_of_integer (1 : IntInf.int))) t; +fun numneg t = nummul (uminus_int one_inta) t; fun less_eq_nat m n = integer_of_nat m <= integer_of_nat n; @@ -1228,7 +1244,7 @@ fun numsub s t = (if equal_numa s t then C zero_inta else numadd (s, numneg t)); fun simpnum (C j) = C j - | simpnum (Bound n) = CN (n, Int_of_integer (1 : IntInf.int), C zero_inta) + | simpnum (Bound n) = CN (n, one_inta, C zero_inta) | simpnum (Neg t) = numneg (simpnum t) | simpnum (Add (t, s)) = numadd (simpnum t, simpnum s) | simpnum (Sub (t, s)) = numsub (simpnum t) (simpnum s) @@ -1334,26 +1350,27 @@ end | simpfm (Dvd (i, a)) = (if equal_inta i zero_inta then simpfm (Eq a) - else (if equal_inta (abs_int i) (Int_of_integer (1 : IntInf.int)) then T + else (if equal_inta (abs_int i) one_inta then T else let val aa = simpnum a; in (case aa of C v => - (if dvd (semiring_div_int, equal_int) i v then T else F) + (if dvd (semidom_modulo_int, equal_int) i v then T + else F) | Bound _ => Dvd (i, aa) | CN (_, _, _) => Dvd (i, aa) | Neg _ => Dvd (i, aa) | Add (_, _) => Dvd (i, aa) | Sub (_, _) => Dvd (i, aa) | Mul (_, _) => Dvd (i, aa)) end)) | simpfm (NDvd (i, a)) = (if equal_inta i zero_inta then simpfm (NEq a) - else (if equal_inta (abs_int i) (Int_of_integer (1 : IntInf.int)) then F + else (if equal_inta (abs_int i) one_inta then F else let val aa = simpnum a; in (case aa of C v => - (if not (dvd (semiring_div_int, equal_int) i v) then T + (if not (dvd (semidom_modulo_int, equal_int) i v) then T else F) | Bound _ => NDvd (i, aa) | CN (_, _, _) => NDvd (i, aa) | Neg _ => NDvd (i, aa) | Add (_, _) => NDvd (i, aa) @@ -1371,438 +1388,413 @@ fun size_list x = gen_length zero_nat x; -fun a_beta (And (p, q)) = (fn k => And (a_beta p k, a_beta q k)) - | a_beta (Or (p, q)) = (fn k => Or (a_beta p k, a_beta q k)) - | a_beta T = (fn _ => T) - | a_beta F = (fn _ => F) - | a_beta (Lt (C bo)) = (fn _ => Lt (C bo)) - | a_beta (Lt (Bound bp)) = (fn _ => Lt (Bound bp)) - | a_beta (Lt (Neg bt)) = (fn _ => Lt (Neg bt)) - | a_beta (Lt (Add (bu, bv))) = (fn _ => Lt (Add (bu, bv))) - | a_beta (Lt (Sub (bw, bx))) = (fn _ => Lt (Sub (bw, bx))) - | a_beta (Lt (Mul (by, bz))) = (fn _ => Lt (Mul (by, bz))) - | a_beta (Le (C co)) = (fn _ => Le (C co)) - | a_beta (Le (Bound cp)) = (fn _ => Le (Bound cp)) - | a_beta (Le (Neg ct)) = (fn _ => Le (Neg ct)) - | a_beta (Le (Add (cu, cv))) = (fn _ => Le (Add (cu, cv))) - | a_beta (Le (Sub (cw, cx))) = (fn _ => Le (Sub (cw, cx))) - | a_beta (Le (Mul (cy, cz))) = (fn _ => Le (Mul (cy, cz))) - | a_beta (Gt (C doa)) = (fn _ => Gt (C doa)) - | a_beta (Gt (Bound dp)) = (fn _ => Gt (Bound dp)) - | a_beta (Gt (Neg dt)) = (fn _ => Gt (Neg dt)) - | a_beta (Gt (Add (du, dv))) = (fn _ => Gt (Add (du, dv))) - | a_beta (Gt (Sub (dw, dx))) = (fn _ => Gt (Sub (dw, dx))) - | a_beta (Gt (Mul (dy, dz))) = (fn _ => Gt (Mul (dy, dz))) - | a_beta (Ge (C eo)) = (fn _ => Ge (C eo)) - | a_beta (Ge (Bound ep)) = (fn _ => Ge (Bound ep)) - | a_beta (Ge (Neg et)) = (fn _ => Ge (Neg et)) - | a_beta (Ge (Add (eu, ev))) = (fn _ => Ge (Add (eu, ev))) - | a_beta (Ge (Sub (ew, ex))) = (fn _ => Ge (Sub (ew, ex))) - | a_beta (Ge (Mul (ey, ez))) = (fn _ => Ge (Mul (ey, ez))) - | a_beta (Eq (C fo)) = (fn _ => Eq (C fo)) - | a_beta (Eq (Bound fp)) = (fn _ => Eq (Bound fp)) - | a_beta (Eq (Neg ft)) = (fn _ => Eq (Neg ft)) - | a_beta (Eq (Add (fu, fv))) = (fn _ => Eq (Add (fu, fv))) - | a_beta (Eq (Sub (fw, fx))) = (fn _ => Eq (Sub (fw, fx))) - | a_beta (Eq (Mul (fy, fz))) = (fn _ => Eq (Mul (fy, fz))) - | a_beta (NEq (C go)) = (fn _ => NEq (C go)) - | a_beta (NEq (Bound gp)) = (fn _ => NEq (Bound gp)) - | a_beta (NEq (Neg gt)) = (fn _ => NEq (Neg gt)) - | a_beta (NEq (Add (gu, gv))) = (fn _ => NEq (Add (gu, gv))) - | a_beta (NEq (Sub (gw, gx))) = (fn _ => NEq (Sub (gw, gx))) - | a_beta (NEq (Mul (gy, gz))) = (fn _ => NEq (Mul (gy, gz))) - | a_beta (Dvd (aa, C ho)) = (fn _ => Dvd (aa, C ho)) - | a_beta (Dvd (aa, Bound hp)) = (fn _ => Dvd (aa, Bound hp)) - | a_beta (Dvd (aa, Neg ht)) = (fn _ => Dvd (aa, Neg ht)) - | a_beta (Dvd (aa, Add (hu, hv))) = (fn _ => Dvd (aa, Add (hu, hv))) - | a_beta (Dvd (aa, Sub (hw, hx))) = (fn _ => Dvd (aa, Sub (hw, hx))) - | a_beta (Dvd (aa, Mul (hy, hz))) = (fn _ => Dvd (aa, Mul (hy, hz))) - | a_beta (NDvd (ac, C io)) = (fn _ => NDvd (ac, C io)) - | a_beta (NDvd (ac, Bound ip)) = (fn _ => NDvd (ac, Bound ip)) - | a_beta (NDvd (ac, Neg it)) = (fn _ => NDvd (ac, Neg it)) - | a_beta (NDvd (ac, Add (iu, iv))) = (fn _ => NDvd (ac, Add (iu, iv))) - | a_beta (NDvd (ac, Sub (iw, ix))) = (fn _ => NDvd (ac, Sub (iw, ix))) - | a_beta (NDvd (ac, Mul (iy, iz))) = (fn _ => NDvd (ac, Mul (iy, iz))) - | a_beta (NOT ae) = (fn _ => NOT ae) - | a_beta (Imp (aj, ak)) = (fn _ => Imp (aj, ak)) - | a_beta (Iff (al, am)) = (fn _ => Iff (al, am)) - | a_beta (E an) = (fn _ => E an) - | a_beta (A ao) = (fn _ => A ao) - | a_beta (Closed ap) = (fn _ => Closed ap) - | a_beta (NClosed aq) = (fn _ => NClosed aq) - | a_beta (Lt (CN (cm, c, e))) = - (if equal_nat cm zero_nat - then (fn k => - Lt (CN (zero_nat, Int_of_integer (1 : IntInf.int), - Mul (divide_inta k c, e)))) - else (fn _ => Lt (CN (suc (minus_nat cm one_nat), c, e)))) - | a_beta (Le (CN (dm, c, e))) = - (if equal_nat dm zero_nat - then (fn k => - Le (CN (zero_nat, Int_of_integer (1 : IntInf.int), - Mul (divide_inta k c, e)))) - else (fn _ => Le (CN (suc (minus_nat dm one_nat), c, e)))) - | a_beta (Gt (CN (em, c, e))) = - (if equal_nat em zero_nat - then (fn k => - Gt (CN (zero_nat, Int_of_integer (1 : IntInf.int), - Mul (divide_inta k c, e)))) - else (fn _ => Gt (CN (suc (minus_nat em one_nat), c, e)))) - | a_beta (Ge (CN (fm, c, e))) = - (if equal_nat fm zero_nat - then (fn k => - Ge (CN (zero_nat, Int_of_integer (1 : IntInf.int), - Mul (divide_inta k c, e)))) - else (fn _ => Ge (CN (suc (minus_nat fm one_nat), c, e)))) - | a_beta (Eq (CN (gm, c, e))) = - (if equal_nat gm zero_nat - then (fn k => - Eq (CN (zero_nat, Int_of_integer (1 : IntInf.int), - Mul (divide_inta k c, e)))) - else (fn _ => Eq (CN (suc (minus_nat gm one_nat), c, e)))) - | a_beta (NEq (CN (hm, c, e))) = - (if equal_nat hm zero_nat - then (fn k => - NEq (CN (zero_nat, Int_of_integer (1 : IntInf.int), - Mul (divide_inta k c, e)))) - else (fn _ => NEq (CN (suc (minus_nat hm one_nat), c, e)))) - | a_beta (Dvd (i, CN (im, c, e))) = - (if equal_nat im zero_nat - then (fn k => - Dvd (times_inta (divide_inta k c) i, - CN (zero_nat, Int_of_integer (1 : IntInf.int), - Mul (divide_inta k c, e)))) - else (fn _ => Dvd (i, CN (suc (minus_nat im one_nat), c, e)))) - | a_beta (NDvd (i, CN (jm, c, e))) = - (if equal_nat jm zero_nat - then (fn k => - NDvd (times_inta (divide_inta k c) i, - CN (zero_nat, Int_of_integer (1 : IntInf.int), - Mul (divide_inta k c, e)))) - else (fn _ => NDvd (i, CN (suc (minus_nat jm one_nat), c, e)))); +fun a_beta (And (p, q)) k = And (a_beta p k, a_beta q k) + | a_beta (Or (p, q)) k = Or (a_beta p k, a_beta q k) + | a_beta T k = T + | a_beta F k = F + | a_beta (Lt (C va)) k = Lt (C va) + | a_beta (Lt (Bound va)) k = Lt (Bound va) + | a_beta (Lt (Neg va)) k = Lt (Neg va) + | a_beta (Lt (Add (va, vb))) k = Lt (Add (va, vb)) + | a_beta (Lt (Sub (va, vb))) k = Lt (Sub (va, vb)) + | a_beta (Lt (Mul (va, vb))) k = Lt (Mul (va, vb)) + | a_beta (Le (C va)) k = Le (C va) + | a_beta (Le (Bound va)) k = Le (Bound va) + | a_beta (Le (Neg va)) k = Le (Neg va) + | a_beta (Le (Add (va, vb))) k = Le (Add (va, vb)) + | a_beta (Le (Sub (va, vb))) k = Le (Sub (va, vb)) + | a_beta (Le (Mul (va, vb))) k = Le (Mul (va, vb)) + | a_beta (Gt (C va)) k = Gt (C va) + | a_beta (Gt (Bound va)) k = Gt (Bound va) + | a_beta (Gt (Neg va)) k = Gt (Neg va) + | a_beta (Gt (Add (va, vb))) k = Gt (Add (va, vb)) + | a_beta (Gt (Sub (va, vb))) k = Gt (Sub (va, vb)) + | a_beta (Gt (Mul (va, vb))) k = Gt (Mul (va, vb)) + | a_beta (Ge (C va)) k = Ge (C va) + | a_beta (Ge (Bound va)) k = Ge (Bound va) + | a_beta (Ge (Neg va)) k = Ge (Neg va) + | a_beta (Ge (Add (va, vb))) k = Ge (Add (va, vb)) + | a_beta (Ge (Sub (va, vb))) k = Ge (Sub (va, vb)) + | a_beta (Ge (Mul (va, vb))) k = Ge (Mul (va, vb)) + | a_beta (Eq (C va)) k = Eq (C va) + | a_beta (Eq (Bound va)) k = Eq (Bound va) + | a_beta (Eq (Neg va)) k = Eq (Neg va) + | a_beta (Eq (Add (va, vb))) k = Eq (Add (va, vb)) + | a_beta (Eq (Sub (va, vb))) k = Eq (Sub (va, vb)) + | a_beta (Eq (Mul (va, vb))) k = Eq (Mul (va, vb)) + | a_beta (NEq (C va)) k = NEq (C va) + | a_beta (NEq (Bound va)) k = NEq (Bound va) + | a_beta (NEq (Neg va)) k = NEq (Neg va) + | a_beta (NEq (Add (va, vb))) k = NEq (Add (va, vb)) + | a_beta (NEq (Sub (va, vb))) k = NEq (Sub (va, vb)) + | a_beta (NEq (Mul (va, vb))) k = NEq (Mul (va, vb)) + | a_beta (Dvd (v, C vb)) k = Dvd (v, C vb) + | a_beta (Dvd (v, Bound vb)) k = Dvd (v, Bound vb) + | a_beta (Dvd (v, Neg vb)) k = Dvd (v, Neg vb) + | a_beta (Dvd (v, Add (vb, vc))) k = Dvd (v, Add (vb, vc)) + | a_beta (Dvd (v, Sub (vb, vc))) k = Dvd (v, Sub (vb, vc)) + | a_beta (Dvd (v, Mul (vb, vc))) k = Dvd (v, Mul (vb, vc)) + | a_beta (NDvd (v, C vb)) k = NDvd (v, C vb) + | a_beta (NDvd (v, Bound vb)) k = NDvd (v, Bound vb) + | a_beta (NDvd (v, Neg vb)) k = NDvd (v, Neg vb) + | 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 (Imp (v, va)) k = Imp (v, va) + | a_beta (Iff (v, va)) k = Iff (v, va) + | a_beta (E v) k = E v + | a_beta (A v) k = A v + | a_beta (Closed v) k = Closed v + | a_beta (NClosed v) k = NClosed v + | a_beta (Lt (CN (vd, c, e))) k = + (if equal_nat vd zero_nat + then Lt (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) + else Lt (CN (suc (minus_nat vd one_nat), c, e))) + | a_beta (Le (CN (vd, c, e))) k = + (if equal_nat vd zero_nat + then Le (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) + else Le (CN (suc (minus_nat vd one_nat), c, e))) + | a_beta (Gt (CN (vd, c, e))) k = + (if equal_nat vd zero_nat + then Gt (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) + else Gt (CN (suc (minus_nat vd one_nat), c, e))) + | a_beta (Ge (CN (vd, c, e))) k = + (if equal_nat vd zero_nat + then Ge (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) + else Ge (CN (suc (minus_nat vd one_nat), c, e))) + | a_beta (Eq (CN (vd, c, e))) k = + (if equal_nat vd zero_nat + then Eq (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) + else Eq (CN (suc (minus_nat vd one_nat), c, e))) + | a_beta (NEq (CN (vd, c, e))) k = + (if equal_nat vd zero_nat + then NEq (CN (zero_nat, one_inta, Mul (divide_inta k c, e))) + else NEq (CN (suc (minus_nat vd one_nat), c, e))) + | a_beta (Dvd (i, CN (ve, c, e))) k = + (if equal_nat ve zero_nat + then Dvd (times_inta (divide_inta k c) i, + CN (zero_nat, one_inta, Mul (divide_inta k c, e))) + else Dvd (i, CN (suc (minus_nat ve one_nat), c, e))) + | a_beta (NDvd (i, CN (ve, c, e))) k = + (if equal_nat ve zero_nat + then NDvd (times_inta (divide_inta k c) i, + CN (zero_nat, one_inta, Mul (divide_inta k c, e))) + else NDvd (i, CN (suc (minus_nat ve one_nat), c, e))); -fun gcd_int k l = - abs_int - (if equal_inta l zero_inta then k - else gcd_int l (mod_int (abs_int k) (abs_int l))); +fun gcd_integer k l = + abs (if l = (0 : IntInf.int) then k + else gcd_integer l (modulo_integer (abs k) (abs l))); -fun lcm_int a b = - divide_inta (times_inta (abs_int a) (abs_int b)) (gcd_int a b); +fun lcm_integer a b = divide_integer (abs a * abs b) (gcd_integer a b); + +fun lcm_int (Int_of_integer x) (Int_of_integer y) = + Int_of_integer (lcm_integer x y); fun delta (And (p, q)) = lcm_int (delta p) (delta q) | delta (Or (p, q)) = lcm_int (delta p) (delta q) - | delta T = Int_of_integer (1 : IntInf.int) - | delta F = Int_of_integer (1 : IntInf.int) - | delta (Lt u) = Int_of_integer (1 : IntInf.int) - | delta (Le v) = Int_of_integer (1 : IntInf.int) - | delta (Gt w) = Int_of_integer (1 : IntInf.int) - | delta (Ge x) = Int_of_integer (1 : IntInf.int) - | delta (Eq y) = Int_of_integer (1 : IntInf.int) - | delta (NEq z) = Int_of_integer (1 : IntInf.int) - | delta (Dvd (aa, C bo)) = Int_of_integer (1 : IntInf.int) - | delta (Dvd (aa, Bound bp)) = Int_of_integer (1 : IntInf.int) - | delta (Dvd (aa, Neg bt)) = Int_of_integer (1 : IntInf.int) - | delta (Dvd (aa, Add (bu, bv))) = Int_of_integer (1 : IntInf.int) - | delta (Dvd (aa, Sub (bw, bx))) = Int_of_integer (1 : IntInf.int) - | delta (Dvd (aa, Mul (by, bz))) = Int_of_integer (1 : IntInf.int) - | delta (NDvd (ac, C co)) = Int_of_integer (1 : IntInf.int) - | delta (NDvd (ac, Bound cp)) = Int_of_integer (1 : IntInf.int) - | delta (NDvd (ac, Neg ct)) = Int_of_integer (1 : IntInf.int) - | delta (NDvd (ac, Add (cu, cv))) = Int_of_integer (1 : IntInf.int) - | delta (NDvd (ac, Sub (cw, cx))) = Int_of_integer (1 : IntInf.int) - | delta (NDvd (ac, Mul (cy, cz))) = Int_of_integer (1 : IntInf.int) - | delta (NOT ae) = Int_of_integer (1 : IntInf.int) - | delta (Imp (aj, ak)) = Int_of_integer (1 : IntInf.int) - | delta (Iff (al, am)) = Int_of_integer (1 : IntInf.int) - | delta (E an) = Int_of_integer (1 : IntInf.int) - | delta (A ao) = Int_of_integer (1 : IntInf.int) - | delta (Closed ap) = Int_of_integer (1 : IntInf.int) - | delta (NClosed aq) = Int_of_integer (1 : IntInf.int) - | delta (Dvd (i, CN (cm, c, e))) = - (if equal_nat cm zero_nat then i else Int_of_integer (1 : IntInf.int)) - | delta (NDvd (i, CN (dm, c, e))) = - (if equal_nat dm zero_nat then i else Int_of_integer (1 : IntInf.int)); + | delta T = one_inta + | delta F = one_inta + | delta (Lt v) = one_inta + | delta (Le v) = one_inta + | delta (Gt v) = one_inta + | delta (Ge v) = one_inta + | delta (Eq v) = one_inta + | delta (NEq v) = one_inta + | delta (Dvd (v, C vb)) = one_inta + | delta (Dvd (v, Bound vb)) = one_inta + | delta (Dvd (v, Neg vb)) = one_inta + | delta (Dvd (v, Add (vb, vc))) = one_inta + | delta (Dvd (v, Sub (vb, vc))) = one_inta + | delta (Dvd (v, Mul (vb, vc))) = one_inta + | delta (NDvd (v, C vb)) = one_inta + | delta (NDvd (v, Bound vb)) = one_inta + | delta (NDvd (v, Neg vb)) = one_inta + | 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 (Imp (v, va)) = one_inta + | delta (Iff (v, va)) = one_inta + | delta (E v) = one_inta + | delta (A v) = one_inta + | delta (Closed v) = one_inta + | delta (NClosed v) = one_inta + | delta (Dvd (i, CN (ve, c, e))) = + (if equal_nat ve zero_nat then i else one_inta) + | delta (NDvd (i, CN (ve, c, e))) = + (if equal_nat ve zero_nat then i else one_inta); fun alpha (And (p, q)) = alpha p @ alpha q | alpha (Or (p, q)) = alpha p @ alpha q | alpha T = [] | alpha F = [] - | alpha (Lt (C bo)) = [] - | alpha (Lt (Bound bp)) = [] - | alpha (Lt (Neg bt)) = [] - | alpha (Lt (Add (bu, bv))) = [] - | alpha (Lt (Sub (bw, bx))) = [] - | alpha (Lt (Mul (by, bz))) = [] - | alpha (Le (C co)) = [] - | alpha (Le (Bound cp)) = [] - | alpha (Le (Neg ct)) = [] - | alpha (Le (Add (cu, cv))) = [] - | alpha (Le (Sub (cw, cx))) = [] - | alpha (Le (Mul (cy, cz))) = [] - | alpha (Gt (C doa)) = [] - | alpha (Gt (Bound dp)) = [] - | alpha (Gt (Neg dt)) = [] - | alpha (Gt (Add (du, dv))) = [] - | alpha (Gt (Sub (dw, dx))) = [] - | alpha (Gt (Mul (dy, dz))) = [] - | alpha (Ge (C eo)) = [] - | alpha (Ge (Bound ep)) = [] - | alpha (Ge (Neg et)) = [] - | alpha (Ge (Add (eu, ev))) = [] - | alpha (Ge (Sub (ew, ex))) = [] - | alpha (Ge (Mul (ey, ez))) = [] - | alpha (Eq (C fo)) = [] - | alpha (Eq (Bound fp)) = [] - | alpha (Eq (Neg ft)) = [] - | alpha (Eq (Add (fu, fv))) = [] - | alpha (Eq (Sub (fw, fx))) = [] - | alpha (Eq (Mul (fy, fz))) = [] - | alpha (NEq (C go)) = [] - | alpha (NEq (Bound gp)) = [] - | alpha (NEq (Neg gt)) = [] - | alpha (NEq (Add (gu, gv))) = [] - | alpha (NEq (Sub (gw, gx))) = [] - | alpha (NEq (Mul (gy, gz))) = [] - | alpha (Dvd (aa, ab)) = [] - | alpha (NDvd (ac, ad)) = [] - | alpha (NOT ae) = [] - | alpha (Imp (aj, ak)) = [] - | alpha (Iff (al, am)) = [] - | alpha (E an) = [] - | alpha (A ao) = [] - | alpha (Closed ap) = [] - | alpha (NClosed aq) = [] - | alpha (Lt (CN (cm, c, e))) = (if equal_nat cm zero_nat then [e] else []) - | alpha (Le (CN (dm, c, e))) = - (if equal_nat dm zero_nat - then [Add (C (uminus_int (Int_of_integer (1 : IntInf.int))), e)] else []) - | alpha (Gt (CN (em, c, e))) = (if equal_nat em zero_nat then [] else []) - | alpha (Ge (CN (fm, c, e))) = (if equal_nat fm zero_nat then [] else []) - | alpha (Eq (CN (gm, c, e))) = - (if equal_nat gm zero_nat - then [Add (C (uminus_int (Int_of_integer (1 : IntInf.int))), e)] else []) - | alpha (NEq (CN (hm, c, e))) = (if equal_nat hm zero_nat then [e] else []); + | alpha (Lt (C va)) = [] + | alpha (Lt (Bound va)) = [] + | alpha (Lt (Neg va)) = [] + | alpha (Lt (Add (va, vb))) = [] + | alpha (Lt (Sub (va, vb))) = [] + | alpha (Lt (Mul (va, vb))) = [] + | alpha (Le (C va)) = [] + | alpha (Le (Bound va)) = [] + | alpha (Le (Neg va)) = [] + | alpha (Le (Add (va, vb))) = [] + | alpha (Le (Sub (va, vb))) = [] + | alpha (Le (Mul (va, vb))) = [] + | alpha (Gt (C va)) = [] + | alpha (Gt (Bound va)) = [] + | alpha (Gt (Neg va)) = [] + | alpha (Gt (Add (va, vb))) = [] + | alpha (Gt (Sub (va, vb))) = [] + | alpha (Gt (Mul (va, vb))) = [] + | alpha (Ge (C va)) = [] + | alpha (Ge (Bound va)) = [] + | alpha (Ge (Neg va)) = [] + | alpha (Ge (Add (va, vb))) = [] + | alpha (Ge (Sub (va, vb))) = [] + | alpha (Ge (Mul (va, vb))) = [] + | alpha (Eq (C va)) = [] + | alpha (Eq (Bound va)) = [] + | alpha (Eq (Neg va)) = [] + | alpha (Eq (Add (va, vb))) = [] + | alpha (Eq (Sub (va, vb))) = [] + | alpha (Eq (Mul (va, vb))) = [] + | alpha (NEq (C va)) = [] + | alpha (NEq (Bound va)) = [] + | alpha (NEq (Neg va)) = [] + | alpha (NEq (Add (va, vb))) = [] + | alpha (NEq (Sub (va, vb))) = [] + | alpha (NEq (Mul (va, vb))) = [] + | alpha (Dvd (v, va)) = [] + | alpha (NDvd (v, va)) = [] + | alpha (NOT v) = [] + | alpha (Imp (v, va)) = [] + | alpha (Iff (v, va)) = [] + | alpha (E v) = [] + | alpha (A v) = [] + | alpha (Closed v) = [] + | alpha (NClosed v) = [] + | alpha (Lt (CN (vd, c, e))) = (if equal_nat vd zero_nat then [e] else []) + | alpha (Le (CN (vd, c, e))) = + (if equal_nat vd zero_nat then [Add (C (uminus_int one_inta), e)] else []) + | alpha (Gt (CN (vd, c, e))) = (if equal_nat vd zero_nat then [] else []) + | alpha (Ge (CN (vd, c, e))) = (if equal_nat vd zero_nat then [] else []) + | alpha (Eq (CN (vd, c, e))) = + (if equal_nat vd zero_nat then [Add (C (uminus_int one_inta), e)] else []) + | alpha (NEq (CN (vd, c, e))) = (if equal_nat vd zero_nat then [e] else []); fun zeta (And (p, q)) = lcm_int (zeta p) (zeta q) | zeta (Or (p, q)) = lcm_int (zeta p) (zeta q) - | zeta T = Int_of_integer (1 : IntInf.int) - | zeta F = Int_of_integer (1 : IntInf.int) - | zeta (Lt (C bo)) = Int_of_integer (1 : IntInf.int) - | zeta (Lt (Bound bp)) = Int_of_integer (1 : IntInf.int) - | zeta (Lt (Neg bt)) = Int_of_integer (1 : IntInf.int) - | zeta (Lt (Add (bu, bv))) = Int_of_integer (1 : IntInf.int) - | zeta (Lt (Sub (bw, bx))) = Int_of_integer (1 : IntInf.int) - | zeta (Lt (Mul (by, bz))) = Int_of_integer (1 : IntInf.int) - | zeta (Le (C co)) = Int_of_integer (1 : IntInf.int) - | zeta (Le (Bound cp)) = Int_of_integer (1 : IntInf.int) - | zeta (Le (Neg ct)) = Int_of_integer (1 : IntInf.int) - | zeta (Le (Add (cu, cv))) = Int_of_integer (1 : IntInf.int) - | zeta (Le (Sub (cw, cx))) = Int_of_integer (1 : IntInf.int) - | zeta (Le (Mul (cy, cz))) = Int_of_integer (1 : IntInf.int) - | zeta (Gt (C doa)) = Int_of_integer (1 : IntInf.int) - | zeta (Gt (Bound dp)) = Int_of_integer (1 : IntInf.int) - | zeta (Gt (Neg dt)) = Int_of_integer (1 : IntInf.int) - | zeta (Gt (Add (du, dv))) = Int_of_integer (1 : IntInf.int) - | zeta (Gt (Sub (dw, dx))) = Int_of_integer (1 : IntInf.int) - | zeta (Gt (Mul (dy, dz))) = Int_of_integer (1 : IntInf.int) - | zeta (Ge (C eo)) = Int_of_integer (1 : IntInf.int) - | zeta (Ge (Bound ep)) = Int_of_integer (1 : IntInf.int) - | zeta (Ge (Neg et)) = Int_of_integer (1 : IntInf.int) - | zeta (Ge (Add (eu, ev))) = Int_of_integer (1 : IntInf.int) - | zeta (Ge (Sub (ew, ex))) = Int_of_integer (1 : IntInf.int) - | zeta (Ge (Mul (ey, ez))) = Int_of_integer (1 : IntInf.int) - | zeta (Eq (C fo)) = Int_of_integer (1 : IntInf.int) - | zeta (Eq (Bound fp)) = Int_of_integer (1 : IntInf.int) - | zeta (Eq (Neg ft)) = Int_of_integer (1 : IntInf.int) - | zeta (Eq (Add (fu, fv))) = Int_of_integer (1 : IntInf.int) - | zeta (Eq (Sub (fw, fx))) = Int_of_integer (1 : IntInf.int) - | zeta (Eq (Mul (fy, fz))) = Int_of_integer (1 : IntInf.int) - | zeta (NEq (C go)) = Int_of_integer (1 : IntInf.int) - | zeta (NEq (Bound gp)) = Int_of_integer (1 : IntInf.int) - | zeta (NEq (Neg gt)) = Int_of_integer (1 : IntInf.int) - | zeta (NEq (Add (gu, gv))) = Int_of_integer (1 : IntInf.int) - | zeta (NEq (Sub (gw, gx))) = Int_of_integer (1 : IntInf.int) - | zeta (NEq (Mul (gy, gz))) = Int_of_integer (1 : IntInf.int) - | zeta (Dvd (aa, C ho)) = Int_of_integer (1 : IntInf.int) - | zeta (Dvd (aa, Bound hp)) = Int_of_integer (1 : IntInf.int) - | zeta (Dvd (aa, Neg ht)) = Int_of_integer (1 : IntInf.int) - | zeta (Dvd (aa, Add (hu, hv))) = Int_of_integer (1 : IntInf.int) - | zeta (Dvd (aa, Sub (hw, hx))) = Int_of_integer (1 : IntInf.int) - | zeta (Dvd (aa, Mul (hy, hz))) = Int_of_integer (1 : IntInf.int) - | zeta (NDvd (ac, C io)) = Int_of_integer (1 : IntInf.int) - | zeta (NDvd (ac, Bound ip)) = Int_of_integer (1 : IntInf.int) - | zeta (NDvd (ac, Neg it)) = Int_of_integer (1 : IntInf.int) - | zeta (NDvd (ac, Add (iu, iv))) = Int_of_integer (1 : IntInf.int) - | zeta (NDvd (ac, Sub (iw, ix))) = Int_of_integer (1 : IntInf.int) - | zeta (NDvd (ac, Mul (iy, iz))) = Int_of_integer (1 : IntInf.int) - | zeta (NOT ae) = Int_of_integer (1 : IntInf.int) - | zeta (Imp (aj, ak)) = Int_of_integer (1 : IntInf.int) - | zeta (Iff (al, am)) = Int_of_integer (1 : IntInf.int) - | zeta (E an) = Int_of_integer (1 : IntInf.int) - | zeta (A ao) = Int_of_integer (1 : IntInf.int) - | zeta (Closed ap) = Int_of_integer (1 : IntInf.int) - | zeta (NClosed aq) = Int_of_integer (1 : IntInf.int) - | zeta (Lt (CN (cm, c, e))) = - (if equal_nat cm zero_nat then c else Int_of_integer (1 : IntInf.int)) - | zeta (Le (CN (dm, c, e))) = - (if equal_nat dm zero_nat then c else Int_of_integer (1 : IntInf.int)) - | zeta (Gt (CN (em, c, e))) = - (if equal_nat em zero_nat then c else Int_of_integer (1 : IntInf.int)) - | zeta (Ge (CN (fm, c, e))) = - (if equal_nat fm zero_nat then c else Int_of_integer (1 : IntInf.int)) - | zeta (Eq (CN (gm, c, e))) = - (if equal_nat gm zero_nat then c else Int_of_integer (1 : IntInf.int)) - | zeta (NEq (CN (hm, c, e))) = - (if equal_nat hm zero_nat then c else Int_of_integer (1 : IntInf.int)) - | zeta (Dvd (i, CN (im, c, e))) = - (if equal_nat im zero_nat then c else Int_of_integer (1 : IntInf.int)) - | zeta (NDvd (i, CN (jm, c, e))) = - (if equal_nat jm zero_nat then c else Int_of_integer (1 : IntInf.int)); + | zeta T = one_inta + | zeta F = one_inta + | zeta (Lt (C va)) = one_inta + | zeta (Lt (Bound va)) = one_inta + | zeta (Lt (Neg va)) = one_inta + | zeta (Lt (Add (va, vb))) = one_inta + | zeta (Lt (Sub (va, vb))) = one_inta + | zeta (Lt (Mul (va, vb))) = one_inta + | zeta (Le (C va)) = one_inta + | zeta (Le (Bound va)) = one_inta + | zeta (Le (Neg va)) = one_inta + | zeta (Le (Add (va, vb))) = one_inta + | zeta (Le (Sub (va, vb))) = one_inta + | zeta (Le (Mul (va, vb))) = one_inta + | zeta (Gt (C va)) = one_inta + | zeta (Gt (Bound va)) = one_inta + | zeta (Gt (Neg va)) = one_inta + | zeta (Gt (Add (va, vb))) = one_inta + | zeta (Gt (Sub (va, vb))) = one_inta + | zeta (Gt (Mul (va, vb))) = one_inta + | zeta (Ge (C va)) = one_inta + | zeta (Ge (Bound va)) = one_inta + | zeta (Ge (Neg va)) = one_inta + | zeta (Ge (Add (va, vb))) = one_inta + | zeta (Ge (Sub (va, vb))) = one_inta + | zeta (Ge (Mul (va, vb))) = one_inta + | zeta (Eq (C va)) = one_inta + | zeta (Eq (Bound va)) = one_inta + | zeta (Eq (Neg va)) = one_inta + | zeta (Eq (Add (va, vb))) = one_inta + | zeta (Eq (Sub (va, vb))) = one_inta + | zeta (Eq (Mul (va, vb))) = one_inta + | zeta (NEq (C va)) = one_inta + | zeta (NEq (Bound va)) = one_inta + | zeta (NEq (Neg va)) = one_inta + | zeta (NEq (Add (va, vb))) = one_inta + | zeta (NEq (Sub (va, vb))) = one_inta + | zeta (NEq (Mul (va, vb))) = one_inta + | zeta (Dvd (v, C vb)) = one_inta + | zeta (Dvd (v, Bound vb)) = one_inta + | zeta (Dvd (v, Neg vb)) = one_inta + | zeta (Dvd (v, Add (vb, vc))) = one_inta + | zeta (Dvd (v, Sub (vb, vc))) = one_inta + | zeta (Dvd (v, Mul (vb, vc))) = one_inta + | zeta (NDvd (v, C vb)) = one_inta + | zeta (NDvd (v, Bound vb)) = one_inta + | zeta (NDvd (v, Neg vb)) = one_inta + | 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 (Imp (v, va)) = one_inta + | zeta (Iff (v, va)) = one_inta + | zeta (E v) = one_inta + | zeta (A v) = one_inta + | zeta (Closed v) = one_inta + | zeta (NClosed v) = one_inta + | zeta (Lt (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) + | zeta (Le (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) + | zeta (Gt (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) + | zeta (Ge (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) + | zeta (Eq (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) + | zeta (NEq (CN (vd, c, e))) = (if equal_nat vd zero_nat then c else one_inta) + | zeta (Dvd (i, CN (ve, c, e))) = + (if equal_nat ve zero_nat then c else one_inta) + | zeta (NDvd (i, CN (ve, c, e))) = + (if equal_nat ve zero_nat then c else one_inta); fun beta (And (p, q)) = beta p @ beta q | beta (Or (p, q)) = beta p @ beta q | beta T = [] | beta F = [] - | beta (Lt (C bo)) = [] - | beta (Lt (Bound bp)) = [] - | beta (Lt (Neg bt)) = [] - | beta (Lt (Add (bu, bv))) = [] - | beta (Lt (Sub (bw, bx))) = [] - | beta (Lt (Mul (by, bz))) = [] - | beta (Le (C co)) = [] - | beta (Le (Bound cp)) = [] - | beta (Le (Neg ct)) = [] - | beta (Le (Add (cu, cv))) = [] - | beta (Le (Sub (cw, cx))) = [] - | beta (Le (Mul (cy, cz))) = [] - | beta (Gt (C doa)) = [] - | beta (Gt (Bound dp)) = [] - | beta (Gt (Neg dt)) = [] - | beta (Gt (Add (du, dv))) = [] - | beta (Gt (Sub (dw, dx))) = [] - | beta (Gt (Mul (dy, dz))) = [] - | beta (Ge (C eo)) = [] - | beta (Ge (Bound ep)) = [] - | beta (Ge (Neg et)) = [] - | beta (Ge (Add (eu, ev))) = [] - | beta (Ge (Sub (ew, ex))) = [] - | beta (Ge (Mul (ey, ez))) = [] - | beta (Eq (C fo)) = [] - | beta (Eq (Bound fp)) = [] - | beta (Eq (Neg ft)) = [] - | beta (Eq (Add (fu, fv))) = [] - | beta (Eq (Sub (fw, fx))) = [] - | beta (Eq (Mul (fy, fz))) = [] - | beta (NEq (C go)) = [] - | beta (NEq (Bound gp)) = [] - | beta (NEq (Neg gt)) = [] - | beta (NEq (Add (gu, gv))) = [] - | beta (NEq (Sub (gw, gx))) = [] - | beta (NEq (Mul (gy, gz))) = [] - | beta (Dvd (aa, ab)) = [] - | beta (NDvd (ac, ad)) = [] - | beta (NOT ae) = [] - | beta (Imp (aj, ak)) = [] - | beta (Iff (al, am)) = [] - | beta (E an) = [] - | beta (A ao) = [] - | beta (Closed ap) = [] - | beta (NClosed aq) = [] - | beta (Lt (CN (cm, c, e))) = (if equal_nat cm zero_nat then [] else []) - | beta (Le (CN (dm, c, e))) = (if equal_nat dm zero_nat then [] else []) - | beta (Gt (CN (em, c, e))) = (if equal_nat em zero_nat then [Neg e] else []) - | beta (Ge (CN (fm, c, e))) = - (if equal_nat fm zero_nat - then [Sub (C (uminus_int (Int_of_integer (1 : IntInf.int))), e)] else []) - | beta (Eq (CN (gm, c, e))) = - (if equal_nat gm zero_nat - then [Sub (C (uminus_int (Int_of_integer (1 : IntInf.int))), e)] else []) - | beta (NEq (CN (hm, c, e))) = - (if equal_nat hm zero_nat then [Neg e] else []); + | beta (Lt (C va)) = [] + | beta (Lt (Bound va)) = [] + | beta (Lt (Neg va)) = [] + | beta (Lt (Add (va, vb))) = [] + | beta (Lt (Sub (va, vb))) = [] + | beta (Lt (Mul (va, vb))) = [] + | beta (Le (C va)) = [] + | beta (Le (Bound va)) = [] + | beta (Le (Neg va)) = [] + | beta (Le (Add (va, vb))) = [] + | beta (Le (Sub (va, vb))) = [] + | beta (Le (Mul (va, vb))) = [] + | beta (Gt (C va)) = [] + | beta (Gt (Bound va)) = [] + | beta (Gt (Neg va)) = [] + | beta (Gt (Add (va, vb))) = [] + | beta (Gt (Sub (va, vb))) = [] + | beta (Gt (Mul (va, vb))) = [] + | beta (Ge (C va)) = [] + | beta (Ge (Bound va)) = [] + | beta (Ge (Neg va)) = [] + | beta (Ge (Add (va, vb))) = [] + | beta (Ge (Sub (va, vb))) = [] + | beta (Ge (Mul (va, vb))) = [] + | beta (Eq (C va)) = [] + | beta (Eq (Bound va)) = [] + | beta (Eq (Neg va)) = [] + | beta (Eq (Add (va, vb))) = [] + | beta (Eq (Sub (va, vb))) = [] + | beta (Eq (Mul (va, vb))) = [] + | beta (NEq (C va)) = [] + | beta (NEq (Bound va)) = [] + | beta (NEq (Neg va)) = [] + | beta (NEq (Add (va, vb))) = [] + | beta (NEq (Sub (va, vb))) = [] + | beta (NEq (Mul (va, vb))) = [] + | beta (Dvd (v, va)) = [] + | beta (NDvd (v, va)) = [] + | beta (NOT v) = [] + | beta (Imp (v, va)) = [] + | beta (Iff (v, va)) = [] + | beta (E v) = [] + | beta (A v) = [] + | beta (Closed v) = [] + | beta (NClosed v) = [] + | beta (Lt (CN (vd, c, e))) = (if equal_nat vd zero_nat then [] else []) + | beta (Le (CN (vd, c, e))) = (if equal_nat vd zero_nat then [] else []) + | beta (Gt (CN (vd, c, e))) = (if equal_nat vd zero_nat then [Neg e] else []) + | beta (Ge (CN (vd, c, e))) = + (if equal_nat vd zero_nat then [Sub (C (uminus_int one_inta), e)] else []) + | beta (Eq (CN (vd, c, e))) = + (if equal_nat vd zero_nat then [Sub (C (uminus_int one_inta), e)] else []) + | beta (NEq (CN (vd, c, e))) = + (if equal_nat vd zero_nat then [Neg e] else []); fun mirror (And (p, q)) = And (mirror p, mirror q) | mirror (Or (p, q)) = Or (mirror p, mirror q) | mirror T = T | mirror F = F - | mirror (Lt (C bo)) = Lt (C bo) - | mirror (Lt (Bound bp)) = Lt (Bound bp) - | mirror (Lt (Neg bt)) = Lt (Neg bt) - | mirror (Lt (Add (bu, bv))) = Lt (Add (bu, bv)) - | mirror (Lt (Sub (bw, bx))) = Lt (Sub (bw, bx)) - | mirror (Lt (Mul (by, bz))) = Lt (Mul (by, bz)) - | mirror (Le (C co)) = Le (C co) - | mirror (Le (Bound cp)) = Le (Bound cp) - | mirror (Le (Neg ct)) = Le (Neg ct) - | mirror (Le (Add (cu, cv))) = Le (Add (cu, cv)) - | mirror (Le (Sub (cw, cx))) = Le (Sub (cw, cx)) - | mirror (Le (Mul (cy, cz))) = Le (Mul (cy, cz)) - | mirror (Gt (C doa)) = Gt (C doa) - | mirror (Gt (Bound dp)) = Gt (Bound dp) - | mirror (Gt (Neg dt)) = Gt (Neg dt) - | mirror (Gt (Add (du, dv))) = Gt (Add (du, dv)) - | mirror (Gt (Sub (dw, dx))) = Gt (Sub (dw, dx)) - | mirror (Gt (Mul (dy, dz))) = Gt (Mul (dy, dz)) - | mirror (Ge (C eo)) = Ge (C eo) - | mirror (Ge (Bound ep)) = Ge (Bound ep) - | mirror (Ge (Neg et)) = Ge (Neg et) - | mirror (Ge (Add (eu, ev))) = Ge (Add (eu, ev)) - | mirror (Ge (Sub (ew, ex))) = Ge (Sub (ew, ex)) - | mirror (Ge (Mul (ey, ez))) = Ge (Mul (ey, ez)) - | mirror (Eq (C fo)) = Eq (C fo) - | mirror (Eq (Bound fp)) = Eq (Bound fp) - | mirror (Eq (Neg ft)) = Eq (Neg ft) - | mirror (Eq (Add (fu, fv))) = Eq (Add (fu, fv)) - | mirror (Eq (Sub (fw, fx))) = Eq (Sub (fw, fx)) - | mirror (Eq (Mul (fy, fz))) = Eq (Mul (fy, fz)) - | mirror (NEq (C go)) = NEq (C go) - | mirror (NEq (Bound gp)) = NEq (Bound gp) - | mirror (NEq (Neg gt)) = NEq (Neg gt) - | mirror (NEq (Add (gu, gv))) = NEq (Add (gu, gv)) - | mirror (NEq (Sub (gw, gx))) = NEq (Sub (gw, gx)) - | mirror (NEq (Mul (gy, gz))) = NEq (Mul (gy, gz)) - | mirror (Dvd (aa, C ho)) = Dvd (aa, C ho) - | mirror (Dvd (aa, Bound hp)) = Dvd (aa, Bound hp) - | mirror (Dvd (aa, Neg ht)) = Dvd (aa, Neg ht) - | mirror (Dvd (aa, Add (hu, hv))) = Dvd (aa, Add (hu, hv)) - | mirror (Dvd (aa, Sub (hw, hx))) = Dvd (aa, Sub (hw, hx)) - | mirror (Dvd (aa, Mul (hy, hz))) = Dvd (aa, Mul (hy, hz)) - | mirror (NDvd (ac, C io)) = NDvd (ac, C io) - | mirror (NDvd (ac, Bound ip)) = NDvd (ac, Bound ip) - | mirror (NDvd (ac, Neg it)) = NDvd (ac, Neg it) - | mirror (NDvd (ac, Add (iu, iv))) = NDvd (ac, Add (iu, iv)) - | mirror (NDvd (ac, Sub (iw, ix))) = NDvd (ac, Sub (iw, ix)) - | mirror (NDvd (ac, Mul (iy, iz))) = NDvd (ac, Mul (iy, iz)) - | mirror (NOT ae) = NOT ae - | mirror (Imp (aj, ak)) = Imp (aj, ak) - | mirror (Iff (al, am)) = Iff (al, am) - | mirror (E an) = E an - | mirror (A ao) = A ao - | mirror (Closed ap) = Closed ap - | mirror (NClosed aq) = NClosed aq - | mirror (Lt (CN (cm, c, e))) = - (if equal_nat cm zero_nat then Gt (CN (zero_nat, c, Neg e)) - else Lt (CN (suc (minus_nat cm one_nat), c, e))) - | mirror (Le (CN (dm, c, e))) = - (if equal_nat dm zero_nat then Ge (CN (zero_nat, c, Neg e)) - else Le (CN (suc (minus_nat dm one_nat), c, e))) - | mirror (Gt (CN (em, c, e))) = - (if equal_nat em zero_nat then Lt (CN (zero_nat, c, Neg e)) - else Gt (CN (suc (minus_nat em one_nat), c, e))) - | mirror (Ge (CN (fm, c, e))) = - (if equal_nat fm zero_nat then Le (CN (zero_nat, c, Neg e)) - else Ge (CN (suc (minus_nat fm one_nat), c, e))) - | mirror (Eq (CN (gm, c, e))) = - (if equal_nat gm zero_nat then Eq (CN (zero_nat, c, Neg e)) - else Eq (CN (suc (minus_nat gm one_nat), c, e))) - | mirror (NEq (CN (hm, c, e))) = - (if equal_nat hm zero_nat then NEq (CN (zero_nat, c, Neg e)) - else NEq (CN (suc (minus_nat hm one_nat), c, e))) - | mirror (Dvd (i, CN (im, c, e))) = - (if equal_nat im zero_nat then Dvd (i, CN (zero_nat, c, Neg e)) - else Dvd (i, CN (suc (minus_nat im one_nat), c, e))) - | mirror (NDvd (i, CN (jm, c, e))) = - (if equal_nat jm zero_nat then NDvd (i, CN (zero_nat, c, Neg e)) - else NDvd (i, CN (suc (minus_nat jm one_nat), c, e))); + | mirror (Lt (C va)) = Lt (C va) + | mirror (Lt (Bound va)) = Lt (Bound va) + | mirror (Lt (Neg va)) = Lt (Neg va) + | mirror (Lt (Add (va, vb))) = Lt (Add (va, vb)) + | mirror (Lt (Sub (va, vb))) = Lt (Sub (va, vb)) + | mirror (Lt (Mul (va, vb))) = Lt (Mul (va, vb)) + | mirror (Le (C va)) = Le (C va) + | mirror (Le (Bound va)) = Le (Bound va) + | mirror (Le (Neg va)) = Le (Neg va) + | mirror (Le (Add (va, vb))) = Le (Add (va, vb)) + | mirror (Le (Sub (va, vb))) = Le (Sub (va, vb)) + | mirror (Le (Mul (va, vb))) = Le (Mul (va, vb)) + | mirror (Gt (C va)) = Gt (C va) + | mirror (Gt (Bound va)) = Gt (Bound va) + | mirror (Gt (Neg va)) = Gt (Neg va) + | mirror (Gt (Add (va, vb))) = Gt (Add (va, vb)) + | mirror (Gt (Sub (va, vb))) = Gt (Sub (va, vb)) + | mirror (Gt (Mul (va, vb))) = Gt (Mul (va, vb)) + | mirror (Ge (C va)) = Ge (C va) + | mirror (Ge (Bound va)) = Ge (Bound va) + | mirror (Ge (Neg va)) = Ge (Neg va) + | mirror (Ge (Add (va, vb))) = Ge (Add (va, vb)) + | mirror (Ge (Sub (va, vb))) = Ge (Sub (va, vb)) + | mirror (Ge (Mul (va, vb))) = Ge (Mul (va, vb)) + | mirror (Eq (C va)) = Eq (C va) + | mirror (Eq (Bound va)) = Eq (Bound va) + | mirror (Eq (Neg va)) = Eq (Neg va) + | mirror (Eq (Add (va, vb))) = Eq (Add (va, vb)) + | mirror (Eq (Sub (va, vb))) = Eq (Sub (va, vb)) + | mirror (Eq (Mul (va, vb))) = Eq (Mul (va, vb)) + | mirror (NEq (C va)) = NEq (C va) + | mirror (NEq (Bound va)) = NEq (Bound va) + | mirror (NEq (Neg va)) = NEq (Neg va) + | mirror (NEq (Add (va, vb))) = NEq (Add (va, vb)) + | mirror (NEq (Sub (va, vb))) = NEq (Sub (va, vb)) + | mirror (NEq (Mul (va, vb))) = NEq (Mul (va, vb)) + | mirror (Dvd (v, C vb)) = Dvd (v, C vb) + | mirror (Dvd (v, Bound vb)) = Dvd (v, Bound vb) + | mirror (Dvd (v, Neg vb)) = Dvd (v, Neg vb) + | mirror (Dvd (v, Add (vb, vc))) = Dvd (v, Add (vb, vc)) + | mirror (Dvd (v, Sub (vb, vc))) = Dvd (v, Sub (vb, vc)) + | mirror (Dvd (v, Mul (vb, vc))) = Dvd (v, Mul (vb, vc)) + | mirror (NDvd (v, C vb)) = NDvd (v, C vb) + | mirror (NDvd (v, Bound vb)) = NDvd (v, Bound vb) + | mirror (NDvd (v, Neg vb)) = NDvd (v, Neg vb) + | 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 (Imp (v, va)) = Imp (v, va) + | mirror (Iff (v, va)) = Iff (v, va) + | mirror (E v) = E v + | mirror (A v) = A v + | mirror (Closed v) = Closed v + | mirror (NClosed v) = NClosed v + | mirror (Lt (CN (vd, c, e))) = + (if equal_nat vd zero_nat then Gt (CN (zero_nat, c, Neg e)) + else Lt (CN (suc (minus_nat vd one_nat), c, e))) + | mirror (Le (CN (vd, c, e))) = + (if equal_nat vd zero_nat then Ge (CN (zero_nat, c, Neg e)) + else Le (CN (suc (minus_nat vd one_nat), c, e))) + | mirror (Gt (CN (vd, c, e))) = + (if equal_nat vd zero_nat then Lt (CN (zero_nat, c, Neg e)) + else Gt (CN (suc (minus_nat vd one_nat), c, e))) + | mirror (Ge (CN (vd, c, e))) = + (if equal_nat vd zero_nat then Le (CN (zero_nat, c, Neg e)) + else Ge (CN (suc (minus_nat vd one_nat), c, e))) + | mirror (Eq (CN (vd, c, e))) = + (if equal_nat vd zero_nat then Eq (CN (zero_nat, c, Neg e)) + else Eq (CN (suc (minus_nat vd one_nat), c, e))) + | mirror (NEq (CN (vd, c, e))) = + (if equal_nat vd zero_nat then NEq (CN (zero_nat, c, Neg e)) + else NEq (CN (suc (minus_nat vd one_nat), c, e))) + | mirror (Dvd (i, CN (ve, c, e))) = + (if equal_nat ve zero_nat then Dvd (i, CN (zero_nat, c, Neg e)) + else Dvd (i, CN (suc (minus_nat ve one_nat), c, e))) + | mirror (NDvd (i, CN (ve, c, e))) = + (if equal_nat ve zero_nat then NDvd (i, CN (zero_nat, c, Neg e)) + else NDvd (i, CN (suc (minus_nat ve one_nat), c, e))); fun member A_ [] y = false | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y; @@ -1813,7 +1805,7 @@ fun zsplit0 (C c) = (zero_inta, C c) | zsplit0 (Bound n) = - (if equal_nat n zero_nat then (Int_of_integer (1 : IntInf.int), C zero_inta) + (if equal_nat n zero_nat then (one_inta, C zero_inta) else (zero_inta, Bound n)) | zsplit0 (CN (n, i, a)) = let @@ -1823,38 +1815,34 @@ (if equal_nat n zero_nat then (plus_inta i ia, ab) else (ia, CN (n, i, ab))) end - | zsplit0 (Neg a) = - let - val aa = zsplit0 a; - val (i, ab) = aa; - in - (uminus_int i, Neg ab) - end - | zsplit0 (Add (a, b)) = - let - val aa = zsplit0 a; - val (ia, ab) = aa; - val ba = zsplit0 b; - val (ib, bb) = ba; - in - (plus_inta ia ib, Add (ab, bb)) - end - | zsplit0 (Sub (a, b)) = - let - val aa = zsplit0 a; - val (ia, ab) = aa; - val ba = zsplit0 b; - val (ib, bb) = ba; - in - (minus_inta ia ib, Sub (ab, bb)) - end - | zsplit0 (Mul (i, a)) = - let - val aa = zsplit0 a; - val (ia, ab) = aa; - in - (times_inta i ia, Mul (i, ab)) - end; + | zsplit0 (Neg a) = let + val aa = zsplit0 a; + val (i, ab) = aa; + in + (uminus_int i, Neg ab) + end + | zsplit0 (Add (a, b)) = let + val aa = zsplit0 a; + val (ia, ab) = aa; + val ba = zsplit0 b; + val (ib, bb) = ba; + in + (plus_inta ia ib, Add (ab, bb)) + end + | zsplit0 (Sub (a, b)) = let + val aa = zsplit0 a; + val (ia, ab) = aa; + val ba = zsplit0 b; + val (ib, bb) = ba; + in + (minus_inta ia ib, Sub (ab, bb)) + end + | zsplit0 (Mul (i, a)) = let + val aa = zsplit0 a; + val (ia, ab) = aa; + in + (times_inta i ia, Mul (i, ab)) + end; fun zlfm (And (p, q)) = And (zlfm p, zlfm q) | zlfm (Or (p, q)) = Or (zlfm p, zlfm q) @@ -1950,20 +1938,18 @@ | zlfm (NOT (NClosed p)) = Closed p | zlfm T = T | zlfm F = F - | zlfm (NOT (E ci)) = NOT (E ci) - | zlfm (NOT (A cj)) = NOT (A cj) - | zlfm (E ao) = E ao - | zlfm (A ap) = A ap - | zlfm (Closed aq) = Closed aq - | zlfm (NClosed ar) = NClosed ar; + | 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 + | zlfm (NClosed v) = NClosed v; fun unita p = let val pa = zlfm p; val l = zeta pa; - val q = - And (Dvd (l, CN (zero_nat, Int_of_integer (1 : IntInf.int), C zero_inta)), - a_beta pa l); + val q = And (Dvd (l, CN (zero_nat, one_inta, C zero_inta)), a_beta pa l); val d = delta q; val b = remdups equal_num (map simpnum (beta q)); val a = remdups equal_num (map simpnum (alpha q)); @@ -2001,8 +1987,7 @@ | decr (NClosed v) = NClosed v; fun upto_aux i j js = - (if less_int j i then js - else upto_aux i (minus_inta j (Int_of_integer (1 : IntInf.int))) (j :: js)); + (if less_int j i then js else upto_aux i (minus_inta j one_inta) (j :: js)); fun uptoa i j = upto_aux i j []; @@ -2012,7 +1997,7 @@ fun cooper p = let val (q, (b, d)) = unita p; - val js = uptoa (Int_of_integer (1 : IntInf.int)) d; + val js = uptoa one_inta d; val mq = simpfm (minusinf q); val md = evaldjf (fn j => simpfm (subst0 (C j) mq)) js; in @@ -2056,54 +2041,54 @@ | 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 ef)) = E (prep (Lt ef)) - | prep (E (Le eg)) = E (prep (Le eg)) - | prep (E (Gt eh)) = E (prep (Gt eh)) - | prep (E (Ge ei)) = E (prep (Ge ei)) - | prep (E (Eq ej)) = E (prep (Eq ej)) - | prep (E (NEq ek)) = E (prep (NEq ek)) - | prep (E (Dvd (el, em))) = E (prep (Dvd (el, em))) - | prep (E (NDvd (en, eo))) = E (prep (NDvd (en, eo))) + | prep (E (Lt v)) = E (prep (Lt v)) + | prep (E (Le v)) = E (prep (Le v)) + | prep (E (Gt v)) = E (prep (Gt v)) + | prep (E (Ge v)) = E (prep (Ge v)) + | prep (E (Eq v)) = E (prep (Eq v)) + | 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 gw))) = E (prep (NOT (Lt gw))) - | prep (E (NOT (Le gx))) = E (prep (NOT (Le gx))) - | prep (E (NOT (Gt gy))) = E (prep (NOT (Gt gy))) - | prep (E (NOT (Ge gz))) = E (prep (NOT (Ge gz))) - | prep (E (NOT (Eq ha))) = E (prep (NOT (Eq ha))) - | prep (E (NOT (NEq hb))) = E (prep (NOT (NEq hb))) - | prep (E (NOT (Dvd (hc, hd)))) = E (prep (NOT (Dvd (hc, hd)))) - | prep (E (NOT (NDvd (he, hf)))) = E (prep (NOT (NDvd (he, hf)))) - | prep (E (NOT (NOT hg))) = E (prep (NOT (NOT hg))) - | prep (E (NOT (Or (hj, hk)))) = E (prep (NOT (Or (hj, hk)))) - | prep (E (NOT (E hp))) = E (prep (NOT (E hp))) - | prep (E (NOT (A hq))) = E (prep (NOT (A hq))) - | prep (E (NOT (Closed hr))) = E (prep (NOT (Closed hr))) - | prep (E (NOT (NClosed hs))) = E (prep (NOT (NClosed hs))) - | prep (E (And (eq, er))) = E (prep (And (eq, er))) - | prep (E (E ey)) = E (prep (E ey)) - | prep (E (A ez)) = E (prep (A ez)) - | prep (E (Closed fa)) = E (prep (Closed fa)) - | prep (E (NClosed fb)) = E (prep (NClosed fb)) + | 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 jn)) = prep (NOT (E (NOT (Lt jn)))) - | prep (A (Le jo)) = prep (NOT (E (NOT (Le jo)))) - | prep (A (Gt jp)) = prep (NOT (E (NOT (Gt jp)))) - | prep (A (Ge jq)) = prep (NOT (E (NOT (Ge jq)))) - | prep (A (Eq jr)) = prep (NOT (E (NOT (Eq jr)))) - | prep (A (NEq js)) = prep (NOT (E (NOT (NEq js)))) - | prep (A (Dvd (jt, ju))) = prep (NOT (E (NOT (Dvd (jt, ju))))) - | prep (A (NDvd (jv, jw))) = prep (NOT (E (NOT (NDvd (jv, jw))))) - | prep (A (NOT jx)) = prep (NOT (E (NOT (NOT jx)))) - | prep (A (Or (ka, kb))) = prep (NOT (E (NOT (Or (ka, kb))))) - | prep (A (Imp (kc, kd))) = prep (NOT (E (NOT (Imp (kc, kd))))) - | prep (A (Iff (ke, kf))) = prep (NOT (E (NOT (Iff (ke, kf))))) - | prep (A (E kg)) = prep (NOT (E (NOT (E kg)))) - | prep (A (A kh)) = prep (NOT (E (NOT (A kh)))) - | prep (A (Closed ki)) = prep (NOT (E (NOT (Closed ki)))) - | prep (A (NClosed kj)) = prep (NOT (E (NOT (NClosed kj)))) + | 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)) @@ -2112,33 +2097,33 @@ | 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 bo)) = NOT (prep (Lt bo)) - | prep (NOT (Le bp)) = NOT (prep (Le bp)) - | prep (NOT (Gt bq)) = NOT (prep (Gt bq)) - | prep (NOT (Ge br)) = NOT (prep (Ge br)) - | prep (NOT (Eq bs)) = NOT (prep (Eq bs)) - | prep (NOT (NEq bt)) = NOT (prep (NEq bt)) - | prep (NOT (Dvd (bu, bv))) = NOT (prep (Dvd (bu, bv))) - | prep (NOT (NDvd (bw, bx))) = NOT (prep (NDvd (bw, bx))) - | prep (NOT (E ch)) = NOT (prep (E ch)) - | prep (NOT (Closed cj)) = NOT (prep (Closed cj)) - | prep (NOT (NClosed ck)) = NOT (prep (NClosed ck)) + | 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 T = T | prep F = F - | prep (Lt u) = Lt u + | prep (Lt v) = Lt v | prep (Le v) = Le v - | prep (Gt w) = Gt w - | prep (Ge x) = Ge x - | prep (Eq y) = Eq y - | prep (NEq z) = NEq z - | prep (Dvd (aa, ab)) = Dvd (aa, ab) - | prep (NDvd (ac, ad)) = NDvd (ac, ad) - | prep (Closed ap) = Closed ap - | prep (NClosed aq) = NClosed aq; + | prep (Gt v) = Gt v + | prep (Ge v) = Ge v + | prep (Eq v) = Eq v + | prep (NEq v) = NEq v + | prep (Dvd (v, va)) = Dvd (v, va) + | prep (NDvd (v, va)) = NDvd (v, va) + | prep (Closed v) = Closed v + | prep (NClosed v) = NClosed v; fun pa p = qelim (prep p) cooper;