Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Decision_Procs/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 157 kB

Quelle Parametric_Ferrante_Rackoff.thy Sprache: Isabelle

(*  Title:      HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
    Author:     Amine Chaieb
*)

section \<open>A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008\<close>

theory Parametric_Ferrante_Rackoff
imports
  Reflected_Multivariate_Polynomial
  Dense_Linear_Order
  DP_Library
  "HOL-Library.Code_Target_Numeral"
begin

subsection \<open>Terms\<close>

datatype (plugins del: size) tm = CP poly | Bound nat | Add tm tm | Mul poly tm
  | Neg tm | Sub tm tm | CNP nat poly tm

instantiation tm :: size
begin

primrec size_tm :: "tm \ nat"
  where
    "size_tm (CP c) = polysize c"
  | "size_tm (Bound n) = 1"
  | "size_tm (Neg a) = 1 + size_tm a"
  | "size_tm (Add a b) = 1 + size_tm a + size_tm b"
  | "size_tm (Sub a b) = 3 + size_tm a + size_tm b"
  | "size_tm (Mul c a) = 1 + polysize c + size_tm a"
  | "size_tm (CNP n c a) = 3 + polysize c + size_tm a "

instance ..

end

text \<open>Semantics of terms tm.\<close>
primrec Itm :: "'a::field_char_0 list \ 'a list \ tm \ 'a"
  where
    "Itm vs bs (CP c) = (Ipoly vs c)"
  | "Itm vs bs (Bound n) = bs!n"
  | "Itm vs bs (Neg a) = -(Itm vs bs a)"
  | "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
  | "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
  | "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
  | "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"

fun allpolys :: "(poly \ bool) \ tm \ bool"
  where
    "allpolys P (CP c) = P c"
  | "allpolys P (CNP n c p) = (P c \ allpolys P p)"
  | "allpolys P (Mul c p) = (P c \ allpolys P p)"
  | "allpolys P (Neg p) = allpolys P p"
  | "allpolys P (Add p q) = (allpolys P p \ allpolys P q)"
  | "allpolys P (Sub p q) = (allpolys P p \ allpolys P q)"
  | "allpolys P p = True"

primrec tmboundslt :: "nat \ tm \ bool"
  where
    "tmboundslt n (CP c) = True"
  | "tmboundslt n (Bound m) = (m < n)"
  | "tmboundslt n (CNP m c a) = (m < n \ tmboundslt n a)"
  | "tmboundslt n (Neg a) = tmboundslt n a"
  | "tmboundslt n (Add a b) = (tmboundslt n a \ tmboundslt n b)"
  | "tmboundslt n (Sub a b) = (tmboundslt n a \ tmboundslt n b)"
  | "tmboundslt n (Mul i a) = tmboundslt n a"

primrec tmbound0 :: "tm \ bool" \ \a \tm\ is \<^emph>\independent\ of Bound 0\
  where
    "tmbound0 (CP c) = True"
  | "tmbound0 (Bound n) = (n>0)"
  | "tmbound0 (CNP n c a) = (n\0 \ tmbound0 a)"
  | "tmbound0 (Neg a) = tmbound0 a"
  | "tmbound0 (Add a b) = (tmbound0 a \ tmbound0 b)"
  | "tmbound0 (Sub a b) = (tmbound0 a \ tmbound0 b)"
  | "tmbound0 (Mul i a) = tmbound0 a"

lemma tmbound0_I:
  assumes "tmbound0 a"
  shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
  using assms by (induct a rule: tm.induct) auto

primrec tmbound :: "nat \ tm \ bool" \ \a \tm\ is \<^emph>\independent\ of Bound n\
  where
    "tmbound n (CP c) = True"
  | "tmbound n (Bound m) = (n \ m)"
  | "tmbound n (CNP m c a) = (n\m \ tmbound n a)"
  | "tmbound n (Neg a) = tmbound n a"
  | "tmbound n (Add a b) = (tmbound n a \ tmbound n b)"
  | "tmbound n (Sub a b) = (tmbound n a \ tmbound n b)"
  | "tmbound n (Mul i a) = tmbound n a"

lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t"
  by (induct t) auto

lemma tmbound_I:
  assumes bnd: "tmboundslt (length bs) t"
    and nb: "tmbound n t"
    and le: "n \ length bs"
  shows "Itm vs (bs[n:=x]) t = Itm vs bs t"
  using nb le bnd
  by (induct t rule: tm.induct) auto

fun decrtm0 :: "tm \ tm"
  where
    "decrtm0 (Bound n) = Bound (n - 1)"
  | "decrtm0 (Neg a) = Neg (decrtm0 a)"
  | "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
  | "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
  | "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
  | "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
  | "decrtm0 a = a"

fun incrtm0 :: "tm \ tm"
  where
    "incrtm0 (Bound n) = Bound (n + 1)"
  | "incrtm0 (Neg a) = Neg (incrtm0 a)"
  | "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
  | "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
  | "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
  | "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
  | "incrtm0 a = a"

lemma decrtm0:
  assumes nb: "tmbound0 t"
  shows "Itm vs (x # bs) t = Itm vs bs (decrtm0 t)"
  using nb by (induct t rule: decrtm0.induct) simp_all

lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
  by (induct t rule: decrtm0.induct) simp_all

primrec decrtm :: "nat \ tm \ tm"
  where
    "decrtm m (CP c) = (CP c)"
  | "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
  | "decrtm m (Neg a) = Neg (decrtm m a)"
  | "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
  | "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
  | "decrtm m (Mul c a) = Mul c (decrtm m a)"
  | "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"

primrec removen :: "nat \ 'a list \ 'a list"
  where
    "removen n [] = []"
  | "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"

lemma removen_same: "n \ length xs \ removen n xs = xs"
  by (induct xs arbitrary: n) auto

lemma nth_length_exceeds: "n \ length xs \ xs!n = []!(n - length xs)"
  by (induct xs arbitrary: n) auto

lemma removen_length: "length (removen n xs) = (if n \ length xs then length xs else length xs - 1)"
  by (induct xs arbitrary: n) auto

lemma removen_nth:
  "(removen n xs)!m =
    (if n \<ge> length xs then xs!m
     else if m < n then xs!m
     else if m \<le> length xs then xs!(Suc m)
     else []!(m - (length xs - 1)))"
proof (induct xs arbitrary: n m)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  let ?l = "length (x # xs)"
  consider "n \ ?l" | "n < ?l" by arith
  then show ?case
  proof cases
    case 1
    with removen_same[OF this] show ?thesis by simp
  next
    case nl: 2
    consider "m < n" | "m \ n" by arith
    then show ?thesis
    proof cases
      case 1
      then show ?thesis
        using Cons by (cases m) auto
    next
      case 2
      consider "m \ ?l" | "m > ?l" by arith
      then show ?thesis
      proof cases
        case 1
        then show ?thesis
          using Cons by (cases m) auto
      next
        case ml: 2
        have th: "length (removen n (x # xs)) = length xs"
          using removen_length[where n = n and xs= "x # xs"] nl by simp
        with ml have "m \ length (removen n (x # xs))"
          by auto
        from th nth_length_exceeds[OF this] have "(removen n (x # xs))!m = [] ! (m - length xs)"
           by auto
        then have "(removen n (x # xs))!m = [] ! (m - (length (x # xs) - 1))"
          by auto
        then show ?thesis
          using ml nl by auto
      qed
    qed
  qed
qed

lemma decrtm:
  assumes bnd: "tmboundslt (length bs) t"
    and nb: "tmbound m t"
    and nle: "m \ length bs"
  shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
  using bnd nb nle by (induct t rule: tm.induct) (auto simp: removen_nth)

primrec tmsubst0:: "tm \ tm \ tm"
  where
    "tmsubst0 t (CP c) = CP c"
  | "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
  | "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
  | "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
  | "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
  | "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)"
  | "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"

lemma tmsubst0: "Itm vs (x # bs) (tmsubst0 t a) = Itm vs (Itm vs (x # bs) t # bs) a"
  by (induct a rule: tm.induct) auto

lemma tmsubst0_nb: "tmbound0 t \ tmbound0 (tmsubst0 t a)"
  by (induct a rule: tm.induct) auto

primrec tmsubst:: "nat \ tm \ tm \ tm"
  where
    "tmsubst n t (CP c) = CP c"
  | "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
  | "tmsubst n t (CNP m c a) =
      (if n = m then Add (Mul c t) (tmsubst n t a) else CNP m c (tmsubst n t a))"
  | "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
  | "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
  | "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)"
  | "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"

