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;
blanchet@55059
     1
(*  Title:      HOL/BNF_Util.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@49282
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     4
    Copyright   2012
blanchet@48975
     5
blanchet@48975
     6
Library for bounded natural functors.
blanchet@48975
     7
*)
blanchet@48975
     8
blanchet@48975
     9
header {* Library for Bounded Natural Functors *}
blanchet@48975
    10
blanchet@49282
    11
theory BNF_Util
blanchet@55056
    12
imports BNF_Cardinal_Arithmetic
blanchet@48975
    13
begin
blanchet@48975
    14
blanchet@55084
    15
definition
blanchet@55945
    16
  rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
blanchet@55084
    17
where
blanchet@55945
    18
  "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
blanchet@55084
    19
blanchet@55945
    20
lemma rel_funI [intro]:
blanchet@55084
    21
  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
blanchet@55945
    22
  shows "rel_fun A B f g"
blanchet@55945
    23
  using assms by (simp add: rel_fun_def)
blanchet@55084
    24
blanchet@55945
    25
lemma rel_funD:
blanchet@55945
    26
  assumes "rel_fun A B f g" and "A x y"
blanchet@55084
    27
  shows "B (f x) (g y)"
blanchet@55945
    28
  using assms by (simp add: rel_fun_def)
blanchet@55084
    29
blanchet@48975
    30
definition collect where
blanchet@49463
    31
"collect F x = (\<Union>f \<in> F. f x)"
blanchet@48975
    32
blanchet@48975
    33
lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
blanchet@48975
    34
by simp
blanchet@48975
    35
blanchet@48975
    36
lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
blanchet@48975
    37
by simp
blanchet@48975
    38
blanchet@55066
    39
lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
blanchet@48975
    40
unfolding bij_def inj_on_def by auto blast
blanchet@48975
    41
blanchet@49312
    42
(* Operator: *)
blanchet@49312
    43
definition "Gr A f = {(a, f a) | a. a \<in> A}"
blanchet@48975
    44
traytel@51893
    45
definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
traytel@51893
    46
traytel@55803
    47
definition vimage2p where
traytel@55803
    48
  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
traytel@55803
    49
blanchet@55062
    50
ML_file "Tools/BNF/bnf_util.ML"
blanchet@55062
    51
ML_file "Tools/BNF/bnf_tactics.ML"
blanchet@49283
    52
blanchet@48975
    53
end