# Theory DLO

Up to index of Isabelle/HOL/LinearQuantifierElim

theory DLO
imports QE Complex_Main
`(*  Author:     Tobias Nipkow, 2007  *)header "DLO"theory DLOimports QE Complex_Mainbeginsubsection "Basics"class dlo = linorder +assumes dense: "x < z ==> ∃y. x < y ∧ y < z"and no_ub: "∃u. x < u" and no_lb: "∃l. l < x"instance real :: dloproof  fix r s :: real  let ?v = "(r + s) / 2"  assume "r < s"  hence "r < ?v ∧ ?v < s" by simp  thus "∃v. r < v ∧ v < s" ..next  fix r :: real  have "r < r + 1" by arith  thus "∃s. r < s" ..next  fix r :: real  have "r - 1 < r" by arith  thus "∃s. s < r" ..qeddatatype atom = Less nat nat | Eq nat natfun is_Less :: "atom => bool" where"is_Less (Less i j) = True" |"is_Less f = False"abbreviation "is_Eq ≡ Not o is_Less"lemma is_Less_iff: "is_Less a = (∃i j. a = Less i j)"by(cases a) autolemma is_Eq_iff: "(∀i j. a ≠ Less i j) = (∃i j. a = Eq i j)"by(cases a) autolemma not_is_Eq_iff: "(∀i j. a ≠ Eq i j) = (∃i j. a = Less i j)"by(cases a) autofun neg⇣d⇣l⇣o :: "atom => atom fm" where"neg⇣d⇣l⇣o (Less i j) = Or (Atom(Less j i)) (Atom(Eq i j))" |"neg⇣d⇣l⇣o (Eq i j) = Or (Atom(Less i j)) (Atom(Less j i))"fun I⇣d⇣l⇣o :: "atom => 'a::dlo list => bool" where"I⇣d⇣l⇣o (Eq i j) xs = (xs!i = xs!j)" |"I⇣d⇣l⇣o (Less i j) xs = (xs!i < xs!j)"fun depends⇣d⇣l⇣o :: "atom => bool" where"depends⇣d⇣l⇣o(Eq i j) = (i=0 | j=0)" |"depends⇣d⇣l⇣o(Less i j) = (i=0 | j=0)"fun decr⇣d⇣l⇣o :: "atom => atom" where"decr⇣d⇣l⇣o (Less i j) = Less (i - 1) (j - 1)" |"decr⇣d⇣l⇣o (Eq i j) = Eq (i - 1) (j - 1)"(* needed for code generation *)definition [code del]: "nnf = ATOM.nnf neg⇣d⇣l⇣o"definition [code del]: "qelim = ATOM.qelim depends⇣d⇣l⇣o decr⇣d⇣l⇣o"definition [code del]: "lift_dnf_qe = ATOM.lift_dnf_qe neg⇣d⇣l⇣o depends⇣d⇣l⇣o decr⇣d⇣l⇣o"definition [code del]: "lift_nnf_qe = ATOM.lift_nnf_qe neg⇣d⇣l⇣o"hide_const nnf qelim lift_dnf_qe lift_nnf_qelemmas DLO_code_lemmas = nnf_def qelim_def lift_dnf_qe_def lift_nnf_qe_definterpretation DLO!:  ATOM neg⇣d⇣l⇣o "(λa. True)" I⇣d⇣l⇣o depends⇣d⇣l⇣o decr⇣d⇣l⇣oapply(unfold_locales)apply(case_tac a)apply simp_allapply(case_tac a)apply (simp_all add:linorder_class.not_less_iff_gr_or_eq                    linorder_not_less linorder_neq_iff)apply(case_tac a)apply(simp_all add:nth_Cons')donelemmas [folded DLO_code_lemmas, code] =  DLO.nnf.simps DLO.qelim_def DLO.lift_dnf_qe.simps DLO.lift_dnf_qe.simpssetup {* Sign.revert_abbrev "" @{const_abbrev DLO.I} *}definition lbounds where "lbounds as = [i. Less (Suc i) 0 \<leftarrow> as]"definition ubounds where "ubounds as = [i. Less 0 (Suc i) \<leftarrow> as]"definition ebounds where "ebounds as = [i. Eq (Suc i) 0 \<leftarrow> as] @ [i. Eq 0 (Suc i) \<leftarrow> as]"lemma set_lbounds: "set(lbounds as) = {i. Less (Suc i) 0 : set as}"by(auto simp: lbounds_def split:nat.splits atom.splits)lemma set_ubounds: "set(ubounds as) = {i. Less 0 (Suc i) : set as}"by(auto simp: ubounds_def split:nat.splits atom.splits)lemma set_ebounds:  "set(ebounds as) = {k. Eq (Suc k) 0 : set as ∨ Eq 0 (Suc k) : set as}"by(auto simp: ebounds_def split: atom.splits nat.splits)abbreviation "LB f xs ≡ {xs!i|i. Less (Suc i) 0 : set(DLO.atoms⇣0 f)}"abbreviation "UB f xs ≡ {xs!i|i. Less 0 (Suc i) : set(DLO.atoms⇣0 f)}"definition "EQ f xs = {xs!k|k.  Eq (Suc k) 0 : set(DLO.atoms⇣0 f) ∨ Eq 0 (Suc k) : set(DLO.atoms⇣0 f)}"lemma EQ_And[simp]: "EQ (And f g) xs = (EQ f xs Un EQ g xs)"by(auto simp:EQ_def)lemma EQ_Or[simp]: "EQ (Or f g) xs = (EQ f xs Un EQ g xs)"by(auto simp:EQ_def)lemma EQ_conv_set_ebounds:  "x ∈ EQ f xs = (∃e∈set(ebounds(DLO.atoms⇣0 f)). x = xs!e)"by(auto simp: EQ_def set_ebounds)fun isubst where "isubst k 0 = k" | "isubst k (Suc i) = i"fun asubst :: "nat => atom => atom" where"asubst k (Less i j) = Less (isubst k i) (isubst k j)"|"asubst k (Eq i j) = Eq (isubst k i) (isubst k j)"abbreviation "subst φ k ≡ map⇘fm⇙ (asubst k) φ"lemma I_subst: "qfree f ==> DLO.I (subst f k) xs = DLO.I f (xs!k # xs)"apply(induct f)apply(simp_all)apply(case_tac a)apply(simp_all add:nth.simps split:nat.splits)donefun amin_inf :: "atom => atom fm" where"amin_inf (Less _ 0) = FalseF" |"amin_inf (Less 0 _) = TrueF" |"amin_inf (Less (Suc i) (Suc j)) = Atom(Less i j)" |"amin_inf (Eq 0 0) = TrueF" |"amin_inf (Eq 0 _) = FalseF" |"amin_inf (Eq _ 0) = FalseF" |"amin_inf (Eq (Suc i) (Suc j)) = Atom(Eq i j)"abbreviation min_inf :: "atom fm => atom fm" ("inf⇣-") where"inf⇣- ≡ amap⇘fm⇙ amin_inf"fun aplus_inf :: "atom => atom fm" where"aplus_inf (Less 0 _) = FalseF" |"aplus_inf (Less _ 0) = TrueF" |"aplus_inf (Less (Suc i) (Suc j)) = Atom(Less i j)" |"aplus_inf (Eq 0 0) = TrueF" |"aplus_inf (Eq 0 _) = FalseF" |"aplus_inf (Eq _ 0) = FalseF" |"aplus_inf (Eq (Suc i) (Suc j)) = Atom(Eq i j)"abbreviation plus_inf :: "atom fm => atom fm" ("inf⇣+") where"inf⇣+ ≡ amap⇘fm⇙ aplus_inf"lemma min_inf:  "nqfree f ==> ∃x. ∀y≤x. DLO.I (inf⇣- f) xs = DLO.I f (y # xs)"  (is "_ ==> ∃x. ?P f x")proof(induct f)  case (Atom a)  show ?case  proof (cases a rule: amin_inf.cases)    case 1 thus ?thesis by(auto simp add:nth_Cons' linorder_not_less)  next    case 2 thus ?thesis      by (simp) (metis no_lb linorder_not_less order_less_le_trans)  next    case 5 thus ?thesis      by(simp add:nth_Cons') (metis no_lb linorder_not_less)  next    case 6 thus ?thesis by simp (metis no_lb linorder_not_less)  qed simp_allnext  case (And f1 f2)  then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+  hence "?P (And f1 f2) (min x1 x2)" by(force simp:and_def)  thus ?case ..next  case (Or f1 f2)  then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+  hence "?P (Or f1 f2) (min x1 x2)" by(force simp:or_def)  thus ?case ..qed simp_alllemma plus_inf:  "nqfree f ==> ∃x.∀y≥x. DLO.I (inf⇣+ f) xs = DLO.I f (y # xs)"  (is "_ ==> ∃x. ?P f x")proof (induct f)  have dlo_bound: "!!z::'a. ∃x. ∀y≥x. y > z"  proof -    fix z    from no_ub obtain w :: 'a where "w > z" ..    then have "∀y≥w. y > z" by auto    then show "?thesis z" ..  qed  case (Atom a)  show ?case  proof (cases a rule: aplus_inf.cases)    case 1 thus ?thesis      by (simp add: nth_Cons') (metis linorder_not_less)  next    case 2 thus ?thesis by (auto intro: dlo_bound)  next    case 5 thus ?thesis       by simp (metis dlo_bound less_imp_neq)  next    case 6 thus ?thesis      by simp (metis dlo_bound less_imp_neq)  qed simp_allnext  case (And f1 f2)  then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+  hence "?P (And f1 f2) (max x1 x2)" by(force simp:and_def)  thus ?case ..next  case (Or f1 f2)  then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+  hence "?P (Or f1 f2) (max x1 x2)" by(force simp:or_def)  thus ?case ..qed simp_alldeclare[[simp_depth_limit=2]]lemma LBex: "[| nqfree f; DLO.I f (x#xs); ¬DLO.I (inf⇣- f) xs; x ∉ EQ f xs |]  ==> ∃l∈ LB f xs. l < x"proof(induct f)  case (Atom a) thus ?case    by (cases a rule: amin_inf.cases)       (simp_all add: nth.simps EQ_def split: nat.splits)qed autolemma UBex: "[| nqfree f; DLO.I f (x#xs); ¬DLO.I (inf⇣+ f) xs; x ∉ EQ f xs |]  ==> ∃u ∈ UB f xs. x < u"proof(induct f)  case (Atom a) thus ?case    by (cases a rule: aplus_inf.cases)       (simp_all add: nth.simps EQ_def split: nat.splits)qed autodeclare[[simp_depth_limit=50]]lemma finite_LB: "finite(LB f xs)"proof -  have "LB f xs = (λk. xs!k) ` set(lbounds(DLO.atoms⇣0 f))"    by (auto simp:set_lbounds image_def)  thus ?thesis by simpqedlemma finite_UB: "finite(UB f xs)"proof -  have "UB f xs = (λk.  xs!k) ` set(ubounds(DLO.atoms⇣0 f))"    by (auto simp:set_ubounds image_def)  thus ?thesis by simpqedlemma qfree_amin_inf: "qfree (amin_inf a)"by(cases a rule:amin_inf.cases) simp_alllemma qfree_min_inf: "nqfree φ ==> qfree(inf⇣- φ)"by(induct φ)(simp_all add:qfree_amin_inf)lemma qfree_aplus_inf: "qfree (aplus_inf a)"by(cases a rule:aplus_inf.cases) simp_alllemma qfree_plus_inf: "nqfree φ ==> qfree(inf⇣+ φ)"by(induct φ)(simp_all add:qfree_aplus_inf)end`