src/HOL/HOLCF/Algebraic.thy
author wenzelm
Fri Oct 12 18:58:20 2012 +0200 (2012-10-12)
changeset 49834 b27bbb021df1
parent 41959 b460124855b8
child 58880 0baae4311a9f
permissions -rw-r--r--
discontinued obsolete typedef (open) syntax;
wenzelm@41959
     1
(*  Title:      HOL/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@41287
    11
default_sort bifinite
huffman@41287
    12
huffman@27409
    13
subsection {* Type constructor for finite deflations *}
huffman@27409
    14
wenzelm@49834
    15
typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
huffman@41430
    16
by (fast intro: finite_deflation_bottom)
huffman@27409
    17
huffman@41287
    18
instantiation fin_defl :: (bifinite) below
huffman@27409
    19
begin
huffman@27409
    20
huffman@31076
    21
definition below_fin_defl_def:
huffman@41287
    22
  "below \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
huffman@27409
    23
huffman@27409
    24
instance ..
huffman@27409
    25
end
huffman@27409
    26
huffman@41287
    27
instance fin_defl :: (bifinite) po
huffman@39974
    28
using type_definition_fin_defl below_fin_defl_def
huffman@39974
    29
by (rule typedef_po)
huffman@27409
    30
huffman@27409
    31
lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
huffman@27409
    32
using Rep_fin_defl by simp
huffman@27409
    33
huffman@31164
    34
lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
huffman@31164
    35
using finite_deflation_Rep_fin_defl
huffman@31164
    36
by (rule finite_deflation_imp_deflation)
huffman@31164
    37
wenzelm@30729
    38
interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
huffman@27409
    39
by (rule finite_deflation_Rep_fin_defl)
huffman@27409
    40
huffman@31076
    41
lemma fin_defl_belowI:
huffman@27409
    42
  "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
huffman@31076
    43
unfolding below_fin_defl_def
huffman@31076
    44
by (rule Rep_fin_defl.belowI)
huffman@27409
    45
huffman@31076
    46
lemma fin_defl_belowD:
huffman@27409
    47
  "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
huffman@31076
    48
unfolding below_fin_defl_def
huffman@31076
    49
by (rule Rep_fin_defl.belowD)
huffman@27409
    50
huffman@27409
    51
lemma fin_defl_eqI:
huffman@27409
    52
  "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
huffman@31076
    53
apply (rule below_antisym)
huffman@31076
    54
apply (rule fin_defl_belowI, simp)
huffman@31076
    55
apply (rule fin_defl_belowI, simp)
huffman@27409
    56
done
huffman@27409
    57
huffman@39974
    58
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
huffman@39974
    59
unfolding below_fin_defl_def .
huffman@39974
    60
huffman@27409
    61
lemma Abs_fin_defl_mono:
huffman@27409
    62
  "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
huffman@27409
    63
    \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
huffman@31076
    64
unfolding below_fin_defl_def
huffman@27409
    65
by (simp add: Abs_fin_defl_inverse)
huffman@27409
    66
huffman@39974
    67
lemma (in finite_deflation) compact_belowI:
huffman@39974
    68
  assumes "\<And>x. compact x \<Longrightarrow> d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
huffman@39974
    69
by (rule belowI, rule assms, erule subst, rule compact)
huffman@27409
    70
huffman@39974
    71
lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)"
huffman@39974
    72
using finite_deflation_Rep_fin_defl
huffman@39974
    73
by (rule finite_deflation_imp_compact)
huffman@33586
    74
huffman@27409
    75
subsection {* Defining algebraic deflations by ideal completion *}
huffman@27409
    76
wenzelm@49834
    77
typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
huffman@40888
    78
by (rule below.ex_ideal)
huffman@27409
    79
huffman@41287
    80
instantiation defl :: (bifinite) below
huffman@27409
    81
begin
huffman@27409
    82
huffman@27409
    83
definition
huffman@39989
    84
  "x \<sqsubseteq> y \<longleftrightarrow> Rep_defl x \<subseteq> Rep_defl y"
huffman@27409
    85
huffman@27409
    86
instance ..
huffman@27409
    87
end
huffman@27409
    88
huffman@41287
    89
instance defl :: (bifinite) po
huffman@39989
    90
using type_definition_defl below_defl_def
huffman@39974
    91
by (rule below.typedef_ideal_po)
huffman@27409
    92
huffman@41287
    93
instance defl :: (bifinite) cpo
huffman@39989
    94
using type_definition_defl below_defl_def
huffman@39974
    95
by (rule below.typedef_ideal_cpo)
huffman@27409
    96
huffman@27409
    97
definition
huffman@41287
    98
  defl_principal :: "'a fin_defl \<Rightarrow> 'a defl" where
huffman@39989
    99
  "defl_principal t = Abs_defl {u. u \<sqsubseteq> t}"
huffman@27409
   100
huffman@41287
   101
