Theory VSAlgos

section "Algorithms"
subsection "Equality VS Helper Functions"
theory VSAlgos
  imports Debruijn Optimizations
begin


text "This is a subprocess which simply separates out the equality atoms from the other kinds of atoms

Note that we search for equality atoms that are of degree one or two

This is used within the equalityVS algorithm"
fun find_eq :: "nat ⇒ atom list ⇒ real mpoly list * atom list" where
  "find_eq var [] = ([],[])"|
  "find_eq var ((Less p)#as) = (let (A,B) = find_eq var as in (A,Less p#B))" |
  "find_eq var ((Eq p)#as) = (let (A,B) = find_eq var as in
   if MPoly_Type.degree p var < 3 ∧ MPoly_Type.degree p var ≠ 0
  then (p # A,B) 
  else (A,Eq p # B)
)"|
  "find_eq var ((Leq p)#as) = (let (A,B) = find_eq var as in (A,Leq p#B))" |
  "find_eq var ((Neq p)#as) = (let (A,B) = find_eq var as in (A,Neq p#B))"




(* given ax^2+bx+c returns formula representing a=0 and b=0 and c=0 *)
fun split_p :: "nat ⇒ real mpoly ⇒ atom fm" where
  "split_p var p = And (Atom (Eq (isolate_variable_sparse p var 2)))
                (And (Atom (Eq (isolate_variable_sparse p var 1)))
                     (Atom (Eq (isolate_variable_sparse p var 0))))"



text "
The linearsubstitution virtually substitutes in an equation of $b*x+c=0$ into an arbitrary atom

linearsubstitution x b c (Eq p) = F corresponds to removing variable x from polynomial p and replacing
it with an equivalent function F where F doesn't mention variable x

If there exists a way to assign variables that makes p = 0 true,
then that same set of variables will make F true

If there exists a way to assign variables that makes F true and also have b*x+c=0,
then that same set of variables will make p=0 true

Same applies for other kinds of atoms that aren't equality
"
fun linear_substitution :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ atom ⇒ atom" where
  "linear_substitution var a b (Eq p) = 
  (let d = MPoly_Type.degree p var in
    (Eq (∑i∈{0..<(d+1)}.  isolate_variable_sparse p var i * (a^i) * (b^(d-i))))
  )" |
  "linear_substitution var a b (Less p) = 
  (let d = MPoly_Type.degree p var in
    let P = (∑i∈{0..<(d+1)}. isolate_variable_sparse p var i * (a^i) * (b^(d-i))) in
      (Less(P * (b ^ (d mod 2))))
    )"|
  "linear_substitution var a b (Leq p) = 
  (let d = MPoly_Type.degree p var in
    let P = (∑i∈{0..<(d+1)}. isolate_variable_sparse p var i * (a^i) * (b^(d-i))) in
      (Leq(P * (b ^ (d mod 2))))
    )"|
  "linear_substitution var a b (Neq p) = 
  (let d = MPoly_Type.degree p var in
    (Neq (∑i∈{0..<(d+1)}.  isolate_variable_sparse p var i * (a^i) * (b^(d-i))))
  )"

fun linear_substitution_fm_helper :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ atom fm ⇒ nat ⇒ atom fm" where
  "linear_substitution_fm_helper var b c F z = liftmap (λx.λA. Atom(linear_substitution (var+x) (liftPoly 0 x b) (liftPoly 0 x c) A)) F z"

fun linear_substitution_fm :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ atom fm ⇒ atom fm" where
  "linear_substitution_fm var b c F = linear_substitution_fm_helper var b c F 0"


text "
quadraticpart1 var a b A takes in an expression of the form
(a+b * sqrt(c))/d
for an arbitrary c and substitutes it in for the variable var in the atom A
"
fun quadratic_part_1 :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ atom ⇒ real mpoly" where
  "quadratic_part_1 var a b d (Eq p) = (
  let deg = MPoly_Type.degree p var in
  ∑i∈{0..<(deg+1)}. (isolate_variable_sparse p var i) * ((a+b*(Var var))^i) * (d^(deg - i))
)" |
  "quadratic_part_1 var a b d (Less p) = (
  let deg = MPoly_Type.degree p var in
  let P = ∑i∈{0..<(deg+1)}. (isolate_variable_sparse p var i) * ((a+b*(Var var))^i) * (d^(deg - i)) in
  P * (d ^ (deg mod 2))
)"|
  "quadratic_part_1 var a b d (Leq p) = (
  let deg = MPoly_Type.degree p var in
  let P = ∑i∈{0..<(deg+1)}. (isolate_variable_sparse p var i) * ((a+b*(Var var))^i) * (d^(deg - i)) in
  P * (d ^ (deg mod 2))
)"|
  "quadratic_part_1 var a b d (Neq p) = (
  let deg = MPoly_Type.degree p var in
  ∑i∈{0..<(deg+1)}. (isolate_variable_sparse p var i) * ((a+b*(Var var))^i) * (d^(deg - i))
)"

