src/HOLCF/Pcpodef.thy
author haftmann
Tue Jul 10 17:30:50 2007 +0200 (2007-07-10)
changeset 23709 fd31da8f752a
parent 23152 9497234a2743
child 25827 c2adeb1bae5c
permissions -rw-r--r--
moved lfp_induct2 here
     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 (rule type_definition.Rep_inject [OF type, THEN iffD1])
    28   apply (erule (1) antisym_less)
    29  apply (erule (1) trans_less)
    30 done
    31 
    32 
    33 subsection {* Proving a subtype is chain-finite *}
    34 
    35 lemma monofun_Rep:
    36   assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    37   shows "monofun Rep"
    38 by (rule monofunI, unfold less)
    39 
    40 lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]
    41 lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]
    42 
    43 theorem typedef_chfin:
    44   fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
    45   assumes type: "type_definition Rep Abs A"
    46     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    47   shows "OFCLASS('b, chfin_class)"
    48  apply (intro_classes, clarify)
    49  apply (drule ch2ch_Rep [OF less])
    50  apply (drule chfin [rule_format])
    51  apply (unfold max_in_chain_def)
    52  apply (simp add: type_definition.Rep_inject [OF type])
    53 done
    54 
    55 
    56 subsection {* Proving a subtype is complete *}
    57 
    58 text {*
    59   A subtype of a cpo is itself a cpo if the ordering is
    60   defined in the standard way, and the defining subset
    61   is closed with respect to limits of chains.  A set is
    62   closed if and only if membership in the set is an
    63   admissible predicate.
    64 *}
    65 
    66 lemma Abs_inverse_lub_Rep:
    67   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
    68   assumes type: "type_definition Rep Abs A"
    69     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    70     and adm:  "adm (\<lambda>x. x \<in> A)"
    71   shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
    72  apply (rule type_definition.Abs_inverse [OF type])
    73  apply (erule admD [OF adm ch2ch_Rep [OF less], rule_format])
    74  apply (rule type_definition.Rep [OF type])
    75 done
    76 
    77 theorem typedef_lub:
    78   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
    79   assumes type: "type_definition Rep Abs A"
    80     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    81     and adm: "adm (\<lambda>x. x \<in> A)"
    82   shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
    83  apply (frule ch2ch_Rep [OF less])
    84  apply (rule is_lubI)
    85   apply (rule ub_rangeI)
    86   apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
    87   apply (erule is_ub_thelub)
    88  apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
    89  apply (erule is_lub_thelub)
    90  apply (erule ub2ub_Rep [OF less])
    91 done
    92 
    93 lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
    94 
    95 theorem typedef_cpo:
    96   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
    97   assumes type: "type_definition Rep Abs A"
    98     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    99     and adm: "adm (\<lambda>x. x \<in> A)"
   100   shows "OFCLASS('b, cpo_class)"
   101 proof
   102   fix S::"nat \<Rightarrow> 'b" assume "chain S"
   103   hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
   104     by (rule typedef_lub [OF type less adm])
   105   thus "\<exists>x. range S <<| x" ..
   106 qed
   107 
   108 
   109 subsubsection {* Continuity of @{term Rep} and @{term Abs} *}
   110 
   111 text {* For any sub-cpo, the @{term Rep} function is continuous. *}
   112 
   113 theorem typedef_cont_Rep:
   114   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   115   assumes type: "type_definition Rep Abs A"
   116     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   117     and adm: "adm (\<lambda>x. x \<in> A)"
   118   shows "cont Rep"
   119  apply (rule contI)
   120  apply (simp only: typedef_thelub [OF type less adm])
   121  apply (simp only: Abs_inverse_lub_Rep [OF type less adm])
   122  apply (rule thelubE [OF _ refl])
   123  apply (erule ch2ch_Rep [OF less])
   124 done
   125 
   126 text {*
   127   For a sub-cpo, we can make the @{term Abs} function continuous
   128   only if we restrict its domain to the defining subset by
   129   composing it with another continuous function.
   130 *}
   131 
   132 theorem typedef_is_lubI:
   133   assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   134   shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
   135  apply (rule is_lubI)
   136   apply (rule ub_rangeI)
   137   apply (subst less)
   138   apply (erule is_ub_lub)
   139  apply (subst less)
   140  apply (erule is_lub_lub)
   141  apply (erule ub2ub_Rep [OF less])
   142 done
   143 
   144 theorem typedef_cont_Abs:
   145   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   146   fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
   147   assumes type: "type_definition Rep Abs A"
   148     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   149     and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
   150     and f_in_A: "\<And>x. f x \<in> A"
   151     and cont_f: "cont f"
   152   shows "cont (\<lambda>x. Abs (f x))"
   153  apply (rule contI)
   154  apply (rule typedef_is_lubI [OF less])
   155  apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
   156  apply (erule cont_f [THEN contE])
   157 done
   158 
   159 subsection {* Proving subtype elements are compact *}
   160 
   161 theorem typedef_compact:
   162   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   163   assumes type: "type_definition Rep Abs A"
   164     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   165     and adm: "adm (\<lambda>x. x \<in> A)"
   166   shows "compact (Rep k) \<Longrightarrow> compact k"
   167 proof (unfold compact_def)
   168   have cont_Rep: "cont Rep"
   169     by (rule typedef_cont_Rep [OF type less adm])
   170   assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
   171   with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
   172   thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold less)
   173 qed
   174 
   175 subsection {* Proving a subtype is pointed *}
   176 
   177 text {*
   178   A subtype of a cpo has a least element if and only if
   179   the defining subset has a least element.
   180 *}
   181 
   182 theorem typedef_pcpo_generic:
   183   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   184   assumes type: "type_definition Rep Abs A"
   185     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   186     and z_in_A: "z \<in> A"
   187     and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
   188   shows "OFCLASS('b, pcpo_class)"
   189  apply (intro_classes)
   190  apply (rule_tac x="Abs z" in exI, rule allI)
   191  apply (unfold less)
   192  apply (subst type_definition.Abs_inverse [OF type z_in_A])
   193  apply (rule z_least [OF type_definition.Rep [OF type]])
   194 done
   195 
   196 text {*
   197   As a special case, a subtype of a pcpo has a least element
   198   if the defining subset contains @{term \<bottom>}.
   199 *}
   200 
   201 theorem typedef_pcpo:
   202   fixes Abs :: "'a::pcpo \<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 UU_in_A: "\<bottom> \<in> A"
   206   shows "OFCLASS('b, pcpo_class)"
   207 by (rule typedef_pcpo_generic [OF type less UU_in_A], rule minimal)
   208 
   209 subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
   210 
   211 text {*
   212   For a sub-pcpo where @{term \<bottom>} is a member of the defining
   213   subset, @{term Rep} and @{term Abs} are both strict.
   214 *}
   215 
   216 theorem typedef_Abs_strict:
   217   assumes type: "type_definition Rep Abs A"
   218     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   219     and UU_in_A: "\<bottom> \<in> A"
   220   shows "Abs \<bottom> = \<bottom>"
   221  apply (rule UU_I, unfold less)
   222  apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
   223 done
   224 
   225 theorem typedef_Rep_strict:
   226   assumes type: "type_definition Rep Abs A"
   227     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   228     and UU_in_A: "\<bottom> \<in> A"
   229   shows "Rep \<bottom> = \<bottom>"
   230  apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
   231  apply (rule type_definition.Abs_inverse [OF type UU_in_A])
   232 done
   233 
   234 theorem typedef_Abs_defined:
   235   assumes type: "type_definition Rep Abs A"
   236     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   237     and UU_in_A: "\<bottom> \<in> A"
   238   shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
   239  apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
   240  apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
   241 done
   242 
   243 theorem typedef_Rep_defined:
   244   assumes type: "type_definition Rep Abs A"
   245     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   246     and UU_in_A: "\<bottom> \<in> A"
   247   shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
   248  apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
   249  apply (simp add: type_definition.Rep_inject [OF type])
   250 done
   251 
   252 subsection {* Proving a subtype is flat *}
   253 
   254 theorem typedef_flat:
   255   fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
   256   assumes type: "type_definition Rep Abs A"
   257     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   258     and UU_in_A: "\<bottom> \<in> A"
   259   shows "OFCLASS('b, flat_class)"
   260  apply (intro_classes)
   261  apply (unfold less)
   262  apply (simp add: type_definition.Rep_inject [OF type, symmetric])
   263  apply (simp add: typedef_Rep_strict [OF type less UU_in_A])
   264  apply (simp add: ax_flat)
   265 done
   266 
   267 subsection {* HOLCF type definition package *}
   268 
   269 use "Tools/pcpodef_package.ML"
   270 
   271 end