theory QElin_opt
imports QElin
begin
subsubsection{*An optimization*}
text{* Atoms are simplified asap. *}
definition
"asimp a = (case a of
Less r cs => (if ∀c∈ set cs. c = 0
then if r<0 then TrueF else FalseF
else Atom a) |
Eq r cs => (if ∀c∈ set cs. c = 0
then if r=0 then TrueF else FalseF else Atom a))"
lemma asimp_pretty:
"asimp (Less r cs) =
(if ∀c∈ set cs. c = 0
then if r<0 then TrueF else FalseF
else Atom(Less r cs))"
"asimp (Eq r cs) =
(if ∀c∈ set cs. c = 0
then if r=0 then TrueF else FalseF
else Atom(Eq r cs))"
by(auto simp:asimp_def)
definition qe_FMo1 :: "atom list => atom fm" where
"qe_FMo1 as = list_conj [asimp(combine p q). p\<leftarrow>lbounds as, q\<leftarrow>ubounds as]"
lemma I_asimp: "R.I (asimp a) xs = IR a xs"
by(simp add:asimp_def iprod0_if_coeffs0 split:atom.split)
lemma I_qe_FMo1: "R.I (qe_FMo1 as) xs = R.I (qe_FM1 as) xs"
by(simp add:qe_FM1_def qe_FMo1_def I_asimp)
definition "qe_FMo = Re.lift_dnfeq_qe qe_FMo1"
lemma qfree_qe_FMo1: "qfree (qe_FMo1 as)"
by(auto simp:qe_FM1_def qe_FMo1_def asimp_def intro!:qfree_list_conj
split:atom.split)
corollary I_qe_FMo: "R.I (qe_FMo φ) xs = R.I φ xs"
unfolding qe_FMo_def
apply(rule Re.I_lift_dnfeq_qe)
apply(rule qfree_qe_FMo1)
apply(rule allI)
apply(subst I_qe_FMo1)
apply(rule I_qe_FM1)
prefer 2 apply blast
apply(clarify)
apply(drule_tac x=a in bspec) apply simp
apply(simp add: dependsR_def split:atom.splits list.splits)
done
theorem qfree_qe_FMo: "qfree (qe_FMo f)"
by(simp add:qe_FMo_def Re.qfree_lift_dnfeq_qe qfree_qe_FMo1)
end