src/HOLCF/Algebraic.thy
author huffman
Wed Oct 06 10:49:27 2010 -0700 (2010-10-06)
changeset 39974 b525988432e9
parent 39972 4244ff4f9649
child 39984 0300d5170622
permissions -rw-r--r--
major reorganization/simplification of HOLCF type classes:
removed profinite/bifinite classes and approx function;
universal domain uses approx_chain locale instead of bifinite class;
ideal_completion locale does not use 'take' functions, requires countable basis instead;
replaced type 'udom alg_defl' with type 'sfp';
replaced class 'rep' with class 'sfp';
renamed REP('a) to SFP('a);
huffman@27409
     1
(*  Title:      HOLCF/Algebraic.thy
huffman@27409
     2
    Author:     Brian Huffman
huffman@27409
     3
*)
huffman@27409
     4
huffman@39974
     5
header {* Algebraic deflations and SFP domains *}
huffman@27409
     6
huffman@27409
     7
theory Algebraic
huffman@39974
     8
imports Universal Bifinite
huffman@27409
     9
begin
huffman@27409
    10
huffman@27409
    11
subsection {* Type constructor for finite deflations *}
huffman@27409
    12
huffman@39974
    13
typedef (open) fin_defl = "{d::udom \<rightarrow> udom. finite_deflation d}"
huffman@39974
    14
by (fast intro: finite_deflation_UU)
huffman@27409
    15
huffman@39974
    16
instantiation fin_defl :: below
huffman@27409
    17
begin
huffman@27409
    18
huffman@31076
    19
definition below_fin_defl_def:
huffman@27409
    20
    "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
huffman@27409
    21
huffman@27409
    22
instance ..
huffman@27409
    23
end
huffman@27409
    24
huffman@39974
    25
instance fin_defl :: po
huffman@39974
    26
using type_definition_fin_defl below_fin_defl_def
huffman@39974
    27
by (rule typedef_po)
huffman@27409
    28
huffman@27409
    29
lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
huffman@27409
    30
using Rep_fin_defl by simp
huffman@27409
    31
huffman@31164
    32
lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
huffman@31164
    33
using finite_deflation_Rep_fin_defl
huffman@31164
    34
by (rule finite_deflation_imp_deflation)
huffman@31164
    35
wenzelm@30729
    36
interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
huffman@27409
    37
by (rule finite_deflation_Rep_fin_defl)
huffman@27409
    38
huffman@31076
    39
lemma fin_defl_belowI:
huffman@27409
    40
  "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
huffman@31076
    41
unfolding below_fin_defl_def
huffman@31076
    42
by (rule Rep_fin_defl.belowI)
huffman@27409
    43
huffman@31076
    44
lemma fin_defl_belowD:
huffman@27409
    45
  "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
huffman@31076
    46
unfolding below_fin_defl_def
huffman@31076
    47
by (rule Rep_fin_defl.belowD)
huffman@27409
    48
huffman@27409
    49
lemma fin_defl_eqI:
huffman@27409
    50
  "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
huffman@31076
    51
apply (rule below_antisym)
huffman@31076
    52
apply (rule fin_defl_belowI, simp)
huffman@31076
    53
apply (rule fin_defl_belowI, simp)
huffman@27409
    54
done
huffman@27409
    55
huffman@39974
    56
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
huffman@39974
    57
unfolding below_fin_defl_def .
huffman@39974
    58
huffman@27409
    59
lemma Abs_fin_defl_mono:
huffman@27409
    60
  "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
huffman@27409
    61
    \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
huffman@31076
    62
unfolding below_fin_defl_def
huffman@27409
    63
by (simp add: Abs_fin_defl_inverse)
huffman@27409
    64
huffman@39974
    65
lemma (in finite_deflation) compact_belowI:
huffman@39974
    66
  assumes "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
huffman@39974
    67
by (rule belowI, rule assms, erule subst, rule compact)
huffman@27409
    68
