author | wenzelm |
Fri, 09 Nov 2001 00:09:47 +0100 | |
changeset 12114 | a8e860c86252 |
parent 12023 | d982f98e0f0d |
child 12257 | e3f7d6fb55d7 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Set.thy |
2 |
ID: $Id$ |
|
12020 | 3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
923 | 5 |
*) |
6 |
||
11979 | 7 |
header {* Set theory for higher-order logic *} |
8 |
||
9 |
theory Set = HOL |
|
10 |
files ("subset.ML") ("equalities.ML") ("mono.ML"): |
|
11 |
||
12 |
text {* A set in HOL is simply a predicate. *} |
|
923 | 13 |
|
2261 | 14 |
|
11979 | 15 |
subsection {* Basic syntax *} |
2261 | 16 |
|
3947 | 17 |
global |
18 |
||
11979 | 19 |
typedecl 'a set |
20 |
arities set :: ("term") "term" |
|
3820 | 21 |
|
923 | 22 |
consts |
11979 | 23 |
"{}" :: "'a set" ("{}") |
24 |
UNIV :: "'a set" |
|
25 |
insert :: "'a => 'a set => 'a set" |
|
26 |
Collect :: "('a => bool) => 'a set" -- "comprehension" |
|
27 |
Int :: "'a set => 'a set => 'a set" (infixl 70) |
|
28 |
Un :: "'a set => 'a set => 'a set" (infixl 65) |
|
29 |
UNION :: "'a set => ('a => 'b set) => 'b set" -- "general union" |
|
30 |
INTER :: "'a set => ('a => 'b set) => 'b set" -- "general intersection" |
|
31 |
Union :: "'a set set => 'a set" -- "union of a set" |
|
32 |
Inter :: "'a set set => 'a set" -- "intersection of a set" |
|
33 |
Pow :: "'a set => 'a set set" -- "powerset" |
|
34 |
Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers" |
|
35 |
Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers" |
|
36 |
image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) |
|
37 |
||
38 |
syntax |
|
39 |
"op :" :: "'a => 'a set => bool" ("op :") |
|
40 |
consts |
|
41 |
"op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50) -- "membership" |
|
42 |
||
43 |
local |
|
44 |
||
45 |
instance set :: ("term") ord .. |
|
46 |
instance set :: ("term") minus .. |
|
923 | 47 |
|
48 |
||
11979 | 49 |
subsection {* Additional concrete syntax *} |
2261 | 50 |
|
923 | 51 |
syntax |
11979 | 52 |
range :: "('a => 'b) => 'b set" -- "of function" |
923 | 53 |
|
11979 | 54 |
"op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership" |
55 |
"op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50) |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
56 |
|
11979 | 57 |
"@Finset" :: "args => 'a set" ("{(_)}") |
58 |
"@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") |
|
59 |
"@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})") |
|
923 | 60 |
|
11979 | 61 |
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" 10) |
62 |
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10) |
|
63 |
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10) |
|
64 |
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10) |
|
923 | 65 |
|
11979 | 66 |
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10) |
67 |
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10) |
|
923 | 68 |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
69 |
syntax (HOL) |
11979 | 70 |
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10) |
71 |
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10) |
|
923 | 72 |
|
73 |
translations |
|
10832 | 74 |
"range f" == "f`UNIV" |
923 | 75 |
"x ~: y" == "~ (x : y)" |
76 |
"{x, xs}" == "insert x {xs}" |
|
77 |
"{x}" == "insert x {}" |
|
78 |
"{x. P}" == "Collect (%x. P)" |
|
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset
|
79 |
"UN x y. B" == "UN x. UN y. B" |
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset
|
80 |
"UN x. B" == "UNION UNIV (%x. B)" |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
81 |
"INT x y. B" == "INT x. INT y. B" |
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset
|
82 |
"INT x. B" == "INTER UNIV (%x. B)" |
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset
|
83 |
"UN x:A. B" == "UNION A (%x. B)" |
923 | 84 |
"INT x:A. B" == "INTER A (%x. B)" |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
85 |
"ALL x:A. P" == "Ball A (%x. P)" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
86 |
"EX x:A. P" == "Bex A (%x. P)" |
923 | 87 |
|
2388 | 88 |
syntax ("" output) |
11979 | 89 |
"_setle" :: "'a set => 'a set => bool" ("op <=") |
90 |
"_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50) |
|
91 |
"_setless" :: "'a set => 'a set => bool" ("op <") |
|
92 |
"_setless" :: "'a set => 'a set => bool" ("(_/ < _)" [50, 51] 50) |
|
923 | 93 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset
|
94 |
syntax (xsymbols) |
11979 | 95 |
"_setle" :: "'a set => 'a set => bool" ("op \<subseteq>") |
96 |
"_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50) |
|
97 |
"_setless" :: "'a set => 'a set => bool" ("op \<subset>") |
|
98 |
"_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50) |
|
99 |
"op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70) |
|
100 |
"op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65) |
|
101 |
"op :" :: "'a => 'a set => bool" ("op \<in>") |
|
102 |
"op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50) |
|
103 |
"op ~:" :: "'a => 'a set => bool" ("op \<notin>") |
|
104 |
"op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50) |
|
105 |
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10) |
|
106 |
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10) |
|
107 |
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" 10) |
|
108 |
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10) |
|
109 |
Union :: "'a set set => 'a set" ("\<Union>_" [90] 90) |
|
110 |
Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90) |
|
111 |
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10) |
|
112 |
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10) |
|
2261 | 113 |
|
2412 | 114 |
translations |
11979 | 115 |
"op \<subseteq>" => "op <= :: _ set => _ set => bool" |
116 |
"op \<subset>" => "op < :: _ set => _ set => bool" |
|
2261 | 117 |
|
118 |
||
11979 | 119 |
typed_print_translation {* |
120 |
let |
|
121 |
fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = |
|
122 |
list_comb (Syntax.const "_setle", ts) |
|
123 |
| le_tr' _ _ _ = raise Match; |
|
124 |
||
125 |
fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = |
|
126 |
list_comb (Syntax.const "_setless", ts) |
|
127 |
| less_tr' _ _ _ = raise Match; |
|
128 |
in [("op <=", le_tr'), ("op <", less_tr')] end |
|
129 |
*} |
|
2261 | 130 |
|
11979 | 131 |
text {* |
132 |
\medskip Translate between @{text "{e | x1...xn. P}"} and @{text |
|
133 |
"{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is |
|
134 |
only translated if @{text "[0..n] subset bvs(e)"}. |
|
135 |
*} |
|
136 |
||
137 |
parse_translation {* |
|
138 |
let |
|
139 |
val ex_tr = snd (mk_binder_tr ("EX ", "Ex")); |
|
3947 | 140 |
|
11979 | 141 |
fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1 |
142 |
| nvars _ = 1; |
|
143 |
||
144 |
fun setcompr_tr [e, idts, b] = |
|
145 |
let |
|
146 |
val eq = Syntax.const "op =" $ Bound (nvars idts) $ e; |
|
147 |
val P = Syntax.const "op &" $ eq $ b; |
|
148 |
val exP = ex_tr [idts, P]; |
|
149 |
in Syntax.const "Collect" $ Abs ("", dummyT, exP) end; |
|
150 |
||
151 |
in [("@SetCompr", setcompr_tr)] end; |
|
152 |
*} |
|
923 | 153 |
|
11979 | 154 |
print_translation {* |
155 |
let |
|
156 |
val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY")); |
|
157 |
||
158 |
fun setcompr_tr' [Abs (_, _, P)] = |
|
159 |
let |
|
160 |
fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1) |
|
161 |
| check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) = |
|
162 |
if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso |
|
163 |
((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) then () |
|
164 |
else raise Match; |
|
923 | 165 |
|
11979 | 166 |
fun tr' (_ $ abs) = |
167 |
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs] |
|
168 |
in Syntax.const "@SetCompr" $ e $ idts $ Q end; |
|
169 |
in check (P, 0); tr' P end; |
|
170 |
in [("Collect", setcompr_tr')] end; |
|
171 |
*} |
|
172 |
||
173 |
||
174 |
subsection {* Rules and definitions *} |
|
175 |
||
176 |
text {* Isomorphisms between predicates and sets. *} |
|
923 | 177 |
|
11979 | 178 |
axioms |
179 |
mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)" |
|
180 |
Collect_mem_eq [simp]: "{x. x:A} = A" |
|
181 |
||
182 |
defs |
|
183 |
Ball_def: "Ball A P == ALL x. x:A --> P(x)" |
|
184 |
Bex_def: "Bex A P == EX x. x:A & P(x)" |
|
185 |
||
186 |
defs (overloaded) |
|
187 |
subset_def: "A <= B == ALL x:A. x:B" |
|
188 |
psubset_def: "A < B == (A::'a set) <= B & ~ A=B" |
|
189 |
Compl_def: "- A == {x. ~x:A}" |
|
923 | 190 |
|
191 |
defs |
|
11979 | 192 |
Un_def: "A Un B == {x. x:A | x:B}" |
193 |
Int_def: "A Int B == {x. x:A & x:B}" |
|
194 |
set_diff_def: "A - B == {x. x:A & ~x:B}" |
|
195 |
INTER_def: "INTER A B == {y. ALL x:A. y: B(x)}" |
|
196 |
UNION_def: "UNION A B == {y. EX x:A. y: B(x)}" |
|
197 |
Inter_def: "Inter S == (INT x:S. x)" |
|
198 |
Union_def: "Union S == (UN x:S. x)" |
|
199 |
Pow_def: "Pow A == {B. B <= A}" |
|
200 |
empty_def: "{} == {x. False}" |
|
201 |
UNIV_def: "UNIV == {x. True}" |
|
202 |
insert_def: "insert a B == {x. x=a} Un B" |
|
203 |
image_def: "f`A == {y. EX x:A. y = f(x)}" |
|
204 |
||
205 |
||
206 |
subsection {* Lemmas and proof tool setup *} |
|
207 |
||
208 |
subsubsection {* Relating predicates and sets *} |
|
209 |
||
210 |
lemma CollectI [intro!]: "P(a) ==> a : {x. P(x)}" |
|
211 |
by simp |
|
212 |
||
213 |
lemma CollectD: "a : {x. P(x)} ==> P(a)" |
|
214 |
by simp |
|
215 |
||
216 |
lemma set_ext: "(!!x. (x:A) = (x:B)) ==> A = B" |
|
217 |
proof - |
|
218 |
case rule_context |
|
219 |
show ?thesis |
|
220 |
apply (rule prems [THEN ext, THEN arg_cong, THEN box_equals]) |
|
221 |
apply (rule Collect_mem_eq) |
|
222 |
apply (rule Collect_mem_eq) |
|
223 |
done |
|
224 |
qed |
|
225 |
||
226 |
lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}" |
|
227 |
by simp |
|
228 |
||
229 |
lemmas CollectE [elim!] = CollectD [elim_format] |
|
230 |
||
231 |
||
232 |
subsubsection {* Bounded quantifiers *} |
|
233 |
||
234 |
lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" |
|
235 |
by (simp add: Ball_def) |
|
236 |
||
237 |
lemmas strip = impI allI ballI |
|
238 |
||
239 |
lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x" |
|
240 |
by (simp add: Ball_def) |
|
241 |
||
242 |
lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" |
|
243 |
by (unfold Ball_def) blast |
|
244 |
||
245 |
text {* |
|
246 |
\medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and |
|
247 |
@{prop "a:A"}; creates assumption @{prop "P a"}. |
|
248 |
*} |
|
249 |
||
250 |
ML {* |
|
251 |
local val ballE = thm "ballE" |
|
252 |
in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end; |
|
253 |
*} |
|
254 |
||
255 |
text {* |
|
256 |
Gives better instantiation for bound: |
|
257 |
*} |
|
258 |
||
259 |
ML_setup {* |
|
260 |
claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1); |
|
261 |
*} |
|
262 |
||
263 |
lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" |
|
264 |
-- {* Normally the best argument order: @{prop "P x"} constrains the |
|
265 |
choice of @{prop "x:A"}. *} |
|
266 |
by (unfold Bex_def) blast |
|
267 |
||
268 |
lemma rev_bexI: "x:A ==> P x ==> EX x:A. P x" |
|
269 |
-- {* The best argument order when there is only one @{prop "x:A"}. *} |
|
270 |
by (unfold Bex_def) blast |
|
271 |
||
272 |
lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x" |
|
273 |
by (unfold Bex_def) blast |
|
274 |
||
275 |
lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q" |
|
276 |
by (unfold Bex_def) blast |
|
277 |
||
278 |
lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)" |
|
279 |
-- {* Trival rewrite rule. *} |
|
280 |
by (simp add: Ball_def) |
|
281 |
||
282 |
lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)" |
|
283 |
-- {* Dual form for existentials. *} |
|
284 |
by (simp add: Bex_def) |
|
285 |
||
286 |
lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)" |
|
287 |
by blast |
|
288 |
||
289 |
lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)" |
|
290 |
by blast |
|
291 |
||
292 |
lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)" |
|
293 |
by blast |
|
294 |
||
295 |
lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)" |
|
296 |
by blast |
|
297 |
||
298 |
lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)" |
|
299 |
by blast |
|
300 |
||
301 |
lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)" |
|
302 |
by blast |
|
303 |
||
304 |
ML_setup {* |
|
305 |
let |
|
306 |
val Ball_def = thm "Ball_def"; |
|
307 |
val Bex_def = thm "Bex_def"; |
|
308 |
||
309 |
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
|
310 |
("EX x:A. P x & Q x", HOLogic.boolT); |
|
311 |
||
312 |
val prove_bex_tac = |
|
313 |
rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac; |
|
314 |
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; |
|
315 |
||
316 |
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
|
317 |
("ALL x:A. P x --> Q x", HOLogic.boolT); |
|
318 |
||
319 |
val prove_ball_tac = |
|
320 |
rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac; |
|
321 |
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; |
|
322 |
||
323 |
val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; |
|
324 |
val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball; |
|
325 |
in |
|
326 |
Addsimprocs [defBALL_regroup, defBEX_regroup] |
|
327 |
end; |
|
328 |
*} |
|
329 |
||
330 |
||
331 |
subsubsection {* Congruence rules *} |
|
332 |
||
333 |
lemma ball_cong [cong]: |
|
334 |
"A = B ==> (!!x. x:B ==> P x = Q x) ==> |
|
335 |
(ALL x:A. P x) = (ALL x:B. Q x)" |
|
336 |
by (simp add: Ball_def) |
|
337 |
||
338 |
lemma bex_cong [cong]: |
|
339 |
"A = B ==> (!!x. x:B ==> P x = Q x) ==> |
|
340 |
(EX x:A. P x) = (EX x:B. Q x)" |
|
341 |
by (simp add: Bex_def cong: conj_cong) |
|
1273 | 342 |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
343 |
|
11979 | 344 |
subsubsection {* Subsets *} |
345 |
||
346 |
lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B" |
|
347 |
by (simp add: subset_def) |
|
348 |
||
349 |
text {* |
|
350 |
\medskip Map the type @{text "'a set => anything"} to just @{typ |
|
351 |
'a}; for overloading constants whose first argument has type @{typ |
|
352 |
"'a set"}. |
|
353 |
*} |
|
354 |
||
355 |
ML {* |
|
356 |
fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type); |
|
357 |
*} |
|
358 |
||
359 |
ML " |
|
360 |
(* While (:) is not, its type must be kept |
|
361 |
for overloading of = to work. *) |
|
362 |
Blast.overloaded (\"op :\", domain_type); |
|
363 |
||
364 |
overload_1st_set \"Ball\"; (*need UNION, INTER also?*) |
|
365 |
overload_1st_set \"Bex\"; |
|
366 |
||
367 |
(*Image: retain the type of the set being expressed*) |
|
368 |
Blast.overloaded (\"image\", domain_type); |
|
369 |
" |
|
370 |
||
371 |
lemma subsetD [elim]: "A <= B ==> c:A ==> c:B" |
|
372 |
-- {* Rule in Modus Ponens style. *} |
|
373 |
by (unfold subset_def) blast |
|
374 |
||
375 |
declare subsetD [intro?] -- FIXME |
|
376 |
||
377 |
lemma rev_subsetD: "c:A ==> A <= B ==> c:B" |
|
378 |
-- {* The same, with reversed premises for use with @{text erule} -- |
|
379 |
cf @{text rev_mp}. *} |
|
380 |
by (rule subsetD) |
|
381 |
||
382 |
declare rev_subsetD [intro?] -- FIXME |
|
383 |
||
384 |
text {* |
|
385 |
\medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}. |
|
386 |
*} |
|
387 |
||
388 |
ML {* |
|
389 |
local val rev_subsetD = thm "rev_subsetD" |
|
390 |
in fun impOfSubs th = th RSN (2, rev_subsetD) end; |
|
391 |
*} |
|
392 |
||
393 |
lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P" |
|
394 |
-- {* Classical elimination rule. *} |
|
395 |
by (unfold subset_def) blast |
|
396 |
||
397 |
text {* |
|
398 |
\medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and |
|
399 |
creates the assumption @{prop "c:B"}. |
|
400 |
*} |
|
401 |
||
402 |
ML {* |
|
403 |
local val subsetCE = thm "subsetCE" |
|
404 |
in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end; |
|
405 |
*} |
|
406 |
||
407 |
lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A" |
|
408 |
by blast |
|
409 |
||
410 |
lemma subset_refl: "A <= (A::'a set)" |
|
411 |
by fast |
|
412 |
||
413 |
lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)" |
|
414 |
by blast |
|
923 | 415 |
|
2261 | 416 |
|
11979 | 417 |
subsubsection {* Equality *} |
418 |
||
419 |
lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)" |
|
420 |
-- {* Anti-symmetry of the subset relation. *} |
|
421 |
by (rule set_ext) (blast intro: subsetD) |
|
422 |
||
423 |
lemmas equalityI = subset_antisym |
|
424 |
||
425 |
text {* |
|
426 |
\medskip Equality rules from ZF set theory -- are they appropriate |
|
427 |
here? |
|
428 |
*} |
|
429 |
||
430 |
lemma equalityD1: "A = B ==> A <= (B::'a set)" |
|
431 |
by (simp add: subset_refl) |
|
432 |
||
433 |
lemma equalityD2: "A = B ==> B <= (A::'a set)" |
|
434 |
by (simp add: subset_refl) |
|
435 |
||
436 |
text {* |
|
437 |
\medskip Be careful when adding this to the claset as @{text |
|
438 |
subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{} |
|
439 |
<= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}! |
|
440 |
*} |
|
441 |
||
442 |
lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P" |
|
443 |
by (simp add: subset_refl) |
|
923 | 444 |
|
11979 | 445 |
lemma equalityCE [elim]: |
446 |
"A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P" |
|
447 |
by blast |
|
448 |
||
449 |
text {* |
|
450 |
\medskip Lemma for creating induction formulae -- for "pattern |
|
451 |
matching" on @{text p}. To make the induction hypotheses usable, |
|
452 |
apply @{text spec} or @{text bspec} to put universal quantifiers over the free |
|
453 |
variables in @{text p}. |
|
454 |
*} |
|
455 |
||
456 |
lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z --> R) ==> R" |
|
457 |
by simp |
|
923 | 458 |
|
11979 | 459 |
lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)" |
460 |
by simp |
|
461 |
||
462 |
||
463 |
subsubsection {* The universal set -- UNIV *} |
|
464 |
||
465 |
lemma UNIV_I [simp]: "x : UNIV" |
|
466 |
by (simp add: UNIV_def) |
|
467 |
||
468 |
declare UNIV_I [intro] -- {* unsafe makes it less likely to cause problems *} |
|
469 |
||
470 |
lemma UNIV_witness [intro?]: "EX x. x : UNIV" |
|
471 |
by simp |
|
472 |
||
473 |
lemma subset_UNIV: "A <= UNIV" |
|
474 |
by (rule subsetI) (rule UNIV_I) |
|
2388 | 475 |
|
11979 | 476 |
text {* |
477 |
\medskip Eta-contracting these two rules (to remove @{text P}) |
|
478 |
causes them to be ignored because of their interaction with |
|
479 |
congruence rules. |
|
480 |
*} |
|
481 |
||
482 |
lemma ball_UNIV [simp]: "Ball UNIV P = All P" |
|
483 |
by (simp add: Ball_def) |
|
484 |
||
485 |
lemma bex_UNIV [simp]: "Bex UNIV P = Ex P" |
|
486 |
by (simp add: Bex_def) |
|
487 |
||
488 |
||
489 |
subsubsection {* The empty set *} |
|
490 |
||
491 |
lemma empty_iff [simp]: "(c : {}) = False" |
|
492 |
by (simp add: empty_def) |
|
493 |
||
494 |
lemma emptyE [elim!]: "a : {} ==> P" |
|
495 |
by simp |
|
496 |
||
497 |
lemma empty_subsetI [iff]: "{} <= A" |
|
498 |
-- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *} |
|
499 |
by blast |
|
500 |
||
501 |
lemma equals0I: "(!!y. y:A ==> False) ==> A = {}" |
|
502 |
by blast |
|
2388 | 503 |
|
11979 | 504 |
lemma equals0D: "A={} ==> a ~: A" |
505 |
-- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *} |
|
506 |
by blast |
|
507 |
||
508 |
lemma ball_empty [simp]: "Ball {} P = True" |
|
509 |
by (simp add: Ball_def) |
|
510 |
||
511 |
lemma bex_empty [simp]: "Bex {} P = False" |
|
512 |
by (simp add: Bex_def) |
|
513 |
||
514 |
lemma UNIV_not_empty [iff]: "UNIV ~= {}" |
|
515 |
by (blast elim: equalityE) |
|
516 |
||
517 |
||
12023 | 518 |
subsubsection {* The Powerset operator -- Pow *} |
11979 | 519 |
|
520 |
lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)" |
|
521 |
by (simp add: Pow_def) |
|
522 |
||
523 |
lemma PowI: "A <= B ==> A : Pow B" |
|
524 |
by (simp add: Pow_def) |
|
525 |
||
526 |
lemma PowD: "A : Pow B ==> A <= B" |
|
527 |
by (simp add: Pow_def) |
|
528 |
||
529 |
lemma Pow_bottom: "{}: Pow B" |
|
530 |
by simp |
|
531 |
||
532 |
lemma Pow_top: "A : Pow A" |
|
533 |
by (simp add: subset_refl) |
|
2684 | 534 |
|
2388 | 535 |
|
11979 | 536 |
subsubsection {* Set complement *} |
537 |
||
538 |
lemma Compl_iff [simp]: "(c : -A) = (c~:A)" |
|
539 |
by (unfold Compl_def) blast |
|
540 |
||
541 |
lemma ComplI [intro!]: "(c:A ==> False) ==> c : -A" |
|
542 |
by (unfold Compl_def) blast |
|
543 |
||
544 |
text {* |
|
545 |
\medskip This form, with negated conclusion, works well with the |
|
546 |
Classical prover. Negated assumptions behave like formulae on the |
|
547 |
right side of the notional turnstile ... *} |
|
548 |
||
549 |
lemma ComplD: "c : -A ==> c~:A" |
|
550 |
by (unfold Compl_def) blast |
|
551 |
||
552 |
lemmas ComplE [elim!] = ComplD [elim_format] |
|
553 |
||
554 |
||
555 |
subsubsection {* Binary union -- Un *} |
|
923 | 556 |
|
11979 | 557 |
lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)" |
558 |
by (unfold Un_def) blast |
|
559 |
||
560 |
lemma UnI1 [elim?]: "c:A ==> c : A Un B" |
|
561 |
by simp |
|
562 |
||
563 |
lemma UnI2 [elim?]: "c:B ==> c : A Un B" |
|
564 |
by simp |
|
923 | 565 |
|
11979 | 566 |
text {* |
567 |
\medskip Classical introduction rule: no commitment to @{prop A} vs |
|
568 |
@{prop B}. |
|
569 |
*} |
|
570 |
||
571 |
lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B" |
|
572 |
by auto |
|
573 |
||
574 |
lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P" |
|
575 |
by (unfold Un_def) blast |
|
576 |
||
577 |
||
12023 | 578 |
subsubsection {* Binary intersection -- Int *} |
923 | 579 |
|
11979 | 580 |
lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)" |
581 |
by (unfold Int_def) blast |
|
582 |
||
583 |
lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B" |
|
584 |
by simp |
|
585 |
||
586 |
lemma IntD1: "c : A Int B ==> c:A" |
|
587 |
by simp |
|
588 |
||
589 |
lemma IntD2: "c : A Int B ==> c:B" |
|
590 |
by simp |
|
591 |
||
592 |
lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P" |
|
593 |
by simp |
|
594 |
||
595 |
||
12023 | 596 |
subsubsection {* Set difference *} |
11979 | 597 |
|
598 |
lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)" |
|
599 |
by (unfold set_diff_def) blast |
|
923 | 600 |
|
11979 | 601 |
lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B" |
602 |
by simp |
|
603 |
||
604 |
lemma DiffD1: "c : A - B ==> c : A" |
|
605 |
by simp |
|
606 |
||
607 |
lemma DiffD2: "c : A - B ==> c : B ==> P" |
|
608 |
by simp |
|
609 |
||
610 |
lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P" |
|
611 |
by simp |
|
612 |
||
613 |
||
614 |
subsubsection {* Augmenting a set -- insert *} |
|
615 |
||
616 |
lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)" |
|
617 |
by (unfold insert_def) blast |
|
618 |
||
619 |
lemma insertI1: "a : insert a B" |
|
620 |
by simp |
|
621 |
||
622 |
lemma insertI2: "a : B ==> a : insert b B" |
|
623 |
by simp |
|
923 | 624 |
|
11979 | 625 |
lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P" |
626 |
by (unfold insert_def) blast |
|
627 |
||
628 |
lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B" |
|
629 |
-- {* Classical introduction rule. *} |
|
630 |
by auto |
|
631 |
||
632 |
lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A - {x} <= B else A <= B)" |
|
633 |
by auto |
|
634 |
||
635 |
||
636 |
subsubsection {* Singletons, using insert *} |
|
637 |
||
638 |
lemma singletonI [intro!]: "a : {a}" |
|
639 |
-- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *} |
|
640 |
by (rule insertI1) |
|
641 |
||
642 |
lemma singletonD: "b : {a} ==> b = a" |
|
643 |
by blast |
|
644 |
||
645 |
lemmas singletonE [elim!] = singletonD [elim_format] |
|
646 |
||
647 |
lemma singleton_iff: "(b : {a}) = (b = a)" |
|
648 |
by blast |
|
649 |
||
650 |
lemma singleton_inject [dest!]: "{a} = {b} ==> a = b" |
|
651 |
by blast |
|
652 |
||
653 |
lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})" |
|
654 |
by blast |
|
655 |
||
656 |
lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})" |
|
657 |
by blast |
|
658 |
||
659 |
lemma subset_singletonD: "A <= {x} ==> A={} | A = {x}" |
|
660 |
by fast |
|
661 |
||
662 |
lemma singleton_conv [simp]: "{x. x = a} = {a}" |
|
663 |
by blast |
|
664 |
||
665 |
lemma singleton_conv2 [simp]: "{x. a = x} = {a}" |
|
666 |
by blast |
|
923 | 667 |
|
11979 | 668 |
lemma diff_single_insert: "A - {x} <= B ==> x : A ==> A <= insert x B" |
669 |
by blast |
|
670 |
||
671 |
||
672 |
subsubsection {* Unions of families *} |
|
673 |
||
674 |
text {* |
|
675 |
@{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}. |
|
676 |
*} |
|
677 |
||
678 |
lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)" |
|
679 |
by (unfold UNION_def) blast |
|
680 |
||
681 |
lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)" |
|
682 |
-- {* The order of the premises presupposes that @{term A} is rigid; |
|
683 |
@{term b} may be flexible. *} |
|
684 |
by auto |
|
685 |
||
686 |
lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R" |
|
687 |
by (unfold UNION_def) blast |
|
923 | 688 |
|
11979 | 689 |
lemma UN_cong [cong]: |
690 |
"A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" |
|
691 |
by (simp add: UNION_def) |
|
692 |
||
693 |
||
694 |
subsubsection {* Intersections of families *} |
|
695 |
||
696 |
text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *} |
|
697 |
||
698 |
lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)" |
|
699 |
by (unfold INTER_def) blast |
|
923 | 700 |
|
11979 | 701 |
lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)" |
702 |
by (unfold INTER_def) blast |
|
703 |
||
704 |
lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a" |
|
705 |
by auto |
|
706 |
||
707 |
lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R" |
|
708 |
-- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *} |
|
709 |
by (unfold INTER_def) blast |
|
710 |
||
711 |
lemma INT_cong [cong]: |
|
712 |
"A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)" |
|
713 |
by (simp add: INTER_def) |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
714 |
|
923 | 715 |
|
11979 | 716 |
subsubsection {* Union *} |
717 |
||
718 |
lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)" |
|
719 |
by (unfold Union_def) blast |
|
720 |
||
721 |
lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C" |
|
722 |
-- {* The order of the premises presupposes that @{term C} is rigid; |
|
723 |
@{term A} may be flexible. *} |
|
724 |
by auto |
|
725 |
||
726 |
lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R" |
|
727 |
by (unfold Union_def) blast |
|
728 |
||
729 |
||
730 |
subsubsection {* Inter *} |
|
731 |
||
732 |
lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)" |
|
733 |
by (unfold Inter_def) blast |
|
734 |
||
735 |
lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" |
|
736 |
by (simp add: Inter_def) |
|
737 |
||
738 |
text {* |
|
739 |
\medskip A ``destruct'' rule -- every @{term X} in @{term C} |
|
740 |
contains @{term A} as an element, but @{prop "A:X"} can hold when |
|
741 |
@{prop "X:C"} does not! This rule is analogous to @{text spec}. |
|
742 |
*} |
|
743 |
||
744 |
lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X" |
|
745 |
by auto |
|
746 |
||
747 |
lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" |
|
748 |
-- {* ``Classical'' elimination rule -- does not require proving |
|
749 |
@{prop "X:C"}. *} |
|
750 |
by (unfold Inter_def) blast |
|
751 |
||
752 |
text {* |
|
753 |
\medskip Image of a set under a function. Frequently @{term b} does |
|
754 |
not have the syntactic form of @{term "f x"}. |
|
755 |
*} |
|
756 |
||
757 |
lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A" |
|
758 |
by (unfold image_def) blast |
|
759 |
||
760 |
lemma imageI: "x : A ==> f x : f ` A" |
|
761 |
by (rule image_eqI) (rule refl) |
|
762 |
||
763 |
lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A" |
|
764 |
-- {* This version's more effective when we already have the |
|
765 |
required @{term x}. *} |
|
766 |
by (unfold image_def) blast |
|
767 |
||
768 |
lemma imageE [elim!]: |
|
769 |
"b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P" |
|
770 |
-- {* The eta-expansion gives variable-name preservation. *} |
|
771 |
by (unfold image_def) blast |
|
772 |
||
773 |
lemma image_Un: "f`(A Un B) = f`A Un f`B" |
|
774 |
by blast |
|
775 |
||
776 |
lemma image_iff: "(z : f`A) = (EX x:A. z = f x)" |
|
777 |
by blast |
|
778 |
||
779 |
lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)" |
|
780 |
-- {* This rewrite rule would confuse users if made default. *} |
|
781 |
by blast |
|
782 |
||
783 |
lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)" |
|
784 |
apply safe |
|
785 |
prefer 2 apply fast |
|
786 |
apply (rule_tac x = "{a. a : A & f a : B}" in exI) |
|
787 |
apply fast |
|
788 |
done |
|
789 |
||
790 |
lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B" |
|
791 |
-- {* Replaces the three steps @{text subsetI}, @{text imageE}, |
|
792 |
@{text hypsubst}, but breaks too many existing proofs. *} |
|
793 |
by blast |
|
794 |
||
795 |
text {* |
|
796 |
\medskip Range of a function -- just a translation for image! |
|
797 |
*} |
|
798 |
||
799 |
lemma range_eqI: "b = f x ==> b : range f" |
|
800 |
by simp |
|
801 |
||
802 |
lemma rangeI: "f x : range f" |
|
803 |
by simp |
|
804 |
||
805 |
lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P" |
|
806 |
by blast |
|
807 |
||
808 |
||
809 |
subsubsection {* Set reasoning tools *} |
|
810 |
||
811 |
text {* |
|
812 |
Rewrite rules for boolean case-splitting: faster than @{text |
|
813 |
"split_if [split]"}. |
|
814 |
*} |
|
815 |
||
816 |
lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))" |
|
817 |
by (rule split_if) |
|
818 |
||
819 |
lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))" |
|
820 |
by (rule split_if) |
|
821 |
||
822 |
text {* |
|
823 |
Split ifs on either side of the membership relation. Not for @{text |
|
824 |
"[simp]"} -- can cause goals to blow up! |
|
825 |
*} |
|
826 |
||
827 |
lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))" |
|
828 |
by (rule split_if) |
|
829 |
||
830 |
lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))" |
|
831 |
by (rule split_if) |
|
832 |
||
833 |
lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 |
|
834 |
||
835 |
lemmas mem_simps = |
|
836 |
insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff |
|
837 |
mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff |
|
838 |
-- {* Each of these has ALREADY been added @{text "[simp]"} above. *} |
|
839 |
||
840 |
(*Would like to add these, but the existing code only searches for the |
|
841 |
outer-level constant, which in this case is just "op :"; we instead need |
|
842 |
to use term-nets to associate patterns with rules. Also, if a rule fails to |
|
843 |
apply, then the formula should be kept. |
|
844 |
[("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]), |
|
845 |
("op Int", [IntD1,IntD2]), |
|
846 |
("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] |
|
847 |
*) |
|
848 |
||
849 |
ML_setup {* |
|
850 |
val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs; |
|
851 |
simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs); |
|
852 |
*} |
|
853 |
||
854 |
declare subset_UNIV [simp] subset_refl [simp] |
|
855 |
||
856 |
||
857 |
subsubsection {* The ``proper subset'' relation *} |
|
858 |
||
859 |
lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B" |
|
860 |
by (unfold psubset_def) blast |
|
861 |
||
862 |
lemma psubset_insert_iff: |
|
863 |
"(A < insert x B) = (if x:B then A < B else if x:A then A - {x} < B else A <= B)" |
|
864 |
apply (simp add: psubset_def subset_insert_iff) |
|
865 |
apply blast |
|
866 |
done |
|
867 |
||
868 |
lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)" |
|
869 |
by (simp only: psubset_def) |
|
870 |
||
871 |
lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B" |
|
872 |
by (simp add: psubset_eq) |
|
873 |
||
874 |
lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C" |
|
875 |
by (auto simp add: psubset_eq) |
|
876 |
||
877 |
lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C" |
|
878 |
by (auto simp add: psubset_eq) |
|
879 |
||
880 |
lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)" |
|
881 |
by (unfold psubset_def) blast |
|
882 |
||
883 |
lemma atomize_ball: |
|
884 |
"(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)" |
|
885 |
by (simp only: Ball_def atomize_all atomize_imp) |
|
886 |
||
887 |
declare atomize_ball [symmetric, rulify] |
|
888 |
||
889 |
||
890 |
subsection {* Further set-theory lemmas *} |
|
891 |
||
892 |
use "subset.ML" |
|
893 |
use "equalities.ML" |
|
894 |
use "mono.ML" |
|
895 |
||
11982
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
896 |
lemma Least_mono: |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
897 |
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
898 |
==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
899 |
-- {* Courtesy of Stephan Merz *} |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
900 |
apply clarify |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
901 |
apply (erule_tac P = "%x. x : S" in LeastI2) |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
902 |
apply fast |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
903 |
apply (rule LeastI2) |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
904 |
apply (auto elim: monoD intro!: order_antisym) |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
905 |
done |
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset
|
906 |
|
12020 | 907 |
|
12023 | 908 |
subsection {* Transitivity rules for calculational reasoning *} |
12020 | 909 |
|
910 |
lemma forw_subst: "a = b ==> P b ==> P a" |
|
911 |
by (rule ssubst) |
|
912 |
||
913 |
lemma back_subst: "P a ==> a = b ==> P b" |
|
914 |
by (rule subst) |
|
915 |
||
916 |
lemma set_rev_mp: "x:A ==> A <= B ==> x:B" |
|
917 |
by (rule subsetD) |
|
918 |
||
919 |
lemma set_mp: "A <= B ==> x:A ==> x:B" |
|
920 |
by (rule subsetD) |
|
921 |
||
922 |
lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b" |
|
923 |
by (simp add: order_less_le) |
|
924 |
||
925 |
lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b" |
|
926 |
by (simp add: order_less_le) |
|
927 |
||
928 |
lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P" |
|
929 |
by (rule order_less_asym) |
|
930 |
||
931 |
lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" |
|
932 |
by (rule subst) |
|
933 |
||
934 |
lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" |
|
935 |
by (rule ssubst) |
|
936 |
||
937 |
lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" |
|
938 |
by (rule subst) |
|
939 |
||
940 |
lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" |
|
941 |
by (rule ssubst) |
|
942 |
||
943 |
lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> |
|
944 |
(!!x y. x < y ==> f x < f y) ==> f a < c" |
|
945 |
proof - |
|
946 |
assume r: "!!x y. x < y ==> f x < f y" |
|
947 |
assume "a < b" hence "f a < f b" by (rule r) |
|
948 |
also assume "f b < c" |
|
949 |
finally (order_less_trans) show ?thesis . |
|
950 |
qed |
|
951 |
||
952 |
lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> |
|
953 |
(!!x y. x < y ==> f x < f y) ==> a < f c" |
|
954 |
proof - |
|
955 |
assume r: "!!x y. x < y ==> f x < f y" |
|
956 |
assume "a < f b" |
|
957 |
also assume "b < c" hence "f b < f c" by (rule r) |
|
958 |
finally (order_less_trans) show ?thesis . |
|
959 |
qed |
|
960 |
||
961 |
lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> |
|
962 |
(!!x y. x <= y ==> f x <= f y) ==> f a < c" |
|
963 |
proof - |
|
964 |
assume r: "!!x y. x <= y ==> f x <= f y" |
|
965 |
assume "a <= b" hence "f a <= f b" by (rule r) |
|
966 |
also assume "f b < c" |
|
967 |
finally (order_le_less_trans) show ?thesis . |
|
968 |
qed |
|
969 |
||
970 |
lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> |
|
971 |
(!!x y. x < y ==> f x < f y) ==> a < f c" |
|
972 |
proof - |
|
973 |
assume r: "!!x y. x < y ==> f x < f y" |
|
974 |
assume "a <= f b" |
|
975 |
also assume "b < c" hence "f b < f c" by (rule r) |
|
976 |
finally (order_le_less_trans) show ?thesis . |
|
977 |
qed |
|
978 |
||
979 |
lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> |
|
980 |
(!!x y. x < y ==> f x < f y) ==> f a < c" |
|
981 |
proof - |
|
982 |
assume r: "!!x y. x < y ==> f x < f y" |
|
983 |
assume "a < b" hence "f a < f b" by (rule r) |
|
984 |
also assume "f b <= c" |
|
985 |
finally (order_less_le_trans) show ?thesis . |
|
986 |
qed |
|
987 |
||
988 |
lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> |
|
989 |
(!!x y. x <= y ==> f x <= f y) ==> a < f c" |
|
990 |
proof - |
|
991 |
assume r: "!!x y. x <= y ==> f x <= f y" |
|
992 |
assume "a < f b" |
|
993 |
also assume "b <= c" hence "f b <= f c" by (rule r) |
|
994 |
finally (order_less_le_trans) show ?thesis . |
|
995 |
qed |
|
996 |
||
997 |
lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> |
|
998 |
(!!x y. x <= y ==> f x <= f y) ==> a <= f c" |
|
999 |
proof - |
|
1000 |
assume r: "!!x y. x <= y ==> f x <= f y" |
|
1001 |
assume "a <= f b" |
|
1002 |
also assume "b <= c" hence "f b <= f c" by (rule r) |
|
1003 |
finally (order_trans) show ?thesis . |
|
1004 |
qed |
|
1005 |
||
1006 |
lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> |
|
1007 |
(!!x y. x <= y ==> f x <= f y) ==> f a <= c" |
|
1008 |
proof - |
|
1009 |
assume r: "!!x y. x <= y ==> f x <= f y" |
|
1010 |
assume "a <= b" hence "f a <= f b" by (rule r) |
|
1011 |
also assume "f b <= c" |
|
1012 |
finally (order_trans) show ?thesis . |
|
1013 |
qed |
|
1014 |
||
1015 |
lemma ord_le_eq_subst: "a <= b ==> f b = c ==> |
|
1016 |
(!!x y. x <= y ==> f x <= f y) ==> f a <= c" |
|
1017 |
proof - |
|
1018 |
assume r: "!!x y. x <= y ==> f x <= f y" |
|
1019 |
assume "a <= b" hence "f a <= f b" by (rule r) |
|
1020 |
also assume "f b = c" |
|
1021 |
finally (ord_le_eq_trans) show ?thesis . |
|
1022 |
qed |
|
1023 |
||
1024 |
lemma ord_eq_le_subst: "a = f b ==> b <= c ==> |
|
1025 |
(!!x y. x <= y ==> f x <= f y) ==> a <= f c" |
|
1026 |
proof - |
|
1027 |
assume r: "!!x y. x <= y ==> f x <= f y" |
|
1028 |
assume "a = f b" |
|
1029 |
also assume "b <= c" hence "f b <= f c" by (rule r) |
|
1030 |
finally (ord_eq_le_trans) show ?thesis . |
|
1031 |
qed |
|
1032 |
||
1033 |
lemma ord_less_eq_subst: "a < b ==> f b = c ==> |
|
1034 |
(!!x y. x < y ==> f x < f y) ==> f a < c" |
|
1035 |
proof - |
|
1036 |
assume r: "!!x y. x < y ==> f x < f y" |
|
1037 |
assume "a < b" hence "f a < f b" by (rule r) |
|
1038 |
also assume "f b = c" |
|
1039 |
finally (ord_less_eq_trans) show ?thesis . |
|
1040 |
qed |
|
1041 |
||
1042 |
lemma ord_eq_less_subst: "a = f b ==> b < c ==> |
|
1043 |
(!!x y. x < y ==> f x < f y) ==> a < f c" |
|
1044 |
proof - |
|
1045 |
assume r: "!!x y. x < y ==> f x < f y" |
|
1046 |
assume "a = f b" |
|
1047 |
also assume "b < c" hence "f b < f c" by (rule r) |
|
1048 |
finally (ord_eq_less_trans) show ?thesis . |
|
1049 |
qed |
|
1050 |
||
1051 |
text {* |
|
1052 |
Note that this list of rules is in reverse order of priorities. |
|
1053 |
*} |
|
1054 |
||
1055 |
lemmas basic_trans_rules [trans] = |
|
1056 |
order_less_subst2 |
|
1057 |
order_less_subst1 |
|
1058 |
order_le_less_subst2 |
|
1059 |
order_le_less_subst1 |
|
1060 |
order_less_le_subst2 |
|
1061 |
order_less_le_subst1 |
|
1062 |
order_subst2 |
|
1063 |
order_subst1 |
|
1064 |
ord_le_eq_subst |
|
1065 |
ord_eq_le_subst |
|
1066 |
ord_less_eq_subst |
|
1067 |
ord_eq_less_subst |
|
1068 |
forw_subst |
|
1069 |
back_subst |
|
1070 |
rev_mp |
|
1071 |
mp |
|
1072 |
set_rev_mp |
|
1073 |
set_mp |
|
1074 |
order_neq_le_trans |
|
1075 |
order_le_neq_trans |
|
1076 |
order_less_trans |
|
1077 |
order_less_asym' |
|
1078 |
order_le_less_trans |
|
1079 |
order_less_le_trans |
|
1080 |
order_trans |
|
1081 |
order_antisym |
|
1082 |
ord_le_eq_trans |
|
1083 |
ord_eq_le_trans |
|
1084 |
ord_less_eq_trans |
|
1085 |
ord_eq_less_trans |
|
1086 |
trans |
|
1087 |
||
11979 | 1088 |
end |