# Theory PolyAtoms

section "Atoms"
theory PolyAtoms
imports ExecutiblePolyProps
begin

subsection "Definition"

datatype (atoms: 'a) fm =
TrueF | FalseF | Atom 'a | And "'a fm" "'a fm" | Or "'a fm" "'a fm" |
Neg "'a fm" | ExQ "'a fm" | AllQ "'a fm" | ExN "nat" "'a fm" | AllN "nat" "'a fm"

definition neg where
"neg φ = (if φ=TrueF then FalseF else if φ=FalseF then TrueF else Neg φ)"

definition "and" :: "'a fm ⇒ 'a fm ⇒ 'a fm" where
"and φ⇩1 φ⇩2 =
(if φ⇩1=TrueF then φ⇩2 else if φ⇩2=TrueF then φ⇩1 else
if φ⇩1=FalseF ∨ φ⇩2=FalseF then FalseF else And φ⇩1 φ⇩2)"

definition or :: "'a fm ⇒ 'a fm ⇒ 'a fm" where
"or φ⇩1 φ⇩2 =
(if φ⇩1=FalseF then φ⇩2 else if φ⇩2=FalseF then φ⇩1 else
if φ⇩1=TrueF ∨ φ⇩2=TrueF then TrueF else Or φ⇩1 φ⇩2)"

definition list_conj :: "'a fm list ⇒ 'a fm" where
"list_conj fs = foldr and fs TrueF"

definition list_disj :: "'a fm list ⇒ 'a fm" where
"list_disj fs = foldr or fs FalseF"

text "
The atom datatype corresponds to the defined in Tobias's LinearQuantifierElim.
"

datatype atom = Less "real mpoly" | Eq "real mpoly" | Leq "real mpoly" | Neq "real mpoly"

text
"
For each atom, the real mpoly corresponds to a polynomial from the Polynomials library where
we allow for real valued coefficients.

The variables in the polynomials are in De Bruijn notation where variable 0 corresponds to the
variable of the innermost quantifier, then variable 1 is the next quantifier out from that, and
so on. Any variable number greater than the number of quantifiers is a free variable. This means
that we have a list of infinite free variables we can pick from and if we want to refer to the
ith free variable (indexed at 0)  within an atom that is bound in j quantifiers, then we would use
var (i+j).

The polynomials are all standardized so that they are compared to a 0 on the right. This means
the atom Less p corresponds to $p\\leq0$ and the atom Eq p corresponds to $p=0$ and so on. This
restriction doesn't lose any generality and having all 4 of these kinds of atoms prevents loss
of efficiency as the negation of these atoms do not introduce additional logical connectives. The
following aNeg function demonstrates this.
"

fun aNeg :: "atom ⇒ atom" where
"aNeg (Less p) = Leq (-p)" |
"aNeg (Eq p) = Neq p" |
"aNeg (Leq p) = Less (-p)" |
"aNeg (Neq p) = Eq p"

subsection "Evaluation"

text "
In order to do any proofs with these atoms, we need a method of comparing two atoms to check if they
are equal. Instead of trying to manipulate the polynomials to a standard form to compare them, it
is a lot easier to plug in values for every variable and check if the results are equal. If every
single real value input for each variable matches in truth value for both atoms, then they are equal.

aEval a l corresponds to plugging in the real value list l into the variables of atom a and then
evaluating the truth value of it
"
fun aEval :: "atom ⇒ real list ⇒ bool" where
"aEval (Eq p) L = (insertion (nth_default 0 L) p = 0)" |
"aEval (Less p) L = (insertion (nth_default 0 L) p < 0)" |
"aEval (Leq p) L = (insertion (nth_default 0 L) p ≤ 0)" |
"aEval (Neq p) L = (insertion (nth_default 0 L) p ≠ 0)"

text "
aNeg\\_aEval shows the general format for how things are proven equal. Plugging in the values to an
original atom a will results in the opposite truth value if we transformed with the aNeg function.
"
lemma aNeg_aEval : "aEval a L ⟷ (¬ aEval (aNeg a) L)"
apply(cases a)
apply(auto)
apply(smt insertionNegative)
apply(smt insertionNegative)
apply(smt insertionNegative)
apply(smt insertionNegative)
done

text "
We can extend this to formulas instead of just atoms. Given a formula in prenex normal form,
we simply iterate through and apply the quantifiers
"

fun eval :: "atom fm ⇒ real list ⇒ bool" where
"eval (Atom a) Γ = aEval a Γ" |
"eval (TrueF) _ = True" |
"eval (FalseF) _ = False" |
"eval (And φ ψ) Γ = ((eval φ Γ) ∧ (eval ψ Γ))" |
"eval (Or φ ψ) Γ = ((eval φ Γ) ∨ (eval ψ Γ))" |
"eval (Neg φ) Γ = (¬ (eval φ Γ))" |
"eval (ExQ φ) Γ = (∃x. (eval φ (x#Γ)))" |
"eval (AllQ φ) Γ = (∀x. (eval φ (x#Γ)))"|
"eval (AllN i φ) Γ = (∀l. length l = i ⟶ (eval φ (l @ Γ)))"|
"eval (ExN i φ) Γ = (∃l. length l = i ∧ (eval φ (l @ Γ)))"

lemma "eval (ExQ (Or (Atom A) (Atom B))) xs =  eval (Or (ExQ(Atom A)) (ExQ(Atom B))) xs"
by(auto)

lemma eval_neg_neg : "eval (neg (neg f)) L ⟷ eval f L"

lemma eval_neg : "(¬ eval (neg f) L) ⟷ eval f L"

lemma eval_and : "eval (and a b) L ⟷ (eval a L ∧ eval b L)"

lemma eval_or : "eval (or a b) L ⟷ (eval a L ∨ eval b L)"

lemma eval_Or : "eval (Or a b) L ⟷ (eval a L ∨ eval b L)"
by (simp)

lemma eval_And : "eval (And a b) L ⟷ (eval a L ∧ eval b L)"
by (simp)

lemma eval_not : "eval (neg a) L ⟷ ¬(eval a L)"

lemma eval_true : "eval TrueF L"
by simp

lemma eval_false : "¬(eval FalseF L)"
by simp

lemma eval_Neg : "eval (Neg φ) L = eval (neg φ) L"

lemma eval_Neg_Neg : "eval (Neg (Neg φ)) L = eval φ L"

lemma eval_Neg_And : "eval (Neg (And φ ψ)) L = eval (Or (Neg φ) (Neg ψ)) L"
by simp

lemma aEval_leq : "aEval (Leq p) L = (aEval (Less p) L ∨ aEval (Eq p) L)"
by auto

text "This function is misleading because it is true iff
the variable given doesn't occur as a free variable in the atom fm"
fun freeIn :: "nat ⇒ atom fm ⇒ bool" where
"freeIn var (Atom(Eq p)) = (var ∉ (vars p))"|
"freeIn var (Atom(Less p)) = (var ∉ (vars p))"|
"freeIn var (Atom(Leq p)) = (var ∉ (vars p))"|
"freeIn var (Atom(Neq p)) = (var ∉ (vars p))"|
"freeIn var (TrueF) = True"|
"freeIn var (FalseF) = True"|
"freeIn var (And a b) = ((freeIn var a) ∧ (freeIn var b))"|
"freeIn var (Or a b) = ((freeIn var a) ∧ (freeIn var b))"|
"freeIn var (Neg a) = freeIn var a"|
"freeIn var (ExQ a) = freeIn (var+1) a"|
"freeIn var (AllQ a) = freeIn (var+1) a"|
"freeIn var (AllN i a) = freeIn (var+i) a"|
"freeIn var (ExN i a) = freeIn (var+i) a"

fun liftmap :: "(nat ⇒ atom ⇒ atom fm) ⇒ atom fm ⇒ nat ⇒ atom fm" where
"liftmap f TrueF var = TrueF"|
"liftmap f FalseF var = FalseF"|
"liftmap f (Atom a) var = f var a"|
"liftmap f (And φ ψ) var = And (liftmap f φ var) (liftmap f ψ var)"|
"liftmap f (Or φ ψ) var = Or (liftmap f φ var) (liftmap f ψ var)"|
"liftmap f (Neg φ) var = Neg (liftmap f φ var)"|
"liftmap f (ExQ φ) var = ExQ (liftmap f φ (var+1))"|
"liftmap f (AllQ φ) var = AllQ (liftmap f φ (var+1))"|
"liftmap f (AllN i φ) var = AllN i (liftmap f φ (var+i))"|
"liftmap f (ExN i φ) var = ExN i (liftmap f φ (var+i))"

(*
fun greatestFreeVariable :: "atom fm ⇒ nat option" where
"greatestFreeVariable F = None"

fun is_closed :: "atom fm ⇒ real list ⇒ bool" where
"is_closed F xs = (case greatestFreeVariable F of Some x ⇒ (x = length xs) | None ⇒ (0=length xs))"
*)

fun depth :: "'a fm ⇒ nat"where
"depth TrueF = 1"|
"depth FalseF = 1"|
"depth (Atom _) = 1"|
"depth (And φ ψ) = max (depth φ) (depth ψ) + 1"|
"depth (Or φ ψ) = max (depth φ) (depth ψ) + 1"|
"depth (Neg φ) = depth φ + 1"|
"depth (ExQ φ) = depth φ + 1"|
"depth (AllQ φ) = depth φ + 1"|
"depth (AllN i φ) = depth φ + 1"|
"depth (ExN i φ) = depth φ + 1"

value "AllQ (And
(ExQ (Atom (Eq (Var 1 * Var 2 - (Var 0)^2 * Var 3))))
(Neg (AllQ (Atom (Leq (Const 5 * (Var 1)^2 - Var 0)))))
)"