lemma fin_defl_countable: "\<exists>f::'a fin_defl \<Rightarrow> nat. inj f"
huffman@41286
   102
proof -
huffman@41287
   103
  obtain f :: "'a compact_basis \<Rightarrow> nat" where inj_f: "inj f"
huffman@41286
   104
    using compact_basis.countable ..
huffman@41286
   105
  have *: "\<And>d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
huffman@39974
   106
    apply (rule finite_imageI)
huffman@39974
   107
    apply (rule finite_vimageI)
huffman@39974
   108
    apply (rule Rep_fin_defl.finite_fixes)
huffman@39974
   109
    apply (simp add: inj_on_def Rep_compact_basis_inject)
huffman@39974
   110
    done
huffman@39974
   111
  have range_eq: "range Rep_compact_basis = {x. compact x}"
huffman@39974
   112
    using type_definition_compact_basis by (rule type_definition.Rep_range)
huffman@41286
   113
  have "inj (\<lambda>d. set_encode
huffman@41286
   114
    (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
huffman@39974
   115
    apply (rule inj_onI)
huffman@39974
   116
    apply (simp only: set_encode_eq *)
huffman@41286
   117
    apply (simp only: inj_image_eq_iff inj_f)
huffman@39974
   118
    apply (drule_tac f="image Rep_compact_basis" in arg_cong)
huffman@39974
   119
    apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
huffman@39974
   120
    apply (rule Rep_fin_defl_inject [THEN iffD1])
huffman@39974
   121
    apply (rule below_antisym)
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
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   125
    apply (drule_tac x=z in spec, simp)
huffman@39974
   126
    done
huffman@41286
   127
  thus ?thesis by - (rule exI)
huffman@39974
   128
qed
huffman@39974
   129
huffman@39989
   130
interpretation defl: ideal_completion below defl_principal Rep_defl
huffman@39989
   131
using type_definition_defl below_defl_def
huffman@39989
   132
using defl_principal_def fin_defl_countable
huffman@39984
   133
by (rule below.typedef_ideal_completion)
huffman@27409
   134
huffman@27409
   135
text {* Algebraic deflations are pointed *}
huffman@27409
   136
huffman@39989
   137
lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
huffman@39989
   138
apply (induct x rule: defl.principal_induct, simp)
huffman@39989
   139
apply (rule defl.principal_mono)
huffman@39974
   140
apply (simp add: below_fin_defl_def)
huffman@41430
   141
apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom)
huffman@27409
   142
done
huffman@27409
   143
huffman@41287
   144
instance defl :: (bifinite) pcpo
huffman@39989
   145
by intro_classes (fast intro: defl_minimal)
huffman@27409
   146
huffman@39989
   147
lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
huffman@41430
   148
by (rule defl_minimal [THEN bottomI, symmetric])
huffman@27409
   149
huffman@27409
   150
subsection {* Applying algebraic deflations *}
huffman@27409
   151
huffman@27409
   152
definition
huffman@41287
   153
  cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
huffman@27409
   154
where
huffman@41394
   155
  "cast = defl.extension Rep_fin_defl"
huffman@27409
   156
huffman@39989
   157
lemma cast_defl_principal:
huffman@39989
   158
  "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
huffman@27409
   159
unfolding cast_def
huffman@41394
   160
apply (rule defl.extension_principal)
huffman@31076
   161
apply (simp only: below_fin_defl_def)
huffman@27409
   162
done
huffman@27409
   163
huffman@27409
   164
lemma deflation_cast: "deflation (cast\<cdot>d)"
huffman@39989
   165
apply (induct d rule: defl.principal_induct)
huffman@27409
   166
apply (rule adm_subst [OF _ adm_deflation], simp)
huffman@39989
   167
apply (simp add: cast_defl_principal)
huffman@27409
   168
apply (rule finite_deflation_imp_deflation)
huffman@27409
   169
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   170
done
huffman@27409
   171
huffman@27409
   172
lemma finite_deflation_cast:
huffman@27409
   173
  "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
huffman@39989
   174
apply (drule defl.compact_imp_principal, clarify)
huffman@39989
   175
apply (simp add: cast_defl_principal)
huffman@27409
   176
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   177
done
huffman@27409
   178
wenzelm@30729
   179
interpretation cast: deflation "cast\<cdot>d"
huffman@27409
   180
by (rule deflation_cast)
huffman@27409
   181
huffman@33586
   182
declare cast.idem [simp]
huffman@33586
   183
huffman@39974
   184
lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
huffman@39974
   185
apply (rule finite_deflation_imp_compact)
huffman@39974
   186
apply (erule finite_deflation_cast)
huffman@31164
   187
done
huffman@31164
   188
huffman@39974
   189
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
huffman@39989
   190
apply (induct A rule: defl.principal_induct, simp)
huffman@39989
   191
apply (induct B rule: defl.principal_induct, simp)
huffman@39989
   192
