src/HOLCF/TypedefPcpo.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16208 cfe047ad6384
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16058
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/TypedefPcpo.thy
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     2
    ID:         $Id$
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     3
    Author:     Brian Huffman
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     4
*)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     5
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     6
header {* Subtypes of pcpos *}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     7
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     8
theory TypedefPcpo
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
     9
imports Adm
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    10
begin
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    11
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    12
subsection {* Proving a subtype is a partial order *}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    13
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    14
text {*
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    15
  A subtype of a partial order is itself a partial order,
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    16
  if the ordering is defined in the standard way.
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    17
*}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    18
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    19
theorem typedef_po:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    20
fixes Abs :: "'a::po \<Rightarrow> 'b::sq_ord"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    21
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    22
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    23
shows "OFCLASS('b, po_class)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    24
 apply (intro_classes, unfold less)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    25
   apply (rule refl_less)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    26
  apply (subst type_definition.Rep_inject [OF type, symmetric])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    27
  apply (rule antisym_less, assumption+)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    28
 apply (rule trans_less, assumption+)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    29
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    30
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    31
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    32
subsection {* Proving a subtype is complete *}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    33
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    34
text {*
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    35
  A subtype of a cpo is itself a cpo if the ordering is
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    36
  defined in the standard way, and the defining subset
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    37
  is closed with respect to limits of chains.  A set is
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    38
  closed if and only if membership in the set is an
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    39
  admissible predicate.
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    40
*}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    41
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    42
lemma chain_Rep:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    43
assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    44
shows "chain S \<Longrightarrow> chain (\<lambda>n. Rep (S n))"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    45
by (rule chainI, drule chainE, unfold less)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    46
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    47
lemma lub_Rep_in_A:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    48
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    49
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    50
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    51
    and adm:  "adm (\<lambda>x. x \<in> A)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    52
shows "chain S \<Longrightarrow> (LUB n. Rep (S n)) \<in> A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    53
 apply (erule admD [OF adm chain_Rep [OF less], rule_format])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    54
 apply (rule type_definition.Rep [OF type])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    55
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    56
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    57
theorem typedef_is_lub:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    58
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    59
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    60
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    61
    and adm: "adm (\<lambda>x. x \<in> A)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    62
shows "chain S \<Longrightarrow> range S <<| Abs (LUB n. Rep (S n))"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    63
 apply (rule is_lubI)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    64
  apply (rule ub_rangeI)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    65
  apply (subst less)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    66
  apply (subst type_definition.Abs_inverse [OF type])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    67
   apply (erule lub_Rep_in_A [OF type less adm])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    68
  apply (rule is_ub_thelub)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    69
  apply (erule chain_Rep [OF less])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    70
 apply (subst less)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    71
 apply (subst type_definition.Abs_inverse [OF type])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    72
  apply (erule lub_Rep_in_A [OF type less adm])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    73
 apply (rule is_lub_thelub)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    74
  apply (erule chain_Rep [OF less])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    75
 apply (rule ub_rangeI)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    76
 apply (drule ub_rangeD)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    77
 apply (unfold less)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    78
 apply assumption
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    79
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    80
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    81
theorem typedef_cpo:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    82
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    83
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    84
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    85
    and adm: "adm (\<lambda>x. x \<in> A)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    86
shows "OFCLASS('b, cpo_class)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    87
 apply (intro_classes)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    88
 apply (rule_tac x="Abs (LUB n. Rep (S n))" in exI)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    89
 apply (erule typedef_is_lub [OF type less adm])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    90
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    91
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    92
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    93
subsubsection {* Continuity of @{term Rep} and @{term Abs} *}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    94
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    95
text {* For any sub-cpo, the @{term Rep} function is continuous. *}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    96
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    97
theorem typedef_cont_Rep:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    98
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
    99
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   100
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   101
    and adm: "adm (\<lambda>x. x \<in> A)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   102
shows "cont Rep"
16208
cfe047ad6384 changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents: 16080
diff changeset
   103
 apply (rule contI)
