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