(*  Title:      HOL/Decision_Procs/Cooper.thy

    Author:     Amine Chaieb

*)

theory Cooper

imports Complex_Main "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"

begin

(* Periodicity of dvd *)

  (*********************************************************************************)

  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)

  (*********************************************************************************)

datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num

  | Mul int num

primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}

where

  "num_size (C c) = 1"

| "num_size (Bound n) = 1"

| "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 (CN n c a) = 4 + num_size a"

| "num_size (Mul c a) = 1 + num_size a"

primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int" where

  "Inum bs (C c) = c"

| "Inum bs (Bound n) = bs!n"

| "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"

| "Inum bs (Mul c a) = c* Inum bs a"

datatype fm  =

  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|

  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm

  | Closed nat | NClosed nat

fun fmsize :: "fm \<Rightarrow> nat"  -- {* A size for fm *}

where

  "fmsize (NOT p) = 1 + fmsize p"

| "fmsize (And p q) = 1 + fmsize p + fmsize q"

| "fmsize (Or p q) = 1 + fmsize p + fmsize q"

| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"

| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"

| "fmsize (E p) = 1 + fmsize p"

| "fmsize (A p) = 4+ fmsize p"

| "fmsize (Dvd i t) = 2"

| "fmsize (NDvd i t) = 2"

| "fmsize p = 1"

lemma fmsize_pos: "fmsize p > 0"

  by (induct p rule: fmsize.induct) simp_all

primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- {* Semantics of formulae (fm) *}

where

  "Ifm bbs bs T = True"

| "Ifm bbs bs F = False"

| "Ifm bbs bs (Lt a) = (Inum bs a < 0)"

| "Ifm bbs bs (Gt a) = (Inum bs a > 0)"

| "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"

| "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"

| "Ifm bbs bs (Eq a) = (Inum bs a = 0)"

| "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"

| "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"

| "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"

| "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"

| "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"

| "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"

| "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"

| "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"

| "Ifm bbs bs (E p) = (\<exists>x. Ifm bbs (x#bs) p)"

| "Ifm bbs bs (A p) = (\<forall>x. Ifm bbs (x#bs) p)"

| "Ifm bbs bs (Closed n) = bbs!n"

| "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"

consts prep :: "fm \<Rightarrow> fm"

recdef prep "measure fmsize"

  "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)

lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"

  by (induct p arbitrary: bs rule: prep.induct) auto

fun qfree :: "fm \<Rightarrow> bool"  -- {* Quantifier freeness *}

where

  "qfree (E p) = False"

| "qfree (A p) = False"

| "qfree (NOT p) = qfree p"

| "qfree (And p q) = (qfree p \<and> qfree q)"

| "qfree (Or  p q) = (qfree p \<and> qfree q)"

| "qfree (Imp p q) = (qfree p \<and> qfree q)"

| "qfree (Iff p q) = (qfree p \<and> qfree q)"

| "qfree p = True"

text {* Boundedness and substitution *}

primrec numbound0 :: "num \<Rightarrow> bool"  -- {* a num is INDEPENDENT of Bound 0 *}

where

  "numbound0 (C c) = True"

| "numbound0 (Bound n) = (n>0)"

| "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)"

| "numbound0 (Mul i a) = numbound0 a"

lemma numbound0_I:

  assumes nb: "numbound0 a"

  shows "Inum (b#bs) a = Inum (b'#bs) a"

  using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)

primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *}

where

  "bound0 T = True"

| "bound0 F = True"

| "bound0 (Lt a) = numbound0 a"

| "bound0 (Le a) = numbound0 a"

| "bound0 (Gt a) = numbound0 a"

| "bound0 (Ge a) = numbound0 a"

| "bound0 (Eq a) = numbound0 a"

| "bound0 (NEq a) = numbound0 a"

| "bound0 (Dvd i a) = numbound0 a"

| "bound0 (NDvd i a) = numbound0 a"

| "bound0 (NOT p) = bound0 p"

| "bound0 (And p q) = (bound0 p \<and> bound0 q)"

| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"

| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"

| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"

| "bound0 (E p) = False"

| "bound0 (A p) = False"

