(*  Title:      HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

    Author:     Amine Chaieb

*)

header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}

theory Parametric_Ferrante_Rackoff

imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library

  "~~/src/HOL/Library/Efficient_Nat"

begin

subsection {* Terms *}

datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm 

  | Neg tm | Sub tm tm | CNP nat poly tm

  (* A size for poly to make inductive proofs simpler*)

primrec tmsize :: "tm \<Rightarrow> nat" where

  "tmsize (CP c) = polysize c"

| "tmsize (Bound n) = 1"

| "tmsize (Neg a) = 1 + tmsize a"

| "tmsize (Add a b) = 1 + tmsize a + tmsize b"

| "tmsize (Sub a b) = 3 + tmsize a + tmsize b"

| "tmsize (Mul c a) = 1 + polysize c + tmsize a"

| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "

  (* Semantics of terms tm *)

primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> '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 \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool"  where

  "allpolys P (CP c) = P c"

| "allpolys P (CNP n c p) = (P c \<and> allpolys P p)"

| "allpolys P (Mul c p) = (P c \<and> allpolys P p)"

| "allpolys P (Neg p) = allpolys P p"

| "allpolys P (Add p q) = (allpolys P p \<and> allpolys P q)"

| "allpolys P (Sub p q) = (allpolys P p \<and> allpolys P q)"

| "allpolys P p = True"

primrec tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool" where

  "tmboundslt n (CP c) = True"

| "tmboundslt n (Bound m) = (m < n)"

| "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"

| "tmboundslt n (Neg a) = tmboundslt n a"

| "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"

| "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 

| "tmboundslt n (Mul i a) = tmboundslt n a"

primrec tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *) where

  "tmbound0 (CP c) = True"

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

| "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"

| "tmbound0 (Neg a) = tmbound0 a"

| "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"

| "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 

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

lemma tmbound0_I:

  assumes nb: "tmbound0 a"

  shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"

using nb

by (induct a rule: tm.induct,auto)

primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where

  "tmbound n (CP c) = True"

| "tmbound n (Bound m) = (n \<noteq> m)"

| "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"

| "tmbound n (Neg a) = tmbound n a"

| "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"

| "tmbound n (Sub a b) = (tmbound n a \<and> 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 \<le> 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 \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> tm \<Rightarrow> 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 \<Rightarrow> 'a list \<Rightarrow> 'a list" where

  "removen n [] = []"

| "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"

lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs"

  by (induct xs arbitrary: n, auto)

lemma nth_length_exceeds: "n \<ge> length xs \<Longrightarrow> xs!n = []!(n - length xs)"

  by (induct xs arbitrary: n, auto)

lemma removen_length: "length (removen n xs) = (if n \<ge> 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 thus ?case by simp

next

  case (Cons x xs n m)

  {assume nxs: "n \<ge> length (x#xs)" hence ?case using removen_same[OF nxs] by simp}

  moreover

  {assume nxs: "\<not> (n \<ge> length (x#xs))" 

    {assume mln: "m < n" hence ?case using Cons by (cases m, auto)}

    moreover

    {assume mln: "\<not> (m < n)" 

      {assume mxs: "m \<le> length (x#xs)" hence ?case using Cons by (cases m, auto)}

      moreover

      {assume mxs: "\<not> (m \<le> length (x#xs))" 

        have th: "length (removen n (x#xs)) = length xs" 

          using removen_length[where n="n" and xs="x#xs"] nxs by simp

        with mxs have mxs':"m \<ge> length (removen n (x#xs))" by auto

        hence "(removen n (x#xs))!m = [] ! (m - length xs)" 

          using th nth_length_exceeds[OF mxs'] by auto

        hence th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))" 

          by auto

        hence ?case using nxs mln mxs by auto }

      ultimately have ?case by blast

    }

    ultimately have ?case by blast

  } ultimately show ?case by blast

qed

lemma decrtm: assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound m t" 

  and nle: "m \<le> 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 add: removen_nth)

primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> 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:

  shows "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 \<Longrightarrow> tmbound0 (tmsubst0 t a)"

  by (induct a rule: tm.induct) auto

primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> 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 \<le> 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 \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"

  by (induct t, auto)

  (* Simplification *)

consts

  tmadd:: "tm \<times> tm \<Rightarrow> tm"

recdef tmadd "measure (\<lambda> (t,s). size t + size s)"

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

apply (induct t s rule: tmadd.induct, simp_all add: Let_def)

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

