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