merged
authorhuffman
Sun, 24 Oct 2010 15:11:24 -0700
changeset 40099 0fb7891f0c7c
parent 40098 9dbb01456031 (diff)
parent 40079 07445603208a (current diff)
child 40105 0d579da1902a
child 40212 20df78048db5
merged
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOLCF/Bifinite.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Bifinite.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -5,7 +5,7 @@
 header {* Bifinite domains *}
 
 theory Bifinite
-imports Algebraic Cprod Sprod Ssum Up Lift One Tr
+imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable
 begin
 
 subsection {* Class of bifinite domains *}
--- a/src/HOLCF/Cfun.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Cfun.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -95,12 +95,6 @@
 lemma UU_CFun: "\<bottom> \<in> CFun"
 by (simp add: CFun_def inst_fun_pcpo)
 
-instance cfun :: (finite_po, finite_po) finite_po
-by (rule typedef_finite_po [OF type_definition_CFun])
-
-instance cfun :: (finite_po, chfin) chfin
-by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
-
 instance cfun :: (cpo, discrete_cpo) discrete_cpo
 by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
 
@@ -550,7 +544,10 @@
 lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
 by (simp add: strict_conv_if)
 
- definition
+lemma strict3 [simp]: "strict\<cdot>x\<cdot>\<bottom> = \<bottom>"
+by (simp add: strict_conv_if)
+
+definition
   strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
   "strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))"
 
--- a/src/HOLCF/Discrete.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Discrete.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -44,22 +44,6 @@
  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
 by (fast elim: discr_chain0)
 
-instance discr :: (finite) finite_po
-proof
-  have "finite (Discr ` (UNIV :: 'a set))"
-    by (rule finite_imageI [OF finite])
-  also have "(Discr ` (UNIV :: 'a set)) = UNIV"
-    by (auto, case_tac x, auto)
-  finally show "finite (UNIV :: 'a discr set)" .
-qed
-
-instance discr :: (type) chfin
-apply intro_classes
-apply (rule_tac x=0 in exI)
-apply (unfold max_in_chain_def)
-apply (clarify, erule discr_chain0 [symmetric])
-done
-
 subsection {* \emph{undiscr} *}
 
 definition
--- a/src/HOLCF/FOCUS/Fstream.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -42,11 +42,7 @@
 
 
 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
-apply (rule flat_eq [THEN iffD1, symmetric])
-apply (rule Def_not_UU)
-apply (drule antisym_less_inverse)
-apply (erule (1) conjunct2 [THEN trans_less])
-done
+by simp
 
 
 section "fscons"
--- a/src/HOLCF/Fun_Cpo.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Fun_Cpo.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -110,26 +110,6 @@
   from Yij Yik show "Y j = Y k" by auto
 qed
 
-instance "fun" :: (finite, chfin) chfin
-proof
-  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
-  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
-  assume "chain Y"
-  hence "\<And>x. chain (\<lambda>i. Y i x)"
-    by (rule ch2ch_fun)
-  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
-    by (rule chfin)
-  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
-    by (rule LeastI_ex)
-  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
-    by (rule maxinch_mono [OF _ Max_ge], simp_all)
-  hence "max_in_chain (Max (range ?n)) Y"
-    by (rule maxinch2maxinch_lambda)
-  thus "\<exists>n. max_in_chain n Y" ..
-qed
-
-instance "fun" :: (finite, finite_po) finite_po ..
-
 instance "fun" :: (type, discrete_cpo) discrete_cpo
 proof
   fix f g :: "'a \<Rightarrow> 'b"
--- a/src/HOLCF/Library/Sum_Cpo.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Library/Sum_Cpo.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -213,8 +213,6 @@
 apply (case_tac "\<Squnion>i. Y i", simp_all)
 done
 
-instance sum :: (finite_po, finite_po) finite_po ..
-
 instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
 by intro_classes (simp add: below_sum_def split: sum.split)
 
