src/HOLCF/Algebraic.thy
author huffman
Thu Oct 07 13:33:06 2010 -0700 (2010-10-07)
changeset 39984 0300d5170622
parent 39974 b525988432e9
child 39985 310f98585107
permissions -rw-r--r--
add lemma typedef_ideal_completion
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@27409
   102
definition
huffman@39974
   103
  sfp_principal :: "fin_defl \<Rightarrow> sfp" where
huffman@39974
   104
  "sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
huffman@27409
   105
huffman@39974
   106
lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
huffman@39974
   107
proof
huffman@39974
   108
  have *: "\<And>d. finite (approx_chain.place udom_approx `
huffman@39974
   109
               Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
huffman@39974
   110
    apply (rule finite_imageI)
huffman@39974
   111
    apply (rule finite_vimageI)
huffman@39974
   112
    apply (rule Rep_fin_defl.finite_fixes)
huffman@39974
   113
    apply (simp add: inj_on_def Rep_compact_basis_inject)
huffman@39974
   114
    done
huffman@39974
   115
  have range_eq: "range Rep_compact_basis = {x. compact x}"
huffman@39974
   116
    using type_definition_compact_basis by (rule type_definition.Rep_range)
huffman@39974
   117
  show "inj (\<lambda>d. set_encode
huffman@39974
   118
    (approx_chain.place udom_approx ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
huffman@39974
   119
    apply (rule inj_onI)
huffman@39974
   120
    apply (simp only: set_encode_eq *)
huffman@39974
   121
    apply (simp only: inj_image_eq_iff approx_chain.inj_place [OF udom_approx])
huffman@39974
   122
    apply (drule_tac f="image Rep_compact_basis" in arg_cong)
huffman@39974
   123
    apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
huffman@39974
   124
    apply (rule Rep_fin_defl_inject [THEN iffD1])
huffman@39974
   125
    apply (rule below_antisym)
huffman@39974
   126
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   127
    apply (drule_tac x=z in spec, simp)
huffman@39974
   128
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   129
    apply (drule_tac x=z in spec, simp)
huffman@39974
   130
    done
huffman@39974
   131
qed
huffman@39974
   132
huffman@39974
   133
interpretation sfp: ideal_completion below sfp_principal Rep_sfp
huffman@39984
   134
using type_definition_sfp below_sfp_def
huffman@39984
   135
using sfp_principal_def fin_defl_countable
huffman@39984
   136
by (rule below.typedef_ideal_completion)
huffman@27409
   137
huffman@27409
   138
text {* Algebraic deflations are pointed *}
huffman@27409
   139
huffman@39974
   140
lemma sfp_minimal: "sfp_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
huffman@39974
   141
apply (induct x rule: sfp.principal_induct, simp)
huffman@39974
   142
apply (rule sfp.principal_mono)
huffman@39974
   143
apply (simp add: below_fin_defl_def)
huffman@39974
   144
apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
huffman@27409
   145
done
huffman@27409
   146
huffman@39974
   147
instance sfp :: pcpo
huffman@39974
   148
by intro_classes (fast intro: sfp_minimal)
huffman@27409
   149
huffman@39974
   150
lemma inst_sfp_pcpo: "\<bottom> = sfp_principal (Abs_fin_defl \<bottom>)"
huffman@39974
   151
by (rule sfp_minimal [THEN UU_I, symmetric])
huffman@27409
   152
huffman@27409
   153
subsection {* Applying algebraic deflations *}
huffman@27409
   154
huffman@27409
   155
definition
huffman@39974
   156
  cast :: "sfp \<rightarrow> udom \<rightarrow> udom"
huffman@27409
   157
where
huffman@39974
   158
  "cast = sfp.basis_fun Rep_fin_defl"
huffman@27409
   159
huffman@39974
   160
lemma cast_sfp_principal:
huffman@39974
   161
  "cast\<cdot>(sfp_principal a) = Rep_fin_defl a"
huffman@27409
   162
unfolding cast_def
huffman@39974
   163
apply (rule sfp.basis_fun_principal)
huffman@31076
   164
apply (simp only: below_fin_defl_def)
huffman@27409
   165
done
huffman@27409
   166
huffman@27409
   167
lemma deflation_cast: "deflation (cast\<cdot>d)"
huffman@39974
   168
apply (induct d rule: sfp.principal_induct)
huffman@27409
   169
apply (rule adm_subst [OF _ adm_deflation], simp)
huffman@39974
   170
apply (simp add: cast_sfp_principal)
huffman@27409
   171
apply (rule finite_deflation_imp_deflation)
huffman@27409
   172
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   173
done
huffman@27409
   174
huffman@27409
   175
lemma finite_deflation_cast:
huffman@27409
   176
  "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
huffman@39974
   177
apply (drule sfp.compact_imp_principal, clarify)
huffman@39974
   178
apply (simp add: cast_sfp_principal)
huffman@27409
   179
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   180
done
huffman@27409
   181
wenzelm@30729
   182
interpretation cast: deflation "cast\<cdot>d"
huffman@27409
   183
by (rule deflation_cast)
huffman@27409
   184
huffman@33586
   185
declare cast.idem [simp]
huffman@33586
   186
huffman@39974
   187
lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
huffman@39974
   188
apply (rule finite_deflation_imp_compact)
huffman@39974
   189
apply (erule finite_deflation_cast)
huffman@31164
   190
done
huffman@31164
   191
huffman@39974
   192
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
huffman@39974
   193
apply (induct A rule: sfp.principal_induct, simp)
huffman@39974
   194
apply (induct B rule: sfp.principal_induct, simp)
huffman@39974
   195
apply (simp add: cast_sfp_principal below_fin_defl_def)
huffman@31164
   196
done
huffman@31164
   197
huffman@39974
   198
lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
huffman@39974
   199
apply (rule iffI)
huffman@39974
   200
apply (simp only: compact_def cast_below_cast [symmetric])
huffman@39974
   201
apply (erule adm_subst [OF cont_Rep_CFun2])
huffman@39974
   202
apply (erule compact_cast)
brianh@39972
   203
done
brianh@39972
   204
huffman@31164
   205
lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
huffman@39974
   206
by (simp only: cast_below_cast)
huffman@31164
   207
huffman@33586
   208
lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
huffman@33586
   209
by (simp add: below_antisym cast_below_imp_below)
huffman@33586
   210
huffman@33586
   211
lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
huffman@39974
   212
apply (subst inst_sfp_pcpo)
huffman@39974
   213
apply (subst cast_sfp_principal)
huffman@33586
   214
apply (rule Abs_fin_defl_inverse)
huffman@33586
   215
apply (simp add: finite_deflation_UU)
huffman@33586
   216
done
huffman@33586
   217
huffman@33586
   218
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
huffman@33586
   219
by (rule cast.below [THEN UU_I])
huffman@33586
   220
huffman@33586
   221
subsection {* Deflation membership relation *}
huffman@33586
   222
huffman@33586
   223
definition
huffman@39974
   224
  in_sfp :: "udom \<Rightarrow> sfp \<Rightarrow> bool" (infixl ":::" 50)
huffman@33586
   225
where
huffman@33586
   226
  "x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
huffman@33586
   227
huffman@39974
   228
lemma adm_in_sfp: "adm (\<lambda>x. x ::: A)"
huffman@39974
   229
unfolding in_sfp_def by simp
huffman@33586
   230
huffman@39974
   231
lemma in_sfpI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
huffman@39974
   232
unfolding in_sfp_def .
huffman@33586
   233
huffman@33586
   234
lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
huffman@39974
   235
unfolding in_sfp_def .
huffman@33586
   236
huffman@39974
   237
lemma cast_in_sfp [simp]: "cast\<cdot>A\<cdot>x ::: A"
huffman@39974
   238
unfolding in_sfp_def by (rule cast.idem)
huffman@33586
   239
huffman@39974
   240
lemma bottom_in_sfp [simp]: "\<bottom> ::: A"
huffman@39974
   241
unfolding in_sfp_def by (rule cast_strict2)
huffman@33586
   242
huffman@39974
   243
lemma sfp_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
huffman@39974
   244
unfolding in_sfp_def
huffman@33586
   245
 apply (rule deflation.belowD)
huffman@33586
   246
   apply (rule deflation_cast)
huffman@33586
   247
  apply (erule monofun_cfun_arg)
huffman@33586
   248
 apply assumption
huffman@33586
   249
done
huffman@33586
   250
huffman@39974
   251
lemma rev_sfp_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
huffman@39974
   252
by (rule sfp_belowD)
huffman@33586
   253
huffman@39974
   254
lemma sfp_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
huffman@33586
   255
apply (rule cast_below_imp_below)
huffman@33586
   256
apply (rule cast.belowI)
huffman@39974
   257
apply (simp add: in_sfp_def)
huffman@27409
   258
done
huffman@27409
   259
huffman@39974
   260
subsection {* Class of SFP domains *}
huffman@39974
   261
huffman@39974
   262
text {*
huffman@39974
   263
  We define a SFP domain as a pcpo that is isomorphic to some
huffman@39974
   264
  algebraic deflation over the universal domain.
huffman@39974
   265
*}
huffman@39974
   266
huffman@39974
   267
class sfp = pcpo +
huffman@39974
   268
  fixes emb :: "'a::pcpo \<rightarrow> udom"
huffman@39974
   269
  fixes prj :: "udom \<rightarrow> 'a::pcpo"
huffman@39974
   270
  fixes sfp :: "'a itself \<Rightarrow> sfp"
huffman@39974
   271
  assumes ep_pair_emb_prj: "ep_pair emb prj"
huffman@39974
   272
  assumes cast_SFP: "cast\<cdot>(sfp TYPE('a)) = emb oo prj"
huffman@39974
   273
huffman@39974
   274
syntax "_SFP" :: "type \<Rightarrow> sfp"  ("(1SFP/(1'(_')))")
huffman@39974
   275
translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
huffman@39974
   276
huffman@39974
   277
interpretation sfp:
huffman@39974
   278
  pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
huffman@39974
   279
  unfolding pcpo_ep_pair_def
huffman@39974
   280
  by (rule ep_pair_emb_prj)
huffman@39974
   281
huffman@39974
   282
lemmas emb_inverse = sfp.e_inverse
huffman@39974
   283
lemmas emb_prj_below = sfp.e_p_below
huffman@39974
   284
lemmas emb_eq_iff = sfp.e_eq_iff
huffman@39974
   285
lemmas emb_strict = sfp.e_strict
huffman@39974
   286
lemmas prj_strict = sfp.p_strict
huffman@39974
   287
huffman@39974
   288
subsection {* SFP domains have a countable compact basis *}
huffman@39974
   289
huffman@39974
   290
text {*
huffman@39974
   291
  Eventually it should be possible to generalize this to an unpointed
huffman@39974
   292
  variant of the sfp class.
huffman@39974
   293
*}
huffman@33586
   294
huffman@39974
   295
interpretation compact_basis:
huffman@39974
   296
  ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
huffman@39974
   297
proof -
huffman@39974
   298
  obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
huffman@39974
   299
  and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
huffman@39974
   300
    by (rule sfp.obtain_principal_chain)
huffman@39974
   301
  def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(sfp_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a"
huffman@39974
   302
  interpret sfp_approx: approx_chain approx
huffman@39974
   303
  proof (rule approx_chain.intro)
huffman@39974
   304
    show "chain (\<lambda>i. approx i)"
huffman@39974
   305
      unfolding approx_def by (simp add: Y)
huffman@39974
   306
    show "(\<Squnion>i. approx i) = ID"
huffman@39974
   307
      unfolding approx_def
huffman@39974
   308
      by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
huffman@39974
   309
    show "\<And>i. finite_deflation (approx i)"
huffman@39974
   310
      unfolding approx_def
huffman@39974
   311
      apply (rule sfp.finite_deflation_p_d_e)
huffman@39974
   312
      apply (rule finite_deflation_cast)
huffman@39974
   313
      apply (rule sfp.compact_principal)
huffman@39974
   314
      apply (rule below_trans [OF monofun_cfun_fun])
huffman@39974
   315
      apply (rule is_ub_thelub, simp add: Y)
huffman@39974
   316
      apply (simp add: lub_distribs Y SFP [symmetric] cast_SFP)
huffman@39974
   317
      done
huffman@39974
   318
  qed
huffman@39974
   319
  (* FIXME: why does show ?thesis fail here? *)
huffman@39974
   320
  show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" ..
huffman@39974
   321
qed
huffman@39974
   322
huffman@39974
   323
subsection {* Type combinators *}
huffman@39974
   324
huffman@39974
   325
definition
huffman@39974
   326
  sfp_fun1 ::
huffman@39974
   327
    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (sfp \<rightarrow> sfp)"
huffman@39974
   328
where
huffman@39974
   329
  "sfp_fun1 approx f =
huffman@39974
   330
    sfp.basis_fun (\<lambda>a.
huffman@39974
   331
      sfp_principal (Abs_fin_defl
huffman@39974
   332
        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))"
huffman@27409
   333
huffman@39974
   334
definition
huffman@39974
   335
  sfp_fun2 ::
huffman@39974
   336
    "(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
huffman@39974
   337
      \<Rightarrow> (sfp \<rightarrow> sfp \<rightarrow> sfp)"
huffman@39974
   338
where
huffman@39974
   339
  "sfp_fun2 approx f =
huffman@39974
   340
    sfp.basis_fun (\<lambda>a.
huffman@39974
   341
      sfp.basis_fun (\<lambda>b.
huffman@39974
   342
        sfp_principal (Abs_fin_defl
huffman@39974
   343
          (udom_emb approx oo
huffman@39974
   344
            f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))"
huffman@39974
   345
huffman@39974
   346
lemma cast_sfp_fun1:
huffman@39974
   347
  assumes approx: "approx_chain approx"
huffman@39974
   348
  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
huffman@39974
   349
  shows "cast\<cdot>(sfp_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx"
huffman@39974
   350
proof -
huffman@39974
   351
  have 1: "\<And>a. finite_deflation
huffman@39974
   352
        (udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)"
huffman@39974
   353
    apply (rule ep_pair.finite_deflation_e_d_p)
huffman@39974
   354
    apply (rule approx_chain.ep_pair_udom [OF approx])
huffman@39974
   355
    apply (rule f, rule finite_deflation_Rep_fin_defl)
huffman@27409
   356
    done
huffman@39974
   357
  show ?thesis
huffman@39974
   358
    by (induct A rule: sfp.principal_induct, simp)
huffman@39974
   359
       (simp only: sfp_fun1_def
huffman@39974
   360
                   sfp.basis_fun_principal
huffman@39974
   361
                   sfp.basis_fun_mono
huffman@39974
   362
                   sfp.principal_mono
huffman@39974
   363
                   Abs_fin_defl_mono [OF 1 1]
huffman@39974
   364
                   monofun_cfun below_refl
huffman@39974
   365
                   Rep_fin_defl_mono
huffman@39974
   366
                   cast_sfp_principal
huffman@39974
   367
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@39974
   368
qed
huffman@39974
   369
huffman@39974
   370
lemma cast_sfp_fun2:
huffman@39974
   371
  assumes approx: "approx_chain approx"
huffman@39974
   372
  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
huffman@39974
   373
                finite_deflation (f\<cdot>a\<cdot>b)"
huffman@39974
   374
  shows "cast\<cdot>(sfp_fun2 approx f\<cdot>A\<cdot>B) =
huffman@39974
   375
    udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx"
huffman@39974
   376
proof -
huffman@39974
   377
  have 1: "\<And>a b. finite_deflation (udom_emb approx oo
huffman@39974
   378
      f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)"
huffman@39974
   379
    apply (rule ep_pair.finite_deflation_e_d_p)
huffman@39974
   380
    apply (rule ep_pair_udom [OF approx])
huffman@39974
   381
    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
huffman@39974
   382
    done
huffman@39974
   383
  show ?thesis
huffman@39974
   384
    by (induct A B rule: sfp.principal_induct2, simp, simp)
huffman@39974
   385
       (simp only: sfp_fun2_def
huffman@39974
   386
                   sfp.basis_fun_principal
huffman@39974
   387
                   sfp.basis_fun_mono
huffman@39974
   388
                   sfp.principal_mono
huffman@39974
   389
                   Abs_fin_defl_mono [OF 1 1]
huffman@39974
   390
                   monofun_cfun below_refl
huffman@39974
   391
                   Rep_fin_defl_mono
huffman@39974
   392
                   cast_sfp_principal
huffman@39974
   393
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@39974
   394
qed
huffman@39974
   395
huffman@39974
   396
subsection {* Instance for universal domain type *}
huffman@39974
   397
huffman@39974
   398
instantiation udom :: sfp
huffman@39974
   399
begin
huffman@39974
   400
huffman@39974
   401
definition [simp]:
huffman@39974
   402
  "emb = (ID :: udom \<rightarrow> udom)"
huffman@39974
   403
huffman@39974
   404
definition [simp]:
huffman@39974
   405
  "prj = (ID :: udom \<rightarrow> udom)"
huffman@39974
   406
huffman@39974
   407
definition
huffman@39974
   408
  "sfp (t::udom itself) = (\<Squnion>i. sfp_principal (Abs_fin_defl (udom_approx i)))"
huffman@39974
   409
huffman@39974
   410
instance proof
huffman@39974
   411
  show "ep_pair emb (prj :: udom \<rightarrow> udom)"
huffman@39974
   412
    by (simp add: ep_pair.intro)
huffman@39974
   413
next
huffman@39974
   414
  show "cast\<cdot>SFP(udom) = emb oo (prj :: udom \<rightarrow> udom)"
huffman@39974
   415
    unfolding sfp_udom_def
huffman@27409
   416
    apply (subst contlub_cfun_arg)
huffman@27409
   417
    apply (rule chainI)
huffman@39974
   418
    apply (rule sfp.principal_mono)
huffman@39974
   419
    apply (simp add: below_fin_defl_def)
huffman@39974
   420
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
huffman@39974
   421
    apply (rule chainE)
huffman@39974
   422
    apply (rule chain_udom_approx)
huffman@39974
   423
    apply (subst cast_sfp_principal)
huffman@39974
   424
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
huffman@27409
   425
    done
huffman@27409
   426
qed
huffman@27409
   427
huffman@27409
   428
end
huffman@39974
   429
huffman@39974
   430
subsection {* Instance for continuous function space *}
huffman@39974
   431
huffman@39974
   432
definition
huffman@39974
   433
  cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
huffman@39974
   434
where
huffman@39974
   435
  "cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@39974
   436
huffman@39974
   437
lemma cfun_approx: "approx_chain cfun_approx"
huffman@39974
   438
proof (rule approx_chain.intro)
huffman@39974
   439
  show "chain (\<lambda>i. cfun_approx i)"
huffman@39974
   440
    unfolding cfun_approx_def by simp
huffman@39974
   441
  show "(\<Squnion>i. cfun_approx i) = ID"
huffman@39974
   442
    unfolding cfun_approx_def
huffman@39974
   443
    by (simp add: lub_distribs cfun_map_ID)
huffman@39974
   444
  show "\<And>i. finite_deflation (cfun_approx i)"
huffman@39974
   445
    unfolding cfun_approx_def
huffman@39974
   446
    by (intro finite_deflation_cfun_map finite_deflation_udom_approx)
huffman@39974
   447
qed
huffman@39974
   448
huffman@39974
   449
definition cfun_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
huffman@39974
   450
where "cfun_sfp = sfp_fun2 cfun_approx cfun_map"
huffman@39974
   451
huffman@39974
   452
lemma cast_cfun_sfp:
huffman@39974
   453
  "cast\<cdot>(cfun_sfp\<cdot>A\<cdot>B) =
huffman@39974
   454
    udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx"
huffman@39974
   455
unfolding cfun_sfp_def
huffman@39974
   456
apply (rule cast_sfp_fun2 [OF cfun_approx])
huffman@39974
   457
apply (erule (1) finite_deflation_cfun_map)
huffman@39974
   458
done
huffman@39974
   459
huffman@39974
   460
instantiation cfun :: (sfp, sfp) sfp
huffman@39974
   461
begin
huffman@39974
   462
huffman@39974
   463
definition
huffman@39974
   464
  "emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb"
huffman@39974
   465
huffman@39974
   466
definition
huffman@39974
   467
  "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx"
huffman@39974
   468
huffman@39974
   469
definition
huffman@39974
   470
  "sfp (t::('a \<rightarrow> 'b) itself) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
huffman@39974
   471
huffman@39974
   472
instance proof
huffman@39974
   473
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
huffman@39974
   474
    unfolding emb_cfun_def prj_cfun_def
huffman@39974
   475
    using ep_pair_udom [OF cfun_approx]
huffman@39974
   476
    by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj)
huffman@39974
   477
next
huffman@39974
   478
  show "cast\<cdot>SFP('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
huffman@39974
   479
    unfolding emb_cfun_def prj_cfun_def sfp_cfun_def cast_cfun_sfp
huffman@39974
   480
    by (simp add: cast_SFP oo_def expand_cfun_eq cfun_map_map)
huffman@39974
   481
qed
huffman@39974
   482
huffman@39974
   483
end
huffman@39974
   484
huffman@39974
   485
lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
huffman@39974
   486
by (rule sfp_cfun_def)
huffman@39974
   487
huffman@39974
   488
end