| "bound0 (Closed P) = True"

| "bound0 (NClosed P) = True"

lemma bound0_I:

  assumes bp: "bound0 p"

  shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"

  using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]

  by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)

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 (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: "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"

  by (induct t rule: numsubst0.induct) (auto simp: nth_Cons')

lemma numsubst0_I':

  "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"

  by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])

primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm"  -- {* substitue a num into a formula for Bound 0 *}

where

  "subst0 t T = T"

| "subst0 t F = F"

| "subst0 t (Lt a) = Lt (numsubst0 t a)"

| "subst0 t (Le a) = Le (numsubst0 t a)"

| "subst0 t (Gt a) = Gt (numsubst0 t a)"

| "subst0 t (Ge a) = Ge (numsubst0 t a)"

| "subst0 t (Eq a) = Eq (numsubst0 t a)"

| "subst0 t (NEq a) = NEq (numsubst0 t a)"

| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"

| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"

| "subst0 t (NOT p) = NOT (subst0 t p)"

| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"

| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"

| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"

| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"

| "subst0 t (Closed P) = (Closed P)"

| "subst0 t (NClosed P) = (NClosed P)"

lemma subst0_I:

  assumes qfp: "qfree p"

  shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"

  using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]

  by (induct p) (simp_all add: gr0_conv_Suc)

fun decrnum:: "num \<Rightarrow> num"

where

  "decrnum (Bound n) = Bound (n - 1)"

| "decrnum (Neg a) = Neg (decrnum a)"

| "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"

fun decr :: "fm \<Rightarrow> fm"

where

  "decr (Lt a) = Lt (decrnum a)"

| "decr (Le a) = Le (decrnum a)"

| "decr (Gt a) = Gt (decrnum a)"

| "decr (Ge a) = Ge (decrnum a)"

| "decr (Eq a) = Eq (decrnum a)"

| "decr (NEq a) = NEq (decrnum a)"

| "decr (Dvd i a) = Dvd i (decrnum a)"

| "decr (NDvd i a) = NDvd i (decrnum a)"

| "decr (NOT p) = NOT (decr p)"

| "decr (And p q) = And (decr p) (decr q)"

| "decr (Or p q) = Or (decr p) (decr q)"

| "decr (Imp p q) = Imp (decr p) (decr q)"

| "decr (Iff p q) = Iff (decr p) (decr q)"

| "decr p = p"

lemma decrnum:

  assumes nb: "numbound0 t"

  shows "Inum (x#bs) t = Inum bs (decrnum t)"

  using nb by (induct t rule: decrnum.induct) (auto simp add: gr0_conv_Suc)

lemma decr:

  assumes nb: "bound0 p"

  shows "Ifm bbs (x#bs) p = Ifm bbs bs (decr p)"

  using nb by (induct p rule: decr.induct) (simp_all add: gr0_conv_Suc decrnum)

lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"

  by (induct p) simp_all

fun isatom :: "fm \<Rightarrow> bool"  -- {* test for atomicity *}

where

  "isatom T = True"

| "isatom F = True"

| "isatom (Lt a) = True"

| "isatom (Le a) = True"

| "isatom (Gt a) = True"

| "isatom (Ge a) = True"

| "isatom (Eq a) = True"

| "isatom (NEq a) = True"

| "isatom (Dvd i b) = True"

| "isatom (NDvd i b) = True"

| "isatom (Closed P) = True"

| "isatom (NClosed P) = True"

| "isatom p = False"

lemma numsubst0_numbound0:

  assumes nb: "numbound0 t"

  shows "numbound0 (numsubst0 t a)"

  using nb apply (induct a) 

  apply simp_all

  apply (case_tac nat, simp_all)

  done

lemma subst0_bound0:

  assumes qf: "qfree p" and nb: "numbound0 t"

  shows "bound0 (subst0 t p)"

  using qf numsubst0_numbound0[OF nb] by (induct p) auto

lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"

  by (induct p) simp_all

definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"

