# HG changeset patch # User chaieb # Date 1185479393 -7200 # Node ID c34490f1e0ffad07c2ff6b2ffea3a62bb3d22c8d # Parent 3ddc90d1eda1b9b4048b1c93351a1813a0b35cef Updated proofs; changed shadow syntax to improve (processing) time diff -r 3ddc90d1eda1 -r c34490f1e0ff src/HOL/ex/Reflected_Presburger.thy --- 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 \ num \ 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) = (\ 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 \ fm" recdef prep "measure fmsize" "prep (E T) = T" @@ -139,12 +135,11 @@ consts numbound0:: "num \ bool" (* a num is INDEPENDENT of Bound 0 *) bound0:: "fm \ bool" (* A Formula is independent of Bound 0 *) - numsubst0:: "num \ num \ num" (* substitute a num into a num for Bound 0 *) subst0:: "num \ fm \ 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 \ numbound0 a)" "numbound0 (Neg a) = numbound0 a" "numbound0 (Add a b) = (numbound0 a \ numbound0 b)" "numbound0 (Sub a b) = (numbound0 a \ 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 \ num \ 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 (Add a b) = Add (decrnum a) (decrnum b)" "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 \ nat list \ 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 \ num \ num" -recdef numadd "measure (\ (t,s). size t + size s)" - "numadd (Add (Mul c1 (Bound n1)) r1,Add (Mul c2 (Bound n2)) r2) = +recdef numadd "measure (\ (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 - 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))" + in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2)))) + else if n1 \ 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)" "numadd (a,b) = Add a b" @@ -448,8 +448,7 @@ nummul :: "int \ num \ 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: "\ i. Inum bs (nummul i t) = Inum bs (Mul i t)" @@ -480,7 +479,7 @@ simpnum :: "num \ 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 (Add t s) = numadd (simpnum t, simpnum s)" | "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 "\ n a. zsplit0 t = (n,a) \ (Inum ((x::int) #bs) (CX n a) = Inum (x #bs) t) \ numbound0 a" - (is "\ n a. ?S t = (n,a) \ (?I x (CX n a) = ?I x t) \ ?N a") + shows "\ n a. zsplit0 t = (n,a) \ (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \ numbound0 a" + (is "\ n a. ?S t = (n,a) \ (?I x (CN 0 n a) = ?I x t) \ ?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 \ 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) \ ?N ?b" by blast - from th have "?I x (CX n a') = ?I x (CX (i+?j) ?b)" by simp - also from th2 have "\ = ?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\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 \ 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) \ ?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 "\ = ?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 \ n=-?nt" using prems by (simp add: Let_def split_def) - from abj prems have th2: "(?I x (CX ?nt ?at) = ?I x t) \ ?N ?at" by blast + from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?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 \ n=?ns + ?nt" using prems by (simp add: Let_def split_def) from abjs[symmetric] have bluddy: "\ x y. (x,y) = zsplit0 s" by blast - from prems have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (x # bs) (CX xa xb) = Inum (x # bs) t \ numbound0 xb)" by auto - with bluddy abjt have th3: "(?I x (CX ?nt ?at) = ?I x t) \ ?N ?at" by blast - from abjs prems have th2: "(?I x (CX ?ns ?as) = ?I x s) \ ?N ?as" by blast + from prems have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \ numbound0 xb)" by auto + with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast + from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \ ?N ?as" by blast from th3[simplified] th2[simplified] th[simplified] show ?case by (simp add: left_distrib) next @@ -800,9 +807,9 @@ ultimately have th: "a=Sub ?as ?at \ n=?ns - ?nt" using prems by (simp add: Let_def split_def) from abjs[symmetric] have bluddy: "\ x y. (x,y) = zsplit0 s" by blast - from prems have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (x # bs) (CX xa xb) = Inum (x # bs) t \ numbound0 xb)" by auto - with bluddy abjt have th3: "(?I x (CX ?nt ?at) = ?I x t) \ ?N ?at" by blast - from abjs prems have th2: "(?I x (CX ?ns ?as) = ?I x s) \ ?N ?as" by blast + from prems have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \ numbound0 xb)" by auto + with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast + from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \ ?N ?as" by blast from th3[simplified] th2[simplified] th[simplified] show ?case by (simp add: left_diff_distrib) next @@ -811,9 +818,9 @@ let ?at = "snd (zsplit0 t)" have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \ n=i*?nt" using prems by (simp add: Let_def split_def) - from abj prems have th2: "(?I x (CX ?nt ?at) = ?I x t) \ ?N ?at" by blast - hence " ?I x (Mul i t) = i * ?I x (CX ?nt ?at)" by simp - also have "\ = ?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) \ ?N ?at" by blast + hence " ?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp + also have "\ = ?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 \ iszlfm q)" "iszlfm (Or p q) = (iszlfm p \ iszlfm q)" - "iszlfm (Eq (CX c e)) = (c>0 \ numbound0 e)" - "iszlfm (NEq (CX c e)) = (c>0 \ numbound0 e)" - "iszlfm (Lt (CX c e)) = (c>0 \ numbound0 e)" - "iszlfm (Le (CX c e)) = (c>0 \ numbound0 e)" - "iszlfm (Gt (CX c e)) = (c>0 \ numbound0 e)" - "iszlfm (Ge (CX c e)) = ( c>0 \ numbound0 e)" - "iszlfm (Dvd i (CX c e)) = + "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 (CX c e))= + "iszlfm (NDvd i (CN 0 c e))= (c>0 \ i>0 \ numbound0 e)" "iszlfm p = (isatom p \ (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 = "\ 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 = "\ 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 = "\ 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 = "\ 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 = "\ 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 = "\ 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 = "\ t. Inum (i#bs) t" have "j=0 \ (j\0 \ ?c = 0) \ (j\0 \ ?c >0) \ (j\ 0 \ ?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\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\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\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" ] 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])} 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 = "\ t. Inum (i#bs) t" have "j=0 \ (j\0 \ ?c = 0) \ (j\0 \ ?c >0) \ (j\ 0 \ ?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\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\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\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" ] 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])} 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 \ 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 \ "measure size" "\ (And p q) = ilcm (\ p) (\ q)" "\ (Or p q) = ilcm (\ p) (\ q)" - "\ (Dvd i (CX c e)) = i" - "\ (NDvd i (CX c e)) = i" + "\ (Dvd i (CN 0 c e)) = i" + "\ (NDvd i (CN 0 c e)) = i" "\ p = 1" 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 (CX c e)) = (\ d. i dvd d)" - "d\ (NDvd i (CX c e)) = (\ d. i dvd 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: @@ -1080,18 +1111,18 @@ case (1 p q) let ?d = "\ (And p q)" from prems ilcm_pos have dp: "?d >0" by simp - have d1: "\ p dvd \ (And p q)" using prems ilcm_dvd1 by simp + have d1: "\ p dvd \ (And p q)" using prems by simp hence th: "d\ p ?d" using delta_mono prems(3-4) by(simp del:dvd_ilcm_self1) - have "\ q dvd \ (And p q)" using prems ilcm_dvd2 by simp + have "\ q dvd \ (And p q)" using prems by simp hence th': "d\ 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 = "\ (And p q)" from prems ilcm_pos have dp: "?d >0" by simp - have "\ p dvd \ (And p q)" using prems ilcm_dvd1 by simp + have "\ p dvd \ (And p q)" using prems by simp hence th: "d\ p ?d" using delta_mono prems by(simp del:dvd_ilcm_self1) - have "\ q dvd \ (And p q)" using prems ilcm_dvd2 by simp + have "\ q dvd \ (And p q)" using prems by simp hence th': "d\ 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\ "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 (CX c e)) = (\ k. Eq (CX 1 (Mul (k div c) e)))" - "a\ (NEq (CX c e)) = (\ k. NEq (CX 1 (Mul (k div c) e)))" - "a\ (Lt (CX c e)) = (\ k. Lt (CX 1 (Mul (k div c) e)))" - "a\ (Le (CX c e)) = (\ k. Le (CX 1 (Mul (k div c) e)))" - "a\ (Gt (CX c e)) = (\ k. Gt (CX 1 (Mul (k div c) e)))" - "a\ (Ge (CX c e)) = (\ k. Ge (CX 1 (Mul (k div c) e)))" - "a\ (Dvd i (CX c e)) =(\ k. Dvd ((k div c)*i) (CX 1 (Mul (k div c) e)))" - "a\ (NDvd i (CX c e))=(\ k. NDvd ((k div c)*i) (CX 1 (Mul (k div c) e)))" + "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)" 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 (CX c e)) = (\ k. c dvd k)" - "d\ (NEq (CX c e)) = (\ k. c dvd k)" - "d\ (Lt (CX c e)) = (\ k. c dvd k)" - "d\ (Le (CX c e)) = (\ k. c dvd k)" - "d\ (Gt (CX c e)) = (\ k. c dvd k)" - "d\ (Ge (CX c e)) = (\ k. c dvd k)" - "d\ (Dvd i (CX c e)) =(\ k. c dvd k)" - "d\ (NDvd i (CX c e))=(\ k. c dvd 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)" recdef \ "measure size" "\ (And p q) = ilcm (\ p) (\ q)" "\ (Or p q) = ilcm (\ p) (\ q)" - "\ (Eq (CX c e)) = c" - "\ (NEq (CX c e)) = c" - "\ (Lt (CX c e)) = c" - "\ (Le (CX c e)) = c" - "\ (Gt (CX c e)) = c" - "\ (Ge (CX c e)) = c" - "\ (Dvd i (CX c e)) = c" - "\ (NDvd i (CX c e))= c" + "\ (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" recdef \ "measure size" "\ (And p q) = (\ p @ \ q)" "\ (Or p q) = (\ p @ \ q)" - "\ (Eq (CX c e)) = [Sub (C -1) e]" - "\ (NEq (CX c e)) = [Neg e]" - "\ (Lt (CX c e)) = []" - "\ (Le (CX c e)) = []" - "\ (Gt (CX c e)) = [Neg e]" - "\ (Ge (CX c e)) = [Sub (C -1) e]" + "\ (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 = []" recdef \ "measure size" "\ (And p q) = (\ p @ \ q)" "\ (Or p q) = (\ p @ \ q)" - "\ (Eq (CX c e)) = [Add (C -1) e]" - "\ (NEq (CX c e)) = [e]" - "\ (Lt (CX c e)) = [e]" - "\ (Le (CX c e)) = [Add (C -1) e]" - "\ (Gt (CX c e)) = []" - "\ (Ge (CX c e)) = []" + "\ (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" "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 \\ *) lemma dvd1_eq1: "x >0 \ (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 "\ = (j dvd (- (c*x - ?e)))" by (simp only: zdvd_zminus_iff) also have "\ = (j dvd (c* (- x)) + ?e)" apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib) by (simp add: ring_simps) - also have "\ = Ifm bbs ((- x)#bs) (Dvd j (CX c e))" + also have "\ = 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 "\ = (j dvd (- (c*x - ?e)))" by (simp only: zdvd_zminus_iff) also have "\ = (j dvd (c* (- x)) + ?e)" apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib) by (simp add: ring_simps) - also have "\ = Ifm bbs ((- x)#bs) (Dvd j (CX c e))" + also have "\ = 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: "\ p dvd ilcm (\ p) (\ q)" - by (simp add: ilcm_dvd1[where a="\ p" and b="\ q"]) - from prems have dl2: "\ q dvd ilcm (\ p) (\ q)" - by (simp add: ilcm_dvd2[where a="\ p" and b="\ q"]) + from prems have dl1: "\ p dvd ilcm (\ p) (\ q)" by simp + from prems have dl2: "\ q dvd ilcm (\ p) (\ q)" by simp from prems d\_mono[where p = "p" and l="\ p" and l'="ilcm (\ p) (\ q)"] d\_mono[where p = "q" and l="\ q" and l'="ilcm (\ p) (\ q)"] dl1 dl2 show ?case by (auto simp add: ilcm_pos) next case (2 p q) - from prems have dl1: "\ p dvd ilcm (\ p) (\ q)" - by (simp add: ilcm_dvd1[where a="\ p" and b="\ q"]) - from prems have dl2: "\ q dvd ilcm (\ p) (\ q)" - by (simp add: ilcm_dvd2[where a="\ p" and b="\ q"]) + from prems have dl1: "\ p dvd ilcm (\ p) (\ q)" by simp + from prems have dl2: "\ q dvd ilcm (\ p) (\ q)" by simp from prems d\_mono[where p = "p" and l="\ p" and l'="ilcm (\ p) (\ q)"] d\_mono[where p = "q" and l="\ q" and l'="ilcm (\ p) (\ 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: "\ (x-d) + ?e > 0" let ?v="Neg e" - have vb: "?v \ set (\ (Gt (CX c e)))" by simp + have vb: "?v \ set (\ (Gt (CN 0 c e)))" by simp from prems(11)[simplified simp_thms Inum.simps \.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "\ (\ j\ {1 ..d}. x = - ?e + j)" by auto from H p have "x + ?e > 0 \ x + ?e \ 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 \ 0" hence ?case using c1 @@ -1626,7 +1653,7 @@ moreover {assume H: "\ (x-d) + ?e \ 0" let ?v="Sub (C -1) e" - have vb: "?v \ set (\ (Ge (CX c e)))" by simp + have vb: "?v \ set (\ (Ge (CN 0 c e)))" by simp from prems(11)[simplified simp_thms Inum.simps \.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "\ (\ j\ {1 ..d}. x = - ?e - 1 + j)" by auto from H p have "x + ?e \ 0 \ 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 \ set (\ (Eq (CX c e)))" by simp + have vb: "?v \ set (\ (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 \ set (\ (NEq (CX c e)))" by simp + have vb: "?v \ set (\ (NEq (CN 0 c e)))" by simp {assume "x - d + Inum (((x -d)) # bs) e \ 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 = (\ 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 \ fm \ num list \ int" - "unit p \ (let p' = zlfm p ; l = \ p' ; q = And (Dvd l (CX 1 (C 0))) (a\ p' l); d = \ q; + "unit p \ (let p' = zlfm p ; l = \ p' ; q = And (Dvd l (CN 0 1 (C 0))) (a\ p' l); d = \ q; B = remdups (map simpnum (\ q)) ; a = remdups (map simpnum (\ q)) in if length B \ length a then (q,B,d) else (mirror q, a,d))" @@ -1767,7 +1794,7 @@ let ?I = "\ x p. Ifm bbs (x#bs) p" let ?p' = "zlfm p" let ?l = "\ ?p'" - let ?q = "And (Dvd ?l (CX 1 (C 0))) (a\ ?p' ?l)" + let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\ ?p' ?l)" let ?d = "\ ?q" let ?B = "set (\ ?q)" let ?B'= "remdups (map simpnum (\ ?q))"