author | Fabian Huch <huch@in.tum.de> |
Thu, 28 Mar 2024 15:08:58 +0100 | |
changeset 80058 | 68f6b29ae066 |
parent 77362 | 1a6103f6ab0b |
permissions | -rw-r--r-- |
35849 | 1 |
(* Title: HOL/Algebra/Lattice.thy |
2 |
Author: Clemens Ballarin, started 7 November 2003 |
|
3 |
Copyright: Clemens Ballarin |
|
27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset
|
4 |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset
|
5 |
Most congruence rules by Stephan Hohe. |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
6 |
With additional contributions from Alasdair Armstrong and Simon Foster. |
14551 | 7 |
*) |
8 |
||
35849 | 9 |
theory Lattice |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
10 |
imports Order |
44472 | 11 |
begin |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
12 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
13 |
section \<open>Lattices\<close> |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
14 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
15 |
subsection \<open>Supremum and infimum\<close> |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
16 |
|
35847 | 17 |
definition |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
18 |
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
19 |
where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
20 |
|
35847 | 21 |
definition |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
22 |
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
23 |
where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
24 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
25 |
definition supr :: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
26 |
"('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a " |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
27 |
where "supr L A f = \<Squnion>\<^bsub>L\<^esub>(f ` A)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
28 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
29 |
definition infi :: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
30 |
"('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a " |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
31 |
where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
32 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
33 |
syntax |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
34 |
"_inf1" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3IINF\<index> _./ _)" [0, 10] 10) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
35 |
"_inf" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a" ("(3IINF\<index> _:_./ _)" [0, 0, 10] 10) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
36 |
"_sup1" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
37 |
"_sup" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
38 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
39 |
translations |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
40 |
"IINF\<^bsub>L\<^esub> x. B" == "CONST infi L CONST UNIV (%x. B)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
41 |
"IINF\<^bsub>L\<^esub> x:A. B" == "CONST infi L A (%x. B)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
42 |
"SSUP\<^bsub>L\<^esub> x. B" == "CONST supr L CONST UNIV (%x. B)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
43 |
"SSUP\<^bsub>L\<^esub> x:A. B" == "CONST supr L A (%x. B)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
44 |
|
35847 | 45 |
definition |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
46 |
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
47 |
where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
48 |
|
35847 | 49 |
definition |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
50 |
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35847
diff
changeset
|
51 |
where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
52 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
53 |
definition |
66580
e5b1d4d55bf6
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
ballarin
parents:
65099
diff
changeset
|
54 |
LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67226
diff
changeset
|
55 |
"LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}" \<comment> \<open>least fixed point\<close> |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
56 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
57 |
definition |
66580
e5b1d4d55bf6
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
ballarin
parents:
65099
diff
changeset
|
58 |
GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67226
diff
changeset
|
59 |
"GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}" \<comment> \<open>greatest fixed point\<close> |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
60 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
61 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
62 |
subsection \<open>Dual operators\<close> |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
63 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
64 |
lemma sup_dual [simp]: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
65 |
"\<Squnion>\<^bsub>inv_gorder L\<^esub>A = \<Sqinter>\<^bsub>L\<^esub>A" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
66 |
by (simp add: sup_def inf_def) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
67 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
68 |
lemma inf_dual [simp]: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
69 |
"\<Sqinter>\<^bsub>inv_gorder L\<^esub>A = \<Squnion>\<^bsub>L\<^esub>A" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
70 |
by (simp add: sup_def inf_def) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
71 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
72 |
lemma join_dual [simp]: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
73 |
"p \<squnion>\<^bsub>inv_gorder L\<^esub> q = p \<sqinter>\<^bsub>L\<^esub> q" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
74 |
by (simp add:join_def meet_def) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
75 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
76 |
lemma meet_dual [simp]: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
77 |
"p \<sqinter>\<^bsub>inv_gorder L\<^esub> q = p \<squnion>\<^bsub>L\<^esub> q" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
78 |
by (simp add:join_def meet_def) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
79 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
80 |
lemma top_dual [simp]: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
81 |
"\<top>\<^bsub>inv_gorder L\<^esub> = \<bottom>\<^bsub>L\<^esub>" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
82 |
by (simp add: top_def bottom_def) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
83 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
84 |
lemma bottom_dual [simp]: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
85 |
"\<bottom>\<^bsub>inv_gorder L\<^esub> = \<top>\<^bsub>L\<^esub>" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
86 |
by (simp add: top_def bottom_def) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
87 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
88 |
lemma LFP_dual [simp]: |
66580
e5b1d4d55bf6
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
ballarin
parents:
65099
diff
changeset
|
89 |
"LEAST_FP (inv_gorder L) f = GREATEST_FP L f" |
e5b1d4d55bf6
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
ballarin
parents:
65099
diff
changeset
|
90 |
by (simp add:LEAST_FP_def GREATEST_FP_def) |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
91 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
92 |
lemma GFP_dual [simp]: |
66580
e5b1d4d55bf6
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
ballarin
parents:
65099
diff
changeset
|
93 |
"GREATEST_FP (inv_gorder L) f = LEAST_FP L f" |
e5b1d4d55bf6
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
ballarin
parents:
65099
diff
changeset
|
94 |
by (simp add:LEAST_FP_def GREATEST_FP_def) |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
95 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
96 |
|
61382 | 97 |
subsection \<open>Lattices\<close> |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
98 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
99 |
locale weak_upper_semilattice = weak_partial_order + |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
100 |
assumes sup_of_two_exists: |
67091 | 101 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. least L s (Upper L {x, y})" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
102 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
103 |
locale weak_lower_semilattice = weak_partial_order + |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
104 |
assumes inf_of_two_exists: |
67091 | 105 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. greatest L s (Lower L {x, y})" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
106 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
107 |
locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
108 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
109 |
lemma (in weak_lattice) dual_weak_lattice: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
110 |
"weak_lattice (inv_gorder L)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
111 |
proof - |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
112 |
interpret dual: weak_partial_order "inv_gorder L" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
113 |
by (metis dual_weak_order) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
114 |
show ?thesis |
77362 | 115 |
proof qed (simp_all add: inf_of_two_exists sup_of_two_exists) |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
116 |
qed |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
117 |
|
14666 | 118 |
|
61382 | 119 |
subsubsection \<open>Supremum\<close> |
14551 | 120 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
121 |
lemma (in weak_upper_semilattice) joinI: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
122 |
"[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] |
14551 | 123 |
==> P (x \<squnion> y)" |
124 |
proof (unfold join_def sup_def) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
125 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
126 |
and P: "!!l. least L l (Upper L {x, y}) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
127 |
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
128 |
with L show "P (SOME l. least L l (Upper L {x, y}))" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
129 |
by (fast intro: someI2 P) |
14551 | 130 |
qed |
131 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
132 |
lemma (in weak_upper_semilattice) join_closed [simp]: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
133 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" |
27700 | 134 |
by (rule joinI) (rule least_closed) |
14551 | 135 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
136 |
lemma (in weak_upper_semilattice) join_cong_l: |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
137 |
assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
138 |
and xx': "x .= x'" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
139 |
shows "x \<squnion> y .= x' \<squnion> y" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
140 |
proof (rule joinI, rule joinI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
141 |
fix a b |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
142 |
from xx' carr |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
143 |
have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
144 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
145 |
assume leasta: "least L a (Upper L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
146 |
assume "least L b (Upper L {x', y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
147 |
with carr |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
148 |
have leastb: "least L b (Upper L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
149 |
by (simp add: least_Upper_cong_r[OF _ _ seq]) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
150 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
151 |
from leasta leastb |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
152 |
show "a .= b" by (rule weak_least_unique) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
153 |
qed (rule carr)+ |
14551 | 154 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
155 |
lemma (in weak_upper_semilattice) join_cong_r: |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
156 |
assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
157 |
and yy': "y .= y'" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
158 |
shows "x \<squnion> y .= x \<squnion> y'" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
159 |
proof (rule joinI, rule joinI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
160 |
fix a b |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
161 |
have "{x, y} = {y, x}" by fast |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
162 |
also from carr yy' |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
163 |
have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
164 |
also have "{y', x} = {x, y'}" by fast |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
165 |
finally |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
166 |
have seq: "{x, y} {.=} {x, y'}" . |
14551 | 167 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
168 |
assume leasta: "least L a (Upper L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
169 |
assume "least L b (Upper L {x, y'})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
170 |
with carr |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
171 |
have leastb: "least L b (Upper L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
172 |
by (simp add: least_Upper_cong_r[OF _ _ seq]) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
173 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
174 |
from leasta leastb |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
175 |
show "a .= b" by (rule weak_least_unique) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
176 |
qed (rule carr)+ |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
177 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
178 |
lemma (in weak_partial_order) sup_of_singletonI: (* only reflexivity needed ? *) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
179 |
"x \<in> carrier L ==> least L x (Upper L {x})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
180 |
by (rule least_UpperI) auto |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
181 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
182 |
lemma (in weak_partial_order) weak_sup_of_singleton [simp]: |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
183 |
"x \<in> carrier L ==> \<Squnion>{x} .= x" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
184 |
unfolding sup_def |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
185 |
by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
186 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
187 |
lemma (in weak_partial_order) sup_of_singleton_closed [simp]: |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
188 |
"x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
189 |
unfolding sup_def |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
190 |
by (rule someI2) (auto intro: sup_of_singletonI) |
14666 | 191 |
|
63167 | 192 |
text \<open>Condition on \<open>A\<close>: supremum exists.\<close> |
14551 | 193 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
194 |
lemma (in weak_upper_semilattice) sup_insertI: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
195 |
"[| !!s. least L s (Upper L (insert x A)) ==> P s; |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
196 |
least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] |
14693 | 197 |
==> P (\<Squnion>(insert x A))" |
14551 | 198 |
proof (unfold sup_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
199 |
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
200 |
and P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
201 |
and least_a: "least L a (Upper L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
202 |
from L least_a have La: "a \<in> carrier L" by simp |
14551 | 203 |
from L sup_of_two_exists least_a |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
204 |
obtain s where least_s: "least L s (Upper L {a, x})" by blast |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
205 |
show "P (SOME l. least L l (Upper L (insert x A)))" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
206 |
proof (rule someI2) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
207 |
show "least L s (Upper L (insert x A))" |
14551 | 208 |
proof (rule least_UpperI) |
209 |
fix z |
|
14693 | 210 |
assume "z \<in> insert x A" |
211 |
then show "z \<sqsubseteq> s" |
|
212 |
proof |
|
213 |
assume "z = x" then show ?thesis |
|
214 |
by (simp add: least_Upper_above [OF least_s] L La) |
|
215 |
next |
|
216 |
assume "z \<in> A" |
|
217 |
with L least_s least_a show ?thesis |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
218 |
by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above) |
14693 | 219 |
qed |
220 |
next |
|
221 |
fix y |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
222 |
assume y: "y \<in> Upper L (insert x A)" |
14693 | 223 |
show "s \<sqsubseteq> y" |
224 |
proof (rule least_le [OF least_s], rule Upper_memI) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
225 |
fix z |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
226 |
assume z: "z \<in> {a, x}" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
227 |
then show "z \<sqsubseteq> y" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
228 |
proof |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
229 |
have y': "y \<in> Upper L A" |
77362 | 230 |
by (meson Upper_antimono in_mono subset_insertI y) |
14693 | 231 |
assume "z = a" |
232 |
with y' least_a show ?thesis by (fast dest: least_le) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
233 |
next |
77362 | 234 |
assume "z \<in> {x}" |
14693 | 235 |
with y L show ?thesis by blast |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
236 |
qed |
23350 | 237 |
qed (rule Upper_closed [THEN subsetD, OF y]) |
14693 | 238 |
next |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
239 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
240 |
from least_s show "s \<in> carrier L" by simp |
14551 | 241 |
qed |
23350 | 242 |
qed (rule P) |
14551 | 243 |
qed |
244 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
245 |
lemma (in weak_upper_semilattice) finite_sup_least: |
67091 | 246 |
"[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> least L (\<Squnion>A) (Upper L A)" |
22265 | 247 |
proof (induct set: finite) |
14693 | 248 |
case empty |
249 |
then show ?case by simp |
|
14551 | 250 |
next |
15328 | 251 |
case (insert x A) |
14551 | 252 |
show ?case |
253 |
proof (cases "A = {}") |
|
254 |
case True |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
255 |
with insert show ?thesis |
44472 | 256 |
by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
257 |
(* The above step is hairy; least_cong can make simp loop. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
258 |
Would want special version of simp to apply least_cong. *) |
14551 | 259 |
next |
260 |
case False |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
261 |
with insert have "least L (\<Squnion>A) (Upper L A)" by simp |
14693 | 262 |
with _ show ?thesis |
263 |
by (rule sup_insertI) (simp_all add: insert [simplified]) |
|
14551 | 264 |
qed |
265 |
qed |
|
266 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
267 |
lemma (in weak_upper_semilattice) finite_sup_insertI: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
268 |
assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
269 |
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
270 |
shows "P (\<Squnion> (insert x A))" |
14551 | 271 |
proof (cases "A = {}") |
272 |
case True with P and xA show ?thesis |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
273 |
by (simp add: finite_sup_least) |
14551 | 274 |
next |
275 |
case False with P and xA show ?thesis |
|
276 |
by (simp add: sup_insertI finite_sup_least) |
|
277 |
qed |
|
278 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
279 |
lemma (in weak_upper_semilattice) finite_sup_closed [simp]: |
67091 | 280 |
"[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> \<Squnion>A \<in> carrier L" |
22265 | 281 |
proof (induct set: finite) |
14551 | 282 |
case empty then show ?case by simp |
283 |
next |
|
15328 | 284 |
case insert then show ?case |
14693 | 285 |
by - (rule finite_sup_insertI, simp_all) |
14551 | 286 |
qed |
287 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
288 |
lemma (in weak_upper_semilattice) join_left: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
289 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" |
14693 | 290 |
by (rule joinI [folded join_def]) (blast dest: least_mem) |
14551 | 291 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
292 |
lemma (in weak_upper_semilattice) join_right: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
293 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" |
14693 | 294 |
by (rule joinI [folded join_def]) (blast dest: least_mem) |
14551 | 295 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
296 |
lemma (in weak_upper_semilattice) sup_of_two_least: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
297 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" |
14551 | 298 |
proof (unfold sup_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
299 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
300 |
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
301 |
with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
302 |
by (fast intro: someI2 weak_least_unique) (* blast fails *) |
14551 | 303 |
qed |
304 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
305 |
lemma (in weak_upper_semilattice) join_le: |
14693 | 306 |
assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
23350 | 307 |
and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" |
14551 | 308 |
shows "x \<squnion> y \<sqsubseteq> z" |
23350 | 309 |
proof (rule joinI [OF _ x y]) |
14551 | 310 |
fix s |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
311 |
assume "least L s (Upper L {x, y})" |
23350 | 312 |
with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) |
14551 | 313 |
qed |
14693 | 314 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
315 |
lemma (in weak_lattice) weak_le_iff_meet: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
316 |
assumes "x \<in> carrier L" "y \<in> carrier L" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
317 |
shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) .= y" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
318 |
by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
319 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
320 |
lemma (in weak_upper_semilattice) weak_join_assoc_lemma: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
321 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
322 |
shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}" |
14551 | 323 |
proof (rule finite_sup_insertI) |
63167 | 324 |
\<comment> \<open>The textbook argument in Jacobson I, p 457\<close> |
14551 | 325 |
fix s |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
326 |
assume sup: "least L s (Upper L {x, y, z})" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
327 |
show "x \<squnion> (y \<squnion> z) .= s" |
33657 | 328 |
proof (rule weak_le_antisym) |
14551 | 329 |
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44655
diff
changeset
|
330 |
by (fastforce intro!: join_le elim: least_Upper_above) |
14551 | 331 |
next |
332 |
from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
333 |
by (erule_tac least_le) |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
334 |
(blast intro!: Upper_memI intro: le_trans join_left join_right join_closed) |
27700 | 335 |
qed (simp_all add: L least_closed [OF sup]) |
14551 | 336 |
qed (simp_all add: L) |
337 |
||
63167 | 338 |
text \<open>Commutativity holds for \<open>=\<close>.\<close> |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
339 |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
340 |
lemma join_comm: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
341 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
342 |
shows "x \<squnion> y = y \<squnion> x" |
14551 | 343 |
by (unfold join_def) (simp add: insert_commute) |
344 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
345 |
lemma (in weak_upper_semilattice) weak_join_assoc: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
346 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
347 |
shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)" |
14551 | 348 |
proof - |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
349 |
(* FIXME: could be simplified by improved simp: uniform use of .=, |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
350 |
omit [symmetric] in last step. *) |
14551 | 351 |
have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
352 |
also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma) |
14693 | 353 |
also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
354 |
also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric]) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
355 |
finally show ?thesis by (simp add: L) |
14551 | 356 |
qed |
357 |
||
14693 | 358 |
|
61382 | 359 |
subsubsection \<open>Infimum\<close> |
14551 | 360 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
361 |
lemma (in weak_lower_semilattice) meetI: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
362 |
"[| !!i. greatest L i (Lower L {x, y}) ==> P i; |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
363 |
x \<in> carrier L; y \<in> carrier L |] |
14551 | 364 |
==> P (x \<sqinter> y)" |
365 |
proof (unfold meet_def inf_def) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
366 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
367 |
and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
368 |
with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
369 |
with L show "P (SOME g. greatest L g (Lower L {x, y}))" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
370 |
by (fast intro: someI2 weak_greatest_unique P) |
14551 | 371 |
qed |
372 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
373 |
lemma (in weak_lower_semilattice) meet_closed [simp]: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
374 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L" |
27700 | 375 |
by (rule meetI) (rule greatest_closed) |
14551 | 376 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
377 |
lemma (in weak_lower_semilattice) meet_cong_l: |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
378 |
assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
379 |
and xx': "x .= x'" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
380 |
shows "x \<sqinter> y .= x' \<sqinter> y" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
381 |
proof (rule meetI, rule meetI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
382 |
fix a b |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
383 |
from xx' carr |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
384 |
have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
385 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
386 |
assume greatesta: "greatest L a (Lower L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
387 |
assume "greatest L b (Lower L {x', y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
388 |
with carr |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
389 |
have greatestb: "greatest L b (Lower L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
390 |
by (simp add: greatest_Lower_cong_r[OF _ _ seq]) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
391 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
392 |
from greatesta greatestb |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
393 |
show "a .= b" by (rule weak_greatest_unique) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
394 |
qed (rule carr)+ |
14551 | 395 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
396 |
lemma (in weak_lower_semilattice) meet_cong_r: |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
397 |
assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
398 |
and yy': "y .= y'" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
399 |
shows "x \<sqinter> y .= x \<sqinter> y'" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
400 |
proof (rule meetI, rule meetI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
401 |
fix a b |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
402 |
have "{x, y} = {y, x}" by fast |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
403 |
also from carr yy' |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
404 |
have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
405 |
also have "{y', x} = {x, y'}" by fast |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
406 |
finally |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
407 |
have seq: "{x, y} {.=} {x, y'}" . |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
408 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
409 |
assume greatesta: "greatest L a (Lower L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
410 |
assume "greatest L b (Lower L {x, y'})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
411 |
with carr |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
412 |
have greatestb: "greatest L b (Lower L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
413 |
by (simp add: greatest_Lower_cong_r[OF _ _ seq]) |
14551 | 414 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
415 |
from greatesta greatestb |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
416 |
show "a .= b" by (rule weak_greatest_unique) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
417 |
qed (rule carr)+ |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
418 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
419 |
lemma (in weak_partial_order) inf_of_singletonI: (* only reflexivity needed ? *) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
420 |
"x \<in> carrier L ==> greatest L x (Lower L {x})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
421 |
by (rule greatest_LowerI) auto |
14551 | 422 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
423 |
lemma (in weak_partial_order) weak_inf_of_singleton [simp]: |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
424 |
"x \<in> carrier L ==> \<Sqinter>{x} .= x" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
425 |
unfolding inf_def |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
426 |
by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
427 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
428 |
lemma (in weak_partial_order) inf_of_singleton_closed: |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
429 |
"x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
430 |
unfolding inf_def |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
431 |
by (rule someI2) (auto intro: inf_of_singletonI) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
432 |
|
63167 | 433 |
text \<open>Condition on \<open>A\<close>: infimum exists.\<close> |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
434 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
435 |
lemma (in weak_lower_semilattice) inf_insertI: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
436 |
"[| !!i. greatest L i (Lower L (insert x A)) ==> P i; |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
437 |
greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] |
14693 | 438 |
==> P (\<Sqinter>(insert x A))" |
14551 | 439 |
proof (unfold inf_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
440 |
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
441 |
and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
442 |
and greatest_a: "greatest L a (Lower L A)" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
443 |
from L greatest_a have La: "a \<in> carrier L" by simp |
14551 | 444 |
from L inf_of_two_exists greatest_a |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
445 |
obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
446 |
show "P (SOME g. greatest L g (Lower L (insert x A)))" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
447 |
proof (rule someI2) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
448 |
show "greatest L i (Lower L (insert x A))" |
14551 | 449 |
proof (rule greatest_LowerI) |
450 |
fix z |
|
14693 | 451 |
assume "z \<in> insert x A" |
452 |
then show "i \<sqsubseteq> z" |
|
453 |
proof |
|
454 |
assume "z = x" then show ?thesis |
|
27700 | 455 |
by (simp add: greatest_Lower_below [OF greatest_i] L La) |
14693 | 456 |
next |
457 |
assume "z \<in> A" |
|
458 |
with L greatest_i greatest_a show ?thesis |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
459 |
by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below) |
14693 | 460 |
qed |
461 |
next |
|
462 |
fix y |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
463 |
assume y: "y \<in> Lower L (insert x A)" |
14693 | 464 |
show "y \<sqsubseteq> i" |
465 |
proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
466 |
fix z |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
467 |
assume z: "z \<in> {a, x}" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
468 |
then show "y \<sqsubseteq> z" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
469 |
proof |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
470 |
have y': "y \<in> Lower L A" |
77362 | 471 |
by (meson Lower_antimono in_mono subset_insertI y) |
14693 | 472 |
assume "z = a" |
473 |
with y' greatest_a show ?thesis by (fast dest: greatest_le) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
474 |
next |
14693 | 475 |
assume "z \<in> {x}" |
476 |
with y L show ?thesis by blast |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
477 |
qed |
23350 | 478 |
qed (rule Lower_closed [THEN subsetD, OF y]) |
14693 | 479 |
next |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
480 |
from L show "insert x A \<subseteq> carrier L" by simp |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
481 |
from greatest_i show "i \<in> carrier L" by simp |
14551 | 482 |
qed |
23350 | 483 |
qed (rule P) |
14551 | 484 |
qed |
485 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
486 |
lemma (in weak_lower_semilattice) finite_inf_greatest: |
67091 | 487 |
"[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> greatest L (\<Sqinter>A) (Lower L A)" |
22265 | 488 |
proof (induct set: finite) |
14551 | 489 |
case empty then show ?case by simp |
490 |
next |
|
15328 | 491 |
case (insert x A) |
14551 | 492 |
show ?case |
493 |
proof (cases "A = {}") |
|
494 |
case True |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
495 |
with insert show ?thesis |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
496 |
by simp (simp add: greatest_cong [OF weak_inf_of_singleton] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30363
diff
changeset
|
497 |
inf_of_singleton_closed inf_of_singletonI) |
14551 | 498 |
next |
499 |
case False |
|
500 |
from insert show ?thesis |
|
501 |
proof (rule_tac inf_insertI) |
|
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
502 |
from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp |
14551 | 503 |
qed simp_all |
504 |
qed |
|
505 |
qed |
|
506 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
507 |
lemma (in weak_lower_semilattice) finite_inf_insertI: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
508 |
assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
509 |
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
510 |
shows "P (\<Sqinter> (insert x A))" |
14551 | 511 |
proof (cases "A = {}") |
512 |
case True with P and xA show ?thesis |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
513 |
by (simp add: finite_inf_greatest) |
14551 | 514 |
next |
515 |
case False with P and xA show ?thesis |
|
516 |
by (simp add: inf_insertI finite_inf_greatest) |
|
517 |
qed |
|
518 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
519 |
lemma (in weak_lower_semilattice) finite_inf_closed [simp]: |
67091 | 520 |
"[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> \<Sqinter>A \<in> carrier L" |
22265 | 521 |
proof (induct set: finite) |
14551 | 522 |
case empty then show ?case by simp |
523 |
next |
|
15328 | 524 |
case insert then show ?case |
14551 | 525 |
by (rule_tac finite_inf_insertI) (simp_all) |
526 |
qed |
|
527 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
528 |
lemma (in weak_lower_semilattice) meet_left: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
529 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" |
14693 | 530 |
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
14551 | 531 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
532 |
lemma (in weak_lower_semilattice) meet_right: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
533 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" |
14693 | 534 |
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
14551 | 535 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
536 |
lemma (in weak_lower_semilattice) inf_of_two_greatest: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
537 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> |
60585 | 538 |
greatest L (\<Sqinter>{x, y}) (Lower L {x, y})" |
14551 | 539 |
proof (unfold inf_def) |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
540 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
541 |
with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast |
14551 | 542 |
with L |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
543 |
show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
544 |
by (fast intro: someI2 weak_greatest_unique) (* blast fails *) |
14551 | 545 |
qed |
546 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
547 |
lemma (in weak_lower_semilattice) meet_le: |
14693 | 548 |
assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" |
23350 | 549 |
and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" |
14551 | 550 |
shows "z \<sqsubseteq> x \<sqinter> y" |
23350 | 551 |
proof (rule meetI [OF _ x y]) |
14551 | 552 |
fix i |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
553 |
assume "greatest L i (Lower L {x, y})" |
23350 | 554 |
with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) |
14551 | 555 |
qed |
14693 | 556 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
557 |
lemma (in weak_lattice) weak_le_iff_join: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
558 |
assumes "x \<in> carrier L" "y \<in> carrier L" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
559 |
shows "x \<sqsubseteq> y \<longleftrightarrow> x .= (x \<sqinter> y)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
560 |
by (meson assms(1) assms(2) local.le_refl local.le_trans meet_closed meet_le meet_left meet_right weak_le_antisym weak_refl) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
561 |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
562 |
lemma (in weak_lower_semilattice) weak_meet_assoc_lemma: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
563 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
564 |
shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}" |
14551 | 565 |
proof (rule finite_inf_insertI) |
61382 | 566 |
txt \<open>The textbook argument in Jacobson I, p 457\<close> |
14551 | 567 |
fix i |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
568 |
assume inf: "greatest L i (Lower L {x, y, z})" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
569 |
show "x \<sqinter> (y \<sqinter> z) .= i" |
33657 | 570 |
proof (rule weak_le_antisym) |
14551 | 571 |
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44655
diff
changeset
|
572 |
by (fastforce intro!: meet_le elim: greatest_Lower_below) |
14551 | 573 |
next |
574 |
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" |
|
575 |
by (erule_tac greatest_le) |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
576 |
(blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed) |
27700 | 577 |
qed (simp_all add: L greatest_closed [OF inf]) |
14551 | 578 |
qed (simp_all add: L) |
579 |
||
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
580 |
lemma meet_comm: |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
581 |
fixes L (structure) |
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
582 |
shows "x \<sqinter> y = y \<sqinter> x" |
14551 | 583 |
by (unfold meet_def) (simp add: insert_commute) |
584 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
585 |
lemma (in weak_lower_semilattice) weak_meet_assoc: |
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset
|
586 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
587 |
shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)" |
14551 | 588 |
proof - |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
589 |
(* FIXME: improved simp, see weak_join_assoc above *) |
14551 | 590 |
have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm) |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
591 |
also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
592 |
also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
593 |
also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric]) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
594 |
finally show ?thesis by (simp add: L) |
14551 | 595 |
qed |
596 |
||
61382 | 597 |
text \<open>Total orders are lattices.\<close> |
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
598 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
599 |
sublocale weak_total_order \<subseteq> weak?: weak_lattice |
28823 | 600 |
proof |
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
601 |
fix x y |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
602 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
67091 | 603 |
show "\<exists>s. least L s (Upper L {x, y})" |
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
604 |
proof - |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
605 |
note total L |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
606 |
moreover |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
607 |
{ |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
608 |
assume "x \<sqsubseteq> y" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
609 |
with L have "least L y (Upper L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
610 |
by (rule_tac least_UpperI) auto |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
611 |
} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
612 |
moreover |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
613 |
{ |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
614 |
assume "y \<sqsubseteq> x" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
615 |
with L have "least L x (Upper L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
616 |
by (rule_tac least_UpperI) auto |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
617 |
} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
618 |
ultimately show ?thesis by blast |
14551 | 619 |
qed |
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
620 |
next |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
621 |
fix x y |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
622 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
67091 | 623 |
show "\<exists>i. greatest L i (Lower L {x, y})" |
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
624 |
proof - |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
625 |
note total L |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
626 |
moreover |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
627 |
{ |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
628 |
assume "y \<sqsubseteq> x" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
629 |
with L have "greatest L y (Lower L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
630 |
by (rule_tac greatest_LowerI) auto |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
631 |
} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
632 |
moreover |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
633 |
{ |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
634 |
assume "x \<sqsubseteq> y" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
635 |
with L have "greatest L x (Lower L {x, y})" |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
636 |
by (rule_tac greatest_LowerI) auto |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
637 |
} |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
638 |
ultimately show ?thesis by blast |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
639 |
qed |
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset
|
640 |
qed |
14551 | 641 |
|
14693 | 642 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
643 |
subsection \<open>Weak Bounded Lattices\<close> |
14551 | 644 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
645 |
locale weak_bounded_lattice = |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
646 |
weak_lattice + |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
647 |
weak_partial_order_bottom + |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
648 |
weak_partial_order_top |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
649 |
begin |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
650 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
651 |
lemma bottom_meet: "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqinter> x .= \<bottom>" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
652 |
by (metis bottom_least least_def meet_closed meet_left weak_le_antisym) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
653 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
654 |
lemma bottom_join: "x \<in> carrier L \<Longrightarrow> \<bottom> \<squnion> x .= x" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
655 |
by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
656 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
657 |
lemma bottom_weak_eq: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
658 |
"\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b .= \<bottom>" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
659 |
by (metis bottom_closed bottom_lower weak_le_antisym) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
660 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
661 |
lemma top_join: "x \<in> carrier L \<Longrightarrow> \<top> \<squnion> x .= \<top>" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
662 |
by (metis join_closed join_left top_closed top_higher weak_le_antisym) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
663 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
664 |
lemma top_meet: "x \<in> carrier L \<Longrightarrow> \<top> \<sqinter> x .= x" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
665 |
by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
666 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
667 |
lemma top_weak_eq: "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t .= \<top>" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
668 |
by (metis top_closed top_higher weak_le_antisym) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
669 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
670 |
end |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
671 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
672 |
sublocale weak_bounded_lattice \<subseteq> weak_partial_order .. |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
673 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
674 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
675 |
subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close> |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
676 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
677 |
locale upper_semilattice = partial_order + |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
678 |
assumes sup_of_two_exists: |
67091 | 679 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. least L s (Upper L {x, y})" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
680 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
681 |
sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
682 |
by unfold_locales (rule sup_of_two_exists) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
683 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
684 |
locale lower_semilattice = partial_order + |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
685 |
assumes inf_of_two_exists: |
67091 | 686 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. greatest L s (Lower L {x, y})" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
687 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
688 |
sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
689 |
by unfold_locales (rule inf_of_two_exists) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
690 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
691 |
locale lattice = upper_semilattice + lower_semilattice |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
692 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
693 |
sublocale lattice \<subseteq> weak_lattice .. |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
694 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
695 |
lemma (in lattice) dual_lattice: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
696 |
"lattice (inv_gorder L)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
697 |
proof - |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
698 |
interpret dual: weak_lattice "inv_gorder L" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
699 |
by (metis dual_weak_lattice) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
700 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
701 |
show ?thesis |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
702 |
apply (unfold_locales) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
703 |
apply (simp_all add: inf_of_two_exists sup_of_two_exists) |
77362 | 704 |
apply (rule eq_is_equal) |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
705 |
done |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
706 |
qed |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
707 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
708 |
lemma (in lattice) le_iff_join: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
709 |
assumes "x \<in> carrier L" "y \<in> carrier L" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
710 |
shows "x \<sqsubseteq> y \<longleftrightarrow> x = (x \<sqinter> y)" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
711 |
by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
712 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
713 |
lemma (in lattice) le_iff_meet: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
714 |
assumes "x \<in> carrier L" "y \<in> carrier L" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
715 |
shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) = y" |
77362 | 716 |
by (simp add: assms eq_is_equal weak_le_iff_meet) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
717 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
718 |
text \<open> Total orders are lattices. \<close> |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
719 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
720 |
sublocale total_order \<subseteq> weak?: lattice |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
721 |
by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
722 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
723 |
text \<open>Functions that preserve joins and meets\<close> |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
724 |
|
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
725 |
definition join_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
726 |
"join_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<squnion>\<^bsub>X\<^esub> y) = f x \<squnion>\<^bsub>Y\<^esub> f y)" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
727 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
728 |
definition meet_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
729 |
"meet_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<sqinter>\<^bsub>X\<^esub> y) = f x \<sqinter>\<^bsub>Y\<^esub> f y)" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
730 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
731 |
lemma join_pres_isotone: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
732 |
assumes "f \<in> carrier X \<rightarrow> carrier Y" "join_pres X Y f" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
733 |
shows "isotone X Y f" |
77362 | 734 |
proof (rule isotoneI) |
735 |
show "weak_partial_order X" "weak_partial_order Y" |
|
736 |
using assms unfolding join_pres_def lattice_def upper_semilattice_def lower_semilattice_def |
|
737 |
by (meson partial_order.axioms(1))+ |
|
738 |
show "\<And>x y. \<lbrakk>x \<in> carrier X; y \<in> carrier X; x \<sqsubseteq>\<^bsub>X\<^esub> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq>\<^bsub>Y\<^esub> f y" |
|
739 |
by (metis (no_types, lifting) PiE assms join_pres_def lattice.le_iff_meet) |
|
740 |
qed |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
741 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
742 |
lemma meet_pres_isotone: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
743 |
assumes "f \<in> carrier X \<rightarrow> carrier Y" "meet_pres X Y f" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
744 |
shows "isotone X Y f" |
77362 | 745 |
proof (rule isotoneI) |
746 |
show "weak_partial_order X" "weak_partial_order Y" |
|
747 |
using assms unfolding meet_pres_def lattice_def upper_semilattice_def lower_semilattice_def |
|
748 |
by (meson partial_order.axioms(1))+ |
|
749 |
show "\<And>x y. \<lbrakk>x \<in> carrier X; y \<in> carrier X; x \<sqsubseteq>\<^bsub>X\<^esub> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq>\<^bsub>Y\<^esub> f y" |
|
750 |
by (metis (no_types, lifting) PiE assms lattice.le_iff_join meet_pres_def) |
|
751 |
qed |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
752 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
753 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
754 |
subsection \<open>Bounded Lattices\<close> |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
755 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
756 |
locale bounded_lattice = |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
757 |
lattice + |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
758 |
weak_partial_order_bottom + |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
759 |
weak_partial_order_top |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
760 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
761 |
sublocale bounded_lattice \<subseteq> weak_bounded_lattice .. |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset
|
762 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
763 |
context bounded_lattice |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
764 |
begin |
14551 | 765 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
766 |
lemma bottom_eq: |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
767 |
"\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b = \<bottom>" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
768 |
by (metis bottom_closed bottom_lower le_antisym) |
14551 | 769 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
770 |
lemma top_eq: "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>" |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
771 |
by (metis le_antisym top_closed top_higher) |
14551 | 772 |
|
14693 | 773 |
end |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
774 |
|
69700
7a92cbec7030
new material about summations and powers, along with some tweaks
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
775 |
hide_const (open) Lattice.inf |
7a92cbec7030
new material about summations and powers, along with some tweaks
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
776 |
hide_const (open) Lattice.sup |
7a92cbec7030
new material about summations and powers, along with some tweaks
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
777 |
|
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
63167
diff
changeset
|
778 |
end |