16058
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   104
 apply (simp only: typedef_is_lub [OF type less adm, THEN thelubI])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   105
 apply (subst type_definition.Abs_inverse [OF type])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   106
  apply (erule lub_Rep_in_A [OF type less adm])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   107
 apply (rule thelubE [OF _ refl])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   108
 apply (erule chain_Rep [OF less])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   109
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   110
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   111
text {*
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   112
  For a sub-cpo, we can make the @{term Abs} function continuous
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   113
  only if we restrict its domain to the defining subset by
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   114
  composing it with another continuous function.
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   115
*}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   116
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   117
theorem typedef_cont_Abs:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   118
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   119
fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   120
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   121
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   122
    and adm: "adm (\<lambda>x. x \<in> A)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   123
    and f_in_A: "\<And>x. f x \<in> A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   124
    and cont_f: "cont f"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   125
shows "cont (\<lambda>x. Abs (f x))"
16208
cfe047ad6384 changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents: 16080
diff changeset
   126
 apply (rule contI)
16058
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   127
 apply (rule is_lubI)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   128
  apply (rule ub_rangeI)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   129
  apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   130
  apply (rule monofun_fun_arg [OF cont2mono [OF cont_f]])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   131
  apply (erule is_ub_thelub)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   132
 apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
16208
cfe047ad6384 changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents: 16080
diff changeset
   133
 apply (simp only: contlubE [OF cont2contlub [OF cont_f]])
16058
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   134
 apply (rule is_lub_thelub)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   135
  apply (erule ch2ch_monofun [OF cont2mono [OF cont_f]])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   136
 apply (rule ub_rangeI)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   137
 apply (drule_tac i=i in ub_rangeD)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   138
 apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   139
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   140
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   141
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   142
subsection {* Proving a typedef is pointed *}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   143
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   144
text {*
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   145
  A subtype of a cpo has a least element if and only if
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   146
  the defining subset has a least element.
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   147
*}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   148
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   149
theorem typedef_pcpo:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   150
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   151
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   152
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   153
    and z_in_A: "z \<in> A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   154
    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   155
shows "OFCLASS('b, pcpo_class)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   156
 apply (intro_classes)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   157
 apply (rule_tac x="Abs z" in exI, rule allI)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   158
 apply (unfold less)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   159
 apply (subst type_definition.Abs_inverse [OF type z_in_A])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   160
 apply (rule z_least [OF type_definition.Rep [OF type]])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   161
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   162
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   163
text {*
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   164
  As a special case, a subtype of a pcpo has a least element
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   165
  if the defining subset contains @{term \<bottom>}.
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   166
*}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   167
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   168
theorem typedef_pcpo_UU:
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   169
fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   170
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   171
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   172
    and UU_in_A: "\<bottom> \<in> A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   173
shows "OFCLASS('b, pcpo_class)"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   174
by (rule typedef_pcpo [OF type less UU_in_A], rule minimal)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   175
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   176
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   177
subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   178
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   179
text {*
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   180
  For a sub-pcpo where @{term \<bottom>} is a member of the defining
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   181
  subset, @{term Rep} and @{term Abs} are both strict.
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   182
*}
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   183
16208
cfe047ad6384 changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents: 16080
diff changeset
   184
theorem typedef_Abs_strict:
16058
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   185
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   186
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   187
    and UU_in_A: "\<bottom> \<in> A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   188
shows "Abs \<bottom> = \<bottom>"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   189
 apply (rule UU_I, unfold less)
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   190
 apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   191
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   192
16208
cfe047ad6384 changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents: 16080
diff changeset
   193
theorem typedef_Rep_strict:
16058
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   194
assumes type: "type_definition Rep Abs A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   195
    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   196
    and UU_in_A: "\<bottom> \<in> A"
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   197
shows "Rep \<bottom> = \<bottom>"
16208
cfe047ad6384 changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
huffman
parents: 16080
diff changeset
   198
 apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
16058
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   199
 apply (rule type_definition.Abs_inverse [OF type UU_in_A])
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   200
done
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   201
3d50b521ab16 New theory for defining subtypes of pcpos
huffman
parents:
diff changeset
   202
end