src/HOL/HOLCF/Cpodef.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62175 8ffc4d0e652d
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Cpodef.thy
huffman@16697
     2
    Author:     Brian Huffman
huffman@16697
     3
*)
huffman@16697
     4
wenzelm@62175
     5
section \<open>Subtypes of pcpos\<close>
huffman@16697
     6
huffman@40772
     7
theory Cpodef
huffman@16697
     8
imports Adm
wenzelm@46950
     9
keywords "pcpodef" "cpodef" :: thy_goal
huffman@16697
    10
begin
huffman@16697
    11
wenzelm@62175
    12
subsection \<open>Proving a subtype is a partial order\<close>
huffman@16697
    13
wenzelm@62175
    14
text \<open>
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.
wenzelm@62175
    17
\<close>
huffman@16697
    18
wenzelm@62175
    19
setup \<open>Sign.add_const_constraint (@{const_name Porder.below}, NONE)\<close>
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
wenzelm@62175
    33
setup \<open>Sign.add_const_constraint (@{const_name Porder.below},
wenzelm@62175
    34
  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"})\<close>
haftmann@28073
    35
wenzelm@62175
    36
subsection \<open>Proving a subtype is finite\<close>
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
wenzelm@62175
    49
subsection \<open>Proving a subtype is chain-finite\<close>
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
wenzelm@62175
    68
subsection \<open>Proving a subtype is complete\<close>
huffman@16697
    69
wenzelm@62175
    70
text \<open>
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.
wenzelm@62175
    76
\<close>
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@40770
    94
theorem typedef_is_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
wenzelm@45606
   110
lemmas typedef_lub = typedef_is_lub [THEN lub_eqI]
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@40770
   121
    by (rule typedef_is_lub [OF type below adm])
huffman@16918
   122
  thus "\<exists>x. range S <<| x" ..
huffman@16918
   123
qed
huffman@16697
   124
wenzelm@62175
   125
subsubsection \<open>Continuity of \emph{Rep} and \emph{Abs}\<close>
huffman@16697
   126
wenzelm@62175
   127
text \<open>For any sub-cpo, the @{term Rep} function is continuous.\<close>
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@40834
   134
  shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))"
huffman@40834
   135
 apply (erule cont_apply [OF _ _ cont_const])
huffman@16697
   136
 apply (rule contI)
huffman@40770
   137
 apply (simp only: typedef_lub [OF type below adm])
huffman@31076
   138
 apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
huffman@26027
   139
 apply (rule cpo_lubI)
huffman@31076
   140
 apply (erule ch2ch_Rep [OF below])
huffman@16697
   141
done
huffman@16697
   142
wenzelm@62175
   143
text \<open>
huffman@16697
   144
  For a sub-cpo, we can make the @{term Abs} function continuous
huffman@16697
   145
  only if we restrict its domain to the defining subset by
huffman@16697
   146
  composing it with another continuous function.
wenzelm@62175
   147
\<close>
huffman@16697
   148
huffman@16697
   149
theorem typedef_cont_Abs:
huffman@16697
   150
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   151
  fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
huffman@16697
   152
  assumes type: "type_definition Rep Abs A"
huffman@31076
   153
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16918
   154
    and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
huffman@16697
   155
    and f_in_A: "\<And>x. f x \<in> A"
huffman@40325
   156
  shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
huffman@40325
   157
unfolding cont_def is_lub_def is_ub_def ball_simps below
huffman@40325
   158
by (simp add: type_definition.Abs_inverse [OF type f_in_A])
huffman@16697
   159
wenzelm@62175
   160
subsection \<open>Proving subtype elements are compact\<close>
huffman@17833
   161
huffman@17833
   162
theorem typedef_compact:
huffman@17833
   163
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@17833
   164
  assumes type: "type_definition Rep Abs A"
huffman@31076
   165
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@17833
   166
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@17833
   167
  shows "compact (Rep k) \<Longrightarrow> compact k"
huffman@17833
   168
proof (unfold compact_def)
huffman@17833
   169
  have cont_Rep: "cont Rep"
huffman@40834
   170
    by (rule typedef_cont_Rep [OF type below adm cont_id])
huffman@41182
   171
  assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)"
huffman@41182
   172
  with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst)
huffman@41182
   173
  thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
huffman@17833
   174
qed
huffman@17833
   175
wenzelm@62175
   176
subsection \<open>Proving a subtype is pointed\<close>
huffman@16697
   177
wenzelm@62175
   178
text \<open>
huffman@16697
   179
  A subtype of a cpo has a least element if and only if
huffman@16697
   180
  the defining subset has a least element.
wenzelm@62175
   181
\<close>
huffman@16697
   182
huffman@16918
   183
