src/HOL/BNF_GFP.thy
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55414 eab03e9cee8a
parent 55413 a8e96847523c
child 55415 05f5fdb8d093
permissions -rw-r--r--
renamed '{prod,sum,bool,unit}_case' to 'case_...'
     1 (*  Title:      HOL/BNF_GFP.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Lorenz Panny, TU Muenchen
     4     Author:     Jasmin Blanchette, TU Muenchen
     5     Copyright   2012, 2013
     6 
     7 Greatest fixed point operation on bounded natural functors.
     8 *)
     9 
    10 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
    11 
    12 theory BNF_GFP
    13 imports BNF_FP_Base List_Prefix String
    14 keywords
    15   "codatatype" :: thy_decl and
    16   "primcorecursive" :: thy_goal and
    17   "primcorec" :: thy_decl
    18 begin
    19 
    20 setup {*
    21 Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
    22 *}
    23 
    24 lemma not_TrueE: "\<not> True \<Longrightarrow> P"
    25 by (erule notE, rule TrueI)
    26 
    27 lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
    28 by fast
    29 
    30 lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
    31 by (auto split: sum.splits)
    32 
    33 lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    34 apply rule
    35  apply (rule ext, force split: sum.split)
    36 by (rule ext, metis case_sum_o_inj(2))
    37 
    38 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    39 by fast
    40 
    41 lemma equiv_proj:
    42   assumes e: "equiv A R" and "z \<in> R"
    43   shows "(proj R o fst) z = (proj R o snd) z"
    44 proof -
    45   from assms(2) have z: "(fst z, snd z) \<in> R" by auto
    46   with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
    47     unfolding equiv_def sym_def trans_def by blast+
    48   then show ?thesis unfolding proj_def[abs_def] by auto
    49 qed
    50 
    51 (* Operators: *)
    52 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
    53 
    54 lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
    55 unfolding Id_on_def by simp
    56 
    57 lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
    58 unfolding Id_on_def by auto
    59 
    60 lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
    61 unfolding Id_on_def by auto
    62 
    63 lemma Id_on_UNIV: "Id_on UNIV = Id"
    64 unfolding Id_on_def by auto
    65 
    66 lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
    67 unfolding Id_on_def by auto
    68 
    69 lemma Id_on_Gr: "Id_on A = Gr A id"
    70 unfolding Id_on_def Gr_def by auto
    71 
    72 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
    73 unfolding image2_def by auto
    74 
    75 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
    76 by auto
    77 
    78 lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
    79 unfolding image2_def Gr_def by auto
    80 
    81 lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
    82 unfolding Gr_def by simp
    83 
    84 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
    85 unfolding Gr_def by simp
    86 
    87 lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
    88 unfolding Gr_def by auto
    89 
    90 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    91 by blast
    92 
    93 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})"
    94 by blast
    95 
    96 lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
    97 unfolding fun_eq_iff by auto
    98 
    99 lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
   100 by auto
   101 
   102 lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
   103 by force
   104 
   105 lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
   106 by auto
   107 
   108 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
   109 unfolding fun_eq_iff by auto
   110 
   111 lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
   112 unfolding fun_eq_iff by auto
   113 
   114 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
   115 unfolding Gr_def Grp_def fun_eq_iff by auto
   116 
   117 lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
   118 unfolding fun_eq_iff by auto
   119 
   120 definition relImage where
   121 "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
   122 
   123 definition relInvImage where
   124 "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
   125 
   126 lemma relImage_Gr:
   127 "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
   128 unfolding relImage_def Gr_def relcomp_def by auto
   129 
   130 lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
   131 unfolding Gr_def relcomp_def image_def relInvImage_def by auto
   132 
   133 lemma relImage_mono:
   134 "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
   135 unfolding relImage_def by auto
   136 
   137 lemma relInvImage_mono:
   138 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
   139 unfolding relInvImage_def by auto
   140 
   141 lemma relInvImage_Id_on:
   142 "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
   143 unfolding relInvImage_def Id_on_def by auto
   144 
   145 lemma relInvImage_UNIV_relImage:
   146 "R \<subseteq> relInvImage UNIV (relImage R f) f"
   147 unfolding relInvImage_def relImage_def by auto
   148 
   149 lemma relImage_proj:
   150 assumes "equiv A R"
   151 shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
   152 unfolding relImage_def Id_on_def
   153 using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
   154 by (auto simp: proj_preserves)
   155 
   156 lemma relImage_relInvImage:
   157 assumes "R \<subseteq> f ` A <*> f ` A"
   158 shows "relImage (relInvImage A R f) f = R"
   159 using assms unfolding relImage_def relInvImage_def by fast
   160 
   161 lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
   162 by simp
   163 
   164 lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
   165 by simp
   166 
   167 lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
   168 by simp
   169 
   170 lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x"
   171 unfolding convol_def by auto
   172 
   173 (*Extended Sublist*)
   174 
   175 definition clists where "clists r = |lists (Field r)|"
   176 
   177 definition prefCl where
   178   "prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
   179 definition PrefCl where
   180   "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> prefixeq kl' kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
   181 
   182 lemma prefCl_UN:
   183   "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
   184 unfolding prefCl_def PrefCl_def by fastforce
   185 
   186 definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
   187 definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
   188 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
   189 
   190 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
   191 unfolding Shift_def Succ_def by simp
   192 
   193 lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
   194 unfolding Shift_def clists_def Field_card_of by auto
   195 
   196 lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
   197 unfolding prefCl_def Shift_def
   198 proof safe
   199   fix kl1 kl2
   200   assume "\<forall>kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
   201     "prefixeq kl1 kl2" "k # kl2 \<in> Kl"
   202   thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2] by blast
   203 qed
   204 
   205 lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
   206 unfolding Shift_def by simp
   207 
   208 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
   209 unfolding Succ_def by simp
   210 
   211 lemmas SuccE = SuccD[elim_format]
   212 
   213 lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
   214 unfolding Succ_def by simp
   215 
   216 lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
   217 unfolding Shift_def by simp
   218 
   219 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
   220 unfolding Succ_def Shift_def by auto
   221 
   222 lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
   223 unfolding clists_def Field_card_of by auto
   224 
   225 lemma Cons_clists:
   226   "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
   227 unfolding clists_def Field_card_of by auto
   228 
   229 lemma length_Cons: "length (x # xs) = Suc (length xs)"
   230 by simp
   231 
   232 lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
   233 by simp
   234 
   235 (*injection into the field of a cardinal*)
   236 definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
   237 definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
   238 
   239 lemma ex_toCard_pred:
   240 "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
   241 unfolding toCard_pred_def
   242 using card_of_ordLeq[of A "Field r"]
   243       ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
   244 by blast
   245 
   246 lemma toCard_pred_toCard:
   247   "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
   248 unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
   249 
   250 lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
   251   toCard A r x = toCard A r y \<longleftrightarrow> x = y"
   252 using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
   253 
   254 lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
   255 using toCard_pred_toCard unfolding toCard_pred_def by blast
   256 
   257 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
   258 
   259 lemma fromCard_toCard:
   260 "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
   261 unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
   262 
   263 lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
   264 unfolding Field_card_of csum_def by auto
   265 
   266 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
   267 unfolding Field_card_of csum_def by auto
   268 
   269 lemma nat_rec_0_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
   270 by auto
   271 
   272 lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
   273 by auto
   274 
   275 lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
   276 by auto
   277 
   278 lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
   279 by auto
   280 
   281 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
   282 by simp
   283 
   284 lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
   285 by auto
   286 
   287 definition image2p where
   288   "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
   289 
   290 lemma image2pI: "R x y \<Longrightarrow> (image2p f g R) (f x) (g y)"
   291   unfolding image2p_def by blast
   292 
   293 lemma image2pE: "\<lbrakk>(image2p f g R) fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
   294   unfolding image2p_def by blast
   295 
   296 lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \<le> S)"
   297   unfolding fun_rel_def image2p_def by auto
   298 
   299 lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
   300   unfolding fun_rel_def image2p_def by auto
   301 
   302 
   303 subsection {* Equivalence relations, quotients, and Hilbert's choice *}
   304 
   305 lemma equiv_Eps_in:
   306 "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
   307 apply (rule someI2_ex)
   308 using in_quotient_imp_non_empty by blast
   309 
   310 lemma equiv_Eps_preserves:
   311 assumes ECH: "equiv A r" and X: "X \<in> A//r"
   312 shows "Eps (%x. x \<in> X) \<in> A"
   313 apply (rule in_mono[rule_format])
   314  using assms apply (rule in_quotient_imp_subset)
   315 by (rule equiv_Eps_in) (rule assms)+
   316 
   317 lemma proj_Eps:
   318 assumes "equiv A r" and "X \<in> A//r"
   319 shows "proj r (Eps (%x. x \<in> X)) = X"
   320 unfolding proj_def proof auto
   321   fix x assume x: "x \<in> X"
   322   thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
   323 next
   324   fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
   325   thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
   326 qed
   327 
   328 definition univ where "univ f X == f (Eps (%x. x \<in> X))"
   329 
   330 lemma univ_commute:
   331 assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
   332 shows "(univ f) (proj r x) = f x"
   333 unfolding univ_def proof -
   334   have prj: "proj r x \<in> A//r" using x proj_preserves by fast
   335   hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
   336   moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
   337   ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
   338   thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
   339 qed
   340 
   341 lemma univ_preserves:
   342 assumes ECH: "equiv A r" and RES: "f respects r" and
   343         PRES: "\<forall> x \<in> A. f x \<in> B"
   344 shows "\<forall> X \<in> A//r. univ f X \<in> B"
   345 proof
   346   fix X assume "X \<in> A//r"
   347   then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
   348   hence "univ f X = f x" using assms univ_commute by fastforce
   349   thus "univ f X \<in> B" using x PRES by simp
   350 qed
   351 
   352 ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
   353 ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
   354 ML_file "Tools/BNF/bnf_gfp_util.ML"
   355 ML_file "Tools/BNF/bnf_gfp_tactics.ML"
   356 ML_file "Tools/BNF/bnf_gfp.ML"
   357 
   358 end