src/HOL/BNF_Greatest_Fixpoint.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (21 months ago)
changeset 66983 df83b66f1d94
parent 66248 df85956228c2
child 67091 1393c2340eec
permissions -rw-r--r--
proper merge (amending fb46c031c841);
blanchet@58128
     1
(*  Title:      HOL/BNF_Greatest_Fixpoint.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@55059
     3
    Author:     Lorenz Panny, TU Muenchen
blanchet@55059
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@57698
     5
    Copyright   2012, 2013, 2014
blanchet@48975
     6
blanchet@58352
     7
Greatest fixpoint (codatatype) operation on bounded natural functors.
blanchet@48975
     8
*)
blanchet@48975
     9
wenzelm@60758
    10
section \<open>Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors\<close>
blanchet@48975
    11
blanchet@58128
    12
theory BNF_Greatest_Fixpoint
blanchet@58128
    13
imports BNF_Fixpoint_Base String
blanchet@48975
    14
keywords
blanchet@53310
    15
  "codatatype" :: thy_decl and
panny@53822
    16
  "primcorecursive" :: thy_goal and
panny@53822
    17
  "primcorec" :: thy_decl
blanchet@48975
    18
begin
blanchet@48975
    19
wenzelm@66248
    20
alias proj = Equiv_Relations.proj
blanchet@55024
    21
blanchet@55966
    22
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
blanchet@57896
    23
  by simp
blanchet@55966
    24
blanchet@55966
    25
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
blanchet@57896
    26
  by (cases s) auto
blanchet@55966
    27
blanchet@54485
    28
lemma not_TrueE: "\<not> True \<Longrightarrow> P"
blanchet@57896
    29
  by (erule notE, rule TrueI)
blanchet@54485
    30
blanchet@54485
    31
lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
blanchet@57896
    32
  by fast
blanchet@54485
    33
blanchet@49312
    34
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
blanchet@57896
    35
  by fast
blanchet@49312
    36
blanchet@49312
    37
lemma equiv_proj:
blanchet@57896
    38
  assumes e: "equiv A R" and m: "z \<in> R"
blanchet@49312
    39
  shows "(proj R o fst) z = (proj R o snd) z"
blanchet@49312
    40
proof -
blanchet@57896
    41
  from m have z: "(fst z, snd z) \<in> R" by auto
traytel@53695
    42
  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"
traytel@53695
    43
    unfolding equiv_def sym_def trans_def by blast+
traytel@53695
    44
  then show ?thesis unfolding proj_def[abs_def] by auto
blanchet@49312
    45
qed
blanchet@49312
    46
blanchet@49312
    47
(* Operators: *)
blanchet@49312
    48
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
blanchet@49312
    49
traytel@51447
    50
lemma Id_on_Gr: "Id_on A = Gr A id"
blanchet@57896
    51
  unfolding Id_on_def Gr_def by auto
blanchet@49312
    52
blanchet@49312
    53
lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
blanchet@57896
    54
  unfolding image2_def by auto
blanchet@49312
    55
blanchet@49312
    56
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
blanchet@57896
    57
  by auto
blanchet@49312
    58
blanchet@49312
    59
lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
blanchet@57896
    60
  unfolding image2_def Gr_def by auto
blanchet@49312
    61
blanchet@49312
    62
lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
blanchet@57896
    63
  unfolding Gr_def by simp
blanchet@49312
    64
blanchet@49312
    65
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
blanchet@57896
    66
  unfolding Gr_def by simp
blanchet@49312
    67
wenzelm@61943
    68
lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B"
blanchet@57896
    69
  unfolding Gr_def by auto
blanchet@49312
    70
blanchet@54485
    71
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
blanchet@57896
    72
  by blast
blanchet@54485
    73
blanchet@54485
    74
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})"
blanchet@57896
    75
  by blast
blanchet@54485
    76
haftmann@61424
    77
lemma in_rel_Collect_case_prod_eq: "in_rel (Collect (case_prod X)) = X"
blanchet@57896
    78
  unfolding fun_eq_iff by auto
traytel@51893
    79
haftmann@61424
    80
lemma Collect_case_prod_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
blanchet@57896
    81
  by auto
traytel@51893
    82
haftmann@61424
    83
lemma Collect_case_prod_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
blanchet@57896
    84
  by force
traytel@51893
    85
traytel@51893
    86
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
blanchet@57896
    87
  unfolding fun_eq_iff by auto
traytel@51893
    88
traytel@51893
    89
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
blanchet@57896
    90
  unfolding fun_eq_iff by auto
traytel@51893
    91
traytel@51893
    92
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
blanchet@57896
    93
  unfolding Gr_def Grp_def fun_eq_iff by auto
traytel@51893
    94
blanchet@49312
    95
definition relImage where
blanchet@57896
    96
  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
blanchet@49312
    97
blanchet@49312
    98
