Theory Virtual_Substitution.DNFUni

subsection "Overall General VS Proofs"
theory DNFUni
  imports QE InfinitesimalsUni
begin

fun DNFUni :: "atomUni fmUni ⇒ atomUni list list" where
  "DNFUni (AtomUni a) = [[a]]"|
  "DNFUni (TrueFUni) = [[]]" |
  "DNFUni (FalseFUni) = []"|
  "DNFUni (AndUni A B) = [A' @ B'. A' ← DNFUni A, B' ← DNFUni B]"|
  "DNFUni (OrUni A B) = DNFUni A @ DNFUni B"

lemma eval_DNFUni : "evalUni F x = evalUni (list_disj_Uni(map (list_conj_Uni o (map AtomUni)) (DNFUni F))) x"
proof(induction F)
  case TrueFUni
  then show ?case by auto
next
  case FalseFUni
  then show ?case by auto
next
  case (AtomUni x)
  then show ?case by auto
next
  case (AndUni F1 F2)
  show ?case unfolding DNFUni.simps eval_list_disj_Uni evalUni.simps AndUni List.map_concat List.set_concat apply simp
    unfolding eval_list_conj_Uni_append
    by blast
next
  case (OrUni F1 F2)
  then show ?case  unfolding DNFUni.simps List.map_append eval_list_disj_Uni List.set_append evalUni.simps
    by blast
qed

fun elimVarUni_atom :: "atomUni list ⇒ atomUni ⇒ atomUni fmUni" where
  "elimVarUni_atom F (EqUni (a,b,c)) =
(OrUni
  (AndUni 
    (AndUni (AtomUni (EqUni (0,0,a))) (AtomUni (NeqUni (0,0,b))))
      (list_conj_Uni (map (linearSubstitutionUni b c) F)))
    (AndUni (AtomUni (NeqUni (0,0,a))) (AndUni (AtomUni(LeqUni (0,0,-(b^2)+4*a*c)))
      (OrUni 
        (list_conj_Uni (map (quadraticSubUni (-b) 1 (b^2-4*a*c) (2*a)) F))
        (list_conj_Uni (map (quadraticSubUni (-b) (-1) (b^2-4*a*c) (2*a)) F))
      )
    )
  )
)
" |
  "elimVarUni_atom F (LeqUni (a,b,c)) =
(OrUni
  (AndUni 
    (AndUni (AtomUni (EqUni (0,0,a))) (AtomUni (NeqUni (0,0,b))))
      (list_conj_Uni (map (linearSubstitutionUni b c) F)))
    (AndUni (AtomUni (NeqUni (0,0,a))) (AndUni (AtomUni(LeqUni (0,0,-(b^2)+4*a*c)))
      (OrUni 
        (list_conj_Uni (map (quadraticSubUni (-b) 1 (b^2-4*a*c) (2*a)) F))
        (list_conj_Uni (map (quadraticSubUni (-b) (-1) (b^2-4*a*c) (2*a)) F))
      )
    )
  )
)
" |
  "elimVarUni_atom F (LessUni (a,b,c)) =
(OrUni
  (AndUni 
    (AndUni (AtomUni (EqUni (0,0,a))) (AtomUni (NeqUni (0,0,b))))
      (list_conj_Uni (map (substInfinitesimalLinearUni b c) F)))
    (AndUni (AtomUni (NeqUni (0,0,a))) (AndUni (AtomUni(LeqUni (0,0,-(b^2)+4*a*c)))
      (OrUni 
        (list_conj_Uni (map(substInfinitesimalQuadraticUni (-b) 1 (b^2-4*a*c) (2*a)) F))
        (list_conj_Uni (map(substInfinitesimalQuadraticUni (-b) (-1) (b^2-4*a*c) (2*a)) F))
      )
    )
  )
)
"|
  "elimVarUni_atom F (NeqUni (a,b,c)) =
(OrUni
  (AndUni 
    (AndUni (AtomUni (EqUni (0,0,a))) (AtomUni (NeqUni (0,0,b))))
      (list_conj_Uni (map (substInfinitesimalLinearUni b c) F)))
    (AndUni (AtomUni (NeqUni (0,0,a))) (AndUni (AtomUni(LeqUni (0,0,-(b^2)+4*a*c)))
      (OrUni 
        (list_conj_Uni (map(substInfinitesimalQuadraticUni (-b) 1 (b^2-4*a*c) (2*a)) F))
        (list_conj_Uni (map(substInfinitesimalQuadraticUni (-b) (-1) (b^2-4*a*c) (2*a)) F))
      )
    )
  )
)
"




fun generalVS_DNF :: "atomUni list ⇒ atomUni fmUni" where
  "generalVS_DNF L  = list_disj_Uni (list_conj_Uni(map substNegInfinityUni L) # (map (λA. elimVarUni_atom L A) L))"



end