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