fun negation_free :: "atom fm ⇒ bool" where
"negation_free TrueF = True" |
"negation_free FalseF = True " |
"negation_free (Atom a) = True" |
"negation_free (And φ⇩1 φ⇩2) = ((negation_free φ⇩1) ∧ (negation_free φ⇩2))" |
"negation_free (Or φ⇩1 φ⇩2) = ((negation_free φ⇩1) ∧ (negation_free φ⇩2))" |
"negation_free (ExQ φ) = negation_free φ" |
"negation_free (AllQ φ) = negation_free φ" |
"negation_free (AllN i φ) = negation_free φ" |
"negation_free (ExN i φ) = negation_free φ" |
"negation_free (Neg _) = False"

subsection "Useful Properties"

lemma sum_eq : "eval (Atom(Eq p)) L ⟶ eval (Atom(Eq q)) L ⟶ eval (Atom(Eq(p + q))) L"

lemma freeIn_list_conj : "(∀f∈set(F). freeIn var f) ⟹ freeIn var (list_conj F)"
proof(induct F)
case Nil
then show ?case by(simp add: list_conj_def)
next
case (Cons a F)
then show ?case by (simp add: PolyAtoms.and_def list_conj_def)
qed

lemma freeIn_list_disj :
assumes "∀f∈set (L::atom fm list). freeIn var f"
shows "freeIn var (list_disj L)"
using assms
proof(induction L)
case Nil
then show ?case unfolding list_disj_def  by auto
next
case (Cons a L)
then show ?case unfolding list_disj_def or_def by simp
qed