lemma tmsubst:
  assumes nb: "tmboundslt (length bs) a"
    and nlt: "n \ length bs"
  shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
  using nb nlt
  by (induct a rule: tm.induct) auto

lemma tmsubst_nb0:
  assumes tnb: "tmbound0 t"
  shows "tmbound0 (tmsubst 0 t a)"
  using tnb
  by (induct a rule: tm.induct) auto

lemma tmsubst_nb:
  assumes tnb: "tmbound m t"
  shows "tmbound m (tmsubst m t a)"
  using tnb
  by (induct a rule: tm.induct) auto

lemma incrtm0_tmbound: "tmbound n t \ tmbound (Suc n) (incrtm0 t)"
  by (induct t) auto

text \<open>Simplification.\<close>

fun tmadd:: "tm \ tm \ tm"
  where
    "tmadd (CNP n1 c1 r1) (CNP n2 c2 r2) =
      (if n1 = n2 then
        let c = c1 +\<^sub>p c2
        in if c = 0\<^sub>p then tmadd r1 r2 else CNP n1 c (tmadd r1 r2)
      else if n1 \<le> n2 then (CNP n1 c1 (tmadd r1 (CNP n2 c2 r2)))
      else (CNP n2 c2 (tmadd (CNP n1 c1 r1) r2)))"
  | "tmadd (CNP n1 c1 r1) t = CNP n1 c1 (tmadd r1 t)"
  | "tmadd t (CNP n2 c2 r2) = CNP n2 c2 (tmadd t r2)"
  | "tmadd (CP b1) (CP b2) = CP (b1 +\<^sub>p b2)"
  | "tmadd a b = Add a b"

lemma tmadd [simp]: "Itm vs bs (tmadd t s) = Itm vs bs (Add t s)"
proof (induct t s rule: tmadd.induct)
  case (1 n1 c1 r1 n2 c2 r2)
  show ?case
  proof (cases "c1 +\<^sub>p c2 = 0\<^sub>p")
    case 0: True
    show ?thesis
    proof (cases "n1 \ n2")
      case True
      with 0 show ?thesis
        apply (simp add: 1)
        by (metis INum_int(2) Ipoly.simps(1) comm_semiring_class.distrib mult_eq_0_iff polyadd)
    qed (use 0 1 in auto)
  next
    case False
    then show ?thesis
      using 1 comm_semiring_class.distrib by auto
  qed
qed auto

lemma tmadd_nb0[simp]: "tmbound0 t \ tmbound0 s \ tmbound0 (tmadd t s)"
  by (induct t s rule: tmadd.induct) (auto simp: Let_def)

lemma tmadd_nb[simp]: "tmbound n t \ tmbound n s \ tmbound n (tmadd t s)"
  by (induct t s rule: tmadd.induct) (auto simp: Let_def)

lemma tmadd_blt[simp]: "tmboundslt n t \ tmboundslt n s \ tmboundslt n (tmadd t s)"
  by (induct t s rule: tmadd.induct) (auto simp: Let_def)

lemma tmadd_allpolys_npoly[simp]:
  "allpolys isnpoly t \ allpolys isnpoly s \ allpolys isnpoly (tmadd t s)"
  by (induct t s rule: tmadd.induct) (simp_all add: Let_def polyadd_norm)

fun tmmul:: "tm \ poly \ tm"
  where
    "tmmul (CP j) = (\i. CP (i *\<^sub>p j))"
  | "tmmul (CNP n c a) = (\i. CNP n (i *\<^sub>p c) (tmmul a i))"
  | "tmmul t = (\i. Mul i t)"

lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)"
  by (induct t arbitrary: i rule: tmmul.induct) (simp_all add: field_simps)

lemma tmmul_nb0[simp]: "tmbound0 t \ tmbound0 (tmmul t i)"
  by (induct t arbitrary: i rule: tmmul.induct) auto

lemma tmmul_nb[simp]: "tmbound n t \ tmbound n (tmmul t i)"
  by (induct t arbitrary: n rule: tmmul.induct) auto

lemma tmmul_blt[simp]: "tmboundslt n t \ tmboundslt n (tmmul t i)"
  by (induct t arbitrary: i rule: tmmul.induct) (auto simp: Let_def)

lemma tmmul_allpolys_npoly[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "allpolys isnpoly t \ isnpoly c \ allpolys isnpoly (tmmul t c)"
  by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)

definition tmneg :: "tm \ tm"
  where "tmneg t \ tmmul t (C (- 1,1))"

definition tmsub :: "tm \ tm \ tm"
  where "tmsub s t \ (if s = t then CP 0\<^sub>p else tmadd s (tmneg t))"

lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)"
  using tmneg_def[of t] by simp

lemma tmneg_nb0[simp]: "tmbound0 t \ tmbound0 (tmneg t)"
  using tmneg_def by simp

lemma tmneg_nb[simp]: "tmbound n t \ tmbound n (tmneg t)"
  using tmneg_def by simp

lemma tmneg_blt[simp]: "tmboundslt n t \ tmboundslt n (tmneg t)"
  using tmneg_def by simp

lemma [simp]: "isnpoly (C (-1, 1))"
  by (simp add: isnpoly_def)