definition relInvImage where
blanchet@57896
    99
  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
blanchet@49312
   100
blanchet@49312
   101
lemma relImage_Gr:
blanchet@57896
   102
  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
blanchet@57896
   103
  unfolding relImage_def Gr_def relcomp_def by auto
blanchet@49312
   104
blanchet@49312
   105
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"
blanchet@57896
   106
  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
blanchet@49312
   107
blanchet@49312
   108
lemma relImage_mono:
blanchet@57896
   109
  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
blanchet@57896
   110
  unfolding relImage_def by auto
blanchet@49312
   111
blanchet@49312
   112
lemma relInvImage_mono:
blanchet@57896
   113
  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
blanchet@57896
   114
  unfolding relInvImage_def by auto
blanchet@49312
   115
traytel@51447
   116
lemma relInvImage_Id_on:
blanchet@57896
   117
  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
blanchet@57896
   118
  unfolding relInvImage_def Id_on_def by auto
blanchet@49312
   119
blanchet@49312
   120
lemma relInvImage_UNIV_relImage:
blanchet@57896
   121
  "R \<subseteq> relInvImage UNIV (relImage R f) f"
blanchet@57896
   122
  unfolding relInvImage_def relImage_def by auto
blanchet@49312
   123
blanchet@49312
   124
lemma relImage_proj:
blanchet@57896
   125
  assumes "equiv A R"
blanchet@57896
   126
  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
blanchet@57896
   127
  unfolding relImage_def Id_on_def
blanchet@57896
   128
  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
blanchet@57896
   129
  by (auto simp: proj_preserves)
blanchet@49312
   130
blanchet@49312
   131
lemma relImage_relInvImage:
wenzelm@61943
   132
  assumes "R \<subseteq> f ` A \<times> f ` A"
blanchet@57896
   133
  shows "relImage (relInvImage A R f) f = R"
blanchet@57896
   134
  using assms unfolding relImage_def relInvImage_def by fast
blanchet@49312
   135
blanchet@49312
   136
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
blanchet@57896
   137
  by simp
blanchet@49312
   138
blanchet@64413
   139
lemma fst_diag_id: "(fst \<circ> (\<lambda>x. (x, x))) z = id z" by simp
blanchet@64413
   140
lemma snd_diag_id: "(snd \<circ> (\<lambda>x. (x, x))) z = id z" by simp
blanchet@49312
   141
traytel@55644
   142
lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
traytel@55644
   143
lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
traytel@55644
   144
lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto
traytel@55644
   145
lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto
blanchet@49312
   146
blanchet@49312
   147
definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
blanchet@49312
   148
definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
blanchet@49312
   149
definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
blanchet@49312
   150
blanchet@49312
   151
lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
blanchet@57896
   152
  unfolding Shift_def Succ_def by simp
blanchet@49312
   153
blanchet@49312
   154
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
blanchet@57896
   155
  unfolding Succ_def by simp
blanchet@49312
   156
blanchet@49312
   157
lemmas SuccE = SuccD[elim_format]
blanchet@49312
   158
blanchet@49312
   159
lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
blanchet@57896
   160
  unfolding Succ_def by simp
blanchet@49312
   161
blanchet@49312
   162
lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
blanchet@57896
   163
  unfolding Shift_def by simp
blanchet@49312
   164
blanchet@49312
   165
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
blanchet@57896
   166
  unfolding Succ_def Shift_def by auto
blanchet@49312
   167
blanchet@49312
   168
lemma length_Cons: "length (x # xs) = Suc (length xs)"
blanchet@57896
   169
  by simp
blanchet@49312
   170
blanchet@49312
   171
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
blanchet@57896
   172
  by simp
blanchet@49312
   173
blanchet@49312
   174
(*injection into the field of a cardinal*)
blanchet@49312
   175
definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
blanchet@49312
   176
definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
blanchet@49312
   177
blanchet@49312
   178
lemma ex_toCard_pred:
blanchet@57896
   179
  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
blanchet@57896
   180
  unfolding toCard_pred_def
blanchet@57896
   181
  using card_of_ordLeq[of A "Field r"]
blanchet@57896
   182
    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
blanchet@57896
   183
  by blast
blanchet@49312
   184
blanchet@49312
   185
lemma toCard_pred_toCard:
blanchet@49312
   186
  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
blanchet@57896
   187
  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
blanchet@49312
   188
blanchet@57896
   189
lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y"
blanchet@57896
   190
  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
blanchet@49312
   191
blanchet@49312
   192
definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
blanchet@49312
   193
blanchet@49312
   194
lemma fromCard_toCard:
blanchet@57896
   195
  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
blanchet@57896
   196
  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
blanchet@49312
   197
blanchet@49312
   198
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
blanchet@57896
   199
  unfolding Field_card_of csum_def by auto
blanchet@49312
   200
