# HG changeset patch
# User huffman
# Date 1116913418 -7200
# Node ID 833be7f71ecdb23e723ef1eb48a971d016b8d2ce
# Parent  dab0d004732f4607e5e8c23d03842b5408dcdf85
Simplified version of strict sum theory, using TypedefPcpo

diff -r dab0d004732f -r 833be7f71ecd src/HOLCF/Ssum.ML
--- a/src/HOLCF/Ssum.ML	Tue May 24 05:52:48 2005 +0200
+++ b/src/HOLCF/Ssum.ML	Tue May 24 07:43:38 2005 +0200
@@ -1,76 +1,14 @@
 
 (* legacy ML bindings *)
 
-val Isinl_def = thm "Isinl_def";
-val Isinr_def = thm "Isinr_def";
 val Iwhen_def = thm "Iwhen_def";
-val inj_on_Abs_Ssum = thm "inj_on_Abs_Ssum";
-val strict_IsinlIsinr = thm "strict_IsinlIsinr";
-val noteq_IsinlIsinr = thm "noteq_IsinlIsinr";
-val inject_Isinl = thm "inject_Isinl";
-val inject_Isinr = thm "inject_Isinr";
-val inject_Isinl_rev = thm "inject_Isinl_rev";
-val inject_Isinr_rev = thm "inject_Isinr_rev";
-val Exh_Ssum = thm "Exh_Ssum";
-val IssumE = thm "IssumE";
-val IssumE2 = thm "IssumE2";
 val Iwhen1 = thm "Iwhen1";
 val Iwhen2 = thm "Iwhen2";
 val Iwhen3 = thm "Iwhen3";
 val less_ssum_def = thm "less_ssum_def";
-val less_ssum1a = thm "less_ssum1a";
-val less_ssum1b = thm "less_ssum1b";
-val less_ssum1c = thm "less_ssum1c";
-val less_ssum1d = thm "less_ssum1d";
-val less_ssum2a = thm "less_ssum2a";
-val less_ssum2b = thm "less_ssum2b";
-val less_ssum2c = thm "less_ssum2c";
-val less_ssum2d = thm "less_ssum2d";
-val refl_less_ssum = thm "refl_less_ssum";
-val antisym_less_ssum = thm "antisym_less_ssum";
-val trans_less_ssum = thm "trans_less_ssum";
-val inst_ssum_po = thm "inst_ssum_po";
-val less_ssum3a = thm "less_ssum3a";
-val less_ssum3b = thm "less_ssum3b";
-val less_ssum3c = thm "less_ssum3c";
-val less_ssum3d = thm "less_ssum3d";
-val minimal_ssum = thm "minimal_ssum";
-val UU_ssum_def = thm "UU_ssum_def";
-val least_ssum = thm "least_ssum";
-val monofun_Isinl = thm "monofun_Isinl";
-val monofun_Isinr = thm "monofun_Isinr";
-val monofun_Iwhen1 = thm "monofun_Iwhen1";
-val monofun_Iwhen2 = thm "monofun_Iwhen2";
-val monofun_Iwhen3 = thm "monofun_Iwhen3";
-val ssum_lemma1 = thm "ssum_lemma1";
-val ssum_lemma2 = thm "ssum_lemma2";
-val ssum_lemma3 = thm "ssum_lemma3";
-val ssum_lemma4 = thm "ssum_lemma4";
-val ssum_lemma5 = thm "ssum_lemma5";
-val ssum_lemma6 = thm "ssum_lemma6";
-val ssum_lemma7 = thm "ssum_lemma7";
-val ssum_lemma8 = thm "ssum_lemma8";
-val lub_ssum1a = thm "lub_ssum1a";
-val lub_ssum1b = thm "lub_ssum1b";
-val thelub_ssum1a = thm "thelub_ssum1a";
-val thelub_ssum1b = thm "thelub_ssum1b";
-val cpo_ssum = thm "cpo_ssum";
 val sinl_def = thm "sinl_def";
 val sinr_def = thm "sinr_def";
 val sscase_def = thm "sscase_def";
-val inst_ssum_pcpo = thm "inst_ssum_pcpo";
-val contlub_Isinl = thm "contlub_Isinl";
-val contlub_Isinr = thm "contlub_Isinr";
-val cont_Isinl = thm "cont_Isinl";
-val cont_Isinr = thm "cont_Isinr";
-val contlub_Iwhen1 = thm "contlub_Iwhen1";
-val contlub_Iwhen2 = thm "contlub_Iwhen2";
-val ssum_lemma9 = thm "ssum_lemma9";
-val ssum_lemma10 = thm "ssum_lemma10";
-val ssum_lemma11 = thm "ssum_lemma11";
-val ssum_lemma12 = thm "ssum_lemma12";
-val ssum_lemma13 = thm "ssum_lemma13";
-val contlub_Iwhen3 = thm "contlub_Iwhen3";
 val cont_Iwhen1 = thm "cont_Iwhen1";
 val cont_Iwhen2 = thm "cont_Iwhen2";
 val cont_Iwhen3 = thm "cont_Iwhen3";
@@ -91,12 +29,6 @@
 val less_ssum4b = thm "less_ssum4b";
 val less_ssum4c = thm "less_ssum4c";
 val less_ssum4d = thm "less_ssum4d";
-val ssum_chainE = thm "ssum_chainE";
-val thelub_ssum2a = thm "thelub_ssum2a";
-val thelub_ssum2b = thm "thelub_ssum2b";
-val thelub_ssum2a_rev = thm "thelub_ssum2a_rev";
-val thelub_ssum2b_rev = thm "thelub_ssum2b_rev";
-val thelub_ssum3 = thm "thelub_ssum3";
 val sscase4 = thm "sscase4";
 val Ssum_rews = [strict_sinl, strict_sinr, defined_sinl, defined_sinr,
                 sscase1, sscase2, sscase3]
diff -r dab0d004732f -r 833be7f71ecd src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Tue May 24 05:52:48 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Tue May 24 07:43:38 2005 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOLCF/Ssum.thy
     ID:         $Id$