apply (case_tac "n1 = n2", simp_all add: field_simps)

apply (simp only: right_distrib[symmetric]) 

by (auto simp del: polyadd simp add: polyadd[symmetric])

lemma tmadd_nb0[simp]: "\<lbrakk> tmbound0 t ; tmbound0 s\<rbrakk> \<Longrightarrow> tmbound0 (tmadd (t,s))"

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

lemma tmadd_nb[simp]: "\<lbrakk> tmbound n t ; tmbound n s\<rbrakk> \<Longrightarrow> tmbound n (tmadd (t,s))"

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

lemma tmadd_blt[simp]: "\<lbrakk>tmboundslt n t ; tmboundslt n s\<rbrakk> \<Longrightarrow> tmboundslt n (tmadd (t,s))"

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

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

fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm" where

  "tmmul (CP j) = (\<lambda> i. CP (i *\<^sub>p j))"

| "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))"

| "tmmul t = (\<lambda> 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 \<Longrightarrow> tmbound0 (tmmul t i)"

by (induct t arbitrary: i rule: tmmul.induct, auto )

lemma tmmul_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmmul t i)"

by (induct t arbitrary: n rule: tmmul.induct, auto )

lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)"

by (induct t arbitrary: i rule: tmmul.induct, auto simp add: Let_def)

lemma tmmul_allpolys_npoly[simp]: 

  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"

  shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)" by (induct t rule: tmmul.induct, simp_all add: Let_def polymul_norm)

definition tmneg :: "tm \<Rightarrow> tm" where

  "tmneg t \<equiv> tmmul t (C (- 1,1))"

definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm" where

  "tmsub s t \<equiv> (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] 

apply simp

apply (subst number_of_Min)

apply (simp only: of_int_minus)

apply simp

done

lemma tmneg_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmneg t)"

using tmneg_def by simp

lemma tmneg_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmneg t)"

using tmneg_def by simp

lemma tmneg_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmneg t)"

using tmneg_def by simp

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

lemma tmneg_allpolys_npoly[simp]: 

  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"

  shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)" 

  unfolding tmneg_def by auto

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

using tmsub_def by simp

lemma tmsub_nb0[simp]: "\<lbrakk> tmbound0 t ; tmbound0 s\<rbrakk> \<Longrightarrow> tmbound0 (tmsub t s)"

using tmsub_def by simp

lemma tmsub_nb[simp]: "\<lbrakk> tmbound n t ; tmbound n s\<rbrakk> \<Longrightarrow> tmbound n (tmsub t s)"

using tmsub_def by simp

lemma tmsub_blt[simp]: "\<lbrakk>tmboundslt n t ; tmboundslt n s\<rbrakk> \<Longrightarrow> tmboundslt n (tmsub t s )"

using tmsub_def by simp

lemma tmsub_allpolys_npoly[simp]: 

  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"

  shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)" 

  unfolding tmsub_def by (simp add: isnpoly_def)

fun simptm:: "tm \<Rightarrow> 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, field_inverse_zero})"

  shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{field_char_0, field_inverse_zero})" 

apply (subst polynate[symmetric])

apply simp

done

lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t"

by (induct t rule: simptm.induct, auto simp add: tmneg tmadd tmsub tmmul Let_def polynate_stupid) 

lemma simptm_tmbound0[simp]: 

  "tmbound0 t \<Longrightarrow> tmbound0 (simptm t)"

by (induct t rule: simptm.induct, auto simp add: Let_def)

lemma simptm_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (simptm t)"

by (induct t rule: simptm.induct, auto simp add: Let_def)

lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)"

by (induct t rule: simptm.induct, auto simp add: 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, field_inverse_zero})"

  shows "allpolys isnpoly (simptm p)"

  by (induct p rule: simptm.induct, auto simp add: Let_def)

declare let_cong[fundef_cong del]

fun split0 :: "tm \<Rightarrow> (poly \<times> 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]: "\<exists>x y. (x,y) = split0 p"

  apply (rule exI[where x="fst (split0 p)"])

  apply (rule exI[where x="snd (split0 p)"])

  by simp

lemma split0:

  "tmbound 0 (snd (split0 t)) \<and> (Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t)"

  apply (induct t rule: split0.induct)

  apply simp

  apply (simp add: Let_def split_def field_simps)

  apply (simp add: Let_def split_def field_simps)

  apply (simp add: Let_def split_def field_simps)

  apply (simp add: Let_def split_def field_simps)

  apply (simp add: Let_def split_def field_simps)

  apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric])

  apply (simp add: Let_def split_def field_simps)

  apply (simp add: Let_def split_def field_simps)

  done