lemma tmneg_allpolys_npoly[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "allpolys isnpoly t \ allpolys isnpoly (tmneg t)"
  by (auto simp: tmneg_def)

lemma tmsub[simp]: "Itm vs bs (tmsub a b) = Itm vs bs (Sub a b)"
  using tmsub_def by simp

lemma tmsub_nb0[simp]: "tmbound0 t \ tmbound0 s \ tmbound0 (tmsub t s)"
  using tmsub_def by simp

lemma tmsub_nb[simp]: "tmbound n t \ tmbound n s \ tmbound n (tmsub t s)"
  using tmsub_def by simp

lemma tmsub_blt[simp]: "tmboundslt n t \ tmboundslt n s \ tmboundslt n (tmsub t s)"
  using tmsub_def by simp

lemma tmsub_allpolys_npoly[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "allpolys isnpoly t \ allpolys isnpoly s \ allpolys isnpoly (tmsub t s)"
  by (simp add: tmsub_def isnpoly_def)

fun simptm :: "tm \ tm"
  where
    "simptm (CP j) = CP (polynate j)"
  | "simptm (Bound n) = CNP n (1)\<^sub>p (CP 0\<^sub>p)"
  | "simptm (Neg t) = tmneg (simptm t)"
  | "simptm (Add t s) = tmadd (simptm t) (simptm s)"
  | "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
  | "simptm (Mul i t) =
      (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
  | "simptm (CNP n c t) =
      (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p)) (simptm t))"

lemma polynate_stupid:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "polynate t = 0\<^sub>p \ Ipoly bs t = (0::'a)"
  by (metis INum_int(2) Ipoly.simps(1) polynate)

lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t"
  by (induct t rule: simptm.induct) (auto simp: Let_def polynate_stupid)

lemma simptm_tmbound0[simp]: "tmbound0 t \ tmbound0 (simptm t)"
  by (induct t rule: simptm.induct) (auto simp: Let_def)

lemma simptm_nb[simp]: "tmbound n t \ tmbound n (simptm t)"
  by (induct t rule: simptm.induct) (auto simp: Let_def)

lemma simptm_nlt[simp]: "tmboundslt n t \ tmboundslt n (simptm t)"
  by (induct t rule: simptm.induct) (auto simp: Let_def)

lemma [simp]: "isnpoly 0\<^sub>p"
  and [simp]: "isnpoly (C (1, 1))"
  by (simp_all add: isnpoly_def)

lemma simptm_allpolys_npoly[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "allpolys isnpoly (simptm p)"
  by (induct p rule: simptm.induct) (auto simp: Let_def)

declare let_cong[fundef_cong del]

fun split0 :: "tm \ poly \ tm"
  where
    "split0 (Bound 0) = ((1)\<^sub>p, CP 0\<^sub>p)"
  | "split0 (CNP 0 c t) = (let (c', t') = split0 t in (c +\<^sub>p c', t'))"
  | "split0 (Neg t) = (let (c, t') = split0 t in (~\<^sub>p c, Neg t'))"
  | "split0 (CNP n c t) = (let (c', t') = split0 t in (c', CNP n c t'))"
  | "split0 (Add s t) = (let (c1, s') = split0 s; (c2, t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))"
  | "split0 (Sub s t) = (let (c1, s') = split0 s; (c2, t') = split0 t in (c1 -\<^sub>p c2, Sub s' t'))"
  | "split0 (Mul c t) = (let (c', t') = split0 t in (c *\<^sub>p c', Mul c t'))"
  | "split0 t = (0\<^sub>p, t)"

declare let_cong[fundef_cong]

lemma split0_stupid[simp]: "\x y. (x, y) = split0 p"
  using prod.collapse by blast

lemma split0:
  "tmbound 0 (snd (split0 t)) \ Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t"
proof (induct t rule: split0.induct)
  case (7 c t)
  then show ?case
    by (simp add: Let_def split_def mult.assoc flip: distrib_left)
qed (auto simp: Let_def split_def field_simps)

lemma split0_ci: "split0 t = (c',t') \ Itm vs bs t = Itm vs bs (CNP 0 c' t')"
proof -
  fix c' t'
  assume "split0 t = (c', t')"
  then have "c' = fst (split0 t)" "t' = snd (split0 t)"
    by auto
  with split0[where t="t" and bs="bs"] show "Itm vs bs t = Itm vs bs (CNP 0 c' t')"
    by simp
qed

lemma split0_nb0:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "split0 t = (c',t') \ tmbound 0 t'"
proof -
  fix c' t'
  assume "split0 t = (c', t')"
  then have "c' = fst (split0 t)" "t' = snd (split0 t)"
    by auto
  with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'"
    by simp
qed

lemma split0_nb0'[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "tmbound0 (snd (split0 t))"
  using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
  by (simp add: tmbound0_tmbound_iff)

lemma split0_nb:
  assumes nb: "tmbound n t"
  shows "tmbound n (snd (split0 t))"
  using nb by (induct t rule: split0.induct) (auto simp: Let_def split_def)

lemma split0_blt:
  assumes nb: "tmboundslt n t"
  shows "tmboundslt n (snd (split0 t))"
  using nb by (induct t rule: split0.induct) (auto simp: Let_def split_def)

lemma tmbound_split0: "tmbound 0 t \ Ipoly vs (fst (split0 t)) = 0"
  by (induct t rule: split0.induct) (auto simp: Let_def split_def)

lemma tmboundslt_split0: "tmboundslt n t \ Ipoly vs (fst (split0 t)) = 0 \ n > 0"
  by (induct t rule: split0.induct) (auto simp: Let_def split_def)

lemma tmboundslt0_split0: "tmboundslt 0 t \ Ipoly vs (fst (split0 t)) = 0"
  by (induct t rule: split0.induct) (auto simp: Let_def split_def)

lemma allpolys_split0: "allpolys isnpoly p \ allpolys isnpoly (snd (split0 p))"
  by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)

lemma isnpoly_fst_split0:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "allpolys isnpoly p \ isnpoly (fst (split0 p))"
  by (induct p rule: split0.induct)
    (auto simp  add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)

subsection \<open>Formulae\<close>

datatype (plugins del: size) fm = T | F | Le tm | Lt tm | Eq tm | NEq tm |
  Not fm | And fm fm | Or fm fm | Imp fm fm | Iff fm fm | E fm | A fm

instantiation fm :: size
begin

primrec size_fm :: "fm \ nat"
  where
    "size_fm (Not p) = 1 + size_fm p"
  | "size_fm (And p q) = 1 + size_fm p + size_fm q"
  | "size_fm (Or p q) = 1 + size_fm p + size_fm q"
  | "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
  | "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
  | "size_fm (E p) = 1 + size_fm p"
  | "size_fm (A p) = 4 + size_fm p"
  | "size_fm T = 1"
  | "size_fm F = 1"
  | "size_fm (Le _) = 1"
  | "size_fm (Lt _) = 1"
  | "size_fm (Eq _) = 1"
  | "size_fm (NEq _) = 1"

instance ..

end

lemma fmsize_pos [simp]: "size p > 0" for p :: fm
  by (induct p) simp_all

text \<open>Semantics of formulae (fm).\<close>
primrec Ifm ::"'a::linordered_field list \ 'a list \ fm \ bool"
  where
    "Ifm vs bs T = True"
  | "Ifm vs bs F = False"
  | "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
  | "Ifm vs bs (Le a) = (Itm vs bs a \ 0)"
  | "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
  | "Ifm vs bs (NEq a) = (Itm vs bs a \ 0)"
  | "Ifm vs bs (Not p) = (\ (Ifm vs bs p))"
  | "Ifm vs bs (And p q) = (Ifm vs bs p \ Ifm vs bs q)"
  | "Ifm vs bs (Or p q) = (Ifm vs bs p \ Ifm vs bs q)"
  | "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \ (Ifm vs bs q))"
  | "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
  | "Ifm vs bs (E p) = (\x. Ifm vs (x#bs) p)"
  | "Ifm vs bs (A p) = (\x. Ifm vs (x#bs) p)"

fun not:: "fm \ fm"
  where
    "not (Not (Not p)) = not p"
  | "not (Not p) = p"
  | "not T = F"
  | "not F = T"
  | "not (Lt t) = Le (tmneg t)"
  | "not (Le t) = Lt (tmneg t)"
  | "not (Eq t) = NEq t"
  | "not (NEq t) = Eq t"
  | "not p = Not p"

lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (Not p)"
  by (induct p rule: not.induct) auto

definition conj :: "fm \ fm \ 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 if p = q then p
     else And p q)"

lemma conj[simp]: "Ifm vs bs (conj p q) = Ifm vs bs (And p q)"
  by (cases "p=F \ q=F", simp_all add: conj_def) (cases p, simp_all)

definition disj :: "fm \ fm \ 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 if p = q then p
     else Or p q)"

lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)"
  by (cases "p = T \ q = T", simp_all add: disj_def) (cases p, simp_all)

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

lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)"
  by (cases "p = F \ q = T") (simp_all add: imp_def)

definition iff :: "fm \ fm \ 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[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)"
  by (unfold iff_def, cases "p = q", simp, cases "p = Not q", simp) (cases "Not p= q", auto)

text \<open>Quantifier freeness.\<close>
fun qfree:: "fm \ bool"
  where
    "qfree (E p) = False"
  | "qfree (A p) = False"
  | "qfree (Not p) = qfree p"
  | "qfree (And p q) = (qfree p \ qfree q)"
  | "qfree (Or p q) = (qfree p \ qfree q)"
  | "qfree (Imp p q) = (qfree p \ qfree q)"
  | "qfree (Iff p q) = (qfree p \ qfree q)"
  | "qfree p = True"

text \<open>Boundedness and substitution.\<close>
primrec boundslt :: "nat \ fm \ bool"
  where
    "boundslt n T = True"
  | "boundslt n F = True"
  | "boundslt n (Lt t) = tmboundslt n t"
  | "boundslt n (Le t) = tmboundslt n t"
  | "boundslt n (Eq t) = tmboundslt n t"
  | "boundslt n (NEq t) = tmboundslt n t"
  | "boundslt n (Not p) = boundslt n p"
  | "boundslt n (And p q) = (boundslt n p \ boundslt n q)"
  | "boundslt n (Or p q) = (boundslt n p \ boundslt n q)"
  | "boundslt n (Imp p q) = ((boundslt n p) \ (boundslt n q))"
  | "boundslt n (Iff p q) = (boundslt n p \ boundslt n q)"
  | "boundslt n (E p) = boundslt (Suc n) p"
  | "boundslt n (A p) = boundslt (Suc n) p"

fun bound0:: "fm \ bool" \ \a formula is independent of Bound 0\
  where
    "bound0 T = True"
  | "bound0 F = True"
  | "bound0 (Lt a) = tmbound0 a"
  | "bound0 (Le a) = tmbound0 a"
  | "bound0 (Eq a) = tmbound0 a"
  | "bound0 (NEq a) = tmbound0 a"
  | "bound0 (Not p) = bound0 p"
  | "bound0 (And p q) = (bound0 p \ bound0 q)"
  | "bound0 (Or p q) = (bound0 p \ bound0 q)"
  | "bound0 (Imp p q) = ((bound0 p) \ (bound0 q))"
  | "bound0 (Iff p q) = (bound0 p \ bound0 q)"
  | "bound0 p = False"

lemma bound0_I:
  assumes bp: "bound0 p"
  shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p"
  using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
  by (induct p rule: bound0.induct) auto

