merged
authorhuffman
Sat, 27 Nov 2010 14:34:54 -0800
changeset 40773 6c12f5e24e34
parent 40772 c8b52f9e1680 (diff)
parent 40766 77a468590560 (current diff)
child 40774 0437dbc127b3
merged
src/Pure/ML-Systems/bash.ML
--- a/NEWS	Sat Nov 27 22:02:16 2010 +0100
+++ b/NEWS	Sat Nov 27 14:34:54 2010 -0800
@@ -461,6 +461,22 @@
 * Case combinators generated by the domain package for type 'foo'
 are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
 
+* Several theorems have been renamed to more accurately reflect the
+names of constants and types involved. INCOMPATIBILITY.
+  thelub_const    ~> lub_const
+  lub_const       ~> is_lub_const
+  thelubI         ~> lub_eqI
+  is_lub_lub      ~> is_lubD2
+  lubI            ~> is_lub_lub
+  unique_lub      ~> is_lub_unique
+  is_ub_lub       ~> is_lub_rangeD1
+  lub_bin_chain   ~> is_lub_bin_chain
+  thelub_Pair     ~> lub_Pair
+  lub_cprod       ~> is_lub_prod
+  thelub_cprod    ~> lub_prod
+  minimal_cprod   ~> minimal_prod
+  inst_cprod_pcpo ~> inst_prod_pcpo
+
 * Many legacy theorem names have been discontinued. INCOMPATIBILITY.
   sq_ord_less_eq_trans ~> below_eq_trans
   sq_ord_eq_less_trans ~> eq_below_trans
--- a/src/HOLCF/Bifinite.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Bifinite.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -642,7 +642,7 @@
 apply (simp add: contlub_cfun_fun)
 apply (simp add: discr_approx_def)
 apply (case_tac x, simp)
-apply (rule thelubI)
+apply (rule lub_eqI)
 apply (rule is_lubI)
 apply (rule ub_rangeI, simp)
 apply (drule ub_rangeD)
--- a/src/HOLCF/Cfun.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Cfun.thy	Sat Nov 27 14:34:54 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
@@ -209,15 +209,9 @@
 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
 by (rule cont_Rep_cfun2 [THEN cont2contlubE])
 
-lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
-by (rule cont_Rep_cfun2 [THEN contE])
-
 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
 by (rule cont_Rep_cfun1 [THEN cont2contlubE])
 
-lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
-by (rule cont_Rep_cfun1 [THEN contE])
-
 text {* monotonicity of application *}
 
 lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
@@ -264,7 +258,7 @@
 lemma contlub_LAM:
   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
     \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
-apply (simp add: thelub_cfun)
+apply (simp add: lub_cfun)
 apply (simp add: Abs_cfun_inverse2)
 apply (simp add: thelub_fun ch2ch_lambda)
 done
@@ -287,7 +281,7 @@
 by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
 
 lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
-by (rule lub_cfun [THEN thelubI])
+by (rule lub_cfun [THEN lub_eqI])
 
 subsection {* Continuity simplification procedure *}
 
@@ -370,7 +364,7 @@
 apply (rule allI)
 apply (subst contlub_cfun_fun)
 apply assumption
-apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
+apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
 done
 
 lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
@@ -484,28 +478,28 @@
 default_sort pcpo
 
 definition
-  strict :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
-  "strict = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
+  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
+  "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
 
-lemma cont_strict: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
+lemma cont_seq: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
 unfolding cont_def is_lub_def is_ub_def ball_simps
 by (simp add: lub_eq_bottom_iff)
 
-lemma strict_conv_if: "strict\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
-unfolding strict_def by (simp add: cont_strict)
+lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
+unfolding seq_def by (simp add: cont_seq)
 
-lemma strict1 [simp]: "strict\<cdot>\<bottom> = \<bottom>"
-by (simp add: strict_conv_if)
+lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
+by (simp add: seq_conv_if)
 
-lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
-by (simp add: strict_conv_if)
+lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
+by (simp add: seq_conv_if)
 
-lemma strict3 [simp]: "strict\<cdot>x\<cdot>\<bottom> = \<bottom>"
-by (simp add: strict_conv_if)
+lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
+by (simp add: seq_conv_if)
 
 definition
   strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
-  "strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))"
+  "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))"
 
 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
 unfolding strictify_def by simp