huffman@39974
    69
lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)"
huffman@39974
    70
using finite_deflation_Rep_fin_defl
huffman@39974
    71
by (rule finite_deflation_imp_compact)
huffman@33586
    72
huffman@27409
    73
subsection {* Defining algebraic deflations by ideal completion *}
huffman@27409
    74
huffman@39974
    75
text {*
huffman@39974
    76
  An SFP domain is one that can be represented as the limit of a
huffman@39974
    77
  sequence of finite posets.  Here we use omega-algebraic deflations
huffman@39974
    78
  (i.e. countable ideals of finite deflations) to model sequences of
huffman@39974
    79
  finite posets.
huffman@39974
    80
*}
huffman@39974
    81
huffman@39974
    82
typedef (open) sfp = "{S::fin_defl set. below.ideal S}"
huffman@31076
    83
by (fast intro: below.ideal_principal)
huffman@27409
    84
huffman@39974
    85
instantiation sfp :: below
huffman@27409
    86
begin
huffman@27409
    87
huffman@27409
    88
definition
huffman@39974
    89
  "x \<sqsubseteq> y \<longleftrightarrow> Rep_sfp x \<subseteq> Rep_sfp y"
huffman@27409
    90
huffman@27409
    91
instance ..
huffman@27409
    92
end
huffman@27409
    93
huffman@39974
    94
instance sfp :: po
huffman@39974
    95
using type_definition_sfp below_sfp_def
huffman@39974
    96
by (rule below.typedef_ideal_po)
huffman@27409
    97
huffman@39974
    98
instance sfp :: cpo
huffman@39974
    99
using type_definition_sfp below_sfp_def
huffman@39974
   100
by (rule below.typedef_ideal_cpo)
huffman@27409
   101
huffman@39974
   102
lemma Rep_sfp_lub:
huffman@39974
   103
  "chain Y \<Longrightarrow> Rep_sfp (\<Squnion>i. Y i) = (\<Union>i. Rep_sfp (Y i))"
huffman@39974
   104
using type_definition_sfp below_sfp_def
huffman@39974
   105
by (rule below.typedef_ideal_rep_contlub)
huffman@27409
   106
huffman@39974
   107
lemma ideal_Rep_sfp: "below.ideal (Rep_sfp xs)"
huffman@39974
   108
by (rule Rep_sfp [unfolded mem_Collect_eq])
huffman@27409
   109
huffman@27409
   110
definition
huffman@39974
   111
  sfp_principal :: "fin_defl \<Rightarrow> sfp" where
huffman@39974
   112
  "sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
huffman@27409
   113
huffman@39974
   114
lemma Rep_sfp_principal:
huffman@39974
   115
  "Rep_sfp (sfp_principal t) = {u. u \<sqsubseteq> t}"
huffman@39974
   116
unfolding sfp_principal_def
huffman@39974
   117
by (simp add: Abs_sfp_inverse below.ideal_principal)
huffman@27409
   118
huffman@39974
   119
lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
huffman@39974
   120
proof
huffman@39974
   121
  have *: "\<And>d. finite (approx_chain.place udom_approx `
huffman@39974
   122
               Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
huffman@39974
   123
    apply (rule finite_imageI)
huffman@39974
   124
    apply (rule finite_vimageI)
huffman@39974
   125
    apply (rule Rep_fin_defl.finite_fixes)
huffman@39974
   126
    apply (simp add: inj_on_def Rep_compact_basis_inject)
huffman@39974
   127
    done
huffman@39974
   128
  have range_eq: "range Rep_compact_basis = {x. compact x}"
huffman@39974
   129
    using type_definition_compact_basis by (rule type_definition.Rep_range)
huffman@39974
   130
  show "inj (\<lambda>d. set_encode
