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