--- a/src/HOLCF/Completion.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Completion.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -55,7 +55,7 @@
 lemma lub_image_principal:
   assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
-apply (rule thelubI)
+apply (rule lub_eqI)
 apply (rule is_lub_maximal)
 apply (rule ub_imageI)
 apply (simp add: f)
@@ -100,7 +100,7 @@
   assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
   assumes S: "chain S"
   shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))"
-    and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
+    and typedef_ideal_rep_lub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
 proof -
   have 1: "ideal (\<Union>i. Rep (S i))"
     apply (rule ideal_UN)
@@ -117,7 +117,7 @@
     apply (simp add: below 2 is_ub_def, fast)
     done
   hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
-    by (rule thelubI)
+    by (rule lub_eqI)
   show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
     by (simp add: 4 2)
 qed
@@ -140,13 +140,13 @@
 subsection {* Lemmas about least upper bounds *}
 
 lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
-apply (erule exE, drule lubI)
+apply (erule exE, drule is_lub_lub)
 apply (drule is_lubD1)
 apply (erule (1) is_ubD)
 done
 
 lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
-by (erule exE, drule lubI, erule is_lub_lub)
+by (erule exE, drule is_lub_lub, erule is_lubD2)
 
 subsection {* Locale for ideal completion *}
 
@@ -154,7 +154,7 @@
   fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
   fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
   assumes ideal_rep: "\<And>x. ideal (rep x)"
-  assumes rep_contlub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
+  assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
   assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
   assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
   assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
@@ -162,8 +162,8 @@
 
 lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
 apply (frule bin_chain)
-apply (drule rep_contlub)
-apply (simp only: thelubI [OF lub_bin_chain])
+apply (drule rep_lub)
+apply (simp only: lub_eqI [OF is_lub_bin_chain])
 apply (rule subsetI, rule UN_I [where a=0], simp_all)
 done
 
@@ -215,7 +215,7 @@
 subsubsection {* Principal ideals approximate all elements *}
 
 lemma compact_principal [simp]: "compact (principal a)"
-by (rule compactI2, simp add: principal_below_iff_mem_rep rep_contlub)
+by (rule compactI2, simp add: principal_below_iff_mem_rep rep_lub)
 
 text {* Construct a chain whose lub is the same as a given ideal *}
 
@@ -285,7 +285,7 @@
   have 1: "\<forall>i. enum (X i) \<preceq> enum (X (Suc i))"
     by (simp add: X_chain)
   have 2: "x = (\<Squnion>n. principal (enum (X n)))"
-    apply (simp add: eq_iff rep_contlub 1 rep_principal)
+    apply (simp add: eq_iff rep_lub 1 rep_principal)
     apply (auto, rename_tac a)
     apply (subgoal_tac "\<exists>i. a = enum i", erule exE)
     apply (rule_tac x=i in exI, simp add: X_covers)
@@ -345,7 +345,7 @@
   have chain: "chain (\<lambda>i. f (Y i))"
     by (rule chainI, simp add: f_mono Y)
   have rep_x: "rep x = (\<Union>n. {a. a \<preceq> Y n})"
-    by (simp add: x rep_contlub Y rep_principal)
+    by (simp add: x rep_lub Y rep_principal)
   have "f ` rep x <<| (\<Squnion>n. f (Y n))"
     apply (rule is_lubI)
     apply (rule ub_imageI, rename_tac a)
@@ -375,7 +375,7 @@
      apply (rule is_ub_thelub_ex [OF lub imageI])
      apply (erule (1) subsetD [OF rep_mono])
     apply (rule is_lub_thelub_ex [OF lub ub_imageI])
-    apply (simp add: rep_contlub, clarify)
+    apply (simp add: rep_lub, clarify)
     apply (erule rev_below_trans [OF is_ub_thelub])
     apply (erule is_ub_thelub_ex [OF lub imageI])
     done
@@ -421,7 +421,7 @@
   show "ideal (Rep x)"
     using Rep [of x] by simp
   show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))"
-    using type below by (rule typedef_ideal_rep_contlub)
+    using type below by (rule typedef_ideal_rep_lub)
   show "Rep (principal a) = {b. b \<preceq> a}"
     by (simp add: principal Abs_inverse ideal_principal)
   show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y"