--- a/src/HOLCF/Lift.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Lift.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -5,17 +5,14 @@
 header {* Lifting types of class type to flat pcpo's *}
 
 theory Lift
-imports Discrete Up Countable
+imports Discrete Up
 begin
 
 default_sort type
 
-pcpodef 'a lift = "UNIV :: 'a discr u set"
+pcpodef (open) 'a lift = "UNIV :: 'a discr u set"
 by simp_all
 
-instance lift :: (finite) finite_po
-by (rule typedef_finite_po [OF type_definition_lift])
-
 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
 
 definition
@@ -33,7 +30,7 @@
 done
 
 rep_datatype "\<bottom>\<Colon>'a lift" Def
-  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
+  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
 
 lemmas lift_distinct1 = lift.distinct(1)
 lemmas lift_distinct2 = lift.distinct(2)
@@ -65,7 +62,7 @@
   by simp
 
 lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
-by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
+by (simp add: below_lift_def Def_def Abs_lift_inverse)
 
 lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
 by (induct y, simp, simp add: Def_below_Def)
@@ -80,6 +77,18 @@
     by (induct x) auto
 qed
 
+subsection {* Continuity of @{const lift_case} *}
+
+lemma lift_case_eq: "lift_case \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
+apply (induct x, unfold lift.cases)
+apply (simp add: Rep_lift_strict)
+apply (simp add: Def_def Abs_lift_inverse)
+done
+
+lemma cont2cont_lift_case [simp]:
+  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
+unfolding lift_case_eq by (simp add: cont_Rep_lift [THEN cont_compose])
+
 subsection {* Further operations *}
 
 definition
@@ -90,59 +99,14 @@
   flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
   "flift2 f = (FLIFT x. Def (f x))"
 
-subsection {* Continuity Proofs for flift1, flift2 *}
-
-text {* Need the instance of @{text flat}. *}
-
-lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)"
-apply (induct x)
-apply simp
-apply simp
-apply (rule cont_id [THEN cont2cont_fun])
-done
-
-lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
-apply (rule flatdom_strict2cont)
-apply simp
-done
-
-lemma cont_flift1: "cont flift1"
-unfolding flift1_def
-apply (rule cont2cont_LAM)
-apply (rule cont_lift_case2)
-apply (rule cont_lift_case1)
-done
-
-lemma FLIFT_mono:
-  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
-apply (rule monofunE [where f=flift1])
-apply (rule cont2mono [OF cont_flift1])
-apply (simp add: fun_below_iff)
-done
-
-lemma cont2cont_flift1 [simp, cont2cont]:
-  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
-apply (rule cont_flift1 [THEN cont_compose])
-apply simp
-done
-
-lemma cont2cont_lift_case [simp]:
-  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
-apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
-apply (simp add: flift1_def cont_lift_case2)
-apply simp
-done
-
-text {* rewrites for @{term flift1}, @{term flift2} *}
-
 lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
-by (simp add: flift1_def cont_lift_case2)
+by (simp add: flift1_def)
 
 lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
 by (simp add: flift2_def)
 
 lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
-by (simp add: flift1_def cont_lift_case2)
+by (simp add: flift1_def)
 
 lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
 by (simp add: flift2_def)
@@ -153,4 +117,12 @@
 lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
 by (cases x, simp_all)
 
+lemma FLIFT_mono:
+  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
+by (rule cfun_belowI, case_tac x, simp_all)
+
+lemma cont2cont_flift1 [simp, cont2cont]:
+  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
+by (simp add: flift1_def cont2cont_LAM)
+
 end
--- a/src/HOLCF/Pcpo.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Pcpo.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -262,18 +262,6 @@
 
 end
 
-class finite_po = finite + po
-begin
-
-subclass chfin
-apply default
-apply (drule finite_range_imp_finch)
-apply (rule finite)
-apply (simp add: finite_chain_def)
-done
-
-end
-
 class flat = pcpo +
   assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
 begin
@@ -299,7 +287,7 @@
 
 end
 
-text {* Discrete cpos *}
+subsection {* Discrete cpos *}
 
 class discrete_cpo = below +
   assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
@@ -320,14 +308,14 @@
   thus "S i = S 0" by (rule sym)
 qed
 
-subclass cpo
+subclass chfin
 proof
   fix S :: "nat \<Rightarrow> 'a"
   assume S: "chain S"
