```subsection "Recursive QE"
imports EqualityVS GeneralVSProofs Reindex OptimizationProofs DNF
begin

lemma existN_eval : "∀xs. eval (ExN n φ) xs = (∃L. (length L = n ∧ eval φ (L@xs)))"
proof(induction n)
case 0
then show ?case  by simp
next
case (Suc n)
{fix xs
have "eval (ExN (Suc n) φ) xs = (∃l. length l = Suc n ∧ eval φ (l @ xs))"
by simp
also have "... = (∃x.∃L. (length L = n ∧ eval φ (L@(x#xs))))"
proof safe
fix l
assume h : "length l = Suc n" "eval φ (l @ xs)"
show "∃x L. length L = n ∧ eval φ (L @ x # xs)"
apply(rule exI[where x="l ! n"])
apply(rule exI[where x="take n l"])
using h apply auto
by (metis Cons_nth_drop_Suc append.assoc append_Cons append_take_drop_id lessI order_refl self_append_conv self_append_conv2 take_all)
next
fix x L
assume h : "eval φ (L @ x # xs)" "n = length L"
show "∃l. length l = Suc (length L) ∧ eval φ (l @ xs)"
apply(rule exI[where x="L@[x]"])
using h by auto
qed
also have "... = (∃x.∃L. (length L = n ∧ eval φ ((L@[x])@xs)))"
by simp
also have "... = (∃x.∃L. (length (L@[x]) = (Suc n) ∧ eval φ ((L@[x])@xs)))"
by simp
also have "... = (∃L. (length L = (Suc n) ∧ eval φ (L@xs)))"
by (metis append_butlast_last_id length_0_conv nat.simps(3))
finally have "eval (ExN (Suc n) φ) xs = (∃L. (length L = (Suc n) ∧ eval φ (L@xs)))"
by simp
}
then show ?case by simp
qed

lemma boundedFlipNegQuantifier : "(¬(∀x∈A. ¬ P x)) = (∃x∈A. P x)"
by blast

theorem QE_dnf'_eval:
assumes steph : "⋀amount F Γ.
(∃xs. (length xs = amount ∧ eval (list_disj (map(λ(L,F,n). ExN n (list_conj (map fm.Atom L @ F))) F))  (xs @ Γ))) = (eval (step amount F)  Γ)"
assumes opt : "⋀xs F . eval (opt F) xs = eval F xs"
shows "eval (QE_dnf' opt step φ) xs = eval φ xs"
proof(induction φ arbitrary : xs)
case (Atom x)
then show ?case by (simp add: simp_atom_eval)
next
case (And φ1 φ2)
then show ?case by (simp add: eval_and)
next
case (Or φ1 φ2)
then show ?case by (simp add: eval_or)
next
case (Neg φ)
then show ?case  apply simp
by (metis  eval_neg )
next
case (ExQ φ)
have h1 : "⋀F. (∃xs. length xs = Suc 0 ∧
F xs) = (∃x.
F [x])"
by (metis length_0_conv length_Suc_conv)
show ?case
apply simp
unfolding h1 apply(rule ex_cong1)
unfolding ExQ[symmetric]
unfolding opt[symmetric, of "(QE_dnf' opt step φ)"]
unfolding dnf_modified_eval[symmetric, of "(opt (QE_dnf' opt step φ))"]
apply(rule bex_cong) apply simp
subgoal for x f
apply(cases f)
by (metis Un_iff eval.simps(1) imageI)
done
next
case (AllQ φ)
have h1 : "⋀F. (∀xs::real list. (length xs = Suc 0 ⟶
F xs)) = (∀x.
F [x])"
by (metis length_0_conv length_Suc_conv)
show ?case
apply simp
unfolding h1 apply(rule all_cong1)
unfolding AllQ[symmetric]
unfolding eval_neg[symmetric, of "(QE_dnf' opt step φ)"]
unfolding opt[symmetric, of "neg(QE_dnf' opt step φ)"]
unfolding Set.bex_simps(8)[symmetric] HOL.Not_eq_iff
unfolding dnf_modified_eval[symmetric, of "(opt (neg(QE_dnf' opt step φ)))"]
apply(rule bex_cong) apply simp
subgoal for x f
apply(cases f)
by (metis Un_iff eval.simps(1) imageI)
done
next
case (ExN amount φ)
show ?case
apply(cases amount)
unfolding ExN[symmetric]
unfolding opt[of "(QE_dnf' opt step φ)",symmetric]
unfolding dnf_modified_eval[of "(opt (QE_dnf' opt step φ))",symmetric]
apply(rule ex_cong1)
subgoal for nat xs
apply(cases "length xs = Suc nat")
apply simp_all
apply(rule bex_cong)
apply simp_all
subgoal for f
apply(cases f)
apply simp
apply(rule ex_cong1)
unfolding eval_list_conj
apply auto
by (meson Un_iff eval.simps(1) imageI)
done
done
next
case (AllN amount φ)
show ?case
apply(cases amount)
unfolding AllN[symmetric]
unfolding eval_neg[symmetric, of "(QE_dnf' opt step φ)"]
unfolding opt[symmetric, of "neg(QE_dnf' opt step φ)"]
unfolding Set.bex_simps(8)[symmetric]
unfolding HOL.imp_conv_disj
unfolding HOL.de_Morgan_conj[symmetric]
unfolding HOL.not_ex[symmetric]
unfolding  HOL.Not_eq_iff
unfolding dnf_modified_eval[symmetric, of "(opt (neg(QE_dnf' opt step φ)))"]
apply(rule ex_cong1)
subgoal for nat xs
apply(cases "length xs = Suc nat")
apply simp_all
apply(rule bex_cong)
apply simp_all
subgoal for f
apply(cases f)
apply simp
apply(rule ex_cong1)
unfolding eval_list_conj
apply auto
by (meson Un_iff eval.simps(1) imageI)
done
done
qed auto

theorem QE_dnf_eval:
assumes steph : "⋀var amount new L F Γ.
amount≤var+1 ⟹
(∃xs. (length xs = var+1 ∧ eval (list_conj (map fm.Atom L @ F)) (xs @ Γ))) = (∃xs. (length xs = var+1 ∧eval (step amount var L F) (xs @ Γ)))"
assumes opt : "⋀xs F . eval (opt F) xs = eval F xs"
shows "eval (QE_dnf opt step φ) xs = eval φ xs"
proof(induction φ arbitrary:xs)
case (Atom x)
then show ?case by (simp add: simp_atom_eval)
next
case (And φ1 φ2)
then show ?case by (simp add: eval_and)
next
case (Or φ1 φ2)
then show ?case by (simp add: eval_or)
next
case (Neg φ)
then show ?case
by (metis eval.simps(6) eval_neg QE_dnf.simps(3))
next
case (ExQ φ)
have h : "(∃x. ∃(al, fl, n)∈set (dnf_modified (opt (QE_dnf opt step φ))).
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ x # xs)) ∧ (∀f∈set fl. eval f (L @ x # xs))) =
(∃(al, fl, n)∈set (dnf_modified (opt (QE_dnf opt step φ))). ∃x.
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ x # xs)) ∧ (∀f∈set fl. eval f (L @ x # xs)))"
apply safe
by blast+
have lessThan : "⋀c. Suc 0 ≤ c + 1"
by simp
unfolding ExQ[symmetric]
unfolding opt[symmetric, of "(QE_dnf opt step φ)"]
unfolding dnf_modified_eval[symmetric, of "opt(QE_dnf opt step φ)"]
unfolding h
apply(rule bex_cong)
apply simp
subgoal for f
apply(cases f)
apply simp
subgoal for a b c
using steph[of "Suc 0" c a b xs, symmetric, OF lessThan] apply (simp add:eval_list_conj)
apply safe
subgoal for xs' l' l''
apply(rule exI[where x="l'!c"])
apply(rule exI[where x="take c l'"])
apply auto
apply (metis Un_iff append.assoc append_Cons append_Nil eval.simps(1) image_eqI lessI order_refl take_Suc_conv_app_nth take_all)
by (metis Un_iff append.assoc append_Cons append_Nil lessI order_refl take_Suc_conv_app_nth take_all)
subgoal for A B C D
apply(rule exI[where x="D@[C]"]) by auto
subgoal for A B
apply(rule exI[where x="B@[A]"]) by auto
done
done
done
next
case (AllQ φ)
have h : "(∃x. ∃(al, fl, n)∈set (dnf_modified (opt (neg(QE_dnf opt step φ)))).
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ x # xs)) ∧ (∀f∈set fl. eval f (L @ x # xs))) =
(∃(al, fl, n)∈set (dnf_modified (opt (neg(QE_dnf opt step φ)))). ∃x.
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ x # xs)) ∧ (∀f∈set fl. eval f (L @ x # xs)))"
apply safe
by blast+
have lessThan : "⋀c. Suc 0 ≤ c + 1"
by simp
show ?case
unfolding AllQ[symmetric]
unfolding eval_neg[symmetric, of "(QE_dnf opt step φ)"]
unfolding opt[symmetric, of "neg(QE_dnf opt step φ)"]
unfolding HOL.Not_eq_iff[symmetric, of "(∀f∈set (dnf_modified (opt (neg (QE_dnf opt step φ)))). ¬ eval (case f of (al, fl, n) ⇒ ExN (Suc n) (step (Suc 0) n al fl)) xs)"]
unfolding SMT.verit_connective_def(3)[symmetric]
unfolding boundedFlipNegQuantifier
unfolding dnf_modified_eval[symmetric, of "opt(neg(QE_dnf opt step φ))"]
unfolding h
apply(rule bex_cong)
apply simp
subgoal for f
apply(cases f)
apply simp
subgoal for a b c
using steph[of "Suc 0" c a b xs, symmetric,OF lessThan] apply (simp add:eval_list_conj)
apply safe
subgoal for xs' l' l''
apply(rule exI[where x="l'!c"])
apply(rule exI[where x="take c l'"])
apply auto
apply (metis Un_iff append.assoc append_Cons append_Nil eval.simps(1) image_eqI lessI order_refl take_Suc_conv_app_nth take_all)
by (metis Un_iff append.assoc append_Cons append_Nil lessI order_refl take_Suc_conv_app_nth take_all)
subgoal for A B C D
apply(rule exI[where x="D@[C]"]) by auto
subgoal for A B
apply(rule exI[where x="B@[A]"]) by auto
done
done
done
next
case (ExN x1 φ)
show ?case
proof(cases x1)
case 0
then show ?thesis using ExN by simp
next
case (Suc nat)
have h : "(∃l. length l = Suc nat ∧
(∃(al, fl, n)∈set (dnf_modified (opt (QE_dnf opt step φ))).
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ l @ xs)) ∧ (∀f∈set fl. eval f (L @ l @ xs)))) =
(∃(al, fl, n)∈set (dnf_modified (opt (QE_dnf opt step φ))). (∃l. length l = Suc nat ∧
(∃L. length L = n ∧ (∀a∈set al. aEval a (L @ l @ xs)) ∧ (∀f∈set fl. eval f (L @ l @ xs)))))"
apply safe
by blast+
have lessThan : "⋀c. Suc nat ≤ c + nat + 1" by simp
show ?thesis
unfolding ExN[symmetric]
unfolding opt[symmetric, of "(QE_dnf opt step φ)"]
unfolding dnf_modified_eval[symmetric, of "(opt (QE_dnf opt step φ))"]
unfolding h
apply(rule bex_cong)
apply simp
subgoal for f
apply(cases f)
subgoal for a b c
apply simp
using steph[of "Suc nat" "c+nat",symmetric, OF lessThan]
subgoal for L
apply(rule exI[where x="drop c L"])
apply auto
apply(rule exI[where x="take c L"])
apply auto
apply (metis Un_iff append.assoc append_take_drop_id eval.simps(1) image_eqI)
by (metis Un_iff append.assoc append_take_drop_id)
subgoal for L l
apply(rule exI[where x="l@L"])
by auto
done
done
done
qed
next
case (AllN x1 φ)
then show ?case
proof(cases x1)
case 0
then show ?thesis using AllN by simp
next
case (Suc nat)
have h : "(∃l. length l = Suc nat ∧
(∃(al, fl, n)∈set (dnf_modified (opt (neg(QE_dnf opt step φ)))).
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ l @ xs)) ∧ (∀f∈set fl. eval f (L @ l @ xs)))) =
(∃(al, fl, n)∈set (dnf_modified (opt (neg(QE_dnf opt step φ)))). (∃l. length l = Suc nat ∧
(∃L. length L = n ∧ (∀a∈set al. aEval a (L @ l @ xs)) ∧ (∀f∈set fl. eval f (L @ l @ xs)))))"
apply safe
by blast+
have lessThan : "⋀c. Suc nat ≤ c + nat + 1" by simp
show ?thesis
unfolding AllN[symmetric]
unfolding eval_neg[symmetric, of "QE_dnf opt step φ"]
unfolding HOL.imp_conv_disj
unfolding HOL.de_Morgan_conj[symmetric]
unfolding opt[symmetric, of "neg(QE_dnf opt step φ)"]
unfolding dnf_modified_eval[symmetric, of "(opt (neg(QE_dnf opt step φ)))"]
unfolding HOL.Not_eq_iff[symmetric, of "(∀f∈set (dnf_modified (opt (neg (QE_dnf opt step φ)))).
¬ eval (case f of (al, fl, n) ⇒ ExN (Suc (n + nat)) (step (Suc nat) (n + nat) al fl)) xs)"]
unfolding SMT.verit_connective_def(3)[symmetric]
unfolding boundedFlipNegQuantifier
unfolding h
apply(rule bex_cong)
apply simp
subgoal for f
apply(cases f)
subgoal for a b c
apply simp
using steph[of "Suc nat" "c+nat",symmetric, OF lessThan]
subgoal for L
apply(rule exI[where x="drop c L"])
apply auto
apply(rule exI[where x="take c L"])
apply auto
apply (metis Un_iff append.assoc append_take_drop_id eval.simps(1) image_eqI)
by (metis Un_iff append.assoc append_take_drop_id)
subgoal for L l
apply(rule exI[where x="l@L"])
by auto
done
done
done
qed
qed auto

lemma opt: "eval ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers) F) L= eval F L"
using push_forall_eval eval_nnf unpower_eval groupQuantifiers_eval clearQuantifiers_eval by auto

lemma opt': "eval ((push_forall ( nnf ( unpower 0 ( groupQuantifiers (clearQuantifiers F)))))) L= eval F L"
using push_forall_eval eval_nnf unpower_eval groupQuantifiers_eval clearQuantifiers_eval by auto

lemma opt_no_group: "eval ((push_forall ∘ nnf ∘ unpower 0 o clearQuantifiers) F) L= eval F L"
using push_forall_eval eval_nnf unpower_eval clearQuantifiers_eval by auto

lemma  repeatAmountOfQuantifiers_helper_eval :
assumes  "⋀xs F. eval F xs = eval (step F) xs"
shows  "eval F xs = eval (repeatAmountOfQuantifiers_helper step n F) xs"
apply(induction n arbitrary : F)
apply simp_all
subgoal for n F
using assms[of F xs] by auto
done

lemma  repeatAmountOfQuantifiers_eval :
assumes  "⋀xs F. eval F xs = eval (step F) xs"
shows  "eval F xs = eval (repeatAmountOfQuantifiers step F) xs"
proof-
define F' where "F' = step F"
have h:  "eval F xs = eval F' xs"
using assms unfolding F'_def by auto
show ?thesis