lemma split0_ci: "split0 t = (c',t') \<Longrightarrow> Itm vs bs t = Itm vs bs (CNP 0 c' t')"

proof-

  fix c' t'

  assume "split0 t = (c', t')" hence "c' = fst (split0 t)" and "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, field_inverse_zero})"

  shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"

proof-

  fix c' t'

  assume "split0 t = (c', t')" hence "c' = fst (split0 t)" and "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, field_inverse_zero})"

  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 add: Let_def split_def split0_stupid)

lemma split0_blt: assumes nb:"tmboundslt n t" shows "tmboundslt n (snd (split0 t))"

  using nb by (induct t rule: split0.induct, auto simp add: Let_def split_def split0_stupid)

lemma tmbound_split0: "tmbound 0 t \<Longrightarrow> Ipoly vs (fst(split0 t)) = 0"

 by (induct t rule: split0.induct, auto simp add: Let_def split_def split0_stupid)

lemma tmboundslt_split0: "tmboundslt n t \<Longrightarrow> Ipoly vs (fst(split0 t)) = 0 \<or> n > 0"

by (induct t rule: split0.induct, auto simp add: Let_def split_def split0_stupid)

lemma tmboundslt0_split0: "tmboundslt 0 t \<Longrightarrow> Ipoly vs (fst(split0 t)) = 0"

 by (induct t rule: split0.induct, auto simp add: Let_def split_def split0_stupid)

lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"

by (induct p rule: split0.induct, auto simp  add: isnpoly_def Let_def split_def split0_stupid)

lemma isnpoly_fst_split0:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"

  shows 

  "allpolys isnpoly p \<Longrightarrow> 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 split0_stupid)

subsection{* Formulae *}

datatype 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

  (* A size for fm *)

fun fmsize :: "fm \<Rightarrow> nat" 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 p = 1"

  (* several lemmas about fmsize *)

lemma fmsize_pos[termination_simp]: "fmsize p > 0"        

by (induct p rule: fmsize.induct) simp_all

  (* Semantics of formulae (fm) *)

primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> 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 \<le> 0)"

| "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"

| "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"

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

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

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

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

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

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

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

fun not:: "fm \<Rightarrow> 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 \<Rightarrow> fm \<Rightarrow> fm" where

  "conj p q \<equiv> (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 \<or> q=F",simp_all add: conj_def) (cases p,simp_all)

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

  "disj p q \<equiv> (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 \<or> q=T",simp_all add: disj_def) (cases p,simp_all)

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

  "imp p q \<equiv> (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 \<or> q=T",simp_all add: imp_def) 

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

  "iff p q \<equiv> (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)

  (* Quantifier freeness *)

fun qfree:: "fm \<Rightarrow> bool" 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"

  (* Boundedness and substitution *)

primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> 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 \<and> boundslt n q)"

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

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

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

| "boundslt n (E p) = boundslt (Suc n) p"

| "boundslt n (A p) = boundslt (Suc n) p"

fun bound0:: "fm \<Rightarrow> 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 \<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 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 \<Rightarrow> fm \<Rightarrow> 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 \<and> bound m q)"

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

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

| "bound m (Iff p q) = (bound m p \<and> 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 \<le> 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) 

  {fix y

    from E have bnd: "boundslt (length (y#bs)) p" 

      and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+

    from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }

  thus ?case by simp 

next

  case (A p bs n) {fix y

    from A have bnd: "boundslt (length (y#bs)) p" 

      and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+

    from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }

  thus ?case by simp 

qed auto

fun decr0 :: "fm \<Rightarrow> 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 nb: "bound0 p"

  shows "Ifm vs (x#bs) p = Ifm vs bs (decr0 p)"

  using nb 

  by (induct p rule: decr0.induct, simp_all add: decrtm0)

primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> 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) 

  {fix x

    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] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".

  } thus ?case by auto 

next

  case (A p bs m)  

  {fix x

    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] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".

  } thus ?case by auto

qed (auto simp add: decrtm removen_nth)

primrec subst0:: "tm \<Rightarrow> fm \<Rightarrow> 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 \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> 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 \<le> 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) 

  {fix x 

    from E have bn: "boundslt (length (x#bs)) p" by simp 

    from E have nlm: "Suc n \<le> 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 

    hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"

    by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }  

thus ?case by simp 