-  hence "\<exists>x. S = (\<lambda>i. x)"
-    by (rule discrete_chain_const)
-  thus "\<exists>x. range S <<| x"
-    by (fast intro: lub_const)
+  hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const)
+  hence "max_in_chain 0 S"
+    unfolding max_in_chain_def by auto
+  thus "\<exists>i. max_in_chain i S" ..
 qed
 
 end
--- a/src/HOLCF/Pcpodef.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Pcpodef.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -46,15 +46,6 @@
     by (simp only: type_definition.Abs_image [OF type])
 qed
 
-theorem typedef_finite_po:
-  fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po"
-  assumes type: "type_definition Rep Abs A"
-  shows "OFCLASS('b, finite_po_class)"
- apply (intro_classes)
- apply (rule typedef_finite_UNIV [OF type])
- apply (rule finite)
-done
-
 subsection {* Proving a subtype is chain-finite *}
 
 lemma ch2ch_Rep:
--- a/src/HOLCF/Product_Cpo.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Product_Cpo.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -12,19 +12,16 @@
 
 subsection {* Unit type is a pcpo *}
 
-instantiation unit :: below
+instantiation unit :: discrete_cpo
 begin
 
 definition
   below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
 
-instance ..
-end
+instance proof
+qed simp
 
-instance unit :: discrete_cpo
-by intro_classes simp
-
-instance unit :: finite_po ..
+end
 
 instance unit :: pcpo
 by intro_classes simp
@@ -157,8 +154,6 @@
   thus "\<exists>x. range S <<| x" ..
 qed
 
-instance prod :: (finite_po, finite_po) finite_po ..
-
 instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
 proof
   fix x y :: "'a \<times> 'b"
--- a/src/HOLCF/Sprod.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Sprod.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -12,37 +12,31 @@
 
 subsection {* Definition of strict product type *}
 
-pcpodef (Sprod)  ('a, 'b) sprod (infixr "**" 20) =
+pcpodef ('a, 'b) sprod (infixr "**" 20) =
         "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 by simp_all
 
-instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
-by (rule typedef_finite_po [OF type_definition_Sprod])
-
 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
+by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])
 
 type_notation (xsymbols)
   sprod  ("(_ \<otimes>/ _)" [21,20] 20)
 type_notation (HTML output)
   sprod  ("(_ \<otimes>/ _)" [21,20] 20)
 
-lemma spair_lemma: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> Sprod"
-by (simp add: Sprod_def strict_conv_if)
-
 subsection {* Definitions of constants *}
 
 definition
   sfst :: "('a ** 'b) \<rightarrow> 'a" where
-  "sfst = (\<Lambda> p. fst (Rep_Sprod p))"
+  "sfst = (\<Lambda> p. fst (Rep_sprod p))"
 
 definition
   ssnd :: "('a ** 'b) \<rightarrow> 'b" where
-  "ssnd = (\<Lambda> p. snd (Rep_Sprod p))"
+  "ssnd = (\<Lambda> p. snd (Rep_sprod p))"
 
 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 (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b))"
 
 definition
   ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
@@ -59,28 +53,20 @@
 
 subsection {* Case analysis *}
 
-lemma Rep_Sprod_spair:
-  "Rep_Sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
-unfolding spair_def
-by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
-
-lemmas Rep_Sprod_simps =
-  Rep_Sprod_inject [symmetric] below_Sprod_def
-  Rep_Sprod_strict Rep_Sprod_spair
+lemma spair_sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> sprod"
+by (simp add: sprod_def strict_conv_if)
 
-lemma Exh_Sprod:
-  "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
-apply (insert Rep_Sprod [of z])
-apply (simp add: Rep_Sprod_simps Pair_fst_snd_eq)
-apply (simp add: Sprod_def)
-apply (erule disjE, simp)
-apply (simp add: strict_conv_if)
-apply fast
-done
+lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
+by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)
+
+lemmas Rep_sprod_simps =
+  Rep_sprod_inject [symmetric] below_sprod_def
+  Pair_fst_snd_eq below_prod_def
+  Rep_sprod_strict Rep_sprod_spair
 
 lemma sprodE [case_names bottom spair, cases type: sprod]:
-  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-using Exh_Sprod [of p] by auto
+  obtains "p = \<bottom>" | x y where "p = (:x, y:)" and "x \<noteq> \<bottom>" and "y \<noteq> \<bottom>"
+using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps)
 
 lemma sprod_induct [case_names bottom spair, induct type: sprod]:
   "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