-    Author:     Franz Regensburger
+    Author:     Franz Regensburger and Brian Huffman
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Strict sum with typedef
@@ -9,1016 +9,269 @@
 header {* The type of strict sums *}
 
 theory Ssum
-imports Cprod
+imports Cprod TypedefPcpo
 begin
 
 subsection {* Definition of strict sum type *}
 
 typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
-        "{p::'a * 'b. fst p = UU | snd p = UU}"
-by auto
+        "{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
+by (rule_tac x="<\<bottom>,\<bottom>>" in exI, simp)
 
 syntax (xsymbols)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 syntax (HTML output)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 
-consts
-  Isinl         :: "'a => ('a ++ 'b)"
-  Isinr         :: "'b => ('a ++ 'b)"
-  Iwhen         :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
+subsection {* Class instances *}
+
+instance "++" :: (pcpo, pcpo) sq_ord ..
+defs (overloaded)
+  less_ssum_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Ssum x \<sqsubseteq> Rep_Ssum y"
+
+lemma adm_Ssum: "adm (\<lambda>x. x \<in> Ssum)"
+by (simp add: Ssum_def cont_fst cont_snd)
+
+lemma UU_Ssum: "\<bottom> \<in> Ssum"
+by (simp add: Ssum_def inst_cprod_pcpo2)
+
+instance "++" :: (pcpo, pcpo) po
+by (rule typedef_po [OF type_definition_Ssum less_ssum_def])
 
-defs   -- {*defining the abstract constants*}
-  Isinl_def:     "Isinl(a) == Abs_Ssum(a,UU)"
-  Isinr_def:     "Isinr(b) == Abs_Ssum(UU,b)"
+instance "++" :: (pcpo, pcpo) cpo
+by (rule typedef_cpo [OF type_definition_Ssum less_ssum_def adm_Ssum])
+
+instance "++" :: (pcpo, pcpo) pcpo
+by (rule typedef_pcpo_UU [OF type_definition_Ssum less_ssum_def UU_Ssum])
+
+lemmas cont_Rep_Ssum =
+  typedef_cont_Rep [OF type_definition_Ssum less_ssum_def adm_Ssum]
 
-  Iwhen_def:     "Iwhen(f)(g)(s) == case Rep_Ssum s of (a,b) =>
-                         if a ~= UU then f$a else
-                         if b ~= UU then g$b else UU"
+lemmas cont_Abs_Ssum = 
+  typedef_cont_Abs [OF type_definition_Ssum less_ssum_def adm_Ssum]
+
+lemmas strict_Rep_Ssum =
+  typedef_strict_Rep [OF type_definition_Ssum less_ssum_def UU_Ssum]
+
+lemmas strict_Abs_Ssum =
+  typedef_strict_Abs [OF type_definition_Ssum less_ssum_def UU_Ssum]
 
-lemma inj_on_Abs_Ssum: "inj_on Abs_Ssum Ssum"
-apply (rule inj_on_inverseI)
-apply (erule Abs_Ssum_inverse)
-done
+lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>"
+by (simp add: strict_Abs_Ssum inst_cprod_pcpo2 [symmetric])
+
+
+subsection {* Definitions of constructors *}
 
-text {* Strictness of @{term Isinl}, @{term Isinr} *}
+constdefs
+  sinl :: "'a \<rightarrow> ('a ++ 'b)"
+  "sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>"
+
+  sinr :: "'b \<rightarrow> ('a ++ 'b)"
+  "sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>"
+
+subsection {* Properties of @{term sinl} and @{term sinr} *}
+
+lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum <a, \<bottom>>"
+by (unfold sinl_def, simp add: cont_Abs_Ssum Ssum_def)
 
-lemma strict_IsinlIsinr: "Isinl(UU) = Isinr(UU)"
-by (simp add: Isinl_def Isinr_def)
+lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum <\<bottom>, b>"
+by (unfold sinr_def, simp add: cont_Abs_Ssum Ssum_def)
+
+lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = <a, \<bottom>>"
+by (unfold sinl_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)
+
+lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <\<bottom>, b>"
+by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)
 