primrec bound:: "nat \ fm \ bool" \ \a formula is independent of Bound n\
  where
    "bound m T = True"
  | "bound m F = True"
  | "bound m (Lt t) = tmbound m t"
  | "bound m (Le t) = tmbound m t"
  | "bound m (Eq t) = tmbound m t"
  | "bound m (NEq t) = tmbound m t"
  | "bound m (Not p) = bound m p"
  | "bound m (And p q) = (bound m p \ bound m q)"
  | "bound m (Or p q) = (bound m p \ bound m q)"
  | "bound m (Imp p q) = ((bound m p) \ (bound m q))"
  | "bound m (Iff p q) = (bound m p \ bound m q)"
  | "bound m (E p) = bound (Suc m) p"
  | "bound m (A p) = bound (Suc m) p"

lemma bound_I:
  assumes bnd: "boundslt (length bs) p"
    and nb: "bound n p"
    and le: "n \ length bs"
  shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p"
  using bnd nb le tmbound_I[where bs=bs and vs = vs]
proof (induct p arbitrary: bs n rule: fm.induct)
  case (E p bs n)
  have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" for y
  proof -
    from E have bnd: "boundslt (length (y#bs)) p"
      and nb: "bound (Suc n) p" and le: "Suc n \ length (y#bs)" by simp+
    from E.hyps[OF bnd nb le tmbound_I] show ?thesis .
  qed
  then show ?case by simp
next
  case (A p bs n)
  have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" for y
  proof -
    from A have bnd: "boundslt (length (y#bs)) p"
      and nb: "bound (Suc n) p"
      and le: "Suc n \ length (y#bs)"
      by simp_all
    from A.hyps[OF bnd nb le tmbound_I] show ?thesis .
  qed
  then show ?case by simp
qed auto

fun decr0 :: "fm \ fm"
  where
    "decr0 (Lt a) = Lt (decrtm0 a)"
  | "decr0 (Le a) = Le (decrtm0 a)"
  | "decr0 (Eq a) = Eq (decrtm0 a)"
  | "decr0 (NEq a) = NEq (decrtm0 a)"
  | "decr0 (Not p) = Not (decr0 p)"
  | "decr0 (And p q) = conj (decr0 p) (decr0 q)"
  | "decr0 (Or p q) = disj (decr0 p) (decr0 q)"
  | "decr0 (Imp p q) = imp (decr0 p) (decr0 q)"
  | "decr0 (Iff p q) = iff (decr0 p) (decr0 q)"
  | "decr0 p = p"

lemma decr0:
  assumes "bound0 p"
  shows "Ifm vs (x#bs) p = Ifm vs bs (decr0 p)"
  using assms by (induct p rule: decr0.induct) (simp_all add: decrtm0)

primrec decr :: "nat \ fm \ fm"
  where
    "decr m T = T"
  | "decr m F = F"
  | "decr m (Lt t) = (Lt (decrtm m t))"
  | "decr m (Le t) = (Le (decrtm m t))"
  | "decr m (Eq t) = (Eq (decrtm m t))"
  | "decr m (NEq t) = (NEq (decrtm m t))"
  | "decr m (Not p) = Not (decr m p)"
  | "decr m (And p q) = conj (decr m p) (decr m q)"
  | "decr m (Or p q) = disj (decr m p) (decr m q)"
  | "decr m (Imp p q) = imp (decr m p) (decr m q)"
  | "decr m (Iff p q) = iff (decr m p) (decr m q)"
  | "decr m (E p) = E (decr (Suc m) p)"
  | "decr m (A p) = A (decr (Suc m) p)"

lemma decr:
  assumes bnd: "boundslt (length bs) p"
    and nb: "bound m p"
    and nle: "m < length bs"
  shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p"
  using bnd nb nle
proof (induct p arbitrary: bs m rule: fm.induct)
  case (E p bs m)
  have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" for x
  proof -
    from E
    have bnd: "boundslt (length (x#bs)) p"
      and nb: "bound (Suc m) p"
      and nle: "Suc m < length (x#bs)"
      by auto
    from E(1)[OF bnd nb nle] show ?thesis .
  qed
  then show ?case by auto
next
  case (A p bs m)
  have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" for x
  proof -
    from A
    have bnd: "boundslt (length (x#bs)) p"
      and nb: "bound (Suc m) p"
      and nle: "Suc m < length (x#bs)"
      by auto
    from A(1)[OF bnd nb nle] show ?thesis .
  qed
  then show ?case by auto
qed (auto simp: decrtm removen_nth)

primrec subst0 :: "tm \ fm \ fm"
  where
    "subst0 t T = T"
  | "subst0 t F = F"
  | "subst0 t (Lt a) = Lt (tmsubst0 t a)"
  | "subst0 t (Le a) = Le (tmsubst0 t a)"
  | "subst0 t (Eq a) = Eq (tmsubst0 t a)"
  | "subst0 t (NEq a) = NEq (tmsubst0 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 (E p) = E p"
  | "subst0 t (A p) = A p"

lemma subst0:
  assumes qf: "qfree p"
  shows "Ifm vs (x # bs) (subst0 t p) = Ifm vs ((Itm vs (x # bs) t) # bs) p"
  using qf tmsubst0[where x="x" and bs="bs" and t="t"]
  by (induct p rule: fm.induct) auto

lemma subst0_nb:
  assumes bp: "tmbound0 t"
    and qf: "qfree p"
  shows "bound0 (subst0 t p)"
  using qf tmsubst0_nb[OF bp] bp by (induct p rule: fm.induct) auto

primrec subst:: "nat \ tm \ fm \ fm"
  where
    "subst n t T = T"
  | "subst n t F = F"
  | "subst n t (Lt a) = Lt (tmsubst n t a)"
  | "subst n t (Le a) = Le (tmsubst n t a)"
  | "subst n t (Eq a) = Eq (tmsubst n t a)"
  | "subst n t (NEq a) = NEq (tmsubst n t a)"
  | "subst n t (Not p) = Not (subst n t p)"
  | "subst n t (And p q) = And (subst n t p) (subst n t q)"
  | "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
  | "subst n t (Imp p q) = Imp (subst n t p) (subst n t q)"
  | "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
  | "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
  | "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"

lemma subst:
  assumes nb: "boundslt (length bs) p"
    and nlm: "n \ length bs"
  shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p"
  using nb nlm