@@ -89,22 +75,22 @@
 subsection {* Properties of \emph{spair} *}
 
 lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps)
 
 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps)
 
 lemma spair_strict_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 strict_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 strict_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 strict_conv_if)
 
 lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
 by simp
@@ -118,6 +104,10 @@
 lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
 by simp
 
+lemma spair_below:
+  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
+by (simp add: spair_below_iff)
+
 lemma spair_eq:
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)"
 by (simp add: spair_eq_iff)
@@ -135,16 +125,16 @@
 subsection {* Properties of \emph{sfst} and \emph{ssnd} *}
 
 lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
-by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict)
+by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict)
 
 lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
-by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_strict)
+by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict)
 
 lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
-by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair)
+by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair)
 
 lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
-by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
+by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)
 
 lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
 by (cases p, simp_all)
@@ -158,24 +148,15 @@
 lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
 by simp
 
-lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
+lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
 by (cases p, simp_all)
 
 lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
-apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
-apply (simp only: below_prod_def)
-done
+by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod)
 
 lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
 by (auto simp add: po_eq_conv below_sprod)
 
-lemma spair_below:
-  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
-apply (cases "a = \<bottom>", simp)
-apply (cases "b = \<bottom>", simp)
-apply (simp add: below_sprod)
-done
-
 lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
 apply (simp add: below_sprod)
@@ -195,7 +176,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 strict_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	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Ssum.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -12,17 +12,14 @@
 
 subsection {* Definition of strict sum type *}
 
-pcpodef (Ssum)  ('a, 'b) ssum (infixr "++" 10) = 
-  "{p :: tr \<times> ('a \<times> 'b).
-    (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
-    (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
+pcpodef ('a, 'b) ssum (infixr "++" 10) = 
+  "{p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
+    (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
+    (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>) }"
 by simp_all
 
-instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
-by (rule typedef_finite_po [OF type_definition_Ssum])
-
 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
+by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])
 
 type_notation (xsymbols)
   ssum  ("(_ \<oplus>/ _)" [21, 20] 20)
@@ -34,45 +31,44 @@
 
 definition
   sinl :: "'a \<rightarrow> ('a ++ 'b)" where
-  "sinl = (\<Lambda> a. Abs_Ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>))"
+  "sinl = (\<Lambda> a. Abs_ssum (strict\<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 (strict\<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: "(strict\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
+by (simp add: ssum_def strict_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: "(strict\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
+by (simp add: ssum_def strict_conv_if)
 
-lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
-by (unfold sinl_def, simp add: cont_Abs_Ssum sinl_Ssum)
-
-lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
-by (unfold sinr_def, simp add: cont_Abs_Ssum sinr_Ssum)
+lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
+by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)
 
-lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
-by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum)
+lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
+by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)
 
-lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
-by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
+lemmas Rep_ssum_simps =
+  Rep_ssum_inject [symmetric] below_ssum_def
+  Pair_fst_snd_eq below_prod_def
+  Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
 
 subsection {* Properties of \emph{sinl} and \emph{sinr} *}
 
 text {* Ordering *}
 
 lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl strict_conv_if)
+by (simp add: Rep_ssum_simps strict_conv_if)
 
 lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: below_Ssum_def Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_ssum_simps strict_conv_if)
 
 lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_ssum_simps strict_conv_if)
 
 lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_ssum_simps strict_conv_if)
 
 text {* Equality *}
 
@@ -97,30 +93,30 @@
 text {* Strictness *}
 
 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinl_Abs_Ssum Abs_Ssum_strict)
+by (simp add: Rep_ssum_simps)
 
 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinr_Abs_Ssum Abs_Ssum_strict)
+by (simp add: Rep_ssum_simps)
 
 lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
-by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
+using sinl_eq [of "x" "\<bottom>"] by simp
 
 lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
-by (cut_tac sinr_eq [of "x" "\<bottom>"], simp)
+using sinr_eq [of "x" "\<bottom>"] by simp
 
-lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
+lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
 by simp
 
-lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
+lemma sinr_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
 by simp
 
 text {* Compactness *}
 
 lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinl strict_conv_if)
