src/HOL/Lattices.thy
changeset 32064 53ca12ff305d
parent 32063 2aab4f2af536
child 32204 b330aa4d59cb
     1.1 --- a/src/HOL/Lattices.thy	Mon Jul 13 08:25:43 2009 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Tue Jul 14 15:54:19 2009 +0200
     1.3 @@ -44,38 +44,27 @@
     1.4  context lower_semilattice
     1.5  begin
     1.6  
     1.7 -lemma le_infI1[intro]:
     1.8 -  assumes "a \<sqsubseteq> x"
     1.9 -  shows "a \<sqinter> b \<sqsubseteq> x"
    1.10 -proof (rule order_trans)
    1.11 -  from assms show "a \<sqsubseteq> x" .
    1.12 -  show "a \<sqinter> b \<sqsubseteq> a" by simp 
    1.13 -qed
    1.14 -lemmas (in -) [rule del] = le_infI1
    1.15 +lemma le_infI1:
    1.16 +  "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    1.17 +  by (rule order_trans) auto
    1.18  
    1.19 -lemma le_infI2[intro]:
    1.20 -  assumes "b \<sqsubseteq> x"
    1.21 -  shows "a \<sqinter> b \<sqsubseteq> x"
    1.22 -proof (rule order_trans)
    1.23 -  from assms show "b \<sqsubseteq> x" .
    1.24 -  show "a \<sqinter> b \<sqsubseteq> b" by simp
    1.25 -qed
    1.26 -lemmas (in -) [rule del] = le_infI2
    1.27 +lemma le_infI2:
    1.28 +  "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    1.29 +  by (rule order_trans) auto
    1.30  
    1.31 -lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    1.32 -by(blast intro: inf_greatest)
    1.33 -lemmas (in -) [rule del] = le_infI
    1.34 +lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    1.35 +  by (blast intro: inf_greatest)
    1.36  
    1.37 -lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.38 -  by (blast intro: order_trans)
    1.39 -lemmas (in -) [rule del] = le_infE
    1.40 +lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.41 +  by (blast intro: order_trans le_infI1 le_infI2)
    1.42  
    1.43  lemma le_inf_iff [simp]:
    1.44 -  "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    1.45 -by blast
    1.46 +  "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
    1.47 +  by (blast intro: le_infI elim: le_infE)
    1.48  
    1.49 -lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
    1.50 -  by (blast intro: antisym dest: eq_iff [THEN iffD1])
    1.51 +lemma le_iff_inf:
    1.52 +  "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
    1.53 +  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
    1.54  
    1.55  lemma mono_inf:
    1.56    fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
    1.57 @@ -87,28 +76,29 @@
    1.58  context upper_semilattice
    1.59  begin
    1.60  
    1.61 -lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.62 +lemma le_supI1:
    1.63 +  "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.64    by (rule order_trans) auto
    1.65 -lemmas (in -) [rule del] = le_supI1
    1.66  
    1.67 -lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.68 +lemma le_supI2:
    1.69 +  "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.70    by (rule order_trans) auto 
    1.71 -lemmas (in -) [rule del] = le_supI2
    1.72  
    1.73 -lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.74 +lemma le_supI:
    1.75 +  "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.76    by (blast intro: sup_least)
    1.77 -lemmas (in -) [rule del] = le_supI
    1.78  
    1.79 -lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.80 -  by (blast intro: order_trans)
    1.81 -lemmas (in -) [rule del] = le_supE
    1.82 +lemma le_supE:
    1.83 +  "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.84 +  by (blast intro: le_supI1 le_supI2 order_trans)
    1.85  
    1.86 -lemma ge_sup_conv[simp]:
    1.87 -  "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    1.88 -by blast
    1.89 +lemma le_sup_iff [simp]:
    1.90 +  "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.91 +  by (blast intro: le_supI elim: le_supE)
    1.92  
    1.93 -lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
    1.94 -  by (blast intro: antisym dest: eq_iff [THEN iffD1])
    1.95 +lemma le_iff_sup:
    1.96 +  "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
    1.97 +  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
    1.98  
    1.99  lemma mono_sup:
   1.100    fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
   1.101 @@ -118,62 +108,61 @@
   1.102  end
   1.103  
   1.104  
   1.105 -subsubsection{* Equational laws *}
   1.106 +subsubsection {* Equational laws *}
   1.107  
   1.108  context lower_semilattice
   1.109  begin
   1.110  
   1.111  lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
   1.112 -  by (blast intro: antisym)
   1.113 +  by (rule antisym) auto
   1.114  
   1.115  lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   1.116 -  by (blast intro: antisym)
   1.117 +  by (rule antisym) (auto intro: le_infI1 le_infI2)
   1.118  
   1.119  lemma inf_idem[simp]: "x \<sqinter> x = x"
   1.120 -  by (blast intro: antisym)
   1.121 +  by (rule antisym) auto
   1.122  
   1.123  lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   1.124 -  by (blast intro: antisym)
   1.125 +  by (rule antisym) (auto intro: le_infI2)
   1.126  
   1.127  lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   1.128 -  by (blast intro: antisym)
   1.129 +  by (rule antisym) auto
   1.130  
   1.131  lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   1.132 -  by (blast intro: antisym)
   1.133 +  by (rule antisym) auto
   1.134  
   1.135  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   1.136 -  by (blast intro: antisym)
   1.137 -
   1.138 -lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
   1.139 +  by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
   1.140 +  
   1.141 +lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
   1.142  
   1.143  end
   1.144  
   1.145 -
   1.146  context upper_semilattice
   1.147  begin
   1.148  
   1.149  lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
   1.150 -  by (blast intro: antisym)
   1.151 +  by (rule antisym) auto
   1.152  
   1.153  lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   1.154 -  by (blast intro: antisym)
   1.155 +  by (rule antisym) (auto intro: le_supI1 le_supI2)
   1.156  
   1.157  lemma sup_idem[simp]: "x \<squnion> x = x"
   1.158 -  by (blast intro: antisym)
   1.159 +  by (rule antisym) auto
   1.160  
   1.161  lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   1.162 -  by (blast intro: antisym)
   1.163 +  by (rule antisym) (auto intro: le_supI2)
   1.164  
   1.165  lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   1.166 -  by (blast intro: antisym)
   1.167 +  by (rule antisym) auto
   1.168  
   1.169  lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   1.170 -  by (blast intro: antisym)
   1.171 +  by (rule antisym) auto
   1.172  
   1.173  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   1.174 -  by (blast intro: antisym)
   1.175 +  by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
   1.176  
   1.177 -lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
   1.178 +lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
   1.179  
   1.180  end
   1.181  
   1.182 @@ -191,18 +180,17 @@
   1.183  lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
   1.184    by (blast intro: antisym sup_ge1 sup_least inf_le1)
   1.185  
   1.186 -lemmas ACI = inf_ACI sup_ACI
   1.187 +lemmas inf_sup_aci = inf_aci sup_aci
   1.188  
   1.189  lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
   1.190  
   1.191  text{* Towards distributivity *}
   1.192  
   1.193  lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   1.194 -  by blast
   1.195 +  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   1.196  
   1.197  lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   1.198 -  by blast
   1.199 -
   1.200 +  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   1.201  
   1.202  text{* If you have one of them, you have them all. *}
   1.203  
   1.204 @@ -230,10 +218,6 @@
   1.205    finally show ?thesis .
   1.206  qed
   1.207  
   1.208 -(* seems unused *)
   1.209 -lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
   1.210 -by blast
   1.211 -
   1.212  end
   1.213  
   1.214  
   1.215 @@ -247,7 +231,7 @@
   1.216  
   1.217  lemma sup_inf_distrib2:
   1.218   "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   1.219 -by(simp add:ACI sup_inf_distrib1)
   1.220 +by(simp add: inf_sup_aci sup_inf_distrib1)
   1.221  
   1.222  lemma inf_sup_distrib1:
   1.223   "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   1.224 @@ -255,7 +239,7 @@
   1.225  
   1.226  lemma inf_sup_distrib2:
   1.227   "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   1.228 -by(simp add:ACI inf_sup_distrib1)
   1.229 +by(simp add: inf_sup_aci inf_sup_distrib1)
   1.230  
   1.231  lemma dual_distrib_lattice:
   1.232    "distrib_lattice (op \<ge>) (op >) sup inf"
   1.233 @@ -458,10 +442,6 @@
   1.234  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   1.235    mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
   1.236  
   1.237 -lemmas [rule del] = min_max.le_infI min_max.le_supI
   1.238 -  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
   1.239 -  min_max.le_infI1 min_max.le_infI2
   1.240 -
   1.241  
   1.242  subsection {* Bool as lattice *}
   1.243  
   1.244 @@ -542,8 +522,6 @@
   1.245  
   1.246  text {* redundant bindings *}
   1.247  
   1.248 -lemmas inf_aci = inf_ACI
   1.249 -lemmas sup_aci = sup_ACI
   1.250  
   1.251  no_notation
   1.252    less_eq  (infix "\<sqsubseteq>" 50) and