src/HOL/BNF/BNF_GFP.thy
author traytel
Mon Jul 15 15:50:39 2013 +0200 (2013-07-15)
changeset 52660 7f7311d04727
parent 52659 58b87aa4dc3b
child 52731 dacd47a0633f
permissions -rw-r--r--
killed unused theorems
     1 (*  Title:      HOL/BNF/BNF_GFP.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Greatest fixed point operation on bounded natural functors.
     6 *)
     7 
     8 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
     9 
    10 theory BNF_GFP
    11 imports BNF_FP_Basic Equiv_Relations_More "~~/src/HOL/Library/Sublist"
    12 keywords
    13   "codatatype" :: thy_decl
    14 begin
    15 
    16 lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
    17 unfolding o_def by (auto split: sum.splits)
    18 
    19 lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
    20 by (auto split: sum.splits)
    21 
    22 lemma sum_case_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> sum_case g h = f"
    23 by (metis sum_case_o_inj(1,2) surjective_sum)
    24 
    25 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    26 by auto
    27 
    28 lemma equiv_triv1:
    29 assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R"
    30 shows "(b, c) \<in> R"
    31 using assms unfolding equiv_def sym_def trans_def by blast
    32 
    33 lemma equiv_triv2:
    34 assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R"
    35 shows "(a, c) \<in> R"
    36 using assms unfolding equiv_def trans_def by blast
    37 
    38 lemma equiv_proj:
    39   assumes e: "equiv A R" and "z \<in> R"
    40   shows "(proj R o fst) z = (proj R o snd) z"
    41 proof -
    42   from assms(2) have z: "(fst z, snd z) \<in> R" by auto
    43   have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z])
    44   have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z])
    45   with P show ?thesis unfolding proj_def[abs_def] by auto
    46 qed
    47 
    48 (* Operators: *)
    49 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
    50 
    51 
    52 lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
    53 unfolding Id_on_def by simp
    54 
    55 lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
    56 unfolding Id_on_def by auto
    57 
    58 lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
    59 unfolding Id_on_def by auto
    60 
    61 lemma Id_on_UNIV: "Id_on UNIV = Id"
    62 unfolding Id_on_def by auto
    63 
    64 lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
    65 unfolding Id_on_def by auto
    66 
    67 lemma Id_on_Gr: "Id_on A = Gr A id"
    68 unfolding Id_on_def Gr_def by auto
    69 
    70 lemma Id_on_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> Id_on UNIV"
    71 unfolding Id_on_def by auto
    72 
    73 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
    74 unfolding image2_def by auto
    75 
    76 lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
    77 by auto
    78 
    79 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
    80 by auto
    81 
    82 lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
    83 unfolding image2_def Gr_def by auto
    84 
    85 lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
    86 unfolding Gr_def by simp
    87 
    88 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
    89 unfolding Gr_def by simp
    90 
    91 lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
    92 unfolding Gr_def by auto
    93 
    94 lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
    95 unfolding fun_eq_iff by auto
    96 
    97 lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
    98 by auto
    99 
   100 lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
   101 by force
   102 
   103 lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
   104 by auto
   105 
   106 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
   107 unfolding fun_eq_iff by auto
   108 
   109 lemmas conversep_in_rel_Id_on =
   110   trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]
   111 
   112 lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
   113 unfolding fun_eq_iff by auto
   114 
   115 lemmas relcompp_in_rel_Id_on =
   116   trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]
   117 
   118 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
   119 unfolding Gr_def Grp_def fun_eq_iff by auto
   120 
   121 lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
   122 unfolding fun_eq_iff by auto
   123 
   124 definition relImage where
   125 "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
   126 
   127 definition relInvImage where
   128 "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
   129 
   130 lemma relImage_Gr:
   131 "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
   132 unfolding relImage_def Gr_def relcomp_def by auto
   133 
   134 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"
   135 unfolding Gr_def relcomp_def image_def relInvImage_def by auto
   136 
   137 lemma relImage_mono:
   138 "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
   139 unfolding relImage_def by auto
   140 
   141 lemma relInvImage_mono:
   142 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
   143 unfolding relInvImage_def by auto
   144 
   145 lemma relInvImage_Id_on:
   146 "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
   147 unfolding relInvImage_def Id_on_def by auto
   148 
   149 lemma relInvImage_UNIV_relImage:
   150 "R \<subseteq> relInvImage UNIV (relImage R f) f"
   151 unfolding relInvImage_def relImage_def by auto
   152 
   153 lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})"
   154 unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD)
   155 
   156 lemma relImage_proj:
   157 assumes "equiv A R"
   158 shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
   159 unfolding relImage_def Id_on_def
   160 using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
   161 by (auto simp: proj_preserves)
   162 
   163 lemma relImage_relInvImage:
   164 assumes "R \<subseteq> f ` A <*> f ` A"
   165 shows "relImage (relInvImage A R f) f = R"
   166 using assms unfolding relImage_def relInvImage_def by fastforce
   167 
   168 lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
   169 by simp
   170 
   171 lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
   172 by simp
   173 
   174 lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
   175 by simp
   176 
   177 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"
   178 unfolding convol_def by auto
   179 
   180 (*Extended Sublist*)
   181 
   182 definition prefCl where
   183   "prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
   184 definition PrefCl where
   185   "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> prefixeq kl' kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
   186 
   187 lemma prefCl_UN:
   188   "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
   189 unfolding prefCl_def PrefCl_def by fastforce
   190 
   191 definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
   192 definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
   193 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
   194 
   195 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
   196 unfolding Shift_def Succ_def by simp
   197 
   198 lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
   199 unfolding Shift_def clists_def Field_card_of by auto
   200 
   201 lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
   202 unfolding prefCl_def Shift_def
   203 proof safe
   204   fix kl1 kl2
   205   assume "\<forall>kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
   206     "prefixeq kl1 kl2" "k # kl2 \<in> Kl"
   207   thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2] by blast
   208 qed
   209 
   210 lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
   211 unfolding Shift_def by simp
   212 
   213 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
   214 unfolding Succ_def by simp
   215 
   216 lemmas SuccE = SuccD[elim_format]
   217 
   218 lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
   219 unfolding Succ_def by simp
   220 
   221 lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
   222 unfolding Shift_def by simp
   223 
   224 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
   225 unfolding Succ_def Shift_def by auto
   226 
   227 lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
   228 unfolding clists_def Field_card_of by auto
   229 
   230 lemma Cons_clists:
   231   "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
   232 unfolding clists_def Field_card_of by auto
   233 
   234 lemma length_Cons: "length (x # xs) = Suc (length xs)"
   235 by simp
   236 
   237 lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
   238 by simp
   239 
   240 (*injection into the field of a cardinal*)
   241 definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
   242 definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
   243 
   244 lemma ex_toCard_pred:
   245 "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
   246 unfolding toCard_pred_def
   247 using card_of_ordLeq[of A "Field r"]
   248       ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
   249 by blast
   250 
   251 lemma toCard_pred_toCard:
   252   "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
   253 unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
   254 
   255 lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
   256   toCard A r x = toCard A r y \<longleftrightarrow> x = y"
   257 using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
   258 
   259 lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
   260 using toCard_pred_toCard unfolding toCard_pred_def by blast
   261 
   262 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
   263 
   264 lemma fromCard_toCard:
   265 "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
   266 unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
   267 
   268 (* pick according to the weak pullback *)
   269 definition pickWP where
   270 "pickWP A p1 p2 b1 b2 \<equiv> SOME a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
   271 
   272 lemma pickWP_pred:
   273 assumes "wpull A B1 B2 f1 f2 p1 p2" and
   274 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
   275 shows "\<exists> a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
   276 using assms unfolding wpull_def by blast
   277 
   278 lemma pickWP:
   279 assumes "wpull A B1 B2 f1 f2 p1 p2" and
   280 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
   281 shows "pickWP A p1 p2 b1 b2 \<in> A"
   282       "p1 (pickWP A p1 p2 b1 b2) = b1"
   283       "p2 (pickWP A p1 p2 b1 b2) = b2"
   284 unfolding pickWP_def using assms someI_ex[OF pickWP_pred] by fastforce+
   285 
   286 lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
   287 unfolding Field_card_of csum_def by auto
   288 
   289 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
   290 unfolding Field_card_of csum_def by auto
   291 
   292 lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
   293 by auto
   294 
   295 lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
   296 by auto
   297 
   298 lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
   299 by auto
   300 
   301 lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
   302 by auto
   303 
   304 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
   305 by simp
   306 
   307 lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
   308 by auto
   309 
   310 ML_file "Tools/bnf_gfp_util.ML"
   311 ML_file "Tools/bnf_gfp_tactics.ML"
   312 ML_file "Tools/bnf_gfp.ML"
   313 
   314 end