-text {* distinctness of @{term Isinl}, @{term Isinr} *}
+lemma strict_sinl [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
+by (simp add: sinl_Abs_Ssum UU_Abs_Ssum)
 
-lemma noteq_IsinlIsinr: 
-        "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
-apply (unfold Isinl_def Isinr_def)
+lemma strict_sinr [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
+by (simp add: sinr_Abs_Ssum UU_Abs_Ssum)
+
+lemma noteq_sinlsinr: "sinl\<cdot>a = sinr\<cdot>b \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
+apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum)
 apply (simp add: Abs_Ssum_inject Ssum_def)
 done
 
-text {* injectivity of @{term Isinl}, @{term Isinr} *}
-
-lemma inject_Isinl: "Isinl(a1)=Isinl(a2)==> a1=a2"
-by (simp add: Isinl_def Abs_Ssum_inject Ssum_def)
-
-lemma inject_Isinr: "Isinr(b1)=Isinr(b2) ==> b1=b2"
-by (simp add: Isinr_def Abs_Ssum_inject Ssum_def)
-
-declare inject_Isinl [dest!] inject_Isinr [dest!]
-declare noteq_IsinlIsinr [dest!]
-declare noteq_IsinlIsinr [OF sym, dest!]
-
-lemma inject_Isinl_rev: "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
-by blast
-
-lemma inject_Isinr_rev: "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
-by blast
-
-text {* Exhaustion of the strict sum @{typ "'a ++ 'b"} *}
-text {* choice of the bottom representation is arbitrary *}
-
-lemma Exh_Ssum: 
-        "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"
-apply (unfold Isinl_def Isinr_def)
-apply (rule_tac x=z in Abs_Ssum_cases)
-apply (auto simp add: Ssum_def)
-done
-
-text {* elimination rules for the strict sum @{typ "'a ++ 'b"} *}
-
-lemma IssumE:
-        "[|p=Isinl(UU) ==> Q ; 
-        !!x.[|p=Isinl(x); x~=UU |] ==> Q; 
-        !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q"
-by (rule Exh_Ssum [THEN disjE]) auto
-
-lemma IssumE2:
-"[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
-by (rule_tac p=p in IssumE) auto
-
-text {* rewrites for @{term Iwhen} *}
-
-lemma Iwhen1: "Iwhen f g (Isinl UU) = UU"
-apply (unfold Iwhen_def Isinl_def)
-apply (simp add: Abs_Ssum_inverse Ssum_def)
-done
-
-lemma Iwhen2: "x~=UU ==> Iwhen f g (Isinl x) = f$x"
-apply (unfold Iwhen_def Isinl_def)
-apply (simp add: Abs_Ssum_inverse Ssum_def)
-done
-
-lemma Iwhen3: "y~=UU ==> Iwhen f g (Isinr y) = g$y"
-apply (unfold Iwhen_def Isinr_def)
-apply (simp add: Abs_Ssum_inverse Ssum_def)
-done
-
-text {* instantiate the simplifier *}
-
-lemmas Ssum0_ss = strict_IsinlIsinr[symmetric] Iwhen1 Iwhen2 Iwhen3
-
-declare Ssum0_ss [simp]
-
-subsection {* Ordering for type @{typ "'a ++ 'b"} *}
-
-instance "++"::(pcpo, pcpo) sq_ord ..
-
-defs (overloaded)
-  less_ssum_def: "(op <<) == (%s1 s2. Rep_Ssum s1 << Rep_Ssum s2)"
-
-lemma less_ssum1a: 
-"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
-by (simp add: Isinl_def less_ssum_def Abs_Ssum_inverse Ssum_def inst_cprod_po)
-
-lemma less_ssum1b: 
-"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
-by (simp add: Isinr_def less_ssum_def Abs_Ssum_inverse Ssum_def inst_cprod_po)
-
-lemma less_ssum1c: 
-"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
-by (simp add: Isinr_def Isinl_def less_ssum_def Abs_Ssum_inverse Ssum_def inst_cprod_po eq_UU_iff)
-
-lemma less_ssum1d: 
-"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
-by (simp add: Isinr_def Isinl_def less_ssum_def Abs_Ssum_inverse Ssum_def inst_cprod_po eq_UU_iff)
-
-text {* optimize lemmas about @{term less_ssum} *}
-
-lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)"
-by (simp only: less_ssum1a)
-
-lemma less_ssum2b: "(Isinr x) << (Isinr y) = (x << y)"
-by (simp only: less_ssum1b)
-
-lemma less_ssum2c: "(Isinl x) << (Isinr y) = (x = UU)"
-by (simp only: less_ssum1c)
-
-lemma less_ssum2d: "(Isinr x) << (Isinl y) = (x = UU)"
-by (simp only: less_ssum1d)
-
-subsection {* Type @{typ "'a ++ 'b"} is a partial order *}
-
-lemma refl_less_ssum: "(p::'a++'b) << p"
-by (unfold less_ssum_def, rule refl_less)
-
-lemma antisym_less_ssum: "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
-apply (unfold less_ssum_def)
-apply (subst Rep_Ssum_inject [symmetric])
-by (rule antisym_less)
-
-lemma trans_less_ssum: "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
-by (unfold less_ssum_def, rule trans_less)
-
-instance "++" :: (pcpo, pcpo) po
-by intro_classes
-  (assumption | rule refl_less_ssum antisym_less_ssum trans_less_ssum)+
-
-text {* for compatibility with old HOLCF-Version *}
-lemmas inst_ssum_po = less_ssum_def [THEN meta_eq_to_obj_eq]
-
-subsection {* Type @{typ "'a ++ 'b"} is pointed *}
-
-lemma minimal_ssum: "Isinl UU << s"
-apply (simp add: less_ssum_def Isinl_def Abs_Ssum_inverse Ssum_def)
-apply (simp add: inst_cprod_pcpo [symmetric])
-done
-
-lemmas UU_ssum_def = minimal_ssum [THEN minimal2UU, symmetric, standard]
-
-lemma least_ssum: "? x::'a++'b.!y. x<<y"
-apply (rule_tac x = "Isinl UU" in exI)
-apply (rule minimal_ssum [THEN allI])
-done
-
-subsection {* Monotonicity of @{term Isinl}, @{term Isinr}, @{term Iwhen} *}
-
-text {* @{term Isinl} and @{term Isinr} are monotone *}
-
-lemma monofun_Isinl: "monofun(Isinl)"
-by (simp add: monofun less_ssum2a)
-
-lemma monofun_Isinr: "monofun(Isinr)"
-by (simp add: monofun less_ssum2b)
-
-text {* @{term Iwhen} is monotone in all arguments *}
-
-lemma monofun_Iwhen1: "monofun(Iwhen)"
-apply (rule monofunI [rule_format])
-apply (rule less_fun [THEN iffD2, rule_format])
-apply (rule less_fun [THEN iffD2, rule_format])
-apply (rule_tac p = "xb" in IssumE)
-apply simp
-apply simp
-apply (erule monofun_cfun_fun)
-apply simp
-done
-
-lemma monofun_Iwhen2: "monofun(Iwhen(f))"
-apply (rule monofunI [rule_format])
-apply (rule less_fun [THEN iffD2, rule_format])
-apply (rule_tac p = "xa" in IssumE)
-apply simp
-apply simp
-apply simp
-apply (erule monofun_cfun_fun)
-done
+lemma inject_sinl: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"
+by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def)
 
