src/HOL/Codatatype/BNF_Def.thy
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 49325 340844cbf7af
child 49495 675b9df572df
permissions -rw-r--r--
tuned simpset
     1 (*  Title:      HOL/Codatatype/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 csquare where
    29 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
    30 
    31 (* The pullback of sets *)
    32 definition thePull where
    33 "thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
    34 
    35 lemma wpull_thePull:
    36 "wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
    37 unfolding wpull_def thePull_def by auto
    38 
    39 lemma wppull_thePull:
    40 assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
    41 shows
    42 "\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
    43    j a' \<in> A \<and>
    44    e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
    45 (is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
    46 proof(rule bchoice[of ?A' ?phi], default)
    47   fix a' assume a': "a' \<in> ?A'"
    48   hence "fst a' \<in> B1" unfolding thePull_def by auto
    49   moreover
    50   from a' have "snd a' \<in> B2" unfolding thePull_def by auto
    51   moreover have "f1 (fst a') = f2 (snd a')"
    52   using a' unfolding csquare_def thePull_def by auto
    53   ultimately show "\<exists> ja'. ?phi a' ja'"
    54   using assms unfolding wppull_def by blast
    55 qed
    56 
    57 lemma wpull_wppull:
    58 assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
    59 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')"
    60 shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
    61 unfolding wppull_def proof safe
    62   fix b1 b2
    63   assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
    64   then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
    65   using wp unfolding wpull_def by blast
    66   show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
    67   apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
    68 qed
    69 
    70 lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow>
    71    wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2"
    72 by (erule wpull_wppull) auto
    73 
    74 lemma Id_alt: "Id = Gr UNIV id"
    75 unfolding Gr_def by auto
    76 
    77 lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
    78 unfolding Gr_def by auto
    79 
    80 lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
    81 unfolding Gr_def by auto
    82 
    83 lemma wpull_Gr:
    84 "wpull (Gr A f) A (f ` A) f id fst snd"
    85 unfolding wpull_def Gr_def by auto
    86 
    87 definition "pick_middle P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
    88 
    89 lemma pick_middle:
    90 "(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"
    91 unfolding pick_middle_def apply(rule someI_ex)
    92 using assms unfolding relcomp_def by auto
    93 
    94 definition fstO where "fstO P Q ac = (fst ac, pick_middle P Q (fst ac) (snd ac))"
    95 definition sndO where "sndO P Q ac = (pick_middle P Q (fst ac) (snd ac), snd ac)"
    96 
    97 lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
    98 unfolding fstO_def
    99 by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1])
   100 
   101 lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
   102 unfolding comp_def fstO_def by simp
   103 
   104 lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
   105 unfolding comp_def sndO_def by simp
   106 
   107 lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
   108 unfolding sndO_def
   109 by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct2])
   110 
   111 lemma csquare_fstO_sndO:
   112 "csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
   113 unfolding csquare_def fstO_def sndO_def using pick_middle by simp
   114 
   115 lemma wppull_fstO_sndO:
   116 shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
   117 using pick_middle unfolding wppull_def fstO_def sndO_def relcomp_def by auto
   118 
   119 lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
   120 by (simp split: prod.split)
   121 
   122 lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
   123 by (simp split: prod.split)
   124 
   125 lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
   126 by auto
   127 
   128 lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
   129 unfolding o_def fun_eq_iff by simp
   130 
   131 ML_file "Tools/bnf_def_tactics.ML"
   132 ML_file"Tools/bnf_def.ML"
   133 
   134 end