# HG changeset patch
# User huffman
# Date 1290895743 28800
# Node ID c8b52f9e16805df9581a1625d7053d2454a43449
# Parent  1c6f7d4b110e85b3b10375c8938c59056efec72f
rename Pcpodef.thy to Cpodef.thy;
rename pcpodef.ML to cpodef.ML;

diff -r 1c6f7d4b110e -r c8b52f9e1680 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Sat Nov 27 13:12:10 2010 -0800
+++ b/src/HOLCF/Cfun.thy	Sat Nov 27 14:09:03 2010 -0800
@@ -6,7 +6,7 @@
 header {* The type of continuous functions *}
 
 theory Cfun
-imports Pcpodef Fun_Cpo Product_Cpo
+imports Cpodef Fun_Cpo Product_Cpo
 begin
 
 default_sort cpo
diff -r 1c6f7d4b110e -r c8b52f9e1680 src/HOLCF/Cpodef.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Cpodef.thy	Sat Nov 27 14:09:03 2010 -0800
@@ -0,0 +1,285 @@
+(*  Title:      HOLCF/Pcpodef.thy
+    Author:     Brian Huffman
+*)
+
+header {* Subtypes of pcpos *}
+
+theory Cpodef
+imports Adm
+uses ("Tools/cpodef.ML")
+begin
+
+subsection {* Proving a subtype is a partial order *}
+
+text {*
+  A subtype of a partial order is itself a partial order,
+  if the ordering is defined in the standard way.
+*}
+
+setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
+
+theorem typedef_po:
+  fixes Abs :: "'a::po \<Rightarrow> 'b::type"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  shows "OFCLASS('b, po_class)"
+ apply (intro_classes, unfold below)
+   apply (rule below_refl)
+  apply (erule (1) below_trans)
+ apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
+ apply (erule (1) below_antisym)
+done
+
+setup {* Sign.add_const_constraint (@{const_name Porder.below},
+  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
+
+subsection {* Proving a subtype is finite *}
+
+lemma typedef_finite_UNIV:
+  fixes Abs :: "'a::type \<Rightarrow> 'b::type"
+  assumes type: "type_definition Rep Abs A"
+  shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
+proof -
+  assume "finite A"
+  hence "finite (Abs ` A)" by (rule finite_imageI)
+  thus "finite (UNIV :: 'b set)"
+    by (simp only: type_definition.Abs_image [OF type])
+qed
+
+subsection {* Proving a subtype is chain-finite *}
+
+lemma ch2ch_Rep:
+  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
+unfolding chain_def below .
+
+theorem typedef_chfin:
+  fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  shows "OFCLASS('b, chfin_class)"
+ apply intro_classes
+ apply (drule ch2ch_Rep [OF below])
+ apply (drule chfin)
+ apply (unfold max_in_chain_def)
+ apply (simp add: type_definition.Rep_inject [OF type])
+done
+
+subsection {* Proving a subtype is complete *}
+
+text {*
+  A subtype of a cpo is itself a cpo if the ordering is
+  defined in the standard way, and the defining subset
+  is closed with respect to limits of chains.  A set is
+  closed if and only if membership in the set is an
+  admissible predicate.
+*}
+
+lemma typedef_is_lubI:
+  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
+unfolding is_lub_def is_ub_def below by simp
+
+lemma Abs_inverse_lub_Rep:
+  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and adm:  "adm (\<lambda>x. x \<in> A)"
+  shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
+ apply (rule type_definition.Abs_inverse [OF type])
+ apply (erule admD [OF adm ch2ch_Rep [OF below]])
+ apply (rule type_definition.Rep [OF type])
+done
+
+theorem typedef_is_lub:
+  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and adm: "adm (\<lambda>x. x \<in> A)"
+  shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
+proof -
+  assume S: "chain S"
+  hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
+  hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
+  hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
+    by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
+  thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
+    by (rule typedef_is_lubI [OF below])
+qed
+
+lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
+
+theorem typedef_cpo:
+  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and adm: "adm (\<lambda>x. x \<in> A)"
+  shows "OFCLASS('b, cpo_class)"
+proof
+  fix S::"nat \<Rightarrow> 'b" assume "chain S"
+  hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
+    by (rule typedef_is_lub [OF type below adm])
+  thus "\<exists>x. range S <<| x" ..
+qed
+
+subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
+
+text {* For any sub-cpo, the @{term Rep} function is continuous. *}
+
+theorem typedef_cont_Rep:
+  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and adm: "adm (\<lambda>x. x \<in> A)"
+  shows "cont Rep"
+ apply (rule contI)
+ apply (simp only: typedef_lub [OF type below adm])
+ apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
+ apply (rule cpo_lubI)
+ apply (erule ch2ch_Rep [OF below])
+done
+
+text {*
+  For a sub-cpo, we can make the @{term Abs} function continuous
+  only if we restrict its domain to the defining subset by
+  composing it with another continuous function.
+*}
+
+theorem typedef_cont_Abs:
+  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+  fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
+    and f_in_A: "\<And>x. f x \<in> A"
+  shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
+unfolding cont_def is_lub_def is_ub_def ball_simps below
+by (simp add: type_definition.Abs_inverse [OF type f_in_A])
+
+subsection {* Proving subtype elements are compact *}
+
+theorem typedef_compact:
+  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and adm: "adm (\<lambda>x. x \<in> A)"
+  shows "compact (Rep k) \<Longrightarrow> compact k"
+proof (unfold compact_def)
+  have cont_Rep: "cont Rep"
+    by (rule typedef_cont_Rep [OF type below adm])
+  assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
+  with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
+  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
+qed
+
+subsection {* Proving a subtype is pointed *}
+
+text {*
+  A subtype of a cpo has a least element if and only if
+  the defining subset has a least element.
+*}
+
+theorem typedef_pcpo_generic:
+  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and z_in_A: "z \<in> A"
+    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
+  shows "OFCLASS('b, pcpo_class)"
+ apply (intro_classes)
+ apply (rule_tac x="Abs z" in exI, rule allI)
+ apply (unfold below)
+ apply (subst type_definition.Abs_inverse [OF type z_in_A])
+ apply (rule z_least [OF type_definition.Rep [OF type]])
+done
+
+text {*
+  As a special case, a subtype of a pcpo has a least element
+  if the defining subset contains @{term \<bottom>}.
+*}
+
+theorem typedef_pcpo:
+  fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "OFCLASS('b, pcpo_class)"
+by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
+
+subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
+
+text {*
+  For a sub-pcpo where @{term \<bottom>} is a member of the defining
+  subset, @{term Rep} and @{term Abs} are both strict.
+*}
+
+theorem typedef_Abs_strict:
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "Abs \<bottom> = \<bottom>"
+ apply (rule UU_I, unfold below)
+ apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
+done
+
+theorem typedef_Rep_strict:
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "Rep \<bottom> = \<bottom>"
+ apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
+ apply (rule type_definition.Abs_inverse [OF type UU_in_A])
+done
+
+theorem typedef_Abs_bottom_iff:
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
+ apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
+ apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
+done
+
+theorem typedef_Rep_bottom_iff:
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "(Rep x = \<bottom>) = (x = \<bottom>)"
+ apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
+ apply (simp add: type_definition.Rep_inject [OF type])
+done
+
+theorem typedef_Abs_defined:
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
+by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
+
+theorem typedef_Rep_defined:
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
+by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
+
+subsection {* Proving a subtype is flat *}
+
+theorem typedef_flat:
+  fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
+  assumes type: "type_definition Rep Abs A"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "OFCLASS('b, flat_class)"
+ apply (intro_classes)
+ apply (unfold below)
+ apply (simp add: type_definition.Rep_inject [OF type, symmetric])
+ apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
+ apply (simp add: ax_flat)
+done
+
+subsection {* HOLCF type definition package *}
+
+use "Tools/cpodef.ML"
+
+end
diff -r 1c6f7d4b110e -r c8b52f9e1680 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sat Nov 27 13:12:10 2010 -0800
+++ b/src/HOLCF/IsaMakefile	Sat Nov 27 14:09:03 2010 -0800
@@ -43,6 +43,7 @@
   Completion.thy \
   Cont.thy \
   ConvexPD.thy \
+  Cpodef.thy \
   Cprod.thy \
   Discrete.thy \
   Deflation.thy \
@@ -56,7 +57,6 @@
   LowerPD.thy \
   Map_Functions.thy \
   One.thy \
-  Pcpodef.thy \
   Pcpo.thy \
   Plain_HOLCF.thy \
   Porder.thy \
@@ -78,9 +78,9 @@
   Tools/Domain/domain_induction.ML \
   Tools/Domain/domain_isomorphism.ML \
   Tools/Domain/domain_take_proofs.ML \
+  Tools/cpodef.ML \
   Tools/domaindef.ML \
   Tools/fixrec.ML \
-  Tools/pcpodef.ML \
   document/root.tex
 	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
 
diff -r 1c6f7d4b110e -r c8b52f9e1680 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Sat Nov 27 13:12:10 2010 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,285 +0,0 @@
-(*  Title:      HOLCF/Pcpodef.thy
-    Author:     Brian Huffman
-*)
-
-header {* Subtypes of pcpos *}
-
-theory Pcpodef
-imports Adm
-uses ("Tools/pcpodef.ML")
-begin
-
-subsection {* Proving a subtype is a partial order *}
-
-text {*
-  A subtype of a partial order is itself a partial order,
-  if the ordering is defined in the standard way.
-*}
-
-setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
-
-theorem typedef_po:
-  fixes Abs :: "'a::po \<Rightarrow> 'b::type"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-  shows "OFCLASS('b, po_class)"
- apply (intro_classes, unfold below)
-   apply (rule below_refl)
-  apply (erule (1) below_trans)
- apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
- apply (erule (1) below_antisym)
-done
-
-setup {* Sign.add_const_constraint (@{const_name Porder.below},
-  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
-
-subsection {* Proving a subtype is finite *}
-
-lemma typedef_finite_UNIV:
-  fixes Abs :: "'a::type \<Rightarrow> 'b::type"
-  assumes type: "type_definition Rep Abs A"
-  shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
-proof -
-  assume "finite A"
-  hence "finite (Abs ` A)" by (rule finite_imageI)
-  thus "finite (UNIV :: 'b set)"
-    by (simp only: type_definition.Abs_image [OF type])
-qed
-
-subsection {* Proving a subtype is chain-finite *}
-
-lemma ch2ch_Rep:
-  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-  shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
-unfolding chain_def below .
-
-theorem typedef_chfin:
-  fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-  shows "OFCLASS('b, chfin_class)"
- apply intro_classes
- apply (drule ch2ch_Rep [OF below])
- apply (drule chfin)
- apply (unfold max_in_chain_def)
- apply (simp add: type_definition.Rep_inject [OF type])
-done
-
-subsection {* Proving a subtype is complete *}
-
-text {*
-  A subtype of a cpo is itself a cpo if the ordering is
-  defined in the standard way, and the defining subset
-  is closed with respect to limits of chains.  A set is
-  closed if and only if membership in the set is an
-  admissible predicate.
-*}
-
-lemma typedef_is_lubI:
-  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-  shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
-unfolding is_lub_def is_ub_def below by simp
-
-lemma Abs_inverse_lub_Rep:
-  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and adm:  "adm (\<lambda>x. x \<in> A)"
-  shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
- apply (rule type_definition.Abs_inverse [OF type])
- apply (erule admD [OF adm ch2ch_Rep [OF below]])
- apply (rule type_definition.Rep [OF type])
-done
-
-theorem typedef_is_lub:
-  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and adm: "adm (\<lambda>x. x \<in> A)"
-  shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
-proof -
-  assume S: "chain S"
-  hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
-  hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
-  hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
-    by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
-  thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
-    by (rule typedef_is_lubI [OF below])
-qed
-
-lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
-
-theorem typedef_cpo:
-  fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and adm: "adm (\<lambda>x. x \<in> A)"
-  shows "OFCLASS('b, cpo_class)"
-proof
-  fix S::"nat \<Rightarrow> 'b" assume "chain S"
-  hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
-    by (rule typedef_is_lub [OF type below adm])
-  thus "\<exists>x. range S <<| x" ..
-qed
-
-subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
-
-text {* For any sub-cpo, the @{term Rep} function is continuous. *}
-
-theorem typedef_cont_Rep:
-  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and adm: "adm (\<lambda>x. x \<in> A)"
-  shows "cont Rep"
- apply (rule contI)
- apply (simp only: typedef_lub [OF type below adm])
- apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
- apply (rule cpo_lubI)
- apply (erule ch2ch_Rep [OF below])
-done
-
-text {*
-  For a sub-cpo, we can make the @{term Abs} function continuous
-  only if we restrict its domain to the defining subset by
-  composing it with another continuous function.
-*}
-
-theorem typedef_cont_Abs:
-  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
-  fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
-    and f_in_A: "\<And>x. f x \<in> A"
-  shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
-unfolding cont_def is_lub_def is_ub_def ball_simps below
-by (simp add: type_definition.Abs_inverse [OF type f_in_A])
-
-subsection {* Proving subtype elements are compact *}
-
-theorem typedef_compact:
-  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and adm: "adm (\<lambda>x. x \<in> A)"
-  shows "compact (Rep k) \<Longrightarrow> compact k"
-proof (unfold compact_def)
-  have cont_Rep: "cont Rep"
-    by (rule typedef_cont_Rep [OF type below adm])
-  assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
-  with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
-  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
-qed
-
-subsection {* Proving a subtype is pointed *}
-
-text {*
-  A subtype of a cpo has a least element if and only if
-  the defining subset has a least element.
-*}
-
-theorem typedef_pcpo_generic:
-  fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and z_in_A: "z \<in> A"
-    and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
-  shows "OFCLASS('b, pcpo_class)"
- apply (intro_classes)
- apply (rule_tac x="Abs z" in exI, rule allI)
- apply (unfold below)
- apply (subst type_definition.Abs_inverse [OF type z_in_A])
- apply (rule z_least [OF type_definition.Rep [OF type]])
-done
-
-text {*
-  As a special case, a subtype of a pcpo has a least element
-  if the defining subset contains @{term \<bottom>}.
-*}
-
-theorem typedef_pcpo:
-  fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "OFCLASS('b, pcpo_class)"
-by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
-
-subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
-
-text {*
-  For a sub-pcpo where @{term \<bottom>} is a member of the defining
-  subset, @{term Rep} and @{term Abs} are both strict.
-*}
-
-theorem typedef_Abs_strict:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "Abs \<bottom> = \<bottom>"
- apply (rule UU_I, unfold below)
- apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
-done
-
-theorem typedef_Rep_strict:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "Rep \<bottom> = \<bottom>"
- apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
- apply (rule type_definition.Abs_inverse [OF type UU_in_A])
-done
-
-theorem typedef_Abs_bottom_iff:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
- apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
-done
-
-theorem typedef_Rep_bottom_iff:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "(Rep x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
- apply (simp add: type_definition.Rep_inject [OF type])
-done
-
-theorem typedef_Abs_defined:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
-by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
-
-theorem typedef_Rep_defined:
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
-by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
-
-subsection {* Proving a subtype is flat *}
-
-theorem typedef_flat:
-  fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
-  assumes type: "type_definition Rep Abs A"
-    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-    and UU_in_A: "\<bottom> \<in> A"
-  shows "OFCLASS('b, flat_class)"
- apply (intro_classes)
- apply (unfold below)
- apply (simp add: type_definition.Rep_inject [OF type, symmetric])
- apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
- apply (simp add: ax_flat)
-done
-
-subsection {* HOLCF type definition package *}
-
-use "Tools/pcpodef.ML"
-
-end
diff -r 1c6f7d4b110e -r c8b52f9e1680 src/HOLCF/Tools/cpodef.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/cpodef.ML	Sat Nov 27 14:09:03 2010 -0800
@@ -0,0 +1,383 @@
+(*  Title:      HOLCF/Tools/cpodef.ML
+    Author:     Brian Huffman
+
+Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
+typedef (see also ~~/src/HOL/Tools/typedef.ML).
+*)
+
+signature CPODEF =
+sig
+  type cpo_info =
+    { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
+      is_lub: thm, lub: thm, compact: thm }
+  type pcpo_info =
+    { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
+      Rep_defined: thm, Abs_defined: thm }
+
+  val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+    term -> (binding * binding) option -> tactic -> theory ->
+    (Typedef.info * thm) * theory
+  val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+    term -> (binding * binding) option -> tactic * tactic -> theory ->
+    (Typedef.info * cpo_info) * theory
+  val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+    term -> (binding * binding) option -> tactic * tactic -> theory ->
+    (Typedef.info * cpo_info * pcpo_info) * theory
+
+  val cpodef_proof: (bool * binding)
+    * (binding * (string * sort) list * mixfix) * term
+    * (binding * binding) option -> theory -> Proof.state
+  val cpodef_proof_cmd: (bool * binding)
+    * (binding * (string * string option) list * mixfix) * string
+    * (binding * binding) option -> theory -> Proof.state
+  val pcpodef_proof: (bool * binding)
+    * (binding * (string * sort) list * mixfix) * term
+    * (binding * binding) option -> theory -> Proof.state
+  val pcpodef_proof_cmd: (bool * binding)
+    * (binding * (string * string option) list * mixfix) * string
+    * (binding * binding) option -> theory -> Proof.state
+end;
+
+structure Cpodef :> CPODEF =
+struct
+
+(** type definitions **)
+
+type cpo_info =
+  { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
+    is_lub: thm, lub: thm, compact: thm }
+
+type pcpo_info =
+  { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
+    Rep_defined: thm, Abs_defined: thm }
+
+(* building terms *)
+
+fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
+fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
+
+fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
+
+(* manipulating theorems *)
+
+fun fold_adm_mem thm NONE = thm
+  | fold_adm_mem thm (SOME set_def) =
+    let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
+    in rule OF [set_def, thm] end;
+
+fun fold_UU_mem thm NONE = thm
+  | fold_UU_mem thm (SOME set_def) =
+    let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
+    in rule OF [set_def, thm] end;
+
+(* proving class instances *)
+
+fun prove_cpo
+      (name: binding)
+      (newT: typ)
+      (Rep_name: binding, Abs_name: binding)
+      (type_definition: thm)  (* type_definition Rep Abs A *)
+      (set_def: thm option)   (* A == set *)
+      (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
+      (admissible: thm)       (* adm (%x. x : set) *)
+      (thy: theory)
+    =
+  let
+    val admissible' = fold_adm_mem admissible set_def;
+    val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
+    val (full_tname, Ts) = dest_Type newT;
+    val lhs_sorts = map (snd o dest_TFree) Ts;
+    val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
+    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
+    (* transfer thms so that they will know about the new cpo instance *)
+    val cpo_thms' = map (Thm.transfer thy) cpo_thms;
+    fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
+    val cont_Rep = make @{thm typedef_cont_Rep};
+    val cont_Abs = make @{thm typedef_cont_Abs};
+    val is_lub = make @{thm typedef_is_lub};
+    val lub = make @{thm typedef_lub};
+    val compact = make @{thm typedef_compact};
+    val (_, thy) =
+      thy
+      |> Sign.add_path (Binding.name_of name)
+      |> Global_Theory.add_thms
+        ([((Binding.prefix_name "adm_"      name, admissible'), []),
+          ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
+          ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
+          ((Binding.prefix_name "is_lub_"   name, is_lub     ), []),
+          ((Binding.prefix_name "lub_"      name, lub        ), []),
+          ((Binding.prefix_name "compact_"  name, compact    ), [])])
+      ||> Sign.parent_path;
+    val cpo_info : cpo_info =
+      { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
+        cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact };
+  in
+    (cpo_info, thy)
+  end;
+
+fun prove_pcpo
+      (name: binding)
+      (newT: typ)
+      (Rep_name: binding, Abs_name: binding)
+      (type_definition: thm)  (* type_definition Rep Abs A *)
+      (set_def: thm option)   (* A == set *)
+      (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
+      (UU_mem: thm)           (* UU : set *)
+      (thy: theory)
+    =
+  let
+    val UU_mem' = fold_UU_mem UU_mem set_def;
+    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
+    val (full_tname, Ts) = dest_Type newT;
+    val lhs_sorts = map (snd o dest_TFree) Ts;
+    val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
+    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
+    val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
+    fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
+    val Rep_strict = make @{thm typedef_Rep_strict};
+    val Abs_strict = make @{thm typedef_Abs_strict};
+    val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff};
+    val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff};
+    val Rep_defined = make @{thm typedef_Rep_defined};
+    val Abs_defined = make @{thm typedef_Abs_defined};
+    val (_, thy) =
+      thy
+      |> Sign.add_path (Binding.name_of name)
+      |> Global_Theory.add_thms
+        ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
+          ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
+          ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
+          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
+          ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
+          ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
+      ||> Sign.parent_path;
+    val pcpo_info =
+      { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
+        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
+        Rep_defined = Rep_defined, Abs_defined = Abs_defined };
+  in
+    (pcpo_info, thy)
+  end;
+
+(* prepare_cpodef *)
+
+fun declare_type_name a =
+  Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+
+fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
+  let
+    val _ = Theory.requires thy "Cpodef" "cpodefs";
+
+    (*rhs*)
+    val tmp_ctxt =
+      ProofContext.init_global thy
+      |> fold (Variable.declare_typ o TFree) raw_args;
+    val set = prep_term tmp_ctxt raw_set;
+    val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
+
+    val setT = Term.fastype_of set;
+    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
+      error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
+
+    (*lhs*)
+    val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
+    val full_tname = Sign.full_name thy tname;
+    val newT = Type (full_tname, map TFree lhs_tfrees);
+
+    val morphs = opt_morphs
+      |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
+  in
+    (newT, oldT, set, morphs)
+  end
+
+fun add_podef def opt_name typ set opt_morphs tac thy =
+  let
+    val name = the_default (#1 typ) opt_name;
+    val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
+      |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
+    val oldT = #rep_type (#1 info);
+    val newT = #abs_type (#1 info);
+    val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
+
+    val RepC = Const (Rep_name, newT --> oldT);
+    val below_eqn = Logic.mk_equals (below_const newT,
+      Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
+    val lthy3 = thy2
+      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
+    val ((_, (_, below_ldef)), lthy4) = lthy3
+      |> Specification.definition (NONE,
+          ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
+    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
+    val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
+    val thy5 = lthy4
+      |> Class.prove_instantiation_instance
+          (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
+      |> Local_Theory.exit_global;
+  in ((info, below_def), thy5) end;
+
+fun prepare_cpodef
+      (prep_term: Proof.context -> 'a -> term)
+      (def: bool)
+      (name: binding)
+      (typ: binding * (string * sort) list * mixfix)
+      (raw_set: 'a)
+      (opt_morphs: (binding * binding) option)
+      (thy: theory)
+    : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
+  let
+    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
+      prepare prep_term name typ raw_set opt_morphs thy;
+
+    val goal_nonempty =
+      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+    val goal_admissible =
+      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+
+    fun cpodef_result nonempty admissible thy =
+      let
+        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
+          |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
+        val (cpo_info, thy3) = thy2
+          |> prove_cpo name newT morphs type_definition set_def below_def admissible;
+      in
+        ((info, cpo_info), thy3)
+      end;
+  in
+    (goal_nonempty, goal_admissible, cpodef_result)
+  end
+  handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
+
+fun prepare_pcpodef
+      (prep_term: Proof.context -> 'a -> term)
+      (def: bool)
+      (name: binding)
+      (typ: binding * (string * sort) list * mixfix)
+      (raw_set: 'a)
+      (opt_morphs: (binding * binding) option)
+      (thy: theory)
+    : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
+  let
+    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
+      prepare prep_term name typ raw_set opt_morphs thy;
+
+    val goal_UU_mem =
+      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+
+    val goal_admissible =
+      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+
+    fun pcpodef_result UU_mem admissible thy =
+      let
+        val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
+        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
+          |> add_podef def (SOME name) typ set opt_morphs tac;
+        val (cpo_info, thy3) = thy2
+          |> prove_cpo name newT morphs type_definition set_def below_def admissible;
+        val (pcpo_info, thy4) = thy3
+          |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
+      in
+        ((info, cpo_info, pcpo_info), thy4)
+      end;
+  in
+    (goal_UU_mem, goal_admissible, pcpodef_result)
+  end
+  handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
+
+
+(* tactic interface *)
+
+fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+  let
+    val name = the_default (#1 typ) opt_name;
+    val (goal1, goal2, cpodef_result) =
+      prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
+    val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+    val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
+  in cpodef_result thm1 thm2 thy end;
+
+fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+  let
+    val name = the_default (#1 typ) opt_name;
+    val (goal1, goal2, pcpodef_result) =
+      prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
+    val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+    val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
+  in pcpodef_result thm1 thm2 thy end;
+
+
+(* proof interface *)
+
+local
+
+fun gen_cpodef_proof prep_term prep_constraint
+    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
+  let
+    val ctxt = ProofContext.init_global thy;
+    val args = map (apsnd (prep_constraint ctxt)) raw_args;
+    val (goal1, goal2, make_result) =
+      prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
+    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
+      | after_qed _ = raise Fail "cpodef_proof";
+  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+
+fun gen_pcpodef_proof prep_term prep_constraint
+    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
+  let
+    val ctxt = ProofContext.init_global thy;
+    val args = map (apsnd (prep_constraint ctxt)) raw_args;
+    val (goal1, goal2, make_result) =
+      prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
+    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
+      | after_qed _ = raise Fail "pcpodef_proof";
+  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+
+in
+
+fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x;
+fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x;
+
+fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x;
+fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x;
+
+end;
+
+
+
+(** outer syntax **)
+
+val typedef_proof_decl =
+  Scan.optional (Parse.$$$ "(" |--
+      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+        Parse.binding >> (fn s => (true, SOME s)))
+        --| Parse.$$$ ")") (true, NONE) --
+    (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
+    (Parse.$$$ "=" |-- Parse.term) --
+    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
+
+fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
+  (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
+    ((def, the_default t opt_name), (t, args, mx), A, morphs);
+
+val _ =
+  Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
+  Keyword.thy_goal
+    (typedef_proof_decl >>
+      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
+
+val _ =
+  Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
+  Keyword.thy_goal
+    (typedef_proof_decl >>
+      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
+
+end;
diff -r 1c6f7d4b110e -r c8b52f9e1680 src/HOLCF/Tools/domaindef.ML
--- a/src/HOLCF/Tools/domaindef.ML	Sat Nov 27 13:12:10 2010 -0800
+++ b/src/HOLCF/Tools/domaindef.ML	Sat Nov 27 14:09:03 2010 -0800
@@ -19,7 +19,7 @@
 
   val add_domaindef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> theory ->
-    (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory
+    (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory
 
   val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
     * (binding * binding) option -> theory -> theory
@@ -86,7 +86,7 @@
       (raw_defl: 'a)
       (opt_morphs: (binding * binding) option)
       (thy: theory)
-    : (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory =
+    : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
   let
     val _ = Theory.requires thy "Domain" "domaindefs";
 
@@ -118,7 +118,7 @@
     val tac1 = rtac @{thm defl_set_bottom} 1;
     val tac2 = rtac @{thm adm_defl_set} 1;
     val ((info, cpo_info, pcpo_info), thy) = thy
-      |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
+      |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
 
     (*definitions*)
     val Rep_const = Const (#Rep_name (#1 info), newT --> udomT);
diff -r 1c6f7d4b110e -r c8b52f9e1680 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Sat Nov 27 13:12:10 2010 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,383 +0,0 @@
-(*  Title:      HOLCF/Tools/pcpodef.ML
-    Author:     Brian Huffman
-
-Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef (see also ~~/src/HOL/Tools/typedef.ML).
-*)
-
-signature PCPODEF =
-sig
-  type cpo_info =
-    { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
-      is_lub: thm, lub: thm, compact: thm }
-  type pcpo_info =
-    { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
-      Rep_defined: thm, Abs_defined: thm }
-
-  val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> tactic -> theory ->
-    (Typedef.info * thm) * theory
-  val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> tactic * tactic -> theory ->
-    (Typedef.info * cpo_info) * theory
-  val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
-    term -> (binding * binding) option -> tactic * tactic -> theory ->
-    (Typedef.info * cpo_info * pcpo_info) * theory
-
-  val cpodef_proof: (bool * binding)
-    * (binding * (string * sort) list * mixfix) * term
-    * (binding * binding) option -> theory -> Proof.state
-  val cpodef_proof_cmd: (bool * binding)
-    * (binding * (string * string option) list * mixfix) * string
-    * (binding * binding) option -> theory -> Proof.state
-  val pcpodef_proof: (bool * binding)
-    * (binding * (string * sort) list * mixfix) * term
-    * (binding * binding) option -> theory -> Proof.state
-  val pcpodef_proof_cmd: (bool * binding)
-    * (binding * (string * string option) list * mixfix) * string
-    * (binding * binding) option -> theory -> Proof.state
-end;
-
-structure Pcpodef :> PCPODEF =
-struct
-
-(** type definitions **)
-
-type cpo_info =
-  { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
-    is_lub: thm, lub: thm, compact: thm }
-
-type pcpo_info =
-  { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
-    Rep_defined: thm, Abs_defined: thm }
-
-(* building terms *)
-
-fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
-
-fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
-
-(* manipulating theorems *)
-
-fun fold_adm_mem thm NONE = thm
-  | fold_adm_mem thm (SOME set_def) =
-    let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
-    in rule OF [set_def, thm] end;
-
-fun fold_UU_mem thm NONE = thm
-  | fold_UU_mem thm (SOME set_def) =
-    let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
-    in rule OF [set_def, thm] end;
-
-(* proving class instances *)
-
-fun prove_cpo
-      (name: binding)
-      (newT: typ)
-      (Rep_name: binding, Abs_name: binding)
-      (type_definition: thm)  (* type_definition Rep Abs A *)
-      (set_def: thm option)   (* A == set *)
-      (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
-      (admissible: thm)       (* adm (%x. x : set) *)
-      (thy: theory)
-    =
-  let
-    val admissible' = fold_adm_mem admissible set_def;
-    val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
-    val (full_tname, Ts) = dest_Type newT;
-    val lhs_sorts = map (snd o dest_TFree) Ts;
-    val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
-    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
-    (* transfer thms so that they will know about the new cpo instance *)
-    val cpo_thms' = map (Thm.transfer thy) cpo_thms;
-    fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
-    val cont_Rep = make @{thm typedef_cont_Rep};
-    val cont_Abs = make @{thm typedef_cont_Abs};
-    val is_lub = make @{thm typedef_is_lub};
-    val lub = make @{thm typedef_lub};
-    val compact = make @{thm typedef_compact};
-    val (_, thy) =
-      thy
-      |> Sign.add_path (Binding.name_of name)
-      |> Global_Theory.add_thms
-        ([((Binding.prefix_name "adm_"      name, admissible'), []),
-          ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
-          ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
-          ((Binding.prefix_name "is_lub_"   name, is_lub     ), []),
-          ((Binding.prefix_name "lub_"      name, lub        ), []),
-          ((Binding.prefix_name "compact_"  name, compact    ), [])])
-      ||> Sign.parent_path;
-    val cpo_info : cpo_info =
-      { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
-        cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact };
-  in
-    (cpo_info, thy)
-  end;
-
-fun prove_pcpo
-      (name: binding)
-      (newT: typ)
-      (Rep_name: binding, Abs_name: binding)
-      (type_definition: thm)  (* type_definition Rep Abs A *)
-      (set_def: thm option)   (* A == set *)
-      (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
-      (UU_mem: thm)           (* UU : set *)
-      (thy: theory)
-    =
-  let
-    val UU_mem' = fold_UU_mem UU_mem set_def;
-    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
-    val (full_tname, Ts) = dest_Type newT;
-    val lhs_sorts = map (snd o dest_TFree) Ts;
-    val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
-    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
-    val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
-    fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
-    val Rep_strict = make @{thm typedef_Rep_strict};
-    val Abs_strict = make @{thm typedef_Abs_strict};
-    val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff};
-    val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff};
-    val Rep_defined = make @{thm typedef_Rep_defined};
-    val Abs_defined = make @{thm typedef_Abs_defined};
-    val (_, thy) =
-      thy
-      |> Sign.add_path (Binding.name_of name)
-      |> Global_Theory.add_thms
-        ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
-          ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
-          ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
-          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
-          ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
-          ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
-      ||> Sign.parent_path;
-    val pcpo_info =
-      { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
-        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
-        Rep_defined = Rep_defined, Abs_defined = Abs_defined };
-  in
-    (pcpo_info, thy)
-  end;
-
-(* prepare_cpodef *)
-
-fun declare_type_name a =
-  Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-
-fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
-  let
-    val _ = Theory.requires thy "Pcpodef" "pcpodefs";
-
-    (*rhs*)
-    val tmp_ctxt =
-      ProofContext.init_global thy
-      |> fold (Variable.declare_typ o TFree) raw_args;
-    val set = prep_term tmp_ctxt raw_set;
-    val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
-
-    val setT = Term.fastype_of set;
-    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
-      error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
-
-    (*lhs*)
-    val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
-    val full_tname = Sign.full_name thy tname;
-    val newT = Type (full_tname, map TFree lhs_tfrees);
-
-    val morphs = opt_morphs
-      |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
-  in
-    (newT, oldT, set, morphs)
-  end
-
-fun add_podef def opt_name typ set opt_morphs tac thy =
-  let
-    val name = the_default (#1 typ) opt_name;
-    val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
-      |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
-    val oldT = #rep_type (#1 info);
-    val newT = #abs_type (#1 info);
-    val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
-
-    val RepC = Const (Rep_name, newT --> oldT);
-    val below_eqn = Logic.mk_equals (below_const newT,
-      Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
-    val lthy3 = thy2
-      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
-    val ((_, (_, below_ldef)), lthy4) = lthy3
-      |> Specification.definition (NONE,
-          ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
-    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
-    val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
-    val thy5 = lthy4
-      |> Class.prove_instantiation_instance
-          (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
-      |> Local_Theory.exit_global;
-  in ((info, below_def), thy5) end;
-
-fun prepare_cpodef
-      (prep_term: Proof.context -> 'a -> term)
-      (def: bool)
-      (name: binding)
-      (typ: binding * (string * sort) list * mixfix)
-      (raw_set: 'a)
-      (opt_morphs: (binding * binding) option)
-      (thy: theory)
-    : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
-  let
-    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
-      prepare prep_term name typ raw_set opt_morphs thy;
-
-    val goal_nonempty =
-      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
-    val goal_admissible =
-      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
-
-    fun cpodef_result nonempty admissible thy =
-      let
-        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
-          |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
-        val (cpo_info, thy3) = thy2
-          |> prove_cpo name newT morphs type_definition set_def below_def admissible;
-      in
-        ((info, cpo_info), thy3)
-      end;
-  in
-    (goal_nonempty, goal_admissible, cpodef_result)
-  end
-  handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
-
-fun prepare_pcpodef
-      (prep_term: Proof.context -> 'a -> term)
-      (def: bool)
-      (name: binding)
-      (typ: binding * (string * sort) list * mixfix)
-      (raw_set: 'a)
-      (opt_morphs: (binding * binding) option)
-      (thy: theory)
-    : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
-  let
-    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
-      prepare prep_term name typ raw_set opt_morphs thy;
-
-    val goal_UU_mem =
-      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
-
-    val goal_admissible =
-      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
-
-    fun pcpodef_result UU_mem admissible thy =
-      let
-        val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
-        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
-          |> add_podef def (SOME name) typ set opt_morphs tac;
-        val (cpo_info, thy3) = thy2
-          |> prove_cpo name newT morphs type_definition set_def below_def admissible;
-        val (pcpo_info, thy4) = thy3
-          |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
-      in
-        ((info, cpo_info, pcpo_info), thy4)
-      end;
-  in
-    (goal_UU_mem, goal_admissible, pcpodef_result)
-  end
-  handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
-
-
-(* tactic interface *)
-
-fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
-  let
-    val name = the_default (#1 typ) opt_name;
-    val (goal1, goal2, cpodef_result) =
-      prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
-    val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
-      handle ERROR msg => cat_error msg
-        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
-    val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
-      handle ERROR msg => cat_error msg
-        ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
-  in cpodef_result thm1 thm2 thy end;
-
-fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
-  let
-    val name = the_default (#1 typ) opt_name;
-    val (goal1, goal2, pcpodef_result) =
-      prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
-    val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
-      handle ERROR msg => cat_error msg
-        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
-    val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
-      handle ERROR msg => cat_error msg
-        ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
-  in pcpodef_result thm1 thm2 thy end;
-
-
-(* proof interface *)
-
-local
-
-fun gen_cpodef_proof prep_term prep_constraint
-    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
-  let
-    val ctxt = ProofContext.init_global thy;
-    val args = map (apsnd (prep_constraint ctxt)) raw_args;
-    val (goal1, goal2, make_result) =
-      prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
-    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
-      | after_qed _ = raise Fail "cpodef_proof";
-  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
-
-fun gen_pcpodef_proof prep_term prep_constraint
-    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
-  let
-    val ctxt = ProofContext.init_global thy;
-    val args = map (apsnd (prep_constraint ctxt)) raw_args;
-    val (goal1, goal2, make_result) =
-      prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
-    fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2)
-      | after_qed _ = raise Fail "pcpodef_proof";
-  in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
-
-in
-
-fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x;
-fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x;
-
-fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x;
-fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x;
-
-end;
-
-
-
-(** outer syntax **)
-
-val typedef_proof_decl =
-  Scan.optional (Parse.$$$ "(" |--
-      ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
-        Parse.binding >> (fn s => (true, SOME s)))
-        --| Parse.$$$ ")") (true, NONE) --
-    (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
-    (Parse.$$$ "=" |-- Parse.term) --
-    Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
-
-fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
-  (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
-    ((def, the_default t opt_name), (t, args, mx), A, morphs);
-
-val _ =
-  Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
-  Keyword.thy_goal
-    (typedef_proof_decl >>
-      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
-
-val _ =
-  Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
-  Keyword.thy_goal
-    (typedef_proof_decl >>
-      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
-
-end;