-lemma monofun_Iwhen3: "monofun(Iwhen(f)(g))"
-apply (rule monofunI [rule_format])
-apply (rule_tac p = "x" in IssumE)
-apply simp
-apply (rule_tac p = "y" in IssumE)
-apply simp
-apply (rule_tac P = "xa=UU" in notE)
-apply assumption
-apply (rule UU_I)
-apply (rule less_ssum2a [THEN iffD1])
-apply assumption
-apply simp
-apply (rule monofun_cfun_arg)
-apply (erule less_ssum2a [THEN iffD1])
-apply (simp del: Iwhen2)
-apply (rule_tac s = "UU" and t = "xa" in subst)
-apply (erule less_ssum2c [THEN iffD1, symmetric])
-apply simp
-apply (rule_tac p = "y" in IssumE)
-apply simp
-apply (simp only: less_ssum2d)
-apply (simp only: less_ssum2d)
-apply simp
-apply (rule monofun_cfun_arg)
-apply (erule less_ssum2b [THEN iffD1])
-done
-
-text {* some kind of exhaustion rules for chains in @{typ "'a ++ 'b"} *}
-
-lemma ssum_lemma1: "[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))"
-by fast
-
-lemma ssum_lemma2: "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|]   
-      ==> (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)"
-apply (erule exE)
-apply (rule_tac p = "Y (i) " in IssumE)
-apply (drule spec)
-apply (erule notE, assumption)
-apply (drule spec)
-apply (erule notE, assumption)
-apply fast
-done
-
-lemma ssum_lemma3: "[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|]  
-      ==> (!i.? y. Y(i)=Isinr(y))"
-apply (erule exE)
-apply (erule exE)
-apply (rule allI)
-apply (rule_tac p = "Y (ia) " in IssumE)
-apply (rule exI)
-apply (rule trans)
-apply (rule_tac [2] strict_IsinlIsinr)
-apply assumption
-apply (erule_tac [2] exI)
-apply (erule conjE)
-apply (rule_tac m = "i" and n = "ia" in nat_less_cases)
-prefer 2 apply simp
-apply (rule exI, rule refl)
-apply (erule_tac P = "x=UU" in notE)
-apply (rule less_ssum2d [THEN iffD1])
-apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst)
-apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst)
-apply (erule chain_mono)
-apply assumption
-apply (erule_tac P = "xa=UU" in notE)
-apply (rule less_ssum2c [THEN iffD1])
-apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst)
-apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst)
-apply (erule chain_mono)
-apply assumption
-done
-
-lemma ssum_lemma4: "chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
-apply (rule case_split_thm)
-apply (erule disjI1)
-apply (rule disjI2)
-apply (erule ssum_lemma3)
-apply (rule ssum_lemma2)
-apply (erule ssum_lemma1)
-done
-
-text {* restricted surjectivity of @{term Isinl} *}
-
-lemma ssum_lemma5: "z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z"
-apply simp
-apply (case_tac "x=UU")
-apply simp
-apply simp
-done
-
-text {* restricted surjectivity of @{term Isinr} *}
-
-lemma ssum_lemma6: "z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z"
-apply simp
-apply (case_tac "x=UU")
-apply simp
-apply simp
-done
-
-text {* technical lemmas *}
-
-lemma ssum_lemma7: "[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU"
-apply (rule_tac p = "z" in IssumE)
-apply simp
-apply (erule notE)
-apply (rule antisym_less)
-apply (erule less_ssum2a [THEN iffD1])
-apply (rule minimal)
-apply fast
-apply simp
-apply (rule notE)
-apply (erule_tac [2] less_ssum2c [THEN iffD1])
-apply assumption
-done
-
-lemma ssum_lemma8: "[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU"
-apply (rule_tac p = "z" in IssumE)
-apply simp
-apply (erule notE)
-apply (erule less_ssum2d [THEN iffD1])
-apply simp
-apply (rule notE)
-apply (erule_tac [2] less_ssum2d [THEN iffD1])
-apply assumption
-apply fast
-done
-
-subsection {* Type @{typ "'a ++ 'b"} is a cpo in three steps *}
-
-lemma lub_ssum1a: "[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==> 
-      range(Y) <<| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
-apply (rule is_lubI)
-apply (rule ub_rangeI)
-apply (erule allE)
-apply (erule exE)
-apply (rule_tac t = "Y (i) " in ssum_lemma5 [THEN subst])
-apply assumption
-apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp])
-apply (rule is_ub_thelub)
-apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply (rule_tac p = "u" in IssumE2)
-apply (rule_tac t = "u" in ssum_lemma5 [THEN subst])
-apply assumption
-apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp])
-apply (rule is_lub_thelub)
-apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
-apply simp
-apply (rule less_ssum2c [THEN iffD2])
-apply (rule chain_UU_I_inverse)
-apply (rule allI)
-apply (rule_tac p = "Y (i) " in IssumE)
-apply simp
-apply simp
-apply (erule notE)
-apply (rule less_ssum2c [THEN iffD1])
-apply (rule_tac t = "Isinl (x) " in subst)
-apply assumption
-apply (erule ub_rangeD)
-apply simp
-done
-
-lemma lub_ssum1b: "[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==> 
-      range(Y) <<| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
-apply (rule is_lubI)
-apply (rule ub_rangeI)
-apply (erule allE)
-apply (erule exE)
-apply (rule_tac t = "Y (i) " in ssum_lemma6 [THEN subst])
-apply assumption
-apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp])
-apply (rule is_ub_thelub)
-apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply (rule_tac p = "u" in IssumE2)
-apply simp
-apply (rule less_ssum2d [THEN iffD2])
-apply (rule chain_UU_I_inverse)
-apply (rule allI)
-apply (rule_tac p = "Y (i) " in IssumE)
-apply simp
-apply simp
-apply (erule notE)
-apply (rule less_ssum2d [THEN iffD1])
-apply (rule_tac t = "Isinr (y) " in subst)
-apply assumption
-apply (erule ub_rangeD)
-apply (rule_tac t = "u" in ssum_lemma6 [THEN subst])
-apply assumption
-apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp])
-apply (rule is_lub_thelub)
-apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
-done
-
-lemmas thelub_ssum1a = lub_ssum1a [THEN thelubI, standard]
-(*
-[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
- lub (range ?Y1) = Isinl
- (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i))))
-*)
+lemma inject_sinr: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
+by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def)
 
