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