23 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
23 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
24 |
24 |
25 |
25 |
26 subsection {* Predicates as (complete) lattices *} |
26 subsection {* Predicates as (complete) lattices *} |
27 |
27 |
28 text {* |
|
29 Handy introduction and elimination rules for @{text "\<le>"} |
|
30 on unary and binary predicates |
|
31 *} |
|
32 |
|
33 lemma predicate1I: |
|
34 assumes PQ: "\<And>x. P x \<Longrightarrow> Q x" |
|
35 shows "P \<le> Q" |
|
36 apply (rule le_funI) |
|
37 apply (rule le_boolI) |
|
38 apply (rule PQ) |
|
39 apply assumption |
|
40 done |
|
41 |
|
42 lemma predicate1D [Pure.dest?, dest?]: |
|
43 "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x" |
|
44 apply (erule le_funE) |
|
45 apply (erule le_boolE) |
|
46 apply assumption+ |
|
47 done |
|
48 |
|
49 lemma rev_predicate1D: |
|
50 "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x" |
|
51 by (rule predicate1D) |
|
52 |
|
53 lemma predicate2I [Pure.intro!, intro!]: |
|
54 assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y" |
|
55 shows "P \<le> Q" |
|
56 apply (rule le_funI)+ |
|
57 apply (rule le_boolI) |
|
58 apply (rule PQ) |
|
59 apply assumption |
|
60 done |
|
61 |
|
62 lemma predicate2D [Pure.dest, dest]: |
|
63 "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y" |
|
64 apply (erule le_funE)+ |
|
65 apply (erule le_boolE) |
|
66 apply assumption+ |
|
67 done |
|
68 |
|
69 lemma rev_predicate2D: |
|
70 "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y" |
|
71 by (rule predicate2D) |
|
72 |
|
73 |
|
74 subsubsection {* Equality *} |
28 subsubsection {* Equality *} |
75 |
29 |
76 lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)" |
30 lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)" |
77 by (simp add: set_eq_iff fun_eq_iff) |
31 by (simp add: set_eq_iff fun_eq_iff) |
78 |
32 |
89 by (simp add: subset_iff le_fun_def) |
43 by (simp add: subset_iff le_fun_def) |
90 |
44 |
91 |
45 |
92 subsubsection {* Top and bottom elements *} |
46 subsubsection {* Top and bottom elements *} |
93 |
47 |
94 lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P" |
|
95 by (simp add: bot_fun_def) |
|
96 |
|
97 lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P" |
|
98 by (simp add: bot_fun_def) |
|
99 |
|
100 lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})" |
48 lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})" |
101 by (auto simp add: fun_eq_iff) |
49 by (auto simp add: fun_eq_iff) |
102 |
50 |
103 lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})" |
51 lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})" |
104 by (auto simp add: fun_eq_iff) |
52 by (auto simp add: fun_eq_iff) |
105 |
53 |
106 lemma top1I [intro!]: "\<top> x" |
|
107 by (simp add: top_fun_def) |
|
108 |
|
109 lemma top2I [intro!]: "\<top> x y" |
|
110 by (simp add: top_fun_def) |
|
111 |
|
112 |
54 |
113 subsubsection {* Binary intersection *} |
55 subsubsection {* Binary intersection *} |
114 |
|
115 lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x" |
|
116 by (simp add: inf_fun_def) |
|
117 |
|
118 lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y" |
|
119 by (simp add: inf_fun_def) |
|
120 |
|
121 lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P" |
|
122 by (simp add: inf_fun_def) |
|
123 |
|
124 lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P" |
|
125 by (simp add: inf_fun_def) |
|
126 |
|
127 lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x" |
|
128 by (simp add: inf_fun_def) |
|
129 |
|
130 lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y" |
|
131 by (simp add: inf_fun_def) |
|
132 |
|
133 lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x" |
|
134 by (simp add: inf_fun_def) |
|
135 |
|
136 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" |
|
137 by (simp add: inf_fun_def) |
|
138 |
56 |
139 lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" |
57 lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" |
140 by (simp add: inf_fun_def) |
58 by (simp add: inf_fun_def) |
141 |
59 |
142 lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" |
60 lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" |
143 by (simp add: inf_fun_def) |
61 by (simp add: inf_fun_def) |
144 |
62 |
145 |
63 |
146 subsubsection {* Binary union *} |
64 subsubsection {* Binary union *} |
147 |
65 |
148 lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x" |
|
149 by (simp add: sup_fun_def) |
|
150 |
|
151 lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y" |
|
152 by (simp add: sup_fun_def) |
|
153 |
|
154 lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x" |
|
155 by (simp add: sup_fun_def) |
|
156 |
|
157 lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y" |
|
158 by (simp add: sup_fun_def) |
|
159 |
|
160 lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P" |
|
161 by (simp add: sup_fun_def) iprover |
|
162 |
|
163 lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P" |
|
164 by (simp add: sup_fun_def) iprover |
|
165 |
|
166 text {* |
|
167 \medskip Classical introduction rule: no commitment to @{text A} vs |
|
168 @{text B}. |
|
169 *} |
|
170 |
|
171 lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x" |
|
172 by (auto simp add: sup_fun_def) |
|
173 |
|
174 lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y" |
|
175 by (auto simp add: sup_fun_def) |
|
176 |
|
177 lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" |
66 lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" |
178 by (simp add: sup_fun_def) |
67 by (simp add: sup_fun_def) |
179 |
68 |
180 lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" |
69 lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" |
181 by (simp add: sup_fun_def) |
70 by (simp add: sup_fun_def) |
182 |
71 |
183 |
72 |
184 subsubsection {* Intersections of families *} |
73 subsubsection {* Intersections of families *} |
185 |
74 |
186 lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)" |
75 lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))" |
187 by (simp add: INF_apply) |
|
188 |
|
189 lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)" |
|
190 by (simp add: INF_apply) |
|
191 |
|
192 lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b" |
|
193 by (auto simp add: INF_apply) |
|
194 |
|
195 lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c" |
|
196 by (auto simp add: INF_apply) |
|
197 |
|
198 lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b" |
|
199 by (auto simp add: INF_apply) |
|
200 |
|
201 lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c" |
|
202 by (auto simp add: INF_apply) |
|
203 |
|
204 lemma INF1_E [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R" |
|
205 by (auto simp add: INF_apply) |
|
206 |
|
207 lemma INF2_E [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R" |
|
208 by (auto simp add: INF_apply) |
|
209 |
|
210 lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))" |
|
211 by (simp add: INF_apply fun_eq_iff) |
76 by (simp add: INF_apply fun_eq_iff) |
212 |
77 |
213 lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))" |
78 lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))" |
214 by (simp add: INF_apply fun_eq_iff) |
79 by (simp add: INF_apply fun_eq_iff) |
215 |
80 |
216 |
81 |
217 subsubsection {* Unions of families *} |
82 subsubsection {* Unions of families *} |
218 |
|
219 lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)" |
|
220 by (simp add: SUP_apply) |
|
221 |
|
222 lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)" |
|
223 by (simp add: SUP_apply) |
|
224 |
|
225 lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b" |
|
226 by (auto simp add: SUP_apply) |
|
227 |
|
228 lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c" |
|
229 by (auto simp add: SUP_apply) |
|
230 |
|
231 lemma SUP1_E [elim!]: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R" |
|
232 by (auto simp add: SUP_apply) |
|
233 |
|
234 lemma SUP2_E [elim!]: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R" |
|
235 by (auto simp add: SUP_apply) |
|
236 |
83 |
237 lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))" |
84 lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))" |
238 by (simp add: SUP_apply fun_eq_iff) |
85 by (simp add: SUP_apply fun_eq_iff) |
239 |
86 |
240 lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))" |
87 lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))" |