fun quadratic_part_2 :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly" where
  "quadratic_part_2 var sq p = (
  let deg = MPoly_Type.degree p var in
  ∑i∈{0..<deg+1}. 
    (isolate_variable_sparse p var i)*(sq^(i div 2)) * (Const(of_nat(i mod 2))) * (Var var) 
   +(isolate_variable_sparse p var i)*(sq^(i div 2)) * Const(1-of_nat(i mod 2))
)
"

text"
quadraticsub var a b c d A represents virtually substituting an expression of the form
(a+b*sqrt(c))/d into variable var in atom A
"
primrec quadratic_sub :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ atom ⇒ atom fm" where
  "quadratic_sub var a b c d (Eq p) = (
    let (p1::real mpoly) = quadratic_part_1 var a b d (Eq p) in
    let (p2::real mpoly) = quadratic_part_2 var c p1 in
    let (A::real mpoly) = isolate_variable_sparse p2 var 0 in
    let (B::real mpoly) = isolate_variable_sparse p2 var 1 in
    And
      (Atom(Leq (A*B)))
      (Atom (Eq (A^2-B^2*c)))
)" | 
  "quadratic_sub var a b c d (Less p) = (
    let (p1::real mpoly) = quadratic_part_1 var a b d (Less p) in
    let (p2::real mpoly) = quadratic_part_2 var c p1 in
    let (A::real mpoly) = isolate_variable_sparse p2 var 0 in
    let (B::real mpoly) = isolate_variable_sparse p2 var 1 in
    Or
      (And
        (Atom(Less(A)))
        (Atom (Less (B^2*c-A^2))))
      (And
        (Atom(Leq B))
        (Or
          (Atom(Less A))
          (Atom(Less (A^2-B^2*c)))))
)" |
  "quadratic_sub var a b c d (Leq p) = (
    let (p1::real mpoly) = quadratic_part_1 var a b d (Leq p) in
    let (p2::real mpoly) = quadratic_part_2 var c p1 in
    let (A::real mpoly) = isolate_variable_sparse p2 var 0 in
    let (B::real mpoly) = isolate_variable_sparse p2 var 1 in
    Or
      (And
        (Atom(Leq(A)))
        (Atom (Leq(B^2*c-A^2))))
      (And
        (Atom(Leq B))
        (Atom(Leq (A^2-B^2*c))))
)" |
  "quadratic_sub var a b c d (Neq p) = (
    let (p1::real mpoly) = quadratic_part_1 var a b d (Neq p) in
    let (p2::real mpoly) = quadratic_part_2 var c p1 in
    let (A::real mpoly) = isolate_variable_sparse p2 var 0 in
    let (B::real mpoly) = isolate_variable_sparse p2 var 1 in
    Or
      (Atom(Less(-A*B)))
      (Atom (Neq(A^2-B^2*c)))
)"


fun quadratic_sub_fm_helper :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ atom fm ⇒ nat ⇒ atom fm" where
  "quadratic_sub_fm_helper var a b c d F z = liftmap (λx.λA. quadratic_sub (var+x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d) A) F z"

fun quadratic_sub_fm :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ atom fm ⇒ atom fm" where
  "quadratic_sub_fm var a b c d F = quadratic_sub_fm_helper var a b c d F 0"

subsection "General VS Helper Functions"
  (*
  allZero p var
  takes in a polynomial of the form sum a_i x^i where x is the variable var
  returns the formula where all a_i=0
*)
fun allZero :: "real mpoly ⇒ nat ⇒ atom fm" where
  "allZero p var = list_conj [Atom(Eq(isolate_variable_sparse p var i)). i <- [0..<(MPoly_Type.degree p var)+1]]"

