Theory Virtual_Substitution.Optimizations

section "Optimizations"
theory Optimizations
  imports Debruijn
begin

text "Does negation normal form conversion"
fun nnf :: "atom fm ⇒ atom fm" where
  "nnf TrueF = TrueF" |
  "nnf FalseF = FalseF " |
  "nnf (Atom a) = Atom a" |
  "nnf (And φ⇩1 φ⇩2) = And (nnf φ⇩1) (nnf φ⇩2)" |
  "nnf (Or φ⇩1 φ⇩2) = Or (nnf φ⇩1) (nnf φ⇩2)" |
  "nnf (ExQ φ) = ExQ (nnf φ)" |
  "nnf (AllQ φ) = AllQ (nnf φ)"|
  "nnf (AllN i φ) = AllN i (nnf φ)"|
  "nnf (ExN i φ) = ExN i (nnf φ)" |
  "nnf (Neg TrueF) = FalseF" |
  "nnf (Neg FalseF) = TrueF" |
  "nnf (Neg (Neg φ)) = (nnf φ)" |
  "nnf (Neg (And φ⇩1 φ⇩2)) = (Or (nnf (Neg φ⇩1)) (nnf (Neg φ⇩2)))" |
  "nnf (Neg (Or φ⇩1 φ⇩2)) = (And (nnf (Neg φ⇩1)) (nnf (Neg φ⇩2)))" |
  "nnf (Neg (Atom a)) = Atom(aNeg a)" |
  "nnf (Neg (ExQ φ)) = AllQ (nnf (Neg φ))" |
  "nnf (Neg (AllQ φ)) = ExQ (nnf (Neg φ))"|
  "nnf (Neg (AllN i φ)) = ExN i (nnf (Neg φ))"|
  "nnf (Neg (ExN i φ)) = AllN i (nnf (Neg φ))"


subsection "Simplify Constants"

fun simp_atom :: "atom ⇒ atom fm" where
  "simp_atom (Eq p)   = (case get_if_const p of None ⇒ Atom(Eq   p) | Some(r) ⇒ (if r=0 then TrueF else FalseF))"|
  "simp_atom (Less p) = (case get_if_const p of None ⇒ Atom(Less p) | Some(r) ⇒ (if r<0 then TrueF else FalseF))"|
  "simp_atom (Leq p)  = (case get_if_const p of None ⇒ Atom(Leq  p) | Some(r) ⇒ (if r≤0 then TrueF else FalseF))"|
  "simp_atom (Neq p)  = (case get_if_const p of None ⇒ Atom(Neq  p) | Some(r) ⇒ (if r≠0 then TrueF else FalseF))"

fun simpfm :: "atom fm ⇒ atom fm" where
  "simpfm TrueF = TrueF"|
  "simpfm FalseF = FalseF"|
  "simpfm (Atom a) = simp_atom a"|
  "simpfm (And φ ψ) = and (simpfm φ) (simpfm ψ)"|
  "simpfm (Or φ ψ) = or (simpfm φ) (simpfm ψ)"|
  "simpfm (ExQ φ) = ExQ (simpfm φ)"|
  "simpfm (Neg φ) = neg (simpfm φ)"|
  "simpfm (AllQ φ) = AllQ(simpfm φ)"|
  "simpfm (AllN i φ) = AllN i (simpfm φ)"|
  "simpfm (ExN i φ) = ExN i (simpfm φ)"


subsection "Group Quantifiers"

