|
1 (* Title: HOL/BNF/BNF_Util.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Library for bounded natural functors. |
|
7 *) |
|
8 |
|
9 header {* Library for Bounded Natural Functors *} |
|
10 |
|
11 theory BNF_Util |
|
12 imports "../Cardinals/Cardinal_Arithmetic" |
|
13 begin |
|
14 |
|
15 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" |
|
16 by blast |
|
17 |
|
18 lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})" |
|
19 by blast |
|
20 |
|
21 definition collect where |
|
22 "collect F x = (\<Union>f \<in> F. f x)" |
|
23 |
|
24 (* Weak pullbacks: *) |
|
25 definition wpull where |
|
26 "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> |
|
27 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))" |
|
28 |
|
29 (* Weak pseudo-pullbacks *) |
|
30 definition wppull where |
|
31 "wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow> |
|
32 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> |
|
33 (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))" |
|
34 |
|
35 lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y" |
|
36 by simp |
|
37 |
|
38 lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z" |
|
39 by simp |
|
40 |
|
41 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y" |
|
42 by simp |
|
43 |
|
44 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z" |
|
45 by simp |
|
46 |
|
47 lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f" |
|
48 unfolding bij_def inj_on_def by auto blast |
|
49 |
|
50 lemma pair_mem_Collect_split: |
|
51 "(\<lambda>x y. (x, y) \<in> {(x, y). P x y}) = P" |
|
52 by simp |
|
53 |
|
54 lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R" |
|
55 by simp |
|
56 |
|
57 lemma Collect_fst_snd_mem_eq: "{p. (fst p, snd p) \<in> A} = A" |
|
58 by simp |
|
59 |
|
60 (* Operator: *) |
|
61 definition "Gr A f = {(a, f a) | a. a \<in> A}" |
|
62 |
|
63 ML_file "Tools/bnf_util.ML" |
|
64 ML_file "Tools/bnf_tactics.ML" |
|
65 |
|
66 end |