apply (simp add: cast_defl_principal below_fin_defl_def)
huffman@31164
   193
done
huffman@31164
   194
huffman@39974
   195
lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
huffman@39974
   196
apply (rule iffI)
huffman@39974
   197
apply (simp only: compact_def cast_below_cast [symmetric])
huffman@40327
   198
apply (erule adm_subst [OF cont_Rep_cfun2])
huffman@39974
   199
apply (erule compact_cast)
brianh@39972
   200
done
brianh@39972
   201
huffman@31164
   202
lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
huffman@39974
   203
by (simp only: cast_below_cast)
huffman@31164
   204
huffman@33586
   205
lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
huffman@33586
   206
by (simp add: below_antisym cast_below_imp_below)
huffman@33586
   207
huffman@33586
   208
lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
huffman@39989
   209
apply (subst inst_defl_pcpo)
huffman@39989
   210
apply (subst cast_defl_principal)
huffman@33586
   211
apply (rule Abs_fin_defl_inverse)
huffman@41430
   212
apply (simp add: finite_deflation_bottom)
huffman@33586
   213
done
huffman@33586
   214
huffman@33586
   215
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
huffman@41430
   216
by (rule cast.below [THEN bottomI])
huffman@33586
   217
huffman@41290
   218
subsection {* Deflation combinators *}
huffman@41290
   219
huffman@41290
   220
definition
huffman@41290
   221
  "defl_fun1 e p f =
huffman@41394
   222
    defl.extension (\<lambda>a.
huffman@41290
   223
      defl_principal (Abs_fin_defl
huffman@41290
   224
        (e oo f\<cdot>(Rep_fin_defl a) oo p)))"
huffman@41290
   225
huffman@41290
   226
definition
huffman@41290
   227
  "defl_fun2 e p f =
huffman@41394
   228
    defl.extension (\<lambda>a.
huffman@41394
   229
      defl.extension (\<lambda>b.
huffman@41290
   230
        defl_principal (Abs_fin_defl
huffman@41290
   231
          (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"
huffman@41290
   232
huffman@41290
   233
lemma cast_defl_fun1:
huffman@41290
   234
  assumes ep: "ep_pair e p"
huffman@41290
   235
  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
huffman@41290
   236
  shows "cast\<cdot>(defl_fun1 e p f\<cdot>A) = e oo f\<cdot>(cast\<cdot>A) oo p"
huffman@41290
   237
proof -
huffman@41290
   238
  have 1: "\<And>a. finite_deflation (e oo f\<cdot>(Rep_fin_defl a) oo p)"
huffman@41290
   239
    apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
huffman@41290
   240
    apply (rule f, rule finite_deflation_Rep_fin_defl)
huffman@41290
   241
    done
huffman@41290
   242
  show ?thesis
huffman@41290
   243
    by (induct A rule: defl.principal_induct, simp)
huffman@41290
   244
       (simp only: defl_fun1_def
huffman@41394
   245
                   defl.extension_principal
huffman@41394
   246
                   defl.extension_mono
huffman@41290
   247
                   defl.principal_mono
huffman@41290
   248
                   Abs_fin_defl_mono [OF 1 1]
huffman@41290
   249
                   monofun_cfun below_refl
huffman@41290
   250
                   Rep_fin_defl_mono
huffman@41290
   251
                   cast_defl_principal
huffman@41290
   252
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@41290
   253
qed
huffman@41290
   254
huffman@41290
   255
lemma cast_defl_fun2:
huffman@41290
   256
  assumes ep: "ep_pair e p"
huffman@41290
   257
  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
huffman@41290
   258
                finite_deflation (f\<cdot>a\<cdot>b)"
huffman@41290
   259
  shows "cast\<cdot>(defl_fun2 e p f\<cdot>A\<cdot>B) = e oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo p"
huffman@41290
   260
proof -
huffman@41290
   261
  have 1: "\<And>a b. finite_deflation
huffman@41290
   262
      (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p)"
huffman@41290
   263
    apply (rule ep_pair.finite_deflation_e_d_p [OF ep])
huffman@41290
   264
    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
huffman@41290
   265
    done
huffman@41290
   266
  show ?thesis
huffman@41290
   267
    apply (induct A rule: defl.principal_induct, simp)
huffman@41290
   268
    apply (induct B rule: defl.principal_induct, simp)
huffman@41290
   269
    by (simp only: defl_fun2_def
huffman@41394
   270
                   defl.extension_principal
huffman@41394
   271
                   defl.extension_mono
huffman@41290
   272
                   defl.principal_mono
huffman@41290
   273
                   Abs_fin_defl_mono [OF 1 1]
huffman@41290
   274
                   monofun_cfun below_refl
huffman@41290
   275
                   Rep_fin_defl_mono
huffman@41290
   276
                   cast_defl_principal
huffman@41290
   277
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@41290
   278
qed
huffman@41290
   279
huffman@27409
   280
end