huffman@39974
   131
    (approx_chain.place udom_approx ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
huffman@39974
   132
    apply (rule inj_onI)
huffman@39974
   133
    apply (simp only: set_encode_eq *)
huffman@39974
   134
    apply (simp only: inj_image_eq_iff approx_chain.inj_place [OF udom_approx])
huffman@39974
   135
    apply (drule_tac f="image Rep_compact_basis" in arg_cong)
huffman@39974
   136
    apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
huffman@39974
   137
    apply (rule Rep_fin_defl_inject [THEN iffD1])
huffman@39974
   138
    apply (rule below_antisym)
huffman@39974
   139
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   140
    apply (drule_tac x=z in spec, simp)
huffman@39974
   141
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   142
    apply (drule_tac x=z in spec, simp)
huffman@39974
   143
    done
huffman@39974
   144
qed
huffman@39974
   145
huffman@39974
   146
interpretation sfp: ideal_completion below sfp_principal Rep_sfp
huffman@27409
   147
apply default
huffman@39974
   148
apply (rule ideal_Rep_sfp)
huffman@39974
   149
apply (erule Rep_sfp_lub)
huffman@39974
   150
apply (rule Rep_sfp_principal)
huffman@39974
   151
apply (simp only: below_sfp_def)
huffman@39974
   152
apply (rule fin_defl_countable)
huffman@27409
   153
done
huffman@27409
   154
huffman@27409
   155
text {* Algebraic deflations are pointed *}
huffman@27409
   156
huffman@39974
   157
lemma sfp_minimal: "sfp_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
huffman@39974
   158
apply (induct x rule: sfp.principal_induct, simp)
huffman@39974
   159
apply (rule sfp.principal_mono)
huffman@39974
   160
apply (simp add: below_fin_defl_def)
huffman@39974
   161
apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
huffman@27409
   162
done
huffman@27409
   163
huffman@39974
   164
instance sfp :: pcpo
huffman@39974
   165
by intro_classes (fast intro: sfp_minimal)
huffman@27409
   166
huffman@39974
   167
lemma inst_sfp_pcpo: "\<bottom> = sfp_principal (Abs_fin_defl \<bottom>)"
huffman@39974
   168
by (rule sfp_minimal [THEN UU_I, symmetric])
huffman@27409
   169
huffman@27409
   170
subsection {* Applying algebraic deflations *}
huffman@27409
   171
huffman@27409
   172
definition
huffman@39974
   173
  cast :: "sfp \<rightarrow> udom \<rightarrow> udom"
huffman@27409
   174
where
huffman@39974
   175
  "cast = sfp.basis_fun Rep_fin_defl"
huffman@27409
   176
huffman@39974
   177
lemma cast_sfp_principal:
huffman@39974
   178
  "cast\<cdot>(sfp_principal a) = Rep_fin_defl a"
huffman@27409
   179
unfolding cast_def
huffman@39974
   180
apply (rule sfp.basis_fun_principal)
huffman@31076
   181
apply (simp only: below_fin_defl_def)
huffman@27409
   182
done
huffman@27409
   183
huffman@27409
   184
lemma deflation_cast: "deflation (cast\<cdot>d)"
huffman@39974
   185
apply (induct d rule: sfp.principal_induct)
huffman@27409
   186
apply (rule adm_subst [OF _ adm_deflation], simp)
huffman@39974
   187
apply (simp add: cast_sfp_principal)
huffman@27409
   188
apply (rule finite_deflation_imp_deflation)
huffman@27409
   189
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   190
done
huffman@27409
   191
huffman@27409
   192
lemma finite_deflation_cast:
huffman@27409
   193
  "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
huffman@39974
   194
apply (drule sfp.compact_imp_principal, clarify)
huffman@39974
   195
apply (simp add: cast_sfp_principal)
huffman@27409
   196
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   197
done
huffman@27409
   198
wenzelm@30729
   199
interpretation cast: deflation "cast\<cdot>d"
huffman@27409
   200
by (rule deflation_cast)
huffman@27409
   201
huffman@33586
   202
declare cast.idem [simp]
huffman@33586
   203
huffman@39974
   204
lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
huffman@39974
   205
apply (rule finite_deflation_imp_compact)
huffman@39974
   206
apply (erule finite_deflation_cast)
huffman@31164
   207
done
huffman@31164
   208
huffman@39974
   209
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
huffman@39974
   210
apply (induct A rule: sfp.principal_induct, simp)
huffman@39974
   211
apply (induct B rule: sfp.principal_induct, simp)
huffman@39974
   212
apply (simp add: cast_sfp_principal below_fin_defl_def)
huffman@31164
   213
done
huffman@31164
   214
huffman@39974
   215
lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
huffman@39974
   216
apply (rule iffI)
huffman@39974
   217
apply (simp only: compact_def cast_below_cast [symmetric])
huffman@39974
   218
apply (erule adm_subst [OF cont_Rep_CFun2])
huffman@39974
   219
apply (erule compact_cast)
brianh@39972
   220
done
brianh@39972
   221
huffman@31164
   222
lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
huffman@39974
   223
by (simp only: cast_below_cast)
huffman@31164
   224
huffman@33586
   225
lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
huffman@33586
   226
by (simp add: below_antisym cast_below_imp_below)
huffman@33586
   227
huffman@33586
   228
lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
huffman@39974
   229
apply (subst inst_sfp_pcpo)
huffman@39974
   230
apply (subst cast_sfp_principal)
huffman@33586
   231
apply (rule Abs_fin_defl_inverse)
huffman@33586
   232
apply (simp add: finite_deflation_UU)
huffman@33586
   233
done
huffman@33586
   234
huffman@33586
   235
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
huffman@33586
   236
by (rule cast.below [THEN UU_I])
huffman@33586
   237
huffman@33586
   238
subsection {* Deflation membership relation *}
huffman@33586
   239
huffman@33586
   240
definition
huffman@39974
   241
  in_sfp :: "udom \<Rightarrow> sfp \<Rightarrow> bool" (infixl ":::" 50)
huffman@33586
   242
where
huffman@33586
   243
  "x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
huffman@33586
   244
huffman@39974
   245
lemma adm_in_sfp: "adm (\<lambda>x. x ::: A)"
huffman@39974
   246
unfolding in_sfp_def by simp
huffman@33586
   247
huffman@39974
   248
lemma in_sfpI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
huffman@39974
   249
unfolding in_sfp_def .
huffman@33586
   250
huffman@33586
   251
lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
huffman@39974
   252
unfolding in_sfp_def .
huffman@33586
   253
huffman@39974
   254
lemma cast_in_sfp [simp]: "cast\<cdot>A\<cdot>x ::: A"
huffman@39974
   255
unfolding in_sfp_def by (rule cast.idem)
huffman@33586
   256
huffman@39974
   257
lemma bottom_in_sfp [simp]: "\<bottom> ::: A"
huffman@39974
   258
unfolding in_sfp_def by (rule cast_strict2)
huffman@33586
   259
huffman@39974
   260
lemma sfp_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
huffman@39974
   261
unfolding in_sfp_def
huffman@33586
   262
 apply (rule deflation.belowD)
huffman@33586
   263
   apply (rule deflation_cast)
huffman@33586
   264
  apply (erule monofun_cfun_arg)
huffman@33586
   265
 apply assumption
huffman@33586
   266
done
huffman@33586
   267
huffman@39974
   268
lemma rev_sfp_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
huffman@39974
   269
by (rule sfp_belowD)
huffman@33586
   270
huffman@39974
   271
lemma sfp_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
huffman@33586
   272
apply (rule cast_below_imp_below)
huffman@33586
   273
apply (rule cast.belowI)
huffman@39974
   274
apply (simp add: in_sfp_def)
huffman@27409
   275
done
huffman@27409
   276
huffman@39974
   277
subsection {* Class of SFP domains *}
huffman@39974
   278
huffman@39974
   279
text {*
huffman@39974
   280
  We define a SFP domain as a pcpo that is isomorphic to some
huffman@39974
   281
  algebraic deflation over the universal domain.
huffman@39974
   282
*}
huffman@39974
   283
huffman@39974
   284
class sfp = pcpo +
huffman@39974
   285
  fixes emb :: "'a::pcpo \<rightarrow> udom"
huffman@39974
   286
  fixes prj :: "udom \<rightarrow> 'a::pcpo"
huffman@39974
   287
  fixes sfp :: "'a itself \<Rightarrow> sfp"
huffman@39974
   288
  assumes ep_pair_emb_prj: "ep_pair emb prj"
huffman@39974
   289
  assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
huffman@39974
   290
huffman@39974
   291
syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
huffman@39974
   292
translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
huffman@39974
   293
huffman@39974
   294
interpretation sfp:
huffman@39974
   295
  pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
huffman@39974
   296
  unfolding pcpo_ep_pair_def
huffman@39974
   297
  by (rule ep_pair_emb_prj)
huffman@39974
   298
huffman@39974
   299
lemmas emb_inverse = sfp.e_inverse
huffman@39974
   300
lemmas emb_prj_below = sfp.e_p_below
huffman@39974
   301
lemmas emb_eq_iff = sfp.e_eq_iff
huffman@39974
   302
lemmas emb_strict = sfp.e_strict
huffman@39974
   303
lemmas prj_strict = sfp.p_strict
huffman@39974
   304
huffman@39974
   305
subsection {* SFP domains have a countable compact basis *}
huffman@39974
   306
huffman@39974
   307
text {*
huffman@39974
   308
  Eventually it should be possible to generalize this to an unpointed
huffman@39974
   309
  variant of the sfp class.
huffman@39974
   310
*}
huffman@33586
   311
huffman@39974
   312
interpretation compact_basis:
huffman@39974
   313
  ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
huffman@39974
   314
proof -
huffman@39974
   315
  obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
huffman@39974
   316
  and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
huffman@39974
   317
    by (rule sfp.obtain_principal_chain)
huffman@39974
   318
  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
huffman@39974
   319
  interpret sfp_approx: approx_chain approx
huffman@39974
   320
  proof (rule approx_chain.intro)
huffman@39974
   321
    show "chain (\<lambda>i. approx i)"
huffman@39974
   322
      unfolding approx_def by (simp add: Y)
huffman@39974
   323
    show "(\<Squnion>i. approx i) = ID"
huffman@39974
   324
      unfolding approx_def
huffman@39974
   325
      by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
huffman@39974
   326
    show "\<And>i. finite_deflation (approx i)"
huffman@39974
   327
      unfolding approx_def
huffman@39974
   328
      apply (rule sfp.finite_deflation_p_d_e)
huffman@39974
   329
      apply (rule finite_deflation_cast)
huffman@39974
   330
      apply (rule sfp.compact_principal)
huffman@39974
   331
      apply (rule below_trans [OF monofun_cfun_fun])
huffman@39974
   332
      apply (rule is_ub_thelub, simp add: Y)
huffman@39974
   333
      apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
huffman@39974
   334
      done
huffman@39974
   335
  qed
huffman@39974
   336
  (* FIXME: why does show ?thesis fail here? *)
huffman@39974
   337
  show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
huffman@39974
   338
qed
huffman@39974
   339
huffman@39974
   340
subsection {* Type combinators *}
huffman@39974
   341
huffman@39974
   342
definition
huffman@39974
   343
  sfp_fun1 ::
huffman@39974
   344
    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
huffman@39974
   345
where
huffman@39974
   346
  "sfp_fun1 approx f =
huffman@39974
   347
    sfp.basis_fun (\<lambda>a.
huffman@39974
   348
      sfp_principal (Abs_fin_defl
huffman@39974
   349
        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
huffman@27409
   350
huffman@39974
   351
definition
huffman@39974
   352
  sfp_fun2 ::
huffman@39974
   353
    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
huffman@39974
   354
      \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
huffman@39974
   355
where
huffman@39974
   356
  "sfp_fun2 approx f =
huffman@39974
   357
    sfp.basis_fun (\<lambda>a.
huffman@39974
   358
      sfp.basis_fun (\<lambda>b.
huffman@39974
   359
        sfp_principal (Abs_fin_defl
huffman@39974
   360
          (udom_emb approx oo
huffman@39974
   361
            f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
huffman@39974
   362
huffman@39974
   363
lemma cast_sfp_fun1:
huffman@39974
   364
  assumes approx: "approx_chain approx"
huffman@39974
   365
  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
huffman@39974
   366
  shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
huffman@39974
   367
proof -
huffman@39974
   368
  have 1: "\<And>a. finite_deflation
huffman@39974
   369
        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
huffman@39974
   370
    apply (rule ep_pair.finite_deflation_e_d_p)
huffman@39974
   371
    apply (rule approx_chain.ep_pair_udom [OF approx])
huffman@39974
   372
    apply (rule f, rule finite_deflation_Rep_fin_defl)
huffman@27409
   373
    done
huffman@39974
   374
  show ?thesis
huffman@39974
   375
    by (induct A rule: sfp.principal_induct, simp)
huffman@39974
   376
       (simp only: sfp_fun1_def
huffman@39974
   377
                   sfp.basis_fun_principal
huffman@39974
   378
                   sfp.basis_fun_mono
huffman@39974
   379
                   sfp.principal_mono
huffman@39974
   380
                   Abs_fin_defl_mono [OF 1 1]
huffman@39974
   381
                   monofun_cfun below_refl
huffman@39974
   382
                   Rep_fin_defl_mono
huffman@39974
   383
                   cast_sfp_principal
huffman@39974
   384
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@39974
   385
qed
huffman@39974
   386
huffman@39974
   387
lemma cast_sfp_fun2:
huffman@39974
   388
  assumes approx: "approx_chain approx"
huffman@39974
   389
  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
huffman@39974
   390
                finite_deflation (f\<cdot>a\<cdot>b)"
huffman@39974
   391
  shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) =
huffman@39974
   392
    udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
huffman@39974
   393
proof -
huffman@39974
   394
  have 1: "\<And>a b. finite_deflation (udom_emb approx oo
huffman@39974
   395
      f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)"
huffman@39974
   396
    apply (rule ep_pair.finite_deflation_e_d_p)
huffman@39974
   397
    apply (rule ep_pair_udom [OF approx])
huffman@39974
   398
    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
huffman@39974
   399
    done
huffman@39974
   400
  show ?thesis
huffman@39974
   401
    by (induct A B rule: sfp.principal_induct2, simp, simp)
huffman@39974
   402
       (simp only: sfp_fun2_def
huffman@39974
   403
                   sfp.basis_fun_principal
huffman@39974
   404
                   sfp.basis_fun_mono
huffman@39974
   405
                   sfp.principal_mono
huffman@39974
   406
                   Abs_fin_defl_mono [OF 1 1]
huffman@39974
   407
                   monofun_cfun below_refl
huffman@39974
   408
                   Rep_fin_defl_mono
huffman@39974
   409
                   cast_sfp_principal
huffman@39974
   410
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@39974
   411
qed
huffman@39974
   412
huffman@39974
   413
subsection {* Instance for universal domain type *}
huffman@39974
   414
huffman@39974
   415
instantiation udom :: sfp
huffman@39974
   416
begin
huffman@39974
   417
huffman@39974
   418
definition [simp]:
huffman@39974
   419
  "emb = (ID :: udom \<rightarrow> udom)"
huffman@39974
   420
huffman@39974
   421
definition [simp]:
huffman@39974
   422
  "prj = (ID :: udom \<rightarrow> udom)"
huffman@39974
   423
huffman@39974
   424
definition
huffman@39974
   425
  "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
huffman@39974
   426
huffman@39974
   427
instance proof
huffman@39974
   428
  show "ep_pair emb (prj :: udom \<rightarrow> udom)"
huffman@39974
   429
    by (simp add: ep_pair.intro)
huffman@39974
   430
next
huffman@39974
   431
  show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
huffman@39974
   432
    unfolding sfp_udom_def
huffman@27409
   433
    apply (subst contlub_cfun_arg)
huffman@27409
   434
    apply (rule chainI)
huffman@39974
   435
    apply (rule sfp.principal_mono)
huffman@39974
   436
    apply (simp add: below_fin_defl_def)
huffman@39974
   437
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
huffman@39974
   438
    apply (rule chainE)
huffman@39974
   439
    apply (rule chain_udom_approx)
huffman@39974
   440
    apply (subst cast_sfp_principal)
huffman@39974
   441
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
huffman@27409
   442
    done
huffman@27409
   443
qed
huffman@27409
   444
huffman@27409
   445
end
huffman@39974
   446
huffman@39974
   447
subsection {* Instance for continuous function space *}
huffman@39974
   448
huffman@39974
   449
definition
huffman@39974
   450
  cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
huffman@39974
   451
where
huffman@39974
   452
  "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@39974
   453
huffman@39974
   454
lemma cfun_approx: "approx_chain cfun_approx"
huffman@39974
   455
proof (rule approx_chain.intro)
huffman@39974
   456
  show "chain (\<lambda>i. cfun_approx i)"
huffman@39974
   457
    unfolding cfun_approx_def by simp
huffman@39974
   458
  show "(\<Squnion>i. cfun_approx i) = ID"
huffman@39974
   459
    unfolding cfun_approx_def
huffman@39974
   460
    by (simp add: lub_distribs cfun_map_ID)
huffman@39974
   461
  show "\<And>i. finite_deflation (cfun_approx i)"
huffman@39974
   462
    unfolding cfun_approx_def
huffman@39974
   463
    by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
huffman@39974
   464
qed
huffman@39974
   465
huffman@39974
   466
definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
huffman@39974
   467
where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
huffman@39974
   468
huffman@39974
   469
lemma cast_cfun_sfp:
huffman@39974
   470
  "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
huffman@39974
   471
    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
huffman@39974
   472
unfolding cfun_sfp_def
huffman@39974
   473
apply (rule cast_sfp_fun2 [OF cfun_approx])
huffman@39974
   474
apply (erule (1) finite_deflation_cfun_map)
huffman@39974
   475
done
huffman@39974
   476
huffman@39974
   477
instantiation cfun :: (sfp, sfp) sfp
huffman@39974
   478
begin
huffman@39974
   479
huffman@39974
   480
definition
huffman@39974
   481
  "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
huffman@39974
   482
huffman@39974
   483
definition
huffman@39974
   484
  "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
huffman@39974
   485
huffman@39974
   486
definition
huffman@39974
   487
  "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
huffman@39974
   488
huffman@39974
   489
instance proof
huffman@39974
   490
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
huffman@39974
   491
    unfolding emb_cfun_def prj_cfun_def
huffman@39974
   492
    using ep_pair_udom [OF cfun_approx]
huffman@39974
   493
    by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
huffman@39974
   494
next
huffman@39974
   495
  show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
huffman@39974
   496
    unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
huffman@39974
   497
    by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
huffman@39974
   498
qed
huffman@39974
   499
huffman@39974
   500
end
huffman@39974
   501
huffman@39974
   502
lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
huffman@39974
   503
by (rule sfp_cfun_def)
huffman@39974
   504
huffman@39974
   505
end