--- a/src/HOLCF/Cont.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Cont.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -72,7 +72,7 @@
 apply (erule contE)
 apply (erule bin_chain)
 apply (rule_tac f=f in arg_cong)
-apply (erule lub_bin_chain [THEN thelubI])
+apply (erule is_lub_bin_chain [THEN lub_eqI])
 done
 
 text {* continuity implies monotonicity *}
@@ -80,7 +80,7 @@
 lemma cont2mono: "cont f \<Longrightarrow> monofun f"
 apply (rule monofunI)
 apply (drule (1) binchain_cont)
-apply (drule_tac i=0 in is_ub_lub)
+apply (drule_tac i=0 in is_lub_rangeD1)
 apply simp
 done
 
@@ -92,7 +92,7 @@
 
 lemma cont2contlubE:
   "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
-apply (rule thelubI [symmetric])
+apply (rule lub_eqI [symmetric])
 apply (erule (1) contE)
 done
 
@@ -142,9 +142,7 @@
 text {* constant functions are continuous *}
 
 lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
-apply (rule contI)
-apply (rule lub_const)
-done
+  using is_lub_const by (rule contI)
 
 text {* application of functions is continuous *}
 
@@ -235,7 +233,7 @@
 lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
 apply (rule contI)
 apply (drule discrete_chain_const, clarify)
-apply (simp add: lub_const)
+apply (simp add: is_lub_const)
 done
 
 end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Cpodef.thy	Sat Nov 27 14:34:54 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
--- a/src/HOLCF/FOCUS/Fstream.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -225,7 +225,7 @@
 lemma fstream_lub_lemma1:
     "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
 apply (case_tac "max_in_chain i Y")
-apply  (drule (1) lub_finch1 [THEN thelubI, THEN sym])
+apply  (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
 apply  (force)
 apply (unfold max_in_chain_def)
 apply auto
@@ -254,7 +254,7 @@
 apply   (rule chainI)
 apply   (fast)
 apply  (erule chain_shift)
-apply (subst lub_const [THEN thelubI])
+apply (subst lub_const)
 apply (subst lub_range_shift)
 apply  (assumption)
 apply (simp)
--- a/src/HOLCF/FOCUS/Fstreams.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -246,7 +246,7 @@
 apply (drule fstreams_lub_lemma1, auto)
 apply (rule_tac x="j" in exI, auto)
 apply (case_tac "max_in_chain j Y")
-apply (frule lub_finch1 [THEN thelubI], auto)
+apply (frule lub_finch1 [THEN lub_eqI], auto)
 apply (rule_tac x="j" in exI)
 apply (erule subst) back back
 apply (simp add: below_prod_def sconc_mono)
@@ -266,7 +266,7 @@
 lemma lub_Pair_not_UU_lemma: 
   "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
       ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
-apply (frule thelub_cprod, clarsimp)
+apply (frule lub_prod, clarsimp)
 apply (drule chain_UU_I_inverse2, clarsimp)
 apply (case_tac "Y i", clarsimp)
 apply (case_tac "max_in_chain i Y")
@@ -298,7 +298,7 @@
 apply (drule fstreams_lub_lemma2, auto)
 apply (rule_tac x="j" in exI, auto)
 apply (case_tac "max_in_chain j Y")
-apply (frule lub_finch1 [THEN thelubI], auto)
+apply (frule lub_finch1 [THEN lub_eqI], auto)
 apply (rule_tac x="j" in exI)
 apply (erule subst) back back
 apply (simp add: sconc_mono)
@@ -312,7 +312,7 @@
 apply (rule sconc_mono)
 apply (subgoal_tac "tt ~= tta" "tta << ms")
 apply (blast intro: fstreams_chain_lemma)
-apply (frule lub_cprod [THEN thelubI], auto)
+apply (frule lub_prod, auto)
 apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
 apply (drule fstreams_mono, simp)
 apply (rule is_ub_thelub chainI)
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -37,7 +37,7 @@
 prefer 2 apply fast
 apply (unfold finite_chain_def)
 apply safe
-apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
+apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst])
 apply assumption
 apply (erule spec)
 done
