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
```