-lemmas thelub_ssum1b = lub_ssum1b [THEN thelubI, standard]
-(*
-[| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
- lub (range ?Y1) = Isinr
- (lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i))))
-*)
-
-lemma cpo_ssum: "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
-apply (rule ssum_lemma4 [THEN disjE])
-apply assumption
-apply (rule exI)
-apply (erule lub_ssum1a)
-apply assumption
-apply (rule exI)
-apply (erule lub_ssum1b)
-apply assumption
-done
-
-instance "++" :: (pcpo, pcpo) cpo
-by intro_classes (rule cpo_ssum)
-
-instance "++" :: (pcpo, pcpo) pcpo
-by intro_classes (rule least_ssum)
-
-text {* for compatibility with old HOLCF-Version *}
-lemma inst_ssum_pcpo: "UU = Isinl UU"
-apply (simp add: UU_def UU_ssum_def)
-done
-
-declare inst_ssum_pcpo [symmetric, simp]
-
-subsection {* Continuous versions of constants *}
-
-consts  
-        sinl    :: "'a -> ('a++'b)" 
-        sinr    :: "'b -> ('a++'b)" 
-        sscase  :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
-
-defs
-
-sinl_def:        "sinl   == (LAM x. Isinl(x))"
-sinr_def:        "sinr   == (LAM x. Isinr(x))"
-sscase_def:      "sscase   == (LAM f g s. Iwhen(f)(g)(s))"
-
-translations
-"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
-
-text {* continuity for @{term Isinl} and @{term Isinr} *}
-
-lemma contlub_Isinl: "contlub(Isinl)"
-apply (rule contlubI)
-apply (intro strip)
-apply (rule trans)
-apply (rule_tac [2] thelub_ssum1a [symmetric])
-apply (rule_tac [3] allI)
-apply (rule_tac [3] exI)
-apply (rule_tac [3] refl)
-apply (erule_tac [2] monofun_Isinl [THEN ch2ch_monofun])
-apply (case_tac "lub (range (Y))=UU")
-apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
-apply assumption
-apply (rule_tac f = "Isinl" in arg_cong)
-apply (rule chain_UU_I_inverse [symmetric])
-apply (rule allI)
-apply (rule_tac s = "UU" and t = "Y (i) " in ssubst)
-apply (erule chain_UU_I [THEN spec])
-apply assumption
-apply (rule Iwhen1)
-apply (rule_tac f = "Isinl" in arg_cong)
-apply (rule lub_equal)
-apply assumption
-apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply (erule monofun_Isinl [THEN ch2ch_monofun])
-apply (rule allI)
-apply (case_tac "Y (k) =UU")
-apply (erule ssubst)
-apply (rule Iwhen1[symmetric])
-apply simp
-done
-
-lemma contlub_Isinr: "contlub(Isinr)"
-apply (rule contlubI)
-apply (intro strip)
-apply (rule trans)
-apply (rule_tac [2] thelub_ssum1b [symmetric])
-apply (rule_tac [3] allI)
-apply (rule_tac [3] exI)
-apply (rule_tac [3] refl)
-apply (erule_tac [2] monofun_Isinr [THEN ch2ch_monofun])
-apply (case_tac "lub (range (Y))=UU")
-apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
-apply assumption
-apply (rule arg_cong, rule chain_UU_I_inverse [symmetric])
-apply (rule allI)
-apply (rule_tac s = "UU" and t = "Y (i) " in ssubst)
-apply (erule chain_UU_I [THEN spec])
-apply assumption
-apply (rule strict_IsinlIsinr [THEN subst])
-apply (rule Iwhen1)
-apply (rule arg_cong, rule lub_equal)
-apply assumption
-apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply (erule monofun_Isinr [THEN ch2ch_monofun])
-apply (rule allI)
-apply (case_tac "Y (k) =UU")
-apply (simp only: Ssum0_ss)
-apply simp
-done
-
-lemma cont_Isinl [iff]: "cont(Isinl)"
-apply (rule monocontlub2cont)
-apply (rule monofun_Isinl)
-apply (rule contlub_Isinl)
-done
-
-lemma cont_Isinr [iff]: "cont(Isinr)"
-apply (rule monocontlub2cont)
-apply (rule monofun_Isinr)
-apply (rule contlub_Isinr)
-done
-
-text {* continuity for @{term Iwhen} in the first two arguments *}
-
-lemma contlub_Iwhen1: "contlub(Iwhen)"
-apply (rule contlubI)
-apply (intro strip)
-apply (rule trans)
-apply (rule_tac [2] thelub_fun [symmetric])
-apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
-apply (rule expand_fun_eq [THEN iffD2])
-apply (intro strip)
-apply (rule trans)
-apply (rule_tac [2] thelub_fun [symmetric])
-apply (rule_tac [2] ch2ch_fun)
-apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
-apply (rule expand_fun_eq [THEN iffD2])
-apply (intro strip)
-apply (rule_tac p = "xa" in IssumE)
-apply (simp only: Ssum0_ss)
-apply (rule lub_const [THEN thelubI, symmetric])
-apply simp
-apply (erule contlub_cfun_fun)
-apply simp
-apply (rule lub_const [THEN thelubI, symmetric])
-done
-
-lemma contlub_Iwhen2: "contlub(Iwhen(f))"
-apply (rule contlubI)
-apply (intro strip)
-apply (rule trans)
-apply (rule_tac [2] thelub_fun [symmetric])
-apply (erule_tac [2] monofun_Iwhen2 [THEN ch2ch_monofun])
-apply (rule expand_fun_eq [THEN iffD2])
-apply (intro strip)
-apply (rule_tac p = "x" in IssumE)
-apply (simp only: Ssum0_ss)
-apply (rule lub_const [THEN thelubI, symmetric])
-apply simp
-apply (rule lub_const [THEN thelubI, symmetric])
-apply simp
-apply (erule contlub_cfun_fun)
-done
-
-text {* continuity for @{term Iwhen} in its third argument *}
-
-text {* first 5 ugly lemmas *}
-
-lemma ssum_lemma9: "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
-apply (intro strip)
-apply (rule_tac p = "Y (i) " in IssumE)
-apply (erule exI)
-apply (erule exI)
-apply (rule_tac P = "y=UU" in notE)
-apply assumption
-apply (rule less_ssum2d [THEN iffD1])
-apply (erule subst)
-apply (erule subst)
-apply (erule is_ub_thelub)
-done
+lemma sinl_eq: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
+by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def)
 