fun alternateNegInfinity :: "real mpoly ⇒ nat ⇒ atom fm" where
  "alternateNegInfinity p var = foldl (λF.λi.
let a_n = isolate_variable_sparse p var i in
let exp = (if i mod 2 = 0 then Const(1) else Const(-1)) in
  or (Atom(Less (exp * a_n)))
    (and (Atom (Eq a_n)) F)
) FalseF ([0..<((MPoly_Type.degree p var)+1)])"


(*
  substNegInfity var a
  substitutes negative infinity for the variable var in the atom a
  defined in pages 610-611
*)
fun substNegInfinity :: "nat ⇒ atom ⇒ atom fm" where
  "substNegInfinity var (Eq p) = allZero p var " |
  "substNegInfinity var (Less p) = alternateNegInfinity p var"|
  "substNegInfinity var (Leq p) = Or (alternateNegInfinity p var) (allZero p var)"|
  "substNegInfinity var (Neq p) = Neg (allZero p var)"

(*
  convertDerivative var p
  is equivalent to p^+ < 0 defined on page 615 around variable var
*)
function convertDerivative :: "nat ⇒ real mpoly ⇒ atom fm" where
  "convertDerivative var p = (if (MPoly_Type.degree p var) = 0 then Atom (Less p) else
  Or (Atom (Less p)) (And (Atom(Eq p)) (convertDerivative var (derivative var p))))"
  by pat_completeness auto
termination
  apply(relation "measures [λ(var,p). MPoly_Type.degree p var]")
  apply auto
  using degree_derivative
  by (metis less_add_one)

(*
  substInfinitesimalLinear var b c A
  substitutes -c/b+epsilon for variable var in atom A
  assumes b is nonzero
  defined in page 615
*)
fun substInfinitesimalLinear :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ atom ⇒ atom fm" where
  "substInfinitesimalLinear var b c (Eq p) = allZero p var"|
  "substInfinitesimalLinear var b c (Less p) = 
  liftmap
    (λx. λA. Atom(linear_substitution (var+x) (liftPoly 0 x b) (liftPoly 0 x c) A)) 
    (convertDerivative var p)
    0"|
  "substInfinitesimalLinear var b c (Leq p) = 
Or
  (allZero p var)
  (liftmap
    (λx. λA. Atom(linear_substitution (var+x) (liftPoly 0 x b) (liftPoly 0 x c) A)) 
    (convertDerivative var p)
    0)"|
  "substInfinitesimalLinear var b c (Neq p) = neg (allZero p var)"

(*
  substInfinitesimalQuadratic var a b c A
  substitutes (quadratic equation)+epsilon for variable var in atom A
  assumes a is nonzero and the determinant is positive
  defined in page 615
*)
fun substInfinitesimalQuadratic :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ atom ⇒ atom fm" where
  "substInfinitesimalQuadratic var a b c d (Eq p) = allZero p var"|
  "substInfinitesimalQuadratic var a b c d (Less p) = quadratic_sub_fm var a b c d (convertDerivative var p)"|
  "substInfinitesimalQuadratic var a b c d (Leq p) = 
Or
  (allZero p var)
  (quadratic_sub_fm var a b c d (convertDerivative var p))"|
  "substInfinitesimalQuadratic var a b c d (Neq p) = neg (allZero p var)"


fun substInfinitesimalLinear_fm :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ atom fm ⇒ atom fm" where
  "substInfinitesimalLinear_fm var b c F = liftmap (λx.λA. substInfinitesimalLinear (var+x) (liftPoly 0 x b) (liftPoly 0 x c) A) F 0"


fun substInfinitesimalQuadratic_fm :: "nat ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ real mpoly ⇒ atom fm ⇒ atom fm" where
  "substInfinitesimalQuadratic_fm var a b c d F = liftmap (λx.λA. substInfinitesimalQuadratic (var+x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d) A) F 0"

subsection "VS Algorithms"

text
  "elimVar var L F
  attempts to do quadratic elimination on the variable defined by var.
  L is the list of conjuctive atoms, F is a list of unnecessary garbage"
