src/HOL/HOLCF/Cpodef.thy
author wenzelm
Thu Mar 15 22:08:53 2012 +0100 (2012-03-15)
changeset 46950 d0181abdbdac
parent 45606 b1e1508643b1
child 48891 c0eafbd55de3
permissions -rw-r--r--
declare command keywords via theory header, including strict checking outside Pure;
     1 (*  Title:      HOL/HOLCF/Cpodef.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Subtypes of pcpos *}
     6 
     7 theory Cpodef
     8 imports Adm
     9 keywords "pcpodef" "cpodef" :: thy_goal
    10 uses ("Tools/cpodef.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 setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
    21 
    22 theorem typedef_po:
    23   fixes Abs :: "'a::po \<Rightarrow> 'b::type"
    24   assumes type: "type_definition Rep Abs A"
    25     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    26   shows "OFCLASS('b, po_class)"
    27  apply (intro_classes, unfold below)
    28    apply (rule below_refl)
    29   apply (erule (1) below_trans)
    30  apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
    31  apply (erule (1) below_antisym)
    32 done
    33 
    34 setup {* Sign.add_const_constraint (@{const_name Porder.below},
    35   SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
    36 
    37 subsection {* Proving a subtype is finite *}
    38 
    39 lemma typedef_finite_UNIV:
    40   fixes Abs :: "'a::type \<Rightarrow> 'b::type"
    41   assumes type: "type_definition Rep Abs A"
    42   shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
    43 proof -
    44   assume "finite A"
    45   hence "finite (Abs ` A)" by (rule finite_imageI)
    46   thus "finite (UNIV :: 'b set)"
    47     by (simp only: type_definition.Abs_image [OF type])
    48 qed
    49 
    50 subsection {* Proving a subtype is chain-finite *}
    51 
    52 lemma ch2ch_Rep:
    53   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    54   shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
    55 unfolding chain_def below .
    56 
    57 theorem typedef_chfin:
    58   fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
    59   assumes type: "type_definition Rep Abs A"
    60     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    61   shows "OFCLASS('b, chfin_class)"
    62  apply intro_classes
    63  apply (drule ch2ch_Rep [OF below])
    64  apply (drule chfin)
    65  apply (unfold max_in_chain_def)
    66  apply (simp add: type_definition.Rep_inject [OF type])
    67 done
    68 
    69 subsection {* Proving a subtype is complete *}
    70 
    71 text {*
    72   A subtype of a cpo is itself a cpo if the ordering is
    73   defined in the standard way, and the defining subset
    74   is closed with respect to limits of chains.  A set is
    75   closed if and only if membership in the set is an
    76   admissible predicate.
    77 *}
    78 
    79 lemma typedef_is_lubI:
    80   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    81   shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
    82 unfolding is_lub_def is_ub_def below by simp
    83 
    84 lemma Abs_inverse_lub_Rep:
    85   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
    86   assumes type: "type_definition Rep Abs A"
    87     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    88     and adm:  "adm (\<lambda>x. x \<in> A)"
    89   shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
    90  apply (rule type_definition.Abs_inverse [OF type])
    91  apply (erule admD [OF adm ch2ch_Rep [OF below]])
    92  apply (rule type_definition.Rep [OF type])
    93 done
    94 
    95 theorem typedef_is_lub:
    96   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
    97   assumes type: "type_definition Rep Abs A"
    98     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    99     and adm: "adm (\<lambda>x. x \<in> A)"
   100   shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
   101 proof -
   102   assume S: "chain S"
   103   hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
   104   hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
   105   hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
   106     by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
   107   thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
   108     by (rule typedef_is_lubI [OF below])
   109 qed
   110 
   111 lemmas typedef_lub = typedef_is_lub [THEN lub_eqI]
   112 
   113 theorem typedef_cpo:
   114   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   115   assumes type: "type_definition Rep Abs A"
   116     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   117     and adm: "adm (\<lambda>x. x \<in> A)"
   118   shows "OFCLASS('b, cpo_class)"
   119 proof
   120   fix S::"nat \<Rightarrow> 'b" assume "chain S"
   121   hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
   122     by (rule typedef_is_lub [OF type below adm])
   123   thus "\<exists>x. range S <<| x" ..
   124 qed
   125 
   126 subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
   127 
   128 text {* For any sub-cpo, the @{term Rep} function is continuous. *}
   129 
   130 theorem typedef_cont_Rep:
   131   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   132   assumes type: "type_definition Rep Abs A"
   133     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   134     and adm: "adm (\<lambda>x. x \<in> A)"
   135   shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))"
   136  apply (erule cont_apply [OF _ _ cont_const])
   137  apply (rule contI)
   138  apply (simp only: typedef_lub [OF type below adm])
   139  apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
   140  apply (rule cpo_lubI)
   141  apply (erule ch2ch_Rep [OF below])
   142 done
   143 
   144 text {*
   145   For a sub-cpo, we can make the @{term Abs} function continuous
   146   only if we restrict its domain to the defining subset by
   147   composing it with another continuous function.
   148 *}
   149 
   150 theorem typedef_cont_Abs:
   151   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   152   fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
   153   assumes type: "type_definition Rep Abs A"
   154     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   155     and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
   156     and f_in_A: "\<And>x. f x \<in> A"
   157   shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
   158 unfolding cont_def is_lub_def is_ub_def ball_simps below
   159 by (simp add: type_definition.Abs_inverse [OF type f_in_A])
   160 
   161 subsection {* Proving subtype elements are compact *}
   162 
   163 theorem typedef_compact:
   164   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   165   assumes type: "type_definition Rep Abs A"
   166     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   167     and adm: "adm (\<lambda>x. x \<in> A)"
   168   shows "compact (Rep k) \<Longrightarrow> compact k"
   169 proof (unfold compact_def)
   170   have cont_Rep: "cont Rep"
   171     by (rule typedef_cont_Rep [OF type below adm cont_id])
   172   assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)"
   173   with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst)
   174   thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
   175 qed
   176 
   177 subsection {* Proving a subtype is pointed *}
   178 
   179 text {*
   180   A subtype of a cpo has a least element if and only if
   181   the defining subset has a least element.
   182 *}
   183 
   184 theorem typedef_pcpo_generic:
   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 z_in_A: "z \<in> A"
   189     and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
   190   shows "OFCLASS('b, pcpo_class)"
   191  apply (intro_classes)
   192  apply (rule_tac x="Abs z" in exI, rule allI)
   193  apply (unfold below)
   194  apply (subst type_definition.Abs_inverse [OF type z_in_A])
   195  apply (rule z_least [OF type_definition.Rep [OF type]])
   196 done
   197 
   198 text {*
   199   As a special case, a subtype of a pcpo has a least element
   200   if the defining subset contains @{term \<bottom>}.
   201 *}
   202 
   203 theorem typedef_pcpo:
   204   fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
   205   assumes type: "type_definition Rep Abs A"
   206     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   207     and bottom_in_A: "\<bottom> \<in> A"
   208   shows "OFCLASS('b, pcpo_class)"
   209 by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
   210 
   211 subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
   212 
   213 text {*
   214   For a sub-pcpo where @{term \<bottom>} is a member of the defining
   215   subset, @{term Rep} and @{term Abs} are both strict.
   216 *}
   217 
   218 theorem typedef_Abs_strict:
   219   assumes type: "type_definition Rep Abs A"
   220     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   221     and bottom_in_A: "\<bottom> \<in> A"
   222   shows "Abs \<bottom> = \<bottom>"
   223  apply (rule bottomI, unfold below)
   224  apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
   225 done
   226 
   227 theorem typedef_Rep_strict:
   228   assumes type: "type_definition Rep Abs A"
   229     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   230     and bottom_in_A: "\<bottom> \<in> A"
   231   shows "Rep \<bottom> = \<bottom>"
   232  apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
   233  apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
   234 done
   235 
   236 theorem typedef_Abs_bottom_iff:
   237   assumes type: "type_definition Rep Abs A"
   238     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   239     and bottom_in_A: "\<bottom> \<in> A"
   240   shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
   241  apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
   242  apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
   243 done
   244 
   245 theorem typedef_Rep_bottom_iff:
   246   assumes type: "type_definition Rep Abs A"
   247     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   248     and bottom_in_A: "\<bottom> \<in> A"
   249   shows "(Rep x = \<bottom>) = (x = \<bottom>)"
   250  apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
   251  apply (simp add: type_definition.Rep_inject [OF type])
   252 done
   253 
   254 subsection {* Proving a subtype is flat *}
   255 
   256 theorem typedef_flat:
   257   fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
   258   assumes type: "type_definition Rep Abs A"
   259     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   260     and bottom_in_A: "\<bottom> \<in> A"
   261   shows "OFCLASS('b, flat_class)"
   262  apply (intro_classes)
   263  apply (unfold below)
   264  apply (simp add: type_definition.Rep_inject [OF type, symmetric])
   265  apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])
   266  apply (simp add: ax_flat)
   267 done
   268 
   269 subsection {* HOLCF type definition package *}
   270 
   271 use "Tools/cpodef.ML"
   272 
   273 end