src/HOL/HOLCF/Cpodef.thy
author wenzelm
Thu Mar 14 16:55:06 2019 +0100 (5 weeks ago)
changeset 69913 ca515cf61651
parent 69605 a96320074298
permissions -rw-r--r--
more specific keyword kinds;
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
wenzelm@67312
     8
  imports Adm
wenzelm@69913
     9
  keywords "pcpodef" "cpodef" :: thy_goal_defn
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@67312
    19
setup \<open>Sign.add_const_constraint (\<^const_name>\<open>Porder.below\<close>, 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"
nipkow@67399
    24
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    25
  shows "OFCLASS('b, po_class)"
wenzelm@67312
    26
  apply (intro_classes, unfold below)
wenzelm@67312
    27
    apply (rule below_refl)
wenzelm@67312
    28
   apply (erule (1) below_trans)
wenzelm@67312
    29
  apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
wenzelm@67312
    30
  apply (erule (1) below_antisym)
wenzelm@67312
    31
  done
huffman@16697
    32
wenzelm@67312
    33
setup \<open>Sign.add_const_constraint (\<^const_name>\<open>Porder.below\<close>, SOME \<^typ>\<open>'a::below \<Rightarrow> 'a::below \<Rightarrow> bool\<close>)\<close>
wenzelm@67312
    34
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"
wenzelm@67312
    44
  then have "finite (Abs ` A)"
wenzelm@67312
    45
    by (rule finite_imageI)
wenzelm@67312
    46
  then show "finite (UNIV :: 'b set)"
huffman@27296
    47
    by (simp only: type_definition.Abs_image [OF type])
huffman@25827
    48
qed
huffman@25827
    49
wenzelm@67312
    50
wenzelm@62175
    51
subsection \<open>Proving a subtype is chain-finite\<close>
huffman@17812
    52
huffman@40035
    53
lemma ch2ch_Rep:
nipkow@67399
    54
  assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@40035
    55
  shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
wenzelm@67312
    56
  unfolding chain_def below .
huffman@17812
    57
huffman@17812
    58
theorem typedef_chfin:
huffman@17812
    59
  fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
huffman@17812
    60
  assumes type: "type_definition Rep Abs A"
nipkow@67399
    61
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@17812
    62
  shows "OFCLASS('b, chfin_class)"
wenzelm@67312
    63
  apply intro_classes
wenzelm@67312
    64
  apply (drule ch2ch_Rep [OF below])
wenzelm@67312
    65
  apply (drule chfin)
wenzelm@67312
    66
  apply (unfold max_in_chain_def)
wenzelm@67312
    67
  apply (simp add: type_definition.Rep_inject [OF type])
wenzelm@67312
    68
  done
wenzelm@67312
    69
huffman@17812
    70
wenzelm@62175
    71
subsection \<open>Proving a subtype is complete\<close>
huffman@16697
    72
wenzelm@62175
    73
text \<open>
huffman@16697
    74
  A subtype of a cpo is itself a cpo if the ordering is
huffman@16697
    75
  defined in the standard way, and the defining subset
huffman@16697
    76
  is closed with respect to limits of chains.  A set is
huffman@16697
    77
  closed if and only if membership in the set is an
huffman@16697
    78
  admissible predicate.
wenzelm@62175
    79
\<close>
huffman@16697
    80
huffman@40035
    81
lemma typedef_is_lubI:
nipkow@67399
    82
  assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@40035
    83
  shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
wenzelm@67312
    84
  by (simp add: is_lub_def is_ub_def below)
huffman@40035
    85
huffman@16918
    86
lemma Abs_inverse_lub_Rep:
huffman@16697
    87
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
    88
  assumes type: "type_definition Rep Abs A"
nipkow@67399
    89
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    90
    and adm:  "adm (\<lambda>x. x \<in> A)"
huffman@16918
    91
  shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
wenzelm@67312
    92
  apply (rule type_definition.Abs_inverse [OF type])
wenzelm@67312
    93
  apply (erule admD [OF adm ch2ch_Rep [OF below]])
wenzelm@67312
    94
  apply (rule type_definition.Rep [OF type])
wenzelm@67312
    95
  done
huffman@16697
    96
huffman@40770
    97
theorem typedef_is_lub:
huffman@16697
    98
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
    99
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   100
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   101
    and adm: "adm (\<lambda>x. x \<in> A)"
wenzelm@67312
   102
  assumes S: "chain S"
wenzelm@67312
   103
  shows "range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@40035
   104
proof -
wenzelm@67312
   105
  from S have "chain (\<lambda>i. Rep (S i))"
wenzelm@67312
   106
    by (rule ch2ch_Rep [OF below])
wenzelm@67312
   107
  then have "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))"
wenzelm@67312
   108
    by (rule cpo_lubI)
wenzelm@67312
   109
  then have "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
huffman@40035
   110
    by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
wenzelm@67312
   111
  then show "range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@40035
   112
    by (rule typedef_is_lubI [OF below])
huffman@40035
   113
qed
huffman@16697
   114
wenzelm@45606
   115
lemmas typedef_lub = typedef_is_lub [THEN lub_eqI]
huffman@16918
   116
huffman@16697
   117
theorem typedef_cpo:
huffman@16697
   118
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
   119
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   120
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   121
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16697
   122
  shows "OFCLASS('b, cpo_class)"
huffman@16918
   123
proof
wenzelm@67312
   124
  fix S :: "nat \<Rightarrow> 'b"
wenzelm@67312
   125
  assume "chain S"
wenzelm@67312
   126
  then have "range S <<| Abs (\<Squnion>i. Rep (S i))"
huffman@40770
   127
    by (rule typedef_is_lub [OF type below adm])
wenzelm@67312
   128
  then show "\<exists>x. range S <<| x" ..
huffman@16918
   129
qed
huffman@16697
   130
wenzelm@67312
   131
wenzelm@62175
   132
subsubsection \<open>Continuity of \emph{Rep} and \emph{Abs}\<close>
huffman@16697
   133
wenzelm@69597
   134
text \<open>For any sub-cpo, the \<^term>\<open>Rep\<close> function is continuous.\<close>
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"
nipkow@67399
   139
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   140
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@40834
   141
  shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))"
