renaming
authornipkow
Sun Dec 10 13:14:43 2006 +0100 (2006-12-10)
changeset 21734283461c15fa7
parent 21733 131dd2a27137
child 21735 0c65e072f4be
renaming
src/HOL/LOrder.thy
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/LOrder.thy	Sun Dec 10 07:12:26 2006 +0100
     1.2 +++ b/src/HOL/LOrder.thy	Sun Dec 10 13:14:43 2006 +0100
     1.3 @@ -1,6 +1,11 @@
     1.4  (*  Title:   HOL/LOrder.thy
     1.5      ID:      $Id$
     1.6      Author:  Steven Obua, TU Muenchen
     1.7 +
     1.8 +FIXME integrate properly with lattice locales
     1.9 +- make it a class?
    1.10 +- get rid of the implicit there-is-a-meet/join but require eplicit ops.
    1.11 +Also rename meet/join to inf/sup. 
    1.12  *)
    1.13  
    1.14  header "Lattice Orders"
    1.15 @@ -114,7 +119,7 @@
    1.16  
    1.17  declare
    1.18   join_semilat.antisym_intro[rule del] meet_semilat.antisym_intro[rule del]
    1.19 - join_semilat.less_eq_supE[rule del] meet_semilat.less_eq_infE[rule del]
    1.20 + join_semilat.le_supE[rule del] meet_semilat.le_infE[rule del]
    1.21  
    1.22  interpretation meet_join_lat:
    1.23    lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
    1.24 @@ -122,17 +127,17 @@
    1.25  
    1.26  lemmas meet_left_le = meet_semilat.inf_le1
    1.27  lemmas meet_right_le = meet_semilat.inf_le2
    1.28 -lemmas le_meetI[rule del] = meet_semilat.less_eq_infI
    1.29 +lemmas le_meetI[rule del] = meet_semilat.le_infI
    1.30  (* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
    1.31  lemmas join_left_le = join_semilat.sup_ge1
    1.32  lemmas join_right_le = join_semilat.sup_ge2
    1.33 -lemmas join_leI[rule del] = join_semilat.less_eq_supI
    1.34 +lemmas join_leI[rule del] = join_semilat.le_supI
    1.35  
    1.36  lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
    1.37  
    1.38 -lemmas le_meet = meet_semilat.less_eq_inf_conv
    1.39 +lemmas le_meet = meet_semilat.le_inf_iff
    1.40  
    1.41 -lemmas le_join = join_semilat.above_sup_conv
    1.42 +lemmas le_join = join_semilat.ge_sup_conv
    1.43  
    1.44  lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
    1.45  by (auto simp add: is_meet_def min_def)
    1.46 @@ -162,10 +167,10 @@
    1.47  lemmas join_idempotent = join_semilat.sup_idem
    1.48  lemmas meet_comm = meet_semilat.inf_commute
    1.49  lemmas join_comm = join_semilat.sup_commute
    1.50 -lemmas meet_leI1[rule del] = meet_semilat.less_eq_infI1
    1.51 -lemmas meet_leI2[rule del] = meet_semilat.less_eq_infI2
    1.52 -lemmas le_joinI1[rule del] = join_semilat.less_eq_supI1
    1.53 -lemmas le_joinI2[rule del] = join_semilat.less_eq_supI2
    1.54 +lemmas meet_leI1[rule del] = meet_semilat.le_infI1
    1.55 +lemmas meet_leI2[rule del] = meet_semilat.le_infI2
    1.56 +lemmas le_joinI1[rule del] = join_semilat.le_supI1
    1.57 +lemmas le_joinI2[rule del] = join_semilat.le_supI2
    1.58  lemmas meet_assoc = meet_semilat.inf_assoc
    1.59  lemmas join_assoc = join_semilat.sup_assoc
    1.60  lemmas meet_left_comm = meet_semilat.inf_left_commute
    1.61 @@ -176,21 +181,8 @@
    1.62  lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
    1.63  lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
    1.64  
    1.65 -lemma le_def_meet: "(x <= y) = (meet x y = x)"
    1.66 -apply rule
    1.67 -apply(simp add: order_antisym)
    1.68 -apply(subgoal_tac "meet x y <= y")
    1.69 -apply(simp)
    1.70 -apply(simp (no_asm))
    1.71 -done
    1.72 -
    1.73 -lemma le_def_join: "(x <= y) = (join x y = y)"
    1.74 -apply rule
    1.75 -apply(simp add: order_antisym)
    1.76 -apply(subgoal_tac "x <= join x y")
    1.77 -apply(simp)
    1.78 -apply(simp (no_asm))
    1.79 -done
    1.80 +lemmas le_def_meet = meet_semilat.le_iff_inf
    1.81 +lemmas le_def_join = join_semilat.le_iff_sup
    1.82  
    1.83  lemmas join_absorp2 = join_semilat.sup_absorb2
    1.84  lemmas join_absorp1 = join_semilat.sup_absorb1
    1.85 @@ -198,41 +190,14 @@
    1.86  lemmas meet_absorp1 = meet_semilat.inf_absorb1
    1.87  lemmas meet_absorp2 = meet_semilat.inf_absorb2
    1.88  
    1.89 -lemma meet_join_absorp: "meet x (join x y) = x"
    1.90 -by(simp add:meet_absorp1)
    1.91 -
    1.92 -lemma join_meet_absorp: "join x (meet x y) = x"
    1.93 -by(simp add:join_absorp1)
    1.94 -
    1.95 -lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
    1.96 -by(simp add:meet_leI2)
    1.97 -
    1.98 -lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
    1.99 -by(simp add:le_joinI2)
   1.100 +interpretation meet_join_lat:
   1.101 +  lattice ["op \<le> \<Colon> 'a\<Colon>{meet_semilorder,join_semilorder} \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
   1.102 +by unfold_locales
   1.103  
   1.104 -lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
   1.105 -proof -
   1.106 -  have a: "x <= ?r" by (simp_all add:le_meetI)
   1.107 -  have b: "meet y z <= ?r" by (simp add:le_joinI2)
   1.108 -  from a b show ?thesis by (simp add: join_leI)
   1.109 -qed
   1.110 -  
   1.111 -lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
   1.112 -proof -
   1.113 -  have a: "?l <= x" by (simp_all add: join_leI)
   1.114 -  have b: "?l <= join y z" by (simp add:meet_leI2)
   1.115 -  from a b show ?thesis by (simp add: le_meetI)
   1.116 -qed
   1.117 +lemmas meet_join_absorp = meet_join_lat.inf_sup_absorb
   1.118 +lemmas join_meet_absorp = meet_join_lat.sup_inf_absorb
   1.119  
   1.120 -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"
   1.121 -by (auto simp:meet_leI2 meet_leI1)
   1.122 -
   1.123 -lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
   1.124 -proof -
   1.125 -  assume a: "x <= z"
   1.126 -  have b: "?t <= join x y" by (simp_all add: join_leI meet_join_eq_imp_le )
   1.127 -  have c: "?t <= z" by (simp_all add: a join_leI)
   1.128 -  from b c show ?thesis by (simp add: le_meetI)
   1.129 -qed
   1.130 +lemmas distrib_join_le = meet_join_lat.distrib_sup_le
   1.131 +lemmas distrib_meet_le = meet_join_lat.distrib_inf_le
   1.132  
   1.133  end
     2.1 --- a/src/HOL/Lattices.thy	Sun Dec 10 07:12:26 2006 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Sun Dec 10 13:14:43 2006 +0100
     2.3 @@ -35,30 +35,35 @@
     2.4  
     2.5  lemmas antisym_intro[intro!] = antisym
     2.6  
     2.7 -lemma less_eq_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
     2.8 +lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
     2.9  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
    2.10   apply(blast intro:trans)
    2.11  apply simp
    2.12  done
    2.13  
    2.14 -lemma less_eq_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    2.15 +lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    2.16  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    2.17   apply(blast intro:trans)
    2.18  apply simp
    2.19  done
    2.20  
    2.21 -lemma less_eq_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    2.22 +lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    2.23  by(blast intro: inf_greatest)
    2.24  
    2.25 -lemma less_eq_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    2.26 +lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    2.27  by(blast intro: trans)
    2.28  
    2.29 -lemma less_eq_inf_conv [simp]:
    2.30 +lemma le_inf_iff [simp]:
    2.31   "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    2.32  by blast
    2.33  
    2.34 -lemmas below_inf_conv = less_eq_inf_conv
    2.35 -  -- {* a duplicate for backward compatibility *}
    2.36 +lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
    2.37 +apply rule
    2.38 + apply(simp add: antisym)
    2.39 +apply(subgoal_tac "x \<sqinter> y \<sqsubseteq> y")
    2.40 + apply(simp)
    2.41 +apply(simp (no_asm))
    2.42 +done
    2.43  
    2.44  end
    2.45  
    2.46 @@ -68,28 +73,36 @@
    2.47  
    2.48  lemmas antisym_intro[intro!] = antisym
    2.49  
    2.50 -lemma less_eq_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    2.51 +lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    2.52  apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    2.53   apply(blast intro:trans)
    2.54  apply simp
    2.55  done
    2.56  
    2.57 -lemma less_eq_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    2.58 +lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    2.59  apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    2.60   apply(blast intro:trans)
    2.61  apply simp
    2.62  done
    2.63  
    2.64 -lemma less_eq_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    2.65 +lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    2.66  by(blast intro: sup_least)
    2.67  
    2.68 -lemma less_eq_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    2.69 +lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    2.70  by(blast intro: trans)
    2.71  
    2.72 -lemma above_sup_conv[simp]:
    2.73 +lemma ge_sup_conv[simp]:
    2.74   "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    2.75  by blast
    2.76  
    2.77 +lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
    2.78 +apply rule
    2.79 + apply(simp add: antisym)
    2.80 +apply(subgoal_tac "x \<sqsubseteq> x \<squnion> y")
    2.81 +apply(simp)
    2.82 + apply(simp (no_asm))
    2.83 +done
    2.84 +
    2.85  end
    2.86  
    2.87  
    2.88 @@ -162,9 +175,18 @@
    2.89  lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
    2.90  by(blast intro: antisym sup_ge1 sup_least inf_le1)
    2.91  
    2.92 -lemmas (in lattice) ACI = inf_ACI sup_ACI
    2.93 +lemmas ACI = inf_ACI sup_ACI
    2.94 +
    2.95 +text{* Towards distributivity *}
    2.96  
    2.97 -text{* Towards distributivity: if you have one of them, you have them all. *}
    2.98 +lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    2.99 +by blast
   2.100 +
   2.101 +lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   2.102 +by blast
   2.103 +
   2.104 +
   2.105 +text{* If you have one of them, you have them all. *}
   2.106  
   2.107  lemma distrib_imp1:
   2.108  assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   2.109 @@ -190,6 +212,10 @@
   2.110    finally show ?thesis .
   2.111  qed
   2.112  
   2.113 +(* seems unused *)
   2.114 +lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
   2.115 +by blast
   2.116 +
   2.117  end
   2.118  
   2.119  
   2.120 @@ -237,10 +263,10 @@
   2.121  
   2.122  declare
   2.123   min_max.antisym_intro[rule del]
   2.124 - min_max.less_eq_infI[rule del] min_max.less_eq_supI[rule del]
   2.125 - min_max.less_eq_supE[rule del] min_max.less_eq_infE[rule del]
   2.126 - min_max.less_eq_supI1[rule del] min_max.less_eq_supI2[rule del]
   2.127 - min_max.less_eq_infI1[rule del] min_max.less_eq_infI2[rule del]
   2.128 + min_max.le_infI[rule del] min_max.le_supI[rule del]
   2.129 + min_max.le_supE[rule del] min_max.le_infE[rule del]
   2.130 + min_max.le_supI1[rule del] min_max.le_supI2[rule del]
   2.131 + min_max.le_infI1[rule del] min_max.le_infI2[rule del]
   2.132  
   2.133  lemmas le_maxI1 = min_max.sup_ge1
   2.134  lemmas le_maxI2 = min_max.sup_ge2