src/HOLCF/Pcpodef.thy
author huffman
Wed Jul 06 00:04:31 2005 +0200 (2005-07-06)
changeset 16697 007f4caab6c1
child 16738 b70bac29b11d
permissions -rw-r--r--
renamed from TypedefPcpo.thy;
added theorems Rep_defined, Abs_defined;
uses pcpodef_package.ML
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
huffman@16697
    10
uses ("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@16697
    27
  apply (subst type_definition.Rep_inject [OF type, symmetric])
huffman@16697
    28
  apply (rule antisym_less, assumption+)
huffman@16697
    29
 apply (rule trans_less, assumption+)
huffman@16697
    30
done
huffman@16697
    31
huffman@16697
    32
huffman@16697
    33
subsection {* Proving a subtype is complete *}
huffman@16697
    34
huffman@16697
    35
text {*
huffman@16697
    36
  A subtype of a cpo is itself a cpo if the ordering is
huffman@16697
    37
  defined in the standard way, and the defining subset
huffman@16697
    38
  is closed with respect to limits of chains.  A set is
huffman@16697
    39
  closed if and only if membership in the set is an
huffman@16697
    40
  admissible predicate.
huffman@16697
    41
*}
huffman@16697
    42
huffman@16697
    43
lemma chain_Rep:
huffman@16697
    44
  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    45
  shows "chain S \<Longrightarrow> chain (\<lambda>n. Rep (S n))"
huffman@16697
    46
by (rule chainI, drule chainE, unfold less)
huffman@16697
    47
huffman@16697
    48
lemma lub_Rep_in_A:
huffman@16697
    49
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
    50
  assumes type: "type_definition Rep Abs A"
huffman@16697
    51
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    52
    and adm:  "adm (\<lambda>x. x \<in> A)"
huffman@16697
    53
  shows "chain S \<Longrightarrow> (LUB n. Rep (S n)) \<in> A"
huffman@16697
    54
 apply (erule admD [OF adm chain_Rep [OF less], rule_format])
huffman@16697
    55
 apply (rule type_definition.Rep [OF type])
huffman@16697
    56
done
huffman@16697
    57
huffman@16697
    58
theorem typedef_is_lub:
huffman@16697
    59
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
    60
  assumes type: "type_definition Rep Abs A"
huffman@16697
    61
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    62
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16697
    63
  shows "chain S \<Longrightarrow> range S <<| Abs (LUB n. Rep (S n))"
huffman@16697
    64
 apply (rule is_lubI)
huffman@16697
    65
  apply (rule ub_rangeI)
huffman@16697
    66
  apply (subst less)
huffman@16697
    67
  apply (subst type_definition.Abs_inverse [OF type])
huffman@16697
    68
   apply (erule lub_Rep_in_A [OF type less adm])
huffman@16697
    69
  apply (rule is_ub_thelub)
huffman@16697
    70
  apply (erule chain_Rep [OF less])
huffman@16697
    71
 apply (subst less)
huffman@16697
    72
 apply (subst type_definition.Abs_inverse [OF type])
huffman@16697
    73
  apply (erule lub_Rep_in_A [OF type less adm])
huffman@16697
    74
 apply (rule is_lub_thelub)
huffman@16697
    75
  apply (erule chain_Rep [OF less])
huffman@16697
    76
 apply (rule ub_rangeI)
huffman@16697
    77
 apply (drule ub_rangeD)
huffman@16697
    78
 apply (unfold less)
huffman@16697
    79
 apply assumption
huffman@16697
    80
done
huffman@16697
    81
huffman@16697
    82
theorem typedef_cpo:
huffman@16697
    83
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
huffman@16697
    84
  assumes type: "type_definition Rep Abs A"
huffman@16697
    85
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
    86
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16697
    87
  shows "OFCLASS('b, cpo_class)"
huffman@16697
    88
 apply (intro_classes)
huffman@16697
    89
 apply (rule_tac x="Abs (LUB n. Rep (S n))" in exI)
huffman@16697
    90
 apply (erule typedef_is_lub [OF type less adm])
huffman@16697
    91
done
huffman@16697
    92
huffman@16697
    93
huffman@16697
    94
subsubsection {* Continuity of @{term Rep} and @{term Abs} *}
huffman@16697
    95
huffman@16697
    96
text {* For any sub-cpo, the @{term Rep} function is continuous. *}
huffman@16697
    97
huffman@16697
    98
theorem typedef_cont_Rep:
huffman@16697
    99
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   100
  assumes type: "type_definition Rep Abs A"
huffman@16697
   101
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   102
    and adm: "adm (\<lambda>x. x \<in> A)"
huffman@16697
   103
  shows "cont Rep"
huffman@16697
   104
 apply (rule contI)
huffman@16697
   105
 apply (simp only: typedef_is_lub [OF type less adm, THEN thelubI])
huffman@16697
   106
 apply (subst type_definition.Abs_inverse [OF type])
huffman@16697
   107
  apply (erule lub_Rep_in_A [OF type less adm])
huffman@16697
   108
 apply (rule thelubE [OF _ refl])
huffman@16697
   109
 apply (erule chain_Rep [OF less])
huffman@16697
   110
done
huffman@16697
   111
huffman@16697
   112
text {*
huffman@16697
   113
  For a sub-cpo, we can make the @{term Abs} function continuous
huffman@16697
   114
  only if we restrict its domain to the defining subset by
huffman@16697
   115
  composing it with another continuous function.
huffman@16697
   116
*}
huffman@16697
   117
huffman@16697
   118
theorem typedef_cont_Abs:
huffman@16697
   119
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   120
  fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
huffman@16697
   121
  assumes type: "type_definition Rep Abs A"
huffman@16697
   122
    and less: "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
    and f_in_A: "\<And>x. f x \<in> A"
huffman@16697
   125
    and cont_f: "cont f"
huffman@16697
   126
  shows "cont (\<lambda>x. Abs (f x))"
huffman@16697
   127
 apply (rule contI)
huffman@16697
   128
 apply (rule is_lubI)
huffman@16697
   129
  apply (rule ub_rangeI)
huffman@16697
   130
  apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
huffman@16697
   131
  apply (rule monofun_fun_arg [OF cont2mono [OF cont_f]])
huffman@16697
   132
  apply (erule is_ub_thelub)
huffman@16697
   133
 apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
huffman@16697
   134
 apply (simp only: contlubE [OF cont2contlub [OF cont_f]])
huffman@16697
   135
 apply (rule is_lub_thelub)
huffman@16697
   136
  apply (erule ch2ch_monofun [OF cont2mono [OF cont_f]])
huffman@16697
   137
 apply (rule ub_rangeI)
huffman@16697
   138
 apply (drule_tac i=i in ub_rangeD)
huffman@16697
   139
 apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
huffman@16697
   140
done
huffman@16697
   141
huffman@16697
   142
subsection {* Proving a subtype is pointed *}
huffman@16697
   143
huffman@16697
   144
text {*
huffman@16697
   145
  A subtype of a cpo has a least element if and only if
huffman@16697
   146
  the defining subset has a least element.
huffman@16697
   147
*}
huffman@16697
   148
huffman@16697
   149
theorem typedef_pcpo:
huffman@16697
   150
  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
huffman@16697
   151
  assumes type: "type_definition Rep Abs A"
huffman@16697
   152
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   153
    and z_in_A: "z \<in> A"
huffman@16697
   154
    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
huffman@16697
   155
  shows "OFCLASS('b, pcpo_class)"
huffman@16697
   156
 apply (intro_classes)
huffman@16697
   157
 apply (rule_tac x="Abs z" in exI, rule allI)
huffman@16697
   158
 apply (unfold less)
huffman@16697
   159
 apply (subst type_definition.Abs_inverse [OF type z_in_A])
huffman@16697
   160
 apply (rule z_least [OF type_definition.Rep [OF type]])
huffman@16697
   161
done
huffman@16697
   162
huffman@16697
   163
text {*
huffman@16697
   164
  As a special case, a subtype of a pcpo has a least element
huffman@16697
   165
  if the defining subset contains @{term \<bottom>}.
huffman@16697
   166
*}
huffman@16697
   167
huffman@16697
   168
theorem typedef_pcpo_UU:
huffman@16697
   169
  fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
huffman@16697
   170
  assumes type: "type_definition Rep Abs A"
huffman@16697
   171
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   172
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   173
  shows "OFCLASS('b, pcpo_class)"
huffman@16697
   174
by (rule typedef_pcpo [OF type less UU_in_A], rule minimal)
huffman@16697
   175
huffman@16697
   176
subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
huffman@16697
   177
huffman@16697
   178
text {*
huffman@16697
   179
  For a sub-pcpo where @{term \<bottom>} is a member of the defining
huffman@16697
   180
  subset, @{term Rep} and @{term Abs} are both strict.
huffman@16697
   181
*}
huffman@16697
   182
huffman@16697
   183
theorem typedef_Abs_strict:
huffman@16697
   184
  assumes type: "type_definition Rep Abs A"
huffman@16697
   185
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   186
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   187
  shows "Abs \<bottom> = \<bottom>"
huffman@16697
   188
 apply (rule UU_I, unfold less)
huffman@16697
   189
 apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
huffman@16697
   190
done
huffman@16697
   191
huffman@16697
   192
theorem typedef_Rep_strict:
huffman@16697
   193
  assumes type: "type_definition Rep Abs A"
huffman@16697
   194
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   195
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   196
  shows "Rep \<bottom> = \<bottom>"
huffman@16697
   197
 apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
huffman@16697
   198
 apply (rule type_definition.Abs_inverse [OF type UU_in_A])
huffman@16697
   199
done
huffman@16697
   200
huffman@16697
   201
theorem typedef_Abs_defined:
huffman@16697
   202
  assumes type: "type_definition Rep Abs A"
huffman@16697
   203
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   204
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   205
  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
huffman@16697
   206
 apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
huffman@16697
   207
 apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
huffman@16697
   208
done
huffman@16697
   209
huffman@16697
   210
theorem typedef_Rep_defined:
huffman@16697
   211
  assumes type: "type_definition Rep Abs A"
huffman@16697
   212
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@16697
   213
    and UU_in_A: "\<bottom> \<in> A"
huffman@16697
   214
  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
huffman@16697
   215
 apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
huffman@16697
   216
 apply (simp add: type_definition.Rep_inject [OF type])
huffman@16697
   217
done
huffman@16697
   218
huffman@16697
   219
subsection {* HOLCF type definition package *}
huffman@16697
   220
huffman@16697
   221
use "pcpodef_package.ML"
huffman@16697
   222
huffman@16697
   223
end