wenzelm@67312
   142
  apply (erule cont_apply [OF _ _ cont_const])
wenzelm@67312
   143
  apply (rule contI)
wenzelm@67312
   144
  apply (simp only: typedef_lub [OF type below adm])
wenzelm@67312
   145
  apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
wenzelm@67312
   146
  apply (rule cpo_lubI)
wenzelm@67312
   147
  apply (erule ch2ch_Rep [OF below])
wenzelm@67312
   148
  done
huffman@16697
   149
wenzelm@62175
   150
text \<open>
wenzelm@69597
   151
  For a sub-cpo, we can make the \<^term>\<open>Abs\<close> function continuous
huffman@16697
   152
  only if we restrict its domain to the defining subset by
huffman@16697
   153
  composing it with another continuous function.
wenzelm@62175
   154
\<close>
huffman@16697
   155
huffman@16697
   156
theorem typedef_cont_Abs:
huffman@16697
   157
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   158
  fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
huffman@16697
   159
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   160
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16918
   161
    and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
huffman@16697
   162
    and f_in_A: "\<And>x. f x \<in> A"
huffman@40325
   163
  shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
wenzelm@67312
   164
  unfolding cont_def is_lub_def is_ub_def ball_simps below
wenzelm@67312
   165
  by (simp add: type_definition.Abs_inverse [OF type f_in_A])
wenzelm@67312
   166
huffman@16697
   167
wenzelm@62175
   168
subsection \<open>Proving subtype elements are compact\<close>
huffman@17833
   169
huffman@17833
   170
theorem typedef_compact:
huffman@17833
   171
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@17833
   172
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   173
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@17833
   174
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@17833
   175
  shows "compact (Rep k) \<Longrightarrow> compact k"
huffman@17833
   176
proof (unfold compact_def)
huffman@17833
   177
  have cont_Rep: "cont Rep"
huffman@40834
   178
    by (rule typedef_cont_Rep [OF type below adm cont_id])
huffman@41182
   179
  assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)"
huffman@41182
   180
  with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst)
wenzelm@67312
   181
  then show "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
huffman@17833
   182
qed
huffman@17833
   183
wenzelm@67312
   184
wenzelm@62175
   185
subsection \<open>Proving a subtype is pointed\<close>
huffman@16697
   186
wenzelm@62175
   187
text \<open>
huffman@16697
   188
  A subtype of a cpo has a least element if and only if
huffman@16697
   189
  the defining subset has a least element.
wenzelm@62175
   190
\<close>
huffman@16697
   191
huffman@16918
   192
theorem typedef_pcpo_generic:
huffman@16697
   193
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   194
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   195
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   196
    and z_in_A: "z \<in> A"
huffman@16697
   197
    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
huffman@16697
   198
  shows "OFCLASS('b, pcpo_class)"