where

  "djf f p q =

    (if q = T then T

     else if q = F then f p

     else (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"

definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"

  where "evaldjf f ps = foldr (djf f) ps F"

lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"

  by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def)

    (cases "f p", simp_all add: Let_def djf_def)

lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) = (\<exists>p \<in> set ps. Ifm bbs bs (f p))"

  by (induct ps) (simp_all add: evaldjf_def djf_Or)

lemma evaldjf_bound0:

  assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"

  shows "bound0 (evaldjf f xs)"

  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)

lemma evaldjf_qf:

  assumes nb: "\<forall>x\<in> set xs. qfree (f x)"

  shows "qfree (evaldjf f xs)"

  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)

fun disjuncts :: "fm \<Rightarrow> fm list"

where

  "disjuncts (Or p q) = disjuncts p @ disjuncts q"

| "disjuncts F = []"

| "disjuncts p = [p]"

lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p"

 by (induct p rule: disjuncts.induct) auto

lemma disjuncts_nb:

  assumes nb: "bound0 p"

  shows "\<forall>q \<in> set (disjuncts p). bound0 q"

proof -

  from nb have "list_all bound0 (disjuncts p)"

    by (induct p rule: disjuncts.induct) auto

  thus ?thesis by (simp only: list_all_iff)

qed

lemma disjuncts_qf:

  assumes qf: "qfree p"

  shows "\<forall>q \<in> set (disjuncts p). qfree q"

proof -

  from qf have "list_all qfree (disjuncts p)"

    by (induct p rule: disjuncts.induct) auto

  thus ?thesis by (simp only: list_all_iff)

qed

definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"

  where "DJ f p = evaldjf f (disjuncts p)"

lemma DJ:

  assumes fdj: "\<forall>p q. f (Or p q) = Or (f p) (f q)"

    and fF: "f F = F"

  shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"

proof -

  have "Ifm bbs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (f q))"

    by (simp add: DJ_def evaldjf_ex)

  also have "\<dots> = Ifm bbs bs (f p)"

    using fdj fF by (induct p rule: disjuncts.induct) auto

  finally show ?thesis .

qed

lemma DJ_qf:

  assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"

  shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "

proof clarify

  fix p assume qf: "qfree p"

  have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def)

  from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" .

  with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)" by blast

  from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp

qed

lemma DJ_qe:

  assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"

  shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"

proof clarify

  fix p :: fm and bs

  assume qf: "qfree p"

  from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)" by blast

  from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto

  have "Ifm bbs bs (DJ qe p) = (\<exists>q\<in> set (disjuncts p). Ifm bbs bs (qe q))"

    by (simp add: DJ_def evaldjf_ex)

  also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm bbs bs (E q))"

    using qe disjuncts_qf[OF qf] by auto

  also have "\<dots> = Ifm bbs bs (E p)"

    by (induct p rule: disjuncts.induct) auto

  finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)"

    using qfth by blast

qed

text {* Simplification *}

text {* Algebraic simplifications for nums *}

fun bnds :: "num \<Rightarrow> nat list"

where

  "bnds (Bound n) = [n]"

| "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)"

| "bnds (Mul i a) = bnds a"

| "bnds a = []"

fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"

where

  "lex_ns [] ms = True"

| "lex_ns ns [] = False"

| "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) "

definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"

  where "lex_bnd t s = lex_ns (bnds t) (bnds s)"

consts numadd:: "num \<times> num \<Rightarrow> num"

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

       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)"

  "numadd (a, b) = Add a b"

(*function (sequential)

  numadd :: "num \<Rightarrow> num \<Rightarrow> 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 \<le> 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, simp_all add: Let_def)

  apply (case_tac "c1 + c2 = 0", case_tac "n1 \<le> n2", simp_all)

   apply (case_tac "n1 = n2")

    apply(simp_all add: algebra_simps)

  apply(simp add: distrib_right[symmetric])

  done

lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"

  by (induct t s rule: numadd.induct) (auto simp add: Let_def)

fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"

where

  "nummul i (C j) = C (i * j)"

| "nummul i (CN n c t) = CN n (c*i) (nummul i t)"

| "nummul i t = Mul i t"

lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"

  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: algebra_simps numadd)