fun groupQuantifiers :: "atom fm ⇒ atom fm" where
  "groupQuantifiers TrueF = TrueF"|
  "groupQuantifiers FalseF = FalseF"|
  "groupQuantifiers (And A B) = And (groupQuantifiers A) (groupQuantifiers B)"|
  "groupQuantifiers (Or A B) = Or (groupQuantifiers A) (groupQuantifiers B)"|
  "groupQuantifiers (Neg A) = Neg (groupQuantifiers A)"|
  "groupQuantifiers (Atom A) = Atom A"|
  "groupQuantifiers (ExQ (ExQ A)) = groupQuantifiers (ExN 2 A)"|
  "groupQuantifiers (ExQ (ExN j A)) = groupQuantifiers (ExN (j+1) A)"|
  "groupQuantifiers (ExN j (ExQ A)) = groupQuantifiers (ExN (j+1) A)"|
  "groupQuantifiers (ExN i (ExN j A)) = groupQuantifiers (ExN (i+j) A)"|
  "groupQuantifiers (ExQ A) = ExQ (groupQuantifiers A)"|
  "groupQuantifiers (AllQ (AllQ A)) = groupQuantifiers (AllN 2 A)"|
  "groupQuantifiers (AllQ (AllN j A)) = groupQuantifiers (AllN (j+1) A)"|
  "groupQuantifiers (AllN j (AllQ A)) = groupQuantifiers (AllN (j+1) A)"|
  "groupQuantifiers (AllN i (AllN j A)) = groupQuantifiers (AllN (i+j) A)"|
  "groupQuantifiers (AllQ A) = AllQ (groupQuantifiers A)"|
  "groupQuantifiers (AllN j A) = AllN j A"|
  "groupQuantifiers (ExN j A) = ExN j A"

subsection "Clear Quantifiers"

text "clearQuantifiers F goes through the formula F and removes all quantifiers who's variables
are not present in the formula. For example, clearQuantifiers (ExQ(TrueF)) evaluates to TrueF. This
preserves the truth value of the formula as shown in the clearQuantifiers\\_eval proof. This is used
within the QE overall procedure to eliminate quantifiers in the cases where QE was successful."
fun depth' :: "'a fm ⇒ nat"where
  "depth' TrueF = 1"|
  "depth' FalseF = 1"|
  "depth' (Atom _) = 1"|
  "depth' (And φ ψ) = max (depth' φ) (depth' ψ) + 1"|
  "depth' (Or φ ψ) = max (depth' φ) (depth' ψ) + 1"|
  "depth' (Neg φ) = depth' φ + 1"|
  "depth' (ExQ φ) = depth' φ + 1"|
  "depth' (AllQ φ) = depth' φ + 1"|
  "depth' (AllN i φ) = depth' φ  + i * 2 + 1"|
  "depth' (ExN i φ) = depth' φ  + i * 2 + 1"