theorem typedef_pcpo_generic:
huffman@16697
   184
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   185
  assumes type: "type_definition Rep Abs A"
huffman@31076
   186
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   187
    and z_in_A: "z \<in> A"
huffman@16697
   188
    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
huffman@16697
   189
  shows "OFCLASS('b, pcpo_class)"
huffman@16697
   190
 apply (intro_classes)
huffman@16697
   191
 apply (rule_tac x="Abs z" in exI, rule allI)
huffman@31076
   192
 apply (unfold below)
huffman@16697
   193
 apply (subst type_definition.Abs_inverse [OF type z_in_A])
huffman@16697
   194
 apply (rule z_least [OF type_definition.Rep [OF type]])
huffman@16697
   195
done
huffman@16697
   196
wenzelm@62175
   197
text \<open>
huffman@16697
   198
  As a special case, a subtype of a pcpo has a least element
huffman@16697
   199
  if the defining subset contains @{term \<bottom>}.
wenzelm@62175
   200
\<close>
huffman@16697
   201
huffman@16918
   202
theorem typedef_pcpo:
huffman@16697
   203
  fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
huffman@16697
   204
  assumes type: "type_definition Rep Abs A"
huffman@31076
   205
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   206
    and bottom_in_A: "\<bottom> \<in> A"
huffman@16697
   207
  shows "OFCLASS('b, pcpo_class)"
huffman@41430
   208
by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
huffman@16697
   209
wenzelm@62175
   210
subsubsection \<open>Strictness of \emph{Rep} and \emph{Abs}\<close>
huffman@16697
   211
wenzelm@62175
   212
text \<open>
huffman@16697
   213
  For a sub-pcpo where @{term \<bottom>} is a member of the defining
huffman@16697
   214
  subset, @{term Rep} and @{term Abs} are both strict.
wenzelm@62175
   215
\<close>
huffman@16697
   216
huffman@16697
   217
theorem typedef_Abs_strict:
huffman@16697
   218
  assumes type: "type_definition Rep Abs A"
huffman@31076
   219
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   220
    and bottom_in_A: "\<bottom> \<in> A"
huffman@16697
   221
  shows "Abs \<bottom> = \<bottom>"
huffman@41430
   222
 apply (rule bottomI, unfold below)
huffman@41430
   223
 apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
huffman@16697
   224
done
huffman@16697
   225
huffman@16697
   226
theorem typedef_Rep_strict:
huffman@16697
   227
  assumes type: "type_definition Rep Abs A"
huffman@31076
   228
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   229
    and bottom_in_A: "\<bottom> \<in> A"
huffman@16697
   230
  shows "Rep \<bottom> = \<bottom>"
huffman@41430
   231
 apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
huffman@41430
   232
 apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
huffman@16697
   233
done
huffman@16697
   234
huffman@40321
   235
theorem typedef_Abs_bottom_iff:
huffman@25926
   236
  assumes type: "type_definition Rep Abs A"
huffman@31076
   237
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   238
    and bottom_in_A: "\<bottom> \<in> A"
huffman@25926
   239
  shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
huffman@41430
   240
 apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
huffman@41430
   241
 apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
huffman@25926
   242
done
huffman@25926
   243
huffman@40321
   244
theorem typedef_Rep_bottom_iff:
huffman@25926
   245
  assumes type: "type_definition Rep Abs A"
huffman@31076
   246
    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   247
    and bottom_in_A: "\<bottom> \<in> A"
huffman@25926
   248
  shows "(Rep x = \<bottom>) = (x = \<bottom>)"
huffman@41430
   249
 apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
huffman@25926
   250
 apply (simp add: type_definition.Rep_inject [OF type])
huffman@25926
   251
done
huffman@25926
   252
wenzelm@62175
   253
subsection \<open>Proving a subtype is flat\<close>
huffman@19519
   254
huffman@19519
   255
theorem typedef_flat:
huffman@19519
   256
  fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
huffman@19519
   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@41430
   259
    and bottom_in_A: "\<bottom> \<in> A"
huffman@19519
   260
  shows "OFCLASS('b, flat_class)"
huffman@19519
   261
 apply (intro_classes)
huffman@31076
   262
 apply (unfold below)
huffman@19519
   263
 apply (simp add: type_definition.Rep_inject [OF type, symmetric])
huffman@41430
   264
 apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])
huffman@19519
   265
 apply (simp add: ax_flat)
huffman@19519
   266
done
huffman@19519
   267
wenzelm@62175
   268
subsection \<open>HOLCF type definition package\<close>
huffman@16697
   269
wenzelm@48891
   270
ML_file "Tools/cpodef.ML"
huffman@16697
   271
huffman@16697
   272
end