src/HOLCF/Pcpodef.thy
author huffman
Wed Oct 27 13:54:18 2010 -0700 (2010-10-27)
changeset 40321 d065b195ec89
parent 40089 8adc57fb8454
child 40325 24971566ff4f
permissions -rw-r--r--
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman@16697
     1
(*  Title:      HOLCF/Pcpodef.thy
huffman@16697
     2
    Author:     Brian Huffman
huffman@16697
     3
*)
huffman@16697
     4
huffman@16697
     5
header {* Subtypes of pcpos *}
huffman@16697
     6
huffman@16697
     7
theory Pcpodef
huffman@16697
     8
imports Adm
haftmann@31738
     9
uses ("Tools/pcpodef.ML")
huffman@16697
    10
begin
huffman@16697
    11
huffman@16697
    12
subsection {* Proving a subtype is a partial order *}
huffman@16697
    13
huffman@16697
    14
text {*
huffman@16697
    15
  A subtype of a partial order is itself a partial order,
huffman@16697
    16
  if the ordering is defined in the standard way.
huffman@16697
    17
*}
huffman@16697
    18
huffman@31076
    19
setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
haftmann@28073
    20
huffman@16697
    21
theorem typedef_po:
haftmann@28073
    22
  fixes Abs :: "'a::po \<Rightarrow> 'b::type"
huffman@16697
    23
  assumes type: "type_definition Rep Abs A"
huffman@31076
    24
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    25
  shows "OFCLASS('b, po_class)"
huffman@31076
    26
 apply (intro_classes, unfold below)
huffman@31076
    27
   apply (rule below_refl)
huffman@31076
    28
  apply (erule (1) below_trans)
huffman@26420
    29
 apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
huffman@31076
    30
 apply (erule (1) below_antisym)
huffman@16697
    31
done
huffman@16697
    32
huffman@31076
    33
