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