src/HOLCF/Pcpodef.thy
author huffman
Sun Oct 17 09:53:47 2010 -0700 (2010-10-17)
changeset 40035 a12d35795cb9
parent 35900 aa5dfb03eb1e
child 40089 8adc57fb8454
permissions -rw-r--r--
simplify some proofs
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@25827
    49
theorem typedef_finite_po:
huffman@25827
    50
  fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po"
huffman@25827
    51
  assumes type: "type_definition Rep Abs A"
huffman@25827
    52
  shows "OFCLASS('b, finite_po_class)"
huffman@25827
    53
 apply (intro_classes)
huffman@27296
    54
 apply (rule typedef_finite_UNIV [OF type])
huffman@25827
    55
 apply (rule finite)
huffman@25827
    56
done
huffman@25827
    57
huffman@17812
    58
subsection {* Proving a subtype is chain-finite *}
huffman@17812
    59
huffman@40035
    60
lemma ch2ch_Rep:
huffman@31076
    61
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@40035
    62
  shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
huffman@40035
    63
unfolding chain_def below .
huffman@17812
    64
huffman@17812
    65
theorem typedef_chfin:
huffman@17812
    66
  fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
huffman@17812
    67
  assumes type: "type_definition Rep Abs A"
huffman@31076
    68
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@17812
    69
  shows "OFCLASS('b, chfin_class)"
huffman@25921
    70
 apply intro_classes
huffman@31076
    71
 apply (drule ch2ch_Rep [OF below])
huffman@25921
    72
 apply (drule chfin)
huffman@17812
    73
 apply (unfold max_in_chain_def)
huffman@17812
    74
 apply (simp add: type_definition.Rep_inject [OF type])
huffman@17812
    75
done
huffman@17812
    76
huffman@16697
    77
subsection {* Proving a subtype is complete *}
huffman@16697
    78
huffman@16697
    79
text {*
huffman@16697
    80
  A subtype of a cpo is itself a cpo if the ordering is
huffman@16697
    81
  defined in the standard way, and the defining subset
huffman@16697
    82
  is closed with respect to limits of chains.  A set is
huffman@16697
    83
  closed if and only if membership in the set is an
huffman@16697
    84
  admissible predicate.
huffman@16697
    85
*}
huffman@16697
    86
huffman@40035
    87
lemma typedef_is_lubI:
huffman@40035
    88
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@40035
    89
  shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
huffman@40035
    90
unfolding is_lub_def is_ub_def below by simp
huffman@40035
    91
huffman@16918
    92
lemma Abs_inverse_lub_Rep:
huffman@16697
    93
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
    94
  assumes type: "type_definition Rep Abs A"
huffman@31076
    95
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    96
    and adm:  "adm (\<lambda>x. x \<in> A)"
huffman@16918
    97
  shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
huffman@16918
    98
 apply (rule type_definition.Abs_inverse [OF type])
huffman@31076
    99
 apply (erule admD [OF adm ch2ch_Rep [OF below]])
huffman@16697
   100
 apply (rule type_definition.Rep [OF type])
huffman@16697
   101
done
huffman@16697
   102
huffman@16918
   103
theorem typedef_lub:
huffman@16697
   104
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
   105
  assumes type: "type_definition Rep Abs A"
huffman@31076
   106
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   107
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16918
   108
  shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@40035
   109
proof -
huffman@40035
   110
  assume S: "chain S"
huffman@40035
   111
  hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
huffman@40035
   112
  hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
huffman@40035
   113
  hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
huffman@40035
   114
    by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
huffman@40035
   115
  thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@40035
   116
    by (rule typedef_is_lubI [OF below])
huffman@40035
   117
qed
huffman@16697
   118
huffman@16918
   119
lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
huffman@16918
   120
huffman@16697
   121
theorem typedef_cpo:
huffman@16697
   122
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
   123
  assumes type: "type_definition Rep Abs A"
huffman@31076
   124
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   125
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16697
   126
  shows "OFCLASS('b, cpo_class)"