proof (induct p arbitrary: bs n t rule: fm.induct)
  case (E p bs n)
  have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
        Ifm vs (x#bs[n:= Itm vs bs t]) p" for x
  proof -
    from E have bn: "boundslt (length (x#bs)) p"
      by simp
    from E have nlm: "Suc n \ length (x#bs)"
      by simp
    from E(1)[OF bn nlm]
    have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
        Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
      by simp
    then show ?thesis
      by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
  qed
  then show ?case by simp
next
  case (A p bs n)
  have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
        Ifm vs (x#bs[n:= Itm vs bs t]) p" for x
  proof -
    from A have bn: "boundslt (length (x#bs)) p"
      by simp
    from A have nlm: "Suc n \ length (x#bs)"
      by simp
    from A(1)[OF bn nlm]
    have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
        Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
      by simp
    then show ?thesis
      by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
  qed
  then show ?case by simp
qed (auto simp: tmsubst)

lemma subst_nb:
  assumes "tmbound m t"
  shows "bound m (subst m t p)"
  using assms tmsubst_nb incrtm0_tmbound by (induct p arbitrary: m t rule: fm.induct) auto

lemma not_qf[simp]: "qfree p \ qfree (not p)"
  by (induct p rule: not.induct) auto
lemma not_bn0[simp]: "bound0 p \ bound0 (not p)"
  by (induct p rule: not.induct) auto
lemma not_nb[simp]: "bound n p \ bound n (not p)"
  by (induct p rule: not.induct) auto
lemma not_blt[simp]: "boundslt n p \ boundslt n (not p)"
  by (induct p rule: not.induct) auto

lemma conj_qf[simp]: "qfree p \ qfree q \ qfree (conj p q)"
  using conj_def by auto
lemma conj_nb0[simp]: "bound0 p \ bound0 q \ bound0 (conj p q)"
  using conj_def by auto
lemma conj_nb[simp]: "bound n p \ bound n q \ bound n (conj p q)"
  using conj_def by auto
lemma conj_blt[simp]: "boundslt n p \ boundslt n q \ boundslt n (conj p q)"
  using conj_def by auto

lemma disj_qf[simp]: "qfree p \ qfree q \ qfree (disj p q)"
  using disj_def by auto
lemma disj_nb0[simp]: "bound0 p \ bound0 q \ bound0 (disj p q)"
  using disj_def by auto
lemma disj_nb[simp]: "bound n p \ bound n q \ bound n (disj p q)"
  using disj_def by auto
lemma disj_blt[simp]: "boundslt n p \ boundslt n q \ boundslt n (disj p q)"
  using disj_def by auto

lemma imp_qf[simp]: "qfree p \ qfree q \ qfree (imp p q)"
  using imp_def by (cases "p = F \ q = T") (simp_all add: imp_def)
lemma imp_nb0[simp]: "bound0 p \ bound0 q \ bound0 (imp p q)"
  using imp_def by (cases "p = F \ q = T \ p = q") (simp_all add: imp_def)
lemma imp_nb[simp]: "bound n p \ bound n q \ bound n (imp p q)"
  using imp_def by (cases "p = F \ q = T \ p = q") (simp_all add: imp_def)
lemma imp_blt[simp]: "boundslt n p \ boundslt n q \ boundslt n (imp p q)"
  using imp_def by auto

lemma iff_qf[simp]: "qfree p \ qfree q \ qfree (iff p q)"
  unfolding iff_def by (cases "p = q") auto
lemma iff_nb0[simp]: "bound0 p \ bound0 q \ bound0 (iff p q)"
  using iff_def unfolding iff_def by (cases "p = q") auto
lemma iff_nb[simp]: "bound n p \ bound n q \ bound n (iff p q)"
  using iff_def unfolding iff_def by (cases "p = q") auto
lemma iff_blt[simp]: "boundslt n p \ boundslt n q \ boundslt n (iff p q)"
  using iff_def by auto
lemma decr0_qf: "bound0 p \ qfree (decr0 p)"
  by (induct p) simp_all

fun isatom :: "fm \ bool" \ \test for atomicity\
  where
    "isatom T = True"
  | "isatom F = True"
  | "isatom (Lt a) = True"
  | "isatom (Le a) = True"
  | "isatom (Eq a) = True"
  | "isatom (NEq a) = True"
  | "isatom p = False"

lemma bound0_qf: "bound0 p \ qfree p"
  by (induct p) simp_all

definition djf :: "('a \ fm) \ 'a \ fm \ 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 \ fm) \ 'a list \ fm"
  where "evaldjf f ps \ foldr (djf f) ps F"

lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
  by (cases "f p") (simp_all add: Let_def djf_def)

lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \ (\p \ set ps. Ifm vs bs (f p))"
  by (induct ps) (simp_all add: evaldjf_def djf_Or)

lemma evaldjf_bound0:
  assumes "\x \ set xs. bound0 (f x)"
  shows "bound0 (evaldjf f xs)"
  using assms
proof (induct xs)
  case Nil
  then show ?case
    by (simp add: evaldjf_def)
next
  case (Cons a xs)
  then show ?case
    by (cases "f a") (simp_all add: evaldjf_def djf_def Let_def)
qed

lemma evaldjf_qf:
  assumes "\x\ set xs. qfree (f x)"
  shows "qfree (evaldjf f xs)"
  using assms
proof (induct xs)
  case Nil
  then show ?case
    by (simp add: evaldjf_def)
next
  case (Cons a xs)
  then show ?case
    by (cases "f a") (simp_all add: evaldjf_def djf_def Let_def)
qed

fun disjuncts :: "fm \ fm list"
  where
    "disjuncts (Or p q) = disjuncts p @ disjuncts q"
  | "disjuncts F = []"
  | "disjuncts p = [p]"

lemma disjuncts: "(\q \ set (disjuncts p). Ifm vs bs q) = Ifm vs bs p"
  by (induct p rule: disjuncts.induct) auto

lemma disjuncts_nb:
  assumes "bound0 p"
  shows "\q \ set (disjuncts p). bound0 q"
proof -
  from assms have "list_all bound0 (disjuncts p)"
    by (induct p rule: disjuncts.induct) auto
  then show ?thesis
    by (simp only: list_all_iff)
qed

lemma disjuncts_qf:
  assumes "qfree p"
  shows "\q \ set (disjuncts p). qfree q"
proof -
  from assms have "list_all qfree (disjuncts p)"
    by (induct p rule: disjuncts.induct) auto
  then show ?thesis
    by (simp only: list_all_iff)
qed

definition DJ :: "(fm \ fm) \ fm \ fm"
  where "DJ f p \ evaldjf f (disjuncts p)"

lemma DJ:
  assumes fdj: "\p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))"
    and fF: "f F = F"
  shows "Ifm vs bs (DJ f p) = Ifm vs bs (f p)"
proof -
  have "Ifm vs bs (DJ f p) = (\q \ set (disjuncts p). Ifm vs bs (f q))"
    by (simp add: DJ_def evaldjf_ex)
  also have "\ = Ifm vs bs (f p)"
    using fdj fF by (induct p rule: disjuncts.induct) auto
  finally show ?thesis .
qed

lemma DJ_qf:
  assumes fqf: "\p. qfree p \ qfree (f p)"
  shows "\p. qfree p \ 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 "\q\ set (disjuncts p). qfree q" .
  with fqf have th':"\q\ 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: "\bs p. qfree p \ qfree (qe p) \ (Ifm vs bs (qe p) = Ifm vs bs (E p))"
  shows "\bs p. qfree p \ qfree (DJ qe p) \ (Ifm vs bs ((DJ qe p)) = Ifm vs bs (E p))"
proof clarify
  fix p :: fm and bs
  assume qf: "qfree p"
  from qe have qth: "\p. qfree p \ qfree (qe p)"
    by blast
  from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)"
    by auto
  have "Ifm vs bs (DJ qe p) \ (\q\ set (disjuncts p). Ifm vs bs (qe q))"
    by (simp add: DJ_def evaldjf_ex)
  also have "\ = (\q \ set(disjuncts p). Ifm vs bs (E q))"
    using qe disjuncts_qf[OF qf] by auto
  also have "\ = Ifm vs bs (E p)"
    by (induct p rule: disjuncts.induct) auto
  finally show "qfree (DJ qe p) \ Ifm vs bs (DJ qe p) = Ifm vs bs (E p)"
    using qfth by blast
qed

fun conjuncts :: "fm \ fm list"
  where
    "conjuncts (And p q) = conjuncts p @ conjuncts q"
  | "conjuncts T = []"
  | "conjuncts p = [p]"

definition list_conj :: "fm list \ fm"
  where "list_conj ps \ foldr conj ps T"

definition CJNB :: "(fm \ fm) \ fm \ fm"
  where "CJNB f p \
    (let cjs = conjuncts p;
      (yes, no) = partition bound0 cjs
     in conj (decr0 (list_conj yes)) (f (list_conj no)))"

lemma conjuncts_qf: "qfree p \ \q \ set (conjuncts p). qfree q"
proof -
  assume qf: "qfree p"
  then have "list_all qfree (conjuncts p)"
    by (induct p rule: conjuncts.induct) auto
  then show ?thesis
    by (simp only: list_all_iff)
qed

lemma conjuncts: "(\q\ set (conjuncts p). Ifm vs bs q) = Ifm vs bs p"
  by (induct p rule: conjuncts.induct) auto

lemma conjuncts_nb:
  assumes "bound0 p"
  shows "\q \ set (conjuncts p). bound0 q"
proof -
  from assms have "list_all bound0 (conjuncts p)"
    by (induct p rule:conjuncts.induct) auto
  then show ?thesis
    by (simp only: list_all_iff)
qed

fun islin :: "fm \ bool"
  where
    "islin (And p q) = (islin p \ islin q \ p \ T \ p \ F \ q \ T \ q \ F)"
  | "islin (Or p q) = (islin p \ islin q \ p \ T \ p \ F \ q \ T \ q \ F)"
  | "islin (Eq (CNP 0 c s)) = (isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s)"
  | "islin (NEq (CNP 0 c s)) = (isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s)"
  | "islin (Lt (CNP 0 c s)) = (isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s)"
  | "islin (Le (CNP 0 c s)) = (isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s)"
  | "islin (Not p) = False"
  | "islin (Imp p q) = False"
  | "islin (Iff p q) = False"
  | "islin p = bound0 p"

lemma islin_stupid:
  assumes nb: "tmbound0 p"
  shows "islin (Lt p)"
    and "islin (Le p)"
    and "islin (Eq p)"
    and "islin (NEq p)"
  using nb by (cases p, auto, rename_tac nat a b, case_tac nat, auto)+