lemma var_not_in_aEval : "freeIn var (Atom φ) ⟹ (∃x. aEval φ (list_update L var x)) = (∀x. aEval φ (list_update L var x))"
proof(induction φ)
case (Less p)
then show ?case
apply(auto)
using not_contains_insertion
by metis
next
case (Eq p)
then show ?case
apply(auto)
using not_contains_insertion
by blast
next
case (Leq p)
then show ?case
apply(auto)
using not_contains_insertion
by metis
next
case (Neq p)
then show ?case
apply(auto)
using not_contains_insertion
by metis
qed

lemma var_not_in_aEval2 : "freeIn 0 (Atom φ) ⟹ (∃x. aEval φ (x#L)) = (∀x. aEval φ (x#L))"
by (metis list_update_code(2) var_not_in_aEval)

lemma plugInLinear :
assumes lLength : "length L>var"
assumes nonzero : "B≠0"
assumes hb : "∀v. insertion (nth_default 0 (list_update L var v)) b = B"
assumes hc : "∀v. insertion (nth_default 0 (list_update L var v)) c = C"
shows "aEval (Eq(b*Var var + c)) (list_update L var (-C/B))"

subsection "Some eval results"
lemma doubleExist : "eval (ExN 2 A) L = eval (ExQ (ExQ A)) L"
apply(simp)
proof(safe)
fix l
assume h : "length l = 2" "eval A (l @ L)"
show "∃x xa. eval A (xa # x # L)"
proof(cases l)
case Nil
then show ?thesis using h by auto
next
case (Cons a list)
then have Cons' : "l = a # list" by auto
then show ?thesis proof(cases list)
case Nil
then show ?thesis using h Cons  by auto
next
case (Cons b list)
show ?thesis
apply(rule exI[where x=b])apply(rule exI[where x=a])
using h Cons' Cons  by auto
qed
qed
next
fix x xa
assume h : "eval A (xa # x # L)"
show "∃l. length l = 2 ∧ eval A (l @ L)"
apply(rule exI[where x="[xa,x]"]) using h by simp
qed

lemma doubleForall : "eval (AllN 2 A) L = eval (AllQ (AllQ A)) L"
apply(simp)using doubleExist eval_neg by fastforce

