src/HOL/Codatatype/BNF_Util.thy
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 49314 f252c7c2ac7b
child 49463 83ac281bcdc2
permissions -rw-r--r--
tuned simpset
     1 (*  Title:      HOL/Codatatype/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 "../Cardinals/Cardinal_Arithmetic"
    13 begin
    14 
    15 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    16 by blast
    17 
    18 lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
    19 by blast
    20 
    21 lemma mem_Collect_eq_split: "{(x, y). (x, y) \<in> X} = X"
    22 by simp
    23 
    24 definition collect where
    25   "collect F x = (\<Union>f \<in> F. f x)"
    26 
    27 (* Weak pullbacks: *)
    28 definition wpull where
    29 "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
    30  (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))"
    31 
    32 (* Weak pseudo-pullbacks *)
    33 definition wppull where
    34 "wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
    35  (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
    36            (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
    37 
    38 lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
    39 by simp
    40 
    41 lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
    42 by simp
    43 
    44 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
    45 by simp
    46 
    47 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
    48 by simp
    49 
    50 lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
    51 unfolding bij_def inj_on_def by auto blast
    52 
    53 (* Operator: *)
    54 definition "Gr A f = {(a, f a) | a. a \<in> A}"
    55 
    56 ML_file "Tools/bnf_util.ML"
    57 ML_file "Tools/bnf_tactics.ML"
    58 
    59 end