huffman@16918
   127
proof
huffman@16918
   128
  fix S::"nat \<Rightarrow> 'b" assume "chain S"
huffman@16918
   129
  hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@31076
   130
    by (rule typedef_lub [OF type below adm])
huffman@16918
   131
  thus "\<exists>x. range S <<| x" ..
huffman@16918
   132
qed
huffman@16697
   133
huffman@35900
   134
subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
huffman@16697
   135
huffman@16697
   136
text {* For any sub-cpo, the @{term Rep} function is continuous. *}
huffman@16697
   137
huffman@16697
   138
theorem typedef_cont_Rep:
huffman@16697
   139
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   140
  assumes type: "type_definition Rep Abs A"
huffman@31076
   141
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   142
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16697
   143
  shows "cont Rep"
huffman@16697
   144
 apply (rule contI)
huffman@31076
   145
 apply (simp only: typedef_thelub [OF type below adm])
huffman@31076
   146
 apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
huffman@26027
   147
 apply (rule cpo_lubI)
huffman@31076
   148
 apply (erule ch2ch_Rep [OF below])
huffman@16697
   149
done
huffman@16697
   150
huffman@16697
   151
text {*
huffman@16697
   152
  For a sub-cpo, we can make the @{term Abs} function continuous
huffman@16697
   153
  only if we restrict its domain to the defining subset by
huffman@16697
   154
  composing it with another continuous function.
huffman@16697
   155
*}
huffman@16697
   156
huffman@16697
   157
theorem typedef_cont_Abs:
huffman@16697
   158
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   159
  fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
huffman@16697
   160
  assumes type: "type_definition Rep Abs A"
huffman@31076
   161
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16918
   162
    and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
huffman@16697
   163
    and f_in_A: "\<And>x. f x \<in> A"
huffman@16697
   164
    and cont_f: "cont f"
huffman@16697
   165
  shows "cont (\<lambda>x. Abs (f x))"
huffman@16697
   166
 apply (rule contI)
huffman@31076
   167
 apply (rule typedef_is_lubI [OF below])
huffman@16918
   168
 apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
huffman@16918
   169
 apply (erule cont_f [THEN contE])
huffman@16697
   170
done
huffman@16697
   171
huffman@17833
   172
subsection {* Proving subtype elements are compact *}
huffman@17833
   173
huffman@17833
   174
theorem typedef_compact:
huffman@17833
   175
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@17833
   176
  assumes type: "type_definition Rep Abs A"
huffman@31076
   177
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@17833
   178
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@17833
   179
  shows "compact (Rep k) \<Longrightarrow> compact k"
huffman@17833
   180
proof (unfold compact_def)
huffman@17833
   181
  have cont_Rep: "cont Rep"
huffman@31076
   182
    by (rule typedef_cont_Rep [OF type below adm])
huffman@17833
   183
  assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
huffman@17833
   184
  with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
huffman@31076
   185
  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
huffman@17833
   186
qed
huffman@17833
   187
huffman@16697
   188
subsection {* Proving a subtype is pointed *}
huffman@16697
   189
huffman@16697
   190
text {*
huffman@16697
   191
  A subtype of a cpo has a least element if and only if
huffman@16697
   192
  the defining subset has a least element.
huffman@16697
   193
*}
huffman@16697
   194
huffman@16918
   195
theorem typedef_pcpo_generic:
huffman@16697
   196
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   197
  assumes type: "type_definition Rep Abs A"
huffman@31076
   198
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   199
    and z_in_A: "z \<in> A"
huffman@16697
   200
    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
huffman@16697
   201
  shows "OFCLASS('b, pcpo_class)"
huffman@16697
   202
 apply (intro_classes)
huffman@16697
   203
 apply (rule_tac x="Abs z" in exI, rule allI)
huffman@31076
   204
 apply (unfold below)
huffman@16697
   205
 apply (subst type_definition.Abs_inverse [OF type z_in_A])