-lemma ssum_lemma10: "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
-apply (intro strip)
-apply (rule_tac p = "Y (i) " in IssumE)
-apply (rule exI)
-apply (erule trans)
-apply (rule strict_IsinlIsinr)
-apply (erule_tac [2] exI)
-apply (rule_tac P = "xa=UU" in notE)
-apply assumption
-apply (rule less_ssum2c [THEN iffD1])
-apply (erule subst)
-apply (erule subst)
-apply (erule is_ub_thelub)
-done
-
-lemma ssum_lemma11: "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==> 
-    Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
-apply (simp only: Ssum0_ss)
-apply (rule chain_UU_I_inverse [symmetric])
-apply (rule allI)
-apply (rule_tac s = "Isinl (UU) " and t = "Y (i) " in subst)
-apply (rule inst_ssum_pcpo [THEN subst])
-apply (rule chain_UU_I [THEN spec, symmetric])
-apply assumption
-apply (erule inst_ssum_pcpo [THEN ssubst])
-apply (simp only: Ssum0_ss)
-done
-
-lemma ssum_lemma12: "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==> 
-    Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
-apply simp
-apply (rule_tac t = "x" in subst)
-apply (rule inject_Isinl)
-apply (rule trans)
-prefer 2 apply (assumption)
-apply (rule thelub_ssum1a [symmetric])
-apply assumption
-apply (erule ssum_lemma9)
-apply assumption
-apply (rule trans)
-apply (rule contlub_cfun_arg)
-apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply assumption
-apply (rule lub_equal2)
-apply (rule chain_mono2 [THEN exE])
-prefer 2 apply (assumption)
-apply (rule chain_UU_I_inverse2)
-apply (subst inst_ssum_pcpo)
-apply (erule contrapos_np)
-apply (rule inject_Isinl)
-apply (rule trans)
-apply (erule sym)
-apply (erule notnotD)
-apply (rule exI)
-apply (intro strip)
-apply (rule ssum_lemma9 [THEN spec, THEN exE])
-apply assumption
-apply assumption
-apply (rule_tac t = "Y (i) " in ssubst)
-apply assumption
-apply (rule trans)
-apply (rule cfun_arg_cong)
-apply (rule Iwhen2)
-apply force
-apply (rule_tac t = "Y (i) " in ssubst)
-apply assumption
-apply auto
-apply (subst Iwhen2)
-apply force
-apply (rule refl)
-apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
-apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
-done
+lemma sinr_eq: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"
+by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def)
 
-lemma ssum_lemma13: "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==> 
-    Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
-apply simp
-apply (rule_tac t = "x" in subst)
-apply (rule inject_Isinr)
-apply (rule trans)
-prefer 2 apply (assumption)
-apply (rule thelub_ssum1b [symmetric])
-apply assumption
-apply (erule ssum_lemma10)
-apply assumption
-apply (rule trans)
-apply (rule contlub_cfun_arg)
-apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply assumption
-apply (rule lub_equal2)
-apply (rule chain_mono2 [THEN exE])
-prefer 2 apply (assumption)
-apply (rule chain_UU_I_inverse2)
-apply (subst inst_ssum_pcpo)
-apply (erule contrapos_np)
-apply (rule inject_Isinr)
-apply (rule trans)
-apply (erule sym)
-apply (rule strict_IsinlIsinr [THEN subst])
-apply (erule notnotD)
-apply (rule exI)
-apply (intro strip)
-apply (rule ssum_lemma10 [THEN spec, THEN exE])
-apply assumption
-apply assumption
-apply (rule_tac t = "Y (i) " in ssubst)
-apply assumption
-apply (rule trans)
-apply (rule cfun_arg_cong)
-apply (rule Iwhen3)
-apply force
-apply (rule_tac t = "Y (i) " in ssubst)
-apply assumption
-apply (subst Iwhen3)
-apply force
-apply (rule_tac t = "Y (i) " in ssubst)
-apply assumption
-apply simp
-apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
-apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
-apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
-done
-
-lemma contlub_Iwhen3: "contlub(Iwhen(f)(g))"
-apply (rule contlubI)
-apply (intro strip)
-apply (rule_tac p = "lub (range (Y))" in IssumE)
-apply (erule ssum_lemma11)
-apply assumption
-apply (erule ssum_lemma12)
-apply assumption
-apply assumption
-apply (erule ssum_lemma13)
-apply assumption
-apply assumption
-done
-
-lemma cont_Iwhen1: "cont(Iwhen)"
-apply (rule monocontlub2cont)
-apply (rule monofun_Iwhen1)
-apply (rule contlub_Iwhen1)
-done
-
-lemma cont_Iwhen2: "cont(Iwhen(f))"
-apply (rule monocontlub2cont)
-apply (rule monofun_Iwhen2)
-apply (rule contlub_Iwhen2)
-done
-
-lemma cont_Iwhen3: "cont(Iwhen(f)(g))"
-apply (rule monocontlub2cont)
-apply (rule monofun_Iwhen3)
-apply (rule contlub_Iwhen3)
-done
-
-text {* continuous versions of lemmas for @{typ "'a ++ 'b"} *}
-
-lemma strict_sinl [simp]: "sinl$UU =UU"
-apply (unfold sinl_def)
-apply (simp add: cont_Isinl)
-done
-
-lemma strict_sinr [simp]: "sinr$UU=UU"
-apply (unfold sinr_def)
-apply (simp add: cont_Isinr)
-done
-
-lemma noteq_sinlsinr: 
-        "sinl$a=sinr$b ==> a=UU & b=UU"
-apply (unfold sinl_def sinr_def)
-apply (auto dest!: noteq_IsinlIsinr)
-done
-
-lemma inject_sinl: 
-        "sinl$a1=sinl$a2==> a1=a2"
-apply (unfold sinl_def sinr_def)
-apply auto
-done
-
-lemma inject_sinr: 
-        "sinr$a1=sinr$a2==> a1=a2"
-apply (unfold sinl_def sinr_def)
-apply auto
-done
-
-declare inject_sinl [dest!] inject_sinr [dest!]
-
-lemma defined_sinl [simp]: "x~=UU ==> sinl$x ~= UU"
+lemma defined_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
 apply (erule contrapos_nn)
 apply (rule inject_sinl)
 apply auto
 done
 
