equal
deleted
inserted
replaced
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 BNF_Cardinal_Arithmetic |
|
13 Transfer (*FIXME: define fun_rel here, reuse in Transfer once this theory is in HOL*) |
|
14 begin |
|
15 |
|
16 definition collect where |
|
17 "collect F x = (\<Union>f \<in> F. f x)" |
|
18 |
|
19 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y" |
|
20 by simp |
|
21 |
|
22 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z" |
|
23 by simp |
|
24 |
|
25 lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f" |
|
26 unfolding bij_def inj_on_def by auto blast |
|
27 |
|
28 (* Operator: *) |
|
29 definition "Gr A f = {(a, f a) | a. a \<in> A}" |
|
30 |
|
31 definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)" |
|
32 |
|
33 ML_file "Tools/bnf_util.ML" |
|
34 ML_file "Tools/bnf_tactics.ML" |
|
35 |
|
36 end |
|