lemma unwrapExist : "eval (ExN (j + 1) A) L = eval (ExQ (ExN j A)) L"
apply simp
apply safe
subgoal for l
apply(rule exI[where x="nth l j"])
apply(rule exI[where x="take j l"])
apply auto
by (metis Cons_nth_drop_Suc append.assoc append_Cons append_eq_append_conv_if append_take_drop_id lessI)
subgoal for x l
apply(rule exI[where x="l @ [x]"])
by auto
done

lemma unwrapExist' : "eval (ExN (j + 1) A) L =  eval (ExN j (ExQ A)) L"
apply simp
apply safe
subgoal for l
apply(rule exI[where x="drop 1 l"])
apply auto
apply(rule exI[where x="nth l 0"])
by (metis Cons_nth_drop_Suc append_Cons drop0 zero_less_Suc)
subgoal for l x
apply(rule exI[where x="x#l"])
by auto
done

lemma unwrapExist'' : "eval (ExN (i + j) A) L = eval (ExN i(ExN j A)) L"
apply simp
apply safe
subgoal for l
apply(rule exI[where x="drop j l"])
apply auto
apply(rule exI[where x="take j l"])
apply auto
by (metis append.assoc append_take_drop_id)
subgoal for l la
apply(rule exI[where x="la@l"])
by auto
done

lemma unwrapForall : "eval (AllN (j + 1) A) L = eval (AllQ (AllN j A)) L"
using unwrapExist[of j "neg A" L] eval_neg by fastforce

lemma unwrapForall' : "eval (AllN (j + 1) A) L =  eval (AllN j (AllQ A)) L"
using unwrapExist'[of j "neg A" L] eval_neg by fastforce

lemma unwrapForall'' : "eval (AllN (i + j) A) L = eval (AllN i(AllN j A)) L"
using unwrapExist''[of i j "neg A" L] eval_neg by fastforce

lemma var_not_in_eval : "∀var. ∀L. (freeIn var φ ⟶ ((∃x. eval φ (list_update L var x)) = (∀x. eval φ (list_update L var x))))"
proof(induction φ)
case TrueF
then show ?case by(auto)
next
case FalseF
then show ?case by(auto)
next
case (Atom x)
then show ?case
using var_not_in_aEval eval.simps(1) by blast
next
case (And φ1 φ2)
then show ?case by (meson eval.simps(4) freeIn.simps(7))
next
case (Or φ1 φ2)
then show ?case by fastforce
next
case (Neg φ)
then show ?case by (meson eval.simps(6) freeIn.simps(9))
next
case (ExQ φ)
fix xa L var x
have  "(xa::real) # L[var := x] = (xa#L)[var+1:=x]"
by simp
then show ?case using ExQ
by (metis Suc_eq_plus1 eval.simps(7) freeIn.simps(10) list_update_code(3))
next
case (AllQ φ)
fix xa L var x
have  "(xa::real) # L[var := x] = (xa#L)[var+1:=x]"
by simp
then show ?case using AllQ
by (metis Suc_eq_plus1 eval.simps(8) freeIn.simps(11) list_update_code(3))
next
case (ExN i φ)
{fix xa L var x
assume "length (xa::real list) = i"
have  "xa @ L[var := x] = (xa@L)[var+i:=x]"
by (simp add: ‹length xa = i› list_update_append)
}
then show ?case using ExN
by (metis eval.simps(10) freeIn.simps(13))
next
case (AllN i φ)
{fix xa L var x
assume "length (xa::real list) = i"
have  "xa @ L[var := x] = (xa@L)[var+i:=x]"
by (simp add: ‹length xa = i› list_update_append)
}
then show ?case using AllN
by (metis eval.simps(9) freeIn.simps(12))
qed

lemma var_not_in_eval2 : "∀L. (freeIn 0 φ ⟶ ((∃x. eval φ (x#L)) = (∀x. eval φ (x#L))))"
by (metis list_update_code(2) var_not_in_eval)

lemma var_not_in_eval3 :
assumes "freeIn var φ"
assumes "length xs' = var"
shows "((∃x. eval φ (xs'@x#L)) = (∀x. eval φ (xs'@x#L)))"
using assms
by (metis list_update_length var_not_in_eval)

lemma eval_list_conj : "eval (list_conj F) L = (∀f∈set(F). eval f L)"
proof -
{ fix f F
have h : "eval (foldr and F f) L = (eval f L ∧ (∀f ∈ set F. eval f L))"
apply(induct F)
apply simp
using eval_and by auto
} then show ?thesis
qed

lemma eval_list_disj : "eval (list_disj F) L = (∃f∈set(F). eval f L)"
proof -
{ fix f F
have h : "eval (foldr or F f) L = (eval f L ∨ (∃f ∈ set F. eval f L))"
apply(induct F)
apply simp
using eval_or by auto
} then show ?thesis
end