setup {* Sign.add_const_constraint (@{const_name Porder.below},
huffman@31076
    34
  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
haftmann@28073
    35
huffman@25827
    36
subsection {* Proving a subtype is finite *}
huffman@25827
    37
huffman@27296
    38
lemma typedef_finite_UNIV:
huffman@27296
    39
  fixes Abs :: "'a::type \<Rightarrow> 'b::type"
huffman@27296
    40
  assumes type: "type_definition Rep Abs A"
huffman@27296
    41
  shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
huffman@25827
    42
proof -
huffman@25827
    43
  assume "finite A"
huffman@25827
    44
  hence "finite (Abs ` A)" by (rule finite_imageI)
huffman@27296
    45
  thus "finite (UNIV :: 'b set)"
huffman@27296
    46
    by (simp only: type_definition.Abs_image [OF type])
huffman@25827
    47
qed
huffman@25827
    48
huffman@17812
    49
subsection {* Proving a subtype is chain-finite *}
huffman@17812
    50
huffman@40035
    51
lemma ch2ch_Rep:
huffman@31076
    52
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@40035
    53
  shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
huffman@40035
    54
unfolding chain_def below .
huffman@17812
    55
huffman@17812
    56
theorem typedef_chfin:
huffman@17812
    57
  fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
huffman@17812
    58
  assumes type: "type_definition Rep Abs A"
huffman@31076
    59
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@17812
    60
  shows "OFCLASS('b, chfin_class)"
huffman@25921
    61
 apply intro_classes
huffman@31076
    62
 apply (drule ch2ch_Rep [OF below])
huffman@25921
    63
 apply (drule chfin)
huffman@17812
    64
 apply (unfold max_in_chain_def)
huffman@17812
    65
 apply (simp add: type_definition.Rep_inject [OF type])
huffman@17812
    66
done
huffman@17812
    67
huffman@16697
    68
subsection {* Proving a subtype is complete *}
huffman@16697
    69
huffman@16697
    70
text {*
huffman@16697
    71
  A subtype of a cpo is itself a cpo if the ordering is
huffman@16697
    72
  defined in the standard way, and the defining subset
huffman@16697
    73
  is closed with respect to limits of chains.  A set is
huffman@16697
    74
  closed if and only if membership in the set is an
huffman@16697
    75
  admissible predicate.
huffman@16697
    76
*}
huffman@16697
    77
huffman@40035
    78
lemma typedef_is_lubI:
huffman@40035
    79
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@40035
    80
  shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
huffman@40035
    81
unfolding is_lub_def is_ub_def below by simp
huffman@40035
    82
huffman@16918
    83
lemma Abs_inverse_lub_Rep:
huffman@16697
    84
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
    85
  assumes type: "type_definition Rep Abs A"
huffman@31076
    86
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    87
    and adm:  "adm (\<lambda>x. x \<in> A)"
huffman@16918
    88
  shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
huffman@16918
    89
 apply (rule type_definition.Abs_inverse [OF type])
huffman@31076
    90
 apply (erule admD [OF adm ch2ch_Rep [OF below]])
huffman@16697
    91
 apply (rule type_definition.Rep [OF type])
huffman@16697
    92
done
huffman@16697
    93
huffman@16918
    94
theorem typedef_lub:
huffman@16697
    95
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
    96
  assumes type: "type_definition Rep Abs A"
huffman@31076
    97
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    98
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16918
    99
  shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@40035
   100
proof -
huffman@40035
   101
  assume S: "chain S"
huffman@40035
   102
  hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
huffman@40035
   103
  hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
huffman@40035
   104
  hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
huffman@40035
   105
    by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
huffman@40035
   106
  thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@40035
   107
    by (rule typedef_is_lubI [OF below])
huffman@40035
   108
qed
huffman@16697
   109
huffman@16918
   110
lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
huffman@16918
   111
huffman@16697
   112
theorem typedef_cpo:
huffman@16697
   113
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
   114
  assumes type: "type_definition Rep Abs A"
huffman@31076
   115
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   116
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16697
   117
  shows "OFCLASS('b, cpo_class)"
huffman@16918
   118
proof
huffman@16918
   119
  fix S::"nat \<Rightarrow> 'b" assume "chain S"
huffman@16918
   120
  hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@31076
   121
    by (rule typedef_lub [OF type below adm])
huffman@16918
   122
  thus "\<exists>x. range S <<| x" ..
huffman@16918
   123
qed
huffman@16697
   124
huffman@35900
   125
subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
huffman@16697
   126
huffman@16697
   127
text {* For any sub-cpo, the @{term Rep} function is continuous. *}
huffman@16697
   128
huffman@16697
   129
theorem typedef_cont_Rep:
huffman@16697
   130
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   131
  assumes type: "type_definition Rep Abs A"
huffman@31076
   132
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   133
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16697
   134
  shows "cont Rep"
huffman@16697
   135
 apply (rule contI)
huffman@31076
   136
 apply (simp only: typedef_thelub [OF type below adm])
huffman@31076
   137
 apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
huffman@26027
   138
 apply (rule cpo_lubI)
huffman@31076
   139
 apply (erule ch2ch_Rep [OF below])
huffman@16697
   140
done
huffman@16697
   141
huffman@16697
   142
text {*
huffman@16697
   143
  For a sub-cpo, we can make the @{term Abs} function continuous
huffman@16697
   144
  only if we restrict its domain to the defining subset by
huffman@16697
   145
  composing it with another continuous function.
huffman@16697
   146
*}
huffman@16697
   147
huffman@16697
   148
theorem typedef_cont_Abs:
huffman@16697
   149
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   150
  fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
huffman@16697
   151
  assumes type: "type_definition Rep Abs A"
huffman@31076
   152
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16918
   153
    and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
huffman@16697
   154
    and f_in_A: "\<And>x. f x \<in> A"
huffman@16697
   155
    and cont_f: "cont f"
huffman@16697
   156
  shows "cont (\<lambda>x. Abs (f x))"
huffman@16697
   157
 apply (rule contI)
huffman@31076
   158
 apply (rule typedef_is_lubI [OF below])
huffman@16918
   159
 apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
huffman@16918
   160
 apply (erule cont_f [THEN contE])
huffman@16697
   161
done
huffman@16697
   162
huffman@17833
   163
subsection {* Proving subtype elements are compact *}
huffman@17833
   164
huffman@17833
   165
theorem typedef_compact:
huffman@17833
   166
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@17833
   167
  assumes type: "type_definition Rep Abs A"
huffman@31076
   168
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@17833
   169
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@17833
   170
  shows "compact (Rep k) \<Longrightarrow> compact k"
huffman@17833
   171
proof (unfold compact_def)
huffman@17833
   172
  have cont_Rep: "cont Rep"
huffman@31076
   173
    by (rule typedef_cont_Rep [OF type below adm])
huffman@17833
   174
  assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
huffman@17833
   175
  with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
huffman@31076
   176
  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
huffman@17833
   177
qed
huffman@17833
   178
huffman@16697
   179
subsection {* Proving a subtype is pointed *}
huffman@16697
   180
huffman@16697
   181
text {*
huffman@16697
   182
  A subtype of a cpo has a least element if and only if
huffman@16697
   183
  the defining subset has a least element.
huffman@16697
   184
*}
huffman@16697
   185
huffman@16918
   186
theorem typedef_pcpo_generic:
huffman@16697
   187
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   188
  assumes type: "type_definition Rep Abs A"
huffman@31076
   189
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   190
    and z_in_A: "z \<in> A"
huffman@16697
   191
    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
huffman@16697
   192
  shows "OFCLASS('b, pcpo_class)"
huffman@16697
   193
 apply (intro_classes)
huffman@16697
   194
 apply (rule_tac x="Abs z" in exI, rule allI)
huffman@31076
   195
 apply (unfold below)
huffman@16697
   196
 apply (subst type_definition.Abs_inverse [OF type z_in_A])
huffman@16697
   197
 apply (rule z_least [OF type_definition.Rep [OF type]])
huffman@16697
   198
done
huffman@16697
   199
huffman@16697
   200
text {*
huffman@16697
   201
  As a special case, a subtype of a pcpo has a least element
huffman@16697
   202
  if the defining subset contains @{term \<bottom>}.
huffman@16697
   203
*}
huffman@16697
   204
huffman@16918
   205
theorem typedef_pcpo:
huffman@16697
   206
  fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
huffman@16697
   207
  assumes type: "type_definition Rep Abs A"
huffman@31076
   208
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   209
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   210
  shows "OFCLASS('b, pcpo_class)"
huffman@31076
   211
by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
huffman@16697
   212
huffman@35900
   213
subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
huffman@16697
   214
huffman@16697
   215
text {*
huffman@16697
   216
  For a sub-pcpo where @{term \<bottom>} is a member of the defining
huffman@16697
   217
  subset, @{term Rep} and @{term Abs} are both strict.
huffman@16697
   218
*}
huffman@16697
   219
huffman@16697
   220
theorem typedef_Abs_strict:
huffman@16697
   221
  assumes type: "type_definition Rep Abs A"
huffman@31076
   222
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   223
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   224
  shows "Abs \<bottom> = \<bottom>"
huffman@31076
   225
 apply (rule UU_I, unfold below)
huffman@16697
   226
 apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
huffman@16697
   227
done
huffman@16697
   228
huffman@16697
   229
theorem typedef_Rep_strict:
huffman@16697
   230
  assumes type: "type_definition Rep Abs A"
huffman@31076
   231
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   232
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   233
  shows "Rep \<bottom> = \<bottom>"
huffman@31076
   234
 apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
huffman@16697
   235
 apply (rule type_definition.Abs_inverse [OF type UU_in_A])
huffman@16697
   236
done
huffman@16697
   237
huffman@40321
   238
theorem typedef_Abs_bottom_iff:
huffman@25926
   239
  assumes type: "type_definition Rep Abs A"
huffman@31076
   240
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@25926
   241
    and UU_in_A: "\<bottom> \<in> A"
huffman@25926
   242
  shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
huffman@31076
   243
 apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
huffman@25926
   244
 apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
huffman@25926
   245
done
huffman@25926
   246
huffman@40321
   247
theorem typedef_Rep_bottom_iff:
huffman@25926
   248
  assumes type: "type_definition Rep Abs A"
huffman@31076
   249
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@25926
   250
    and UU_in_A: "\<bottom> \<in> A"
huffman@25926
   251
  shows "(Rep x = \<bottom>) = (x = \<bottom>)"
huffman@31076
   252
 apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
huffman@25926
   253
 apply (simp add: type_definition.Rep_inject [OF type])
huffman@25926
   254
done
huffman@25926
   255
huffman@16697
   256
theorem typedef_Abs_defined:
huffman@16697
   257
  assumes type: "type_definition Rep Abs A"
huffman@31076
   258
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   259
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   260
  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
huffman@40321
   261
by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
huffman@16697
   262
huffman@16697
   263
theorem typedef_Rep_defined:
huffman@16697
   264
  assumes type: "type_definition Rep Abs A"
huffman@31076
   265
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   266
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   267
  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
huffman@40321
   268
by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
huffman@16697
   269
huffman@19519
   270
subsection {* Proving a subtype is flat *}
huffman@19519
   271
huffman@19519
   272
theorem typedef_flat:
huffman@19519
   273
  fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
huffman@19519
   274
  assumes type: "type_definition Rep Abs A"
huffman@31076
   275
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@19519
   276
    and UU_in_A: "\<bottom> \<in> A"
huffman@19519
   277
  shows "OFCLASS('b, flat_class)"
huffman@19519
   278
 apply (intro_classes)
huffman@31076
   279
 apply (unfold below)
huffman@19519
   280
 apply (simp add: type_definition.Rep_inject [OF type, symmetric])
huffman@31076
   281
 apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
huffman@19519
   282
 apply (simp add: ax_flat)
huffman@19519
   283
done
huffman@19519
   284
huffman@16697
   285
subsection {* HOLCF type definition package *}
huffman@16697
   286
haftmann@31738
   287
use "Tools/pcpodef.ML"
huffman@16697
   288
huffman@16697
   289
end