--- a/src/HOLCF/Fix.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Fix.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -183,7 +183,7 @@
   hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
     by - (rule admD [OF adm'], simp, assumption)
   hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
-    by (simp add: thelub_Pair)
+    by (simp add: lub_Pair)
   hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
     by simp
   thus "P (fix\<cdot>F) (fix\<cdot>G)"
--- a/src/HOLCF/Fixrec.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Fixrec.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -105,9 +105,9 @@
 default_sort pcpo
 
 definition
-  match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
+  match_bottom :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
 where
-  "match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)"
+  "match_bottom = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
 
 definition
   match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
@@ -149,10 +149,10 @@
 where
   "match_FF = (\<Lambda> x k. If x then fail else k)"
 
-lemma match_UU_simps [simp]:
-  "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
-  "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
-by (simp_all add: match_UU_def)
+lemma match_bottom_simps [simp]:
+  "match_bottom\<cdot>\<bottom>\<cdot>k = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> match_bottom\<cdot>x\<cdot>k = fail"
+by (simp_all add: match_bottom_def)
 
 lemma match_Pair_simps [simp]:
   "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
@@ -244,7 +244,7 @@
       (@{const_name ONE}, @{const_name match_ONE}),
       (@{const_name TT}, @{const_name match_TT}),
       (@{const_name FF}, @{const_name match_FF}),
-      (@{const_name UU}, @{const_name match_UU}) ]
+      (@{const_name UU}, @{const_name match_bottom}) ]
 *}
 
 hide_const (open) succeed fail run
--- a/src/HOLCF/Fun_Cpo.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Fun_Cpo.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -80,7 +80,7 @@
 lemma thelub_fun:
   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
     \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
-by (rule lub_fun [THEN thelubI])
+by (rule lub_fun [THEN lub_eqI])
 
 instance "fun"  :: (type, cpo) cpo
 by intro_classes (rule exI, erule lub_fun)
--- a/src/HOLCF/HOLCF.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/HOLCF.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -30,5 +30,10 @@
 lemmas cont2cont_Rep_CFun = cont2cont_APP
 lemmas cont_Rep_CFun_app = cont_APP_app
 lemmas cont_Rep_CFun_app_app = cont_APP_app_app
+lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
+lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
+(*
+lemmas thelubI = lub_eqI
+*)
 
 end
--- a/src/HOLCF/IsaMakefile	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/IsaMakefile	Sat Nov 27 14:34:54 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
 
--- a/src/HOLCF/Library/List_Cpo.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Library/List_Cpo.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -141,7 +141,7 @@
   fix S :: "nat \<Rightarrow> 'a list"
   assume "chain S" thus "\<exists>x. range S <<| x"
   proof (induct rule: list_chain_induct)
-    case Nil thus ?case by (auto intro: lub_const)
+    case Nil thus ?case by (auto intro: is_lub_const)
   next
     case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
   qed
@@ -163,7 +163,7 @@
   fixes A :: "nat \<Rightarrow> 'a::cpo"
   assumes A: "chain A" and B: "chain B"
   shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
-by (intro thelubI is_lub_Cons cpo_lubI A B)
+by (intro lub_eqI is_lub_Cons cpo_lubI A B)
 
 lemma cont2cont_list_case:
   assumes f: "cont (\<lambda>x. f x)"
@@ -175,7 +175,7 @@
 apply (rule cont_apply [OF f])
 apply (rule contI)
 apply (erule list_chain_cases)
-apply (simp add: lub_const)
+apply (simp add: is_lub_const)
 apply (simp add: lub_Cons)
 apply (simp add: cont2contlubE [OF h2])
 apply (simp add: cont2contlubE [OF h3])
--- a/src/HOLCF/Library/Sum_Cpo.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Library/Sum_Cpo.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -98,10 +98,10 @@
 lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
  apply (rule is_lubI)
   apply (rule ub_rangeI)
-  apply (simp add: is_ub_lub)
+  apply (simp add: is_lub_rangeD1)
  apply (frule ub_rangeD [where i=arbitrary])
  apply (erule Inl_belowE, simp)
- apply (erule is_lub_lub)
+ apply (erule is_lubD2)
  apply (rule ub_rangeI)
  apply (drule ub_rangeD, simp)
 done
@@ -109,10 +109,10 @@
 lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
  apply (rule is_lubI)
   apply (rule ub_rangeI)
-  apply (simp add: is_ub_lub)
+  apply (simp add: is_lub_rangeD1)
  apply (frule ub_rangeD [where i=arbitrary])
  apply (erule Inr_belowE, simp)
- apply (erule is_lub_lub)
+ apply (erule is_lubD2)
  apply (rule ub_rangeI)
  apply (drule ub_rangeD, simp)
 done