-lemma defined_sinr [simp]: "x~=UU ==> sinr$x ~= UU"
+lemma defined_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
 apply (erule contrapos_nn)
 apply (rule inject_sinr)
 apply auto
 done
 
+subsection {* Case analysis *}
+
 lemma Exh_Ssum1: 
-        "z=UU | (? a. z=sinl$a & a~=UU) | (? b. z=sinr$b & b~=UU)"
-apply (unfold sinl_def sinr_def)
-apply simp
-apply (subst inst_ssum_pcpo)
-apply (rule 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 (simp add: sinl_Abs_Ssum sinr_Abs_Ssum UU_Abs_Ssum)
+apply (rule_tac x=z in Abs_Ssum_cases)
+apply (rule_tac p=y in cprodE)
+apply (auto simp add: Ssum_def)
 done
 
 lemma ssumE:
-assumes major: "p=UU ==> Q"
-assumes prem2: "!!x.[|p=sinl$x; x~=UU |] ==> Q"
-assumes prem3: "!!y.[|p=sinr$y; y~=UU |] ==> Q"
-shows "Q"
-apply (rule major [THEN IssumE])
-apply (subst inst_ssum_pcpo)
-apply assumption
-apply (rule prem2)
-prefer 2 apply (assumption)
-apply (simp add: sinl_def)
-apply (rule prem3)
-prefer 2 apply (assumption)
-apply (simp add: sinr_def)
-done
-
+  "\<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"
+by (cut_tac z=p in Exh_Ssum1, auto)
 
 lemma ssumE2:
-assumes preml: "!!x.[|p=sinl$x|] ==> Q"
-assumes premr: "!!y.[|p=sinr$y|] ==> Q"
-shows "Q"
-apply (rule IssumE2)
-apply (rule preml)
-apply (rule_tac [2] premr)
-apply (unfold sinl_def sinr_def)
-apply auto
-done
-
-lemmas ssum_conts = cont_lemmas1 cont_Iwhen1 cont_Iwhen2
-                cont_Iwhen3 cont2cont_CF1L
-
-lemma sscase1 [simp]: 
-        "sscase$f$g$UU = UU"
-apply (unfold sscase_def sinl_def sinr_def)
-apply (subst inst_ssum_pcpo)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (simp only: Ssum0_ss)
-done
-
-lemma sscase2 [simp]: 
-        "x~=UU==> sscase$f$g$(sinl$x) = f$x"
-apply (unfold sscase_def sinl_def sinr_def)
-apply (simplesubst beta_cfun)
-apply (rule cont_Isinl)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
+  "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+apply (rule_tac p=p in ssumE)
+apply (simp only: strict_sinl [symmetric])
 apply simp
-done
-
-lemma sscase3 [simp]: 
-        "x~=UU==> sscase$f$g$(sinr$x) = g$x"
-apply (unfold sscase_def sinl_def sinr_def)
-apply (simplesubst beta_cfun)
-apply (rule cont_Isinr)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
 apply simp
 done
 
-lemma less_ssum4a: 
-        "(sinl$x << sinl$y) = (x << y)"
-apply (unfold sinl_def sinr_def)
-apply (subst beta_cfun)
-apply (rule cont_Isinl)
-apply (subst beta_cfun)
-apply (rule cont_Isinl)
-apply (rule less_ssum2a)
-done
+subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
 
-lemma less_ssum4b: 
-        "(sinr$x << sinr$y) = (x << y)"
-apply (unfold sinl_def sinr_def)
-apply (subst beta_cfun)
-apply (rule cont_Isinr)
-apply (subst beta_cfun)
-apply (rule cont_Isinr)
-apply (rule less_ssum2b)
-done
-
-lemma less_ssum4c: 
-        "(sinl$x << sinr$y) = (x = UU)"
-apply (unfold sinl_def sinr_def)
-apply (simplesubst beta_cfun)
-apply (rule cont_Isinr)
-apply (subst beta_cfun)
-apply (rule cont_Isinl)
-apply (rule less_ssum2c)
+lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
+apply (rule iffI)
+apply (erule less_cprod5c)
+apply (simp add: monofun_cfun)
 done
 
-lemma less_ssum4d: 
-        "(sinr$x << sinl$y) = (x = UU)"
-apply (unfold sinl_def sinr_def)
-apply (simplesubst beta_cfun)
-apply (rule cont_Isinl)
-apply (subst beta_cfun)
-apply (rule cont_Isinr)
-apply (rule less_ssum2d)
-done
+lemma less_ssum4a: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
+by (simp add: less_ssum_def Rep_Ssum_sinl cpair_less)
+
+lemma less_ssum4b: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
+by (simp add: less_ssum_def Rep_Ssum_sinr cpair_less)
+
+lemma less_ssum4c: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
+by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
 
-lemma ssum_chainE: 
-        "chain(Y) ==> (!i.? x.(Y i)=sinl$x)|(!i.? y.(Y i)=sinr$y)"
-apply (unfold sinl_def sinr_def)
-apply simp
-apply (erule ssum_lemma4)
+lemma less_ssum4d: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
+by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+
+subsection {* Chains of strict sums *}
+
+lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
+apply (rule_tac p=p in ssumE)
+apply (rule_tac x="\<bottom>" in exI, simp)
+apply (simp add: less_ssum4a sinl_eq)
+apply (simp add: less_ssum4d)
 done
 
-lemma thelub_ssum2a: 
-"[| chain(Y); !i.? x. Y(i) = sinl$x |] ==>  
-    lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))"
-apply (unfold sinl_def sinr_def sscase_def)
-apply (subst beta_cfun)
-apply (rule cont_Isinl)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun [THEN ext])
-apply (intro ssum_conts)
-apply (rule thelub_ssum1a)
-apply assumption
-apply (rule allI)
-apply (erule allE)
-apply (erule exE)
-apply (rule exI)
-apply (erule box_equals)
-apply (rule refl)
-apply simp
+lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
+apply (rule_tac p=p in ssumE)
+apply (rule_tac x="\<bottom>" in exI, simp)
+apply (simp add: less_ssum4c)
+apply (simp add: less_ssum4b sinr_eq)
+done
+
+lemma ssum_chain_lemma:
+"chain Y \<Longrightarrow> (\<exists>A. chain A \<and> Y = (\<lambda>i. sinl\<cdot>(A i))) \<or>
+             (\<exists>B. chain B \<and> Y = (\<lambda>i. sinr\<cdot>(B i)))"
+ apply (rule_tac p="lub (range Y)" in ssumE2)
+  apply (rule disjI1)
+  apply (rule_tac x="\<lambda>i. cfst\<cdot>(Rep_Ssum (Y i))" in exI)
+  apply (rule conjI)
+   apply (rule chain_monofun)
+   apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun])
+  apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
+  apply (drule less_sinlD, clarify)
+  apply (simp add: sinl_eq Rep_Ssum_sinl)
+ apply (rule disjI2)
+ apply (rule_tac x="\<lambda>i. csnd\<cdot>(Rep_Ssum (Y i))" in exI)
+ apply (rule conjI)
+  apply (rule chain_monofun)
+  apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun])
+ apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
+ apply (drule less_sinrD, clarify)
+ apply (simp add: sinr_eq Rep_Ssum_sinr)
 done
 