function clearQuantifiers :: "atom fm ⇒ atom fm" where
  "clearQuantifiers TrueF = TrueF"|
  "clearQuantifiers FalseF = FalseF"|
  "clearQuantifiers (Atom a) = simp_atom a"|
  "clearQuantifiers (And φ ψ) = and (clearQuantifiers φ) (clearQuantifiers ψ)"|
  "clearQuantifiers (Or φ ψ) = or (clearQuantifiers φ) (clearQuantifiers ψ)"|
  "clearQuantifiers (Neg φ) = neg (clearQuantifiers φ)"|
  "clearQuantifiers (ExQ φ) = 
  (let φ' = clearQuantifiers φ in
  (if freeIn 0 φ' then lowerFm 0 1 φ' else ExQ φ'))"|
  "clearQuantifiers (AllQ φ) = 
  (let φ' = clearQuantifiers φ in
  (if freeIn 0 φ' then lowerFm 0 1 φ' else AllQ φ'))"|
  "clearQuantifiers (ExN 0 φ) = clearQuantifiers φ"|
  "clearQuantifiers (ExN (Suc i) φ) = clearQuantifiers (ExN i (ExQ φ))"|
  "clearQuantifiers (AllN 0 φ) = clearQuantifiers φ"|
  "clearQuantifiers (AllN (Suc i) φ) = clearQuantifiers (AllN i (AllQ φ))"
  by pat_completeness auto
termination
  apply(relation "measures [λA. depth' A]")
  by auto

subsection "Push Forall"

fun push_forall :: "atom fm ⇒ atom fm" where
  "push_forall TrueF = TrueF"|
  "push_forall FalseF = FalseF"|
  "push_forall (Atom a) = simp_atom a"|
  "push_forall (And φ ψ) = and (push_forall φ) (push_forall ψ)"|
  "push_forall (Or φ ψ) = or (push_forall φ) (push_forall ψ)"|
  "push_forall (ExQ φ) = ExQ (push_forall φ)"|
  "push_forall (ExN i φ) = ExN i (push_forall φ)"|
  "push_forall (Neg φ) = neg (push_forall φ)"|
  "push_forall (AllQ TrueF) = TrueF"|
  "push_forall (AllQ FalseF) = FalseF"|
  "push_forall (AllQ (Atom a)) = (if freeIn 0 (Atom a) then Atom(lowerAtom 0 1 a) else AllQ (Atom a))"|
  "push_forall (AllQ (And φ ψ)) = and (push_forall (AllQ φ)) (push_forall (AllQ ψ))"|
  "push_forall (AllQ (Or φ ψ)) = ( 
  if freeIn 0 φ  
  then(
    if freeIn 0 ψ
    then or (lowerFm 0 1 φ) (lowerFm 0 1 ψ)
    else or (lowerFm 0 1 φ) (AllQ ψ))
  else (
    if freeIn 0 ψ
    then or (AllQ φ) (lowerFm 0 1 ψ)
    else AllQ (or φ ψ))
)"|
  "push_forall (AllQ φ) = (if freeIn 0 φ then lowerFm 0 1 φ else AllQ φ)"|
  "push_forall (AllN i φ) = AllN i (push_forall  φ)" (* TODO, several bugs in this *)


subsection "Unpower"

fun to_list :: "nat ⇒ real mpoly ⇒ (real mpoly * nat) list" where
  "to_list v p = [(isolate_variable_sparse p v x, x). x ← [0..<(MPoly_Type.degree p v)+1]]"

fun chop :: "(real mpoly * nat) list ⇒ (real mpoly * nat) list"where
  "chop [] = []"|
  "chop ((p,i)#L) = (if p=0 then chop L else (p,i)#L)"

fun decreasePower :: "nat ⇒ real mpoly ⇒ real mpoly * nat"where
  "decreasePower v p = (case chop (to_list v p) of [] ⇒ (p,0) | ((p,i)#L) ⇒ (sum_list [term * (Var v) ^ (x-i). (term,x)←((p,i)#L)],i))"

fun unpower :: "nat ⇒ atom fm ⇒ atom fm" where
  "unpower v (Atom (Eq p)) = (case decreasePower v p of (_,0) ⇒ Atom(Eq p)| (p,_) ⇒ Or(Atom (Eq p))(Atom (Eq (Var v))) )"|
  "unpower v (Atom (Neq p)) = (case decreasePower v p of (_,0) ⇒ Atom(Neq p)| (p,_) ⇒ And(Atom (Neq p))(Atom (Neq (Var v))) )"|
  "unpower v (Atom (Less p)) = (case decreasePower v p of (_,0) ⇒ Atom(Less p)| (p,n) ⇒
  if n mod 2 = 0 then 
    And(Atom (Less p))(Atom(Neq (Var v)))
  else
    Or
      (And (Atom (Less ( p))) (Atom (Less (-Var v))))
      (And (Atom (Less (-p))) (Atom (Less (Var v))))
 )"|
  "unpower v (Atom (Leq p)) = (case decreasePower v p of (_,0) ⇒ Atom(Leq p)| (p,n) ⇒
  if n mod 2 = 0 then 
    Or (Atom (Leq p)) (Atom (Eq (Var v)))
  else
    Or (Atom (Eq p))
    (Or
      (And (Atom (Less ( p))) (Atom (Leq (-Var v))))
      (And (Atom (Less (-p))) (Atom (Leq (Var v)))))
 )"|
  "unpower v (And a b) = And (unpower v a) (unpower v b)"|
  "unpower v (Or a b) = Or (unpower v a) (unpower v b)"|
  "unpower v (Neg a) = Neg (unpower v a)"|
  "unpower v (TrueF) = TrueF"|
  "unpower v (FalseF) = FalseF"|
  "unpower v (AllQ F) = AllQ(unpower (v+1) F)"|
  "unpower v (ExQ F) = ExQ (unpower (v+1) F)"|
  "unpower v (AllN x F) = AllN x (unpower (v+x) F)"|
  "unpower v (ExN x F) = ExN x (unpower (v+x) F)"



end