--- a/src/HOLCF/One.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/One.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -54,7 +54,7 @@
 
 definition
   one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
-  "one_case = (\<Lambda> a x. strict\<cdot>x\<cdot>a)"
+  "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)"
 
 translations
   "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
--- a/src/HOLCF/Pcpo.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Pcpo.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -19,19 +19,19 @@
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
 lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
-  by (fast dest: cpo elim: lubI)
+  by (fast dest: cpo elim: is_lub_lub)
 
 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
-  by (blast dest: cpo intro: lubI)
+  by (blast dest: cpo intro: is_lub_lub)
 
 text {* Properties of the lub *}
 
 lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
-  by (blast dest: cpo intro: lubI [THEN is_ub_lub])
+  by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
 
 lemma is_lub_thelub:
   "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
-  by (blast dest: cpo intro: lubI [THEN is_lub_lub])
+  by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2])
 
 lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
   by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
@@ -70,7 +70,7 @@
 lemma maxinch_is_thelub:
   "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
 apply (rule iffI)
-apply (fast intro!: thelubI lub_finch1)
+apply (fast intro!: lub_eqI lub_finch1)
 apply (unfold max_in_chain_def)
 apply (safe intro!: below_antisym)
 apply (fast elim!: chain_mono)
--- a/src/HOLCF/Pcpodef.thy	Sat Nov 27 22:02:16 2010 +0100
+++ /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_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_thelub = typedef_lub [THEN thelubI, 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_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_thelub [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
--- a/src/HOLCF/Porder.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Porder.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -126,7 +126,7 @@
 lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x"
   unfolding is_lub_def by fast
 
-lemma is_lub_lub: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
+lemma is_lubD2: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
   unfolding is_lub_def by fast
 
 lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
@@ -137,40 +137,34 @@
 
 text {* lubs are unique *}
 
-lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
-apply (unfold is_lub_def is_ub_def)
-apply (blast intro: below_antisym)
-done
+lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
+  unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
 
 text {* technical lemmas about @{term lub} and @{term is_lub} *}
 
-lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
-apply (unfold lub_def)
-apply (rule theI)
-apply assumption
-apply (erule (1) unique_lub)
-done
+lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M"
+  unfolding lub_def by (rule theI [OF _ is_lub_unique])
 
-lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
-  by (rule unique_lub [OF lubI])
+lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l"
+  by (rule is_lub_unique [OF is_lub_lub])
 
 lemma is_lub_singleton: "{x} <<| x"
   by (simp add: is_lub_def)
 
 lemma lub_singleton [simp]: "lub {x} = x"
-  by (rule thelubI [OF is_lub_singleton])
+  by (rule is_lub_singleton [THEN lub_eqI])
 
 lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
   by (simp add: is_lub_def)
 
 lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
-  by (rule is_lub_bin [THEN thelubI])
+  by (rule is_lub_bin [THEN lub_eqI])
 
 lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x"
   by (erule is_lubI, erule (1) is_ubD)
 
 lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x"
-  by (rule is_lub_maximal [THEN thelubI])
+  by (rule is_lub_maximal [THEN lub_eqI])
 
 subsection {* Countable chains *}
 
@@ -197,7 +191,7 @@
 
 text {* technical lemmas about (least) upper bounds of chains *}
 
-lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
+lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
   by (rule is_lubD1 [THEN ub_rangeD])
 
 lemma is_ub_range_shift:
@@ -221,11 +215,11 @@
 lemma chain_const [simp]: "chain (\<lambda>i. c)"
   by (simp add: chainI)
 
-lemma lub_const: "range (\<lambda>x. c) <<| c"
+lemma is_lub_const: "range (\<lambda>x. c) <<| c"
 by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
 
-lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
-  by (rule lub_const [THEN thelubI])
+lemma lub_const [simp]: "(\<Squnion>i. c) = c"
+  by (rule is_lub_const [THEN lub_eqI])
 
 subsection {* Finite chains *}
 
@@ -324,7 +318,7 @@
   "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
   unfolding max_in_chain_def by simp
 
-lemma lub_bin_chain:
+lemma is_lub_bin_chain:
   "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
 apply (frule bin_chain)
 apply (drule bin_chainmax)
@@ -335,7 +329,7 @@
 text {* the maximal element in a chain is its lub *}
 
 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
-  by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
+  by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI)
 
 end
 
--- a/src/HOLCF/Product_Cpo.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Product_Cpo.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -111,46 +111,30 @@
 
 lemma is_lub_Pair:
   "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
-apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: is_ub_lub)
-apply (frule ub2ub_monofun [OF monofun_fst])
-apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: below_prod_def is_lub_lub)
-done
+unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
 
