# Theory UniAtoms

```section "General VS Proofs"
subsection "Univariate Atoms"
theory UniAtoms
imports Debruijn
begin

datatype atomUni = LessUni "real * real * real" | EqUni "real * real * real" | LeqUni "real * real * real" | NeqUni "real * real * real"
datatype (atoms: 'a) fmUni =
TrueFUni | FalseFUni | AtomUni 'a | AndUni "'a fmUni" "'a fmUni" | OrUni "'a fmUni" "'a fmUni"

fun aEvalUni :: "atomUni ⇒ real ⇒ bool" where
"aEvalUni (EqUni (a,b,c)) x = (a*x^2+b*x+c = 0)" |
"aEvalUni (LessUni (a,b,c)) x = (a*x^2+b*x+c < 0)" |
"aEvalUni (LeqUni (a,b,c)) x = (a*x^2+b*x+c ≤ 0)" |
"aEvalUni (NeqUni (a,b,c)) x = (a*x^2+b*x+c ≠ 0)"

fun aNegUni :: "atomUni ⇒ atomUni" where
"aNegUni (LessUni (a,b,c)) = LeqUni (-a,-b,-c)" |
"aNegUni (EqUni p) = NeqUni p" |
"aNegUni (LeqUni (a,b,c)) = LessUni (-a,-b,-c)" |
"aNegUni (NeqUni p) = EqUni p"

fun evalUni :: "atomUni fmUni ⇒ real ⇒ bool" where
"evalUni (AtomUni a) x = aEvalUni a x" |
"evalUni (TrueFUni) _ = True" |
"evalUni (FalseFUni) _ = False" |
"evalUni (AndUni φ ψ) x = ((evalUni φ x) ∧ (evalUni ψ x))" |
"evalUni (OrUni φ ψ) x = ((evalUni φ x) ∨ (evalUni ψ x))"

fun negUni :: "atomUni fmUni ⇒ atomUni fmUni" where
"negUni (AtomUni a) = AtomUni(aNegUni a)" |
"negUni (TrueFUni) = FalseFUni" |
"negUni (FalseFUni) = TrueFUni" |
"negUni (AndUni φ ψ) = (OrUni (negUni φ) (negUni ψ))" |
"negUni (OrUni φ ψ) = (AndUni (negUni φ) (negUni ψ))"

fun convert_poly :: "nat ⇒ real mpoly ⇒ real list ⇒ (real * real * real) option" where
"convert_poly var p xs = (
if MPoly_Type.degree p var < 3
then let (A,B,C) = get_coeffs var p in Some(insertion (nth_default 0 (xs)) A,insertion (nth_default 0 (xs)) B,insertion (nth_default 0 (xs)) C)
else None)"

fun convert_atom :: "nat ⇒ atom ⇒ real list ⇒ atomUni option" where
"convert_atom var (Less p) xs = map_option LessUni (convert_poly var p xs)"|
"convert_atom var (Eq p) xs = map_option EqUni (convert_poly var p xs)"|
"convert_atom var (Leq p) xs = map_option LeqUni (convert_poly var p xs)"|
"convert_atom var (Neq p) xs = map_option NeqUni (convert_poly var p xs)"

lemma convert_atom_change :
assumes "length xs' = var"
shows "convert_atom var At (xs' @ x # Γ) = convert_atom var At (xs' @ x' # Γ)"
apply(cases At)using assms apply simp_all
by (metis insertion_lowerPoly1 not_in_isovarspar)+

lemma degree_convert_eq :
assumes "convert_poly var p xs = Some(a)"
shows "MPoly_Type.degree p var < 3"
using assms apply(cases "MPoly_Type.degree p var < 3") by auto

lemma poly_to_univar :
assumes "MPoly_Type.degree p var < 3"
assumes "get_coeffs var p = (A,B,C)"
assumes "a = insertion (nth_default 0 (xs'@y#xs)) A"
assumes "b = insertion (nth_default 0 (xs'@y#xs)) B"
assumes "c = insertion (nth_default 0 (xs'@y#xs)) C"
assumes "length xs' = var"
shows "insertion (nth_default 0 (xs'@x#xs)) p = (a*x^2)+(b*x)+c"
proof-
have ha: "⋀x. a = insertion (nth_default 0 (xs'@x # xs)) A" using assms(2) apply auto
by (metis assms(3) assms(6) insertion_lowerPoly1 not_in_isovarspar)
have hb: "⋀x. b = insertion (nth_default 0 (xs'@x # xs)) B" using assms(2) apply auto
by (metis assms(4) assms(6) insertion_lowerPoly1 not_in_isovarspar)
have hc: "⋀x. c = insertion (nth_default 0 (xs'@x # xs)) C" using assms(2) apply auto
by (metis assms(5) assms(6) insertion_lowerPoly1 not_in_isovarspar)
show ?thesis
proof(cases "MPoly_Type.degree p var = 0")
case True
have h1 : "var < length (xs'@x#xs)" using assms by auto
show ?thesis using assms ha hb hc sum_over_degree_insertion[OF h1 True, of y] apply(simp add: isovar_greater_degree[of p ] True)
using True degree0isovarspar by force
next
case False
then have notzero : "MPoly_Type.degree p var ≠ 0" by auto
show ?thesis proof(cases "MPoly_Type.degree p var = 1" )
case True
have h1 : "var < length (xs'@x#xs)" using assms by auto
show ?thesis using  sum_over_degree_insertion[OF h1 True, of x,  symmetric] unfolding assms(6)[symmetric] list_update_length unfolding assms(6) apply simp using ha hb hc assms apply auto
by (smt (verit, ccfv_threshold) One_nat_def True express_poly h1 insertion_add insertion_mult insertion_pow insertion_var list_update_length)
next
case False
then have deg2 : "MPoly_Type.degree p var = 2" using notzero assms by auto
have h1 : "var < length (xs'@x#xs)" using assms by auto
have two : "2 = Suc(Suc 0)" by auto
show ?thesis
using  sum_over_degree_insertion[OF h1 deg2, of x,  symmetric] unfolding assms(6)[symmetric] list_update_length unfolding assms(6) two apply simp using ha hb hc assms apply auto
using deg2 express_poly h1 insertion_add insertion_mult insertion_pow insertion_var list_update_length
by (smt (verit, best) numeral_2_eq_2)
qed
qed
qed

lemma "aEval_aEvalUni":
assumes "convert_atom var a (xs'@x#xs) = Some a'"
assumes "length xs' = var"
shows "aEval a (xs'@x#xs) = aEvalUni a' x"
proof(cases a)
case (Less x)
then show ?thesis
proof(cases "MPoly_Type.degree x var < 3")
case True
then show ?thesis
using poly_to_univar[OF True]
by (metis One_nat_def aEvalUni.simps(2) get_coeffs.elims)
next
case False
then show ?thesis using assms Less by auto
qed
next
case (Eq x)
then show ?thesis
proof(cases "MPoly_Type.degree x var < 3")
case True
then show ?thesis
using poly_to_univar[OF True]
by (metis One_nat_def aEvalUni.simps(1) get_coeffs.elims)
next
case False
then show ?thesis using assms Eq by auto
qed
next
case (Leq x)
then show ?thesis
proof(cases "MPoly_Type.degree x var < 3")
case True
then show ?thesis
using poly_to_univar[OF True]
by (metis One_nat_def aEvalUni.simps(3) get_coeffs.elims)
next
case False
then show ?thesis using assms Leq by auto
qed
next
case (Neq x)
then show ?thesis
proof(cases "MPoly_Type.degree x var < 3")
case True
then show ?thesis
using poly_to_univar[OF True]
by (metis One_nat_def aEvalUni.simps(4) get_coeffs.elims)
next
case False
then show ?thesis using assms Neq by auto
qed
qed

fun convert_fm :: "nat ⇒ atom fm ⇒ real list ⇒ (atomUni fmUni) option" where
"convert_fm var (Atom a) Γ = map_option (AtomUni) (convert_atom var a Γ)" |
"convert_fm var (TrueF) _ = Some TrueFUni" |
"convert_fm var (FalseF) _ = Some FalseFUni" |
"convert_fm var (And φ ψ) Γ = (case ((convert_fm var φ Γ),(convert_fm var ψ Γ)) of (Some a, Some b) ⇒ Some (AndUni a b) | _ ⇒ None)" |
"convert_fm var (Or φ ψ) Γ = (case ((convert_fm var φ Γ),(convert_fm var ψ Γ)) of (Some a, Some b) ⇒ Some (OrUni a b) | _ ⇒ None)" |
"convert_fm var (Neg φ) Γ = None " |
"convert_fm var (ExQ φ) Γ = None" |
"convert_fm var (AllQ φ) Γ = None"|
"convert_fm var (AllN i φ) Γ = None"|
"convert_fm var (ExN i φ) Γ = None"

lemma "eval_evalUni":
assumes "convert_fm var F (xs'@x#xs) = Some F'"
assumes "length xs' = var"
shows "eval F (xs'@x#xs) = evalUni F' x"
using assms
proof(induction F arbitrary: F')
case TrueF
then show ?case by auto
next
case FalseF
then show ?case by auto
next
case (Atom x)
then show ?case using aEval_aEvalUni by auto
next
case (And F1 F2)
then show ?case apply(cases "convert_fm var F1 (xs'@x#xs)") apply simp apply(cases "convert_fm var F2 (xs'@x#xs)") by auto
next
case (Or F1 F2)
then show ?case apply(cases "convert_fm var F1 (xs'@x#xs)") apply simp apply(cases "convert_fm var F2 (xs'@x#xs)") by auto
next
case (Neg F)
then show ?case by auto
next
case (ExQ F)
then show ?case by auto
next
case (AllQ F)
then show ?case by auto
next
case (ExN x1 φ)
then show ?case by auto
next
case (AllN x1 φ)
then show ?case by auto
qed

fun grab_atoms :: "nat ⇒ atom fm ⇒ atom list option" where
"grab_atoms var TrueF = Some([])" |
"grab_atoms var FalseF = Some([])" |
"grab_atoms var (Atom(Eq p)) = (if MPoly_Type.degree p var < 3 then (if MPoly_Type.degree p var > 0 then Some([Eq p]) else Some([])) else None)"|
"grab_atoms var (Atom(Less p)) = (if MPoly_Type.degree p var < 3 then (if MPoly_Type.degree p var > 0 then Some([Less p]) else Some([])) else None)"|
"grab_atoms var (Atom(Leq p)) = (if MPoly_Type.degree p var < 3 then (if MPoly_Type.degree p var > 0 then Some([Leq p]) else Some([])) else None)"|
"grab_atoms var (Atom(Neq p)) = (if MPoly_Type.degree p var < 3 then (if MPoly_Type.degree p var > 0 then Some([Neq p]) else Some([])) else None)"|
"grab_atoms var (And a b) = (
case grab_atoms var a of
Some(al) ⇒ (
case grab_atoms var b of
Some(bl) ⇒ Some(al@bl)
| None ⇒ None
)
| None ⇒ None
)"|
"grab_atoms var (Or a b) = (
case grab_atoms var a of
Some(al) ⇒ (
case grab_atoms var b of
Some(bl) ⇒ Some(al@bl)
| None ⇒ None
)
| None ⇒ None
)"|

"grab_atoms var (Neg _) = None"|
"grab_atoms var (ExQ _) = None"|
"grab_atoms var (AllQ _) = None"|
"grab_atoms var (AllN i _) = None"|
"grab_atoms var (ExN i _) = None"

lemma nil_grab : "(grab_atoms var F = Some []) ⟹ (freeIn var F)"
proof(induction F)
case TrueF
then show ?case by auto
next
case FalseF
then show ?case by auto
next
case (Atom x)
then show ?case proof(cases x)
case (Less p)
then show ?thesis using Atom apply(cases "MPoly_Type.degree p var < 3") apply auto apply(cases "MPoly_Type.degree p var > 0") apply auto
using degree0isovarspar not_in_isovarspar by blast
next
case (Eq p)
then show ?thesis using Atom apply(cases "MPoly_Type.degree p var < 3") apply auto apply(cases "MPoly_Type.degree p var > 0") apply auto
using degree0isovarspar not_in_isovarspar by blast
next
case (Leq p)
then show ?thesis using Atom apply(cases "MPoly_Type.degree p var < 3") apply auto apply(cases "MPoly_Type.degree p var > 0") apply auto
using degree0isovarspar not_in_isovarspar by blast
next
case (Neq p)
then show ?thesis using Atom apply(cases "MPoly_Type.degree p var < 3") apply auto apply(cases "MPoly_Type.degree p var > 0") apply auto
using degree0isovarspar not_in_isovarspar by blast
qed
next
case (And F1 F2)
then show ?case apply(cases "grab_atoms var F1")
apply(cases "grab_atoms var F2") apply(auto)
apply(cases "grab_atoms var F2") apply(auto)
apply(cases "grab_atoms var F2") by(auto)
next
case (Or F1 F2)
then show ?case apply(cases "grab_atoms var F1")
apply(cases "grab_atoms var F2") apply(auto)
apply(cases "grab_atoms var F2") apply(auto)
apply(cases "grab_atoms var F2") by(auto)
next
case (Neg F)
then show ?case by auto
next
case (ExQ F)
then show ?case by auto
next
case (AllQ F)
then show ?case by auto
next
case (ExN x1 F)
then show ?case by auto
next
case (AllN x1 F)
then show ?case by auto
qed

fun isSome :: "'a option ⇒ bool" where
"isSome (Some _) = True" |
"isSome None = False"

lemma "grab_atoms_convert" : "(isSome (grab_atoms var F)) = (isSome (convert_fm var F xs))"
proof(induction F)
case TrueF
then show ?case by auto
next
case FalseF
then show ?case by auto
next
case (Atom a)
then show ?case apply(cases a) by auto
next
case (And F1 F2)
then show ?case
by (smt convert_fm.simps(4) grab_atoms.simps(7) isSome.elims(2) isSome.elims(3) option.distinct(1) option.simps(5) option.split_sel_asm prod.simps(2))
next
case (Or F1 F2)
then show ?case
by (smt convert_fm.simps(5) grab_atoms.simps(8) isSome.elims(2) isSome.elims(3) option.distinct(1) option.simps(5) option.split_sel_asm prod.simps(2))
next
case (Neg F)
then show ?case by auto
next
case (ExQ F)
then show ?case by auto
next
case (AllQ F)
then show ?case by auto
next
case (ExN x1 F)
then show ?case by auto
next
case (AllN x1 F)
then show ?case by auto
qed

lemma convert_aNeg :
assumes "convert_atom var A (xs'@x#xs) = Some(A')"
assumes "length xs' = var"
shows "aEval (aNeg A) (xs'@x#xs) = aEvalUni (aNegUni A') x"
proof-
have "aEval (aNeg A) (xs'@x#xs) = (¬ aEval A (xs'@x#xs))"
using aNeg_aEval[of A "(xs'@x#xs)"] by auto
also have "... = (¬ aEvalUni A' x)"
using assms aEval_aEvalUni by auto
also have "... = aEvalUni (aNegUni A') x"
by(cases A')(auto)
finally show ?thesis .
qed

lemma convert_neg :
assumes "convert_fm var F (xs'@x#xs) = Some(F')"
assumes "length xs' = var"
shows "eval (Neg F) (xs'@x#xs) = evalUni (negUni F') x"
using assms
proof(induction F arbitrary:F')
case TrueF
then show ?case by auto
next
case FalseF
then show ?case by auto
next
case (Atom p)
then show ?case
using convert_aNeg[of _ p]
by (smt aNeg_aEval convert_fm.simps(1) evalUni.simps(1) eval.simps(1) eval.simps(6) map_option_eq_Some negUni.simps(1))
next
case (And F1 F2)
then show ?case apply auto
apply (metis (no_types, lifting) evalUni.simps(5) negUni.simps(4) option.case_eq_if option.collapse option.distinct(1) option.sel)
apply (smt (verit, del_insts) evalUni.simps(5) isSome.elims(1) negUni.simps(4) option.inject option.simps(4) option.simps(5))
by (smt (verit, del_insts) evalUni.simps(5) isSome.elims(1) negUni.simps(4) option.inject option.simps(4) option.simps(5))
next
case (Or F1 F2)
then show ?case apply auto
apply (smt (verit, del_insts) evalUni.simps(4) isSome.elims(1) negUni.simps(5) option.inject option.simps(4) option.simps(5))
apply (smt (verit, del_insts) evalUni.simps(4) isSome.elims(1) negUni.simps(5) option.inject option.simps(4) option.simps(5))
by (smt (verit, del_insts) evalUni.simps(4) isSome.elims(1) negUni.simps(5) option.inject option.simps(4) option.simps(5))
next
case (Neg F)
then show ?case by auto
next
case (ExQ F)
then show ?case by auto
next
case (AllQ F)
then show ?case by auto
next
case (ExN x1 F)
then show ?case by auto
next
case (AllN x1 F)
then show ?case by auto
qed

fun list_disj_Uni :: "'a fmUni list ⇒ 'a fmUni" where
"list_disj_Uni [] = FalseFUni"|
"list_disj_Uni (x#xs) = OrUni x (list_disj_Uni xs)"

fun list_conj_Uni :: "'a fmUni list ⇒ 'a fmUni" where
"list_conj_Uni [] = TrueFUni"|
"list_conj_Uni (x#xs) = AndUni x (list_conj_Uni xs)"

lemma eval_list_disj_Uni : "evalUni (list_disj_Uni L) x = (∃l∈set(L). evalUni l x)"
by(induction L)(auto)

lemma eval_list_conj_Uni : "evalUni (list_conj_Uni A) x = (∀l∈set A. evalUni l x)"
apply(induction A)by auto

lemma eval_list_conj_Uni_append : "evalUni (list_conj_Uni (A @ B)) x = (evalUni (list_conj_Uni (A)) x ∧ evalUni (list_conj_Uni (B)) x)"
apply(induction A)by auto

fun map_atomUni :: "('a ⇒ 'a fmUni) ⇒ 'a fmUni ⇒ 'a fmUni" where
"map_atomUni f (AtomUni a) = f a" |
"map_atomUni f (TrueFUni) = TrueFUni" |
"map_atomUni f (FalseFUni) = FalseFUni" |
"map_atomUni f (AndUni φ ψ) = (AndUni (map_atomUni f φ) (map_atomUni f ψ))" |
"map_atomUni f (OrUni φ ψ) = (OrUni (map_atomUni f φ) (map_atomUni f ψ))"

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

fun getPoly :: "atomUni => real * real * real" where
"getPoly (EqUni p) = p"|
"getPoly (LeqUni p) = p"|
"getPoly (NeqUni p) = p"|
"getPoly (LessUni p) = p"

lemma liftatom_map_atom :
assumes "∃F'. convert_fm var F xs = Some F'"
shows "liftmap f F 0 = map_atom (f 0) F"
using assms
apply(induction F)
apply(auto)
apply fastforce
apply (metis (no_types, lifting) isSome.elims(2) isSome.elims(3) option.case_eq_if)
apply fastforce
by (metis (no_types, lifting) isSome.elims(2) isSome.elims(3) option.case_eq_if)

lemma eval_map : "(∃l∈set(map f L). evalUni l x) = (∃l∈set(L). evalUni (f l) x)"
by auto

lemma eval_map_all : "(∀l∈set(map f L). evalUni l x) = (∀l∈set(L). evalUni (f l) x)"
by auto

lemma eval_append : "(∃l∈set (A#B).evalUni l x) = (evalUni A x ∨ (∃l∈set (B).evalUni l x))"
by auto

lemma eval_conj_atom : "evalUni (list_conj_Uni (map AtomUni L)) x = (∀l∈set(L). aEvalUni l x)"
unfolding eval_list_conj_Uni
by auto
end```