fun elimVar :: "nat ⇒ atom list ⇒ (atom fm) list ⇒ atom ⇒ atom fm" where
  "elimVar var L F (Eq p) =  (
  let (a,b,c) = get_coeffs var p in

   (Or 
      
      (And (And (Atom (Eq a)) (Atom (Neq b)))
      (list_conj (
        (map (λa. Atom (linear_substitution var (-c) b a)) L)@
        (map (linear_substitution_fm var (-c) b) F)
        )))
      

      (And (Atom (Neq a)) (And (Atom(Leq (-(b^2)+4*a*c)))
        (Or (list_conj (
        (map (quadratic_sub var (-b) 1 (b^2-4*a*c) (2*a)) L)@
        (map (quadratic_sub_fm var (-b) 1 (b^2-4*a*c) (2*a)) F)
        ))
        (list_conj (
        (map (quadratic_sub var (-b) (-1) (b^2-4*a*c) (2*a)) L)@
        (map (quadratic_sub_fm var (-b) (-1) (b^2-4*a*c) (2*a)) F)
        ))
       ))
      ))

)" |
  "elimVar var L F (Less p) =  (
  let (a,b,c) = get_coeffs var p in
    (Or 
      
      (And (And (Atom (Eq a)) (Atom (Neq b)))
      (list_conj (
          (map (substInfinitesimalLinear var (-c) b) L)
          @(map (substInfinitesimalLinear_fm var (-c) b) F)
      )))
      

      (And (Atom (Neq a)) (And (Atom(Leq (-(b^2)+4*a*c)))
        (Or (list_conj (
        (map (substInfinitesimalQuadratic var (-b) 1 (b^2-4*a*c) (2*a)) L)@
        (map (substInfinitesimalQuadratic_fm var (-b) 1 (b^2-4*a*c) (2*a)) F)
        ))
        (list_conj (
        (map (substInfinitesimalQuadratic var (-b) (-1) (b^2-4*a*c) (2*a)) L)@
        (map (substInfinitesimalQuadratic_fm var (-b) (-1) (b^2-4*a*c) (2*a)) F)
        ))
       ))
      ))
)"|
  "elimVar var L F (Neq p) =  (
  let (a,b,c) = get_coeffs var p in
    (Or 
      
      (And (And (Atom (Eq a)) (Atom (Neq b)))
      (list_conj (
          (map (substInfinitesimalLinear var (-c) b) L)
          @(map (substInfinitesimalLinear_fm var (-c) b) F)
      )))
      

      (And (Atom (Neq a)) (And (Atom(Leq (-(b^2)+4*a*c)))
        (Or (list_conj (
        (map (substInfinitesimalQuadratic var (-b) 1 (b^2-4*a*c) (2*a)) L)@
        (map (substInfinitesimalQuadratic_fm var (-b) 1 (b^2-4*a*c) (2*a)) F)
        ))
        (list_conj (
        (map (substInfinitesimalQuadratic var (-b) (-1) (b^2-4*a*c) (2*a)) L)@
        (map (substInfinitesimalQuadratic_fm var (-b) (-1) (b^2-4*a*c) (2*a)) F)
        ))
       ))
      )))
"|
  "elimVar var L F (Leq p) =  (
  let (a,b,c) = get_coeffs var p in

   (Or 
      
      (And (And (Atom (Eq a)) (Atom (Neq b)))
      (list_conj (
        (map (λa. Atom (linear_substitution var (-c) b a)) L)@
        (map (linear_substitution_fm var (-c) b) F)
        )))
      

      (And (Atom (Neq a)) (And (Atom(Leq (-(b^2)+4*a*c)))
        (Or (list_conj (
        (map (quadratic_sub var (-b) 1 (b^2-4*a*c) (2*a)) L)@
        (map (quadratic_sub_fm var (-b) 1 (b^2-4*a*c) (2*a)) F)
        ))
        (list_conj (
        (map (quadratic_sub var (-b) (-1) (b^2-4*a*c) (2*a)) L)@
        (map (quadratic_sub_fm var (-b) (-1) (b^2-4*a*c) (2*a)) F)
        ))
       ))
      ))

)"