+by (rule compact_ssum, simp add: Rep_ssum_sinl)
 
 lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinr strict_conv_if)
+by (rule compact_ssum, simp add: Rep_ssum_sinr)
 
 lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def
@@ -138,24 +134,11 @@
 
 subsection {* Case analysis *}
 
-lemma Exh_Ssum: 
-  "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)"
-apply (induct z rule: Abs_Ssum_induct)
-apply (case_tac y, rename_tac t a b)
-apply (case_tac t rule: trE)
-apply (rule disjI1)
-apply (simp add: Ssum_def Abs_Ssum_strict)
-apply (rule disjI2, rule disjI1, rule_tac x=a in exI)
-apply (simp add: sinl_Abs_Ssum Ssum_def)
-apply (rule disjI2, rule disjI2, rule_tac x=b in exI)
-apply (simp add: sinr_Abs_Ssum Ssum_def)
-done
-
 lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:
-  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
-   \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
-   \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-using Exh_Ssum [of p] by auto
+  obtains "p = \<bottom>"
+  | x where "p = sinl\<cdot>x" and "x \<noteq> \<bottom>"
+  | y where "p = sinr\<cdot>y" and "y \<noteq> \<bottom>"
+using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps)
 
 lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
   "\<lbrakk>P \<bottom>;
@@ -177,7 +160,7 @@
 
 definition
   sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
-  "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_Ssum s))"
+  "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_ssum s))"
 
 translations
   "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
@@ -187,17 +170,17 @@
   "\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
 
 lemma beta_sscase:
-  "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_Ssum s)"
-unfolding sscase_def by (simp add: cont_Rep_Ssum [THEN cont_compose])
+  "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_ssum s)"
+unfolding sscase_def by (simp add: cont_Rep_ssum [THEN cont_compose])
 
 lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
-unfolding beta_sscase by (simp add: Rep_Ssum_strict)
+unfolding beta_sscase by (simp add: Rep_ssum_strict)
 
 lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>x"
-unfolding beta_sscase by (simp add: Rep_Ssum_sinl)
+unfolding beta_sscase by (simp add: Rep_ssum_sinl)
 
 lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<cdot>y"
-unfolding beta_sscase by (simp add: Rep_Ssum_sinr)
+unfolding beta_sscase by (simp add: Rep_ssum_sinr)
 
 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
 by (cases z, simp_all)
--- a/src/HOLCF/Tools/Domain/domain.ML	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain.ML	Sun Oct 24 15:11:24 2010 -0700
@@ -8,25 +8,21 @@
 signature DOMAIN =
 sig
   val add_domain_cmd:
-      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * string) list * mixfix) list) list
       -> theory -> theory
 
   val add_domain:
-      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * typ) list * mixfix) list) list
       -> theory -> theory
 
   val add_new_domain_cmd:
-      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * string) list * mixfix) list) list
       -> theory -> theory
 
   val add_new_domain:
-      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * typ) list * mixfix) list) list
       -> theory -> theory