lemma nummul_nb: "numbound0 t \<Longrightarrow> numbound0 (nummul i t)"

  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: numadd_nb)

definition numneg :: "num \<Rightarrow> num"

  where "numneg t = nummul (- 1) t"

definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"

  where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))"

lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"

  using numneg_def nummul by simp

lemma numneg_nb: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"

  using numneg_def nummul_nb by simp

lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)"

  using numneg numadd numsub_def by simp

lemma numsub_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numsub t s)"

  using numsub_def numadd_nb numneg_nb by simp

fun simpnum :: "num \<Rightarrow> num"

where

  "simpnum (C j) = C j"

| "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)"

| "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"

| "simpnum t = t"

lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t"

  by (induct t rule: simpnum.induct) (auto simp add: numneg numadd numsub nummul)

lemma simpnum_numbound0: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"

  by (induct t rule: simpnum.induct) (auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)

fun not :: "fm \<Rightarrow> fm"

where

  "not (NOT p) = p"

| "not T = F"

| "not F = T"

| "not p = NOT p"

lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"

  by (cases p) auto

lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"

  by (cases p) auto

lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"

  by (cases p) auto

definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"

  where

    "conj p q = (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)"

lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"

  by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all)

lemma conj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)"

  using conj_def by auto

lemma conj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (conj p q)"

  using conj_def by auto

definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"

  where

    "disj p q =

      (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else Or p q)"

lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"

  by (cases "p=T \<or> q=T", simp_all add: disj_def) (cases p, simp_all)

lemma disj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"

  using disj_def by auto

lemma disj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"

  using disj_def by auto

definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"

  where

    "imp p q = (if (p = F \<or> q=T) then T else if p=T then q else if q=F then not p else Imp p q)"

lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"

  by (cases "p=F \<or> q=T", simp_all add: imp_def, cases p) (simp_all add: not)

lemma imp_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)"

  using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf)

lemma imp_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)"

  using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all

definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"

  where

    "iff p q =

      (if (p = q) then T

       else if (p = not q \<or> not p = q) then F

       else if p = F then not q

       else if q = F then not p

       else if p = T then q

       else if q = T then p

       else Iff p q)"

lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"

  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not)

    (cases "not p= q", auto simp add:not)

lemma iff_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"

  by (unfold iff_def,cases "p=q", auto simp add: not_qf)

lemma iff_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"

  using iff_def by (unfold iff_def,cases "p=q", auto simp add: not_bn)

function (sequential) simpfm :: "fm \<Rightarrow> fm"

where

  "simpfm (And p q) = conj (simpfm p) (simpfm q)"

| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"

| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"

| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"

| "simpfm (NOT p) = not (simpfm p)"

| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F | _ \<Rightarrow> Lt a')"

| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0)  then T else F | _ \<Rightarrow> Le a')"

| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt a')"

| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0)  then T else F | _ \<Rightarrow> Ge a')"

| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"

| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq a')"

| "simpfm (Dvd i a) =

    (if i=0 then simpfm (Eq a)

     else if (abs i = 1) then T

     else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> Dvd i a')"

| "simpfm (NDvd i a) =

    (if i=0 then simpfm (NEq a)

     else if (abs i = 1) then F

     else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')"

| "simpfm p = p"

  by pat_completeness auto

termination by (relation "measure fmsize") auto

lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"

proof(induct p rule: simpfm.induct)

  case (6 a)

  let ?sa = "simpnum a"

  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp

  { fix v assume "?sa = C v" hence ?case using sa by simp }

  moreover {

    assume "\<not> (\<exists>v. ?sa = C v)"

    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)

  }

  ultimately show ?case by blast

next

  case (7 a)

  let ?sa = "simpnum a"

  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp

  { fix v assume "?sa = C v" hence ?case using sa by simp }

  moreover {

    assume "\<not> (\<exists>v. ?sa = C v)"

    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)

  }

  ultimately show ?case by blast

next

  case (8 a)

  let ?sa = "simpnum a"

  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp

  { fix v assume "?sa = C v" hence ?case using sa by simp }

  moreover {

    assume "\<not> (\<exists>v. ?sa = C v)"

    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)

  }

  ultimately show ?case by blast

