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