(* single virtual substitution of equality *)
fun qe_eq_one :: "nat ⇒ atom list ⇒ atom fm list ⇒ atom fm" where
  "qe_eq_one var L F = 
    (case find_eq var L of 
        (p#A,L') ⇒ Or (And (Neg (split_p var p))
                      ((elimVar var L F) (Eq p))
                    )
                    (And (split_p var p) 
                      (list_conj (map Atom ((map Eq A)  @ L') @ F))
                    )
      | ([],L') ⇒ list_conj ((map Atom L) @ F)
)"


fun check_nonzero_const :: "real mpoly ⇒ bool"where
  "check_nonzero_const p = (case get_if_const p of Some x ⇒ x ≠ 0 | None ⇒ False)"

fun find_lucky_eq :: "nat ⇒ atom list ⇒ real mpoly option"where
  "find_lucky_eq v [] = None"|
  "find_lucky_eq v (Eq p#L) = 
(let (a,b,c) = get_coeffs v p in
(if (MPoly_Type.degree p v = 1 ∨ MPoly_Type.degree p v = 2) ∧ (check_nonzero_const a ∨ check_nonzero_const b ∨ check_nonzero_const c) then Some p else
find_lucky_eq v L
))"|
  "find_lucky_eq v (_#L) = find_lucky_eq v L"


fun luckyFind :: "nat ⇒ atom list ⇒ atom fm list ⇒ atom fm option" where
  "luckyFind v L F = (case find_lucky_eq v L of Some p ⇒ Some ((elimVar v L F) (Eq p)) | None ⇒ None)"

fun luckyFind' :: "nat ⇒ atom list ⇒ atom fm list ⇒ atom fm" where
  "luckyFind' v L F = (case find_lucky_eq v L of Some p ⇒ (elimVar v L F) (Eq p) | None ⇒ And (list_conj (map Atom L)) (list_conj F))"


fun find_luckiest_eq :: "nat ⇒ atom list ⇒ real mpoly option"where
  "find_luckiest_eq v [] = None"|
  "find_luckiest_eq v (Eq p#L) = 
(if (MPoly_Type.degree p v = 1 ∨ MPoly_Type.degree p v = 2) then
(let (a,b,c) = get_coeffs v p in
 (case get_if_const a of None ⇒ find_luckiest_eq v L
 | Some a ⇒ (case get_if_const b of None ⇒ find_luckiest_eq v L
 | Some b ⇒ (case get_if_const c of None ⇒ find_luckiest_eq v L
 | Some c ⇒ if a≠0∨b≠0∨c≠0 then Some p else find_luckiest_eq v L))))
 else
find_luckiest_eq v L
)"|
  "find_luckiest_eq v (_#L) = find_luckiest_eq v L"



fun luckiestFind :: "nat ⇒ atom list ⇒ atom fm list ⇒ atom fm" where
  "luckiestFind v L F = (case find_luckiest_eq v L of Some p ⇒ (elimVar v L F) (Eq p) | None ⇒ And (list_conj (map Atom L)) (list_conj F))"


primrec qe_eq_repeat_helper :: "nat ⇒ real mpoly list ⇒ atom list ⇒ atom fm list ⇒ atom fm" where
  "qe_eq_repeat_helper var [] L F = list_conj ((map Atom L) @ F)"|
  "qe_eq_repeat_helper var (p#A) L F = 
  Or (And (Neg (split_p var p))
    ((elimVar var ((map Eq (p#A)) @ L) F) (Eq p))
  )
  (And (split_p var p) 
    (qe_eq_repeat_helper var A L F)
  )"

fun qe_eq_repeat :: "nat ⇒ atom list ⇒ atom fm list ⇒ atom fm" where
  "qe_eq_repeat var L F = 
    (case luckyFind var L F of Some(F) ⇒ F | None ⇒ 
    (let (A,L') = find_eq var L in
      qe_eq_repeat_helper var A L' F 
)
)
"

fun all_degree_2 :: "nat ⇒ atom list ⇒ bool" where
  "all_degree_2 var [] = True"|
  "all_degree_2 var (Eq p#as) = ((MPoly_Type.degree p var ≤ 2)∧(all_degree_2 var as))"|
  "all_degree_2 var (Less p#as) = ((MPoly_Type.degree p var ≤ 2)∧(all_degree_2 var as))"|
  "all_degree_2 var (Leq p#as) = ((MPoly_Type.degree p var ≤ 2)∧(all_degree_2 var as))"|
  "all_degree_2 var (Neq p#as) = ((MPoly_Type.degree p var ≤ 2)∧(all_degree_2 var as))"

fun gen_qe :: "nat ⇒ atom list ⇒ atom fm list ⇒ atom fm" where
  "gen_qe var L F = (case F of 
[] ⇒ (case luckyFind var L [] of Some F ⇒ F | None ⇒ (
    (if all_degree_2 var L 
      then list_disj (list_conj (map (substNegInfinity var) L) # (map (elimVar var L []) L)) 
  else (qe_eq_repeat var L []))))
| _ ⇒ qe_eq_repeat var L F
)"

subsection "DNF"

fun dnf :: "atom fm ⇒ (atom list * atom fm list) list" where
  "dnf TrueF = [([],[])]" |
  "dnf FalseF = []" |
  "dnf (Atom φ) = [([φ],[])]" |
  "dnf (And φ⇩1 φ⇩2) = [(A@B,A'@B').(A,A')←dnf φ⇩1,(B,B')←dnf φ⇩2]" |
  "dnf (Or φ⇩1 φ⇩2) = dnf φ⇩1 @ dnf φ⇩2" |
  "dnf (ExQ φ) = [([],[ExQ φ])]" |
  "dnf (Neg φ) = [([],[Neg φ])]"|
  "dnf (AllQ φ) = [([],[AllQ φ])]"|
  "dnf (AllN i φ) = [([],[AllN i φ])]"|
  "dnf (ExN i φ) = [([],[ExN i φ])]"

text "
  dnf F
  returns the \"disjunctive normal form\" of F, but since F can contain quantifiers, we return
  (L,R,n) terms in a list. each term in the list represents a conjunction over the outside disjunctive list
    
  L is all the atoms we are able to reach, we are allowed to go underneath exists binders
  
  R is the remaining formulas (negation exists cannot be simplified) which are also under the same number
      of exist binders.

  n is the total number of binders each conjunct has
"
fun dnf_modified :: "atom fm ⇒ (atom list * atom fm list * nat) list" where
  "dnf_modified TrueF = [([],[],0)]" |
  "dnf_modified FalseF = []" |
  "dnf_modified (Atom φ) = [([φ],[],0)]" |
  "dnf_modified (And φ⇩1 φ⇩2) = [
  let A = map (liftAtom d1 d2) A in
  let B = map (liftAtom 0 d1) B in
  let A' = map (liftFm d1 d2) A' in
  let B' = map (liftFm 0 d1) B' in
    (A @ B, A' @ B',d1+d2).
  (A,A',d1) ← dnf_modified φ⇩1, (B,B',d2) ← dnf_modified φ⇩2]" |
  "dnf_modified (Or φ⇩1 φ⇩2) = dnf_modified φ⇩1 @ dnf_modified φ⇩2" |
  "dnf_modified (ExQ φ) = [(A,A',d+1). (A,A',d) ← dnf_modified φ]" |
  "dnf_modified (Neg φ) = [([],[Neg φ],0)]"|
  "dnf_modified (AllQ φ) = [([],[AllQ φ],0)]"|
  "dnf_modified (AllN i φ) = [([],[AllN i φ],0)]"|
  "dnf_modified (ExN i φ) = [(A,A',d+i). (A,A',d) ← dnf_modified φ]"


(*
repeatedly applies nnf and dnf on subformulas and then attempts to eliminate the quantifier based
on the qe quantifier elimination method given. Works on innermost variables first and builds out
*)
fun QE_dnf :: "(atom fm ⇒ atom fm) ⇒ (nat ⇒ nat ⇒ atom list ⇒ atom fm list ⇒ atom fm) ⇒ atom fm ⇒ atom fm" where
  "QE_dnf opt step (And φ⇩1 φ⇩2) = and (QE_dnf opt step φ⇩1) (QE_dnf opt step φ⇩2)" |
  "QE_dnf opt step (Or φ⇩1 φ⇩2) = or (QE_dnf opt step φ⇩1) (QE_dnf opt step φ⇩2)" |
  "QE_dnf opt step (Neg φ) = neg(QE_dnf opt step φ)" |
  "QE_dnf opt step (ExQ φ) = list_disj [ExN (n+1) (step 1 n al fl). (al,fl,n)←(dnf_modified(opt(QE_dnf opt step φ)))]"|
  "QE_dnf opt step (TrueF) = TrueF"|
  "QE_dnf opt step (FalseF) = FalseF"|
  "QE_dnf opt step (Atom a) = simp_atom a"|
  "QE_dnf opt step (AllQ φ) = Neg(list_disj [ExN (n+1) (step 1 n al fl). (al,fl,n)←(dnf_modified(opt(neg(QE_dnf opt step φ))))])"|
  "QE_dnf opt step (ExN 0 φ) = QE_dnf opt step φ"|
  "QE_dnf opt step (AllN 0 φ) = QE_dnf opt step φ"|
  "QE_dnf opt step (AllN (Suc i) φ) = Neg(list_disj [ExN (n+i+1) (step (Suc i) (n+i) al fl). (al,fl,n)←(dnf_modified(opt(neg(QE_dnf opt step φ))))])"|
  "QE_dnf opt step (ExN (Suc i) φ) = list_disj [ExN (n+i+1) (step (Suc i) (n+i) al fl). (al,fl,n)←(dnf_modified(opt(QE_dnf opt step φ)))]"

fun QE_dnf' :: "(atom fm ⇒ atom fm) ⇒ (nat ⇒ (atom list * atom fm list * nat) list  ⇒ atom fm) ⇒ atom fm ⇒ atom fm" where 
  "QE_dnf' opt step (And φ⇩1 φ⇩2) = and (QE_dnf' opt step φ⇩1) (QE_dnf' opt step φ⇩2)" |
  "QE_dnf' opt step (Or φ⇩1 φ⇩2) = or (QE_dnf' opt step φ⇩1) (QE_dnf' opt step φ⇩2)" |
  "QE_dnf' opt step (Neg φ) = neg(QE_dnf' opt step φ)" |
  "QE_dnf' opt step (ExQ φ) = step 1 (dnf_modified(opt(QE_dnf' opt step φ)))"|
  "QE_dnf' opt step (TrueF) = TrueF"|
  "QE_dnf' opt step (FalseF) = FalseF"|
  "QE_dnf' opt step (Atom a) = simp_atom a"|
  "QE_dnf' opt step (AllQ φ) = Neg(step 1 (dnf_modified(opt(neg(QE_dnf' opt step φ)))))"|
  "QE_dnf' opt step (ExN 0 φ) = QE_dnf' opt step φ"|
  "QE_dnf' opt step (AllN 0 φ) = QE_dnf' opt step φ"|
  "QE_dnf' opt step (AllN (Suc i) φ) = Neg(step  (Suc i) (dnf_modified(opt(neg(QE_dnf' opt step φ)))))"|
  "QE_dnf' opt step (ExN (Suc i) φ) = step (Suc i) (dnf_modified(opt(QE_dnf' opt step φ)))"

subsection "Repeat QE multiple times"

fun countQuantifiers :: "atom fm ⇒ nat" where
  "countQuantifiers (Atom _) = 0"|
  "countQuantifiers (TrueF) = 0"|
  "countQuantifiers (FalseF) = 0"|
  "countQuantifiers (And a b) = countQuantifiers a + countQuantifiers b"|
  "countQuantifiers (Or a b) = countQuantifiers a + countQuantifiers b"|
  "countQuantifiers (Neg a) = countQuantifiers a"|
  "countQuantifiers (ExQ a) = countQuantifiers a + 1"|
  "countQuantifiers (AllQ a) = countQuantifiers a + 1"|
  "countQuantifiers (ExN n a) = countQuantifiers a + n"|
  "countQuantifiers (AllN n a) = countQuantifiers a + n"

fun repeatAmountOfQuantifiers_helper :: "(atom fm ⇒ atom fm) ⇒ nat ⇒ atom fm ⇒ atom fm" where
  "repeatAmountOfQuantifiers_helper step 0 F = F"|
  "repeatAmountOfQuantifiers_helper step (Suc i) F = repeatAmountOfQuantifiers_helper step i (step F)"

fun repeatAmountOfQuantifiers :: "(atom fm ⇒ atom fm) ⇒ atom fm ⇒ atom fm" where
  "repeatAmountOfQuantifiers step F = (
let F = step F in
let n = countQuantifiers F in
repeatAmountOfQuantifiers_helper step n F
)"

end