definition "lt p = (case p of CP (C c) \ if 0>\<^sub>N c then T else F| _ \ Lt p)"
definition "le p = (case p of CP (C c) \ if 0\\<^sub>N c then T else F | _ \ Le p)"
definition "eq p = (case p of CP (C c) \ if c = 0\<^sub>N then T else F | _ \ Eq p)"
definition "neq p = not (eq p)"

lemma lt: "allpolys isnpoly p \ Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
  by (auto simp: lt_def isnpoly_def split: tm.split poly.split)

lemma le: "allpolys isnpoly p \ Ifm vs bs (le p) = Ifm vs bs (Le p)"
  by (auto simp: le_def isnpoly_def split: tm.split poly.split)

lemma eq: "allpolys isnpoly p \ Ifm vs bs (eq p) = Ifm vs bs (Eq p)"
  by (auto simp: eq_def isnpoly_def split: tm.split poly.split)

lemma neq: "allpolys isnpoly p \ Ifm vs bs (neq p) = Ifm vs bs (NEq p)"
  by (simp add: neq_def eq)

lemma lt_lin: "tmbound0 p \ islin (lt p)"
  using islin_stupid
  by(auto simp: lt_def isnpoly_def split: tm.split poly.split)

lemma le_lin: "tmbound0 p \ islin (le p)"
  using islin_stupid
  by(auto simp: le_def isnpoly_def split: tm.split poly.split)

lemma eq_lin: "tmbound0 p \ islin (eq p)"
  using islin_stupid
  by(auto simp: eq_def isnpoly_def split: tm.split poly.split)

lemma neq_lin: "tmbound0 p \ islin (neq p)"
  using islin_stupid
  by(auto simp: neq_def eq_def isnpoly_def split: tm.split poly.split)

definition "simplt t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then lt s else Lt (CNP 0 c s))"
definition "simple t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then le s else Le (CNP 0 c s))"
definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))"
definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"

lemma simplt_islin [simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "islin (simplt t)"
  unfolding simplt_def
  using split0_nb0'
  by (auto simp: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
      islin_stupid allpolys_split0[OF simptm_allpolys_npoly])

lemma simple_islin [simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "islin (simple t)"
  unfolding simple_def
  using split0_nb0'
  by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
      islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)

lemma simpeq_islin [simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "islin (simpeq t)"
  unfolding simpeq_def
  using split0_nb0'
  by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
      islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)

lemma simpneq_islin [simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "islin (simpneq t)"
  unfolding simpneq_def
  using split0_nb0'
  by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
      islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin)

lemma really_stupid: "\ (\c1 s'. (c1, s') \ split0 s)"
  by (cases "split0 s") auto

lemma split0_npoly:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
    and *: "allpolys isnpoly t"
  shows "isnpoly (fst (split0 t))"
    and "allpolys isnpoly (snd (split0 t))"
  using *
  by (induct t rule: split0.induct)
    (auto simp: Let_def split_def polyadd_norm polymul_norm polyneg_norm
      polysub_norm really_stupid)

lemma simplt[simp]: "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)"
proof -
  have *: "allpolys isnpoly (simptm t)"
    by simp
  let ?t = "simptm t"
  show ?thesis
  proof (cases "fst (split0 ?t) = 0\<^sub>p")
    case True
    then show ?thesis
      using split0[of "simptm t" vs bs] lt[OF split0_npoly(2)[OF *], of vs bs]
      by (simp add: simplt_def Let_def split_def lt)
  next
    case False
    then show ?thesis
      using split0[of "simptm t" vs bs]
      by (simp add: simplt_def Let_def split_def)
  qed
qed

lemma simple[simp]: "Ifm vs bs (simple t) = Ifm vs bs (Le t)"
proof -
  have *: "allpolys isnpoly (simptm t)"
    by simp
  let ?t = "simptm t"
  show ?thesis
  proof (cases "fst (split0 ?t) = 0\<^sub>p")
    case True
    then show ?thesis
      using split0[of "simptm t" vs bs] le[OF split0_npoly(2)[OF *], of vs bs]
      by (simp add: simple_def Let_def split_def le)
  next
    case False
    then show ?thesis
      using split0[of "simptm t" vs bs]
      by (simp add: simple_def Let_def split_def)
  qed
qed

lemma simpeq[simp]: "Ifm vs bs (simpeq t) = Ifm vs bs (Eq t)"
proof -
  have n: "allpolys isnpoly (simptm t)"
    by simp
  let ?t = "simptm t"
  show ?thesis
  proof (cases "fst (split0 ?t) = 0\<^sub>p")
    case True
    then show ?thesis
      using split0[of "simptm t" vs bs] eq[OF split0_npoly(2)[OF n], of vs bs]
      by (simp add: simpeq_def Let_def split_def)
  next
    case False
    then show ?thesis using  split0[of "simptm t" vs bs]
      by (simp add: simpeq_def Let_def split_def)
  qed
qed

lemma simpneq[simp]: "Ifm vs bs (simpneq t) = Ifm vs bs (NEq t)"
proof -
  have n: "allpolys isnpoly (simptm t)"
    by simp
  let ?t = "simptm t"
  show ?thesis
  proof (cases "fst (split0 ?t) = 0\<^sub>p")
    case True
    then show ?thesis
      using split0[of "simptm t" vs bs] neq[OF split0_npoly(2)[OF n], of vs bs]
      by (simp add: simpneq_def Let_def split_def)
  next
    case False
    then show ?thesis
      using split0[of "simptm t" vs bs] by (simp add: simpneq_def Let_def split_def)
  qed
qed

lemma lt_nb: "tmbound0 t \ bound0 (lt t)"
  by(auto simp: lt_def split: tm.split poly.split)

lemma le_nb: "tmbound0 t \ bound0 (le t)"
  by(auto simp: le_def split: tm.split poly.split)

lemma eq_nb: "tmbound0 t \ bound0 (eq t)"
  by(auto simp: eq_def split: tm.split poly.split)

lemma neq_nb: "tmbound0 t \ bound0 (neq t)"
  by(auto simp: neq_def eq_def split: tm.split poly.split)

(*THE FOLLOWING PROOFS MIGHT BE COMBINED*)
lemma simplt_nb[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
  shows "bound0 (simplt t)"
proof (simp add: simplt_def Let_def split_def)
  have *: "tmbound0 (simptm t)"
    using t by simp
  let ?c = "fst (split0 (simptm t))"
  from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
  have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
    by auto
  from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]]
  have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0"
    by (simp_all add: isnpoly_def)
  from iffD1[OF isnpolyh_unique[OF ths] th]
  have "fst (split0 (simptm t)) = 0\<^sub>p" .
  then show "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (lt (snd (split0 (simptm t))))) \
      fst (split0 (simptm t)) = 0\<^sub>p"
    by (simp add: simplt_def Let_def split_def lt_nb)
qed

lemma simple_nb[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
  shows "bound0 (simple t)"
proof(simp add: simple_def Let_def split_def)
  have *: "tmbound0 (simptm t)"
    using t by simp
  let ?c = "fst (split0 (simptm t))"
  from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
  have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
    by auto
  from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]]
  have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0"
    by (simp_all add: isnpoly_def)
  from iffD1[OF isnpolyh_unique[OF ths] th]
  have "fst (split0 (simptm t)) = 0\<^sub>p" .
  then show "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (le (snd (split0 (simptm t))))) \
      fst (split0 (simptm t)) = 0\<^sub>p"
    by (simp add: simplt_def Let_def split_def le_nb)
qed

lemma simpeq_nb[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
  shows "bound0 (simpeq t)"
proof (simp add: simpeq_def Let_def split_def)
  have *: "tmbound0 (simptm t)"
    using t by simp
  let ?c = "fst (split0 (simptm t))"
  from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
  have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
    by auto
  from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]]
  have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0"
    by (simp_all add: isnpoly_def)
  from iffD1[OF isnpolyh_unique[OF ths] th]
  have "fst (split0 (simptm t)) = 0\<^sub>p" .
  then show "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (eq (snd (split0 (simptm t))))) \
      fst (split0 (simptm t)) = 0\<^sub>p"
    by (simp add: simpeq_def Let_def split_def eq_nb)
qed

lemma simpneq_nb[simp]:
  assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
  shows "bound0 (simpneq t)"