next

  case (9 a)

  let ?sa = "simpnum a"

  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp

  { fix v assume "?sa = C v" hence ?case using sa by simp }

  moreover {

    assume "\<not> (\<exists>v. ?sa = C v)"

    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)

  }

  ultimately show ?case by blast

next

  case (10 a)

  let ?sa = "simpnum a"

  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp

  { fix v assume "?sa = C v" hence ?case using sa by simp }

  moreover {

    assume "\<not> (\<exists>v. ?sa = C v)"

    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)

  }

  ultimately show ?case by blast

next

  case (11 a)

  let ?sa = "simpnum a"

  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp

  { fix v assume "?sa = C v" hence ?case using sa by simp }

  moreover {

    assume "\<not> (\<exists>v. ?sa = C v)"

    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)

  }

  ultimately show ?case by blast

next

  case (12 i a)

  let ?sa = "simpnum a"

  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp

  { assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def) }

  moreover

  { assume i1: "abs i = 1"

    from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]

    have ?case using i1

      apply (cases "i=0", simp_all add: Let_def)

      apply (cases "i > 0", simp_all)

      done

  }

  moreover

  { assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"

    { fix v assume "?sa = C v"

      hence ?case using sa[symmetric] inz cond

        by (cases "abs i = 1") auto }

    moreover {

      assume "\<not> (\<exists>v. ?sa = C v)"

      hence "simpfm (Dvd i a) = Dvd i ?sa" using inz cond

        by (cases ?sa) (auto simp add: Let_def)

      hence ?case using sa by simp }

    ultimately have ?case by blast }

  ultimately show ?case by blast

next

  case (13 i a)

  let ?sa = "simpnum a" from simpnum_ci

  have sa: "Inum bs ?sa = Inum bs a" by simp

  { assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def) }

  moreover

  { assume i1: "abs i = 1"

    from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]

    have ?case using i1

      apply (cases "i=0", simp_all add: Let_def)

      apply (cases "i > 0", simp_all)

      done

  }

  moreover

  { assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"

    { fix v assume "?sa = C v"

      hence ?case using sa[symmetric] inz cond

        by (cases "abs i = 1") auto }

    moreover {

      assume "\<not> (\<exists>v. ?sa = C v)"

      hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond

        by (cases ?sa) (auto simp add: Let_def)

      hence ?case using sa by simp }

    ultimately have ?case by blast }

  ultimately show ?case by blast

qed (simp_all add: conj disj imp iff not)

lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"

proof (induct p rule: simpfm.induct)

  case (6 a) hence nb: "numbound0 a" by simp

  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

  thus ?case by (cases "simpnum a") (auto simp add: Let_def)

next

  case (7 a) hence nb: "numbound0 a" by simp

  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

  thus ?case by (cases "simpnum a") (auto simp add: Let_def)

next

  case (8 a) hence nb: "numbound0 a" by simp

  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

  thus ?case by (cases "simpnum a") (auto simp add: Let_def)

next

  case (9 a) hence nb: "numbound0 a" by simp

  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

  thus ?case by (cases "simpnum a") (auto simp add: Let_def)

next

  case (10 a) hence nb: "numbound0 a" by simp

  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

  thus ?case by (cases "simpnum a") (auto simp add: Let_def)

next

  case (11 a) hence nb: "numbound0 a" by simp

  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

  thus ?case by (cases "simpnum a") (auto simp add: Let_def)

next

  case (12 i a) hence nb: "numbound0 a" by simp

  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

  thus ?case by (cases "simpnum a") (auto simp add: Let_def)

next

  case (13 i a) hence nb: "numbound0 a" by simp

  hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

  thus ?case by (cases "simpnum a") (auto simp add: Let_def)

qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)

lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"

  by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)

    (case_tac "simpnum a", auto)+

text {* Generic quantifier elimination *}

function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"

where

  "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"

| "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"

| "qelim (NOT p) = (\<lambda>qe. not (qelim p qe))"

| "qelim (And p q) = (\<lambda>qe. conj (qelim p qe) (qelim q qe))"