next

  case (A p bs n)   

  {fix x 

    from A have bn: "boundslt (length (x#bs)) p" by simp 

    from A have nlm: "Suc n \<le> 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 

    hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"

    by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }  

thus ?case by simp 

qed(auto simp add: tmsubst)

lemma subst_nb: assumes tnb: "tmbound m t"

shows "bound m (subst m t p)"

using tnb tmsubst_nb incrtm0_tmbound

by (induct p arbitrary: m t rule: fm.induct, auto)

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

by (induct p rule: not.induct, auto)

lemma not_bn0[simp]: "bound0 p \<Longrightarrow> bound0 (not p)"

by (induct p rule: not.induct, auto)

lemma not_nb[simp]: "bound n p \<Longrightarrow> bound n (not p)"

by (induct p rule: not.induct, auto)

lemma not_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n (not p)"

 by (induct p rule: not.induct, auto)

lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"

using conj_def by auto 

lemma conj_nb0[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"

using conj_def by auto 

lemma conj_nb[simp]: "\<lbrakk>bound n p ; bound n q\<rbrakk> \<Longrightarrow> bound n (conj p q)"

using conj_def by auto 

lemma conj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)"

using conj_def by auto 

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

using disj_def by auto 

lemma disj_nb0[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"

using disj_def by auto 

lemma disj_nb[simp]: "\<lbrakk>bound n p ; bound n q\<rbrakk> \<Longrightarrow> bound n (disj p q)"

using disj_def by auto 

lemma disj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (disj p q)"

using disj_def by auto 

lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"

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

lemma imp_nb0[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"

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

lemma imp_nb[simp]: "\<lbrakk>bound n p ; bound n q\<rbrakk> \<Longrightarrow> bound n (imp p q)"

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

lemma imp_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (imp p q)"

using imp_def by auto 

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

  by (unfold iff_def,cases "p=q", auto)

lemma iff_nb0[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"

using iff_def by (unfold iff_def,cases "p=q", auto)

lemma iff_nb[simp]: "\<lbrakk>bound n p ; bound n q\<rbrakk> \<Longrightarrow> bound n (iff p q)"

using iff_def by (unfold iff_def,cases "p=q", auto)

lemma iff_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (iff p q)"

using iff_def by auto 

lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 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 (Eq a) = True"

| "isatom (NEq a) = True"

| "isatom p = False"

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 \<equiv> (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 \<equiv> foldr (djf f) ps F"

lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs 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 vs bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm vs 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 vs bs q) = Ifm vs bs p"

by(induct p rule: disjuncts.induct, auto)

lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"

proof-

  assume nb: "bound0 p"

  hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)

  thus ?thesis by (simp only: list_all_iff)

qed

lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"

proof-

  assume qf: "qfree p"

  hence "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 \<equiv> evaldjf f (disjuncts p)"

lemma DJ: assumes fdj: "\<forall> 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) = (\<exists> q \<in> set (disjuncts p). Ifm vs bs (f q))"

    by (simp add: DJ_def evaldjf_ex) 

  also have "\<dots> = Ifm vs 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 vs bs (qe p) = Ifm vs bs (E p))"

  shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (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: "\<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 vs bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm vs bs (qe q))"

    by (simp add: DJ_def evaldjf_ex)

  also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm vs bs (E q))" using qe disjuncts_qf[OF qf] by auto

  also have "\<dots> = Ifm vs bs (E p)" by (induct p rule: disjuncts.induct, auto)

  finally show "qfree (DJ qe p) \<and> Ifm vs bs (DJ qe p) = Ifm vs bs (E p)" using qfth by blast

qed

fun conjuncts :: "fm \<Rightarrow> fm list" where

  "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"

| "conjuncts T = []"

| "conjuncts p = [p]"

definition list_conj :: "fm list \<Rightarrow> fm" where

  "list_conj ps \<equiv> foldr conj ps T"

definition CJNB :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where

  "CJNB f p \<equiv> (let cjs = conjuncts p ; (yes,no) = partition bound0 cjs

                   in conj (decr0 (list_conj yes)) (f (list_conj no)))"

lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). qfree q"

proof-

  assume qf: "qfree p"

  hence "list_all qfree (conjuncts p)"

    by (induct p rule: conjuncts.induct, auto)

  thus ?thesis by (simp only: list_all_iff)

qed

lemma conjuncts: "(\<forall> q\<in> set (conjuncts p). Ifm vs bs q) = Ifm vs bs p"

by(induct p rule: conjuncts.induct, auto)

lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). bound0 q"