@@ -50,7 +46,6 @@
     (prep_typ : theory -> (string * sort) list -> 'a -> typ)
     (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
     (arg_sort : bool -> sort)
-    (comp_dbind : binding)
     (raw_specs : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
     (thy : theory) =
@@ -172,7 +167,7 @@
              (dbinds ~~ rhss ~~ iso_infos);
 
     val (take_rews, thy) =
-        Domain_Induction.comp_theorems comp_dbind
+        Domain_Induction.comp_theorems
           dbinds take_info constr_infos thy;
   in
     thy
@@ -240,27 +235,21 @@
     (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
 
 val domains_decl =
-  Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
-    Parse.and_list1 domain_decl;
+  Parse.and_list1 domain_decl;
 
 fun mk_domain
     (definitional : bool)
-    (opt_name : binding option,
-     doms : ((((string * string option) list * binding) * mixfix) *
+    (doms : ((((string * string option) list * binding) * mixfix) *
              ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
   let
-    val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
     val specs : ((string * string option) list * binding * mixfix *
                  (binding * (bool * binding option * string) list * mixfix) list) list =
         map (fn (((vs, t), mx), cons) =>
                 (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
-    val comp_dbind =
-        case opt_name of NONE => Binding.name (space_implode "_" names)
-                       | SOME s => s;
   in
-    if definitional 
-    then add_new_domain_cmd comp_dbind specs
-    else add_domain_cmd comp_dbind specs
+    if definitional
+    then add_new_domain_cmd specs
+    else add_domain_cmd specs
   end;
 
 val _ =
--- a/src/HOLCF/Tools/Domain/domain_induction.ML	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML	Sun Oct 24 15:11:24 2010 -0700
@@ -8,7 +8,7 @@
 signature DOMAIN_INDUCTION =
 sig
   val comp_theorems :
-      binding -> binding list ->
+      binding list ->
       Domain_Take_Proofs.take_induct_info ->
       Domain_Constructors.constr_info list ->
       theory -> thm list * theory
@@ -367,13 +367,14 @@
 (******************************************************************************)
 
 fun comp_theorems
-    (comp_dbind : binding)
     (dbinds : binding list)
     (take_info : Domain_Take_Proofs.take_induct_info)
     (constr_infos : Domain_Constructors.constr_info list)
     (thy : theory) =
 let
-val comp_dname = Binding.name_of comp_dbind;
+
+val comp_dname = space_implode "_" (map Binding.name_of dbinds);
+val comp_dbind = Binding.name comp_dname;
 
 (* Test for emptiness *)
 (* FIXME: reimplement emptiness test
--- a/src/HOLCF/Tools/fixrec.ML	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Sun Oct 24 15:11:24 2010 -0700
@@ -393,10 +393,16 @@
 (******************************** Parsers ********************************)
 (*************************************************************************)
 
+val opt_thm_name' : (bool * Attrib.binding) parser =
+  Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding)
+    || Parse_Spec.opt_thm_name ":" >> pair false;
+
+val spec' : (bool * (Attrib.binding * string)) parser =
+  opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)));
+
 val alt_specs' : (bool * (Attrib.binding * string)) list parser =
-  Parse.enum1 "|"
-    (Parse.opt_keyword "unchecked" -- Parse_Spec.spec --|
-      Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
+  let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(");
+  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end;
 
 val _ =
   Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
--- a/src/HOLCF/Up.thy	Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Up.thy	Sun Oct 24 15:11:24 2010 -0700
@@ -62,108 +62,67 @@
     by (auto split: u.split_asm intro: below_trans)
 qed
 
-lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
-by (auto, case_tac x, auto)
-
-instance u :: (finite_po) finite_po
-by (intro_classes, simp add: u_UNIV)
-
-
 subsection {* Lifted cpo is a cpo *}
 
 lemma is_lub_Iup:
   "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
-apply (rule is_lubI)
-apply (rule ub_rangeI)
-apply (subst Iup_below)
-apply (erule is_ub_lub)
-apply (case_tac u)
-apply (drule ub_rangeD)
-apply simp
-apply simp
-apply (erule is_lub_lub)
-apply (rule ub_rangeI)
-apply (drule_tac i=i in ub_rangeD)
-apply simp
-done
-
-text {* Now some lemmas about chains of @{typ "'a u"} elements *}
-
-lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"
-by (case_tac z, simp_all)
-
-lemma up_lemma2:
-  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
-apply (erule contrapos_nn)
-apply (drule_tac i="j" and j="i + j" in chain_mono)
-apply (rule le_add2)
-apply (case_tac "Y j")
-apply assumption
-apply simp
-done
-
-lemma up_lemma3:
-  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
-by (rule up_lemma1 [OF up_lemma2])
-
-lemma up_lemma4:
-  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
-apply (rule chainI)
-apply (rule Iup_below [THEN iffD1])
-apply (subst up_lemma3, assumption+)+
-apply (simp add: chainE)
-done
-
-lemma up_lemma5:
-  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow>
-    (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
-by (rule ext, rule up_lemma3 [symmetric])
-
-lemma up_lemma6:
-  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
-      \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
-apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
-apply assumption
-apply (subst up_lemma5, assumption+)
-apply (rule is_lub_Iup)
-apply (rule cpo_lubI)
-apply (erule (1) up_lemma4)
-done
+unfolding is_lub_def is_ub_def ball_simps
+by (auto simp add: below_up_def split: u.split)
 
 lemma up_chain_lemma:
-  "chain Y \<Longrightarrow>
-   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = Iup (\<Squnion>i. A i) \<and>
-   (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
-apply (rule disjCI)
-apply (simp add: fun_eq_iff)
-apply (erule exE, rename_tac j)
-apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
-apply (simp add: up_lemma4)
-apply (simp add: up_lemma6 [THEN thelubI])
-apply (rule_tac x=j in exI)
-apply (simp add: up_lemma3)
-done
-
-lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
-apply (frule up_chain_lemma, safe)
-apply (rule_tac x="Iup (\<Squnion>i. A i)" in exI)
-apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
-apply (simp add: is_lub_Iup cpo_lubI)
-apply (rule exI, rule lub_const)
-done
+  assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom"
+  | A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
+proof (cases "\<exists>k. Y k \<noteq> Ibottom")
+  case True
+  then obtain k where k: "Y k \<noteq> Ibottom" ..
+  def A \<equiv> "\<lambda>i. THE a. Iup a = Y (i + k)"
+  have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)"
+  proof
+    fix i :: nat
+    from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono)
+    with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto)
+    thus "Iup (A i) = Y (i + k)"
+      by (cases "Y (i + k)", simp_all add: A_def)
+  qed
+  from Y have chain_A: "chain A"
+    unfolding chain_def Iup_below [symmetric]
+    by (simp add: Iup_A)
+  hence "range A <<| (\<Squnion>i. A i)"
+    by (rule cpo_lubI)
+  hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)"
+    by (rule is_lub_Iup)
+  hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)"
+    by (simp only: Iup_A)
+  hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)"
+    by (simp only: is_lub_range_shift [OF Y])
+  with Iup_A chain_A show ?thesis ..
+next
+  case False
+  then have "\<forall>i. Y i = Ibottom" by simp
+  then show ?thesis ..
+qed
 
 instance u :: (cpo) cpo
-by intro_classes (rule cpo_up)
+proof
+  fix S :: "nat \<Rightarrow> 'a u"
+  assume S: "chain S"
+  thus "\<exists>x. range (\<lambda>i. S i) <<| x"
+  proof (rule up_chain_lemma)
+    assume "\<forall>i. S i = Ibottom"
+    hence "range (\<lambda>i. S i) <<| Ibottom"
+      by (simp add: lub_const)
+    thus ?thesis ..
+  next
+    fix A :: "nat \<Rightarrow> 'a"
+    assume "range S <<| Iup (\<Squnion>i. A i)"
+    thus ?thesis ..
+  qed
+qed
 
 subsection {* Lifted cpo is pointed *}
 
-lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
-apply (rule_tac x = "Ibottom" in exI)
-apply (rule minimal_up [THEN allI])
-done
-
 instance u :: (cpo) pcpo
-by intro_classes (rule least_up)
+by intro_classes fast
 
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_up_pcpo: "\<bottom> = Ibottom"
@@ -192,13 +151,22 @@
 done
 
 lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
-apply (rule contI)
-apply (frule up_chain_lemma, safe)
-apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
-apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
-apply (simp add: cont_cfun_arg)
-apply (simp add: lub_const)
-done
+proof (rule contI2)
+  fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))"
+  from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))"
+  proof (rule up_chain_lemma)
+    fix A and k
+    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)
+    also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
+      by (simp add: A)
+    also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
+      using Y' by (rule lub_range_shift)
+    finally show ?thesis by simp
+  qed simp
+qed (rule monofun_Ifup2)
 
 subsection {* Continuous versions of constants *}
 
@@ -251,18 +219,20 @@
 text {* lifting preserves chain-finiteness *}
 
 lemma up_chain_cases:
-  "chain Y \<Longrightarrow>
-  (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
-  (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
-by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
+  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)
+done
 
 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
 apply (rule compactI2)
-apply (drule up_chain_cases, safe)
+apply (erule up_chain_cases)
+apply simp
 apply (drule (1) compactD2, simp)
-apply (erule exE, rule_tac x="i + j" in exI)
-apply simp
-apply simp
+apply (erule exE)
+apply (drule_tac f="up" and x="x" in monofun_cfun_arg)
+apply (simp, erule exI)
 done
 
 lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"