| "qelim (Or  p q) = (\<lambda>qe. disj (qelim p qe) (qelim q qe))"

| "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"

| "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"

| "qelim p = (\<lambda>y. simpfm p)"

  by pat_completeness auto

termination by (relation "measure fmsize") auto

lemma qelim_ci:

  assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"

  shows "\<And>bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)"

  using qe_inv DJ_qe[OF qe_inv]

  by(induct p rule: qelim.induct)

  (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf

    simpfm simpfm_qf simp del: simpfm.simps)

text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}

fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- {* splits the bounded from the unbounded part *}

where

  "zsplit0 (C c) = (0,C c)"

| "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"

| "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

                          in (ia+ib, Add a' b'))"

| "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ;

                          (ib,b') =  zsplit0 b

                          in (ia-ib, Sub a' b'))"

| "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) (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 m i a n a')

  let ?j = "fst (zsplit0 a)"

  let ?b = "snd (zsplit0 a)"

  have abj: "zsplit0 a = (?j,?b)" by simp

  {assume "m\<noteq>0"

    with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)}

  moreover

  {assume m0: "m =0"

    with abj have th: "a'=?b \<and> n=i+?j" using 3

      by (simp add: Let_def split_def)

    from abj 3 m0 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: distrib_right)

  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 4

    by (simp add: Let_def split_def)

  from abj 4 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)

  let ?ns = "fst (zsplit0 s)"

  let ?as = "snd (zsplit0 s)"

  let ?nt = "fst (zsplit0 t)"

  let ?at = "snd (zsplit0 t)"

  have abjs: "zsplit0 s = (?ns,?as)" by simp

  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp

  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 5

    by (simp add: Let_def split_def)

  from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s" by blast

  from 5 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 5 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

    by (simp add: distrib_right)

next

  case (6 s t n a)

  let ?ns = "fst (zsplit0 s)"

  let ?as = "snd (zsplit0 s)"

  let ?nt = "fst (zsplit0 t)"

  let ?at = "snd (zsplit0 t)"

  have abjs: "zsplit0 s = (?ns,?as)" by simp

  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp

  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 6

    by (simp add: Let_def split_def)

  from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s" by blast

  from 6 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 6 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

    by (simp add: left_diff_distrib)

next

  case (7 i t n a)

  let ?nt = "fst (zsplit0 t)"

  let ?at = "snd (zsplit0 t)"

  have abj: "zsplit0 t = (?nt,?at)" by simp

  hence th: "a=Mul i ?at \<and> n=i*?nt" using 7

    by (simp add: Let_def split_def)

  from abj 7 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: distrib_left)

  finally show ?case using th th2 by simp

qed

consts iszlfm :: "fm \<Rightarrow> bool"  -- {* Linearity test for fm *}

recdef iszlfm "measure size"

  "iszlfm (And p q) = (iszlfm p \<and> iszlfm q)"

  "iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)"

  "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 (CN 0 c e))=

                 (c>0 \<and> i>0 \<and> numbound0 e)"

  "iszlfm p = (isatom p \<and> (bound0 p))"

lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"

  by (induct p rule: iszlfm.induct) auto

consts zlfm :: "fm \<Rightarrow> fm"  -- {* Linearity transformation for fm *}

recdef zlfm "measure fmsize"

  "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) = (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) = (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) = (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) = (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) = (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) = (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) = (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) (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) (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))"

  "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)

lemma zlfm_I:

  assumes qfp: "qfree p"

  shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm p)"

  (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")

  using qfp

proof (induct p rule: zlfm.induct)

  case (5 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) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto

  let ?N = "\<lambda>t. Inum (i#bs) t"

  from 5 Ia nb  show ?case

    apply (auto simp add: Let_def split_def algebra_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) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto

  let ?N = "\<lambda>t. Inum (i#bs) t"

  from 6 Ia nb show ?case

    apply (auto simp add: Let_def split_def algebra_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) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto

  let ?N = "\<lambda>t. Inum (i#bs) t"

  from 7 Ia nb show ?case

    apply (auto simp add: Let_def split_def algebra_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) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto

  let ?N = "\<lambda>t. Inum (i#bs) t"