src/HOL/BNF/BNF_Util.thy
changeset 49510 ba50d204095e
parent 49509 163914705f8d
child 51893 596baae88a88
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF/BNF_Util.thy	Fri Sep 21 16:45:06 2012 +0200
     1.3 @@ -0,0 +1,66 @@
     1.4 +(*  Title:      HOL/BNF/BNF_Util.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Jasmin Blanchette, TU Muenchen
     1.7 +    Copyright   2012
     1.8 +
     1.9 +Library for bounded natural functors.
    1.10 +*)
    1.11 +
    1.12 +header {* Library for Bounded Natural Functors *}
    1.13 +
    1.14 +theory BNF_Util
    1.15 +imports "../Cardinals/Cardinal_Arithmetic"
    1.16 +begin
    1.17 +
    1.18 +lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    1.19 +by blast
    1.20 +
    1.21 +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})"
    1.22 +by blast
    1.23 +
    1.24 +definition collect where
    1.25 +"collect F x = (\<Union>f \<in> F. f x)"
    1.26 +
    1.27 +(* Weak pullbacks: *)
    1.28 +definition wpull where
    1.29 +"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
    1.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))"
    1.31 +
    1.32 +(* Weak pseudo-pullbacks *)
    1.33 +definition wppull where
    1.34 +"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
    1.35 + (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
    1.36 +           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
    1.37 +
    1.38 +lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
    1.39 +by simp
    1.40 +
    1.41 +lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
    1.42 +by simp
    1.43 +
    1.44 +lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
    1.45 +by simp
    1.46 +
    1.47 +lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
    1.48 +by simp
    1.49 +
    1.50 +lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
    1.51 +unfolding bij_def inj_on_def by auto blast
    1.52 +
    1.53 +lemma pair_mem_Collect_split:
    1.54 +"(\<lambda>x y. (x, y) \<in> {(x, y). P x y}) = P"
    1.55 +by simp
    1.56 +
    1.57 +lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R"
    1.58 +by simp
    1.59 +
    1.60 +lemma Collect_fst_snd_mem_eq: "{p. (fst p, snd p) \<in> A} = A"
    1.61 +by simp
    1.62 +
    1.63 +(* Operator: *)
    1.64 +definition "Gr A f = {(a, f a) | a. a \<in> A}"
    1.65 +
    1.66 +ML_file "Tools/bnf_util.ML"
    1.67 +ML_file "Tools/bnf_tactics.ML"
    1.68 +
    1.69 +end