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
```