Theory Virtual_Substitution.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))"
    by (simp add: Bex_def_raw)
  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