src/HOLCF/Algebraic.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 39989 ad60d7311f43
child 40038 9d061b3d8f46
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
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@39989
    75
typedef (open) defl = "{S::fin_defl set. below.ideal S}"
huffman@31076
    76
by (fast intro: below.ideal_principal)
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@39974
   100
proof
huffman@39974
   101
  have *: "\<And>d. finite (approx_chain.place udom_approx `
huffman@39974
   102
               Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x})"
huffman@39974
   103
    apply (rule finite_imageI)
huffman@39974
   104
    apply (rule finite_vimageI)
huffman@39974
   105
    apply (rule Rep_fin_defl.finite_fixes)
huffman@39974
   106
    apply (simp add: inj_on_def Rep_compact_basis_inject)
huffman@39974
   107
    done
huffman@39974
   108
  have range_eq: "range Rep_compact_basis = {x. compact x}"
huffman@39974
   109
    using type_definition_compact_basis by (rule type_definition.Rep_range)
huffman@39974
   110
  show "inj (\<lambda>d. set_encode
huffman@39974
   111
    (approx_chain.place udom_approx ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
huffman@39974
   112
    apply (rule inj_onI)
huffman@39974
   113
    apply (simp only: set_encode_eq *)
huffman@39974
   114
    apply (simp only: inj_image_eq_iff approx_chain.inj_place [OF udom_approx])
huffman@39974
   115
    apply (drule_tac f="image Rep_compact_basis" in arg_cong)
huffman@39974
   116
    apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
huffman@39974
   117
    apply (rule Rep_fin_defl_inject [THEN iffD1])
huffman@39974
   118
    apply (rule below_antisym)
huffman@39974
   119
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   120
    apply (drule_tac x=z in spec, simp)
huffman@39974
   121
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
huffman@39974
   122
    apply (drule_tac x=z in spec, simp)
huffman@39974
   123
    done
huffman@39974
   124
qed
huffman@39974
   125
huffman@39989
   126
interpretation defl: ideal_completion below defl_principal Rep_defl
huffman@39989
   127
using type_definition_defl below_defl_def
huffman@39989
   128
using defl_principal_def fin_defl_countable
huffman@39984
   129
by (rule below.typedef_ideal_completion)
huffman@27409
   130
huffman@27409
   131
text {* Algebraic deflations are pointed *}
huffman@27409
   132
huffman@39989
   133
lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
huffman@39989
   134
apply (induct x rule: defl.principal_induct, simp)
huffman@39989
   135
apply (rule defl.principal_mono)
huffman@39974
   136
apply (simp add: below_fin_defl_def)
huffman@39974
   137
apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
huffman@27409
   138
done
huffman@27409
   139
huffman@39989
   140
instance defl :: pcpo
huffman@39989
   141
by intro_classes (fast intro: defl_minimal)
huffman@27409
   142
huffman@39989
   143
lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
huffman@39989
   144
by (rule defl_minimal [THEN UU_I, symmetric])
huffman@27409
   145
huffman@27409
   146
subsection {* Applying algebraic deflations *}
huffman@27409
   147
huffman@27409
   148
definition
huffman@39989
   149
  cast :: "defl \<rightarrow> udom \<rightarrow> udom"
huffman@27409
   150
where
huffman@39989
   151
  "cast = defl.basis_fun Rep_fin_defl"
huffman@27409
   152
huffman@39989
   153
lemma cast_defl_principal:
huffman@39989
   154
  "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
huffman@27409
   155
unfolding cast_def
huffman@39989
   156
apply (rule defl.basis_fun_principal)
huffman@31076
   157
apply (simp only: below_fin_defl_def)
huffman@27409
   158
done
huffman@27409
   159
huffman@27409
   160
lemma deflation_cast: "deflation (cast\<cdot>d)"
huffman@39989
   161
apply (induct d rule: defl.principal_induct)
huffman@27409
   162
apply (rule adm_subst [OF _ adm_deflation], simp)
huffman@39989
   163
apply (simp add: cast_defl_principal)
huffman@27409
   164
apply (rule finite_deflation_imp_deflation)
huffman@27409
   165
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   166
done
huffman@27409
   167
huffman@27409
   168
lemma finite_deflation_cast:
huffman@27409
   169
  "compact d \<Longrightarrow> finite_deflation (cast\<cdot>d)"
huffman@39989
   170
apply (drule defl.compact_imp_principal, clarify)
huffman@39989
   171
apply (simp add: cast_defl_principal)
huffman@27409
   172
apply (rule finite_deflation_Rep_fin_defl)
huffman@27409
   173
done
huffman@27409
   174
wenzelm@30729
   175
interpretation cast: deflation "cast\<cdot>d"
huffman@27409
   176
by (rule deflation_cast)
huffman@27409
   177
huffman@33586
   178
declare cast.idem [simp]
huffman@33586
   179
huffman@39974
   180
lemma compact_cast [simp]: "compact d \<Longrightarrow> compact (cast\<cdot>d)"
huffman@39974
   181
apply (rule finite_deflation_imp_compact)
huffman@39974
   182
apply (erule finite_deflation_cast)
huffman@31164
   183
done
huffman@31164
   184
huffman@39974
   185
lemma cast_below_cast: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
huffman@39989
   186
apply (induct A rule: defl.principal_induct, simp)
huffman@39989
   187
apply (induct B rule: defl.principal_induct, simp)
huffman@39989
   188
apply (simp add: cast_defl_principal below_fin_defl_def)
huffman@31164
   189
done
huffman@31164
   190
huffman@39974
   191
lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
huffman@39974
   192
apply (rule iffI)
huffman@39974
   193
apply (simp only: compact_def cast_below_cast [symmetric])
huffman@39974
   194
apply (erule adm_subst [OF cont_Rep_CFun2])
huffman@39974
   195
apply (erule compact_cast)
brianh@39972
   196
done
brianh@39972
   197
huffman@31164
   198
lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
huffman@39974
   199
by (simp only: cast_below_cast)
huffman@31164
   200
huffman@33586
   201
lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
huffman@33586
   202
by (simp add: below_antisym cast_below_imp_below)
huffman@33586
   203
huffman@33586
   204
lemma cast_strict1 [simp]: "cast\<cdot>\<bottom> = \<bottom>"
huffman@39989
   205
apply (subst inst_defl_pcpo)
huffman@39989
   206
apply (subst cast_defl_principal)
huffman@33586
   207
apply (rule Abs_fin_defl_inverse)
huffman@33586
   208
apply (simp add: finite_deflation_UU)
huffman@33586
   209
done
huffman@33586
   210
huffman@33586
   211
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
huffman@33586
   212
by (rule cast.below [THEN UU_I])
huffman@33586
   213
huffman@33586
   214
subsection {* Deflation membership relation *}
huffman@33586
   215
huffman@33586
   216
definition
huffman@39989
   217
  in_defl :: "udom \<Rightarrow> defl \<Rightarrow> bool" (infixl ":::" 50)
huffman@33586
   218
where
huffman@33586
   219
  "x ::: A \<longleftrightarrow> cast\<cdot>A\<cdot>x = x"
huffman@33586
   220
huffman@39989
   221
lemma adm_in_defl: "adm (\<lambda>x. x ::: A)"
huffman@39989
   222
unfolding in_defl_def by simp
huffman@33586
   223
huffman@39989
   224
lemma in_deflI: "cast\<cdot>A\<cdot>x = x \<Longrightarrow> x ::: A"
huffman@39989
   225
unfolding in_defl_def .
huffman@33586
   226
huffman@33586
   227
lemma cast_fixed: "x ::: A \<Longrightarrow> cast\<cdot>A\<cdot>x = x"
huffman@39989
   228
unfolding in_defl_def .
huffman@33586
   229
huffman@39989
   230
lemma cast_in_defl [simp]: "cast\<cdot>A\<cdot>x ::: A"
huffman@39989
   231
unfolding in_defl_def by (rule cast.idem)
huffman@33586
   232
huffman@39989
   233
lemma bottom_in_defl [simp]: "\<bottom> ::: A"
huffman@39989
   234
unfolding in_defl_def by (rule cast_strict2)
huffman@33586
   235
huffman@39989
   236
lemma defl_belowD: "A \<sqsubseteq> B \<Longrightarrow> x ::: A \<Longrightarrow> x ::: B"
huffman@39989
   237
unfolding in_defl_def
huffman@33586
   238
 apply (rule deflation.belowD)
huffman@33586
   239
   apply (rule deflation_cast)
huffman@33586
   240
  apply (erule monofun_cfun_arg)
huffman@33586
   241
 apply assumption
huffman@33586
   242
done
huffman@33586
   243
huffman@39989
   244
lemma rev_defl_belowD: "x ::: A \<Longrightarrow> A \<sqsubseteq> B \<Longrightarrow> x ::: B"
huffman@39989
   245
by (rule defl_belowD)
huffman@33586
   246
huffman@39989
   247
lemma defl_belowI: "(\<And>x. x ::: A \<Longrightarrow> x ::: B) \<Longrightarrow> A \<sqsubseteq> B"
huffman@33586
   248
apply (rule cast_below_imp_below)
huffman@33586
   249
apply (rule cast.belowI)
huffman@39989
   250
apply (simp add: in_defl_def)
huffman@27409
   251
done
huffman@27409
   252
huffman@27409
   253
end