src/HOL/Lattices.thy
changeset 21734 283461c15fa7
parent 21733 131dd2a27137
child 22068 00bed5ac9884
     1.1 --- a/src/HOL/Lattices.thy	Sun Dec 10 07:12:26 2006 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sun Dec 10 13:14:43 2006 +0100
     1.3 @@ -35,30 +35,35 @@
     1.4  
     1.5  lemmas antisym_intro[intro!] = antisym
     1.6  
     1.7 -lemma less_eq_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
     1.8 +lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
     1.9  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
    1.10   apply(blast intro:trans)
    1.11  apply simp
    1.12  done
    1.13  
    1.14 -lemma less_eq_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    1.15 +lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    1.16  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    1.17   apply(blast intro:trans)
    1.18  apply simp
    1.19  done
    1.20  
    1.21 -lemma less_eq_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    1.22 +lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    1.23  by(blast intro: inf_greatest)
    1.24  
    1.25 -lemma less_eq_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.26 +lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.27  by(blast intro: trans)
    1.28  
    1.29 -lemma less_eq_inf_conv [simp]:
    1.30 +lemma le_inf_iff [simp]:
    1.31   "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    1.32  by blast
    1.33  
    1.34 -lemmas below_inf_conv = less_eq_inf_conv
    1.35 -  -- {* a duplicate for backward compatibility *}
    1.36 +lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
    1.37 +apply rule
    1.38 + apply(simp add: antisym)
    1.39 +apply(subgoal_tac "x \<sqinter> y \<sqsubseteq> y")
    1.40 + apply(simp)
    1.41 +apply(simp (no_asm))
    1.42 +done
    1.43  
    1.44  end
    1.45  
    1.46 @@ -68,28 +73,36 @@
    1.47  
    1.48  lemmas antisym_intro[intro!] = antisym
    1.49  
    1.50 -lemma less_eq_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.51 +lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.52  apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    1.53   apply(blast intro:trans)
    1.54  apply simp
    1.55  done
    1.56  
    1.57 -lemma less_eq_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.58 +lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.59  apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    1.60   apply(blast intro:trans)
    1.61  apply simp
    1.62  done
    1.63  
    1.64 -lemma less_eq_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.65 +lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.66  by(blast intro: sup_least)
    1.67  
    1.68 -lemma less_eq_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.69 +lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.70  by(blast intro: trans)
    1.71  
    1.72 -lemma above_sup_conv[simp]:
    1.73 +lemma ge_sup_conv[simp]:
    1.74   "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    1.75  by blast
    1.76  
    1.77 +lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
    1.78 +apply rule
    1.79 + apply(simp add: antisym)
    1.80 +apply(subgoal_tac "x \<sqsubseteq> x \<squnion> y")
    1.81 +apply(simp)
    1.82 + apply(simp (no_asm))
    1.83 +done
    1.84 +
    1.85  end
    1.86  
    1.87  
    1.88 @@ -162,9 +175,18 @@
    1.89  lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
    1.90  by(blast intro: antisym sup_ge1 sup_least inf_le1)
    1.91  
    1.92 -lemmas (in lattice) ACI = inf_ACI sup_ACI
    1.93 +lemmas ACI = inf_ACI sup_ACI
    1.94 +
    1.95 +text{* Towards distributivity *}
    1.96  
    1.97 -text{* Towards distributivity: if you have one of them, you have them all. *}
    1.98 +lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.99 +by blast
   1.100 +
   1.101 +lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   1.102 +by blast
   1.103 +
   1.104 +
   1.105 +text{* If you have one of them, you have them all. *}
   1.106  
   1.107  lemma distrib_imp1:
   1.108  assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   1.109 @@ -190,6 +212,10 @@
   1.110    finally show ?thesis .
   1.111  qed
   1.112  
   1.113 +(* seems unused *)
   1.114 +lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
   1.115 +by blast
   1.116 +
   1.117  end
   1.118  
   1.119  
   1.120 @@ -237,10 +263,10 @@
   1.121  
   1.122  declare
   1.123   min_max.antisym_intro[rule del]
   1.124 - min_max.less_eq_infI[rule del] min_max.less_eq_supI[rule del]
   1.125 - min_max.less_eq_supE[rule del] min_max.less_eq_infE[rule del]
   1.126 - min_max.less_eq_supI1[rule del] min_max.less_eq_supI2[rule del]
   1.127 - min_max.less_eq_infI1[rule del] min_max.less_eq_infI2[rule del]
   1.128 + min_max.le_infI[rule del] min_max.le_supI[rule del]
   1.129 + min_max.le_supE[rule del] min_max.le_infE[rule del]
   1.130 + min_max.le_supI1[rule del] min_max.le_supI2[rule del]
   1.131 + min_max.le_infI1[rule del] min_max.le_infI2[rule del]
   1.132  
   1.133  lemmas le_maxI1 = min_max.sup_ge1
   1.134  lemmas le_maxI2 = min_max.sup_ge2