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 r0 then TrueF else FalseF))"|
  "simp_atom (Neq p)  = (case get_if_const p of None  Atom(Neq  p) | Some(r)  (if r0 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