src/HOLCF/Algebraic.thy
author huffman
Thu Oct 07 13:54:43 2010 -0700 (2010-10-07)
changeset 39985 310f98585107
parent 39984 0300d5170622
child 39989 ad60d7311f43
permissions -rw-r--r--
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman@27409
     1
(*  Title:      HOLCF/Algebraic.thy
huffman@27409
     2
    Author:     Brian Huffman
huffman@27409
     3
*)
huffman@27409
     4
huffman@39985
     5
header {* Algebraic deflations *}
huffman@27409
     6
huffman@27409
     7
theory Algebraic
huffman@39985
     8
imports Universal
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@27409
   260
end