src/HOL/BNF/BNF_Def.thy
author blanchet
Fri Sep 21 16:45:06 2012 +0200 (2012-09-21)
changeset 49510 ba50d204095e
parent 49509 src/HOL/Codatatype/BNF_Def.thy@163914705f8d
child 49537 fe1deee434b6
permissions -rw-r--r--
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
     1 (*  Title:      HOL/BNF/BNF_Def.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Definition of bounded natural functors.
     6 *)
     7 
     8 header {* Definition of Bounded Natural Functors *}
     9 
    10 theory BNF_Def
    11 imports BNF_Util
    12 keywords
    13   "print_bnfs" :: diag and
    14   "bnf_def" :: thy_goal
    15 begin
    16 
    17 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
    18 by (rule ext) (auto simp only: o_apply collect_def)
    19 
    20 lemma converse_mono:
    21 "R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
    22 unfolding converse_def by auto
    23 
    24 lemma converse_shift:
    25 "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
    26 unfolding converse_def by auto
    27 
    28 definition convol ("<_ , _>") where
    29 "<f , g> \<equiv> %a. (f a, g a)"
    30 
    31 lemma fst_convol:
    32 "fst o <f , g> = f"
    33 apply(rule ext)
    34 unfolding convol_def by simp
    35 
    36 lemma snd_convol:
    37 "snd o <f , g> = g"
    38 apply(rule ext)
    39 unfolding convol_def by simp
    40 
    41 lemma convol_memI:
    42 "\<lbrakk>f x = f' x; g x = g' x; P x\<rbrakk> \<Longrightarrow> <f , g> x \<in> {(f' a, g' a) |a. P a}"
    43 unfolding convol_def by auto
    44 
    45 definition csquare where
    46 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
    47 
    48 (* The pullback of sets *)
    49 definition thePull where
    50 "thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
    51 
    52 lemma wpull_thePull:
    53 "wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
    54 unfolding wpull_def thePull_def by auto
    55 
    56 lemma wppull_thePull:
    57 assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
    58 shows
    59 "\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
    60    j a' \<in> A \<and>
    61    e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
    62 (is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
    63 proof(rule bchoice[of ?A' ?phi], default)
    64   fix a' assume a': "a' \<in> ?A'"
    65   hence "fst a' \<in> B1" unfolding thePull_def by auto
    66   moreover
    67   from a' have "snd a' \<in> B2" unfolding thePull_def by auto
    68   moreover have "f1 (fst a') = f2 (snd a')"
    69   using a' unfolding csquare_def thePull_def by auto
    70   ultimately show "\<exists> ja'. ?phi a' ja'"
    71   using assms unfolding wppull_def by blast
    72 qed
    73 
    74 lemma wpull_wppull:
    75 assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
    76 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')"
    77 shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
    78 unfolding wppull_def proof safe
    79   fix b1 b2
    80   assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
    81   then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
    82   using wp unfolding wpull_def by blast
    83   show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
    84   apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
    85 qed
    86 
    87 lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow>
    88    wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2"
    89 by (erule wpull_wppull) auto
    90 
    91 lemma Id_alt: "Id = Gr UNIV id"
    92 unfolding Gr_def by auto
    93 
    94 lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
    95 unfolding Gr_def by auto
    96 
    97 lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
    98 unfolding Gr_def by auto
    99 
   100 lemma wpull_Gr:
   101 "wpull (Gr A f) A (f ` A) f id fst snd"
   102 unfolding wpull_def Gr_def by auto
   103 
   104 definition "pick_middle P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
   105 
   106 lemma pick_middle:
   107 "(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"
   108 unfolding pick_middle_def apply(rule someI_ex)
   109 using assms unfolding relcomp_def by auto
   110 
   111 definition fstO where "fstO P Q ac = (fst ac, pick_middle P Q (fst ac) (snd ac))"
   112 definition sndO where "sndO P Q ac = (pick_middle P Q (fst ac) (snd ac), snd ac)"
   113 
   114 lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
   115 unfolding fstO_def
   116 by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1])
   117 
   118 lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
   119 unfolding comp_def fstO_def by simp
   120 
   121 lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
   122 unfolding comp_def sndO_def by simp
   123 
   124 lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
   125 unfolding sndO_def
   126 by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct2])
   127 
   128 lemma csquare_fstO_sndO:
   129 "csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
   130 unfolding csquare_def fstO_def sndO_def using pick_middle by simp
   131 
   132 lemma wppull_fstO_sndO:
   133 shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
   134 using pick_middle unfolding wppull_def fstO_def sndO_def relcomp_def by auto
   135 
   136 lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
   137 by (simp split: prod.split)
   138 
   139 lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
   140 by (simp split: prod.split)
   141 
   142 lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
   143 by auto
   144 
   145 lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
   146 unfolding o_def fun_eq_iff by simp
   147 
   148 ML_file "Tools/bnf_def_tactics.ML"
   149 ML_file"Tools/bnf_def.ML"
   150 
   151 end