# Theory DNF

```section "QE Algorithm Proofs"
subsection "DNF"
theory DNF
imports VSAlgos
begin

theorem dnf_eval :
"(∃(al,fl)∈set (dnf φ).
(∀a∈set al. aEval a xs)
∧ (∀f∈set fl. eval f xs))
= eval φ xs"
proof(induction φ)
case (And φ1 φ2)
define f where "f = (λa. case a of
(al, fl) ⇒ (∀a∈set al. aEval a xs) ∧ (∀f∈set fl. eval f xs))"
have h1:"(∃a∈set (dnf (And φ1 φ2)). f a) = (∃a∈set (dnf φ1). ∃a'∈set(dnf φ2). f a ∧ f a')"
apply simp unfolding f_def apply auto
apply blast
apply blast
subgoal for a b c d
apply(rule bexI[where x="(a,b)"])
apply(rule exI[where x="a@c"])
apply(rule exI[where x="b@d"])
by auto
done
also have h2 : "... = ((∃a∈set (dnf φ1). f a)∧(∃a∈set(dnf φ2). f a))"
by auto
show ?case unfolding f_def[symmetric] unfolding h1 h2 unfolding f_def using And by auto
qed auto

theorem dnf_modified_eval :
"(∃(al,fl,n)∈set (dnf_modified φ).
(∃L. (length L = n
∧ (∀a∈set al. aEval a (L@xs))
∧ (∀f∈set fl. eval f (L@xs))))) = eval φ xs"
proof(induction φ arbitrary:xs)
case (Atom x)
then show ?case
by (cases x, auto)
next
case (And φ1 φ2)
{fix d1 d2 A A' B B' L1 L2
assume A : "(A,A',length (L1::real list))∈set (dnf_modified φ1)" and "(B,B',length (L2::real list))∈set (dnf_modified φ2)"
have "(
(∀a∈set ((map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B)). aEval a ((L1@L2) @ xs))
∧ (∀f∈set ( map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B'). eval f ((L1@L2) @ xs))) =
(
(∀a∈set(map (liftAtom (length L1) (length L2)) A) ∪ set( map (liftAtom 0 (length L1)) B). aEval a ((L1@L2) @ xs))
∧ (∀f∈set( map (liftFm (length L1) (length L2)) A') ∪ set(map (liftFm 0 (length L1)) B'). eval f ((L1@L2) @ xs)))"
by auto
also have "... = (
(∀a∈set(map (liftAtom (length L1) (length L2)) A).aEval a ((L1@L2) @ xs))
∧ (∀a∈set(map (liftAtom 0 (length L1)) B). aEval a ((L1@L2) @ xs))
∧ (∀f∈set(map (liftFm (length L1) (length L2)) A').eval f ((L1@L2) @ xs))
∧ (∀f∈set(map (liftFm 0 (length L1)) B'). eval f ((L1@L2) @ xs)))"
by blast
also have "... =  (
(∀a∈set A. aEval (liftAtom (length L1) (length L2) a) ((L1@L2) @ xs))
∧ (∀a∈set B. aEval (liftAtom 0 (length L1) a) ((L1@L2) @ xs))
∧ (∀f∈set A'. eval (liftFm (length L1) (length L2) f) ((L1@L2) @ xs))
∧ (∀f∈set B'. eval (liftFm 0 (length L1) f) ((L1@L2) @ xs)))"
by simp
also have "... =  (
(∀a∈set A. aEval (liftAtom (length L1) (length L2) a) (insert_into (L1 @ xs) (length L1) L2))
∧ (∀a∈set B. aEval (liftAtom 0 (length L1) a) (insert_into (L2 @ xs) 0 L1))
∧ (∀f∈set A'. eval (liftFm (length L1) (length L2) f) (insert_into (L1 @ xs) (length L1) L2))
∧ (∀f∈set B'. eval (liftFm 0 (length L1) f) (insert_into (L2 @ xs) 0 L1)))"
by auto
also have "... = (
((∀a∈set A. aEval a (L1 @ xs)) ∧ (∀f∈set A'. eval f (L1 @ xs))) ∧
((∀a∈set B. aEval a (L2 @ xs)) ∧ (∀f∈set B'. eval f (L2 @ xs))) )"
proof safe
fix a
show "∀a∈set A. aEval (liftAtom (length L1) (length L2) a) (insert_into (L1 @ xs) (length L1) L2) ⟹
a ∈ set A ⟹ aEval a (L1 @ xs)"
using eval_liftFm[of L2 "length L2" "length L1" "L1 @ xs" "Atom a", OF refl]
by auto
next
fix f
show "∀f∈set A'. eval (liftFm (length L1) (length L2) f) (insert_into (L1 @ xs) (length L1) L2) ⟹
f ∈ set A' ⟹ eval f (L1 @ xs)"
using eval_liftFm[of L2 "length L2" "length L1" "L1 @ xs" f, OF refl] by auto
next
fix a
show " ∀a∈set B. aEval (liftAtom 0 (length L1) a) (insert_into (L2 @ xs) 0 L1) ⟹
a ∈ set B ⟹ aEval a (L2 @ xs)"
using eval_liftFm[of L1 "length L1" "0" "L2@xs" "Atom a", OF refl] by auto
next
fix f
show " ∀f∈set B'. eval (liftFm 0 (length L1) f) (insert_into (L2 @ xs) 0 L1) ⟹ f ∈ set B' ⟹ eval f (L2 @ xs)"
using eval_liftFm[of L1 "length L1" "0" "L2 @ xs" f, OF refl] by auto
next
fix a
show " ∀a∈set A. aEval a (L1 @ xs) ⟹
a ∈ set A ⟹ aEval (liftAtom (length L1) (length L2) a) (insert_into (L1 @ xs) (length L1) L2)"
using eval_liftFm[of L2 "length L2" "length L1" "L1 @ xs" "Atom a", OF refl] by auto
next
fix a
show "∀a∈set B. aEval a (L2 @ xs) ⟹ a ∈ set B ⟹ aEval (liftAtom 0 (length L1) a) (insert_into (L2 @ xs) 0 L1)"
using eval_liftFm[of L1 "length L1" "0" "L2@xs" "Atom a", OF refl] by auto
next
fix f
show "∀f∈set A'. eval f (L1 @ xs) ⟹
f ∈ set A' ⟹ eval (liftFm (length L1) (length L2) f) (insert_into (L1 @ xs) (length L1) L2)"
using eval_liftFm[of L2 "length L2" "length L1" "L1 @ xs" f, OF refl] by auto
next
fix f
show "∀f∈set B'. eval f (L2 @ xs) ⟹ f ∈ set B' ⟹ eval (liftFm 0 (length L1) f) (insert_into (L2 @ xs) 0 L1)"
using eval_liftFm[of L1 "length L1" "0" "L2 @ xs" f, OF refl] by auto
qed
finally have "(
(∀a∈set ((map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B)). aEval a ((L1@L2) @ xs))
∧ (∀f∈set ( map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B'). eval f ((L1@L2) @ xs))) = (
((∀a∈set A. aEval a (L1 @ xs)) ∧ (∀f∈set A'. eval f (L1 @ xs))) ∧
((∀a∈set B. aEval a (L2 @ xs)) ∧ (∀f∈set B'. eval f (L2 @ xs))) )"
by simp
}
then have h : "(∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set (dnf_modified φ2).
(∃L1.∃L2. length L1 = d1 ∧ length L2 = d2 ∧
(∀a∈set ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B)). aEval a ((L1@L2) @ xs))
∧ (∀f∈set ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f ((L1@L2) @ xs)))) = ((∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set(dnf_modified φ2).
(∃L1. length L1 = d1 ∧ (∀a∈set A. aEval a (L1 @ xs)) ∧ (∀f∈set A'. eval f (L1 @ xs))) ∧
(∃L2. length L2 = d2 ∧ (∀a∈set B. aEval a (L2 @ xs)) ∧ (∀f∈set B'. eval f (L2 @ xs))) ))"
proof safe
fix A A' B B'  L1 L2
assume prev : "(⋀A A' L1 B B' L2.
(A, A', length L1) ∈ set (dnf_modified φ1) ⟹
(B, B', length L2) ∈ set (dnf_modified φ2) ⟹
((∀a∈set (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
aEval a ((L1 @ L2) @ xs)) ∧
(∀f∈set (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
eval f ((L1 @ L2) @ xs))) =
(((∀a∈set A. aEval a (L1 @ xs)) ∧ (∀f∈set A'. eval f (L1 @ xs))) ∧
(∀a∈set B. aEval a (L2 @ xs)) ∧ (∀f∈set B'. eval f (L2 @ xs))))"
and A: "(A,A',length L1)∈set (dnf_modified φ1)" and B: "(B,B',length L2)∈set (dnf_modified φ2)"
and h1 : "∀a∈set (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
aEval a ((L1 @ L2) @ xs)"
and h2 : "∀f∈set (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
eval f ((L1 @ L2) @ xs)"
have h : "((∀a∈set (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
aEval a ((L1 @ L2) @ xs)) ∧
(∀f∈set (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
eval f ((L1 @ L2) @ xs))) =
(((∀a∈set A. aEval a (L1 @ xs)) ∧ (∀f∈set A'. eval f (L1 @ xs))) ∧
(∀a∈set B. aEval a (L2 @ xs)) ∧ (∀f∈set B'. eval f (L2 @ xs)))"
using prev[where A="A", where A'="A'", where B="B", where B'="B'"] A B by simp
show "∃(A, A', d1)∈set (dnf_modified φ1).
∃(B, B', d2)∈set (dnf_modified φ2).
(∃L1. length L1 = d1 ∧ (∀a∈set A. aEval a (L1 @ xs)) ∧ (∀f∈set A'. eval f (L1 @ xs))) ∧
(∃L2. length L2 = d2 ∧ (∀a∈set B. aEval a (L2 @ xs)) ∧ (∀f∈set B'. eval f (L2 @ xs)))"
apply (rule bexI[where x="(A, A', length L1)", OF _ A])
apply auto defer
apply (rule bexI[where x="(B, B', length L2)", OF _ B])
apply auto
using h h1 h2
by auto
next
fix A A' d1 B B' d2 L1 L2
assume prev : "(⋀A A' L1 B B' L2.
(A, A', length L1) ∈ set (dnf_modified φ1) ⟹
(B, B', length L2) ∈ set (dnf_modified φ2) ⟹
((∀a∈set (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
aEval a ((L1 @ L2) @ xs)) ∧
(∀f∈set (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
eval f ((L1 @ L2) @ xs))) =
(((∀a∈set A. aEval a (L1 @ xs)) ∧ (∀f∈set A'. eval f (L1 @ xs))) ∧
(∀a∈set B. aEval a (L2 @ xs)) ∧ (∀f∈set B'. eval f (L2 @ xs))))"
and A: "(A,A',length L1)∈set (dnf_modified φ1)" and B: "(B,B',length L2)∈set (dnf_modified φ2)"
and h1 : "∀a∈set A. aEval a (L1 @ xs)" "∀f∈set A'. eval f (L1 @ xs)"
"∀a∈set B. aEval a (L2 @ xs)" "∀f∈set B'. eval f (L2 @ xs)"
have h : "((∀a∈set (map (liftAtom (length L1) (length L2)) A @ map (liftAtom 0 (length L1)) B).
aEval a ((L1 @ L2) @ xs)) ∧
(∀f∈set (map (liftFm (length L1) (length L2)) A' @ map (liftFm 0 (length L1)) B').
eval f ((L1 @ L2) @ xs))) =
(((∀a∈set A. aEval a (L1 @ xs)) ∧ (∀f∈set A'. eval f (L1 @ xs))) ∧
(∀a∈set B. aEval a (L2 @ xs)) ∧ (∀f∈set B'. eval f (L2 @ xs)))"
using prev[where A="A", where A'="A'", where B="B", where B'="B'"] h1 A B by simp
show "∃(A, A', d1)∈set (dnf_modified φ1).
∃(B, B', d2)∈set (dnf_modified φ2).
∃L1 L2.
length L1 = d1 ∧
length L2 = d2 ∧
(∀a∈set (map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B). aEval a ((L1 @ L2) @ xs)) ∧
(∀f∈set (map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f ((L1 @ L2) @ xs))"
apply (rule bexI[where x="(A, A', length L1)", OF _ A])
apply auto defer
apply (rule bexI[where x="(B, B', length L2)", OF _ B])
apply auto
apply (rule exI[where x="L1"])
apply auto
apply (rule exI[where x="L2"])
apply auto
using h h1 by auto
qed

define f where "f (x:: (atom list * atom fm list * nat)) = (case x of (al,fl,n) ⇒ (∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs))))" for x
define g where "((g (uuaa::atom list) (uua::atom fm list) (uu::nat) x):: (atom list * atom fm list * nat)) = (
case x of
(B, B', d2) ⇒
(map (liftAtom uu d2) uuaa @ map (liftAtom 0 uu) B,
map (λx. map_fm_binders (λa x. liftAtom (uu + x) d2 a) x 0) uua @
map (λx. map_fm_binders (λa x. liftAtom (0 + x) uu a) x 0) B',
uu + d2))" for uuaa uua uu x

define f' where "f' L A A' d1 B B' d2 = ((∀a∈set ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B)). aEval a (L @ xs))
∧ (∀f∈set ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f (L @ xs)))" for L A A' d1 B B' d2
have "(∃(al, fl, n)∈set (dnf_modified (And φ1 φ2)).
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs)))
= (∃y∈set (dnf_modified (And φ1 φ2)). f y)"
unfolding f_def by simp
also have "... = (∃y∈set (dnf_modified φ1).
∃a aa b.
(∃uu uua uuaa.
(uuaa, uua, uu) = y ∧
(a, aa, b)
∈ (g uuaa uua uu) `
set (dnf_modified φ2)) ∧
f (a, aa, b))"
using g_def by simp
also have "... = (∃(A,A',d1)∈set (dnf_modified φ1).
∃x∈set (dnf_modified φ2).
f (g A A' d1 x))"
by (smt case_prodE f_def imageE image_eqI prod.simps(2))
also have "... = (∃(A,A',d1)∈set (dnf_modified φ1).
∃x∈set (dnf_modified φ2).
f (case x of (B,B',d2) ⇒ (map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B,
map (λx. liftFm d1 d2 x) A' @
map (λx. liftFm 0 d1 x) B',
d1 + d2)))"
using g_def by simp
also have "... = (∃(A,A',d1)∈set (dnf_modified φ1). ∃x∈set (dnf_modified φ2).
(case (case x of (B,B',d2) ⇒ (map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B,
map (λx. liftFm d1 d2 x) A' @ map (λx. liftFm 0 d1 x) B',
d1 + d2)) of (al,fl,n) ⇒ (∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs))))
)"
using f_def by simp
also have "... = (∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set (dnf_modified φ2).
(case ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B,
map (λx. liftFm d1 d2 x) A' @ map (λx. liftFm 0 d1 x) B',
d1 + d2)) of (al,fl,n) ⇒ (∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs))))
)"
by(smt case_prodE case_prodE2 old.prod.case)
also have "... = (∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set (dnf_modified φ2).
(∃L. length L = d1 + d2 ∧
(∀a∈set ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B)). aEval a (L @ xs))
∧ (∀f∈set ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f (L @ xs))))"
by(smt case_prodE case_prodE2 old.prod.case)
also have "... = (∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set (dnf_modified φ2).
(∃L. length L = d1 + d2 ∧ (f' L A A' d1 B B' d2)))"
using f'_def by simp
also have "... = (∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set (dnf_modified φ2).
(∃L1.∃L2. length L1 = d1 ∧ length L2 = d2 ∧ (f' (L1@L2) A A' d1 B B' d2)))"
proof safe
fix A A' d1 B B' d2 L
assume A: "(A,A',d1)∈set (dnf_modified φ1)" and B: "(B,B',d2)∈set (dnf_modified φ2)"
and L: "length L = d1 + d2" "(f' L A A' d1 B B' d2)"
show "∃(A, A', d1)∈set (dnf_modified φ1).
∃(B, B', d2)∈set (dnf_modified φ2). ∃L1 L2. length L1 = d1 ∧ length L2 = d2 ∧ f' (L1 @ L2) A A' d1 B B' d2"
apply (rule bexI[where x="(A, A', d1)", OF _ A])
apply auto
apply (rule bexI[where x="(B, B', d2)", OF _ B])
apply auto
apply (rule exI[where x="take d1 L"])
apply auto   defer
apply (rule exI[where x="drop d1 L"])
using L
by auto
next
fix A A' d1 B B' d2 L1 L2
assume A: "(A,A', length L1)∈set (dnf_modified φ1)" and B: "(B,B',length L2)∈set (dnf_modified φ2)"
and L: "(f' (L1 @ L2) A A' (length L1) B B' (length L2))"
thm exI
thm bexI
show "∃(A, A', d1)∈set (dnf_modified φ1). ∃(B, B', d2)∈set (dnf_modified φ2). ∃L. length L = d1 + d2 ∧ f' L A A' d1 B B' d2 "
apply (rule bexI[where x="(A, A', length L1)", OF _ A])
apply auto
apply (rule bexI[where x="(B, B', length L2)", OF _ B])
apply auto
apply (rule exI[where x="L1 @ L2"])
using L
by auto
qed

also have "... = (∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set (dnf_modified φ2).
(∃L1.∃L2. length L1 = d1 ∧ length L2 = d2 ∧
(∀a∈set ((map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B)). aEval a ((L1@L2) @ xs))
∧ (∀f∈set ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f ((L1@L2) @ xs))))"
unfolding f'_def by simp
(*also have "... = (∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set (dnf_modified φ2).
(∃L1.∃L2. length L1 = d1 ∧ length L2 = d2 ∧
(∀a∈set (map (liftAtom d1 d2) A) ∪ set ( map (liftAtom 0 d1) B). aEval a ((L1@L2) @ xs))
∧ (∀f∈set ( map (liftFm d1 d2) A' @ map (liftFm 0 d1) B'). eval f ((L1@L2) @ xs))))"
proof -
have *: "(∀a∈set (map (liftAtom d1 d2) A @ map (liftAtom 0 d1) B). aEval a ((L1 @ L2) @ xs))
= (∀a∈set (map (liftAtom d1 d2) A) ∪ set ( map (liftAtom 0 d1) B). aEval a ((L1@L2) @ xs))"
for d1 d2 A B L1 L2 by auto
then show ?thesis apply (subst * ) ..
qed (*
apply (rule bex_cong[OF refl])
unfolding split_beta
apply (rule bex_cong[OF refl])
apply (rule ex_cong1)+
apply (rule conj_cong refl)+
by auto *)
*)
also have "... = ((∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set(dnf_modified φ2).
(∃L. length L = d1 ∧ (∀a∈set A. aEval a (L @ xs)) ∧ (∀f∈set A'. eval f (L @ xs))) ∧
(∃L. length L = d2 ∧ (∀a∈set B. aEval a (L @ xs)) ∧ (∀f∈set B'. eval f (L @ xs))) ))"
using h by simp
also have "... = ((∃(A,A',d1)∈set (dnf_modified φ1). ∃(B,B',d2)∈set(dnf_modified φ2).
f (A,A',d1) ∧
f (B,B',d2)))"
using f_def by simp
also have "... = ((∃a∈set (dnf_modified φ1). ∃a1∈set(dnf_modified φ2). f a ∧ f a1))"
also have "... = ((∃a∈set (dnf_modified φ1). f a) ∧ (∃a∈set (dnf_modified φ2). f a))"
by blast
also have "... = eval (And φ1 φ2) xs"
using And f_def by simp
finally have "(∃(al, fl, n)∈set (dnf_modified (And φ1 φ2)).
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs))) =
eval (And φ1 φ2) xs"
by simp
then show ?case by simp
next
case (Or φ1 φ2)
have h1 : "eval (Or φ1 φ2) xs = eval φ1 xs ∨ eval φ2 xs"
using eval.simps(5) by blast
have h2 : "set (dnf_modified (Or φ1 φ2)) = set(dnf_modified φ1) ∪ set(dnf_modified φ2)"
by simp
show ?case using Or h1 h2
by (metis (no_types, lifting) Un_iff eval.simps(5))
next
case (ExQ φ)
have h1 : "((∃x. (∃(al, fl, n)∈set (dnf_modified φ).
∃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 φ).
(∃x.∃L. length L = n ∧ (∀a∈set al. aEval a ((L@[x]) @ xs)) ∧ (∀f∈set fl. eval f ((L@[x]) @ xs)))))"
apply simp by blast
{ fix n al fl
define f where "f L = (length (L:: real list) = ((n::nat)+1) ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs)))" for L
have "(∃x.∃L. f (L@[x])) = (∃L. f L)"
by (metis (full_types) One_nat_def add_Suc_right f_def list.size(3) nat.simps(3) rev_exhaust)
then have "((∃x. ∃L. length (L@[x]) = (n+1) ∧ (∀a∈set al. aEval a ((L@[x]) @ xs)) ∧ (∀f∈set fl. eval f ((L@[x]) @ xs)))
=
(∃L. length L = (n+1) ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs))))"
unfolding f_def by simp
}
then have h2 : "∀n al fl. (
(∃x. ∃L. length (L@[x]) = (n+1) ∧ (∀a∈set al. aEval a ((L@[x]) @ xs)) ∧ (∀f∈set fl. eval f ((L@[x]) @ xs)))
=
(∃L. length L = (n+1) ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs)))
)"
by simp
{ fix al fl n
define f where "f al fl n = (∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs)))" for al fl n
have "f al fl (n+1) = (case (case (al, fl, n) of (A, A', d) ⇒ (A, A',d+1)) of
(al, fl, n) ⇒ f al fl n)"
by simp
then have "(∃L. length L = (n+1) ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs)))
= (
case (case (al, fl, n) of (A, A', d) ⇒ (A, A',d+1)) of
(al, fl, n) ⇒
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs)))"
unfolding f_def by simp
}
then have h3 : "
(∃(al, fl, n)∈set (dnf_modified φ).
∃L. length L = (n+1) ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs)))
= (∃a∈set (dnf_modified φ).
case (case a of (A, A', d) ⇒ (A, A',d+1)) of
(al, fl, n) ⇒
∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs)))"
by (smt case_prodE case_prodI2) (* takes a second *)
show ?case using ExQ h1 h2 h3 by simp
next
case (ExN x1 φ)