proof (simp add: simpneq_def Let_def split_def)
  have *: "tmbound0 (simptm t)"
    using t by simp
  let ?c = "fst (split0 (simptm t))"
  from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
  have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
    by auto
  from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]]
  have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0"
    by (simp_all add: isnpoly_def)
  from iffD1[OF isnpolyh_unique[OF ths] th]
  have "fst (split0 (simptm t)) = 0\<^sub>p" .
  then show "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (neq (snd (split0 (simptm t))))) \
      fst (split0 (simptm t)) = 0\<^sub>p"
    by (simp add: simpneq_def Let_def split_def neq_nb)
qed

fun conjs :: "fm \ fm list"
  where
    "conjs (And p q) = conjs p @ conjs q"
  | "conjs T = []"
  | "conjs p = [p]"

lemma conjs_ci: "(\q \ set (conjs p). Ifm vs bs q) = Ifm vs bs p"
  by (induct p rule: conjs.induct) auto

definition list_disj :: "fm list \ fm"
  where "list_disj ps \ foldr disj ps F"

lemma list_conj: "Ifm vs bs (list_conj ps) = (\p\ set ps. Ifm vs bs p)"
  by (induct ps) (auto simp: list_conj_def)

lemma list_conj_qf: " \p\ set ps. qfree p \ qfree (list_conj ps)"
  by (induct ps) (auto simp: list_conj_def)

lemma list_disj: "Ifm vs bs (list_disj ps) = (\p\ set ps. Ifm vs bs p)"
  by (induct ps) (auto simp: list_disj_def)

lemma conj_boundslt: "boundslt n p \ boundslt n q \ boundslt n (conj p q)"
  unfolding conj_def by auto

lemma conjs_nb: "bound n p \ \q\ set (conjs p). bound n q"
proof (induct p rule: conjs.induct)
  case (1 p q)
  then show ?case
    unfolding conjs.simps bound.simps by fastforce
qed auto

lemma conjs_boundslt: "boundslt n p \ \q\ set (conjs p). boundslt n q"
proof (induct p rule: conjs.induct)
  case (1 p q)
  then show ?case
    unfolding conjs.simps bound.simps by fastforce
qed auto

lemma list_conj_boundslt: " \p\ set ps. boundslt n p \ boundslt n (list_conj ps)"
  by (induct ps) (auto simp: list_conj_def)

lemma list_conj_nb:
  assumes "\p\ set ps. bound n p"
  shows "bound n (list_conj ps)"
  using assms by (induct ps) (auto simp: list_conj_def)

lemma list_conj_nb': "\p\set ps. bound0 p \ bound0 (list_conj ps)"
  by (induct ps) (auto simp: list_conj_def)

lemma CJNB_qe:
  assumes qe: "\bs p. qfree p \ qfree (qe p) \ (Ifm vs bs (qe p) = Ifm vs bs (E p))"
  shows "\bs p. qfree p \ qfree (CJNB qe p) \ (Ifm vs bs ((CJNB qe p)) = Ifm vs bs (E p))"
proof clarify
  fix bs p
  assume qfp: "qfree p"
  let ?cjs = "conjuncts p"
  let ?yes = "fst (partition bound0 ?cjs)"
  let ?no = "snd (partition bound0 ?cjs)"
  let ?cno = "list_conj ?no"
  let ?cyes = "list_conj ?yes"
  have part: "partition bound0 ?cjs = (?yes,?no)"
    by simp
  from partition_P[OF part] have "\q\ set ?yes. bound0 q"
    by blast
  then have yes_nb: "bound0 ?cyes"
    by (simp add: list_conj_nb')
  then have yes_qf: "qfree (decr0 ?cyes)"
    by (simp add: decr0_qf)
  from conjuncts_qf[OF qfp] partition_set[OF part]
  have " \q\ set ?no. qfree q"
    by auto
  then have no_qf: "qfree ?cno"
    by (simp add: list_conj_qf)
  with qe have cno_qf:"qfree (qe ?cno)"
    and noE: "Ifm vs bs (qe ?cno) = Ifm vs bs (E ?cno)"
    by blast+
  from cno_qf yes_qf have qf: "qfree (CJNB qe p)"
    by (simp add: CJNB_def Let_def split_def)
  have "Ifm vs bs p = ((Ifm vs bs ?cyes) \ (Ifm vs bs ?cno))" for bs
  proof -
    from conjuncts have "Ifm vs bs p = (\q\ set ?cjs. Ifm vs bs q)"
      by blast
    also have "\ = ((\q\ set ?yes. Ifm vs bs q) \ (\q\ set ?no. Ifm vs bs q))"
      using partition_set[OF part] by auto
    finally show ?thesis
      using list_conj[of vs bs] by simp
  qed
  then have "Ifm vs bs (E p) = (\x. (Ifm vs (x#bs) ?cyes) \ (Ifm vs (x#bs) ?cno))"
    by simp
  also fix y have "\ = (\x. (Ifm vs (y#bs) ?cyes) \ (Ifm vs (x#bs) ?cno))"
    using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
  also have "\ = (Ifm vs bs (decr0 ?cyes) \ Ifm vs bs (E ?cno))"
    by (auto simp: decr0[OF yes_nb] simp del: partition_filter_conv)
  also have "\ = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
    using qe[rule_format, OF no_qf] by auto
  finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)"
    by (simp add: Let_def CJNB_def split_def)
  with qf show "qfree (CJNB qe p) \ Ifm vs bs (CJNB qe p) = Ifm vs bs (E p)"
    by blast
qed

fun simpfm :: "fm \ fm"
  where
    "simpfm (Lt t) = simplt (simptm t)"
  | "simpfm (Le t) = simple (simptm t)"
  | "simpfm (Eq t) = simpeq(simptm t)"
  | "simpfm (NEq t) = simpneq(simptm t)"
  | "simpfm (And p q) = conj (simpfm p) (simpfm q)"
  | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
  | "simpfm (Imp p q) = disj (simpfm (Not p)) (simpfm q)"
  | "simpfm (Iff p q) =
      disj (conj (simpfm p) (simpfm q)) (conj (simpfm (Not p)) (simpfm (Not q)))"
  | "simpfm (Not (And p q)) = disj (simpfm (Not p)) (simpfm (Not q))"
  | "simpfm (Not (Or p q)) = conj (simpfm (Not p)) (simpfm (Not q))"
  | "simpfm (Not (Imp p q)) = conj (simpfm p) (simpfm (Not q))"
  | "simpfm (Not (Iff p q)) =
      disj (conj (simpfm p) (simpfm (Not q))) (conj (simpfm (Not p)) (simpfm q))"
  | "simpfm (Not (Eq t)) = simpneq t"
  | "simpfm (Not (NEq t)) = simpeq t"
  | "simpfm (Not (Le t)) = simplt (Neg t)"
  | "simpfm (Not (Lt t)) = simple (Neg t)"
  | "simpfm (Not (Not p)) = simpfm p"
  | "simpfm (Not T) = F"
  | "simpfm (Not F) = T"
  | "simpfm p = p"

lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
  by (induct p arbitrary: bs rule: simpfm.induct) auto

lemma simpfm_bound0:
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "bound0 p \ bound0 (simpfm p)"
  by (induct p rule: simpfm.induct) auto

lemma lt_qf[simp]: "qfree (lt t)"
  by(auto simp: lt_def split: tm.split poly.split)

lemma le_qf[simp]: "qfree (le t)"
  by(auto simp: le_def split: tm.split poly.split)

lemma eq_qf[simp]: "qfree (eq t)"
  by(auto simp: eq_def split: tm.split poly.split)

lemma neq_qf[simp]: "qfree (neq t)"
  by (simp add: neq_def)

lemma simplt_qf[simp]: "qfree (simplt t)"
  by (simp add: simplt_def Let_def split_def)

lemma simple_qf[simp]: "qfree (simple t)"
  by (simp add: simple_def Let_def split_def)

lemma simpeq_qf[simp]: "qfree (simpeq t)"
  by (simp add: simpeq_def Let_def split_def)

lemma simpneq_qf[simp]: "qfree (simpneq t)"
  by (simp add: simpneq_def Let_def split_def)

lemma simpfm_qf[simp]: "qfree p \ qfree (simpfm p)"
  by (induct p rule: simpfm.induct) auto

lemma disj_lin: "islin p \ islin q \ islin (disj p q)"
  by (simp add: disj_def)

lemma conj_lin: "islin p \ islin q \ islin (conj p q)"
  by (simp add: conj_def)

lemma
  assumes "SORT_CONSTRAINT('a::field_char_0)"
  shows "qfree p \ islin (simpfm p)"
  by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)

