src/HOL/BNF_Def.thy
changeset 55058 4e700eb471d4
parent 54961 e60428f432bc
child 55059 ef2e0fb783c6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -0,0 +1,163 @@
     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 +   (*FIXME: register fundef_cong attribute in an interpretation to remove this dependency*)
    1.16 +  FunDef
    1.17 +keywords
    1.18 +  "print_bnfs" :: diag and
    1.19 +  "bnf" :: thy_goal
    1.20 +begin
    1.21 +
    1.22 +lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
    1.23 +  by (rule ext) (auto simp only: o_apply collect_def)
    1.24 +
    1.25 +definition convol ("<_ , _>") where
    1.26 +"<f , g> \<equiv> %a. (f a, g a)"
    1.27 +
    1.28 +lemma fst_convol:
    1.29 +"fst o <f , g> = f"
    1.30 +apply(rule ext)
    1.31 +unfolding convol_def by simp
    1.32 +
    1.33 +lemma snd_convol:
    1.34 +"snd o <f , g> = g"
    1.35 +apply(rule ext)
    1.36 +unfolding convol_def by simp
    1.37 +
    1.38 +lemma convol_mem_GrpI:
    1.39 +"x \<in> A \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))"
    1.40 +unfolding convol_def Grp_def by auto
    1.41 +
    1.42 +definition csquare where
    1.43 +"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
    1.44 +
    1.45 +lemma eq_alt: "op = = Grp UNIV id"
    1.46 +unfolding Grp_def by auto
    1.47 +
    1.48 +lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1"
    1.49 +  by auto
    1.50 +
    1.51 +lemma leq_OOI: "R = op = \<Longrightarrow> R \<le> R OO R"
    1.52 +  by auto
    1.53 +
    1.54 +lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\<lambda>x y. \<exists>z. z \<in> A \<and> f z = x \<and> g z = y)"
    1.55 +  unfolding Grp_def by auto
    1.56 +
    1.57 +lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
    1.58 +unfolding Grp_def by auto
    1.59 +
    1.60 +lemma Grp_UNIV_idI: "x = y \<Longrightarrow> Grp UNIV id x y"
    1.61 +unfolding Grp_def by auto
    1.62 +
    1.63 +lemma Grp_mono: "A \<le> B \<Longrightarrow> Grp A f \<le> Grp B f"
    1.64 +unfolding Grp_def by auto
    1.65 +
    1.66 +lemma GrpI: "\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> Grp A f x y"
    1.67 +unfolding Grp_def by auto
    1.68 +
    1.69 +lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
    1.70 +unfolding Grp_def by auto
    1.71 +
    1.72 +lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
    1.73 +unfolding Grp_def o_def by auto
    1.74 +
    1.75 +lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
    1.76 +unfolding Grp_def o_def by auto
    1.77 +
    1.78 +definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
    1.79 +
    1.80 +lemma pick_middlep:
    1.81 +"(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
    1.82 +unfolding pick_middlep_def apply(rule someI_ex) by auto
    1.83 +
    1.84 +definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"
    1.85 +definition sndOp where "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
    1.86 +
    1.87 +lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
    1.88 +unfolding fstOp_def mem_Collect_eq
    1.89 +by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct1])
    1.90 +
    1.91 +lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc"
    1.92 +unfolding comp_def fstOp_def by simp
    1.93 +
    1.94 +lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
    1.95 +unfolding comp_def sndOp_def by simp
    1.96 +
    1.97 +lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
    1.98 +unfolding sndOp_def mem_Collect_eq
    1.99 +by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2])
   1.100 +
   1.101 +lemma csquare_fstOp_sndOp:
   1.102 +"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
   1.103 +unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
   1.104 +
   1.105 +lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
   1.106 +by (simp split: prod.split)
   1.107 +
   1.108 +lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
   1.109 +by (simp split: prod.split)
   1.110 +
   1.111 +lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
   1.112 +by auto
   1.113 +
   1.114 +lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
   1.115 +  by auto
   1.116 +
   1.117 +lemma Collect_split_mono_strong: 
   1.118 +  "\<lbrakk>\<forall>a\<in>fst ` A. \<forall>b \<in> snd ` A. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
   1.119 +  A \<subseteq> Collect (split Q)"
   1.120 +  by fastforce
   1.121 +
   1.122 +lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
   1.123 +by metis
   1.124 +
   1.125 +lemma sum_case_o_inj:
   1.126 +"sum_case f g \<circ> Inl = f"
   1.127 +"sum_case f g \<circ> Inr = g"
   1.128 +by auto
   1.129 +
   1.130 +lemma card_order_csum_cone_cexp_def:
   1.131 +  "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
   1.132 +  unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order)
   1.133 +
   1.134 +lemma If_the_inv_into_in_Func:
   1.135 +  "\<lbrakk>inj_on g C; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow>
   1.136 +  (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})"
   1.137 +unfolding Func_def by (auto dest: the_inv_into_into)
   1.138 +
   1.139 +lemma If_the_inv_into_f_f:
   1.140 +  "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow>
   1.141 +  ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
   1.142 +unfolding Func_def by (auto elim: the_inv_into_f_f)
   1.143 +
   1.144 +definition vimage2p where
   1.145 +  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
   1.146 +
   1.147 +lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
   1.148 +  unfolding vimage2p_def by -
   1.149 +
   1.150 +lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
   1.151 +  unfolding fun_rel_def vimage2p_def by auto
   1.152 +
   1.153 +lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
   1.154 +  unfolding vimage2p_def convol_def by auto
   1.155 +
   1.156 +lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
   1.157 +  unfolding vimage2p_def Grp_def by auto
   1.158 +
   1.159 +(*FIXME: duplicates lemma from Record.thy*)
   1.160 +lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
   1.161 +  by clarsimp
   1.162 +
   1.163 +ML_file "Tools/bnf_def_tactics.ML"
   1.164 +ML_file "Tools/bnf_def.ML"
   1.165 +
   1.166 +end