src/HOL/BNF/BNF_Util.thy
 author traytel Tue May 07 14:22:54 2013 +0200 (2013-05-07) changeset 51893 596baae88a88 parent 49510 ba50d204095e child 53560 4b5f42cfa244 permissions -rw-r--r--
got rid of the set based relator---use (binary) predicate based relator instead
```     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 definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
```
```    64
```
```    65 ML_file "Tools/bnf_util.ML"
```
```    66 ML_file "Tools/bnf_tactics.ML"
```
```    67
```
```    68 end
```