fun prep :: "fm \ fm"
  where
    "prep (E T) = T"
  | "prep (E F) = F"
  | "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
  | "prep (E (Imp p q)) = disj (prep (E (Not p))) (prep (E q))"
  | "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (Not p) (Not q))))"
  | "prep (E (Not (And p q))) = disj (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))) = disj (prep (E (And p (Not q)))) (prep (E(And (Not p) q)))"
  | "prep (E p) = E (prep p)"
  | "prep (A (And p q)) = conj (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)) = disj (prep (Not p)) (prep (Not q))"
  | "prep (Not (A p)) = prep (E (Not p))"
  | "prep (Not (Or p q)) = conj (prep (Not p)) (prep (Not q))"
  | "prep (Not (Imp p q)) = conj (prep p) (prep (Not q))"
  | "prep (Not (Iff p q)) = disj (prep (And p (Not q))) (prep (And (Not p) q))"
  | "prep (Not p) = not (prep p)"
  | "prep (Or p q) = disj (prep p) (prep q)"
  | "prep (And p q) = conj (prep p) (prep q)"
  | "prep (Imp p q) = prep (Or (Not p) q)"
  | "prep (Iff p q) = disj (prep (And p q)) (prep (And (Not p) (Not q)))"
  | "prep p = p"

lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p"
  by (induct p arbitrary: bs rule: prep.induct) auto

text \<open>Generic quantifier elimination.\<close>
fun qelim :: "fm \ (fm \ fm) \ fm"
  where
    "qelim (E p) = (\qe. DJ (CJNB qe) (qelim p qe))"
  | "qelim (A p) = (\qe. not (qe ((qelim (Not p) qe))))"
  | "qelim (Not p) = (\qe. not (qelim p qe))"
  | "qelim (And p q) = (\qe. conj (qelim p qe) (qelim q qe))"
  | "qelim (Or p q) = (\qe. disj (qelim p qe) (qelim q qe))"
  | "qelim (Imp p q) = (\qe. imp (qelim p qe) (qelim q qe))"
  | "qelim (Iff p q) = (\qe. iff (qelim p qe) (qelim q qe))"
  | "qelim p = (\y. simpfm p)"

lemma qelim:
  assumes qe_inv: "\bs p. qfree p \ qfree (qe p) \ (Ifm vs bs (qe p) = Ifm vs bs (E p))"
  shows "\ bs. qfree (qelim p qe) \ (Ifm vs bs (qelim p qe) = Ifm vs bs p)"
  using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]]
  by (induct p rule: qelim.induct) auto

subsection \<open>Core Procedure\<close>

fun minusinf:: "fm \ fm" \ \virtual substitution of \-\\\
  where
    "minusinf (And p q) = conj (minusinf p) (minusinf q)"
  | "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
  | "minusinf (Eq (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
  | "minusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
  | "minusinf (Lt (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP (~\<^sub>p c)))"
  | "minusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
  | "minusinf p = p"

fun plusinf:: "fm \ fm" \ \virtual substitution of \+\\\
  where
    "plusinf (And p q) = conj (plusinf p) (plusinf q)"
  | "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
  | "plusinf (Eq (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
  | "plusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
  | "plusinf (Lt (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP c))"
  | "plusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP c))"
  | "plusinf p = p"

lemma minusinf_inf:
  assumes "islin p"
  shows "\z. \x < z. Ifm vs (x#bs) (minusinf p) \ Ifm vs (x#bs) p"
  using assms
proof (induct p rule: minusinf.induct)
  case (1 p q)
  then obtain zp zq where zp: "\x
       and zq: "\x
    by force
  then show ?case
    by (rule_tac x="min zp zq" in exI) auto
next
  case (2 p q)
  then obtain zp zq where zp: "\x
       and zq: "\x
    by force
  then show ?case
    by (rule_tac x="min zp zq" in exI) auto
next
  case (3 c e)
  then have nbe: "tmbound0 e"
    by simp
  from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
    by simp_all
  note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
  let ?c = "Ipoly vs c"
  fix y
  let ?e = "Itm vs (y#bs) e"
  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
  then show ?case
  proof cases
    case 1
    then show ?thesis
      using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto
  next
    case c: 2
    have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
      if "x < -?e / ?c" for x
    proof -
      from that have "?c * x < - ?e"
        using pos_less_divide_eq[OF c, where a="x" and b="-?e"]
        by (simp add: mult.commute)
      then have "?c * x + ?e < 0"
        by simp
      then show ?thesis
        using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto
    qed
    then show ?thesis by auto
  next
    case c: 3
    have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
      if "x < -?e / ?c" for x
    proof -
      from that have "?c * x > - ?e"
        using neg_less_divide_eq[OF c, where a="x" and b="-?e"]
        by (simp add: mult.commute)
      then have "?c * x + ?e > 0"
        by simp
      then show ?thesis
        using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto
    qed
    then show ?thesis by auto
  qed
next
  case (4 c e)
  then have nbe: "tmbound0 e"
    by simp
  from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
    by simp_all
  note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
  let ?c = "Ipoly vs c"
  fix y
  let ?e = "Itm vs (y#bs) e"
  consider "?c = 0" | "?c > 0" | "?c < 0"
    by arith
  then show ?case
  proof cases
    case 1
    then show ?thesis
      using eqs by auto
  next
    case c: 2
    have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
      if "x < -?e / ?c" for x
    proof -
      from that have "?c * x < - ?e"
        using pos_less_divide_eq[OF c, where a="x" and b="-?e"]
        by (simp add: mult.commute)
      then have "?c * x + ?e < 0"
        by simp
      then show ?thesis
        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
    qed
    then show ?thesis by auto
  next
    case c: 3
    have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
      if "x < -?e / ?c" for x
    proof -
      from that have "?c * x > - ?e"
        using neg_less_divide_eq[OF c, where a="x" and b="-?e"]
        by (simp add: mult.commute)
      then have "?c * x + ?e > 0"
        by simp
      then show ?thesis
        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
    qed
    then show ?thesis by auto
  qed
next
  case (5 c e)
  then have nbe: "tmbound0 e"
    by simp
  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
    by simp_all
  then have nc': "allpolys isnpoly (CP (~\<^sub>p c))"
    by (simp add: polyneg_norm)
  note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
  let ?c = "Ipoly vs c"
  fix y
  let ?e = "Itm vs (y#bs) e"
  consider "?c = 0" | "?c > 0" | "?c < 0"
    by arith
  then show ?case
  proof cases
    case 1
    then show ?thesis using eqs by auto
  next
    case c: 2
    have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
      if "x < -?e / ?c" for x
    proof -
      from that have "?c * x < - ?e"
        using pos_less_divide_eq[OF c, where a="x" and b="-?e"]
        by (simp add: mult.commute)
      then have "?c * x + ?e < 0" by simp
      then show ?thesis
        using tmbound0_I[OF nbe, where b="y" and b'="x"] c eqs by auto
    qed
    then show ?thesis by auto
  next
    case c: 3
    have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
      if "x < -?e / ?c" for x
    proof -
      from that have "?c * x > - ?e"
        using neg_less_divide_eq[OF c, where a="x" and b="-?e"]
        by (simp add: mult.commute)
      then have "?c * x + ?e > 0"
        by simp
      then show ?thesis
        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] c by auto
    qed
    then show ?thesis by auto
  qed
next
  case (6 c e)
  then have nbe: "tmbound0 e"
    by simp
  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
    by simp_all
  then have nc': "allpolys isnpoly (CP (~\<^sub>p c))"
    by (simp add: polyneg_norm)
  note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
  let ?c = "Ipoly vs c"
  fix y
  let ?e = "Itm vs (y#bs) e"
  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
  then show ?case
  proof cases
    case 1
    then show ?thesis using eqs by auto
  next
    case c: 2
    have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
      if "x < -?e / ?c" for x
    proof -
      from that have "?c * x < - ?e"
        using pos_less_divide_eq[OF c, where a="x" and b="-?e"]
        by (simp add: mult.commute)
      then have "?c * x + ?e < 0"
        by simp
      then show ?thesis
        using tmbound0_I[OF nbe, where b="y" and b'="x"] c eqs
        by auto
    qed
    then show ?thesis by auto
  next
    case c: 3
    have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
      if "x < -?e / ?c" for x
    proof -
      from that have "?c * x > - ?e"
        using neg_less_divide_eq[OF c, where a="x" and b="-?e"]
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.44 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.