diff -r 4d4cde714500 -r 131dd2a27137 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Sat Dec 09 18:06:17 2006 +0100 +++ b/src/HOL/Lattices.thy Sun Dec 10 07:12:26 2006 +0100 @@ -3,7 +3,7 @@ Author: Tobias Nipkow *) -header {* Abstract lattices *} +header {* Lattices via Locales *} theory Lattices imports Orderings @@ -19,67 +19,154 @@ locale lower_semilattice = partial_order + fixes inf :: "'a \ 'a \ 'a" (infixl "\" 70) assumes inf_le1[simp]: "x \ y \ x" and inf_le2[simp]: "x \ y \ y" - and inf_least: "x \ y \ x \ z \ x \ y \ z" + and inf_greatest: "x \ y \ x \ z \ x \ y \ z" locale upper_semilattice = partial_order + fixes sup :: "'a \ 'a \ 'a" (infixl "\" 65) assumes sup_ge1[simp]: "x \ x \ y" and sup_ge2[simp]: "y \ x \ y" - and sup_greatest: "y \ x \ z \ x \ y \ z \ x" + and sup_least: "y \ x \ z \ x \ y \ z \ x" locale lattice = lower_semilattice + upper_semilattice -lemma (in lower_semilattice) inf_commute: "(x \ y) = (y \ x)" -by(blast intro: antisym inf_le1 inf_le2 inf_least) +subsubsection{* Intro and elim rules*} + +context lower_semilattice +begin -lemma (in upper_semilattice) sup_commute: "(x \ y) = (y \ x)" -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest) +lemmas antisym_intro[intro!] = antisym -lemma (in lower_semilattice) inf_assoc: "(x \ y) \ z = x \ (y \ z)" -by(blast intro: antisym inf_le1 inf_le2 inf_least trans del:refl) +lemma less_eq_infI1[intro]: "a \ x \ a \ b \ x" +apply(subgoal_tac "a \ b \ a") + apply(blast intro:trans) +apply simp +done -lemma (in upper_semilattice) sup_assoc: "(x \ y) \ z = x \ (y \ z)" -by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans del:refl) +lemma less_eq_infI2[intro]: "b \ x \ a \ b \ x" +apply(subgoal_tac "a \ b \ b") + apply(blast intro:trans) +apply simp +done + +lemma less_eq_infI[intro!]: "x \ a \ x \ b \ x \ a \ b" +by(blast intro: inf_greatest) -lemma (in lower_semilattice) inf_idem[simp]: "x \ x = x" -by(blast intro: antisym inf_le1 inf_le2 inf_least refl) +lemma less_eq_infE[elim!]: "x \ a \ b \ (x \ a \ x \ b \ P) \ P" +by(blast intro: trans) -lemma (in upper_semilattice) sup_idem[simp]: "x \ x = x" -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl) +lemma less_eq_inf_conv [simp]: + "x \ y \ z = (x \ y \ x \ z)" +by blast + +lemmas below_inf_conv = less_eq_inf_conv + -- {* a duplicate for backward compatibility *} -lemma (in lower_semilattice) inf_left_idem[simp]: "x \ (x \ y) = x \ y" -by (simp add: inf_assoc[symmetric]) +end + + +context upper_semilattice +begin -lemma (in upper_semilattice) sup_left_idem[simp]: "x \ (x \ y) = x \ y" -by (simp add: sup_assoc[symmetric]) +lemmas antisym_intro[intro!] = antisym -lemma (in lattice) inf_sup_absorb: "x \ (x \ y) = x" -by(blast intro: antisym inf_le1 inf_least sup_ge1) +lemma less_eq_supI1[intro]: "x \ a \ x \ a \ b" +apply(subgoal_tac "a \ a \ b") + apply(blast intro:trans) +apply simp +done -lemma (in lattice) sup_inf_absorb: "x \ (x \ y) = x" -by(blast intro: antisym sup_ge1 sup_greatest inf_le1) +lemma less_eq_supI2[intro]: "x \ b \ x \ a \ b" +apply(subgoal_tac "b \ a \ b") + apply(blast intro:trans) +apply simp +done + +lemma less_eq_supI[intro!]: "a \ x \ b \ x \ a \ b \ x" +by(blast intro: sup_least) -lemma (in lower_semilattice) inf_absorb: "x \ y \ x \ y = x" -by(blast intro: antisym inf_le1 inf_least refl) +lemma less_eq_supE[elim!]: "a \ b \ x \ (a \ x \ b \ x \ P) \ P" +by(blast intro: trans) -lemma (in upper_semilattice) sup_absorb: "x \ y \ x \ y = y" -by(blast intro: antisym sup_ge2 sup_greatest refl) +lemma above_sup_conv[simp]: + "x \ y \ z = (x \ z \ y \ z)" +by blast + +end + + +subsubsection{* Equational laws *} -lemma (in lower_semilattice) less_eq_inf_conv [simp]: - "x \ y \ z = (x \ y \ x \ z)" -by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans) +context lower_semilattice +begin + +lemma inf_commute: "(x \ y) = (y \ x)" +by blast + +lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)" +by blast + +lemma inf_idem[simp]: "x \ x = x" +by blast + +lemma inf_left_idem[simp]: "x \ (x \ y) = x \ y" +by blast + +lemma inf_absorb1: "x \ y \ x \ y = x" +by blast + +lemma inf_absorb2: "y \ x \ x \ y = y" +by blast + +lemma inf_left_commute: "x \ (y \ z) = y \ (x \ z)" +by blast + +lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem + +end + + +context upper_semilattice +begin -lemmas (in lower_semilattice) below_inf_conv = less_eq_inf_conv - -- {* a duplicate for backward compatibility *} +lemma sup_commute: "(x \ y) = (y \ x)" +by blast + +lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)" +by blast + +lemma sup_idem[simp]: "x \ x = x" +by blast + +lemma sup_left_idem[simp]: "x \ (x \ y) = x \ y" +by blast + +lemma sup_absorb1: "y \ x \ x \ y = x" +by blast + +lemma sup_absorb2: "x \ y \ x \ y = y" +by blast -lemma (in upper_semilattice) above_sup_conv[simp]: - "x \ y \ z = (x \ z \ y \ z)" -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans) +lemma sup_left_commute: "x \ (y \ z) = y \ (x \ z)" +by blast + +lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem + +end +context lattice +begin + +lemma inf_sup_absorb: "x \ (x \ y) = x" +by(blast intro: antisym inf_le1 inf_greatest sup_ge1) + +lemma sup_inf_absorb: "x \ (x \ y) = x" +by(blast intro: antisym sup_ge1 sup_least inf_le1) + +lemmas (in lattice) ACI = inf_ACI sup_ACI text{* Towards distributivity: if you have one of them, you have them all. *} -lemma (in lattice) distrib_imp1: +lemma distrib_imp1: assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- @@ -91,7 +178,7 @@ finally show ?thesis . qed -lemma (in lattice) distrib_imp2: +lemma distrib_imp2: assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- @@ -103,46 +190,7 @@ finally show ?thesis . qed -text{* A package of rewrite rules for deciding equivalence wrt ACI: *} - -lemma (in lower_semilattice) inf_left_commute: "x \ (y \ z) = y \ (x \ z)" -proof - - have "x \ (y \ z) = (y \ z) \ x" by (simp only: inf_commute) - also have "... = y \ (z \ x)" by (simp only: inf_assoc) - also have "z \ x = x \ z" by (simp only: inf_commute) - finally(back_subst) show ?thesis . -qed - -lemma (in upper_semilattice) sup_left_commute: "x \ (y \ z) = y \ (x \ z)" -proof - - have "x \ (y \ z) = (y \ z) \ x" by (simp only: sup_commute) - also have "... = y \ (z \ x)" by (simp only: sup_assoc) - also have "z \ x = x \ z" by (simp only: sup_commute) - finally(back_subst) show ?thesis . -qed - -lemma (in lower_semilattice) inf_left_idem: "x \ (x \ y) = x \ y" -proof - - have "x \ (x \ y) = (x \ x) \ y" by(simp only:inf_assoc) - also have "\ = x \ y" by(simp) - finally show ?thesis . -qed - -lemma (in upper_semilattice) sup_left_idem: "x \ (x \ y) = x \ y" -proof - - have "x \ (x \ y) = (x \ x) \ y" by(simp only:sup_assoc) - also have "\ = x \ y" by(simp) - finally show ?thesis . -qed - - -lemmas (in lower_semilattice) inf_ACI = - inf_commute inf_assoc inf_left_commute inf_left_idem - -lemmas (in upper_semilattice) sup_ACI = - sup_commute sup_assoc sup_left_commute sup_left_idem - -lemmas (in lattice) ACI = inf_ACI sup_ACI +end subsection{* Distributive lattices *} @@ -150,21 +198,26 @@ locale distrib_lattice = lattice + assumes sup_inf_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)" -lemma (in distrib_lattice) sup_inf_distrib2: +context distrib_lattice +begin + +lemma sup_inf_distrib2: "(y \ z) \ x = (y \ x) \ (z \ x)" by(simp add:ACI sup_inf_distrib1) -lemma (in distrib_lattice) inf_sup_distrib1: +lemma inf_sup_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)" by(rule distrib_imp2[OF sup_inf_distrib1]) -lemma (in distrib_lattice) inf_sup_distrib2: +lemma inf_sup_distrib2: "(y \ z) \ x = (y \ x) \ (z \ x)" by(simp add:ACI inf_sup_distrib1) -lemmas (in distrib_lattice) distrib = +lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 +end + subsection {* min/max on linear orders as special case of inf/sup *} @@ -178,6 +231,17 @@ apply (simp add: max_def linorder_not_le order_less_imp_le) unfolding min_def max_def by auto +text{* Now we have inherited antisymmetry as an intro-rule on all +linear orders. This is a problem because it applies to bool, which is +undesirable. *} + +declare + min_max.antisym_intro[rule del] + min_max.less_eq_infI[rule del] min_max.less_eq_supI[rule del] + min_max.less_eq_supE[rule del] min_max.less_eq_infE[rule del] + min_max.less_eq_supI1[rule del] min_max.less_eq_supI2[rule del] + min_max.less_eq_infI1[rule del] min_max.less_eq_infI2[rule del] + lemmas le_maxI1 = min_max.sup_ge1 lemmas le_maxI2 = min_max.sup_ge2 @@ -187,4 +251,29 @@ lemmas min_ac = min_max.inf_assoc min_max.inf_commute mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute] +text {* ML legacy bindings *} + +ML {* +val Least_def = thm "Least_def"; +val Least_equality = thm "Least_equality"; +val min_def = thm "min_def"; +val min_of_mono = thm "min_of_mono"; +val max_def = thm "max_def"; +val max_of_mono = thm "max_of_mono"; +val min_leastL = thm "min_leastL"; +val max_leastL = thm "max_leastL"; +val min_leastR = thm "min_leastR"; +val max_leastR = thm "max_leastR"; +val le_max_iff_disj = thm "le_max_iff_disj"; +val le_maxI1 = thm "le_maxI1"; +val le_maxI2 = thm "le_maxI2"; +val less_max_iff_disj = thm "less_max_iff_disj"; +val max_less_iff_conj = thm "max_less_iff_conj"; +val min_less_iff_conj = thm "min_less_iff_conj"; +val min_le_iff_disj = thm "min_le_iff_disj"; +val min_less_iff_disj = thm "min_less_iff_disj"; +val split_min = thm "split_min"; +val split_max = thm "split_max"; +*} + end