1 (* Title: HOL/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 begin |
|
14 |
|
15 definition |
|
16 rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" |
|
17 where |
|
18 "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))" |
|
19 |
|
20 lemma rel_funI [intro]: |
|
21 assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)" |
|
22 shows "rel_fun A B f g" |
|
23 using assms by (simp add: rel_fun_def) |
|
24 |
|
25 lemma rel_funD: |
|
26 assumes "rel_fun A B f g" and "A x y" |
|
27 shows "B (f x) (g y)" |
|
28 using assms by (simp add: rel_fun_def) |
|
29 |
|
30 definition collect where |
|
31 "collect F x = (\<Union>f \<in> F. f x)" |
|
32 |
|
33 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y" |
|
34 by simp |
|
35 |
|
36 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z" |
|
37 by simp |
|
38 |
|
39 lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f" |
|
40 unfolding bij_def inj_on_def by auto blast |
|
41 |
|
42 (* Operator: *) |
|
43 definition "Gr A f = {(a, f a) | a. a \<in> A}" |
|
44 |
|
45 definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)" |
|
46 |
|
47 definition vimage2p where |
|
48 "vimage2p f g R = (\<lambda>x y. R (f x) (g y))" |
|
49 |
|
50 ML_file "Tools/BNF/bnf_util.ML" |
|
51 ML_file "Tools/BNF/bnf_tactics.ML" |
|
52 |
|
53 end |
|