src/HOL/BNF_Util.thy
 author wenzelm Fri Mar 07 22:30:58 2014 +0100 (2014-03-07) changeset 55990 41c6b99c5fb7 parent 55945 e96383acecf9 permissions -rw-r--r--
more antiquotations;
```     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
```