src/HOL/HOLCF/Algebraic.thy
author huffman
Sun Dec 19 05:15:31 2010 -0800 (2010-12-19)
changeset 41286 3d7685a4a5ff
parent 40888 28cd51cff70c
child 41287 029a6fc1bfb8
permissions -rw-r--r--
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
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@40502
     8
imports Universal Map_Functions
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@39989
    75
typedef (open) defl = "{S::fin_defl set. below.ideal S}"
huffman@40888
    76
by (rule below.ex_ideal)
huffman@27409
    77
huffman@39989
    78
instantiation defl :: below
huffman@27409
    79
begin
huffman@27409
    80
huffman@27409
    81
definition
huffman@39989
    82
  "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
huffman@27409
    83
huffman@27409
    84
instance ..
huffman@27409
    85
end
huffman@27409
    86
huffman@39989
    87
instance defl :: po
huffman@39989
    88
using type_definition_defl below_defl_def
huffman@39974
    89
by (rule below.typedef_ideal_po)
huffman@27409
    90
huffman@39989
    91
instance defl :: cpo
huffman@39989
    92
using type_definition_defl below_defl_def
huffman@39974
    93
by (rule below.typedef_ideal_cpo)
huffman@27409
    94
huffman@27409
    95
definition
huffman@39989
    96
  defl_principal :: "fin_defl \<Rightarrow> defl" where
huffman@39989
    97
  "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
huffman@27409
    98
huffman@39974
    99
lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
huffman@41286
   100
proof -
huffman@41286
   101
  obtain f :: "udom compact_basis \<Rightarrow> nat" where inj_f: "inj f"
huffman@41286
   102
    using compact_basis.countable ..
huffman@41286
   103
  have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
huffman@39974
   104
    apply (rule finite_imageI)
huffman@39974
   105
    apply (rule finite_vimageI)
huffman@39974
   106
    apply (rule Rep_fin_defl.finite_fixes)
huffman@39974
   107
    apply (simp add: inj_on_def Rep_compact_basis_inject)
huffman@39974
   108
    done
huffman@39974
   109
  have range_eq: "range Rep_compact_basis = {x. compact x}"
huffman@39974
   110
    using type_definition_compact_basis by (rule type_definition.Rep_range)
huffman@41286
   111
  have "inj (\<lambda>d. set_encode
huffman@41286
   112
    (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
huffman@39974
   113
    apply (rule inj_onI)
huffman@39974
   114
    apply (simp only: set_encode_eq *)
huffman@41286
   115
    apply (simp only: inj_image_eq_iff inj_f)
huffman@39974
   116
    apply (drule_tac f="image Rep_compact_basis" in arg_cong)
huffman@39974
   117
    apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
huffman@39974
   118
    apply (rule Rep_fin_defl_inject [THEN iffD1])
huffman@39974
   119
    apply (rule below_antisym)
huffman@39974
   120
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   121
    apply (drule_tac x=z in spec, simp)
huffman@39974
   122
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   123
    apply (drule_tac x=z in spec, simp)
huffman@39974
   124
    done
huffman@41286
   125
  thus ?thesis by - (rule exI)
huffman@39974
   126
qed
huffman@39974
   127
huffman@39989
   128
interpretation defl: ideal_completion below defl_principal Rep_defl
huffman@39989
   129
using type_definition_defl below_defl_def
huffman@39989
   130
using defl_principal_def fin_defl_countable
huffman@39984
   131
by (rule below.typedef_ideal_completion)
huffman@27409
   132
huffman@27409
   133
text {* Algebraic deflations are pointed *}
huffman@27409
   134
huffman@39989
   135
lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
huffman@39989
   136
apply (induct x rule: defl.principal_induct, simp)
huffman@39989
   137
apply (rule defl.principal_mono)
huffman@39974
   138
apply (simp add: below_fin_defl_def)
huffman@39974
   139
apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
huffman@27409
   140
done
huffman@27409
   141
huffman@39989
   142
instance defl :: pcpo
huffman@39989
   143
by intro_classes (fast intro: defl_minimal)
huffman@27409
   144
huffman@39989
   145
lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
huffman@39989
   146
by (rule defl_minimal [THEN UU_I, symmetric])
huffman@27409
   147
huffman@27409
   148
subsection {* Applying algebraic deflations *}
huffman@27409
   149
huffman@27409
   150
definition
huffman@39989
   151
  cast :: "defl \<rightarrow> udom \<rightarrow> udom"
huffman@27409
   152
where
huffman@39989
   153
  "cast = defl.basis_fun Rep_fin_defl"
huffman@27409
   154
huffman@39989
   155
lemma cast_defl_principal:
huffman@39989
   156
  "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
huffman@27409
   157
unfolding cast_def
huffman@39989
   158
apply (rule defl.basis_fun_principal)
huffman@31076
   159
apply (simp only: below_fin_defl_def)
huffman@27409
   160
done
huffman@27409
   161
huffman@27409
   162
lemma deflation_cast: "deflation (cast\<cdot>d)"
huffman@39989
   163
apply (induct d rule: defl.principal_induct)
huffman@27409
   164
apply (rule adm_subst [OF _ adm_deflation], simp)
huffman@39989
   165
apply (simp add: cast_defl_principal)
huffman@27409
   166
apply (rule finite_deflation_imp_deflation)
huffman@27409
   167
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   168
done
huffman@27409
   169
huffman@27409
   170
lemma finite_deflation_cast:
huffman@27409
   171
  "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
huffman@39989
   172
apply (drule defl.compact_imp_principal, clarify)
huffman@39989
   173
apply (simp add: cast_defl_principal)
huffman@27409
   174
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   175
done
huffman@27409
   176
wenzelm@30729
   177
interpretation cast: deflation "cast\<cdot>d"
huffman@27409
   178
by (rule deflation_cast)
huffman@27409
   179
huffman@33586
   180
declare cast.idem [simp]
huffman@33586
   181
huffman@39974
   182
lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
huffman@39974
   183
apply (rule finite_deflation_imp_compact)
huffman@39974
   184
apply (erule finite_deflation_cast)
huffman@31164
   185
done
huffman@31164
   186
huffman@39974
   187
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
huffman@39989
   188
apply (induct A rule: defl.principal_induct, simp)
huffman@39989
   189
apply (induct B rule: defl.principal_induct, simp)
huffman@39989
   190
apply (simp add: cast_defl_principal below_fin_defl_def)
huffman@31164
   191
done
huffman@31164
   192
huffman@39974
   193
lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
huffman@39974
   194
apply (rule iffI)
huffman@39974
   195
apply (simp only: compact_def cast_below_cast [symmetric])
huffman@40327
   196
apply (erule adm_subst [OF cont_Rep_cfun2])
huffman@39974
   197
apply (erule compact_cast)
brianh@39972
   198
done
brianh@39972
   199
huffman@31164
   200
lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
huffman@39974
   201
by (simp only: cast_below_cast)
huffman@31164
   202
huffman@33586
   203
lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
huffman@33586
   204
by (simp add: below_antisym cast_below_imp_below)
huffman@33586
   205
huffman@33586
   206
lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
huffman@39989
   207
apply (subst inst_defl_pcpo)
huffman@39989
   208
apply (subst cast_defl_principal)
huffman@33586
   209
apply (rule Abs_fin_defl_inverse)
huffman@33586
   210
apply (simp add: finite_deflation_UU)
huffman@33586
   211
done
huffman@33586
   212
huffman@33586
   213
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
huffman@33586
   214
by (rule cast.below [THEN UU_I])
huffman@33586
   215
huffman@27409
   216
end