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