author chaieb Thu, 26 Jul 2007 21:49:53 +0200 changeset 23995 c34490f1e0ff parent 23994 3ddc90d1eda1 child 23996 306aba3e5118
Updated proofs; changed shadow syntax to improve (processing) time
```--- a/src/HOL/ex/Reflected_Presburger.thy	Thu Jul 26 21:49:51 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Thu Jul 26 21:49:53 2007 +0200
@@ -19,7 +19,7 @@
(****                            SHADOW SYNTAX AND SEMANTICS                  ****)
(*********************************************************************************)

-datatype num = C int | Bound nat | CX int num | Neg num | Add num num| Sub num num
+datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
| Mul int num

(* A size for num to make inductive proofs simpler*)
@@ -30,14 +30,14 @@
"num_size (Neg a) = 1 + num_size a"
"num_size (Add a b) = 1 + num_size a + num_size b"
"num_size (Sub a b) = 3 + num_size a + num_size b"
-  "num_size (CX c a) = 4 + num_size a"
+  "num_size (CN n c a) = 4 + num_size a"
"num_size (Mul c a) = 1 + num_size a"

consts Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
primrec
"Inum bs (C c) = c"
"Inum bs (Bound n) = bs!n"
-  "Inum bs (CX c a) = c * (bs!0) + (Inum bs a)"
+  "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
"Inum bs (Neg a) = -(Inum bs a)"
"Inum bs (Add a b) = Inum bs a + Inum bs b"
"Inum bs (Sub a b) = Inum bs a - Inum bs b"
@@ -89,10 +89,6 @@
"Ifm bbs bs (Closed n) = bbs!n"
"Ifm bbs bs (NClosed n) = (\<not> bbs!n)"

-lemma "Ifm bbs [] (A(Imp (Gt (Sub (Bound 0) (C 8))) (E(E(Eq(Sub(Add (Mul 3 (Bound 0)) (Mul 5 (Bound 1))) (Bound 2))))))) = P"
-apply simp
-oops
-
consts prep :: "fm \<Rightarrow> fm"
recdef prep "measure fmsize"
"prep (E T) = T"
@@ -139,12 +135,11 @@
consts
numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
-  numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *)
subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
primrec
"numbound0 (C c) = True"
"numbound0 (Bound n) = (n>0)"
-  "numbound0 (CX i a) = False"
+  "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
"numbound0 (Neg a) = numbound0 a"
"numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
"numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
@@ -182,24 +177,25 @@
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
by (induct p rule: bound0.induct) (auto simp add: gr0_conv_Suc)

-primrec
+fun   numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
"numsubst0 t (C c) = (C c)"
-  "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
-  "numsubst0 t (CX i a) = Add (Mul i t) (numsubst0 t a)"
-  "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
-  "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
-  "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
-  "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
+| "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
+| "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
+| "numsubst0 t (CN n i a) = CN n i (numsubst0 t a)"
+| "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
+| "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
+| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
+| "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"

lemma numsubst0_I:
shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
-  by (induct t) (auto simp add: gr0_conv_Suc)
+  by (induct t rule: numsubst0.induct,auto simp add: gr0_conv_Suc)

lemma numsubst0_I':
assumes nb: "numbound0 a"
shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
-  by (induct t) (auto simp add: gr0_conv_Suc numbound0_I[OF nb, where b="b" and b'="b'"])
-
+  using nb
+  by (induct t rule: numsubst0.induct, auto simp add: gr0_conv_Suc numbound0_I[where b="b" and b'="b'"])

primrec
"subst0 t T = T"
@@ -236,6 +232,7 @@
"decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
"decrnum (Mul c a) = Mul c (decrnum a)"
+  "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))"
"decrnum a = a"

recdef decr "measure size"
@@ -285,7 +282,10 @@

lemma numsubst0_numbound0: assumes nb: "numbound0 t"
shows "numbound0 (numsubst0 t a)"
-using nb by (induct a rule: numsubst0.induct, auto)
+using nb apply (induct a rule: numbound0.induct)
+apply simp_all
+apply (case_tac n, simp_all)
+done

lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
shows "bound0 (subst0 t p)"
@@ -387,7 +387,7 @@
lex_ns:: "nat list \<times> nat list \<Rightarrow> bool"
recdef bnds "measure size"
"bnds (Bound n) = [n]"
-  "bnds (CX c a) = 0#(bnds a)"
+  "bnds (CN n c a) = n#(bnds a)"
"bnds (Neg a) = bnds a"
"bnds (Add a b) = (bnds a)@(bnds b)"
"bnds (Sub a b) = (bnds a)@(bnds b)"
@@ -402,15 +402,15 @@

consts
numadd:: "num \<times> num \<Rightarrow> num"
-recdef numadd "measure (\<lambda> (t,s). size t + size s)"
+recdef numadd "measure (\<lambda> (t,s). num_size t + num_size s)"
+  "numadd (CN n1 c1 r1 ,CN n2 c2 r2) =
(if n1=n2 then
(let c = c1 + c2
-  else if n1 \<le> n2 then (Add (Mul c1 (Bound n1)) (numadd (r1,Add (Mul c2 (Bound n2)) r2)))
+  in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2))))
+  else if n1 \<le> n2 then CN n1 c1 (numadd (r1,Add (Mul c2 (Bound n2)) r2))
+  else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1,r2)))"
+  "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
+  "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))"
"numadd (C b1, C b2) = C (b1+b2)"

@@ -448,8 +448,7 @@
nummul :: "int \<Rightarrow> num \<Rightarrow> num"
where
"nummul i (C j) = C (i * j)"
-  | "nummul i (Add a b) = numadd (nummul i a, nummul i b)"
-  | "nummul i (Mul c t) = nummul (i * c) t"
+  | "nummul i (CN n c t) = CN n (c*i) (nummul i t)"
| "nummul i t = Mul i t"

lemma nummul: "\<And> i. Inum bs (nummul i t) = Inum bs (Mul i t)"
@@ -480,7 +479,7 @@
simpnum :: "num \<Rightarrow> num"
where
"simpnum (C j) = C j"
-  | "simpnum (Bound n) = Add (Mul 1 (Bound n)) (C 0)"
+  | "simpnum (Bound n) = CN n 1 (C 0)"
| "simpnum (Neg t) = numneg (simpnum t)"
| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
@@ -737,7 +736,9 @@
where
"zsplit0 (C c) = (0,C c)"
| "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
-  | "zsplit0 (CX i a) = (let (i',a') =  zsplit0 a in (i+i', a'))"
+  | "zsplit0 (CN n i a) =
+      (let (i',a') =  zsplit0 a
+       in if n=0 then (i+i', a') else (i',CN n i a'))"
| "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
| "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ;
(ib,b') =  zsplit0 b
@@ -748,30 +749,36 @@
| "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"

lemma zsplit0_I:
-  shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CX n a) = Inum (x #bs) t) \<and> numbound0 a"
-  (is "\<And> n a. ?S t = (n,a) \<Longrightarrow> (?I x (CX n a) = ?I x t) \<and> ?N a")
+  shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a"
+  (is "\<And> n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
proof(induct t rule: zsplit0.induct)
case (1 c n a) thus ?case by auto
next
case (2 m n a) thus ?case by (cases "m=0") auto
next
-  case (3 i a n a')
+  case (3 m i a n a')
let ?j = "fst (zsplit0 a)"
let ?b = "snd (zsplit0 a)"
-  have abj: "zsplit0 a = (?j,?b)" by simp hence th: "a'=?b \<and> n=i+?j" using prems
-    by (simp add: Let_def split_def)
-  from abj prems  have th2: "(?I x (CX ?j ?b) = ?I x a) \<and> ?N ?b" by blast
-  from th have "?I x (CX n a') = ?I x (CX (i+?j) ?b)" by simp
-  also from th2 have "\<dots> = ?I x (CX i (CX ?j ?b))" by (simp add: left_distrib)
-  finally have "?I x (CX n a') = ?I  x (CX i a)" using th2 by simp
-  with th2 th show ?case by blast
+  have abj: "zsplit0 a = (?j,?b)" by simp
+  {assume "m\<noteq>0"
+    with prems(1)[OF abj] prems(2) have ?case by (auto simp add: Let_def split_def)}
+  moreover
+  {assume m0: "m =0"
+    from abj have th: "a'=?b \<and> n=i+?j" using prems
+      by (simp add: Let_def split_def)
+    from abj prems  have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
+    from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
+    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
+  finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
+  with th2 th have ?case using m0 by blast}
+ultimately show ?case by blast
next
case (4 t n a)
let ?nt = "fst (zsplit0 t)"
let ?at = "snd (zsplit0 t)"
have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems
-  from abj prems  have th2: "(?I x (CX ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
+  from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
from th2[simplified] th[simplified] show ?case by simp
next
case (5 s t n a)
@@ -784,9 +791,9 @@
ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems
from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
-  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CX xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
-  with bluddy abjt have th3: "(?I x (CX ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
-  from abjs prems  have th2: "(?I x (CX ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
+  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
+  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
+  from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
from th3[simplified] th2[simplified] th[simplified] show ?case
next
@@ -800,9 +807,9 @@
ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems
from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
-  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CX xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
-  with bluddy abjt have th3: "(?I x (CX ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
-  from abjs prems  have th2: "(?I x (CX ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
+  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
+  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
+  from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
from th3[simplified] th2[simplified] th[simplified] show ?case
next
@@ -811,9 +818,9 @@
let ?at = "snd (zsplit0 t)"
have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems
-  from abj prems  have th2: "(?I x (CX ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
-  hence " ?I x (Mul i t) = i * ?I x (CX ?nt ?at)" by simp
-  also have "\<dots> = ?I x (CX (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
+  from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
+  hence " ?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
+  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
finally show ?case using th th2 by simp
qed

@@ -822,15 +829,15 @@
recdef iszlfm "measure size"
"iszlfm (And p q) = (iszlfm p \<and> iszlfm q)"
"iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)"
-  "iszlfm (Eq  (CX c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (NEq (CX c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (Lt  (CX c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (Le  (CX c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (Gt  (CX c e)) = (c>0 \<and> numbound0 e)"
-  "iszlfm (Ge  (CX c e)) = ( c>0 \<and> numbound0 e)"
-  "iszlfm (Dvd i (CX c e)) =
+  "iszlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+  "iszlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+  "iszlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+  "iszlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+  "iszlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
+  "iszlfm (Ge  (CN 0 c e)) = ( c>0 \<and> numbound0 e)"
+  "iszlfm (Dvd i (CN 0 c e)) =
(c>0 \<and> i>0 \<and> numbound0 e)"
-  "iszlfm (NDvd i (CX c e))=
+  "iszlfm (NDvd i (CN 0 c e))=
(c>0 \<and> i>0 \<and> numbound0 e)"
"iszlfm p = (isatom p \<and> (bound0 p))"

@@ -846,32 +853,32 @@
"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 (CX c r)) else (Gt (CX (- c) (Neg r))))"
+     if c>0 then (Lt (CN 0 c r)) else (Gt (CN 0 (- c) (Neg r))))"
"zlfm (Le a) = (let (c,r) = zsplit0 a in
if c=0 then Le r else
-     if c>0 then (Le (CX c r)) else (Ge (CX (- c) (Neg r))))"
+     if c>0 then (Le (CN 0 c r)) else (Ge (CN 0 (- c) (Neg r))))"
"zlfm (Gt a) = (let (c,r) = zsplit0 a in
if c=0 then Gt r else
-     if c>0 then (Gt (CX c r)) else (Lt (CX (- c) (Neg r))))"
+     if c>0 then (Gt (CN 0 c r)) else (Lt (CN 0 (- c) (Neg r))))"
"zlfm (Ge a) = (let (c,r) = zsplit0 a in
if c=0 then Ge r else
-     if c>0 then (Ge (CX c r)) else (Le (CX (- c) (Neg r))))"
+     if c>0 then (Ge (CN 0 c r)) else (Le (CN 0 (- c) (Neg r))))"
"zlfm (Eq a) = (let (c,r) = zsplit0 a in
if c=0 then Eq r else
-     if c>0 then (Eq (CX c r)) else (Eq (CX (- c) (Neg r))))"
+     if c>0 then (Eq (CN 0 c r)) else (Eq (CN 0 (- c) (Neg r))))"
"zlfm (NEq a) = (let (c,r) = zsplit0 a in
if c=0 then NEq r else
-     if c>0 then (NEq (CX c r)) else (NEq (CX (- c) (Neg r))))"
+     if c>0 then (NEq (CN 0 c r)) else (NEq (CN 0 (- c) (Neg r))))"
"zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
else (let (c,r) = zsplit0 a in
if c=0 then (Dvd (abs i) r) else
-      if c>0 then (Dvd (abs i) (CX c r))
-      else (Dvd (abs i) (CX (- c) (Neg r)))))"
+      if c>0 then (Dvd (abs i) (CN 0 c r))
+      else (Dvd (abs i) (CN 0 (- c) (Neg r)))))"
"zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
else (let (c,r) = zsplit0 a in
if c=0 then (NDvd (abs i) r) else
-      if c>0 then (NDvd (abs i) (CX c r))
-      else (NDvd (abs i) (CX (- c) (Neg r)))))"
+      if c>0 then (NDvd (abs i) (CN 0 c r))
+      else (NDvd (abs 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))"
@@ -902,67 +909,85 @@
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)" by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
+  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb  show ?case
-    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
+    apply (auto simp add: Let_def split_def ring_simps)
+    apply (cases "?r",auto)
+    apply (case_tac nat, auto)
+    done
next
case (6 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)" by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
+  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb  show ?case
-    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
+    apply (auto simp add: Let_def split_def ring_simps)
+    apply (cases "?r",auto)
+    apply (case_tac nat, auto)
+    done
next
case (7 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)" by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
+  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb  show ?case
-    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
+    apply (auto simp add: Let_def split_def ring_simps)
+    apply (cases "?r",auto)
+    apply (case_tac nat, auto)
+    done
next
case (8 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)" by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
+  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb  show ?case
-    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
+    apply (auto simp add: Let_def split_def ring_simps)
+    apply (cases "?r",auto)
+    apply (case_tac nat, auto)
+    done
next
case (9 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)" by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
+  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb  show ?case
-    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
+    apply (auto simp add: Let_def split_def ring_simps)
+    apply (cases "?r",auto)
+    apply (case_tac nat, auto)
+    done
next
case (10 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)" by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
+  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
from prems Ia nb  show ?case
-    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
+    apply (auto simp add: Let_def split_def ring_simps)
+    apply (cases "?r",auto)
+    apply (case_tac nat, auto)
+    done
next
case (11 j a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)" by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
+  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
moreover
@@ -970,19 +995,22 @@
hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
-      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where d="j"]
-      by (cases "?r", simp_all add: Let_def split_def)}
+      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
+    apply (auto simp add: Let_def split_def ring_simps)
+    apply (cases "?r",auto)
+    apply (case_tac nat, auto)
+    done}
moreover
{assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
hence ?case using Ia cp jnz by (simp add: Let_def split_def
-	zdvd_abs1[where d="j" and t="(?c*i) + ?N ?r", symmetric])}
+	zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
moreover
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
-      zdvd_abs1[where d="j" and t="(?c*i) + ?N ?r", symmetric])}
+      zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
ultimately show ?case by blast
next
case (12 j a)
@@ -990,7 +1018,7 @@
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)" by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
-  have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto
+  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
let ?N = "\<lambda> t. Inum (i#bs) t"
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
moreover
@@ -998,19 +1026,22 @@
hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
-      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where d="j"]
-      by (cases "?r", simp_all add: Let_def split_def)}
+      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
+    apply (auto simp add: Let_def split_def ring_simps)
+    apply (cases "?r",auto)
+    apply (case_tac nat, auto)
+    done}
moreover
{assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
hence ?case using Ia cp jnz by (simp add: Let_def split_def
-	zdvd_abs1[where d="j" and t="(?c*i) + ?N ?r", symmetric])}
+	zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
moreover
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
-      zdvd_abs1[where d="j" and t="(?c*i) + ?N ?r", symmetric])}
+      zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
ultimately show ?case by blast
qed auto

@@ -1023,12 +1054,12 @@
recdef minusinf "measure size"
"minusinf (And p q) = And (minusinf p) (minusinf q)"
"minusinf (Or p q) = Or (minusinf p) (minusinf q)"
-  "minusinf (Eq  (CX c e)) = F"
-  "minusinf (NEq (CX c e)) = T"
-  "minusinf (Lt  (CX c e)) = T"
-  "minusinf (Le  (CX c e)) = T"
-  "minusinf (Gt  (CX c e)) = F"
-  "minusinf (Ge  (CX c e)) = F"
+  "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 \<Longrightarrow> qfree (minusinf p)"
@@ -1037,26 +1068,26 @@
recdef plusinf "measure size"
"plusinf (And p q) = And (plusinf p) (plusinf q)"
"plusinf (Or p q) = Or (plusinf p) (plusinf q)"
-  "plusinf (Eq  (CX c e)) = F"
-  "plusinf (NEq (CX c e)) = T"
-  "plusinf (Lt  (CX c e)) = F"
-  "plusinf (Le  (CX c e)) = F"
-  "plusinf (Gt  (CX c e)) = T"
-  "plusinf (Ge  (CX c e)) = T"
+  "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"

recdef \<delta> "measure size"
"\<delta> (And p q) = ilcm (\<delta> p) (\<delta> q)"
"\<delta> (Or p q) = ilcm (\<delta> p) (\<delta> q)"
-  "\<delta> (Dvd i (CX c e)) = i"
-  "\<delta> (NDvd i (CX c e)) = i"
+  "\<delta> (Dvd i (CN 0 c e)) = i"
+  "\<delta> (NDvd i (CN 0 c e)) = i"
"\<delta> p = 1"

recdef d\<delta> "measure size"
"d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)"
"d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)"
-  "d\<delta> (Dvd i (CX c e)) = (\<lambda> d. i dvd d)"
-  "d\<delta> (NDvd i (CX c e)) = (\<lambda> d. i dvd d)"
+  "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
+  "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
"d\<delta> p = (\<lambda> d. True)"

lemma delta_mono:
@@ -1080,18 +1111,18 @@
case (1 p q)
let ?d = "\<delta> (And p q)"
from prems ilcm_pos have dp: "?d >0" by simp
-  have d1: "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp
+  have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_ilcm_self1)
-  have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp
+  have "\<delta> q dvd \<delta> (And p q)" using prems by simp
hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2)
from th th' dp show ?case by simp
next
case (2 p q)
let ?d = "\<delta> (And p q)"
from prems ilcm_pos have dp: "?d >0" by simp
-  have "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp
+  have "\<delta> p dvd \<delta> (And p q)" using prems by simp
hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_ilcm_self1)
-  have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp
+  have "\<delta> q dvd \<delta> (And p q)" using prems by simp
hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2)
from th th' dp show ?case by simp
qed simp_all
@@ -1107,75 +1138,75 @@
recdef a\<beta> "measure size"
"a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))"
"a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))"
-  "a\<beta> (Eq  (CX c e)) = (\<lambda> k. Eq (CX 1 (Mul (k div c) e)))"
-  "a\<beta> (NEq (CX c e)) = (\<lambda> k. NEq (CX 1 (Mul (k div c) e)))"
-  "a\<beta> (Lt  (CX c e)) = (\<lambda> k. Lt (CX 1 (Mul (k div c) e)))"
-  "a\<beta> (Le  (CX c e)) = (\<lambda> k. Le (CX 1 (Mul (k div c) e)))"
-  "a\<beta> (Gt  (CX c e)) = (\<lambda> k. Gt (CX 1 (Mul (k div c) e)))"
-  "a\<beta> (Ge  (CX c e)) = (\<lambda> k. Ge (CX 1 (Mul (k div c) e)))"
-  "a\<beta> (Dvd i (CX c e)) =(\<lambda> k. Dvd ((k div c)*i) (CX 1 (Mul (k div c) e)))"
-  "a\<beta> (NDvd i (CX c e))=(\<lambda> k. NDvd ((k div c)*i) (CX 1 (Mul (k div c) e)))"
+  "a\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
+  "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
+  "a\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
+  "a\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
+  "a\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
+  "a\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
+  "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+  "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
"a\<beta> p = (\<lambda> k. p)"

recdef d\<beta> "measure size"
"d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))"
"d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))"
-  "d\<beta> (Eq  (CX c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (NEq (CX c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Lt  (CX c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Le  (CX c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Gt  (CX c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Ge  (CX c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Dvd i (CX c e)) =(\<lambda> k. c dvd k)"
-  "d\<beta> (NDvd i (CX c e))=(\<lambda> k. c dvd k)"
+  "d\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
+  "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
"d\<beta> p = (\<lambda> k. True)"

recdef \<zeta> "measure size"
"\<zeta> (And p q) = ilcm (\<zeta> p) (\<zeta> q)"
"\<zeta> (Or p q) = ilcm (\<zeta> p) (\<zeta> q)"
-  "\<zeta> (Eq  (CX c e)) = c"
-  "\<zeta> (NEq (CX c e)) = c"
-  "\<zeta> (Lt  (CX c e)) = c"
-  "\<zeta> (Le  (CX c e)) = c"
-  "\<zeta> (Gt  (CX c e)) = c"
-  "\<zeta> (Ge  (CX c e)) = c"
-  "\<zeta> (Dvd i (CX c e)) = c"
-  "\<zeta> (NDvd i (CX c e))= c"
+  "\<zeta> (Eq  (CN 0 c e)) = c"
+  "\<zeta> (NEq (CN 0 c e)) = c"
+  "\<zeta> (Lt  (CN 0 c e)) = c"
+  "\<zeta> (Le  (CN 0 c e)) = c"
+  "\<zeta> (Gt  (CN 0 c e)) = c"
+  "\<zeta> (Ge  (CN 0 c e)) = c"
+  "\<zeta> (Dvd i (CN 0 c e)) = c"
+  "\<zeta> (NDvd i (CN 0 c e))= c"
"\<zeta> p = 1"

recdef \<beta> "measure size"
"\<beta> (And p q) = (\<beta> p @ \<beta> q)"
"\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
-  "\<beta> (Eq  (CX c e)) = [Sub (C -1) e]"
-  "\<beta> (NEq (CX c e)) = [Neg e]"
-  "\<beta> (Lt  (CX c e)) = []"
-  "\<beta> (Le  (CX c e)) = []"
-  "\<beta> (Gt  (CX c e)) = [Neg e]"
-  "\<beta> (Ge  (CX c e)) = [Sub (C -1) e]"
+  "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
+  "\<beta> (NEq (CN 0 c e)) = [Neg e]"
+  "\<beta> (Lt  (CN 0 c e)) = []"
+  "\<beta> (Le  (CN 0 c e)) = []"
+  "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
+  "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
"\<beta> p = []"

recdef \<alpha> "measure size"
"\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)"
"\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
-  "\<alpha> (Eq  (CX c e)) = [Add (C -1) e]"
-  "\<alpha> (NEq (CX c e)) = [e]"
-  "\<alpha> (Lt  (CX c e)) = [e]"
-  "\<alpha> (Le  (CX c e)) = [Add (C -1) e]"
-  "\<alpha> (Gt  (CX c e)) = []"
-  "\<alpha> (Ge  (CX c e)) = []"
+  "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
+  "\<alpha> (NEq (CN 0 c e)) = [e]"
+  "\<alpha> (Lt  (CN 0 c e)) = [e]"
+  "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
+  "\<alpha> (Gt  (CN 0 c e)) = []"
+  "\<alpha> (Ge  (CN 0 c e)) = []"
"\<alpha> p = []"
consts mirror :: "fm \<Rightarrow> fm"
recdef mirror "measure size"
"mirror (And p q) = And (mirror p) (mirror q)"
"mirror (Or p q) = Or (mirror p) (mirror q)"
-  "mirror (Eq  (CX c e)) = Eq (CX c (Neg e))"
-  "mirror (NEq (CX c e)) = NEq (CX c (Neg e))"
-  "mirror (Lt  (CX c e)) = Gt (CX c (Neg e))"
-  "mirror (Le  (CX c e)) = Ge (CX c (Neg e))"
-  "mirror (Gt  (CX c e)) = Lt (CX c (Neg e))"
-  "mirror (Ge  (CX c e)) = Le (CX c (Neg e))"
-  "mirror (Dvd i (CX c e)) = Dvd i (CX c (Neg e))"
-  "mirror (NDvd i (CX c e)) = NDvd i (CX c (Neg e))"
+  "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"
(* Lemmas for the correctness of \<sigma>\<rho> *)
lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
@@ -1350,25 +1381,25 @@
using lp
proof(induct p rule: iszlfm.induct)
case (9 j c e) hence nb: "numbound0 e" by simp
-  have "Ifm bbs (x#bs) (mirror (Dvd j (CX c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
+  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
also have "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: zdvd_zminus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
-  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CX c e))"
+  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
by simp
finally show ?case .
next
case (10 j c e) hence nb: "numbound0 e" by simp
-  have "Ifm bbs (x#bs) (mirror (Dvd j (CX c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
+  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
also have "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: zdvd_zminus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
-  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CX c e))"
+  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
by simp
finally show ?case by simp
@@ -1404,19 +1435,15 @@
using linp
proof(induct p rule: iszlfm.induct)
case (1 p q)
-  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)"
-    by (simp add: ilcm_dvd1[where a="\<zeta> p" and b="\<zeta> q"])
-  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)"
-    by (simp add: ilcm_dvd2[where a="\<zeta> p" and b="\<zeta> q"])
+  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)"  by simp
from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
dl1 dl2 show ?case by (auto simp add: ilcm_pos)
next
case (2 p q)
-  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)"
-    by (simp add: ilcm_dvd1[where a="\<zeta> p" and b="\<zeta> q"])
-  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)"
-    by (simp add: ilcm_dvd2[where a="\<zeta> p" and b="\<zeta> q"])
+  from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
+  from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
dl1 dl2 show ?case by (auto simp add: ilcm_pos)
@@ -1599,14 +1626,14 @@
with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
show ?case by simp
next
-  case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CX c e))" and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+  case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
let ?e = "Inum (x # bs) e"
{assume "(x-d) +?e > 0" hence ?case using c1
numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
moreover
{assume H: "\<not> (x-d) + ?e > 0"
let ?v="Neg e"
-      have vb: "?v \<in> set (\<beta> (Gt (CX c e)))" by simp
+      have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e + j)" by auto
from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
@@ -1617,7 +1644,7 @@
with nob have ?case by auto}
ultimately show ?case by blast
next
-  case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CX c e))" and c1: "c=1" and bn:"numbound0 e"
+  case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e"
using dvd1_eq1[where x="c"] by simp+
let ?e = "Inum (x # bs) e"
{assume "(x-d) +?e \<ge> 0" hence ?case using  c1
@@ -1626,7 +1653,7 @@
moreover
{assume H: "\<not> (x-d) + ?e \<ge> 0"
let ?v="Sub (C -1) e"
-      have vb: "?v \<in> set (\<beta> (Ge (CX c e)))" by simp
+      have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e - 1 + j)" by auto
from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
@@ -1636,18 +1663,18 @@
with nob have ?case by simp }
ultimately show ?case by blast
next
-  case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+  case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
let ?e = "Inum (x # bs) e"
let ?v="(Sub (C -1) e)"
-    have vb: "?v \<in> set (\<beta> (Eq (CX c e)))" by simp
+    have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
by simp (erule ballE[where x="1"],
simp_all add:ring_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
next
-  case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+  case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
let ?e = "Inum (x # bs) e"
let ?v="Neg e"
-    have vb: "?v \<in> set (\<beta> (NEq (CX c e)))" by simp
+    have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
{assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
hence ?case by (simp add: c1)}
moreover
@@ -1658,7 +1685,7 @@
with prems(11) have ?case using dp by simp}
ultimately show ?case by blast
next
-  case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+  case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
let ?e = "Inum (x # bs) e"
from prems have id: "j dvd d" by simp
from c1 have "?p x = (j dvd (x+ ?e))" by simp
@@ -1667,7 +1694,7 @@
finally show ?case
using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
next
-  case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+  case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
let ?e = "Inum (x # bs) e"
from prems have id: "j dvd d" by simp
from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp
@@ -1752,7 +1779,7 @@
using cp_thm[OF lp up dd dp,where i="i"] by auto

constdefs unit:: "fm \<Rightarrow> fm \<times> num list \<times> int"
-  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CX 1 (C 0))) (a\<beta> p' l); d = \<delta> q;
+  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a\<beta> p' l); d = \<delta> q;
B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"

@@ -1767,7 +1794,7 @@
let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
let ?p' = "zlfm p"
let ?l = "\<zeta> ?p'"
-  let ?q = "And (Dvd ?l (CX 1 (C 0))) (a\<beta> ?p' ?l)"
+  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\<beta> ?p' ?l)"
let ?d = "\<delta> ?q"
let ?B = "set (\<beta> ?q)"
let ?B'= "remdups (map simpnum (\<beta> ?q))"```