proof-

  assume nb: "bound0 p"

  hence "list_all bound0 (conjuncts p)" by (induct p rule:conjuncts.induct,auto)

  thus ?thesis by (simp only: list_all_iff)

qed

fun islin :: "fm \<Rightarrow> bool" where

  "islin (And p q) = (islin p \<and> islin q \<and> p \<noteq> T \<and> p \<noteq> F \<and> q \<noteq> T \<and> q \<noteq> F)"

| "islin (Or p q) = (islin p \<and> islin q \<and> p \<noteq> T \<and> p \<noteq> F \<and> q \<noteq> T \<and> q \<noteq> F)"

| "islin (Eq (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"

| "islin (NEq (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"

| "islin (Lt (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"

| "islin (Le (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> 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, case_tac nat, auto)+

definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"

definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"

definition eq where "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"

definition "neq p = not (eq p)"

lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"

  apply(simp add: lt_def)

  apply(cases p, simp_all)

  apply (case_tac poly, simp_all add: isnpoly_def)

  done

lemma le: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (le p) = Ifm vs bs (Le p)"

  apply(simp add: le_def)

  apply(cases p, simp_all)

  apply (case_tac poly, simp_all add: isnpoly_def)

  done

lemma eq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (eq p) = Ifm vs bs (Eq p)"

  apply(simp add: eq_def)

  apply(cases p, simp_all)

  apply (case_tac poly, simp_all add: isnpoly_def)

  done

lemma neq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (neq p) = Ifm vs bs (NEq p)"

  by(simp add: neq_def eq)

lemma lt_lin: "tmbound0 p \<Longrightarrow> islin (lt p)"

  apply (simp add: lt_def)

  apply (cases p, simp_all)

  apply (case_tac poly, simp_all)

  apply (case_tac nat, simp_all)

  done

lemma le_lin: "tmbound0 p \<Longrightarrow> islin (le p)"

  apply (simp add: le_def)

  apply (cases p, simp_all)

  apply (case_tac poly, simp_all)

  apply (case_tac nat, simp_all)

  done

lemma eq_lin: "tmbound0 p \<Longrightarrow> islin (eq p)"

  apply (simp add: eq_def)

  apply (cases p, simp_all)

  apply (case_tac poly, simp_all)

  apply (case_tac nat, simp_all)

  done

lemma neq_lin: "tmbound0 p \<Longrightarrow> islin (neq p)"

  apply (simp add: neq_def eq_def)

  apply (cases p, simp_all)

  apply (case_tac poly, simp_all)

  apply (case_tac nat, simp_all)

  done

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, field_inverse_zero})"

  shows "islin (simplt t)"

  unfolding simplt_def 

  using split0_nb0'

by (auto simp add: 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, field_inverse_zero})"

  shows "islin (simple t)"

  unfolding simple_def 

  using split0_nb0'

by (auto simp add: 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, field_inverse_zero})"

  shows "islin (simpeq t)"

  unfolding simpeq_def 

  using split0_nb0'

by (auto simp add: 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, field_inverse_zero})"

  shows "islin (simpneq t)"

  unfolding simpneq_def 

  using split0_nb0'

by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin)

lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"

  by (cases "split0 s", auto)

lemma split0_npoly:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"

  and n: "allpolys isnpoly t"

  shows "isnpoly (fst (split0 t))" and "allpolys isnpoly (snd (split0 t))"

  using n

  by (induct t rule: split0.induct, auto simp add: Let_def split_def polyadd_norm polymul_norm polyneg_norm polysub_norm really_stupid)

lemma simplt[simp]:

  shows "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)"

proof-

  have n: "allpolys isnpoly (simptm t)" by simp

  let ?t = "simptm t"

  {assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis

      using split0[of "simptm t" vs bs] lt[OF split0_npoly(2)[OF n], of vs bs]

      by (simp add: simplt_def Let_def split_def lt)}

  moreover

  {assume "fst (split0 ?t) \<noteq> 0\<^sub>p"

    hence ?thesis using  split0[of "simptm t" vs bs] by (simp add: simplt_def Let_def split_def)

  }

  ultimately show ?thesis by blast

qed

lemma simple[simp]:

  shows "Ifm vs bs (simple t) = Ifm vs bs (Le t)"

proof-

  have n: "allpolys isnpoly (simptm t)" by simp

  let ?t = "simptm t"

  {assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis

      using split0[of "simptm t" vs bs] le[OF split0_npoly(2)[OF n], of vs bs]

      by (simp add: simple_def Let_def split_def le)}