-lemma thelub_Pair:
+lemma lub_Pair:
   "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
-by (fast intro: thelubI is_lub_Pair elim: thelubE)
+by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
 
-lemma lub_cprod:
+lemma is_lub_prod:
   fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
   assumes S: "chain S"
   shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-proof -
-  from `chain S` have "chain (\<lambda>i. fst (S i))"
-    by (rule ch2ch_fst)
-  hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
-    by (rule cpo_lubI)
-  from `chain S` have "chain (\<lambda>i. snd (S i))"
-    by (rule ch2ch_snd)
-  hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
-    by (rule cpo_lubI)
-  show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-    using is_lub_Pair [OF 1 2] by simp
-qed
+using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
 
-lemma thelub_cprod:
+lemma lub_prod:
   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
     \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-by (rule lub_cprod [THEN thelubI])
+by (rule is_lub_prod [THEN lub_eqI])
 
 instance prod :: (cpo, cpo) cpo
 proof
   fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   assume "chain S"
   hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-    by (rule lub_cprod)
+    by (rule is_lub_prod)
   thus "\<exists>x. range S <<| x" ..
 qed
 
@@ -164,23 +148,23 @@
 
 subsection {* Product type is pointed *}
 
-lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
+lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
 by (simp add: below_prod_def)
 
 instance prod :: (pcpo, pcpo) pcpo
-by intro_classes (fast intro: minimal_cprod)
+by intro_classes (fast intro: minimal_prod)
 
-lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_cprod [THEN UU_I, symmetric])
+lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
+by (rule minimal_prod [THEN UU_I, symmetric])
 
 lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
-unfolding inst_cprod_pcpo by simp
+unfolding inst_prod_pcpo by simp
 
 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo by (rule fst_conv)
+unfolding inst_prod_pcpo by (rule fst_conv)
 
 lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
-unfolding inst_cprod_pcpo by (rule snd_conv)
+unfolding inst_prod_pcpo by (rule snd_conv)
 
 lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
 by simp
@@ -194,25 +178,25 @@
 apply (rule contI)
 apply (rule is_lub_Pair)
 apply (erule cpo_lubI)
-apply (rule lub_const)
+apply (rule is_lub_const)
 done
 
 lemma cont_pair2: "cont (\<lambda>y. (x, y))"
 apply (rule contI)
 apply (rule is_lub_Pair)
-apply (rule lub_const)
+apply (rule is_lub_const)
 apply (erule cpo_lubI)
 done
 
 lemma cont_fst: "cont fst"
 apply (rule contI)
-apply (simp add: thelub_cprod)
+apply (simp add: lub_prod)
 apply (erule cpo_lubI [OF ch2ch_fst])
 done
 
 lemma cont_snd: "cont snd"
 apply (rule contI)
-apply (simp add: thelub_cprod)
+apply (simp add: lub_prod)
 apply (erule cpo_lubI [OF ch2ch_snd])
 done
 
--- a/src/HOLCF/Sprod.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Sprod.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -37,11 +37,11 @@
 
 definition
   spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
-  "spair = (\<Lambda> a b. Abs_sprod (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b))"
+  "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))"
 
 definition
   ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
-  "ssplit = (\<Lambda> f p. strict\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
+  "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
 syntax
   "_stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
@@ -54,10 +54,10 @@
 
 subsection {* Case analysis *}
 
-lemma spair_sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> sprod"
-by (simp add: sprod_def strict_conv_if)
+lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod"
+by (simp add: sprod_def seq_conv_if)
 
-lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
+lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)"
 by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)
 
 lemmas Rep_sprod_simps =
@@ -82,16 +82,16 @@
 by (simp add: Rep_sprod_simps)
 
 lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
-by (simp add: Rep_sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps seq_conv_if)
 
 lemma spair_below_iff:
   "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