huffman@16697
   206
 apply (rule z_least [OF type_definition.Rep [OF type]])
huffman@16697
   207
done
huffman@16697
   208
huffman@16697
   209
text {*
huffman@16697
   210
  As a special case, a subtype of a pcpo has a least element
huffman@16697
   211
  if the defining subset contains @{term \<bottom>}.
huffman@16697
   212
*}
huffman@16697
   213
huffman@16918
   214
theorem typedef_pcpo:
huffman@16697
   215
  fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
huffman@16697
   216
  assumes type: "type_definition Rep Abs A"
huffman@31076
   217
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   218
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   219
  shows "OFCLASS('b, pcpo_class)"
huffman@31076
   220
by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
huffman@16697
   221
huffman@35900
   222
subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
huffman@16697
   223
huffman@16697
   224
text {*
huffman@16697
   225
  For a sub-pcpo where @{term \<bottom>} is a member of the defining
huffman@16697
   226
  subset, @{term Rep} and @{term Abs} are both strict.
huffman@16697
   227
*}
huffman@16697
   228
huffman@16697
   229
theorem typedef_Abs_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 "Abs \<bottom> = \<bottom>"
huffman@31076
   234
 apply (rule UU_I, unfold below)
huffman@16697
   235
 apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
huffman@16697
   236
done
huffman@16697
   237
huffman@16697
   238
theorem typedef_Rep_strict:
huffman@16697
   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@16697
   241
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   242
  shows "Rep \<bottom> = \<bottom>"
huffman@31076
   243
 apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
huffman@16697
   244
 apply (rule type_definition.Abs_inverse [OF type UU_in_A])
huffman@16697
   245
done
huffman@16697
   246
huffman@25926
   247
theorem typedef_Abs_strict_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 "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
huffman@31076
   252
 apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
huffman@25926
   253
 apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
huffman@25926
   254
done
huffman@25926
   255
huffman@25926
   256
theorem typedef_Rep_strict_iff:
huffman@25926
   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@25926
   259
    and UU_in_A: "\<bottom> \<in> A"
huffman@25926
   260
  shows "(Rep x = \<bottom>) = (x = \<bottom>)"
huffman@31076
   261
 apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
huffman@25926
   262
 apply (simp add: type_definition.Rep_inject [OF type])
huffman@25926
   263
done
huffman@25926
   264
huffman@16697
   265
theorem typedef_Abs_defined:
huffman@16697
   266
  assumes type: "type_definition Rep Abs A"
huffman@31076
   267
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   268
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   269
  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
huffman@31076
   270
by (simp add: typedef_Abs_strict_iff [OF type below UU_in_A])
huffman@16697
   271
huffman@16697
   272
theorem typedef_Rep_defined:
huffman@16697
   273
  assumes type: "type_definition Rep Abs A"
huffman@31076
   274
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   275
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   276
  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
huffman@31076
   277
by (simp add: typedef_Rep_strict_iff [OF type below UU_in_A])
huffman@16697
   278
huffman@19519
   279
subsection {* Proving a subtype is flat *}
huffman@19519
   280
huffman@19519
   281
theorem typedef_flat:
huffman@19519
   282
  fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
huffman@19519
   283
  assumes type: "type_definition Rep Abs A"
huffman@31076
   284
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@19519
   285
    and UU_in_A: "\<bottom> \<in> A"
huffman@19519
   286
  shows "OFCLASS('b, flat_class)"
huffman@19519
   287
 apply (intro_classes)
huffman@31076
   288
 apply (unfold below)
huffman@19519
   289
 apply (simp add: type_definition.Rep_inject [OF type, symmetric])
huffman@31076
   290
 apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
huffman@19519
   291
 apply (simp add: ax_flat)
huffman@19519
   292
done
huffman@19519
   293
huffman@16697
   294
subsection {* HOLCF type definition package *}
huffman@16697
   295
haftmann@31738
   296
use "Tools/pcpodef.ML"
huffman@16697
   297
huffman@16697
   298
end