wenzelm@67312
   199
  apply (intro_classes)
wenzelm@67312
   200
  apply (rule_tac x="Abs z" in exI, rule allI)
wenzelm@67312
   201
  apply (unfold below)
wenzelm@67312
   202
  apply (subst type_definition.Abs_inverse [OF type z_in_A])
wenzelm@67312
   203
  apply (rule z_least [OF type_definition.Rep [OF type]])
wenzelm@67312
   204
  done
huffman@16697
   205
wenzelm@62175
   206
text \<open>
huffman@16697
   207
  As a special case, a subtype of a pcpo has a least element
wenzelm@69597
   208
  if the defining subset contains \<^term>\<open>\<bottom>\<close>.
wenzelm@62175
   209
\<close>
huffman@16697
   210
huffman@16918
   211
theorem typedef_pcpo:
huffman@16697
   212
  fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
huffman@16697
   213
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   214
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   215
    and bottom_in_A: "\<bottom> \<in> A"
huffman@16697
   216
  shows "OFCLASS('b, pcpo_class)"
wenzelm@67312
   217
  by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
wenzelm@67312
   218
huffman@16697
   219
wenzelm@62175
   220
subsubsection \<open>Strictness of \emph{Rep} and \emph{Abs}\<close>
huffman@16697
   221
wenzelm@62175
   222
text \<open>
wenzelm@69597
   223
  For a sub-pcpo where \<^term>\<open>\<bottom>\<close> is a member of the defining
wenzelm@69597
   224
  subset, \<^term>\<open>Rep\<close> and \<^term>\<open>Abs\<close> are both strict.
wenzelm@62175
   225
\<close>
huffman@16697
   226
huffman@16697
   227
theorem typedef_Abs_strict:
huffman@16697
   228
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   229
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   230
    and bottom_in_A: "\<bottom> \<in> A"
huffman@16697
   231
  shows "Abs \<bottom> = \<bottom>"
wenzelm@67312
   232
  apply (rule bottomI, unfold below)
wenzelm@67312
   233
  apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
wenzelm@67312
   234
  done
huffman@16697
   235
huffman@16697
   236
theorem typedef_Rep_strict:
huffman@16697
   237
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   238
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   239
    and bottom_in_A: "\<bottom> \<in> A"
huffman@16697
   240
  shows "Rep \<bottom> = \<bottom>"
wenzelm@67312
   241
  apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
wenzelm@67312
   242
  apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
wenzelm@67312
   243
  done
huffman@16697
   244
huffman@40321
   245
theorem typedef_Abs_bottom_iff:
huffman@25926
   246
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   247
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   248
    and bottom_in_A: "\<bottom> \<in> A"
huffman@25926
   249
  shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
wenzelm@67312
   250
  apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
wenzelm@67312
   251
  apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
wenzelm@67312
   252
  done
huffman@25926
   253
huffman@40321
   254
theorem typedef_Rep_bottom_iff:
huffman@25926
   255
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   256
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   257
    and bottom_in_A: "\<bottom> \<in> A"
huffman@25926
   258
  shows "(Rep x = \<bottom>) = (x = \<bottom>)"
wenzelm@67312
   259
  apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
wenzelm@67312
   260
  apply (simp add: type_definition.Rep_inject [OF type])
wenzelm@67312
   261
  done
wenzelm@67312
   262
huffman@25926
   263
wenzelm@62175
   264
subsection \<open>Proving a subtype is flat\<close>
huffman@19519
   265
huffman@19519
   266
theorem typedef_flat:
huffman@19519
   267
  fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
huffman@19519
   268
  assumes type: "type_definition Rep Abs A"
nipkow@67399
   269
    and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@41430
   270
    and bottom_in_A: "\<bottom> \<in> A"
huffman@19519
   271
  shows "OFCLASS('b, flat_class)"
wenzelm@67312
   272
  apply (intro_classes)
wenzelm@67312
   273
  apply (unfold below)
wenzelm@67312
   274
  apply (simp add: type_definition.Rep_inject [OF type, symmetric])
wenzelm@67312
   275
  apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])
wenzelm@67312
   276
  apply (simp add: ax_flat)
wenzelm@67312
   277
  done
wenzelm@67312
   278
huffman@19519
   279
wenzelm@62175
   280
subsection \<open>HOLCF type definition package\<close>
huffman@16697
   281
wenzelm@69605
   282
ML_file \<open>Tools/cpodef.ML\<close>
huffman@16697
   283
huffman@16697
   284
end