# HG changeset patch # User nipkow # Date 1165752883 -3600 # Node ID 283461c15fa70fefdfa3a427efa1159a56b960fc # Parent 131dd2a271370ffc34dc7d0ee6c0c2ac5dfcc953 renaming diff -r 131dd2a27137 -r 283461c15fa7 src/HOL/LOrder.thy --- a/src/HOL/LOrder.thy Sun Dec 10 07:12:26 2006 +0100 +++ b/src/HOL/LOrder.thy Sun Dec 10 13:14:43 2006 +0100 @@ -1,6 +1,11 @@ (* Title: HOL/LOrder.thy ID: $Id$ Author: Steven Obua, TU Muenchen + +FIXME integrate properly with lattice locales +- make it a class? +- get rid of the implicit there-is-a-meet/join but require eplicit ops. +Also rename meet/join to inf/sup. *) header "Lattice Orders" @@ -114,7 +119,7 @@ declare join_semilat.antisym_intro[rule del] meet_semilat.antisym_intro[rule del] - join_semilat.less_eq_supE[rule del] meet_semilat.less_eq_infE[rule del] + join_semilat.le_supE[rule del] meet_semilat.le_infE[rule del] interpretation meet_join_lat: lattice ["op \ \ 'a\lorder \ 'a \ bool" "op <" meet join] @@ -122,17 +127,17 @@ lemmas meet_left_le = meet_semilat.inf_le1 lemmas meet_right_le = meet_semilat.inf_le2 -lemmas le_meetI[rule del] = meet_semilat.less_eq_infI +lemmas le_meetI[rule del] = meet_semilat.le_infI (* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *) lemmas join_left_le = join_semilat.sup_ge1 lemmas join_right_le = join_semilat.sup_ge2 -lemmas join_leI[rule del] = join_semilat.less_eq_supI +lemmas join_leI[rule del] = join_semilat.le_supI lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le -lemmas le_meet = meet_semilat.less_eq_inf_conv +lemmas le_meet = meet_semilat.le_inf_iff -lemmas le_join = join_semilat.above_sup_conv +lemmas le_join = join_semilat.ge_sup_conv lemma is_meet_min: "is_meet (min::'a \ 'a \ ('a::linorder))" by (auto simp add: is_meet_def min_def) @@ -162,10 +167,10 @@ lemmas join_idempotent = join_semilat.sup_idem lemmas meet_comm = meet_semilat.inf_commute lemmas join_comm = join_semilat.sup_commute -lemmas meet_leI1[rule del] = meet_semilat.less_eq_infI1 -lemmas meet_leI2[rule del] = meet_semilat.less_eq_infI2 -lemmas le_joinI1[rule del] = join_semilat.less_eq_supI1 -lemmas le_joinI2[rule del] = join_semilat.less_eq_supI2 +lemmas meet_leI1[rule del] = meet_semilat.le_infI1 +lemmas meet_leI2[rule del] = meet_semilat.le_infI2 +lemmas le_joinI1[rule del] = join_semilat.le_supI1 +lemmas le_joinI2[rule del] = join_semilat.le_supI2 lemmas meet_assoc = meet_semilat.inf_assoc lemmas join_assoc = join_semilat.sup_assoc lemmas meet_left_comm = meet_semilat.inf_left_commute @@ -176,21 +181,8 @@ lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent -lemma le_def_meet: "(x <= y) = (meet x y = x)" -apply rule -apply(simp add: order_antisym) -apply(subgoal_tac "meet x y <= y") -apply(simp) -apply(simp (no_asm)) -done - -lemma le_def_join: "(x <= y) = (join x y = y)" -apply rule -apply(simp add: order_antisym) -apply(subgoal_tac "x <= join x y") -apply(simp) -apply(simp (no_asm)) -done +lemmas le_def_meet = meet_semilat.le_iff_inf +lemmas le_def_join = join_semilat.le_iff_sup lemmas join_absorp2 = join_semilat.sup_absorb2 lemmas join_absorp1 = join_semilat.sup_absorb1 @@ -198,41 +190,14 @@ lemmas meet_absorp1 = meet_semilat.inf_absorb1 lemmas meet_absorp2 = meet_semilat.inf_absorb2 -lemma meet_join_absorp: "meet x (join x y) = x" -by(simp add:meet_absorp1) - -lemma join_meet_absorp: "join x (meet x y) = x" -by(simp add:join_absorp1) - -lemma meet_mono: "y \ z \ meet x y \ meet x z" -by(simp add:meet_leI2) - -lemma join_mono: "y \ z \ join x y \ join x z" -by(simp add:le_joinI2) +interpretation meet_join_lat: + lattice ["op \ \ 'a\{meet_semilorder,join_semilorder} \ 'a \ bool" "op <" meet join] +by unfold_locales -lemma distrib_join_le: "join x (meet y z) \ meet (join x y) (join x z)" (is "_ <= ?r") -proof - - have a: "x <= ?r" by (simp_all add:le_meetI) - have b: "meet y z <= ?r" by (simp add:le_joinI2) - from a b show ?thesis by (simp add: join_leI) -qed - -lemma distrib_meet_le: "join (meet x y) (meet x z) \ meet x (join y z)" (is "?l <= _") -proof - - have a: "?l <= x" by (simp_all add: join_leI) - have b: "?l <= join y z" by (simp add:meet_leI2) - from a b show ?thesis by (simp add: le_meetI) -qed +lemmas meet_join_absorp = meet_join_lat.inf_sup_absorb +lemmas join_meet_absorp = meet_join_lat.sup_inf_absorb -lemma meet_join_eq_imp_le: "a = c \ a = d \ b = c \ b = d \ meet a b \ join c d" -by (auto simp:meet_leI2 meet_leI1) - -lemma modular_le: "x \ z \ join x (meet y z) \ meet (join x y) z" (is "_ \ ?t <= _") -proof - - assume a: "x <= z" - have b: "?t <= join x y" by (simp_all add: join_leI meet_join_eq_imp_le ) - have c: "?t <= z" by (simp_all add: a join_leI) - from b c show ?thesis by (simp add: le_meetI) -qed +lemmas distrib_join_le = meet_join_lat.distrib_sup_le +lemmas distrib_meet_le = meet_join_lat.distrib_inf_le end diff -r 131dd2a27137 -r 283461c15fa7 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Sun Dec 10 07:12:26 2006 +0100 +++ b/src/HOL/Lattices.thy Sun Dec 10 13:14:43 2006 +0100 @@ -35,30 +35,35 @@ lemmas antisym_intro[intro!] = antisym -lemma less_eq_infI1[intro]: "a \ x \ a \ b \ x" +lemma le_infI1[intro]: "a \ x \ a \ b \ x" apply(subgoal_tac "a \ b \ a") apply(blast intro:trans) apply simp done -lemma less_eq_infI2[intro]: "b \ x \ a \ b \ x" +lemma le_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" +lemma le_infI[intro!]: "x \ a \ x \ b \ x \ a \ b" by(blast intro: inf_greatest) -lemma less_eq_infE[elim!]: "x \ a \ b \ (x \ a \ x \ b \ P) \ P" +lemma le_infE[elim!]: "x \ a \ b \ (x \ a \ x \ b \ P) \ P" by(blast intro: trans) -lemma less_eq_inf_conv [simp]: +lemma le_inf_iff [simp]: "x \ y \ z = (x \ y \ x \ z)" by blast -lemmas below_inf_conv = less_eq_inf_conv - -- {* a duplicate for backward compatibility *} +lemma le_iff_inf: "(x \ y) = (x \ y = x)" +apply rule + apply(simp add: antisym) +apply(subgoal_tac "x \ y \ y") + apply(simp) +apply(simp (no_asm)) +done end @@ -68,28 +73,36 @@ lemmas antisym_intro[intro!] = antisym -lemma less_eq_supI1[intro]: "x \ a \ x \ a \ b" +lemma le_supI1[intro]: "x \ a \ x \ a \ b" apply(subgoal_tac "a \ a \ b") apply(blast intro:trans) apply simp done -lemma less_eq_supI2[intro]: "x \ b \ x \ a \ b" +lemma le_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" +lemma le_supI[intro!]: "a \ x \ b \ x \ a \ b \ x" by(blast intro: sup_least) -lemma less_eq_supE[elim!]: "a \ b \ x \ (a \ x \ b \ x \ P) \ P" +lemma le_supE[elim!]: "a \ b \ x \ (a \ x \ b \ x \ P) \ P" by(blast intro: trans) -lemma above_sup_conv[simp]: +lemma ge_sup_conv[simp]: "x \ y \ z = (x \ z \ y \ z)" by blast +lemma le_iff_sup: "(x \ y) = (x \ y = y)" +apply rule + apply(simp add: antisym) +apply(subgoal_tac "x \ x \ y") +apply(simp) + apply(simp (no_asm)) +done + end @@ -162,9 +175,18 @@ 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 +lemmas ACI = inf_ACI sup_ACI + +text{* Towards distributivity *} -text{* Towards distributivity: if you have one of them, you have them all. *} +lemma distrib_sup_le: "x \ (y \ z) \ (x \ y) \ (x \ z)" +by blast + +lemma distrib_inf_le: "(x \ y) \ (x \ z) \ x \ (y \ z)" +by blast + + +text{* If you have one of them, you have them all. *} lemma distrib_imp1: assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" @@ -190,6 +212,10 @@ finally show ?thesis . qed +(* seems unused *) +lemma modular_le: "x \ z \ x \ (y \ z) \ (x \ y) \ z" +by blast + end @@ -237,10 +263,10 @@ 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] + min_max.le_infI[rule del] min_max.le_supI[rule del] + min_max.le_supE[rule del] min_max.le_infE[rule del] + min_max.le_supI1[rule del] min_max.le_supI2[rule del] + min_max.le_infI1[rule del] min_max.le_infI2[rule del] lemmas le_maxI1 = min_max.sup_ge1 lemmas le_maxI2 = min_max.sup_ge2