-by (simp add: Rep_sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps seq_conv_if)
 
 lemma spair_eq_iff:
   "((:a, b:) = (:c, d:)) =
     (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"
-by (simp add: Rep_sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps seq_conv_if)
 
 lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
 by simp
@@ -177,7 +177,7 @@
 by (rule compactI, simp add: ssnd_below_iff)
 
 lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
-by (rule compact_sprod, simp add: Rep_sprod_spair strict_conv_if)
+by (rule compact_sprod, simp add: Rep_sprod_spair seq_conv_if)
 
 lemma compact_spair_iff:
   "compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))"
--- a/src/HOLCF/Ssum.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Ssum.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -32,22 +32,22 @@
 
 definition
   sinl :: "'a \<rightarrow> ('a ++ 'b)" where
-  "sinl = (\<Lambda> a. Abs_ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>))"
+  "sinl = (\<Lambda> a. Abs_ssum (seq\<cdot>a\<cdot>TT, a, \<bottom>))"
 
 definition
   sinr :: "'b \<rightarrow> ('a ++ 'b)" where
-  "sinr = (\<Lambda> b. Abs_ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b))"
+  "sinr = (\<Lambda> b. Abs_ssum (seq\<cdot>b\<cdot>FF, \<bottom>, b))"
 
-lemma sinl_ssum: "(strict\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
-by (simp add: ssum_def strict_conv_if)
+lemma sinl_ssum: "(seq\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
+by (simp add: ssum_def seq_conv_if)
 
-lemma sinr_ssum: "(strict\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
-by (simp add: ssum_def strict_conv_if)
+lemma sinr_ssum: "(seq\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
+by (simp add: ssum_def seq_conv_if)
 
-lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
+lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (seq\<cdot>a\<cdot>TT, a, \<bottom>)"
 by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)
 
-lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
+lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (seq\<cdot>b\<cdot>FF, \<bottom>, b)"
 by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)
 
 lemmas Rep_ssum_simps =
@@ -60,16 +60,16 @@
 text {* Ordering *}
 
 lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
 
 lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
 
 lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
 
 lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
 
 text {* Equality *}
 
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Nov 27 14:34:54 2010 -0800
@@ -711,7 +711,7 @@
         val goal = mk_trp (mk_eq (lhs, rhs));
         val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
         val start_rules =
-            @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
+            @{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
             @ @{thms pair_collapse split_def}
             @ map_apply_thms @ map_ID_thms;
         val rules0 =
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/cpodef.ML	Sat Nov 27 14:34:54 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;
--- a/src/HOLCF/Tools/domaindef.ML	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Tools/domaindef.ML	Sat Nov 27 14:34:54 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);
--- a/src/HOLCF/Tools/pcpodef.ML	Sat Nov 27 22:02:16 2010 +0100
+++ /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,
-      lub: thm, thelub: 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,
-    lub: thm, thelub: 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 lub = make @{thm typedef_lub};
-    val thelub = make @{thm typedef_thelub};
-    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 "lub_"      name, lub        ), []),
-          ((Binding.prefix_name "thelub_"   name, thelub     ), []),
-          ((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, lub = lub, thelub = thelub, 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;
--- a/src/HOLCF/Up.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/Up.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -111,7 +111,7 @@
   proof (rule up_chain_lemma)
     assume "\<forall>i. S i = Ibottom"
     hence "range (\<lambda>i. S i) <<| Ibottom"
-      by (simp add: lub_const)
+      by (simp add: is_lub_const)
     thus ?thesis ..
   next
     fix A :: "nat \<Rightarrow> 'a"
@@ -160,7 +160,7 @@
     assume A: "\<forall>i. Iup (A i) = Y (i + k)"
     assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
     hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
-      by (simp add: thelubI contlub_cfun_arg)
+      by (simp add: lub_eqI contlub_cfun_arg)
     also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
       by (simp add: A)
     also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
@@ -223,7 +223,7 @@
   assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
   | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
 apply (rule up_chain_lemma [OF Y])
-apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI)
+apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
 done
 
 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
--- a/src/HOLCF/ex/Domain_Proofs.thy	Sat Nov 27 22:02:16 2010 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Sat Nov 27 14:34:54 2010 -0800
@@ -467,7 +467,7 @@
 lemma lub_take_lemma:
   "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
     = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
-apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms)
+apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
 apply (simp only: map_apply_thms pair_collapse)
 apply (simp only: fix_def2)
 apply (rule lub_eq)