-lemma thelub_ssum2b: 
-"[| chain(Y); !i.? x. Y(i) = sinr$x |] ==>  
-    lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"
-apply (unfold sinl_def sinr_def sscase_def)
-apply (subst beta_cfun)
-apply (rule cont_Isinr)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun)
-apply (intro ssum_conts)
-apply (subst beta_cfun [THEN ext])
-apply (intro ssum_conts)
-apply (rule thelub_ssum1b)
-apply assumption
-apply (rule allI)
-apply (erule allE)
-apply (erule exE)
-apply (rule exI)
-apply (erule box_equals)
-apply (rule refl)
-apply simp
-done
+subsection {* Definitions of constants *}
+
+constdefs
+  Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c"
+  "Iwhen \<equiv> \<lambda>f g s.
+    if cfst\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then f\<cdot>(cfst\<cdot>(Rep_Ssum s)) else
+    if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>"
+
+text {* rewrites for @{term Iwhen} *}
+
+lemma Iwhen1 [simp]: "Iwhen f g \<bottom> = \<bottom>"
+by (simp add: Iwhen_def strict_Rep_Ssum)
+
+lemma Iwhen2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinl\<cdot>x) = f\<cdot>x"
+by (simp add: Iwhen_def Rep_Ssum_sinl)
+
+lemma Iwhen3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinr\<cdot>y) = g\<cdot>y"
+by (simp add: Iwhen_def Rep_Ssum_sinr)
+
+lemma Iwhen4: "Iwhen f g (sinl\<cdot>x) = strictify\<cdot>f\<cdot>x"
+by (case_tac "x = \<bottom>", simp_all)
 
-lemma thelub_ssum2a_rev: 
-        "[| chain(Y); lub(range(Y)) = sinl$x|] ==> !i.? x. Y(i)=sinl$x"
-apply (unfold sinl_def sinr_def)
-apply simp
-apply (erule ssum_lemma9)
-apply simp
+lemma Iwhen5: "Iwhen f g (sinr\<cdot>y) = strictify\<cdot>g\<cdot>y"
+by (case_tac "y = \<bottom>" , simp_all)
+
+subsection {* Continuity of @{term Iwhen} *}
+
+text {* @{term Iwhen} is continuous in all arguments *}
+
+lemma cont_Iwhen1: "cont (\<lambda>f. Iwhen f g s)"
+by (rule_tac p=s in ssumE, simp_all)
+
+lemma cont_Iwhen2: "cont (\<lambda>g. Iwhen f g s)"
+by (rule_tac p=s in ssumE, simp_all)
+
+lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)"
+apply (rule contI [rule_format])
+apply (drule ssum_chain_lemma, safe)
+apply (simp add: contlub_cfun_arg [symmetric])
+apply (simp add: Iwhen4)
+apply (simp add: contlub_cfun_arg)
+apply (simp add: thelubE chain_monofun)
+apply (simp add: contlub_cfun_arg [symmetric])
+apply (simp add: Iwhen5)
+apply (simp add: contlub_cfun_arg)
+apply (simp add: thelubE chain_monofun)
 done
 
-lemma thelub_ssum2b_rev: 
-     "[| chain(Y); lub(range(Y)) = sinr$x|] ==> !i.? x. Y(i)=sinr$x"
-apply (unfold sinl_def sinr_def)
-apply simp
-apply (erule ssum_lemma10)
-apply simp
-done
+subsection {* Continuous versions of constants *}
+
+constdefs
+  sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c"
+  "sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
+
+translations
+"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
+
+text {* continuous versions of lemmas for @{term sscase} *}
 
-lemma thelub_ssum3: "chain(Y) ==>  
-    lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i)))) 
-  | lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"
-apply (rule ssum_chainE [THEN disjE])
-apply assumption
-apply (rule disjI1)
-apply (erule thelub_ssum2a)
-apply assumption
-apply (rule disjI2)
-apply (erule thelub_ssum2b)
-apply assumption
-done
+lemma beta_sscase: "sscase\<cdot>f\<cdot>g\<cdot>s = Iwhen f g s"
+by (simp add: sscase_def cont_Iwhen1 cont_Iwhen2 cont_Iwhen3)
+
+lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
+by (simp add: beta_sscase)
 
-lemma sscase4: "sscase$sinl$sinr$z=z"
-apply (rule_tac p = "z" in ssumE)
-apply auto
-done
-
-text {* install simplifier for Ssum *}
+lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>x"
+by (simp add: beta_sscase)
 
-lemmas Ssum_rews = strict_sinl strict_sinr defined_sinl defined_sinr
-                sscase1 sscase2 sscase3
-
-text {* for backward compatibility *}
+lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<cdot>y"
+by (simp add: beta_sscase)
 
-lemmas less_ssum3a = less_ssum2a
-lemmas less_ssum3b = less_ssum2b
-lemmas less_ssum3c = less_ssum2c
-lemmas less_ssum3d = less_ssum2d
+lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
+by (rule_tac p=z in ssumE, simp_all)
 
 end