show ?case
apply simp proof safe
fix a aa b L
have takedrop: "(take b L @ drop b L @ xs) = (L @ xs)" by auto
assume h: "(a, aa, b) ∈ set (dnf_modified φ)" "length L = b + x1" "∀a∈set a. aEval a (L @ xs)" "∀f∈set aa. eval f (L @ xs)"
show "∃l. length l = x1 ∧ eval φ (l @ xs)"
apply(rule exI[where x="drop b L"])
apply auto
using h(2) apply simp
unfolding ExN[symmetric]
apply(rule bexI[where x="(a,aa,b)"])
apply simp
apply(rule exI[where x="take b L"])
apply auto
using h apply simp
unfolding takedrop
using h by auto
next
fix l
assume h: "eval φ (l @ xs)" "x1 = length l"
obtain al fl n where h1 : "(al, fl, n)∈set (dnf_modified φ)" "∃L. length L = n ∧ (∀a∈set al. aEval a (L @ l @ xs)) ∧ (∀f∈set fl. eval f (L @ l @ xs))"
using h(1) unfolding ExN[symmetric]
by blast
obtain L where h2 : "length L = n" "(∀a∈set al. aEval a (L @ l @ xs))" "(∀f∈set fl. eval f (L @ l @ xs))" using h1(2) by metis
show "∃x∈set (dnf_modified φ).
case case x of (A, A', d) ⇒ (A, A', d + length l) of
(al, fl, n) ⇒ ∃L. length L = n ∧ (∀a∈set al. aEval a (L @ xs)) ∧ (∀f∈set fl. eval f (L @ xs))"
apply(rule bexI[where x="(al,fl,n)"])
apply simp
apply(rule exI[where x="L@l"])
apply auto
using h2 h1 by auto
qed
qed auto
end```