--- 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 \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> 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 \<Rightarrow> 'a \<Rightarrow> ('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 \<le> z \<Longrightarrow> meet x y \<le> meet x z"
-by(simp add:meet_leI2)
-
-lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
-by(simp add:le_joinI2)
+interpretation meet_join_lat:
+ lattice ["op \<le> \<Colon> 'a\<Colon>{meet_semilorder,join_semilorder} \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
+by unfold_locales
-lemma distrib_join_le: "join x (meet y z) \<le> 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) \<le> 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 \<or> a = d \<or> b = c \<or> b = d \<Longrightarrow> meet a b \<le> join c d"
-by (auto simp:meet_leI2 meet_leI1)
-
-lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?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
--- 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 \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
apply(blast intro:trans)
apply simp
done
-lemma less_eq_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
apply(blast intro:trans)
apply simp
done
-lemma less_eq_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
by(blast intro: inf_greatest)
-lemma less_eq_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
by(blast intro: trans)
-lemma less_eq_inf_conv [simp]:
+lemma le_inf_iff [simp]:
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
by blast
-lemmas below_inf_conv = less_eq_inf_conv
- -- {* a duplicate for backward compatibility *}
+lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
+apply rule
+ apply(simp add: antisym)
+apply(subgoal_tac "x \<sqinter> y \<sqsubseteq> y")
+ apply(simp)
+apply(simp (no_asm))
+done
end
@@ -68,28 +73,36 @@
lemmas antisym_intro[intro!] = antisym
-lemma less_eq_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
apply(blast intro:trans)
apply simp
done
-lemma less_eq_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
apply(blast intro:trans)
apply simp
done
-lemma less_eq_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
by(blast intro: sup_least)
-lemma less_eq_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
by(blast intro: trans)
-lemma above_sup_conv[simp]:
+lemma ge_sup_conv[simp]:
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
by blast
+lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
+apply rule
+ apply(simp add: antisym)
+apply(subgoal_tac "x \<sqsubseteq> x \<squnion> y")
+apply(simp)
+ apply(simp (no_asm))
+done
+
end
@@ -162,9 +175,18 @@
lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> 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 \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
+by blast
+
+lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
+by blast
+
+
+text{* If you have one of them, you have them all. *}
lemma distrib_imp1:
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
@@ -190,6 +212,10 @@
finally show ?thesis .
qed
+(* seems unused *)
+lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> 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