blanchet@49312
   201
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
blanchet@57896
   202
  unfolding Field_card_of csum_def by auto
blanchet@49312
   203
blanchet@64413
   204
lemma rec_nat_0_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
blanchet@57896
   205
  by auto
blanchet@49312
   206
blanchet@64413
   207
lemma rec_nat_Suc_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
blanchet@57896
   208
  by auto
blanchet@49312
   209
blanchet@64413
   210
lemma rec_list_Nil_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
blanchet@57896
   211
  by auto
blanchet@49312
   212
blanchet@64413
   213
lemma rec_list_Cons_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
blanchet@57896
   214
  by auto
blanchet@49312
   215
blanchet@49312
   216
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
blanchet@57896
   217
  by simp
blanchet@49312
   218
traytel@52731
   219
definition image2p where
traytel@52731
   220
  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
traytel@52731
   221
blanchet@55463
   222
lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
traytel@52731
   223
  unfolding image2p_def by blast
traytel@52731
   224
blanchet@55463
   225
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"
traytel@52731
   226
  unfolding image2p_def by blast
traytel@52731
   227
blanchet@55945
   228
lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
blanchet@55945
   229
  unfolding rel_fun_def image2p_def by auto
traytel@52731
   230
blanchet@55945
   231
lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
blanchet@55945
   232
  unfolding rel_fun_def image2p_def by auto
traytel@52731
   233
blanchet@55022
   234
wenzelm@60758
   235
subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close>
blanchet@55022
   236
blanchet@55022
   237
lemma equiv_Eps_in:
blanchet@64413
   238
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (\<lambda>x. x \<in> X) \<in> X"
blanchet@57896
   239
  apply (rule someI2_ex)
blanchet@57896
   240
  using in_quotient_imp_non_empty by blast
blanchet@55022
   241
blanchet@55022
   242
lemma equiv_Eps_preserves:
blanchet@57896
   243
  assumes ECH: "equiv A r" and X: "X \<in> A//r"
blanchet@64413
   244
  shows "Eps (\<lambda>x. x \<in> X) \<in> A"
blanchet@57896
   245
  apply (rule in_mono[rule_format])
blanchet@57896
   246
   using assms apply (rule in_quotient_imp_subset)
blanchet@57896
   247
  by (rule equiv_Eps_in) (rule assms)+
blanchet@55022
   248
blanchet@55022
   249
lemma proj_Eps:
blanchet@57896
   250
  assumes "equiv A r" and "X \<in> A//r"
blanchet@64413
   251
  shows "proj r (Eps (\<lambda>x. x \<in> X)) = X"
blanchet@57896
   252
unfolding proj_def
blanchet@57896
   253
proof auto
blanchet@55022
   254
  fix x assume x: "x \<in> X"
blanchet@64413
   255
  thus "(Eps (\<lambda>x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
blanchet@55022
   256
next
blanchet@64413
   257
  fix x assume "(Eps (\<lambda>x. x \<in> X),x) \<in> r"
blanchet@55022
   258
  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
blanchet@55022
   259
qed
blanchet@55022
   260
blanchet@64413
   261
definition univ where "univ f X == f (Eps (\<lambda>x. x \<in> X))"
blanchet@55022
   262
blanchet@55022
   263
lemma univ_commute:
blanchet@55022
   264
assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
blanchet@55022
   265
shows "(univ f) (proj r x) = f x"
blanchet@57896
   266
proof (unfold univ_def)
blanchet@55022
   267
  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
blanchet@64413
   268
  hence "Eps (\<lambda>y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
blanchet@64413
   269
  moreover have "proj r (Eps (\<lambda>y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
blanchet@64413
   270
  ultimately have "(x, Eps (\<lambda>y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
blanchet@64413
   271
  thus "f (Eps (\<lambda>y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
blanchet@55022
   272
qed
blanchet@55022
   273
blanchet@55022
   274
lemma univ_preserves:
blanchet@57991
   275
  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
blanchet@57896
   276
  shows "\<forall>X \<in> A//r. univ f X \<in> B"
blanchet@55022
   277
proof
blanchet@55022
   278
  fix X assume "X \<in> A//r"
blanchet@55022
   279
  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
blanchet@57991
   280
  hence "univ f X = f x" using ECH RES univ_commute by fastforce
blanchet@55022
   281
  thus "univ f X \<in> B" using x PRES by simp
blanchet@55022
   282
qed
blanchet@55022
   283
blanchet@55062
   284
ML_file "Tools/BNF/bnf_gfp_util.ML"
blanchet@55062
   285
ML_file "Tools/BNF/bnf_gfp_tactics.ML"
blanchet@55062
   286
ML_file "Tools/BNF/bnf_gfp.ML"
blanchet@55538
   287
ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
blanchet@55538
   288
ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
blanchet@49309
   289
blanchet@48975
   290
end