src/HOL/BNF/BNF_Def.thy
changeset 49510 ba50d204095e
parent 49509 163914705f8d
child 49537 fe1deee434b6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Fri Sep 21 16:45:06 2012 +0200
     1.3 @@ -0,0 +1,151 @@
     1.4 +(*  Title:      HOL/BNF/BNF_Def.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Copyright   2012
     1.7 +
     1.8 +Definition of bounded natural functors.
     1.9 +*)
    1.10 +
    1.11 +header {* Definition of Bounded Natural Functors *}
    1.12 +
    1.13 +theory BNF_Def
    1.14 +imports BNF_Util
    1.15 +keywords
    1.16 +  "print_bnfs" :: diag and
    1.17 +  "bnf_def" :: thy_goal
    1.18 +begin
    1.19 +
    1.20 +lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
    1.21 +by (rule ext) (auto simp only: o_apply collect_def)
    1.22 +
    1.23 +lemma converse_mono:
    1.24 +"R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
    1.25 +unfolding converse_def by auto
    1.26 +
    1.27 +lemma converse_shift:
    1.28 +"R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
    1.29 +unfolding converse_def by auto
    1.30 +
    1.31 +definition convol ("<_ , _>") where
    1.32 +"<f , g> \<equiv> %a. (f a, g a)"
    1.33 +
    1.34 +lemma fst_convol:
    1.35 +"fst o <f , g> = f"
    1.36 +apply(rule ext)
    1.37 +unfolding convol_def by simp
    1.38 +
    1.39 +lemma snd_convol:
    1.40 +"snd o <f , g> = g"
    1.41 +apply(rule ext)
    1.42 +unfolding convol_def by simp
    1.43 +
    1.44 +lemma convol_memI:
    1.45 +"\<lbrakk>f x = f' x; g x = g' x; P x\<rbrakk> \<Longrightarrow> <f , g> x \<in> {(f' a, g' a) |a. P a}"
    1.46 +unfolding convol_def by auto
    1.47 +
    1.48 +definition csquare where
    1.49 +"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
    1.50 +
    1.51 +(* The pullback of sets *)
    1.52 +definition thePull where
    1.53 +"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
    1.54 +
    1.55 +lemma wpull_thePull:
    1.56 +"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
    1.57 +unfolding wpull_def thePull_def by auto
    1.58 +
    1.59 +lemma wppull_thePull:
    1.60 +assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
    1.61 +shows
    1.62 +"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
    1.63 +   j a' \<in> A \<and>
    1.64 +   e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
    1.65 +(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
    1.66 +proof(rule bchoice[of ?A' ?phi], default)
    1.67 +  fix a' assume a': "a' \<in> ?A'"
    1.68 +  hence "fst a' \<in> B1" unfolding thePull_def by auto
    1.69 +  moreover
    1.70 +  from a' have "snd a' \<in> B2" unfolding thePull_def by auto
    1.71 +  moreover have "f1 (fst a') = f2 (snd a')"
    1.72 +  using a' unfolding csquare_def thePull_def by auto
    1.73 +  ultimately show "\<exists> ja'. ?phi a' ja'"
    1.74 +  using assms unfolding wppull_def by blast
    1.75 +qed
    1.76 +
    1.77 +lemma wpull_wppull:
    1.78 +assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
    1.79 +1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')"
    1.80 +shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
    1.81 +unfolding wppull_def proof safe
    1.82 +  fix b1 b2
    1.83 +  assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
    1.84 +  then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
    1.85 +  using wp unfolding wpull_def by blast
    1.86 +  show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
    1.87 +  apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
    1.88 +qed
    1.89 +
    1.90 +lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow>
    1.91 +   wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2"
    1.92 +by (erule wpull_wppull) auto
    1.93 +
    1.94 +lemma Id_alt: "Id = Gr UNIV id"
    1.95 +unfolding Gr_def by auto
    1.96 +
    1.97 +lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
    1.98 +unfolding Gr_def by auto
    1.99 +
   1.100 +lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
   1.101 +unfolding Gr_def by auto
   1.102 +
   1.103 +lemma wpull_Gr:
   1.104 +"wpull (Gr A f) A (f ` A) f id fst snd"
   1.105 +unfolding wpull_def Gr_def by auto
   1.106 +
   1.107 +definition "pick_middle P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
   1.108 +
   1.109 +lemma pick_middle:
   1.110 +"(a,c) \<in> P O Q \<Longrightarrow> (a, pick_middle P Q a c) \<in> P \<and> (pick_middle P Q a c, c) \<in> Q"
   1.111 +unfolding pick_middle_def apply(rule someI_ex)
   1.112 +using assms unfolding relcomp_def by auto
   1.113 +
   1.114 +definition fstO where "fstO P Q ac = (fst ac, pick_middle P Q (fst ac) (snd ac))"
   1.115 +definition sndO where "sndO P Q ac = (pick_middle P Q (fst ac) (snd ac), snd ac)"
   1.116 +
   1.117 +lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
   1.118 +unfolding fstO_def
   1.119 +by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1])
   1.120 +
   1.121 +lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
   1.122 +unfolding comp_def fstO_def by simp
   1.123 +
   1.124 +lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
   1.125 +unfolding comp_def sndO_def by simp
   1.126 +
   1.127 +lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
   1.128 +unfolding sndO_def
   1.129 +by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct2])
   1.130 +
   1.131 +lemma csquare_fstO_sndO:
   1.132 +"csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
   1.133 +unfolding csquare_def fstO_def sndO_def using pick_middle by simp
   1.134 +
   1.135 +lemma wppull_fstO_sndO:
   1.136 +shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
   1.137 +using pick_middle unfolding wppull_def fstO_def sndO_def relcomp_def by auto
   1.138 +
   1.139 +lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
   1.140 +by (simp split: prod.split)
   1.141 +
   1.142 +lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
   1.143 +by (simp split: prod.split)
   1.144 +
   1.145 +lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
   1.146 +by auto
   1.147 +
   1.148 +lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
   1.149 +unfolding o_def fun_eq_iff by simp
   1.150 +
   1.151 +ML_file "Tools/bnf_def_tactics.ML"
   1.152 +ML_file"Tools/bnf_def.ML"
   1.153 +
   1.154 +end