New locales for orders and lattices where the equivalence relation is not restricted to equality.
1.1 --- a/NEWS Wed Jul 30 16:07:00 2008 +0200
1.2 +++ b/NEWS Wed Jul 30 19:03:33 2008 +0200
1.3 @@ -125,6 +125,13 @@
1.4
1.5 *** HOL-Algebra ***
1.6
1.7 +* New locales for orders and lattices where the equivalence relation
1.8 + is not restricted to equality. INCOMPATIBILITY: all order and
1.9 + lattice locales use a record structure with field eq for the
1.10 + equivalence.
1.11 +
1.12 +* New theory of factorial domains.
1.13 +
1.14 * Units_l_inv and Units_r_inv are now simprules by default.
1.15 INCOMPATIBILITY. Simplifier proof that require deletion of l_inv
1.16 and/or r_inv will now also require deletion of these lemmas.
1.17 @@ -136,8 +143,6 @@
1.18 greatest_carrier ~> greatest_closed
1.19 greatest_Lower_above ~> greatest_Lower_below
1.20
1.21 -* New theory of factorial domains.
1.22 -
1.23
1.24 *** HOL-NSA ***
1.25
2.1 --- a/src/HOL/Algebra/Divisibility.thy Wed Jul 30 16:07:00 2008 +0200
2.2 +++ b/src/HOL/Algebra/Divisibility.thy Wed Jul 30 19:03:33 2008 +0200
2.3 @@ -2,11 +2,12 @@
2.4 Title: Divisibility in monoids and rings
2.5 Id: $Id$
2.6 Author: Clemens Ballarin, started 18 July 2008
2.7 - Copyright: Clemens Ballarin
2.8 +
2.9 +Based on work by Stefan Hohe.
2.10 *)
2.11
2.12 theory Divisibility
2.13 -imports Permutation Coset Group GLattice
2.14 +imports Permutation Coset Group
2.15 begin
2.16
2.17 subsection {* Monoid with cancelation law *}
2.18 @@ -490,8 +491,8 @@
2.19 show "x divides y'" by simp
2.20 qed
2.21
2.22 -lemma (in monoid) division_gpartial_order [simp, intro!]:
2.23 - "gpartial_order (division_rel G)"
2.24 +lemma (in monoid) division_weak_partial_order [simp, intro!]:
2.25 + "weak_partial_order (division_rel G)"
2.26 apply unfold_locales
2.27 apply simp_all
2.28 apply (simp add: associated_sym)
2.29 @@ -731,12 +732,12 @@
2.30 apply (iprover intro: divides_trans)+
2.31 done
2.32
2.33 -lemma properfactor_glless:
2.34 +lemma properfactor_lless:
2.35 fixes G (structure)
2.36 - shows "properfactor G = glless (division_rel G)"
2.37 + shows "properfactor G = lless (division_rel G)"
2.38 apply (rule ext) apply (rule ext) apply rule
2.39 - apply (fastsimp elim: properfactorE2 intro: gllessI)
2.40 -apply (fastsimp elim: gllessE intro: properfactorI2)
2.41 + apply (fastsimp elim: properfactorE2 intro: weak_llessI)
2.42 +apply (fastsimp elim: weak_llessE intro: properfactorI2)
2.43 done
2.44
2.45 lemma (in monoid) properfactor_cong_l [trans]:
2.46 @@ -745,9 +746,9 @@
2.47 and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G"
2.48 shows "properfactor G x' y"
2.49 using pf
2.50 -unfolding properfactor_glless
2.51 +unfolding properfactor_lless
2.52 proof -
2.53 - interpret gpartial_order ["division_rel G"] ..
2.54 + interpret weak_partial_order ["division_rel G"] ..
2.55 from x'x
2.56 have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
2.57 also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
2.58 @@ -761,9 +762,9 @@
2.59 and carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
2.60 shows "properfactor G x y'"
2.61 using pf
2.62 -unfolding properfactor_glless
2.63 +unfolding properfactor_lless
2.64 proof -
2.65 - interpret gpartial_order ["division_rel G"] ..
2.66 + interpret weak_partial_order ["division_rel G"] ..
2.67 assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
2.68 also from yy'
2.69 have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
2.70 @@ -2630,7 +2631,7 @@
2.71 "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b"
2.72
2.73 constdefs (structure G)
2.74 - "SomeGcd G A == ginf (division_rel G) A"
2.75 + "SomeGcd G A == inf (division_rel G) A"
2.76
2.77
2.78 locale gcd_condition_monoid = comm_monoid_cancel +
2.79 @@ -2648,12 +2649,12 @@
2.80
2.81 subsubsection {* Connections to \texttt{Lattice.thy} *}
2.82
2.83 -lemma gcdof_ggreatestLower:
2.84 +lemma gcdof_greatestLower:
2.85 fixes G (structure)
2.86 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"
2.87 shows "(x \<in> carrier G \<and> x gcdof a b) =
2.88 - ggreatest (division_rel G) x (Lower (division_rel G) {a, b})"
2.89 -unfolding isgcd_def ggreatest_def Lower_def elem_def
2.90 + greatest (division_rel G) x (Lower (division_rel G) {a, b})"
2.91 +unfolding isgcd_def greatest_def Lower_def elem_def
2.92 proof (simp, safe)
2.93 fix xa
2.94 assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> xa divides x"
2.95 @@ -2674,12 +2675,12 @@
2.96 by (fast intro: r1)
2.97 qed (simp, simp)
2.98
2.99 -lemma lcmof_gleastUpper:
2.100 +lemma lcmof_leastUpper:
2.101 fixes G (structure)
2.102 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"
2.103 shows "(x \<in> carrier G \<and> x lcmof a b) =
2.104 - gleast (division_rel G) x (Upper (division_rel G) {a, b})"
2.105 -unfolding islcm_def gleast_def Upper_def elem_def
2.106 + least (division_rel G) x (Upper (division_rel G) {a, b})"
2.107 +unfolding islcm_def least_def Upper_def elem_def
2.108 proof (simp, safe)
2.109 fix xa
2.110 assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides xa"
2.111 @@ -2700,12 +2701,12 @@
2.112 by (fast intro: r1)
2.113 qed (simp, simp)
2.114
2.115 -lemma somegcd_gmeet:
2.116 +lemma somegcd_meet:
2.117 fixes G (structure)
2.118 assumes carr: "a \<in> carrier G" "b \<in> carrier G"
2.119 - shows "somegcd G a b = gmeet (division_rel G) a b"
2.120 -unfolding somegcd_def gmeet_def ginf_def
2.121 -by (simp add: gcdof_ggreatestLower[OF carr])
2.122 + shows "somegcd G a b = meet (division_rel G) a b"
2.123 +unfolding somegcd_def meet_def inf_def
2.124 +by (simp add: gcdof_greatestLower[OF carr])
2.125
2.126 lemma (in monoid) isgcd_divides_l:
2.127 assumes "a divides b"
2.128 @@ -2910,10 +2911,10 @@
2.129
2.130 subsubsection {* Gcd condition *}
2.131
2.132 -lemma (in gcd_condition_monoid) division_glower_semilattice [simp]:
2.133 - shows "glower_semilattice (division_rel G)"
2.134 +lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
2.135 + shows "weak_lower_semilattice (division_rel G)"
2.136 proof -
2.137 - interpret gpartial_order ["division_rel G"] ..
2.138 + interpret weak_partial_order ["division_rel G"] ..
2.139 show ?thesis
2.140 apply (unfold_locales, simp_all)
2.141 proof -
2.142 @@ -2925,9 +2926,9 @@
2.143 and isgcd: "z gcdof x y"
2.144 by auto
2.145 with carr
2.146 - have "ggreatest (division_rel G) z (Lower (division_rel G) {x, y})"
2.147 - by (subst gcdof_ggreatestLower[symmetric], simp+)
2.148 - thus "\<exists>z. ggreatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
2.149 + have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
2.150 + by (subst gcdof_greatestLower[symmetric], simp+)
2.151 + thus "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
2.152 qed
2.153 qed
2.154
2.155 @@ -2938,15 +2939,15 @@
2.156 shows "a' gcdof b c"
2.157 proof -
2.158 note carr = a'carr carr'
2.159 - interpret glower_semilattice ["division_rel G"] by simp
2.160 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.161 have "a' \<in> carrier G \<and> a' gcdof b c"
2.162 - apply (simp add: gcdof_ggreatestLower carr')
2.163 - apply (subst ggreatest_Lower_cong_l[of _ a])
2.164 + apply (simp add: gcdof_greatestLower carr')
2.165 + apply (subst greatest_Lower_cong_l[of _ a])
2.166 apply (simp add: a'a)
2.167 apply (simp add: carr)
2.168 apply (simp add: carr)
2.169 apply (simp add: carr)
2.170 - apply (simp add: gcdof_ggreatestLower[symmetric] agcd carr)
2.171 + apply (simp add: gcdof_greatestLower[symmetric] agcd carr)
2.172 done
2.173 thus ?thesis ..
2.174 qed
2.175 @@ -2955,10 +2956,10 @@
2.176 assumes carr: "a \<in> carrier G" "b \<in> carrier G"
2.177 shows "somegcd G a b \<in> carrier G"
2.178 proof -
2.179 - interpret glower_semilattice ["division_rel G"] by simp
2.180 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.181 show ?thesis
2.182 - apply (simp add: somegcd_gmeet[OF carr])
2.183 - apply (rule gmeet_closed[simplified], fact+)
2.184 + apply (simp add: somegcd_meet[OF carr])
2.185 + apply (rule meet_closed[simplified], fact+)
2.186 done
2.187 qed
2.188
2.189 @@ -2966,12 +2967,12 @@
2.190 assumes carr: "a \<in> carrier G" "b \<in> carrier G"
2.191 shows "(somegcd G a b) gcdof a b"
2.192 proof -
2.193 - interpret glower_semilattice ["division_rel G"] by simp
2.194 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.195 from carr
2.196 have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
2.197 - apply (subst gcdof_ggreatestLower, simp, simp)
2.198 - apply (simp add: somegcd_gmeet[OF carr] gmeet_def)
2.199 - apply (rule ginf_of_two_ggreatest[simplified], assumption+)
2.200 + apply (subst gcdof_greatestLower, simp, simp)
2.201 + apply (simp add: somegcd_meet[OF carr] meet_def)
2.202 + apply (rule inf_of_two_greatest[simplified], assumption+)
2.203 done
2.204 thus "(somegcd G a b) gcdof a b" by simp
2.205 qed
2.206 @@ -2980,10 +2981,10 @@
2.207 assumes carr: "a \<in> carrier G" "b \<in> carrier G"
2.208 shows "\<exists>x\<in>carrier G. x = somegcd G a b"
2.209 proof -
2.210 - interpret glower_semilattice ["division_rel G"] by simp
2.211 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.212 show ?thesis
2.213 - apply (simp add: somegcd_gmeet[OF carr])
2.214 - apply (rule gmeet_closed[simplified], fact+)
2.215 + apply (simp add: somegcd_meet[OF carr])
2.216 + apply (rule meet_closed[simplified], fact+)
2.217 done
2.218 qed
2.219
2.220 @@ -2991,10 +2992,10 @@
2.221 assumes carr: "a \<in> carrier G" "b \<in> carrier G"
2.222 shows "(somegcd G a b) divides a"
2.223 proof -
2.224 - interpret glower_semilattice ["division_rel G"] by simp
2.225 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.226 show ?thesis
2.227 - apply (simp add: somegcd_gmeet[OF carr])
2.228 - apply (rule gmeet_left[simplified], fact+)
2.229 + apply (simp add: somegcd_meet[OF carr])
2.230 + apply (rule meet_left[simplified], fact+)
2.231 done
2.232 qed
2.233
2.234 @@ -3002,10 +3003,10 @@
2.235 assumes carr: "a \<in> carrier G" "b \<in> carrier G"
2.236 shows "(somegcd G a b) divides b"
2.237 proof -
2.238 - interpret glower_semilattice ["division_rel G"] by simp
2.239 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.240 show ?thesis
2.241 - apply (simp add: somegcd_gmeet[OF carr])
2.242 - apply (rule gmeet_right[simplified], fact+)
2.243 + apply (simp add: somegcd_meet[OF carr])
2.244 + apply (rule meet_right[simplified], fact+)
2.245 done
2.246 qed
2.247
2.248 @@ -3014,10 +3015,10 @@
2.249 and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
2.250 shows "z divides (somegcd G x y)"
2.251 proof -
2.252 - interpret glower_semilattice ["division_rel G"] by simp
2.253 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.254 show ?thesis
2.255 - apply (simp add: somegcd_gmeet L)
2.256 - apply (rule gmeet_le[simplified], fact+)
2.257 + apply (simp add: somegcd_meet L)
2.258 + apply (rule meet_le[simplified], fact+)
2.259 done
2.260 qed
2.261
2.262 @@ -3026,10 +3027,10 @@
2.263 and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G"
2.264 shows "somegcd G x y \<sim> somegcd G x' y"
2.265 proof -
2.266 - interpret glower_semilattice ["division_rel G"] by simp
2.267 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.268 show ?thesis
2.269 - apply (simp add: somegcd_gmeet carr)
2.270 - apply (rule gmeet_cong_l[simplified], fact+)
2.271 + apply (simp add: somegcd_meet carr)
2.272 + apply (rule meet_cong_l[simplified], fact+)
2.273 done
2.274 qed
2.275
2.276 @@ -3038,10 +3039,10 @@
2.277 and yy': "y \<sim> y'"
2.278 shows "somegcd G x y \<sim> somegcd G x y'"
2.279 proof -
2.280 - interpret glower_semilattice ["division_rel G"] by simp
2.281 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.282 show ?thesis
2.283 - apply (simp add: somegcd_gmeet carr)
2.284 - apply (rule gmeet_cong_r[simplified], fact+)
2.285 + apply (simp add: somegcd_meet carr)
2.286 + apply (rule meet_cong_r[simplified], fact+)
2.287 done
2.288 qed
2.289
2.290 @@ -3089,10 +3090,10 @@
2.291 assumes "finite A" "A \<subseteq> carrier G" "A \<noteq> {}"
2.292 shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
2.293 proof -
2.294 - interpret glower_semilattice ["division_rel G"] by simp
2.295 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.296 show ?thesis
2.297 apply (simp add: SomeGcd_def)
2.298 - apply (rule finite_ginf_closed[simplified], fact+)
2.299 + apply (rule finite_inf_closed[simplified], fact+)
2.300 done
2.301 qed
2.302
2.303 @@ -3100,11 +3101,11 @@
2.304 assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"
2.305 shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
2.306 proof -
2.307 - interpret glower_semilattice ["division_rel G"] by simp
2.308 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.309 show ?thesis
2.310 - apply (subst (2 3) somegcd_gmeet, (simp add: carr)+)
2.311 - apply (simp add: somegcd_gmeet carr)
2.312 - apply (rule gmeet_assoc[simplified], fact+)
2.313 + apply (subst (2 3) somegcd_meet, (simp add: carr)+)
2.314 + apply (simp add: somegcd_meet carr)
2.315 + apply (rule weak_meet_assoc[simplified], fact+)
2.316 done
2.317 qed
2.318
2.319 @@ -3866,12 +3867,12 @@
2.320 interpretation factorial_monoid \<subseteq> gcd_condition_monoid
2.321 by (unfold_locales, rule gcdof_exists)
2.322
2.323 -lemma (in factorial_monoid) division_glattice [simp]:
2.324 - shows "glattice (division_rel G)"
2.325 +lemma (in factorial_monoid) division_weak_lattice [simp]:
2.326 + shows "weak_lattice (division_rel G)"
2.327 proof -
2.328 - interpret glower_semilattice ["division_rel G"] by simp
2.329 -
2.330 - show "glattice (division_rel G)"
2.331 + interpret weak_lower_semilattice ["division_rel G"] by simp
2.332 +
2.333 + show "weak_lattice (division_rel G)"
2.334 apply (unfold_locales, simp_all)
2.335 proof -
2.336 fix x y
2.337 @@ -3883,9 +3884,9 @@
2.338 and isgcd: "z lcmof x y"
2.339 by auto
2.340 with carr
2.341 - have "gleast (division_rel G) z (Upper (division_rel G) {x, y})"
2.342 - by (simp add: lcmof_gleastUpper[symmetric])
2.343 - thus "\<exists>z. gleast (division_rel G) z (Upper (division_rel G) {x, y})" by fast
2.344 + have "least (division_rel G) z (Upper (division_rel G) {x, y})"
2.345 + by (simp add: lcmof_leastUpper[symmetric])
2.346 + thus "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast
2.347 qed
2.348 qed
2.349
3.1 --- a/src/HOL/Algebra/GLattice.thy Wed Jul 30 16:07:00 2008 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,1181 +0,0 @@
3.4 -(*
3.5 - Title: HOL/Algebra/Lattice.thy
3.6 - Id: $Id$
3.7 - Author: Clemens Ballarin, started 7 November 2003
3.8 - Copyright: Clemens Ballarin
3.9 -*)
3.10 -
3.11 -theory GLattice imports Congruence begin
3.12 -
3.13 -(* FIXME: unify with Lattice.thy *)
3.14 -
3.15 -
3.16 -section {* Orders and Lattices *}
3.17 -
3.18 -subsection {* Partial Orders *}
3.19 -
3.20 -record 'a gorder = "'a eq_object" +
3.21 - le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
3.22 -
3.23 -locale gpartial_order = equivalence L +
3.24 - assumes le_refl [intro, simp]:
3.25 - "x \<in> carrier L ==> x \<sqsubseteq> x"
3.26 - and le_anti_sym [intro]:
3.27 - "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
3.28 - and le_trans [trans]:
3.29 - "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
3.30 - and le_cong:
3.31 - "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
3.32 -
3.33 -constdefs (structure L)
3.34 - glless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
3.35 - "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
3.36 -
3.37 -
3.38 -subsubsection {* The order relation *}
3.39 -
3.40 -context gpartial_order begin
3.41 -
3.42 -lemma le_cong_l [intro, trans]:
3.43 - "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
3.44 - by (auto intro: le_cong [THEN iffD2])
3.45 -
3.46 -lemma le_cong_r [intro, trans]:
3.47 - "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
3.48 - by (auto intro: le_cong [THEN iffD1])
3.49 -
3.50 -lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
3.51 - by (simp add: le_cong_l)
3.52 -
3.53 -end
3.54 -
3.55 -lemma gllessI:
3.56 - fixes R (structure)
3.57 - assumes "x \<sqsubseteq> y" and "~(x .= y)"
3.58 - shows "x \<sqsubset> y"
3.59 - using assms
3.60 - unfolding glless_def
3.61 - by simp
3.62 -
3.63 -lemma gllessD1:
3.64 - fixes R (structure)
3.65 - assumes "x \<sqsubset> y"
3.66 - shows "x \<sqsubseteq> y"
3.67 - using assms
3.68 - unfolding glless_def
3.69 - by simp
3.70 -
3.71 -lemma gllessD2:
3.72 - fixes R (structure)
3.73 - assumes "x \<sqsubset> y"
3.74 - shows "\<not> (x .= y)"
3.75 - using assms
3.76 - unfolding glless_def
3.77 - by simp
3.78 -
3.79 -lemma gllessE:
3.80 - fixes R (structure)
3.81 - assumes p: "x \<sqsubset> y"
3.82 - and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
3.83 - shows "P"
3.84 - using p
3.85 - by (blast dest: gllessD1 gllessD2 e)
3.86 -
3.87 -(*
3.88 -lemma (in gpartial_order) lless_cong_l [trans]:
3.89 - assumes xx': "x \<doteq> x'"
3.90 - and xy: "x' \<sqsubset> y"
3.91 - and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
3.92 - shows "x \<sqsubseteq> y"
3.93 -using xy
3.94 -unfolding lless_def
3.95 -proof clarify
3.96 - note xx'
3.97 - also assume "x' \<sqsubseteq> y"
3.98 - finally show "x \<sqsubseteq> y" by (simp add: carr)
3.99 -qed
3.100 -*)
3.101 -
3.102 -lemma (in gpartial_order) glless_cong_l [trans]:
3.103 - assumes xx': "x .= x'"
3.104 - and xy: "x' \<sqsubset> y"
3.105 - and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
3.106 - shows "x \<sqsubset> y"
3.107 - using assms
3.108 - apply (elim gllessE, intro gllessI)
3.109 - apply (iprover intro: le_cong_l)
3.110 - apply (iprover intro: trans sym)
3.111 - done
3.112 -
3.113 -(*
3.114 -lemma (in gpartial_order) lless_cong_r:
3.115 - assumes xy: "x \<sqsubset> y"
3.116 - and yy': "y \<doteq> y'"
3.117 - and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
3.118 - shows "x \<sqsubseteq> y'"
3.119 -using xy
3.120 -unfolding lless_def
3.121 -proof clarify
3.122 - assume "x \<sqsubseteq> y"
3.123 - also note yy'
3.124 - finally show "x \<sqsubseteq> y'" by (simp add: carr)
3.125 -qed
3.126 -*)
3.127 -
3.128 -lemma (in gpartial_order) glless_cong_r [trans]:
3.129 - assumes xy: "x \<sqsubset> y"
3.130 - and yy': "y .= y'"
3.131 - and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
3.132 - shows "x \<sqsubset> y'"
3.133 - using assms
3.134 - apply (elim gllessE, intro gllessI)
3.135 - apply (iprover intro: le_cong_r)
3.136 - apply (iprover intro: trans sym)
3.137 - done
3.138 -
3.139 -(*
3.140 -lemma (in gpartial_order) glless_antisym:
3.141 - assumes "a \<in> carrier L" "b \<in> carrier L"
3.142 - and "a \<sqsubset> b" "b \<sqsubset> a"
3.143 - shows "a \<doteq> b"
3.144 - using assms
3.145 - by (elim gllessE) (rule gle_anti_sym)
3.146 -
3.147 -lemma (in gpartial_order) glless_trans [trans]:
3.148 - assumes "a .\<sqsubset> b" "b .\<sqsubset> c"
3.149 - and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
3.150 - shows "a .\<sqsubset> c"
3.151 -using assms
3.152 -apply (elim gllessE, intro gllessI)
3.153 - apply (iprover dest: le_trans)
3.154 -proof (rule ccontr, simp)
3.155 - assume ab: "a \<sqsubseteq> b" and bc: "b \<sqsubseteq> c"
3.156 - and ac: "a \<doteq> c"
3.157 - and nbc: "\<not> b \<doteq> c"
3.158 - note ac[symmetric]
3.159 - also note ab
3.160 - finally have "c \<sqsubseteq> b" by simp
3.161 - with bc have "b \<doteq> c" by (iprover intro: gle_anti_sym carr)
3.162 - with nbc
3.163 - show "False" by simp
3.164 -qed
3.165 -*)
3.166 -
3.167 -subsubsection {* Upper and lower bounds of a set *}
3.168 -
3.169 -constdefs (structure L)
3.170 - Upper :: "[_, 'a set] => 'a set"
3.171 - "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
3.172 -
3.173 - Lower :: "[_, 'a set] => 'a set"
3.174 - "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
3.175 -
3.176 -lemma Upper_closed [intro!, simp]:
3.177 - "Upper L A \<subseteq> carrier L"
3.178 - by (unfold Upper_def) clarify
3.179 -
3.180 -lemma Upper_memD [dest]:
3.181 - fixes L (structure)
3.182 - shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
3.183 - by (unfold Upper_def) blast
3.184 -
3.185 -lemma (in gpartial_order) Upper_elemD [dest]:
3.186 - "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
3.187 - unfolding Upper_def elem_def
3.188 - by (blast dest: sym)
3.189 -
3.190 -lemma Upper_memI:
3.191 - fixes L (structure)
3.192 - shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
3.193 - by (unfold Upper_def) blast
3.194 -
3.195 -lemma (in gpartial_order) Upper_elemI:
3.196 - "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
3.197 - unfolding Upper_def by blast
3.198 -
3.199 -lemma Upper_antimono:
3.200 - "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
3.201 - by (unfold Upper_def) blast
3.202 -
3.203 -lemma (in gpartial_order) Upper_is_closed [simp]:
3.204 - "A \<subseteq> carrier L ==> is_closed (Upper L A)"
3.205 - by (rule is_closedI) (blast intro: Upper_memI)+
3.206 -
3.207 -lemma (in gpartial_order) Upper_mem_cong:
3.208 - assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
3.209 - and aa': "a .= a'"
3.210 - and aelem: "a \<in> Upper L A"
3.211 - shows "a' \<in> Upper L A"
3.212 -proof (rule Upper_memI[OF _ a'carr])
3.213 - fix y
3.214 - assume yA: "y \<in> A"
3.215 - hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
3.216 - also note aa'
3.217 - finally
3.218 - show "y \<sqsubseteq> a'"
3.219 - by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
3.220 -qed
3.221 -
3.222 -lemma (in gpartial_order) Upper_cong:
3.223 - assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
3.224 - and AA': "A {.=} A'"
3.225 - shows "Upper L A = Upper L A'"
3.226 -unfolding Upper_def
3.227 -apply rule
3.228 - apply (rule, clarsimp) defer 1
3.229 - apply (rule, clarsimp) defer 1
3.230 -proof -
3.231 - fix x a'
3.232 - assume carr: "x \<in> carrier L" "a' \<in> carrier L"
3.233 - and a'A': "a' \<in> A'"
3.234 - assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
3.235 -
3.236 - from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
3.237 - from this obtain a
3.238 - where aA: "a \<in> A"
3.239 - and a'a: "a' .= a"
3.240 - by auto
3.241 - note [simp] = subsetD[OF Acarr aA] carr
3.242 -
3.243 - note a'a
3.244 - also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
3.245 - finally show "a' \<sqsubseteq> x" by simp
3.246 -next
3.247 - fix x a
3.248 - assume carr: "x \<in> carrier L" "a \<in> carrier L"
3.249 - and aA: "a \<in> A"
3.250 - assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
3.251 -
3.252 - from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
3.253 - from this obtain a'
3.254 - where a'A': "a' \<in> A'"
3.255 - and aa': "a .= a'"
3.256 - by auto
3.257 - note [simp] = subsetD[OF A'carr a'A'] carr
3.258 -
3.259 - note aa'
3.260 - also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
3.261 - finally show "a \<sqsubseteq> x" by simp
3.262 -qed
3.263 -
3.264 -lemma Lower_closed [intro!, simp]:
3.265 - "Lower L A \<subseteq> carrier L"
3.266 - by (unfold Lower_def) clarify
3.267 -
3.268 -lemma Lower_memD [dest]:
3.269 - fixes L (structure)
3.270 - shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
3.271 - by (unfold Lower_def) blast
3.272 -
3.273 -lemma Lower_memI:
3.274 - fixes L (structure)
3.275 - shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
3.276 - by (unfold Lower_def) blast
3.277 -
3.278 -lemma Lower_antimono:
3.279 - "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
3.280 - by (unfold Lower_def) blast
3.281 -
3.282 -lemma (in gpartial_order) Lower_is_closed [simp]:
3.283 - "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
3.284 - by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
3.285 -
3.286 -lemma (in gpartial_order) Lower_mem_cong:
3.287 - assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
3.288 - and aa': "a .= a'"
3.289 - and aelem: "a \<in> Lower L A"
3.290 - shows "a' \<in> Lower L A"
3.291 -using assms Lower_closed[of L A]
3.292 -by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
3.293 -
3.294 -lemma (in gpartial_order) Lower_cong:
3.295 - assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
3.296 - and AA': "A {.=} A'"
3.297 - shows "Lower L A = Lower L A'"
3.298 -using Lower_memD[of y]
3.299 -unfolding Lower_def
3.300 -apply safe
3.301 - apply clarsimp defer 1
3.302 - apply clarsimp defer 1
3.303 -proof -
3.304 - fix x a'
3.305 - assume carr: "x \<in> carrier L" "a' \<in> carrier L"
3.306 - and a'A': "a' \<in> A'"
3.307 - assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
3.308 - hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
3.309 -
3.310 - from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
3.311 - from this obtain a
3.312 - where aA: "a \<in> A"
3.313 - and a'a: "a' .= a"
3.314 - by auto
3.315 -
3.316 - from aA and subsetD[OF Acarr aA]
3.317 - have "x \<sqsubseteq> a" by (rule aLxCond)
3.318 - also note a'a[symmetric]
3.319 - finally
3.320 - show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
3.321 -next
3.322 - fix x a
3.323 - assume carr: "x \<in> carrier L" "a \<in> carrier L"
3.324 - and aA: "a \<in> A"
3.325 - assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
3.326 - hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
3.327 -
3.328 - from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
3.329 - from this obtain a'
3.330 - where a'A': "a' \<in> A'"
3.331 - and aa': "a .= a'"
3.332 - by auto
3.333 - from a'A' and subsetD[OF A'carr a'A']
3.334 - have "x \<sqsubseteq> a'" by (rule a'LxCond)
3.335 - also note aa'[symmetric]
3.336 - finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
3.337 -qed
3.338 -
3.339 -
3.340 -subsubsection {* Least and greatest, as predicate *}
3.341 -
3.342 -constdefs (structure L)
3.343 - gleast :: "[_, 'a, 'a set] => bool"
3.344 - "gleast L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
3.345 -
3.346 - ggreatest :: "[_, 'a, 'a set] => bool"
3.347 - "ggreatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
3.348 -
3.349 -lemma gleast_closed [intro, simp]:
3.350 - "gleast L l A ==> l \<in> carrier L"
3.351 - by (unfold gleast_def) fast
3.352 -
3.353 -lemma gleast_mem:
3.354 - "gleast L l A ==> l \<in> A"
3.355 - by (unfold gleast_def) fast
3.356 -
3.357 -lemma (in gpartial_order) gleast_unique:
3.358 - "[| gleast L x A; gleast L y A |] ==> x .= y"
3.359 - by (unfold gleast_def) blast
3.360 -
3.361 -lemma gleast_le:
3.362 - fixes L (structure)
3.363 - shows "[| gleast L x A; a \<in> A |] ==> x \<sqsubseteq> a"
3.364 - by (unfold gleast_def) fast
3.365 -
3.366 -lemma (in gpartial_order) gleast_cong:
3.367 - "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> gleast L x A = gleast L x' A"
3.368 - by (unfold gleast_def) (auto dest: sym)
3.369 -
3.370 -text {* @{const gleast} is not congruent in the second parameter for
3.371 - @{term [locale=gpartial_order] "A {.=} A'"} *}
3.372 -
3.373 -lemma (in gpartial_order) gleast_Upper_cong_l:
3.374 - assumes "x .= x'"
3.375 - and "x \<in> carrier L" "x' \<in> carrier L"
3.376 - and "A \<subseteq> carrier L"
3.377 - shows "gleast L x (Upper L A) = gleast L x' (Upper L A)"
3.378 - apply (rule gleast_cong) using assms by auto
3.379 -
3.380 -lemma (in gpartial_order) gleast_Upper_cong_r:
3.381 - assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
3.382 - and AA': "A {.=} A'"
3.383 - shows "gleast L x (Upper L A) = gleast L x (Upper L A')"
3.384 -apply (subgoal_tac "Upper L A = Upper L A'", simp)
3.385 -by (rule Upper_cong) fact+
3.386 -
3.387 -lemma gleast_UpperI:
3.388 - fixes L (structure)
3.389 - assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
3.390 - and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
3.391 - and L: "A \<subseteq> carrier L" "s \<in> carrier L"
3.392 - shows "gleast L s (Upper L A)"
3.393 -proof -
3.394 - have "Upper L A \<subseteq> carrier L" by simp
3.395 - moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
3.396 - moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
3.397 - ultimately show ?thesis by (simp add: gleast_def)
3.398 -qed
3.399 -
3.400 -lemma gleast_Upper_above:
3.401 - fixes L (structure)
3.402 - shows "[| gleast L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
3.403 - by (unfold gleast_def) blast
3.404 -
3.405 -lemma ggreatest_closed [intro, simp]:
3.406 - "ggreatest L l A ==> l \<in> carrier L"
3.407 - by (unfold ggreatest_def) fast
3.408 -
3.409 -lemma ggreatest_mem:
3.410 - "ggreatest L l A ==> l \<in> A"
3.411 - by (unfold ggreatest_def) fast
3.412 -
3.413 -lemma (in gpartial_order) ggreatest_unique:
3.414 - "[| ggreatest L x A; ggreatest L y A |] ==> x .= y"
3.415 - by (unfold ggreatest_def) blast
3.416 -
3.417 -lemma ggreatest_le:
3.418 - fixes L (structure)
3.419 - shows "[| ggreatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
3.420 - by (unfold ggreatest_def) fast
3.421 -
3.422 -lemma (in gpartial_order) ggreatest_cong:
3.423 - "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
3.424 - ggreatest L x A = ggreatest L x' A"
3.425 - by (unfold ggreatest_def) (auto dest: sym)
3.426 -
3.427 -text {* @{const ggreatest} is not congruent in the second parameter for
3.428 - @{term [locale=gpartial_order] "A {.=} A'"} *}
3.429 -
3.430 -lemma (in gpartial_order) ggreatest_Lower_cong_l:
3.431 - assumes "x .= x'"
3.432 - and "x \<in> carrier L" "x' \<in> carrier L"
3.433 - and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
3.434 - shows "ggreatest L x (Lower L A) = ggreatest L x' (Lower L A)"
3.435 - apply (rule ggreatest_cong) using assms by auto
3.436 -
3.437 -lemma (in gpartial_order) ggreatest_Lower_cong_r:
3.438 - assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
3.439 - and AA': "A {.=} A'"
3.440 - shows "ggreatest L x (Lower L A) = ggreatest L x (Lower L A')"
3.441 -apply (subgoal_tac "Lower L A = Lower L A'", simp)
3.442 -by (rule Lower_cong) fact+
3.443 -
3.444 -lemma ggreatest_LowerI:
3.445 - fixes L (structure)
3.446 - assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
3.447 - and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
3.448 - and L: "A \<subseteq> carrier L" "i \<in> carrier L"
3.449 - shows "ggreatest L i (Lower L A)"
3.450 -proof -
3.451 - have "Lower L A \<subseteq> carrier L" by simp
3.452 - moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
3.453 - moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
3.454 - ultimately show ?thesis by (simp add: ggreatest_def)
3.455 -qed
3.456 -
3.457 -lemma ggreatest_Lower_below:
3.458 - fixes L (structure)
3.459 - shows "[| ggreatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
3.460 - by (unfold ggreatest_def) blast
3.461 -
3.462 -text {* Supremum and infimum *}
3.463 -
3.464 -constdefs (structure L)
3.465 - gsup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
3.466 - "\<Squnion>A == SOME x. gleast L x (Upper L A)"
3.467 -
3.468 - ginf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
3.469 - "\<Sqinter>A == SOME x. ggreatest L x (Lower L A)"
3.470 -
3.471 - gjoin :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
3.472 - "x \<squnion> y == \<Squnion> {x, y}"
3.473 -
3.474 - gmeet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
3.475 - "x \<sqinter> y == \<Sqinter> {x, y}"
3.476 -
3.477 -
3.478 -subsection {* Lattices *}
3.479 -
3.480 -locale gupper_semilattice = gpartial_order +
3.481 - assumes gsup_of_two_exists:
3.482 - "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. gleast L s (Upper L {x, y})"
3.483 -
3.484 -locale glower_semilattice = gpartial_order +
3.485 - assumes ginf_of_two_exists:
3.486 - "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. ggreatest L s (Lower L {x, y})"
3.487 -
3.488 -locale glattice = gupper_semilattice + glower_semilattice
3.489 -
3.490 -
3.491 -subsubsection {* Supremum *}
3.492 -
3.493 -lemma (in gupper_semilattice) gjoinI:
3.494 - "[| !!l. gleast L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
3.495 - ==> P (x \<squnion> y)"
3.496 -proof (unfold gjoin_def gsup_def)
3.497 - assume L: "x \<in> carrier L" "y \<in> carrier L"
3.498 - and P: "!!l. gleast L l (Upper L {x, y}) ==> P l"
3.499 - with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast
3.500 - with L show "P (SOME l. gleast L l (Upper L {x, y}))"
3.501 - by (fast intro: someI2 P)
3.502 -qed
3.503 -
3.504 -lemma (in gupper_semilattice) gjoin_closed [simp]:
3.505 - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
3.506 - by (rule gjoinI) (rule gleast_closed)
3.507 -
3.508 -lemma (in gupper_semilattice) gjoin_cong_l:
3.509 - assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
3.510 - and xx': "x .= x'"
3.511 - shows "x \<squnion> y .= x' \<squnion> y"
3.512 -proof (rule gjoinI, rule gjoinI)
3.513 - fix a b
3.514 - from xx' carr
3.515 - have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
3.516 -
3.517 - assume gleasta: "gleast L a (Upper L {x, y})"
3.518 - assume "gleast L b (Upper L {x', y})"
3.519 - with carr
3.520 - have gleastb: "gleast L b (Upper L {x, y})"
3.521 - by (simp add: gleast_Upper_cong_r[OF _ _ seq])
3.522 -
3.523 - from gleasta gleastb
3.524 - show "a .= b" by (rule gleast_unique)
3.525 -qed (rule carr)+
3.526 -
3.527 -lemma (in gupper_semilattice) gjoin_cong_r:
3.528 - assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
3.529 - and yy': "y .= y'"
3.530 - shows "x \<squnion> y .= x \<squnion> y'"
3.531 -proof (rule gjoinI, rule gjoinI)
3.532 - fix a b
3.533 - have "{x, y} = {y, x}" by fast
3.534 - also from carr yy'
3.535 - have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
3.536 - also have "{y', x} = {x, y'}" by fast
3.537 - finally
3.538 - have seq: "{x, y} {.=} {x, y'}" .
3.539 -
3.540 - assume gleasta: "gleast L a (Upper L {x, y})"
3.541 - assume "gleast L b (Upper L {x, y'})"
3.542 - with carr
3.543 - have gleastb: "gleast L b (Upper L {x, y})"
3.544 - by (simp add: gleast_Upper_cong_r[OF _ _ seq])
3.545 -
3.546 - from gleasta gleastb
3.547 - show "a .= b" by (rule gleast_unique)
3.548 -qed (rule carr)+
3.549 -
3.550 -lemma (in gpartial_order) gsup_of_singletonI: (* only reflexivity needed ? *)
3.551 - "x \<in> carrier L ==> gleast L x (Upper L {x})"
3.552 - by (rule gleast_UpperI) auto
3.553 -
3.554 -lemma (in gpartial_order) gsup_of_singleton [simp]:
3.555 - "x \<in> carrier L ==> \<Squnion>{x} .= x"
3.556 - unfolding gsup_def
3.557 - by (rule someI2) (auto intro: gleast_unique gsup_of_singletonI)
3.558 -
3.559 -lemma (in gpartial_order) gsup_of_singleton_closed [simp]:
3.560 - "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
3.561 - unfolding gsup_def
3.562 - by (rule someI2) (auto intro: gsup_of_singletonI)
3.563 -
3.564 -text {* Condition on @{text A}: supremum exists. *}
3.565 -
3.566 -lemma (in gupper_semilattice) gsup_insertI:
3.567 - "[| !!s. gleast L s (Upper L (insert x A)) ==> P s;
3.568 - gleast L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
3.569 - ==> P (\<Squnion>(insert x A))"
3.570 -proof (unfold gsup_def)
3.571 - assume L: "x \<in> carrier L" "A \<subseteq> carrier L"
3.572 - and P: "!!l. gleast L l (Upper L (insert x A)) ==> P l"
3.573 - and gleast_a: "gleast L a (Upper L A)"
3.574 - from L gleast_a have La: "a \<in> carrier L" by simp
3.575 - from L gsup_of_two_exists gleast_a
3.576 - obtain s where gleast_s: "gleast L s (Upper L {a, x})" by blast
3.577 - show "P (SOME l. gleast L l (Upper L (insert x A)))"
3.578 - proof (rule someI2)
3.579 - show "gleast L s (Upper L (insert x A))"
3.580 - proof (rule gleast_UpperI)
3.581 - fix z
3.582 - assume "z \<in> insert x A"
3.583 - then show "z \<sqsubseteq> s"
3.584 - proof
3.585 - assume "z = x" then show ?thesis
3.586 - by (simp add: gleast_Upper_above [OF gleast_s] L La)
3.587 - next
3.588 - assume "z \<in> A"
3.589 - with L gleast_s gleast_a show ?thesis
3.590 - by (rule_tac le_trans [where y = a]) (auto dest: gleast_Upper_above)
3.591 - qed
3.592 - next
3.593 - fix y
3.594 - assume y: "y \<in> Upper L (insert x A)"
3.595 - show "s \<sqsubseteq> y"
3.596 - proof (rule gleast_le [OF gleast_s], rule Upper_memI)
3.597 - fix z
3.598 - assume z: "z \<in> {a, x}"
3.599 - then show "z \<sqsubseteq> y"
3.600 - proof
3.601 - have y': "y \<in> Upper L A"
3.602 - apply (rule subsetD [where A = "Upper L (insert x A)"])
3.603 - apply (rule Upper_antimono)
3.604 - apply blast
3.605 - apply (rule y)
3.606 - done
3.607 - assume "z = a"
3.608 - with y' gleast_a show ?thesis by (fast dest: gleast_le)
3.609 - next
3.610 - assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
3.611 - with y L show ?thesis by blast
3.612 - qed
3.613 - qed (rule Upper_closed [THEN subsetD, OF y])
3.614 - next
3.615 - from L show "insert x A \<subseteq> carrier L" by simp
3.616 - from gleast_s show "s \<in> carrier L" by simp
3.617 - qed
3.618 - qed (rule P)
3.619 -qed
3.620 -
3.621 -lemma (in gupper_semilattice) finite_gsup_gleast:
3.622 - "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> gleast L (\<Squnion>A) (Upper L A)"
3.623 -proof (induct set: finite)
3.624 - case empty
3.625 - then show ?case by simp
3.626 -next
3.627 - case (insert x A)
3.628 - show ?case
3.629 - proof (cases "A = {}")
3.630 - case True
3.631 - with insert show ?thesis
3.632 - by simp (simp add: gleast_cong [OF gsup_of_singleton]
3.633 - gsup_of_singleton_closed gsup_of_singletonI)
3.634 - (* The above step is hairy; gleast_cong can make simp loop.
3.635 - Would want special version of simp to apply gleast_cong. *)
3.636 - next
3.637 - case False
3.638 - with insert have "gleast L (\<Squnion>A) (Upper L A)" by simp
3.639 - with _ show ?thesis
3.640 - by (rule gsup_insertI) (simp_all add: insert [simplified])
3.641 - qed
3.642 -qed
3.643 -
3.644 -lemma (in gupper_semilattice) finite_gsup_insertI:
3.645 - assumes P: "!!l. gleast L l (Upper L (insert x A)) ==> P l"
3.646 - and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"
3.647 - shows "P (\<Squnion> (insert x A))"
3.648 -proof (cases "A = {}")
3.649 - case True with P and xA show ?thesis
3.650 - by (simp add: finite_gsup_gleast)
3.651 -next
3.652 - case False with P and xA show ?thesis
3.653 - by (simp add: gsup_insertI finite_gsup_gleast)
3.654 -qed
3.655 -
3.656 -lemma (in gupper_semilattice) finite_gsup_closed [simp]:
3.657 - "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
3.658 -proof (induct set: finite)
3.659 - case empty then show ?case by simp
3.660 -next
3.661 - case insert then show ?case
3.662 - by - (rule finite_gsup_insertI, simp_all)
3.663 -qed
3.664 -
3.665 -lemma (in gupper_semilattice) gjoin_left:
3.666 - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
3.667 - by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem)
3.668 -
3.669 -lemma (in gupper_semilattice) gjoin_right:
3.670 - "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
3.671 - by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem)
3.672 -
3.673 -lemma (in gupper_semilattice) gsup_of_two_gleast:
3.674 - "[| x \<in> carrier L; y \<in> carrier L |] ==> gleast L (\<Squnion>{x, y}) (Upper L {x, y})"
3.675 -proof (unfold gsup_def)
3.676 - assume L: "x \<in> carrier L" "y \<in> carrier L"
3.677 - with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast
3.678 - with L show "gleast L (SOME z. gleast L z (Upper L {x, y})) (Upper L {x, y})"
3.679 - by (fast intro: someI2 gleast_unique) (* blast fails *)
3.680 -qed
3.681 -
3.682 -lemma (in gupper_semilattice) gjoin_le:
3.683 - assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z"
3.684 - and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
3.685 - shows "x \<squnion> y \<sqsubseteq> z"
3.686 -proof (rule gjoinI [OF _ x y])
3.687 - fix s
3.688 - assume "gleast L s (Upper L {x, y})"
3.689 - with sub z show "s \<sqsubseteq> z" by (fast elim: gleast_le intro: Upper_memI)
3.690 -qed
3.691 -
3.692 -lemma (in gupper_semilattice) gjoin_assoc_lemma:
3.693 - assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
3.694 - shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
3.695 -proof (rule finite_gsup_insertI)
3.696 - -- {* The textbook argument in Jacobson I, p 457 *}
3.697 - fix s
3.698 - assume gsup: "gleast L s (Upper L {x, y, z})"
3.699 - show "x \<squnion> (y \<squnion> z) .= s"
3.700 - proof (rule le_anti_sym)
3.701 - from gsup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
3.702 - by (fastsimp intro!: gjoin_le elim: gleast_Upper_above)
3.703 - next
3.704 - from gsup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
3.705 - by (erule_tac gleast_le)
3.706 - (blast intro!: Upper_memI intro: le_trans gjoin_left gjoin_right gjoin_closed)
3.707 - qed (simp_all add: L gleast_closed [OF gsup])
3.708 -qed (simp_all add: L)
3.709 -
3.710 -text {* Commutativity holds for @{text "="}. *}
3.711 -
3.712 -lemma gjoin_comm:
3.713 - fixes L (structure)
3.714 - shows "x \<squnion> y = y \<squnion> x"
3.715 - by (unfold gjoin_def) (simp add: insert_commute)
3.716 -
3.717 -lemma (in gupper_semilattice) gjoin_assoc:
3.718 - assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
3.719 - shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
3.720 -proof -
3.721 - (* FIXME: could be simplified by improved simp: uniform use of .=,
3.722 - omit [symmetric] in last step. *)
3.723 - have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: gjoin_comm)
3.724 - also from L have "... .= \<Squnion>{z, x, y}" by (simp add: gjoin_assoc_lemma)
3.725 - also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
3.726 - also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: gjoin_assoc_lemma [symmetric])
3.727 - finally show ?thesis by (simp add: L)
3.728 -qed
3.729 -
3.730 -
3.731 -subsubsection {* Infimum *}
3.732 -
3.733 -lemma (in glower_semilattice) gmeetI:
3.734 - "[| !!i. ggreatest L i (Lower L {x, y}) ==> P i;
3.735 - x \<in> carrier L; y \<in> carrier L |]
3.736 - ==> P (x \<sqinter> y)"
3.737 -proof (unfold gmeet_def ginf_def)
3.738 - assume L: "x \<in> carrier L" "y \<in> carrier L"
3.739 - and P: "!!g. ggreatest L g (Lower L {x, y}) ==> P g"
3.740 - with ginf_of_two_exists obtain i where "ggreatest L i (Lower L {x, y})" by fast
3.741 - with L show "P (SOME g. ggreatest L g (Lower L {x, y}))"
3.742 - by (fast intro: someI2 ggreatest_unique P)
3.743 -qed
3.744 -
3.745 -lemma (in glower_semilattice) gmeet_closed [simp]:
3.746 - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
3.747 - by (rule gmeetI) (rule ggreatest_closed)
3.748 -
3.749 -lemma (in glower_semilattice) gmeet_cong_l:
3.750 - assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
3.751 - and xx': "x .= x'"
3.752 - shows "x \<sqinter> y .= x' \<sqinter> y"
3.753 -proof (rule gmeetI, rule gmeetI)
3.754 - fix a b
3.755 - from xx' carr
3.756 - have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
3.757 -
3.758 - assume ggreatesta: "ggreatest L a (Lower L {x, y})"
3.759 - assume "ggreatest L b (Lower L {x', y})"
3.760 - with carr
3.761 - have ggreatestb: "ggreatest L b (Lower L {x, y})"
3.762 - by (simp add: ggreatest_Lower_cong_r[OF _ _ seq])
3.763 -
3.764 - from ggreatesta ggreatestb
3.765 - show "a .= b" by (rule ggreatest_unique)
3.766 -qed (rule carr)+
3.767 -
3.768 -lemma (in glower_semilattice) gmeet_cong_r:
3.769 - assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
3.770 - and yy': "y .= y'"
3.771 - shows "x \<sqinter> y .= x \<sqinter> y'"
3.772 -proof (rule gmeetI, rule gmeetI)
3.773 - fix a b
3.774 - have "{x, y} = {y, x}" by fast
3.775 - also from carr yy'
3.776 - have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
3.777 - also have "{y', x} = {x, y'}" by fast
3.778 - finally
3.779 - have seq: "{x, y} {.=} {x, y'}" .
3.780 -
3.781 - assume ggreatesta: "ggreatest L a (Lower L {x, y})"
3.782 - assume "ggreatest L b (Lower L {x, y'})"
3.783 - with carr
3.784 - have ggreatestb: "ggreatest L b (Lower L {x, y})"
3.785 - by (simp add: ggreatest_Lower_cong_r[OF _ _ seq])
3.786 -
3.787 - from ggreatesta ggreatestb
3.788 - show "a .= b" by (rule ggreatest_unique)
3.789 -qed (rule carr)+
3.790 -
3.791 -lemma (in gpartial_order) ginf_of_singletonI: (* only reflexivity needed ? *)
3.792 - "x \<in> carrier L ==> ggreatest L x (Lower L {x})"
3.793 - by (rule ggreatest_LowerI) auto
3.794 -
3.795 -lemma (in gpartial_order) ginf_of_singleton [simp]:
3.796 - "x \<in> carrier L ==> \<Sqinter>{x} .= x"
3.797 - unfolding ginf_def
3.798 - by (rule someI2) (auto intro: ggreatest_unique ginf_of_singletonI)
3.799 -
3.800 -lemma (in gpartial_order) ginf_of_singleton_closed:
3.801 - "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
3.802 - unfolding ginf_def
3.803 - by (rule someI2) (auto intro: ginf_of_singletonI)
3.804 -
3.805 -text {* Condition on @{text A}: infimum exists. *}
3.806 -
3.807 -lemma (in glower_semilattice) ginf_insertI:
3.808 - "[| !!i. ggreatest L i (Lower L (insert x A)) ==> P i;
3.809 - ggreatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
3.810 - ==> P (\<Sqinter>(insert x A))"
3.811 -proof (unfold ginf_def)
3.812 - assume L: "x \<in> carrier L" "A \<subseteq> carrier L"
3.813 - and P: "!!g. ggreatest L g (Lower L (insert x A)) ==> P g"
3.814 - and ggreatest_a: "ggreatest L a (Lower L A)"
3.815 - from L ggreatest_a have La: "a \<in> carrier L" by simp
3.816 - from L ginf_of_two_exists ggreatest_a
3.817 - obtain i where ggreatest_i: "ggreatest L i (Lower L {a, x})" by blast
3.818 - show "P (SOME g. ggreatest L g (Lower L (insert x A)))"
3.819 - proof (rule someI2)
3.820 - show "ggreatest L i (Lower L (insert x A))"
3.821 - proof (rule ggreatest_LowerI)
3.822 - fix z
3.823 - assume "z \<in> insert x A"
3.824 - then show "i \<sqsubseteq> z"
3.825 - proof
3.826 - assume "z = x" then show ?thesis
3.827 - by (simp add: ggreatest_Lower_below [OF ggreatest_i] L La)
3.828 - next
3.829 - assume "z \<in> A"
3.830 - with L ggreatest_i ggreatest_a show ?thesis
3.831 - by (rule_tac le_trans [where y = a]) (auto dest: ggreatest_Lower_below)
3.832 - qed
3.833 - next
3.834 - fix y
3.835 - assume y: "y \<in> Lower L (insert x A)"
3.836 - show "y \<sqsubseteq> i"
3.837 - proof (rule ggreatest_le [OF ggreatest_i], rule Lower_memI)
3.838 - fix z
3.839 - assume z: "z \<in> {a, x}"
3.840 - then show "y \<sqsubseteq> z"
3.841 - proof
3.842 - have y': "y \<in> Lower L A"
3.843 - apply (rule subsetD [where A = "Lower L (insert x A)"])
3.844 - apply (rule Lower_antimono)
3.845 - apply blast
3.846 - apply (rule y)
3.847 - done
3.848 - assume "z = a"
3.849 - with y' ggreatest_a show ?thesis by (fast dest: ggreatest_le)
3.850 - next
3.851 - assume "z \<in> {x}"
3.852 - with y L show ?thesis by blast
3.853 - qed
3.854 - qed (rule Lower_closed [THEN subsetD, OF y])
3.855 - next
3.856 - from L show "insert x A \<subseteq> carrier L" by simp
3.857 - from ggreatest_i show "i \<in> carrier L" by simp
3.858 - qed
3.859 - qed (rule P)
3.860 -qed
3.861 -
3.862 -lemma (in glower_semilattice) finite_ginf_ggreatest:
3.863 - "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> ggreatest L (\<Sqinter>A) (Lower L A)"
3.864 -proof (induct set: finite)
3.865 - case empty then show ?case by simp
3.866 -next
3.867 - case (insert x A)
3.868 - show ?case
3.869 - proof (cases "A = {}")
3.870 - case True
3.871 - with insert show ?thesis
3.872 - by simp (simp add: ggreatest_cong [OF ginf_of_singleton]
3.873 - ginf_of_singleton_closed ginf_of_singletonI)
3.874 - next
3.875 - case False
3.876 - from insert show ?thesis
3.877 - proof (rule_tac ginf_insertI)
3.878 - from False insert show "ggreatest L (\<Sqinter>A) (Lower L A)" by simp
3.879 - qed simp_all
3.880 - qed
3.881 -qed
3.882 -
3.883 -lemma (in glower_semilattice) finite_ginf_insertI:
3.884 - assumes P: "!!i. ggreatest L i (Lower L (insert x A)) ==> P i"
3.885 - and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"
3.886 - shows "P (\<Sqinter> (insert x A))"
3.887 -proof (cases "A = {}")
3.888 - case True with P and xA show ?thesis
3.889 - by (simp add: finite_ginf_ggreatest)
3.890 -next
3.891 - case False with P and xA show ?thesis
3.892 - by (simp add: ginf_insertI finite_ginf_ggreatest)
3.893 -qed
3.894 -
3.895 -lemma (in glower_semilattice) finite_ginf_closed [simp]:
3.896 - "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
3.897 -proof (induct set: finite)
3.898 - case empty then show ?case by simp
3.899 -next
3.900 - case insert then show ?case
3.901 - by (rule_tac finite_ginf_insertI) (simp_all)
3.902 -qed
3.903 -
3.904 -lemma (in glower_semilattice) gmeet_left:
3.905 - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
3.906 - by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem)
3.907 -
3.908 -lemma (in glower_semilattice) gmeet_right:
3.909 - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
3.910 - by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem)
3.911 -
3.912 -lemma (in glower_semilattice) ginf_of_two_ggreatest:
3.913 - "[| x \<in> carrier L; y \<in> carrier L |] ==>
3.914 - ggreatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
3.915 -proof (unfold ginf_def)
3.916 - assume L: "x \<in> carrier L" "y \<in> carrier L"
3.917 - with ginf_of_two_exists obtain s where "ggreatest L s (Lower L {x, y})" by fast
3.918 - with L
3.919 - show "ggreatest L (SOME z. ggreatest L z (Lower L {x, y})) (Lower L {x, y})"
3.920 - by (fast intro: someI2 ggreatest_unique) (* blast fails *)
3.921 -qed
3.922 -
3.923 -lemma (in glower_semilattice) gmeet_le:
3.924 - assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y"
3.925 - and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
3.926 - shows "z \<sqsubseteq> x \<sqinter> y"
3.927 -proof (rule gmeetI [OF _ x y])
3.928 - fix i
3.929 - assume "ggreatest L i (Lower L {x, y})"
3.930 - with sub z show "z \<sqsubseteq> i" by (fast elim: ggreatest_le intro: Lower_memI)
3.931 -qed
3.932 -
3.933 -lemma (in glower_semilattice) gmeet_assoc_lemma:
3.934 - assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
3.935 - shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
3.936 -proof (rule finite_ginf_insertI)
3.937 - txt {* The textbook argument in Jacobson I, p 457 *}
3.938 - fix i
3.939 - assume ginf: "ggreatest L i (Lower L {x, y, z})"
3.940 - show "x \<sqinter> (y \<sqinter> z) .= i"
3.941 - proof (rule le_anti_sym)
3.942 - from ginf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
3.943 - by (fastsimp intro!: gmeet_le elim: ggreatest_Lower_below)
3.944 - next
3.945 - from ginf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
3.946 - by (erule_tac ggreatest_le)
3.947 - (blast intro!: Lower_memI intro: le_trans gmeet_left gmeet_right gmeet_closed)
3.948 - qed (simp_all add: L ggreatest_closed [OF ginf])
3.949 -qed (simp_all add: L)
3.950 -
3.951 -lemma gmeet_comm:
3.952 - fixes L (structure)
3.953 - shows "x \<sqinter> y = y \<sqinter> x"
3.954 - by (unfold gmeet_def) (simp add: insert_commute)
3.955 -
3.956 -lemma (in glower_semilattice) gmeet_assoc:
3.957 - assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
3.958 - shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
3.959 -proof -
3.960 - (* FIXME: improved simp, see gjoin_assoc above *)
3.961 - have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: gmeet_comm)
3.962 - also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: gmeet_assoc_lemma)
3.963 - also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
3.964 - also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: gmeet_assoc_lemma [symmetric])
3.965 - finally show ?thesis by (simp add: L)
3.966 -qed
3.967 -
3.968 -
3.969 -subsection {* Total Orders *}
3.970 -
3.971 -locale gtotal_order = gpartial_order +
3.972 - assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
3.973 -
3.974 -text {* Introduction rule: the usual definition of total order *}
3.975 -
3.976 -lemma (in gpartial_order) gtotal_orderI:
3.977 - assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
3.978 - shows "gtotal_order L"
3.979 - by unfold_locales (rule total)
3.980 -
3.981 -text {* Total orders are lattices. *}
3.982 -
3.983 -interpretation gtotal_order < glattice
3.984 -proof unfold_locales
3.985 - fix x y
3.986 - assume L: "x \<in> carrier L" "y \<in> carrier L"
3.987 - show "EX s. gleast L s (Upper L {x, y})"
3.988 - proof -
3.989 - note total L
3.990 - moreover
3.991 - {
3.992 - assume "x \<sqsubseteq> y"
3.993 - with L have "gleast L y (Upper L {x, y})"
3.994 - by (rule_tac gleast_UpperI) auto
3.995 - }
3.996 - moreover
3.997 - {
3.998 - assume "y \<sqsubseteq> x"
3.999 - with L have "gleast L x (Upper L {x, y})"
3.1000 - by (rule_tac gleast_UpperI) auto
3.1001 - }
3.1002 - ultimately show ?thesis by blast
3.1003 - qed
3.1004 -next
3.1005 - fix x y
3.1006 - assume L: "x \<in> carrier L" "y \<in> carrier L"
3.1007 - show "EX i. ggreatest L i (Lower L {x, y})"
3.1008 - proof -
3.1009 - note total L
3.1010 - moreover
3.1011 - {
3.1012 - assume "y \<sqsubseteq> x"
3.1013 - with L have "ggreatest L y (Lower L {x, y})"
3.1014 - by (rule_tac ggreatest_LowerI) auto
3.1015 - }
3.1016 - moreover
3.1017 - {
3.1018 - assume "x \<sqsubseteq> y"
3.1019 - with L have "ggreatest L x (Lower L {x, y})"
3.1020 - by (rule_tac ggreatest_LowerI) auto
3.1021 - }
3.1022 - ultimately show ?thesis by blast
3.1023 - qed
3.1024 -qed
3.1025 -
3.1026 -
3.1027 -subsection {* Complete lattices *}
3.1028 -
3.1029 -locale complete_lattice = glattice +
3.1030 - assumes gsup_exists:
3.1031 - "[| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)"
3.1032 - and ginf_exists:
3.1033 - "[| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)"
3.1034 -
3.1035 -text {* Introduction rule: the usual definition of complete lattice *}
3.1036 -
3.1037 -lemma (in gpartial_order) complete_latticeI:
3.1038 - assumes gsup_exists:
3.1039 - "!!A. [| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)"
3.1040 - and ginf_exists:
3.1041 - "!!A. [| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)"
3.1042 - shows "complete_lattice L"
3.1043 - by unfold_locales (auto intro: gsup_exists ginf_exists)
3.1044 -
3.1045 -constdefs (structure L)
3.1046 - top :: "_ => 'a" ("\<top>\<index>")
3.1047 - "\<top> == gsup L (carrier L)"
3.1048 -
3.1049 - bottom :: "_ => 'a" ("\<bottom>\<index>")
3.1050 - "\<bottom> == ginf L (carrier L)"
3.1051 -
3.1052 -
3.1053 -lemma (in complete_lattice) gsupI:
3.1054 - "[| !!l. gleast L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
3.1055 - ==> P (\<Squnion>A)"
3.1056 -proof (unfold gsup_def)
3.1057 - assume L: "A \<subseteq> carrier L"
3.1058 - and P: "!!l. gleast L l (Upper L A) ==> P l"
3.1059 - with gsup_exists obtain s where "gleast L s (Upper L A)" by blast
3.1060 - with L show "P (SOME l. gleast L l (Upper L A))"
3.1061 - by (fast intro: someI2 gleast_unique P)
3.1062 -qed
3.1063 -
3.1064 -lemma (in complete_lattice) gsup_closed [simp]:
3.1065 - "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
3.1066 - by (rule gsupI) simp_all
3.1067 -
3.1068 -lemma (in complete_lattice) top_closed [simp, intro]:
3.1069 - "\<top> \<in> carrier L"
3.1070 - by (unfold top_def) simp
3.1071 -
3.1072 -lemma (in complete_lattice) ginfI:
3.1073 - "[| !!i. ggreatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
3.1074 - ==> P (\<Sqinter>A)"
3.1075 -proof (unfold ginf_def)
3.1076 - assume L: "A \<subseteq> carrier L"
3.1077 - and P: "!!l. ggreatest L l (Lower L A) ==> P l"
3.1078 - with ginf_exists obtain s where "ggreatest L s (Lower L A)" by blast
3.1079 - with L show "P (SOME l. ggreatest L l (Lower L A))"
3.1080 - by (fast intro: someI2 ggreatest_unique P)
3.1081 -qed
3.1082 -
3.1083 -lemma (in complete_lattice) ginf_closed [simp]:
3.1084 - "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
3.1085 - by (rule ginfI) simp_all
3.1086 -
3.1087 -lemma (in complete_lattice) bottom_closed [simp, intro]:
3.1088 - "\<bottom> \<in> carrier L"
3.1089 - by (unfold bottom_def) simp
3.1090 -
3.1091 -text {* Jacobson: Theorem 8.1 *}
3.1092 -
3.1093 -lemma Lower_empty [simp]:
3.1094 - "Lower L {} = carrier L"
3.1095 - by (unfold Lower_def) simp
3.1096 -
3.1097 -lemma Upper_empty [simp]:
3.1098 - "Upper L {} = carrier L"
3.1099 - by (unfold Upper_def) simp
3.1100 -
3.1101 -theorem (in gpartial_order) complete_lattice_criterion1:
3.1102 - assumes top_exists: "EX g. ggreatest L g (carrier L)"
3.1103 - and ginf_exists:
3.1104 - "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. ggreatest L i (Lower L A)"
3.1105 - shows "complete_lattice L"
3.1106 -proof (rule complete_latticeI)
3.1107 - from top_exists obtain top where top: "ggreatest L top (carrier L)" ..
3.1108 - fix A
3.1109 - assume L: "A \<subseteq> carrier L"
3.1110 - let ?B = "Upper L A"
3.1111 - from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: ggreatest_le)
3.1112 - then have B_non_empty: "?B ~= {}" by fast
3.1113 - have B_L: "?B \<subseteq> carrier L" by simp
3.1114 - from ginf_exists [OF B_L B_non_empty]
3.1115 - obtain b where b_ginf_B: "ggreatest L b (Lower L ?B)" ..
3.1116 - have "gleast L b (Upper L A)"
3.1117 -apply (rule gleast_UpperI)
3.1118 - apply (rule ggreatest_le [where A = "Lower L ?B"])
3.1119 - apply (rule b_ginf_B)
3.1120 - apply (rule Lower_memI)
3.1121 - apply (erule Upper_memD [THEN conjunct1])
3.1122 - apply assumption
3.1123 - apply (rule L)
3.1124 - apply (fast intro: L [THEN subsetD])
3.1125 - apply (erule ggreatest_Lower_below [OF b_ginf_B])
3.1126 - apply simp
3.1127 - apply (rule L)
3.1128 -apply (rule ggreatest_closed [OF b_ginf_B])
3.1129 -done
3.1130 - then show "EX s. gleast L s (Upper L A)" ..
3.1131 -next
3.1132 - fix A
3.1133 - assume L: "A \<subseteq> carrier L"
3.1134 - show "EX i. ggreatest L i (Lower L A)"
3.1135 - proof (cases "A = {}")
3.1136 - case True then show ?thesis
3.1137 - by (simp add: top_exists)
3.1138 - next
3.1139 - case False with L show ?thesis
3.1140 - by (rule ginf_exists)
3.1141 - qed
3.1142 -qed
3.1143 -
3.1144 -(* TODO: prove dual version *)
3.1145 -
3.1146 -
3.1147 -subsection {* Examples *}
3.1148 -
3.1149 -(* Not so useful for the generalised version.
3.1150 -
3.1151 -subsubsection {* Powerset of a Set is a Complete Lattice *}
3.1152 -
3.1153 -theorem powerset_is_complete_lattice:
3.1154 - "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
3.1155 - (is "complete_lattice ?L")
3.1156 -proof (rule gpartial_order.complete_latticeI)
3.1157 - show "gpartial_order ?L"
3.1158 - by (rule gpartial_order.intro) auto
3.1159 -next
3.1160 - fix B
3.1161 - assume B: "B \<subseteq> carrier ?L"
3.1162 - show "EX s. gleast ?L s (Upper ?L B)"
3.1163 - proof
3.1164 - from B show "gleast ?L (\<Union> B) (Upper ?L B)"
3.1165 - by (fastsimp intro!: gleast_UpperI simp: Upper_def)
3.1166 - qed
3.1167 -next
3.1168 - fix B
3.1169 - assume B: "B \<subseteq> carrier ?L"
3.1170 - show "EX i. ggreatest ?L i (Lower ?L B)"
3.1171 - proof
3.1172 - from B show "ggreatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
3.1173 - txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
3.1174 - @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
3.1175 - by (fastsimp intro!: ggreatest_LowerI simp: Lower_def)
3.1176 - qed
3.1177 -qed
3.1178 -
3.1179 -text {* An other example, that of the lattice of subgroups of a group,
3.1180 - can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
3.1181 -
3.1182 -*)
3.1183 -
3.1184 -end
4.1 --- a/src/HOL/Algebra/Group.thy Wed Jul 30 16:07:00 2008 +0200
4.2 +++ b/src/HOL/Algebra/Group.thy Wed Jul 30 19:03:33 2008 +0200
4.3 @@ -712,8 +712,8 @@
4.4 text_raw {* \label{sec:subgroup-lattice} *}
4.5
4.6 theorem (in group) subgroups_partial_order:
4.7 - "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
4.8 - by (rule partial_order.intro) simp_all
4.9 + "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
4.10 + by unfold_locales simp_all
4.11
4.12 lemma (in group) subgroup_self:
4.13 "subgroup (carrier G) G"
4.14 @@ -757,7 +757,7 @@
4.15 qed
4.16
4.17 theorem (in group) subgroups_complete_lattice:
4.18 - "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
4.19 + "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
4.20 (is "complete_lattice ?L")
4.21 proof (rule partial_order.complete_lattice_criterion1)
4.22 show "partial_order ?L" by (rule subgroups_partial_order)
5.1 --- a/src/HOL/Algebra/IntRing.thy Wed Jul 30 16:07:00 2008 +0200
5.2 +++ b/src/HOL/Algebra/IntRing.thy Wed Jul 30 19:03:33 2008 +0200
5.3 @@ -208,27 +208,27 @@
5.4 by simp_all
5.5
5.6 interpretation int [unfolded UNIV]:
5.7 - partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
5.8 - where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
5.9 - and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
5.10 - and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
5.11 + partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
5.12 + where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
5.13 + and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
5.14 + and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
5.15 proof -
5.16 - show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
5.17 + show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
5.18 by unfold_locales simp_all
5.19 - show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
5.20 + show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
5.21 by simp
5.22 - show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
5.23 + show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
5.24 by simp
5.25 - show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
5.26 + show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
5.27 by (simp add: lless_def) auto
5.28 qed
5.29
5.30 interpretation int [unfolded UNIV]:
5.31 - lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
5.32 - where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
5.33 - and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
5.34 + lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
5.35 + where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
5.36 + and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
5.37 proof -
5.38 - let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
5.39 + let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
5.40 show "lattice ?Z"
5.41 apply unfold_locales
5.42 apply (simp add: least_def Upper_def)
5.43 @@ -250,7 +250,7 @@
5.44 qed
5.45
5.46 interpretation int [unfolded UNIV]:
5.47 - total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
5.48 + total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
5.49 by unfold_locales clarsimp
5.50
5.51
6.1 --- a/src/HOL/Algebra/Lattice.thy Wed Jul 30 16:07:00 2008 +0200
6.2 +++ b/src/HOL/Algebra/Lattice.thy Wed Jul 30 19:03:33 2008 +0200
6.3 @@ -1,5 +1,5 @@
6.4 (*
6.5 - Title: HOL/Algebra/Lattice.thy
6.6 + Title: HOL/Algebra/GLattice.thy
6.7 Id: $Id$
6.8 Author: Clemens Ballarin, started 7 November 2003
6.9 Copyright: Clemens Ballarin
6.10 @@ -7,88 +7,202 @@
6.11
6.12 theory Lattice imports Congruence begin
6.13
6.14 -
6.15 section {* Orders and Lattices *}
6.16
6.17 subsection {* Partial Orders *}
6.18
6.19 -record 'a order = "'a partial_object" +
6.20 +record 'a gorder = "'a eq_object" +
6.21 le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
6.22
6.23 -locale partial_order =
6.24 - fixes L (structure)
6.25 - assumes refl [intro, simp]:
6.26 - "x \<in> carrier L ==> x \<sqsubseteq> x"
6.27 - and anti_sym [intro]:
6.28 - "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
6.29 - and trans [trans]:
6.30 - "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
6.31 - x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
6.32 +locale weak_partial_order = equivalence L +
6.33 + assumes le_refl [intro, simp]:
6.34 + "x \<in> carrier L ==> x \<sqsubseteq> x"
6.35 + and weak_le_anti_sym [intro]:
6.36 + "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
6.37 + and le_trans [trans]:
6.38 + "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
6.39 + and le_cong:
6.40 + "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
6.41
6.42 constdefs (structure L)
6.43 lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
6.44 - "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
6.45 + "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
6.46
6.47 - -- {* Upper and lower bounds of a set. *}
6.48 +
6.49 +subsubsection {* The order relation *}
6.50 +
6.51 +context weak_partial_order begin
6.52 +
6.53 +lemma le_cong_l [intro, trans]:
6.54 + "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
6.55 + by (auto intro: le_cong [THEN iffD2])
6.56 +
6.57 +lemma le_cong_r [intro, trans]:
6.58 + "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
6.59 + by (auto intro: le_cong [THEN iffD1])
6.60 +
6.61 +lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
6.62 + by (simp add: le_cong_l)
6.63 +
6.64 +end
6.65 +
6.66 +lemma weak_llessI:
6.67 + fixes R (structure)
6.68 + assumes "x \<sqsubseteq> y" and "~(x .= y)"
6.69 + shows "x \<sqsubset> y"
6.70 + using assms unfolding lless_def by simp
6.71 +
6.72 +lemma lless_imp_le:
6.73 + fixes R (structure)
6.74 + assumes "x \<sqsubset> y"
6.75 + shows "x \<sqsubseteq> y"
6.76 + using assms unfolding lless_def by simp
6.77 +
6.78 +lemma weak_lless_imp_not_eq:
6.79 + fixes R (structure)
6.80 + assumes "x \<sqsubset> y"
6.81 + shows "\<not> (x .= y)"
6.82 + using assms unfolding lless_def by simp
6.83 +
6.84 +lemma weak_llessE:
6.85 + fixes R (structure)
6.86 + assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
6.87 + shows "P"
6.88 + using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
6.89 +
6.90 +lemma (in weak_partial_order) lless_cong_l [trans]:
6.91 + assumes xx': "x .= x'"
6.92 + and xy: "x' \<sqsubset> y"
6.93 + and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
6.94 + shows "x \<sqsubset> y"
6.95 + using assms unfolding lless_def by (auto intro: trans sym)
6.96 +
6.97 +lemma (in weak_partial_order) lless_cong_r [trans]:
6.98 + assumes xy: "x \<sqsubset> y"
6.99 + and yy': "y .= y'"
6.100 + and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
6.101 + shows "x \<sqsubset> y'"
6.102 + using assms unfolding lless_def by (auto intro: trans sym)
6.103 +
6.104 +
6.105 +lemma (in weak_partial_order) lless_antisym:
6.106 + assumes "a \<in> carrier L" "b \<in> carrier L"
6.107 + and "a \<sqsubset> b" "b \<sqsubset> a"
6.108 + shows "P"
6.109 + using assms
6.110 + by (elim weak_llessE) auto
6.111 +
6.112 +lemma (in weak_partial_order) lless_trans [trans]:
6.113 + assumes "a \<sqsubset> b" "b \<sqsubset> c"
6.114 + and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
6.115 + shows "a \<sqsubset> c"
6.116 + using assms unfolding lless_def by (blast dest: le_trans intro: sym)
6.117 +
6.118 +
6.119 +subsubsection {* Upper and lower bounds of a set *}
6.120 +
6.121 +constdefs (structure L)
6.122 Upper :: "[_, 'a set] => 'a set"
6.123 - "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>
6.124 - carrier L"
6.125 + "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
6.126
6.127 Lower :: "[_, 'a set] => 'a set"
6.128 - "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>
6.129 - carrier L"
6.130 + "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
6.131
6.132 - -- {* Least and greatest, as predicate. *}
6.133 - least :: "[_, 'a, 'a set] => bool"
6.134 - "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
6.135 -
6.136 - greatest :: "[_, 'a, 'a set] => bool"
6.137 - "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
6.138 -
6.139 - -- {* Supremum and infimum *}
6.140 - sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
6.141 - "\<Squnion>A == THE x. least L x (Upper L A)"
6.142 -
6.143 - inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
6.144 - "\<Sqinter>A == THE x. greatest L x (Lower L A)"
6.145 -
6.146 - join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
6.147 - "x \<squnion> y == sup L {x, y}"
6.148 -
6.149 - meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
6.150 - "x \<sqinter> y == inf L {x, y}"
6.151 -
6.152 -
6.153 -subsubsection {* Upper *}
6.154 -
6.155 -lemma Upper_closed [intro, simp]:
6.156 +lemma Upper_closed [intro!, simp]:
6.157 "Upper L A \<subseteq> carrier L"
6.158 by (unfold Upper_def) clarify
6.159
6.160 lemma Upper_memD [dest]:
6.161 fixes L (structure)
6.162 - shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
6.163 + shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
6.164 by (unfold Upper_def) blast
6.165
6.166 +lemma (in weak_partial_order) Upper_elemD [dest]:
6.167 + "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
6.168 + unfolding Upper_def elem_def
6.169 + by (blast dest: sym)
6.170 +
6.171 lemma Upper_memI:
6.172 fixes L (structure)
6.173 shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
6.174 by (unfold Upper_def) blast
6.175
6.176 +lemma (in weak_partial_order) Upper_elemI:
6.177 + "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
6.178 + unfolding Upper_def by blast
6.179 +
6.180 lemma Upper_antimono:
6.181 "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
6.182 by (unfold Upper_def) blast
6.183
6.184 +lemma (in weak_partial_order) Upper_is_closed [simp]:
6.185 + "A \<subseteq> carrier L ==> is_closed (Upper L A)"
6.186 + by (rule is_closedI) (blast intro: Upper_memI)+
6.187
6.188 -subsubsection {* Lower *}
6.189 +lemma (in weak_partial_order) Upper_mem_cong:
6.190 + assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
6.191 + and aa': "a .= a'"
6.192 + and aelem: "a \<in> Upper L A"
6.193 + shows "a' \<in> Upper L A"
6.194 +proof (rule Upper_memI[OF _ a'carr])
6.195 + fix y
6.196 + assume yA: "y \<in> A"
6.197 + hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
6.198 + also note aa'
6.199 + finally
6.200 + show "y \<sqsubseteq> a'"
6.201 + by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
6.202 +qed
6.203
6.204 -lemma Lower_closed [intro, simp]:
6.205 +lemma (in weak_partial_order) Upper_cong:
6.206 + assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
6.207 + and AA': "A {.=} A'"
6.208 + shows "Upper L A = Upper L A'"
6.209 +unfolding Upper_def
6.210 +apply rule
6.211 + apply (rule, clarsimp) defer 1
6.212 + apply (rule, clarsimp) defer 1
6.213 +proof -
6.214 + fix x a'
6.215 + assume carr: "x \<in> carrier L" "a' \<in> carrier L"
6.216 + and a'A': "a' \<in> A'"
6.217 + assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
6.218 +
6.219 + from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
6.220 + from this obtain a
6.221 + where aA: "a \<in> A"
6.222 + and a'a: "a' .= a"
6.223 + by auto
6.224 + note [simp] = subsetD[OF Acarr aA] carr
6.225 +
6.226 + note a'a
6.227 + also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
6.228 + finally show "a' \<sqsubseteq> x" by simp
6.229 +next
6.230 + fix x a
6.231 + assume carr: "x \<in> carrier L" "a \<in> carrier L"
6.232 + and aA: "a \<in> A"
6.233 + assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
6.234 +
6.235 + from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
6.236 + from this obtain a'
6.237 + where a'A': "a' \<in> A'"
6.238 + and aa': "a .= a'"
6.239 + by auto
6.240 + note [simp] = subsetD[OF A'carr a'A'] carr
6.241 +
6.242 + note aa'
6.243 + also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
6.244 + finally show "a \<sqsubseteq> x" by simp
6.245 +qed
6.246 +
6.247 +lemma Lower_closed [intro!, simp]:
6.248 "Lower L A \<subseteq> carrier L"
6.249 by (unfold Lower_def) clarify
6.250
6.251 lemma Lower_memD [dest]:
6.252 fixes L (structure)
6.253 - shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
6.254 + shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
6.255 by (unfold Lower_def) blast
6.256
6.257 lemma Lower_memI:
6.258 @@ -100,19 +214,86 @@
6.259 "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
6.260 by (unfold Lower_def) blast
6.261
6.262 +lemma (in weak_partial_order) Lower_is_closed [simp]:
6.263 + "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
6.264 + by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
6.265
6.266 -subsubsection {* least *}
6.267 +lemma (in weak_partial_order) Lower_mem_cong:
6.268 + assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
6.269 + and aa': "a .= a'"
6.270 + and aelem: "a \<in> Lower L A"
6.271 + shows "a' \<in> Lower L A"
6.272 +using assms Lower_closed[of L A]
6.273 +by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
6.274 +
6.275 +lemma (in weak_partial_order) Lower_cong:
6.276 + assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
6.277 + and AA': "A {.=} A'"
6.278 + shows "Lower L A = Lower L A'"
6.279 +using Lower_memD[of y]
6.280 +unfolding Lower_def
6.281 +apply safe
6.282 + apply clarsimp defer 1
6.283 + apply clarsimp defer 1
6.284 +proof -
6.285 + fix x a'
6.286 + assume carr: "x \<in> carrier L" "a' \<in> carrier L"
6.287 + and a'A': "a' \<in> A'"
6.288 + assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
6.289 + hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
6.290 +
6.291 + from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
6.292 + from this obtain a
6.293 + where aA: "a \<in> A"
6.294 + and a'a: "a' .= a"
6.295 + by auto
6.296 +
6.297 + from aA and subsetD[OF Acarr aA]
6.298 + have "x \<sqsubseteq> a" by (rule aLxCond)
6.299 + also note a'a[symmetric]
6.300 + finally
6.301 + show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
6.302 +next
6.303 + fix x a
6.304 + assume carr: "x \<in> carrier L" "a \<in> carrier L"
6.305 + and aA: "a \<in> A"
6.306 + assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
6.307 + hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
6.308 +
6.309 + from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
6.310 + from this obtain a'
6.311 + where a'A': "a' \<in> A'"
6.312 + and aa': "a .= a'"
6.313 + by auto
6.314 + from a'A' and subsetD[OF A'carr a'A']
6.315 + have "x \<sqsubseteq> a'" by (rule a'LxCond)
6.316 + also note aa'[symmetric]
6.317 + finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
6.318 +qed
6.319 +
6.320 +
6.321 +subsubsection {* Least and greatest, as predicate *}
6.322 +
6.323 +constdefs (structure L)
6.324 + least :: "[_, 'a, 'a set] => bool"
6.325 + "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
6.326 +
6.327 + greatest :: "[_, 'a, 'a set] => bool"
6.328 + "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
6.329 +
6.330 +text {* Could weaken these to @{term [locale=weak_partial_order] "l \<in> carrier L \<and> l
6.331 + .\<in> A"} and @{term [locale=weak_partial_order] "g \<in> carrier L \<and> g .\<in> A"}. *}
6.332
6.333 lemma least_closed [intro, simp]:
6.334 - shows "least L l A ==> l \<in> carrier L"
6.335 + "least L l A ==> l \<in> carrier L"
6.336 by (unfold least_def) fast
6.337
6.338 lemma least_mem:
6.339 "least L l A ==> l \<in> A"
6.340 by (unfold least_def) fast
6.341
6.342 -lemma (in partial_order) least_unique:
6.343 - "[| least L x A; least L y A |] ==> x = y"
6.344 +lemma (in weak_partial_order) weak_least_unique:
6.345 + "[| least L x A; least L y A |] ==> x .= y"
6.346 by (unfold least_def) blast
6.347
6.348 lemma least_le:
6.349 @@ -120,6 +301,27 @@
6.350 shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
6.351 by (unfold least_def) fast
6.352
6.353 +lemma (in weak_partial_order) least_cong:
6.354 + "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
6.355 + by (unfold least_def) (auto dest: sym)
6.356 +
6.357 +text {* @{const least} is not congruent in the second parameter for
6.358 + @{term [locale=weak_partial_order] "A {.=} A'"} *}
6.359 +
6.360 +lemma (in weak_partial_order) least_Upper_cong_l:
6.361 + assumes "x .= x'"
6.362 + and "x \<in> carrier L" "x' \<in> carrier L"
6.363 + and "A \<subseteq> carrier L"
6.364 + shows "least L x (Upper L A) = least L x' (Upper L A)"
6.365 + apply (rule least_cong) using assms by auto
6.366 +
6.367 +lemma (in weak_partial_order) least_Upper_cong_r:
6.368 + assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
6.369 + and AA': "A {.=} A'"
6.370 + shows "least L x (Upper L A) = least L x (Upper L A')"
6.371 +apply (subgoal_tac "Upper L A = Upper L A'", simp)
6.372 +by (rule Upper_cong) fact+
6.373 +
6.374 lemma least_UpperI:
6.375 fixes L (structure)
6.376 assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
6.377 @@ -133,19 +335,21 @@
6.378 ultimately show ?thesis by (simp add: least_def)
6.379 qed
6.380
6.381 -
6.382 -subsubsection {* greatest *}
6.383 +lemma least_Upper_above:
6.384 + fixes L (structure)
6.385 + shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
6.386 + by (unfold least_def) blast
6.387
6.388 lemma greatest_closed [intro, simp]:
6.389 - shows "greatest L l A ==> l \<in> carrier L"
6.390 + "greatest L l A ==> l \<in> carrier L"
6.391 by (unfold greatest_def) fast
6.392
6.393 lemma greatest_mem:
6.394 "greatest L l A ==> l \<in> A"
6.395 by (unfold greatest_def) fast
6.396
6.397 -lemma (in partial_order) greatest_unique:
6.398 - "[| greatest L x A; greatest L y A |] ==> x = y"
6.399 +lemma (in weak_partial_order) weak_greatest_unique:
6.400 + "[| greatest L x A; greatest L y A |] ==> x .= y"
6.401 by (unfold greatest_def) blast
6.402
6.403 lemma greatest_le:
6.404 @@ -153,6 +357,28 @@
6.405 shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
6.406 by (unfold greatest_def) fast
6.407
6.408 +lemma (in weak_partial_order) greatest_cong:
6.409 + "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
6.410 + greatest L x A = greatest L x' A"
6.411 + by (unfold greatest_def) (auto dest: sym)
6.412 +
6.413 +text {* @{const greatest} is not congruent in the second parameter for
6.414 + @{term [locale=weak_partial_order] "A {.=} A'"} *}
6.415 +
6.416 +lemma (in weak_partial_order) greatest_Lower_cong_l:
6.417 + assumes "x .= x'"
6.418 + and "x \<in> carrier L" "x' \<in> carrier L"
6.419 + and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
6.420 + shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
6.421 + apply (rule greatest_cong) using assms by auto
6.422 +
6.423 +lemma (in weak_partial_order) greatest_Lower_cong_r:
6.424 + assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
6.425 + and AA': "A {.=} A'"
6.426 + shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
6.427 +apply (subgoal_tac "Lower L A = Lower L A'", simp)
6.428 +by (rule Lower_cong) fact+
6.429 +
6.430 lemma greatest_LowerI:
6.431 fixes L (structure)
6.432 assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
6.433 @@ -166,55 +392,116 @@
6.434 ultimately show ?thesis by (simp add: greatest_def)
6.435 qed
6.436
6.437 -
6.438 -subsection {* Lattices *}
6.439 -
6.440 -locale lattice = partial_order +
6.441 - assumes sup_of_two_exists:
6.442 - "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
6.443 - and inf_of_two_exists:
6.444 - "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
6.445 -
6.446 -lemma least_Upper_above:
6.447 - fixes L (structure)
6.448 - shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
6.449 - by (unfold least_def) blast
6.450 -
6.451 lemma greatest_Lower_below:
6.452 fixes L (structure)
6.453 shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
6.454 by (unfold greatest_def) blast
6.455
6.456 +text {* Supremum and infimum *}
6.457 +
6.458 +constdefs (structure L)
6.459 + sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
6.460 + "\<Squnion>A == SOME x. least L x (Upper L A)"
6.461 +
6.462 + inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
6.463 + "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
6.464 +
6.465 + join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
6.466 + "x \<squnion> y == \<Squnion> {x, y}"
6.467 +
6.468 + meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
6.469 + "x \<sqinter> y == \<Sqinter> {x, y}"
6.470 +
6.471 +
6.472 +subsection {* Lattices *}
6.473 +
6.474 +locale weak_upper_semilattice = weak_partial_order +
6.475 + assumes sup_of_two_exists:
6.476 + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
6.477 +
6.478 +locale weak_lower_semilattice = weak_partial_order +
6.479 + assumes inf_of_two_exists:
6.480 + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
6.481 +
6.482 +locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
6.483 +
6.484
6.485 subsubsection {* Supremum *}
6.486
6.487 -lemma (in lattice) joinI:
6.488 +lemma (in weak_upper_semilattice) joinI:
6.489 "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
6.490 ==> P (x \<squnion> y)"
6.491 proof (unfold join_def sup_def)
6.492 assume L: "x \<in> carrier L" "y \<in> carrier L"
6.493 and P: "!!l. least L l (Upper L {x, y}) ==> P l"
6.494 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
6.495 - with L show "P (THE l. least L l (Upper L {x, y}))"
6.496 - by (fast intro: theI2 least_unique P)
6.497 + with L show "P (SOME l. least L l (Upper L {x, y}))"
6.498 + by (fast intro: someI2 P)
6.499 qed
6.500
6.501 -lemma (in lattice) join_closed [simp]:
6.502 +lemma (in weak_upper_semilattice) join_closed [simp]:
6.503 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
6.504 by (rule joinI) (rule least_closed)
6.505
6.506 -lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *)
6.507 +lemma (in weak_upper_semilattice) join_cong_l:
6.508 + assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
6.509 + and xx': "x .= x'"
6.510 + shows "x \<squnion> y .= x' \<squnion> y"
6.511 +proof (rule joinI, rule joinI)
6.512 + fix a b
6.513 + from xx' carr
6.514 + have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
6.515 +
6.516 + assume leasta: "least L a (Upper L {x, y})"
6.517 + assume "least L b (Upper L {x', y})"
6.518 + with carr
6.519 + have leastb: "least L b (Upper L {x, y})"
6.520 + by (simp add: least_Upper_cong_r[OF _ _ seq])
6.521 +
6.522 + from leasta leastb
6.523 + show "a .= b" by (rule weak_least_unique)
6.524 +qed (rule carr)+
6.525 +
6.526 +lemma (in weak_upper_semilattice) join_cong_r:
6.527 + assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
6.528 + and yy': "y .= y'"
6.529 + shows "x \<squnion> y .= x \<squnion> y'"
6.530 +proof (rule joinI, rule joinI)
6.531 + fix a b
6.532 + have "{x, y} = {y, x}" by fast
6.533 + also from carr yy'
6.534 + have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
6.535 + also have "{y', x} = {x, y'}" by fast
6.536 + finally
6.537 + have seq: "{x, y} {.=} {x, y'}" .
6.538 +
6.539 + assume leasta: "least L a (Upper L {x, y})"
6.540 + assume "least L b (Upper L {x, y'})"
6.541 + with carr
6.542 + have leastb: "least L b (Upper L {x, y})"
6.543 + by (simp add: least_Upper_cong_r[OF _ _ seq])
6.544 +
6.545 + from leasta leastb
6.546 + show "a .= b" by (rule weak_least_unique)
6.547 +qed (rule carr)+
6.548 +
6.549 +lemma (in weak_partial_order) sup_of_singletonI: (* only reflexivity needed ? *)
6.550 "x \<in> carrier L ==> least L x (Upper L {x})"
6.551 - by (rule least_UpperI) fast+
6.552 + by (rule least_UpperI) auto
6.553
6.554 -lemma (in partial_order) sup_of_singleton [simp]:
6.555 - "x \<in> carrier L ==> \<Squnion>{x} = x"
6.556 - by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
6.557 +lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
6.558 + "x \<in> carrier L ==> \<Squnion>{x} .= x"
6.559 + unfolding sup_def
6.560 + by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
6.561
6.562 +lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
6.563 + "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
6.564 + unfolding sup_def
6.565 + by (rule someI2) (auto intro: sup_of_singletonI)
6.566
6.567 text {* Condition on @{text A}: supremum exists. *}
6.568
6.569 -lemma (in lattice) sup_insertI:
6.570 +lemma (in weak_upper_semilattice) sup_insertI:
6.571 "[| !!s. least L s (Upper L (insert x A)) ==> P s;
6.572 least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
6.573 ==> P (\<Squnion>(insert x A))"
6.574 @@ -225,8 +512,8 @@
6.575 from L least_a have La: "a \<in> carrier L" by simp
6.576 from L sup_of_two_exists least_a
6.577 obtain s where least_s: "least L s (Upper L {a, x})" by blast
6.578 - show "P (THE l. least L l (Upper L (insert x A)))"
6.579 - proof (rule theI2)
6.580 + show "P (SOME l. least L l (Upper L (insert x A)))"
6.581 + proof (rule someI2)
6.582 show "least L s (Upper L (insert x A))"
6.583 proof (rule least_UpperI)
6.584 fix z
6.585 @@ -238,7 +525,7 @@
6.586 next
6.587 assume "z \<in> A"
6.588 with L least_s least_a show ?thesis
6.589 - by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
6.590 + by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
6.591 qed
6.592 next
6.593 fix y
6.594 @@ -266,55 +553,10 @@
6.595 from L show "insert x A \<subseteq> carrier L" by simp
6.596 from least_s show "s \<in> carrier L" by simp
6.597 qed
6.598 - next
6.599 - fix l
6.600 - assume least_l: "least L l (Upper L (insert x A))"
6.601 - show "l = s"
6.602 - proof (rule least_unique)
6.603 - show "least L s (Upper L (insert x A))"
6.604 - proof (rule least_UpperI)
6.605 - fix z
6.606 - assume "z \<in> insert x A"
6.607 - then show "z \<sqsubseteq> s"
6.608 - proof
6.609 - assume "z = x" then show ?thesis
6.610 - by (simp add: least_Upper_above [OF least_s] L La)
6.611 - next
6.612 - assume "z \<in> A"
6.613 - with L least_s least_a show ?thesis
6.614 - by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
6.615 - qed
6.616 - next
6.617 - fix y
6.618 - assume y: "y \<in> Upper L (insert x A)"
6.619 - show "s \<sqsubseteq> y"
6.620 - proof (rule least_le [OF least_s], rule Upper_memI)
6.621 - fix z
6.622 - assume z: "z \<in> {a, x}"
6.623 - then show "z \<sqsubseteq> y"
6.624 - proof
6.625 - have y': "y \<in> Upper L A"
6.626 - apply (rule subsetD [where A = "Upper L (insert x A)"])
6.627 - apply (rule Upper_antimono)
6.628 - apply blast
6.629 - apply (rule y)
6.630 - done
6.631 - assume "z = a"
6.632 - with y' least_a show ?thesis by (fast dest: least_le)
6.633 - next
6.634 - assume "z \<in> {x}"
6.635 - with y L show ?thesis by blast
6.636 - qed
6.637 - qed (rule Upper_closed [THEN subsetD, OF y])
6.638 - next
6.639 - from L show "insert x A \<subseteq> carrier L" by simp
6.640 - from least_s show "s \<in> carrier L" by simp
6.641 - qed
6.642 - qed (rule least_l)
6.643 qed (rule P)
6.644 qed
6.645
6.646 -lemma (in lattice) finite_sup_least:
6.647 +lemma (in weak_upper_semilattice) finite_sup_least:
6.648 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
6.649 proof (induct set: finite)
6.650 case empty
6.651 @@ -324,7 +566,11 @@
6.652 show ?case
6.653 proof (cases "A = {}")
6.654 case True
6.655 - with insert show ?thesis by (simp add: sup_of_singletonI)
6.656 + with insert show ?thesis
6.657 + by simp (simp add: least_cong [OF weak_sup_of_singleton]
6.658 + sup_of_singleton_closed sup_of_singletonI)
6.659 + (* The above step is hairy; least_cong can make simp loop.
6.660 + Would want special version of simp to apply least_cong. *)
6.661 next
6.662 case False
6.663 with insert have "least L (\<Squnion>A) (Upper L A)" by simp
6.664 @@ -333,19 +579,19 @@
6.665 qed
6.666 qed
6.667
6.668 -lemma (in lattice) finite_sup_insertI:
6.669 +lemma (in weak_upper_semilattice) finite_sup_insertI:
6.670 assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
6.671 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"
6.672 shows "P (\<Squnion> (insert x A))"
6.673 proof (cases "A = {}")
6.674 case True with P and xA show ?thesis
6.675 - by (simp add: sup_of_singletonI)
6.676 + by (simp add: finite_sup_least)
6.677 next
6.678 case False with P and xA show ?thesis
6.679 by (simp add: sup_insertI finite_sup_least)
6.680 qed
6.681
6.682 -lemma (in lattice) finite_sup_closed:
6.683 +lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
6.684 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
6.685 proof (induct set: finite)
6.686 case empty then show ?case by simp
6.687 @@ -354,24 +600,24 @@
6.688 by - (rule finite_sup_insertI, simp_all)
6.689 qed
6.690
6.691 -lemma (in lattice) join_left:
6.692 +lemma (in weak_upper_semilattice) join_left:
6.693 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
6.694 by (rule joinI [folded join_def]) (blast dest: least_mem)
6.695
6.696 -lemma (in lattice) join_right:
6.697 +lemma (in weak_upper_semilattice) join_right:
6.698 "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
6.699 by (rule joinI [folded join_def]) (blast dest: least_mem)
6.700
6.701 -lemma (in lattice) sup_of_two_least:
6.702 +lemma (in weak_upper_semilattice) sup_of_two_least:
6.703 "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
6.704 proof (unfold sup_def)
6.705 assume L: "x \<in> carrier L" "y \<in> carrier L"
6.706 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
6.707 - with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"
6.708 - by (fast intro: theI2 least_unique) (* blast fails *)
6.709 + with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
6.710 + by (fast intro: someI2 weak_least_unique) (* blast fails *)
6.711 qed
6.712
6.713 -lemma (in lattice) join_le:
6.714 +lemma (in weak_upper_semilattice) join_le:
6.715 assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z"
6.716 and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
6.717 shows "x \<squnion> y \<sqsubseteq> z"
6.718 @@ -381,44 +627,48 @@
6.719 with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
6.720 qed
6.721
6.722 -lemma (in lattice) join_assoc_lemma:
6.723 +lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
6.724 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
6.725 - shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
6.726 + shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
6.727 proof (rule finite_sup_insertI)
6.728 -- {* The textbook argument in Jacobson I, p 457 *}
6.729 fix s
6.730 assume sup: "least L s (Upper L {x, y, z})"
6.731 - show "x \<squnion> (y \<squnion> z) = s"
6.732 - proof (rule anti_sym)
6.733 + show "x \<squnion> (y \<squnion> z) .= s"
6.734 + proof (rule weak_le_anti_sym)
6.735 from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
6.736 by (fastsimp intro!: join_le elim: least_Upper_above)
6.737 next
6.738 from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
6.739 by (erule_tac least_le)
6.740 - (blast intro!: Upper_memI intro: trans join_left join_right join_closed)
6.741 + (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
6.742 qed (simp_all add: L least_closed [OF sup])
6.743 qed (simp_all add: L)
6.744
6.745 +text {* Commutativity holds for @{text "="}. *}
6.746 +
6.747 lemma join_comm:
6.748 fixes L (structure)
6.749 shows "x \<squnion> y = y \<squnion> x"
6.750 by (unfold join_def) (simp add: insert_commute)
6.751
6.752 -lemma (in lattice) join_assoc:
6.753 +lemma (in weak_upper_semilattice) weak_join_assoc:
6.754 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
6.755 - shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
6.756 + shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
6.757 proof -
6.758 + (* FIXME: could be simplified by improved simp: uniform use of .=,
6.759 + omit [symmetric] in last step. *)
6.760 have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
6.761 - also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma)
6.762 + also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
6.763 also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
6.764 - also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma)
6.765 - finally show ?thesis .
6.766 + also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
6.767 + finally show ?thesis by (simp add: L)
6.768 qed
6.769
6.770
6.771 subsubsection {* Infimum *}
6.772
6.773 -lemma (in lattice) meetI:
6.774 +lemma (in weak_lower_semilattice) meetI:
6.775 "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
6.776 x \<in> carrier L; y \<in> carrier L |]
6.777 ==> P (x \<sqinter> y)"
6.778 @@ -426,25 +676,73 @@
6.779 assume L: "x \<in> carrier L" "y \<in> carrier L"
6.780 and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
6.781 with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
6.782 - with L show "P (THE g. greatest L g (Lower L {x, y}))"
6.783 - by (fast intro: theI2 greatest_unique P)
6.784 + with L show "P (SOME g. greatest L g (Lower L {x, y}))"
6.785 + by (fast intro: someI2 weak_greatest_unique P)
6.786 qed
6.787
6.788 -lemma (in lattice) meet_closed [simp]:
6.789 +lemma (in weak_lower_semilattice) meet_closed [simp]:
6.790 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
6.791 by (rule meetI) (rule greatest_closed)
6.792
6.793 -lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *)
6.794 +lemma (in weak_lower_semilattice) meet_cong_l:
6.795 + assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
6.796 + and xx': "x .= x'"
6.797 + shows "x \<sqinter> y .= x' \<sqinter> y"
6.798 +proof (rule meetI, rule meetI)
6.799 + fix a b
6.800 + from xx' carr
6.801 + have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
6.802 +
6.803 + assume greatesta: "greatest L a (Lower L {x, y})"
6.804 + assume "greatest L b (Lower L {x', y})"
6.805 + with carr
6.806 + have greatestb: "greatest L b (Lower L {x, y})"
6.807 + by (simp add: greatest_Lower_cong_r[OF _ _ seq])
6.808 +
6.809 + from greatesta greatestb
6.810 + show "a .= b" by (rule weak_greatest_unique)
6.811 +qed (rule carr)+
6.812 +
6.813 +lemma (in weak_lower_semilattice) meet_cong_r:
6.814 + assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
6.815 + and yy': "y .= y'"
6.816 + shows "x \<sqinter> y .= x \<sqinter> y'"
6.817 +proof (rule meetI, rule meetI)
6.818 + fix a b
6.819 + have "{x, y} = {y, x}" by fast
6.820 + also from carr yy'
6.821 + have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
6.822 + also have "{y', x} = {x, y'}" by fast
6.823 + finally
6.824 + have seq: "{x, y} {.=} {x, y'}" .
6.825 +
6.826 + assume greatesta: "greatest L a (Lower L {x, y})"
6.827 + assume "greatest L b (Lower L {x, y'})"
6.828 + with carr
6.829 + have greatestb: "greatest L b (Lower L {x, y})"
6.830 + by (simp add: greatest_Lower_cong_r[OF _ _ seq])
6.831 +
6.832 + from greatesta greatestb
6.833 + show "a .= b" by (rule weak_greatest_unique)
6.834 +qed (rule carr)+
6.835 +
6.836 +lemma (in weak_partial_order) inf_of_singletonI: (* only reflexivity needed ? *)
6.837 "x \<in> carrier L ==> greatest L x (Lower L {x})"
6.838 - by (rule greatest_LowerI) fast+
6.839 + by (rule greatest_LowerI) auto
6.840
6.841 -lemma (in partial_order) inf_of_singleton [simp]:
6.842 - "x \<in> carrier L ==> \<Sqinter> {x} = x"
6.843 - by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
6.844 +lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
6.845 + "x \<in> carrier L ==> \<Sqinter>{x} .= x"
6.846 + unfolding inf_def
6.847 + by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
6.848
6.849 -text {* Condition on A: infimum exists. *}
6.850 +lemma (in weak_partial_order) inf_of_singleton_closed:
6.851 + "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
6.852 + unfolding inf_def
6.853 + by (rule someI2) (auto intro: inf_of_singletonI)
6.854
6.855 -lemma (in lattice) inf_insertI:
6.856 +text {* Condition on @{text A}: infimum exists. *}
6.857 +
6.858 +lemma (in weak_lower_semilattice) inf_insertI:
6.859 "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
6.860 greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
6.861 ==> P (\<Sqinter>(insert x A))"
6.862 @@ -455,8 +753,8 @@
6.863 from L greatest_a have La: "a \<in> carrier L" by simp
6.864 from L inf_of_two_exists greatest_a
6.865 obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
6.866 - show "P (THE g. greatest L g (Lower L (insert x A)))"
6.867 - proof (rule theI2)
6.868 + show "P (SOME g. greatest L g (Lower L (insert x A)))"
6.869 + proof (rule someI2)
6.870 show "greatest L i (Lower L (insert x A))"
6.871 proof (rule greatest_LowerI)
6.872 fix z
6.873 @@ -468,7 +766,7 @@
6.874 next
6.875 assume "z \<in> A"
6.876 with L greatest_i greatest_a show ?thesis
6.877 - by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below)
6.878 + by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
6.879 qed
6.880 next
6.881 fix y
6.882 @@ -496,55 +794,10 @@
6.883 from L show "insert x A \<subseteq> carrier L" by simp
6.884 from greatest_i show "i \<in> carrier L" by simp
6.885 qed
6.886 - next
6.887 - fix g
6.888 - assume greatest_g: "greatest L g (Lower L (insert x A))"
6.889 - show "g = i"
6.890 - proof (rule greatest_unique)
6.891 - show "greatest L i (Lower L (insert x A))"
6.892 - proof (rule greatest_LowerI)
6.893 - fix z
6.894 - assume "z \<in> insert x A"
6.895 - then show "i \<sqsubseteq> z"
6.896 - proof
6.897 - assume "z = x" then show ?thesis
6.898 - by (simp add: greatest_Lower_below [OF greatest_i] L La)
6.899 - next
6.900 - assume "z \<in> A"
6.901 - with L greatest_i greatest_a show ?thesis
6.902 - by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below)
6.903 - qed
6.904 - next
6.905 - fix y
6.906 - assume y: "y \<in> Lower L (insert x A)"
6.907 - show "y \<sqsubseteq> i"
6.908 - proof (rule greatest_le [OF greatest_i], rule Lower_memI)
6.909 - fix z
6.910 - assume z: "z \<in> {a, x}"
6.911 - then show "y \<sqsubseteq> z"
6.912 - proof
6.913 - have y': "y \<in> Lower L A"
6.914 - apply (rule subsetD [where A = "Lower L (insert x A)"])
6.915 - apply (rule Lower_antimono)
6.916 - apply blast
6.917 - apply (rule y)
6.918 - done
6.919 - assume "z = a"
6.920 - with y' greatest_a show ?thesis by (fast dest: greatest_le)
6.921 - next
6.922 - assume "z \<in> {x}"
6.923 - with y L show ?thesis by blast
6.924 - qed
6.925 - qed (rule Lower_closed [THEN subsetD, OF y])
6.926 - next
6.927 - from L show "insert x A \<subseteq> carrier L" by simp
6.928 - from greatest_i show "i \<in> carrier L" by simp
6.929 - qed
6.930 - qed (rule greatest_g)
6.931 qed (rule P)
6.932 qed
6.933
6.934 -lemma (in lattice) finite_inf_greatest:
6.935 +lemma (in weak_lower_semilattice) finite_inf_greatest:
6.936 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
6.937 proof (induct set: finite)
6.938 case empty then show ?case by simp
6.939 @@ -553,7 +806,9 @@
6.940 show ?case
6.941 proof (cases "A = {}")
6.942 case True
6.943 - with insert show ?thesis by (simp add: inf_of_singletonI)
6.944 + with insert show ?thesis
6.945 + by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
6.946 + inf_of_singleton_closed inf_of_singletonI)
6.947 next
6.948 case False
6.949 from insert show ?thesis
6.950 @@ -563,19 +818,19 @@
6.951 qed
6.952 qed
6.953
6.954 -lemma (in lattice) finite_inf_insertI:
6.955 +lemma (in weak_lower_semilattice) finite_inf_insertI:
6.956 assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
6.957 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"
6.958 shows "P (\<Sqinter> (insert x A))"
6.959 proof (cases "A = {}")
6.960 case True with P and xA show ?thesis
6.961 - by (simp add: inf_of_singletonI)
6.962 + by (simp add: finite_inf_greatest)
6.963 next
6.964 case False with P and xA show ?thesis
6.965 by (simp add: inf_insertI finite_inf_greatest)
6.966 qed
6.967
6.968 -lemma (in lattice) finite_inf_closed:
6.969 +lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
6.970 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
6.971 proof (induct set: finite)
6.972 case empty then show ?case by simp
6.973 @@ -584,26 +839,26 @@
6.974 by (rule_tac finite_inf_insertI) (simp_all)
6.975 qed
6.976
6.977 -lemma (in lattice) meet_left:
6.978 +lemma (in weak_lower_semilattice) meet_left:
6.979 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
6.980 by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
6.981
6.982 -lemma (in lattice) meet_right:
6.983 +lemma (in weak_lower_semilattice) meet_right:
6.984 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
6.985 by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
6.986
6.987 -lemma (in lattice) inf_of_two_greatest:
6.988 +lemma (in weak_lower_semilattice) inf_of_two_greatest:
6.989 "[| x \<in> carrier L; y \<in> carrier L |] ==>
6.990 greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
6.991 proof (unfold inf_def)
6.992 assume L: "x \<in> carrier L" "y \<in> carrier L"
6.993 with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
6.994 with L
6.995 - show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"
6.996 - by (fast intro: theI2 greatest_unique) (* blast fails *)
6.997 + show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
6.998 + by (fast intro: someI2 weak_greatest_unique) (* blast fails *)
6.999 qed
6.1000
6.1001 -lemma (in lattice) meet_le:
6.1002 +lemma (in weak_lower_semilattice) meet_le:
6.1003 assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y"
6.1004 and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
6.1005 shows "z \<sqsubseteq> x \<sqinter> y"
6.1006 @@ -613,21 +868,21 @@
6.1007 with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
6.1008 qed
6.1009
6.1010 -lemma (in lattice) meet_assoc_lemma:
6.1011 +lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
6.1012 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
6.1013 - shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
6.1014 + shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
6.1015 proof (rule finite_inf_insertI)
6.1016 txt {* The textbook argument in Jacobson I, p 457 *}
6.1017 fix i
6.1018 assume inf: "greatest L i (Lower L {x, y, z})"
6.1019 - show "x \<sqinter> (y \<sqinter> z) = i"
6.1020 - proof (rule anti_sym)
6.1021 + show "x \<sqinter> (y \<sqinter> z) .= i"
6.1022 + proof (rule weak_le_anti_sym)
6.1023 from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
6.1024 by (fastsimp intro!: meet_le elim: greatest_Lower_below)
6.1025 next
6.1026 from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
6.1027 by (erule_tac greatest_le)
6.1028 - (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)
6.1029 + (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
6.1030 qed (simp_all add: L greatest_closed [OF inf])
6.1031 qed (simp_all add: L)
6.1032
6.1033 @@ -636,33 +891,34 @@
6.1034 shows "x \<sqinter> y = y \<sqinter> x"
6.1035 by (unfold meet_def) (simp add: insert_commute)
6.1036
6.1037 -lemma (in lattice) meet_assoc:
6.1038 +lemma (in weak_lower_semilattice) weak_meet_assoc:
6.1039 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
6.1040 - shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
6.1041 + shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
6.1042 proof -
6.1043 + (* FIXME: improved simp, see weak_join_assoc above *)
6.1044 have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
6.1045 - also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma)
6.1046 + also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
6.1047 also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
6.1048 - also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma)
6.1049 - finally show ?thesis .
6.1050 + also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
6.1051 + finally show ?thesis by (simp add: L)
6.1052 qed
6.1053
6.1054
6.1055 subsection {* Total Orders *}
6.1056
6.1057 -locale total_order = partial_order +
6.1058 +locale weak_total_order = weak_partial_order +
6.1059 assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
6.1060
6.1061 text {* Introduction rule: the usual definition of total order *}
6.1062
6.1063 -lemma (in partial_order) total_orderI:
6.1064 +lemma (in weak_partial_order) weak_total_orderI:
6.1065 assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
6.1066 - shows "total_order L"
6.1067 + shows "weak_total_order L"
6.1068 by unfold_locales (rule total)
6.1069
6.1070 text {* Total orders are lattices. *}
6.1071
6.1072 -interpretation total_order < lattice
6.1073 +interpretation weak_total_order < weak_lattice
6.1074 proof unfold_locales
6.1075 fix x y
6.1076 assume L: "x \<in> carrier L" "y \<in> carrier L"
6.1077 @@ -708,7 +964,7 @@
6.1078
6.1079 subsection {* Complete lattices *}
6.1080
6.1081 -locale complete_lattice = lattice +
6.1082 +locale weak_complete_lattice = weak_lattice +
6.1083 assumes sup_exists:
6.1084 "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
6.1085 and inf_exists:
6.1086 @@ -716,16 +972,13 @@
6.1087
6.1088 text {* Introduction rule: the usual definition of complete lattice *}
6.1089
6.1090 -lemma (in partial_order) complete_latticeI:
6.1091 +lemma (in weak_partial_order) weak_complete_latticeI:
6.1092 assumes sup_exists:
6.1093 "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
6.1094 and inf_exists:
6.1095 "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
6.1096 - shows "complete_lattice L"
6.1097 -proof intro_locales
6.1098 - show "lattice_axioms L"
6.1099 - by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
6.1100 -qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+
6.1101 + shows "weak_complete_lattice L"
6.1102 + by unfold_locales (auto intro: sup_exists inf_exists)
6.1103
6.1104 constdefs (structure L)
6.1105 top :: "_ => 'a" ("\<top>\<index>")
6.1106 @@ -735,41 +988,41 @@
6.1107 "\<bottom> == inf L (carrier L)"
6.1108
6.1109
6.1110 -lemma (in complete_lattice) supI:
6.1111 +lemma (in weak_complete_lattice) supI:
6.1112 "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
6.1113 ==> P (\<Squnion>A)"
6.1114 proof (unfold sup_def)
6.1115 assume L: "A \<subseteq> carrier L"
6.1116 and P: "!!l. least L l (Upper L A) ==> P l"
6.1117 with sup_exists obtain s where "least L s (Upper L A)" by blast
6.1118 - with L show "P (THE l. least L l (Upper L A))"
6.1119 - by (fast intro: theI2 least_unique P)
6.1120 + with L show "P (SOME l. least L l (Upper L A))"
6.1121 + by (fast intro: someI2 weak_least_unique P)
6.1122 qed
6.1123
6.1124 -lemma (in complete_lattice) sup_closed [simp]:
6.1125 +lemma (in weak_complete_lattice) sup_closed [simp]:
6.1126 "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
6.1127 by (rule supI) simp_all
6.1128
6.1129 -lemma (in complete_lattice) top_closed [simp, intro]:
6.1130 +lemma (in weak_complete_lattice) top_closed [simp, intro]:
6.1131 "\<top> \<in> carrier L"
6.1132 by (unfold top_def) simp
6.1133
6.1134 -lemma (in complete_lattice) infI:
6.1135 +lemma (in weak_complete_lattice) infI:
6.1136 "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
6.1137 ==> P (\<Sqinter>A)"
6.1138 proof (unfold inf_def)
6.1139 assume L: "A \<subseteq> carrier L"
6.1140 and P: "!!l. greatest L l (Lower L A) ==> P l"
6.1141 with inf_exists obtain s where "greatest L s (Lower L A)" by blast
6.1142 - with L show "P (THE l. greatest L l (Lower L A))"
6.1143 - by (fast intro: theI2 greatest_unique P)
6.1144 + with L show "P (SOME l. greatest L l (Lower L A))"
6.1145 + by (fast intro: someI2 weak_greatest_unique P)
6.1146 qed
6.1147
6.1148 -lemma (in complete_lattice) inf_closed [simp]:
6.1149 +lemma (in weak_complete_lattice) inf_closed [simp]:
6.1150 "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
6.1151 by (rule infI) simp_all
6.1152
6.1153 -lemma (in complete_lattice) bottom_closed [simp, intro]:
6.1154 +lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
6.1155 "\<bottom> \<in> carrier L"
6.1156 by (unfold bottom_def) simp
6.1157
6.1158 @@ -783,12 +1036,12 @@
6.1159 "Upper L {} = carrier L"
6.1160 by (unfold Upper_def) simp
6.1161
6.1162 -theorem (in partial_order) complete_lattice_criterion1:
6.1163 +theorem (in weak_partial_order) weak_complete_lattice_criterion1:
6.1164 assumes top_exists: "EX g. greatest L g (carrier L)"
6.1165 and inf_exists:
6.1166 "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
6.1167 - shows "complete_lattice L"
6.1168 -proof (rule complete_latticeI)
6.1169 + shows "weak_complete_lattice L"
6.1170 +proof (rule weak_complete_latticeI)
6.1171 from top_exists obtain top where top: "greatest L top (carrier L)" ..
6.1172 fix A
6.1173 assume L: "A \<subseteq> carrier L"
6.1174 @@ -803,7 +1056,7 @@
6.1175 apply (rule greatest_le [where A = "Lower L ?B"])
6.1176 apply (rule b_inf_B)
6.1177 apply (rule Lower_memI)
6.1178 - apply (erule Upper_memD)
6.1179 + apply (erule Upper_memD [THEN conjunct1])
6.1180 apply assumption
6.1181 apply (rule L)
6.1182 apply (fast intro: L [THEN subsetD])
6.1183 @@ -829,16 +1082,226 @@
6.1184 (* TODO: prove dual version *)
6.1185
6.1186
6.1187 +subsection {* Orders and Lattices where @{text eq} is the Equality *}
6.1188 +
6.1189 +locale partial_order = weak_partial_order +
6.1190 + assumes eq_is_equal: "op .= = op ="
6.1191 +begin
6.1192 +
6.1193 +declare weak_le_anti_sym [rule del]
6.1194 +
6.1195 +lemma le_anti_sym [intro]:
6.1196 + "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
6.1197 + using weak_le_anti_sym unfolding eq_is_equal .
6.1198 +
6.1199 +lemma lless_eq:
6.1200 + "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
6.1201 + unfolding lless_def by (simp add: eq_is_equal)
6.1202 +
6.1203 +lemma lless_asym:
6.1204 + assumes "a \<in> carrier L" "b \<in> carrier L"
6.1205 + and "a \<sqsubset> b" "b \<sqsubset> a"
6.1206 + shows "P"
6.1207 + using assms unfolding lless_eq by auto
6.1208 +
6.1209 +lemma lless_trans [trans]:
6.1210 + assumes "a \<sqsubset> b" "b \<sqsubset> c"
6.1211 + and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
6.1212 + shows "a \<sqsubset> c"
6.1213 + using assms unfolding lless_eq by (blast dest: le_trans intro: sym)
6.1214 +
6.1215 +end
6.1216 +
6.1217 +
6.1218 +subsubsection {* Upper and lower bounds of a set *}
6.1219 +
6.1220 +(* all relevant lemmas are global and already proved above *)
6.1221 +
6.1222 +
6.1223 +subsubsection {* Least and greatest, as predicate *}
6.1224 +
6.1225 +lemma (in partial_order) least_unique:
6.1226 + "[| least L x A; least L y A |] ==> x = y"
6.1227 + using weak_least_unique unfolding eq_is_equal .
6.1228 +
6.1229 +lemma (in partial_order) greatest_unique:
6.1230 + "[| greatest L x A; greatest L y A |] ==> x = y"
6.1231 + using weak_greatest_unique unfolding eq_is_equal .
6.1232 +
6.1233 +
6.1234 +subsection {* Lattices *}
6.1235 +
6.1236 +locale upper_semilattice = partial_order +
6.1237 + assumes sup_of_two_exists:
6.1238 + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
6.1239 +
6.1240 +interpretation upper_semilattice < weak_upper_semilattice
6.1241 + by unfold_locales (rule sup_of_two_exists)
6.1242 +
6.1243 +locale lower_semilattice = partial_order +
6.1244 + assumes inf_of_two_exists:
6.1245 + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
6.1246 +
6.1247 +interpretation lower_semilattice < weak_lower_semilattice
6.1248 + by unfold_locales (rule inf_of_two_exists)
6.1249 +
6.1250 +locale lattice = upper_semilattice + lower_semilattice
6.1251 +
6.1252 +
6.1253 +subsubsection {* Supremum *}
6.1254 +
6.1255 +context partial_order begin
6.1256 +
6.1257 +declare weak_sup_of_singleton [simp del]
6.1258 +
6.1259 +lemma sup_of_singleton [simp]:
6.1260 + "x \<in> carrier L ==> \<Squnion>{x} = x"
6.1261 + using weak_sup_of_singleton unfolding eq_is_equal .
6.1262 +
6.1263 +end
6.1264 +
6.1265 +context upper_semilattice begin
6.1266 +
6.1267 +lemma join_assoc_lemma:
6.1268 + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
6.1269 + shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
6.1270 + using weak_join_assoc_lemma unfolding eq_is_equal .
6.1271 +
6.1272 +end
6.1273 +
6.1274 +lemma (in upper_semilattice) join_assoc:
6.1275 + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
6.1276 + shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
6.1277 + using weak_join_assoc unfolding eq_is_equal .
6.1278 +
6.1279 +
6.1280 +subsubsection {* Infimum *}
6.1281 +
6.1282 +context partial_order begin
6.1283 +
6.1284 +declare weak_inf_of_singleton [simp del]
6.1285 +
6.1286 +lemma inf_of_singleton [simp]:
6.1287 + "x \<in> carrier L ==> \<Sqinter>{x} = x"
6.1288 + using weak_inf_of_singleton unfolding eq_is_equal .
6.1289 +
6.1290 +end
6.1291 +
6.1292 +context lower_semilattice begin
6.1293 +
6.1294 +text {* Condition on @{text A}: infimum exists. *}
6.1295 +
6.1296 +lemma meet_assoc_lemma:
6.1297 + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
6.1298 + shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
6.1299 + using weak_meet_assoc_lemma unfolding eq_is_equal .
6.1300 +
6.1301 +end
6.1302 +
6.1303 +lemma (in lower_semilattice) meet_assoc:
6.1304 + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
6.1305 + shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
6.1306 + using weak_meet_assoc unfolding eq_is_equal .
6.1307 +
6.1308 +
6.1309 +subsection {* Total Orders *}
6.1310 +
6.1311 +locale total_order = partial_order +
6.1312 + assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
6.1313 +
6.1314 +interpretation total_order < weak_total_order
6.1315 + by unfold_locales (rule total)
6.1316 +
6.1317 +text {* Introduction rule: the usual definition of total order *}
6.1318 +
6.1319 +lemma (in partial_order) total_orderI:
6.1320 + assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
6.1321 + shows "total_order L"
6.1322 + by unfold_locales (rule total)
6.1323 +
6.1324 +text {* Total orders are lattices. *}
6.1325 +
6.1326 +interpretation total_order < lattice
6.1327 + by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists)
6.1328 +
6.1329 +
6.1330 +subsection {* Complete lattices *}
6.1331 +
6.1332 +locale complete_lattice = lattice +
6.1333 + assumes sup_exists:
6.1334 + "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
6.1335 + and inf_exists:
6.1336 + "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
6.1337 +
6.1338 +interpretation complete_lattice < weak_complete_lattice
6.1339 + by unfold_locales (auto intro: sup_exists inf_exists)
6.1340 +
6.1341 +text {* Introduction rule: the usual definition of complete lattice *}
6.1342 +
6.1343 +lemma (in partial_order) complete_latticeI:
6.1344 + assumes sup_exists:
6.1345 + "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
6.1346 + and inf_exists:
6.1347 + "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
6.1348 + shows "complete_lattice L"
6.1349 + by unfold_locales (auto intro: sup_exists inf_exists)
6.1350 +
6.1351 +theorem (in partial_order) complete_lattice_criterion1:
6.1352 + assumes top_exists: "EX g. greatest L g (carrier L)"
6.1353 + and inf_exists:
6.1354 + "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
6.1355 + shows "complete_lattice L"
6.1356 +proof (rule complete_latticeI)
6.1357 + from top_exists obtain top where top: "greatest L top (carrier L)" ..
6.1358 + fix A
6.1359 + assume L: "A \<subseteq> carrier L"
6.1360 + let ?B = "Upper L A"
6.1361 + from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
6.1362 + then have B_non_empty: "?B ~= {}" by fast
6.1363 + have B_L: "?B \<subseteq> carrier L" by simp
6.1364 + from inf_exists [OF B_L B_non_empty]
6.1365 + obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
6.1366 + have "least L b (Upper L A)"
6.1367 +apply (rule least_UpperI)
6.1368 + apply (rule greatest_le [where A = "Lower L ?B"])
6.1369 + apply (rule b_inf_B)
6.1370 + apply (rule Lower_memI)
6.1371 + apply (erule Upper_memD [THEN conjunct1])
6.1372 + apply assumption
6.1373 + apply (rule L)
6.1374 + apply (fast intro: L [THEN subsetD])
6.1375 + apply (erule greatest_Lower_below [OF b_inf_B])
6.1376 + apply simp
6.1377 + apply (rule L)
6.1378 +apply (rule greatest_closed [OF b_inf_B])
6.1379 +done
6.1380 + then show "EX s. least L s (Upper L A)" ..
6.1381 +next
6.1382 + fix A
6.1383 + assume L: "A \<subseteq> carrier L"
6.1384 + show "EX i. greatest L i (Lower L A)"
6.1385 + proof (cases "A = {}")
6.1386 + case True then show ?thesis
6.1387 + by (simp add: top_exists)
6.1388 + next
6.1389 + case False with L show ?thesis
6.1390 + by (rule inf_exists)
6.1391 + qed
6.1392 +qed
6.1393 +
6.1394 +(* TODO: prove dual version *)
6.1395 +
6.1396 +
6.1397 subsection {* Examples *}
6.1398
6.1399 subsubsection {* Powerset of a Set is a Complete Lattice *}
6.1400
6.1401 theorem powerset_is_complete_lattice:
6.1402 - "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
6.1403 + "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
6.1404 (is "complete_lattice ?L")
6.1405 proof (rule partial_order.complete_latticeI)
6.1406 show "partial_order ?L"
6.1407 - by (rule partial_order.intro) auto
6.1408 + by unfold_locales auto
6.1409 next
6.1410 fix B
6.1411 assume B: "B \<subseteq> carrier ?L"
7.1 --- a/src/HOL/Algebra/ROOT.ML Wed Jul 30 16:07:00 2008 +0200
7.2 +++ b/src/HOL/Algebra/ROOT.ML Wed Jul 30 19:03:33 2008 +0200
7.3 @@ -5,7 +5,7 @@
7.4 *)
7.5
7.6 (* Preliminaries from set and number theory *)
7.7 -no_document use_thys ["FuncSet", "Primes", "Binomial"];
7.8 +no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"];
7.9
7.10
7.11 (*** New development, based on explicit structures ***)
7.12 @@ -17,8 +17,9 @@
7.13 "Bij", (* Automorphism Groups *)
7.14
7.15 (* Rings *)
7.16 - "UnivPoly", (* Rings and polynomials *)
7.17 - "IntRing" (* Ideals and residue classes *)
7.18 + "Divisibility", (* Rings *)
7.19 + "IntRing", (* Ideals and residue classes *)
7.20 + "UnivPoly" (* Polynomials *)
7.21 ];
7.22
7.23
8.1 --- a/src/HOL/IsaMakefile Wed Jul 30 16:07:00 2008 +0200
8.2 +++ b/src/HOL/IsaMakefile Wed Jul 30 19:03:33 2008 +0200
8.3 @@ -509,7 +509,7 @@
8.4 Library/Multiset.thy Library/Permutation.thy Library/Primes.thy \
8.5 Algebra/AbelCoset.thy Algebra/Bij.thy Algebra/Congruence.thy \
8.6 Algebra/Coset.thy Algebra/Divisibility.thy Algebra/Exponent.thy \
8.7 - Algebra/FiniteProduct.thy Algebra/GLattice.thy \
8.8 + Algebra/FiniteProduct.thy \
8.9 Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy \
8.10 Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy \
8.11 Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy \