# HG changeset patch
# User huffman
# Date 1109806924 -3600
# Node ID 60743edae74a183a5c2c5bdabedd320a0d8be8b6
# Parent  eb3b1a5c304e65250b58c993801f5ff6d7f37636
converted to new-style theory

diff -r eb3b1a5c304e -r 60743edae74a src/HOLCF/Sprod0.ML
--- a/src/HOLCF/Sprod0.ML	Wed Mar 02 23:58:02 2005 +0100
+++ b/src/HOLCF/Sprod0.ML	Thu Mar 03 00:42:04 2005 +0100
@@ -1,302 +1,35 @@
-(*  Title:      HOLCF/Sprod0
-    ID:         $Id$
-    Author:     Franz Regensburger
 
-Strict product with typedef.
-*)
-
-(* ------------------------------------------------------------------------ *)
-(* A non-emptyness result for Sprod                                         *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [Sprod_def] "(Spair_Rep a b):Sprod";
-by (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl]);
-qed "SprodI";
-
-Goal "inj_on Abs_Sprod Sprod";
-by (rtac inj_on_inverseI 1);
-by (etac Abs_Sprod_inverse 1);
-qed "inj_on_Abs_Sprod";
-
-(* ------------------------------------------------------------------------ *)
-(* Strictness and definedness of Spair_Rep                                  *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [Spair_Rep_def]
- "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)";
-by (rtac ext 1);
-by (rtac ext 1);
-by (rtac iffI 1);
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
-qed "strict_Spair_Rep";
-
-Goalw [Spair_Rep_def]
- "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)";
-by (case_tac "a=UU|b=UU" 1);
-by (atac 1);
-by (fast_tac (claset() addDs [fun_cong]) 1);
-qed "defined_Spair_Rep_rev";
-
-(* ------------------------------------------------------------------------ *)
-(* injectivity of Spair_Rep and Ispair                                      *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [Spair_Rep_def]
-"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba";
-by (dtac fun_cong 1);
-by (dtac fun_cong 1);
-by (etac (iffD1 RS mp) 1);
-by Auto_tac;  
-qed "inject_Spair_Rep";
-
-
-Goalw [Ispair_def]
-        "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba";
-by (etac inject_Spair_Rep 1);
-by (atac 1);
-by (etac (inj_on_Abs_Sprod  RS inj_onD) 1);
-by (rtac SprodI 1);
-by (rtac SprodI 1);
-qed "inject_Ispair";
-
-
-(* ------------------------------------------------------------------------ *)
-(* strictness and definedness of Ispair                                     *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [Ispair_def] 
- "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU";
-by (etac (strict_Spair_Rep RS arg_cong) 1);
-qed "strict_Ispair";
-
-Goalw [Ispair_def]
-        "Ispair UU b  = Ispair UU UU";
-by (rtac (strict_Spair_Rep RS arg_cong) 1);
-by (rtac disjI1 1);
-by (rtac refl 1);
-qed "strict_Ispair1";
-
-Goalw [Ispair_def]
-        "Ispair a UU = Ispair UU UU";
-by (rtac (strict_Spair_Rep RS arg_cong) 1);
-by (rtac disjI2 1);
-by (rtac refl 1);
-qed "strict_Ispair2";
-
-Goal "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU";
-by (rtac (de_Morgan_disj RS subst) 1);
-by (etac contrapos_nn 1);
-by (etac strict_Ispair 1);
-qed "strict_Ispair_rev";
-
-Goalw [Ispair_def]
-        "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)";
-by (rtac defined_Spair_Rep_rev 1);
-by (rtac (inj_on_Abs_Sprod  RS inj_onD) 1);
-by (atac 1);
-by (rtac SprodI 1);
-by (rtac SprodI 1);
-qed "defined_Ispair_rev";
-
-Goal "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)";
-by (rtac contrapos_nn 1);
-by (etac defined_Ispair_rev 2);
-by (rtac (de_Morgan_disj RS iffD2) 1);
-by (etac conjI 1);
-by (atac 1);
-qed "defined_Ispair";
-
-
-(* ------------------------------------------------------------------------ *)
-(* Exhaustion of the strict product **                                      *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [Ispair_def]
-        "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)";
-by (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1);
-by (etac exE 1);
-by (etac exE 1);
-by (rtac (excluded_middle RS disjE) 1);
-by (rtac disjI2 1);
-by (rtac exI 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (rtac (Rep_Sprod_inverse RS sym RS trans) 1);
-by (etac arg_cong 1);
-by (rtac (de_Morgan_disj RS subst) 1);
-by (atac 1);
-by (rtac disjI1 1);
-by (rtac (Rep_Sprod_inverse RS sym RS trans) 1);
-by (res_inst_tac [("f","Abs_Sprod")] arg_cong 1);
-by (etac trans 1);
-by (etac strict_Spair_Rep 1);
-qed "Exh_Sprod";
-
-(* ------------------------------------------------------------------------ *)
-(* general elimination rule for strict product                              *)
-(* ------------------------------------------------------------------------ *)
+(* legacy ML bindings *)
 
-val [prem1,prem2] = Goal
-"  [| p=Ispair UU UU ==> Q ; !!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] \
-\  ==> Q";
-by (rtac (Exh_Sprod RS disjE) 1);
-by (etac prem1 1);
-by (etac exE 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (etac conjE 1);
-by (etac prem2 1);
-by (atac 1);
-by (atac 1);
-qed "IsprodE";
-
-
-(* ------------------------------------------------------------------------ *)
-(* some results about the selectors Isfst, Issnd                            *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [Isfst_def] "p=Ispair UU UU ==> Isfst p = UU";
-by (rtac some_equality 1);
-by (rtac conjI 1);
-by (fast_tac HOL_cs  1);
-by (strip_tac 1);
-by (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1);
-by (rtac not_sym 1);
-by (rtac defined_Ispair 1);
-by (REPEAT (fast_tac HOL_cs  1));
-qed "strict_Isfst";
-
-
-Goal "Isfst(Ispair UU y) = UU";
-by (stac strict_Ispair1 1);
-by (rtac strict_Isfst 1);
-by (rtac refl 1);
-qed "strict_Isfst1";
-
-Addsimps [strict_Isfst1];
-
-Goal "Isfst(Ispair x UU) = UU";
-by (stac strict_Ispair2 1);
-by (rtac strict_Isfst 1);
-by (rtac refl 1);
-qed "strict_Isfst2";
-
-Addsimps [strict_Isfst2];
-
-
-Goalw [Issnd_def] "p=Ispair UU UU ==>Issnd p=UU";
-by (rtac some_equality 1);
-by (rtac conjI 1);
-by (fast_tac HOL_cs  1);
-by (strip_tac 1);
-by (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1);
-by (rtac not_sym 1);
-by (rtac defined_Ispair 1);
-by (REPEAT (fast_tac HOL_cs  1));
-qed "strict_Issnd";
-
-Goal "Issnd(Ispair UU y) = UU";
-by (stac strict_Ispair1 1);
-by (rtac strict_Issnd 1);
-by (rtac refl 1);
-qed "strict_Issnd1";
-
-Addsimps [strict_Issnd1];
-
-Goal "Issnd(Ispair x UU) = UU";
-by (stac strict_Ispair2 1);
-by (rtac strict_Issnd 1);
-by (rtac refl 1);
-qed "strict_Issnd2";
-
-Addsimps [strict_Issnd2];
-
-Goalw [Isfst_def] "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x";
-by (rtac some_equality 1);
-by (rtac conjI 1);
-by (strip_tac 1);
-by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
-by (etac defined_Ispair 1);
-by (atac 1);
-by (atac 1);
-by (strip_tac 1);
-by (rtac (inject_Ispair RS conjunct1) 1);
-by (fast_tac HOL_cs  3);
-by (fast_tac HOL_cs  1);
-by (fast_tac HOL_cs  1);
-by (fast_tac HOL_cs  1);
-qed "Isfst";
-
-Goalw [Issnd_def] "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y";
-by (rtac some_equality 1);
-by (rtac conjI 1);
-by (strip_tac 1);
-by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
-by (etac defined_Ispair 1);
-by (atac 1);
-by (atac 1);
-by (strip_tac 1);
-by (rtac (inject_Ispair RS conjunct2) 1);
-by (fast_tac HOL_cs  3);
-by (fast_tac HOL_cs  1);
-by (fast_tac HOL_cs  1);
-by (fast_tac HOL_cs  1);
-qed "Issnd";
-
-Goal "y~=UU ==>Isfst(Ispair x y)=x";
-by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
-by (etac Isfst 1);
-by (atac 1);
-by (hyp_subst_tac 1);
-by (rtac strict_Isfst1 1);
-qed "Isfst2";
-
-Goal "~x=UU ==>Issnd(Ispair x y)=y";
-by (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1);
-by (etac Issnd 1);
-by (atac 1);
-by (hyp_subst_tac 1);
-by (rtac strict_Issnd2 1);
-qed "Issnd2";
-
-
-(* ------------------------------------------------------------------------ *)
-(* instantiate the simplifier                                               *)
-(* ------------------------------------------------------------------------ *)
-
-val Sprod0_ss = 
-        HOL_ss 
-        addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
-                 Isfst2,Issnd2];
-
-Addsimps [Isfst2,Issnd2];
-
-Goal "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU";
-by (res_inst_tac [("p","p")] IsprodE 1);
-by (contr_tac 1);
-by (hyp_subst_tac 1);
-by (rtac conjI 1);
-by (asm_simp_tac Sprod0_ss 1);
-by (asm_simp_tac Sprod0_ss 1);
-qed "defined_IsfstIssnd";
-
-
-(* ------------------------------------------------------------------------ *)
-(* Surjective pairing: equivalent to Exh_Sprod                              *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "z = Ispair(Isfst z)(Issnd z)";
-by (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1);
-by (asm_simp_tac Sprod0_ss 1);
-by (etac exE 1);
-by (etac exE 1);
-by (asm_simp_tac Sprod0_ss 1);
-qed "surjective_pairing_Sprod";
-
-Goal "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y";
-by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1);
-by (rotate_tac ~1 1);
-by (asm_lr_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1);
-by (Asm_simp_tac 1);
-qed "Sel_injective_Sprod";
+val Ispair_def = thm "Ispair_def";
+val Isfst_def = thm "Isfst_def";
+val Issnd_def = thm "Issnd_def";
+val SprodI = thm "SprodI";
+val inj_on_Abs_Sprod = thm "inj_on_Abs_Sprod";
+val strict_Spair_Rep = thm "strict_Spair_Rep";
+val defined_Spair_Rep_rev = thm "defined_Spair_Rep_rev";
+val inject_Spair_Rep = thm "inject_Spair_Rep";
+val inject_Ispair = thm "inject_Ispair";
+val strict_Ispair = thm "strict_Ispair";
+val strict_Ispair1 = thm "strict_Ispair1";
+val strict_Ispair2 = thm "strict_Ispair2";
+val strict_Ispair_rev = thm "strict_Ispair_rev";
+val defined_Ispair_rev = thm "defined_Ispair_rev";
+val defined_Ispair = thm "defined_Ispair";
+val Exh_Sprod = thm "Exh_Sprod";
+val IsprodE = thm "IsprodE";
+val strict_Isfst = thm "strict_Isfst";
+val strict_Isfst1 = thm "strict_Isfst1";
+val strict_Isfst2 = thm "strict_Isfst2";
+val strict_Issnd = thm "strict_Issnd";
+val strict_Issnd1 = thm "strict_Issnd1";
+val strict_Issnd2 = thm "strict_Issnd2";
+val Isfst = thm "Isfst";
+val Issnd = thm "Issnd";
+val Isfst2 = thm "Isfst2";
+val Issnd2 = thm "Issnd2";
+val Sprod0_ss = [strict_Isfst1, strict_Isfst2, strict_Issnd1, strict_Issnd2,
+                 Isfst2, Issnd2]
+val defined_IsfstIssnd = thm "defined_IsfstIssnd";
+val surjective_pairing_Sprod = thm "surjective_pairing_Sprod";
+val Sel_injective_Sprod = thm "Sel_injective_Sprod";
diff -r eb3b1a5c304e -r 60743edae74a src/HOLCF/Sprod0.thy
--- a/src/HOLCF/Sprod0.thy	Wed Mar 02 23:58:02 2005 +0100
+++ b/src/HOLCF/Sprod0.thy	Thu Mar 03 00:42:04 2005 +0100
@@ -1,22 +1,24 @@
 (*  Title:      HOLCF/Sprod0.thy
     ID:         $Id$
     Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Strict product with typedef.
 *)
 
-Sprod0 = Cfun3 +
+theory Sprod0 = Cfun3:
 
 constdefs
-  Spair_Rep     :: ['a,'b] => ['a,'b] => bool
+  Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
  "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
 
 typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
+by auto
 
 syntax (xsymbols)
-  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
+  "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
 syntax (HTML output)
-  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
+  "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
 
 consts
   Ispair        :: "['a,'b] => ('a ** 'b)"
@@ -26,13 +28,326 @@
 defs
    (*defining the abstract constants*)
 
-  Ispair_def    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
+  Ispair_def:    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
 
-  Isfst_def     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
+  Isfst_def:     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
 
-  Issnd_def     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
+  Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
 
+(*  Title:      HOLCF/Sprod0
+    ID:         $Id$
+    Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Strict product with typedef.
+*)
+
+(* ------------------------------------------------------------------------ *)
+(* A non-emptyness result for Sprod                                         *)
+(* ------------------------------------------------------------------------ *)
+
+lemma SprodI: "(Spair_Rep a b):Sprod"
+apply (unfold Sprod_def)
+apply (rule CollectI, rule exI, rule exI, rule refl)
+done
+
+lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod"
+apply (rule inj_on_inverseI)
+apply (erule Abs_Sprod_inverse)
+done
+
+(* ------------------------------------------------------------------------ *)
+(* Strictness and definedness of Spair_Rep                                  *)
+(* ------------------------------------------------------------------------ *)
+
+lemma strict_Spair_Rep: 
+ "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
+apply (unfold Spair_Rep_def)
+apply (rule ext)
+apply (rule ext)
+apply (rule iffI)
+apply fast
+apply fast
+done
+
+lemma defined_Spair_Rep_rev: 
+ "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
+apply (unfold Spair_Rep_def)
+apply (case_tac "a=UU|b=UU")
+apply assumption
+apply (fast dest: fun_cong)
+done
+
+(* ------------------------------------------------------------------------ *)
+(* injectivity of Spair_Rep and Ispair                                      *)
+(* ------------------------------------------------------------------------ *)
+
+lemma inject_Spair_Rep: 
+"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
+
+apply (unfold Spair_Rep_def)
+apply (drule fun_cong)
+apply (drule fun_cong)
+apply (erule iffD1 [THEN mp])
+apply auto
+done
+
+
+lemma inject_Ispair: 
+        "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
+apply (unfold Ispair_def)
+apply (erule inject_Spair_Rep)
+apply assumption
+apply (erule inj_on_Abs_Sprod [THEN inj_onD])
+apply (rule SprodI)
+apply (rule SprodI)
+done
+
+
+(* ------------------------------------------------------------------------ *)
+(* strictness and definedness of Ispair                                     *)
+(* ------------------------------------------------------------------------ *)
+
+lemma strict_Ispair: 
+ "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
+apply (unfold Ispair_def)
+apply (erule strict_Spair_Rep [THEN arg_cong])
+done
+
+lemma strict_Ispair1: 
+        "Ispair UU b  = Ispair UU UU"
+apply (unfold Ispair_def)
+apply (rule strict_Spair_Rep [THEN arg_cong])
+apply (rule disjI1)
+apply (rule refl)
+done
+
+lemma strict_Ispair2: 
+        "Ispair a UU = Ispair UU UU"
+apply (unfold Ispair_def)
+apply (rule strict_Spair_Rep [THEN arg_cong])
+apply (rule disjI2)
+apply (rule refl)
+done
+
+lemma strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
+apply (rule de_Morgan_disj [THEN subst])
+apply (erule contrapos_nn)
+apply (erule strict_Ispair)
+done
+
+lemma defined_Ispair_rev: 
+        "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
+apply (unfold Ispair_def)
+apply (rule defined_Spair_Rep_rev)
+apply (rule inj_on_Abs_Sprod [THEN inj_onD])
+apply assumption
+apply (rule SprodI)
+apply (rule SprodI)
+done
+
+lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)"
+apply (rule contrapos_nn)
+apply (erule_tac [2] defined_Ispair_rev)
+apply (rule de_Morgan_disj [THEN iffD2])
+apply (erule conjI)
+apply assumption
+done
+
+
+(* ------------------------------------------------------------------------ *)
+(* Exhaustion of the strict product **                                      *)
+(* ------------------------------------------------------------------------ *)
+
+lemma Exh_Sprod:
+        "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
+apply (unfold Ispair_def)
+apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE])
+apply (erule exE)
+apply (erule exE)
+apply (rule excluded_middle [THEN disjE])
+apply (rule disjI2)
+apply (rule exI)
+apply (rule exI)
+apply (rule conjI)
+apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
+apply (erule arg_cong)
+apply (rule de_Morgan_disj [THEN subst])
+apply assumption
+apply (rule disjI1)
+apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
+apply (rule_tac f = "Abs_Sprod" in arg_cong)
+apply (erule trans)
+apply (erule strict_Spair_Rep)
+done
+
+(* ------------------------------------------------------------------------ *)
+(* general elimination rule for strict product                              *)
+(* ------------------------------------------------------------------------ *)
+
+lemma IsprodE:
+assumes prem1: "p=Ispair UU UU ==> Q"
+assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q"
+shows "Q"
+apply (rule Exh_Sprod [THEN disjE])
+apply (erule prem1)
+apply (erule exE)
+apply (erule exE)
+apply (erule conjE)
+apply (erule conjE)
+apply (erule prem2)
+apply assumption
+apply assumption
+done
+
+
+(* ------------------------------------------------------------------------ *)
+(* some results about the selectors Isfst, Issnd                            *)
+(* ------------------------------------------------------------------------ *)
+
+lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
+apply (unfold Isfst_def)
+apply (rule some_equality)
+apply (rule conjI)
+apply fast
+apply (intro strip)
+apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
+apply (rule not_sym)
+apply (rule defined_Ispair)
+apply (fast+)
+done
+
+
+lemma strict_Isfst1: "Isfst(Ispair UU y) = UU"
+apply (subst strict_Ispair1)
+apply (rule strict_Isfst)
+apply (rule refl)
+done
+
+declare strict_Isfst1 [simp]
+
+lemma strict_Isfst2: "Isfst(Ispair x UU) = UU"
+apply (subst strict_Ispair2)
+apply (rule strict_Isfst)
+apply (rule refl)
+done
+
+declare strict_Isfst2 [simp]
+
+
+lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
+
+apply (unfold Issnd_def)
+apply (rule some_equality)
+apply (rule conjI)
+apply fast
+apply (intro strip)
+apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
+apply (rule not_sym)
+apply (rule defined_Ispair)
+apply (fast+)
+done
+
+lemma strict_Issnd1: "Issnd(Ispair UU y) = UU"
+apply (subst strict_Ispair1)
+apply (rule strict_Issnd)
+apply (rule refl)
+done
+
+declare strict_Issnd1 [simp]
+
+lemma strict_Issnd2: "Issnd(Ispair x UU) = UU"
+apply (subst strict_Ispair2)
+apply (rule strict_Issnd)
+apply (rule refl)
+done
+
+declare strict_Issnd2 [simp]
+
+lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
+apply (unfold Isfst_def)
+apply (rule some_equality)
+apply (rule conjI)
+apply (intro strip)
+apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
+apply (erule defined_Ispair)
+apply assumption
+apply assumption
+apply (intro strip)
+apply (rule inject_Ispair [THEN conjunct1])
+prefer 3 apply fast
+apply (fast+)
+done
+
+lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
+apply (unfold Issnd_def)
+apply (rule some_equality)
+apply (rule conjI)
+apply (intro strip)
+apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
+apply (erule defined_Ispair)
+apply assumption
+apply assumption
+apply (intro strip)
+apply (rule inject_Ispair [THEN conjunct2])
+prefer 3 apply fast
+apply (fast+)
+done
+
+lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x"
+apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
+apply (erule Isfst)
+apply assumption
+apply (erule ssubst)
+apply (rule strict_Isfst1)
+done
+
+lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y"
+apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE])
+apply (erule Issnd)
+apply assumption
+apply (erule ssubst)
+apply (rule strict_Issnd2)
+done
+
+
+(* ------------------------------------------------------------------------ *)
+(* instantiate the simplifier                                               *)
+(* ------------------------------------------------------------------------ *)
+
+lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
+                 Isfst2 Issnd2
+
+declare Isfst2 [simp] Issnd2 [simp]
+
+lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
+apply (rule_tac p = "p" in IsprodE)
+apply simp
+apply (erule ssubst)
+apply (rule conjI)
+apply (simp add: Sprod0_ss)
+apply (simp add: Sprod0_ss)
+done
+
+
+(* ------------------------------------------------------------------------ *)
+(* Surjective pairing: equivalent to Exh_Sprod                              *)
+(* ------------------------------------------------------------------------ *)
+
+lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
+apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
+apply (simp add: Sprod0_ss)
+apply (erule exE)
+apply (erule exE)
+apply (simp add: Sprod0_ss)
+done
+
+lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
+apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ")
+apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric])
+apply simp
+done
 
 end
diff -r eb3b1a5c304e -r 60743edae74a src/HOLCF/Sprod1.ML
--- a/src/HOLCF/Sprod1.ML	Wed Mar 02 23:58:02 2005 +0100
+++ b/src/HOLCF/Sprod1.ML	Thu Mar 03 00:42:04 2005 +0100
@@ -1,24 +1,7 @@
-(*  Title:      HOLCF/Sprod1.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-*)
 
-(* ------------------------------------------------------------------------ *)
-(* less_sprod is a partial order on Sprod                                   *)
-(* ------------------------------------------------------------------------ *)
+(* legacy ML bindings *)
 
-Goalw [less_sprod_def]"(p::'a ** 'b) << p";
-by (fast_tac (HOL_cs addIs [refl_less]) 1);
-qed "refl_less_sprod";
-
-Goalw [less_sprod_def]
-        "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2";
-by (rtac Sel_injective_Sprod 1);
-by (fast_tac (HOL_cs addIs [antisym_less]) 1);
-by (fast_tac (HOL_cs addIs [antisym_less]) 1);
-qed "antisym_less_sprod";
-
-Goalw [less_sprod_def]
-        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3";
-by (blast_tac (HOL_cs addIs [trans_less]) 1);
-qed "trans_less_sprod";
+val less_sprod_def = thm "less_sprod_def";
+val refl_less_sprod = thm "refl_less_sprod";
+val antisym_less_sprod = thm "antisym_less_sprod";
+val trans_less_sprod = thm "trans_less_sprod";
diff -r eb3b1a5c304e -r 60743edae74a src/HOLCF/Sprod1.thy
--- a/src/HOLCF/Sprod1.thy	Wed Mar 02 23:58:02 2005 +0100
+++ b/src/HOLCF/Sprod1.thy	Thu Mar 03 00:42:04 2005 +0100
@@ -1,15 +1,46 @@
 (*  Title:      HOLCF/sprod1.thy
     ID:         $Id$
     Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Partial ordering for the strict product.
 *)
 
-Sprod1 = Sprod0 +
+theory Sprod1 = Sprod0:
+
+instance "**"::(sq_ord,sq_ord)sq_ord ..
+
+defs (overloaded)
+  less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
+
+(*  Title:      HOLCF/Sprod1.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+(* ------------------------------------------------------------------------ *)
+(* less_sprod is a partial order on Sprod                                   *)
+(* ------------------------------------------------------------------------ *)
 
-instance "**"::(sq_ord,sq_ord)sq_ord 
+lemma refl_less_sprod: "(p::'a ** 'b) << p"
+
+apply (unfold less_sprod_def)
+apply (fast intro: refl_less)
+done
 
-defs
-  less_sprod_def "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
+lemma antisym_less_sprod: 
+        "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
+apply (unfold less_sprod_def)
+apply (rule Sel_injective_Sprod)
+apply (fast intro: antisym_less)
+apply (fast intro: antisym_less)
+done
+
+lemma trans_less_sprod: 
+        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
+apply (unfold less_sprod_def)
+apply (blast intro: trans_less)
+done
 
 end
diff -r eb3b1a5c304e -r 60743edae74a src/HOLCF/Sprod2.ML
--- a/src/HOLCF/Sprod2.ML	Wed Mar 02 23:58:02 2005 +0100
+++ b/src/HOLCF/Sprod2.ML	Thu Mar 03 00:42:04 2005 +0100
@@ -1,106 +1,15 @@
-(*  Title:      HOLCF/Sprod2.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
 
-Class Instance **::(pcpo,pcpo)po
-*)
-
-(* for compatibility with old HOLCF-Version *)
-Goal "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)";
-by (fold_goals_tac [less_sprod_def]);
-by (rtac refl 1);
-qed "inst_sprod_po";
-
-(* ------------------------------------------------------------------------ *)
-(* type sprod is pointed                                                    *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "Ispair UU UU << p";
-by (simp_tac(Sprod0_ss addsimps[inst_sprod_po,minimal])1);
-qed "minimal_sprod";
-
-bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
-
-Goal "? x::'a**'b.!y. x<<y";
-by (res_inst_tac [("x","Ispair UU UU")] exI 1);
-by (rtac (minimal_sprod RS allI) 1);
-qed "least_sprod";
-
-(* ------------------------------------------------------------------------ *)
-(* Ispair is monotone in both arguments                                     *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [monofun]  "monofun(Ispair)";
-by (strip_tac 1);
-by (rtac (less_fun RS iffD2) 1);
-by (strip_tac 1);
-by (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1);
-by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
-by (ftac notUU_I 1);
-by (atac 1);
-by (REPEAT(asm_simp_tac(Sprod0_ss addsimps[inst_sprod_po,refl_less,minimal]) 1));
-qed "monofun_Ispair1";
-
-Goalw [monofun]  "monofun(Ispair(x))";
-by (strip_tac 1);
-by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
-by (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1);
-by (ftac notUU_I 1);
-by (atac 1);
-by (REPEAT(asm_simp_tac(Sprod0_ss addsimps[inst_sprod_po,refl_less,minimal]) 1));
-qed "monofun_Ispair2";      
+(* legacy ML bindings *)
 
-Goal "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2";
-by (rtac trans_less 1);
-by (rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS 
-        (less_fun RS iffD1 RS spec)) 1);
-by (rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2);
-by (atac 1);
-by (atac 1);
-qed "monofun_Ispair";
-
-(* ------------------------------------------------------------------------ *)
-(* Isfst and Issnd are monotone                                             *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [monofun]  "monofun(Isfst)";
-by (simp_tac (HOL_ss addsimps [inst_sprod_po]) 1);
-qed "monofun_Isfst";
-
-Goalw [monofun]  "monofun(Issnd)";
-by (simp_tac (HOL_ss addsimps [inst_sprod_po]) 1);
-qed "monofun_Issnd";
-
-(* ------------------------------------------------------------------------ *)
-(* the type 'a ** 'b is a cpo                                               *)
-(* ------------------------------------------------------------------------ *)
-
-Goal 
-"[|chain(S)|] ==> range(S) <<| \
-\ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))";
-by (rtac (is_lubI) 1);
-by (rtac (ub_rangeI) 1);
-by (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1);
-by (rtac monofun_Ispair 1);
-by (rtac is_ub_thelub 1);
-by (etac (monofun_Isfst RS ch2ch_monofun) 1);
-by (rtac is_ub_thelub 1);
-by (etac (monofun_Issnd RS ch2ch_monofun) 1);
-by (strip_tac 1);
-by (res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1);
-by (rtac monofun_Ispair 1);
-by (rtac is_lub_thelub 1);
-by (etac (monofun_Isfst RS ch2ch_monofun) 1);
-by (etac (monofun_Isfst RS ub2ub_monofun) 1);
-by (rtac is_lub_thelub 1);
-by (etac (monofun_Issnd RS ch2ch_monofun) 1);
-by (etac (monofun_Issnd RS ub2ub_monofun) 1);
-qed "lub_sprod";
-
-bind_thm ("thelub_sprod", lub_sprod RS thelubI);
-
-
-Goal "chain(S::nat=>'a**'b)==>? x. range(S)<<| x";
-by (rtac exI 1);
-by (etac lub_sprod 1);
-qed "cpo_sprod";
+val inst_sprod_po = thm "inst_sprod_po";
+val minimal_sprod = thm "minimal_sprod";
+val UU_sprod_def = thm "UU_sprod_def";
+val least_sprod = thm "least_sprod";
+val monofun_Ispair1 = thm "monofun_Ispair1";
+val monofun_Ispair2 = thm "monofun_Ispair2";
+val monofun_Ispair = thm "monofun_Ispair";
+val monofun_Isfst = thm "monofun_Isfst";
+val monofun_Issnd = thm "monofun_Issnd";
+val lub_sprod = thm "lub_sprod";
+val thelub_sprod = thm "thelub_sprod";
+val cpo_sprod = thm "cpo_sprod";
diff -r eb3b1a5c304e -r 60743edae74a src/HOLCF/Sprod2.thy
--- a/src/HOLCF/Sprod2.thy	Wed Mar 02 23:58:02 2005 +0100
+++ b/src/HOLCF/Sprod2.thy	Thu Mar 03 00:42:04 2005 +0100
@@ -1,14 +1,132 @@
 (*  Title:      HOLCF/Sprod2.thy
     ID:         $Id$
     Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Class Instance **::(pcpo,pcpo)po
+*)
+
+theory Sprod2 = Sprod1:
+
+instance "**"::(pcpo,pcpo)po 
+apply (intro_classes)
+apply (rule refl_less_sprod)
+apply (rule antisym_less_sprod, assumption+)
+apply (rule trans_less_sprod, assumption+)
+done
+
+(*  Title:      HOLCF/Sprod2.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class Instance **::(pcpo,pcpo)po
 *)
 
-Sprod2 = Sprod1 + 
+(* for compatibility with old HOLCF-Version *)
+lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
+apply (fold less_sprod_def)
+apply (rule refl)
+done
+
+(* ------------------------------------------------------------------------ *)
+(* type sprod is pointed                                                    *)
+(* ------------------------------------------------------------------------ *)
+
+lemma minimal_sprod: "Ispair UU UU << p"
+apply (simp add: inst_sprod_po minimal)
+done
+
+lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
+
+lemma least_sprod: "? x::'a**'b.!y. x<<y"
+apply (rule_tac x = "Ispair UU UU" in exI)
+apply (rule minimal_sprod [THEN allI])
+done
+
+(* ------------------------------------------------------------------------ *)
+(* Ispair is monotone in both arguments                                     *)
+(* ------------------------------------------------------------------------ *)
+
+lemma monofun_Ispair1: "monofun(Ispair)"
+
+apply (unfold monofun)
+apply (intro strip)
+apply (rule less_fun [THEN iffD2])
+apply (intro strip)
+apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
+apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
+apply (frule notUU_I)
+apply assumption
+apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
+done
+
+lemma monofun_Ispair2: "monofun(Ispair(x))"
+apply (unfold monofun)
+apply (intro strip)
+apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
+apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
+apply (frule notUU_I)
+apply assumption
+apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
+done
 
-instance "**"::(pcpo,pcpo)po 
-		(refl_less_sprod, antisym_less_sprod, trans_less_sprod)
+lemma monofun_Ispair: "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
+apply (rule trans_less)
+apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
+prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
+apply assumption
+apply assumption
+done
+
+(* ------------------------------------------------------------------------ *)
+(* Isfst and Issnd are monotone                                             *)
+(* ------------------------------------------------------------------------ *)
+
+lemma monofun_Isfst: "monofun(Isfst)"
+
+apply (unfold monofun)
+apply (simp add: inst_sprod_po)
+done
+
+lemma monofun_Issnd: "monofun(Issnd)"
+apply (unfold monofun)
+apply (simp add: inst_sprod_po)
+done
+
+(* ------------------------------------------------------------------------ *)
+(* the type 'a ** 'b is a cpo                                               *)
+(* ------------------------------------------------------------------------ *)
+
+lemma lub_sprod: 
+"[|chain(S)|] ==> range(S) <<|  
+  Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
+apply (rule is_lubI)
+apply (rule ub_rangeI)
+apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst])
+apply (rule monofun_Ispair)
+apply (rule is_ub_thelub)
+apply (erule monofun_Isfst [THEN ch2ch_monofun])
+apply (rule is_ub_thelub)
+apply (erule monofun_Issnd [THEN ch2ch_monofun])
+apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst])
+apply (rule monofun_Ispair)
+apply (rule is_lub_thelub)
+apply (erule monofun_Isfst [THEN ch2ch_monofun])
+apply (erule monofun_Isfst [THEN ub2ub_monofun])
+apply (rule is_lub_thelub)
+apply (erule monofun_Issnd [THEN ch2ch_monofun])
+apply (erule monofun_Issnd [THEN ub2ub_monofun])
+done
+
+lemmas thelub_sprod = lub_sprod [THEN thelubI, standard]
+
+
+lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
+apply (rule exI)
+apply (erule lub_sprod)
+done
+
 end
 
 
diff -r eb3b1a5c304e -r 60743edae74a src/HOLCF/Sprod3.ML
--- a/src/HOLCF/Sprod3.ML	Wed Mar 02 23:58:02 2005 +0100
+++ b/src/HOLCF/Sprod3.ML	Thu Mar 03 00:42:04 2005 +0100
@@ -1,499 +1,53 @@
-(*  Title:      HOLCF/Sprod3
-    ID:         $Id$
-    Author:     Franz Regensburger
 
-Class instance of  ** for class pcpo
-*)
-
-(* for compatibility with old HOLCF-Version *)
-Goal "UU = Ispair UU UU";
-by (simp_tac (HOL_ss addsimps [UU_def,UU_sprod_def]) 1);
-qed "inst_sprod_pcpo";
-
-Addsimps [inst_sprod_pcpo RS sym];
-
-(* ------------------------------------------------------------------------ *)
-(* continuity of Ispair, Isfst, Issnd                                       *)
-(* ------------------------------------------------------------------------ *)
-
-Goal 
-"[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
-\ Ispair (lub(range Y)) x =\
-\ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
-\        (lub(range(%i. Issnd(Ispair(Y i) x))))";
-by (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1);
-by (rtac lub_equal 1);
-by (atac 1);
-by (rtac (monofun_Isfst RS ch2ch_monofun) 1);
-by (rtac ch2ch_fun 1);
-by (rtac (monofun_Ispair1 RS ch2ch_monofun) 1);
-by (atac 1);
-by (rtac allI 1);
-by (Asm_simp_tac 1);
-by (rtac sym 1);
-by (dtac chain_UU_I_inverse2 1);
-by (etac exE 1);
-by (rtac lub_chain_maxelem 1);
-by (etac Issnd2 1);
-by (rtac allI 1);
-by (rename_tac "j" 1);
-by (case_tac "Y(j)=UU" 1);
-by Auto_tac;  
-qed "sprod3_lemma1";
-
-Goal 
-"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
-\   Ispair (lub(range Y)) x =\
-\   Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
-\          (lub(range(%i. Issnd(Ispair(Y i) x))))";
-by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1);
-by (atac 1);
-by (rtac trans 1);
-by (rtac strict_Ispair1 1);
-by (rtac (strict_Ispair RS sym) 1);
-by (rtac disjI1 1);
-by (rtac chain_UU_I_inverse 1);
-by Auto_tac;  
-by (etac (chain_UU_I RS spec) 1);
-by (atac 1);
-qed "sprod3_lemma2";
-
-
-Goal 
-"[| chain(Y); x = UU |] ==>\
-\          Ispair (lub(range Y)) x =\
-\          Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
-\                 (lub(range(%i. Issnd(Ispair (Y i) x))))";
-by (etac ssubst 1);
-by (rtac trans 1);
-by (rtac strict_Ispair2 1);
-by (rtac (strict_Ispair RS sym) 1);
-by (rtac disjI1 1);
-by (rtac chain_UU_I_inverse 1);
-by (rtac allI 1);
-by (simp_tac Sprod0_ss  1);
-qed "sprod3_lemma3";
-
-Goal "contlub(Ispair)";
-by (rtac contlubI 1);
-by (strip_tac 1);
-by (rtac (expand_fun_eq RS iffD2) 1);
-by (strip_tac 1);
-by (stac (lub_fun RS thelubI) 1);
-by (etac (monofun_Ispair1 RS ch2ch_monofun) 1);
-by (rtac trans 1);
-by (rtac (thelub_sprod RS sym) 2);
-by (rtac ch2ch_fun 2);
-by (etac (monofun_Ispair1 RS ch2ch_monofun) 2);
-by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
-by (res_inst_tac [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1);
-by (etac sprod3_lemma1 1);
-by (atac 1);
-by (atac 1);
-by (etac sprod3_lemma2 1);
-by (atac 1);
-by (atac 1);
-by (etac sprod3_lemma3 1);
-by (atac 1);
-qed "contlub_Ispair1";
-
-Goal 
-"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
-\         Ispair x (lub(range Y)) =\
-\         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
-\                (lub(range(%i. Issnd (Ispair x (Y i)))))";
-by (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1);
-by (rtac sym 1);
-by (dtac chain_UU_I_inverse2 1);
-by (etac exE 1);
-by (rtac lub_chain_maxelem 1);
-by (etac Isfst2 1);
-by (rtac allI 1);
-by (rename_tac "j" 1);
-by (case_tac "Y(j)=UU" 1);
-by Auto_tac;  
-qed "sprod3_lemma4";
-
-Goal 
-"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
-\         Ispair x (lub(range Y)) =\
-\         Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
-\                (lub(range(%i. Issnd(Ispair x (Y i)))))";
-by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1);
-by (atac 1);
-by (rtac trans 1);
-by (rtac strict_Ispair2 1);
-by (rtac (strict_Ispair RS sym) 1);
-by (rtac disjI2 1);
-by (rtac chain_UU_I_inverse 1);
-by (rtac allI 1);
-by (asm_simp_tac Sprod0_ss  1);
-by (etac (chain_UU_I RS spec) 1);
-by (atac 1);
-qed "sprod3_lemma5";
-
-Goal 
-"[| chain(Y); x = UU |] ==>\
-\         Ispair x (lub(range Y)) =\
-\         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
-\                (lub(range(%i. Issnd (Ispair x (Y i)))))";
-by (res_inst_tac [("s","UU"),("t","x")] ssubst 1);
-by (atac 1);
-by (rtac trans 1);
-by (rtac strict_Ispair1 1);
-by (rtac (strict_Ispair RS sym) 1);
-by (rtac disjI1 1);
-by (rtac chain_UU_I_inverse 1);
-by (rtac allI 1);
-by (simp_tac Sprod0_ss  1);
-qed "sprod3_lemma6";
-
-Goal "contlub(Ispair(x))";
-by (rtac contlubI 1);
-by (strip_tac 1);
-by (rtac trans 1);
-by (rtac (thelub_sprod RS sym) 2);
-by (etac (monofun_Ispair2 RS ch2ch_monofun) 2);
-by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
-by (res_inst_tac [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1);
-by (etac sprod3_lemma4 1);
-by (atac 1);
-by (atac 1);
-by (etac sprod3_lemma5 1);
-by (atac 1);
-by (atac 1);
-by (etac sprod3_lemma6 1);
-by (atac 1);
-qed "contlub_Ispair2";
-
-Goal "cont(Ispair)";
-by (rtac monocontlub2cont 1);
-by (rtac monofun_Ispair1 1);
-by (rtac contlub_Ispair1 1);
-qed "cont_Ispair1";
-
-
-Goal "cont(Ispair(x))";
-by (rtac monocontlub2cont 1);
-by (rtac monofun_Ispair2 1);
-by (rtac contlub_Ispair2 1);
-qed "cont_Ispair2";
-
-Goal "contlub(Isfst)";
-by (rtac contlubI 1);
-by (strip_tac 1);
-by (stac (lub_sprod RS thelubI) 1);
-by (atac 1);
-by (res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")] (excluded_middle RS disjE) 1);
-by (asm_simp_tac Sprod0_ss  1);
-by (res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")] ssubst 1);
-by (atac 1);
-by (rtac trans 1);
-by (asm_simp_tac Sprod0_ss  1);
-by (rtac sym 1);
-by (rtac chain_UU_I_inverse 1);
-by (rtac allI 1);
-by (rtac strict_Isfst 1);
-by (rtac contrapos_np 1);
-by (etac (defined_IsfstIssnd RS conjunct2) 2);
-by (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
-qed "contlub_Isfst";
-
-Goal "contlub(Issnd)";
-by (rtac contlubI 1);
-by (strip_tac 1);
-by (stac (lub_sprod RS thelubI) 1);
-by (atac 1);
-by (res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")] (excluded_middle RS disjE) 1);
-by (asm_simp_tac Sprod0_ss  1);
-by (res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] ssubst 1);
-by (atac 1);
-by (asm_simp_tac Sprod0_ss  1);
-by (rtac sym 1);
-by (rtac chain_UU_I_inverse 1);
-by (rtac allI 1);
-by (rtac strict_Issnd 1);
-by (rtac contrapos_np 1);
-by (etac (defined_IsfstIssnd RS conjunct1) 2);
-by (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
-qed "contlub_Issnd";
-
-Goal "cont(Isfst)";
-by (rtac monocontlub2cont 1);
-by (rtac monofun_Isfst 1);
-by (rtac contlub_Isfst 1);
-qed "cont_Isfst";
-
-Goal "cont(Issnd)";
-by (rtac monocontlub2cont 1);
-by (rtac monofun_Issnd 1);
-by (rtac contlub_Issnd 1);
-qed "cont_Issnd";
-
-Goal "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)";
-by (fast_tac HOL_cs 1);
-qed "spair_eq";
-
-(* ------------------------------------------------------------------------ *)
-(* convert all lemmas to the continuous versions                            *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [spair_def]
-        "(LAM x y. Ispair x y)$a$b = Ispair a b";
-by (stac beta_cfun 1);
-by (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1, cont2cont_CF1L]) 1);
-by (stac beta_cfun 1);
-by (rtac cont_Ispair2 1);
-by (rtac refl 1);
-qed "beta_cfun_sprod";
+(* legacy ML bindings *)
 
-Addsimps [beta_cfun_sprod];
-
-Goalw [spair_def]
-        "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba";
-by (etac inject_Ispair 1);
-by (atac 1);
-by (etac box_equals 1);
-by (rtac beta_cfun_sprod 1);
-by (rtac beta_cfun_sprod 1);
-qed "inject_spair";
-
-Goalw [spair_def] "UU = (:UU,UU:)";
-by (rtac sym 1);
-by (rtac trans 1);
-by (rtac beta_cfun_sprod 1);
-by (rtac sym 1);
-by (rtac inst_sprod_pcpo 1);
-qed "inst_sprod_pcpo2";
-
-Goalw [spair_def] 
-        "(a=UU | b=UU) ==> (:a,b:)=UU";
-by (rtac trans 1);
-by (rtac beta_cfun_sprod 1);
-by (rtac trans 1);
-by (rtac (inst_sprod_pcpo RS sym) 2);
-by (etac strict_Ispair 1);
-qed "strict_spair";
-
-Goalw [spair_def] "(:UU,b:) = UU";
-by (stac beta_cfun_sprod 1);
-by (rtac trans 1);
-by (rtac (inst_sprod_pcpo RS sym) 2);
-by (rtac strict_Ispair1 1);
-qed "strict_spair1";
-
-Goalw [spair_def] "(:a,UU:) = UU";
-by (stac beta_cfun_sprod 1);
-by (rtac trans 1);
-by (rtac (inst_sprod_pcpo RS sym) 2);
-by (rtac strict_Ispair2 1);
-qed "strict_spair2";
-
-Addsimps [strict_spair1,strict_spair2];
-
-Goalw [spair_def] "(:x,y:)~=UU ==> ~x=UU & ~y=UU";
-by (rtac strict_Ispair_rev 1);
-by Auto_tac;  
-qed "strict_spair_rev";
-
-Goalw [spair_def] "(:a,b:) = UU ==> (a = UU | b = UU)";
-by (rtac defined_Ispair_rev 1);
-by Auto_tac;  
-qed "defined_spair_rev";
-
-Goalw [spair_def]
-        "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU";
-by (stac beta_cfun_sprod 1);
-by (stac inst_sprod_pcpo 1);
-by (etac defined_Ispair 1);
-by (atac 1);
-qed "defined_spair";
-
-Goalw [spair_def]
-        "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)";
-by (rtac (Exh_Sprod RS disjE) 1);
-by (rtac disjI1 1);
-by (stac inst_sprod_pcpo 1);
-by (atac 1);
-by (rtac disjI2 1);
-by (etac exE 1);
-by (etac exE 1);
-by (rtac exI 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (stac beta_cfun_sprod 1);
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
-qed "Exh_Sprod2";
-
-
-val [prem1,prem2] = Goalw [spair_def]
-   "[|p=UU ==> Q;  !!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q|] ==> Q";
-by (rtac IsprodE 1);
-by (rtac prem1 1);
-by (stac inst_sprod_pcpo 1);
-by (atac 1);
-by (rtac prem2 1);
-by (atac 2);
-by (atac 2);
-by (stac beta_cfun_sprod 1);
-by (atac 1);
-qed "sprodE";
-
-
-Goalw [sfst_def] 
-        "p=UU==>sfst$p=UU";
-by (stac beta_cfun 1);
-by (rtac cont_Isfst 1);
-by (rtac strict_Isfst 1);
-by (rtac (inst_sprod_pcpo RS subst) 1);
-by (atac 1);
-qed "strict_sfst";
-
-Goalw [sfst_def,spair_def] 
-        "sfst$(:UU,y:) = UU";
-by (stac beta_cfun_sprod 1);
-by (stac beta_cfun 1);
-by (rtac cont_Isfst 1);
-by (rtac strict_Isfst1 1);
-qed "strict_sfst1";
- 
-Goalw [sfst_def,spair_def] 
-        "sfst$(:x,UU:) = UU";
-by (stac beta_cfun_sprod 1);
-by (stac beta_cfun 1);
-by (rtac cont_Isfst 1);
-by (rtac strict_Isfst2 1);
-qed "strict_sfst2";
+val spair_def = thm "spair_def";
+val sfst_def = thm "sfst_def";
+val ssnd_def = thm "ssnd_def";
+val ssplit_def = thm "ssplit_def";
+val inst_sprod_pcpo = thm "inst_sprod_pcpo";
+val sprod3_lemma1 = thm "sprod3_lemma1";
+val sprod3_lemma2 = thm "sprod3_lemma2";
+val sprod3_lemma3 = thm "sprod3_lemma3";
+val contlub_Ispair1 = thm "contlub_Ispair1";
+val sprod3_lemma4 = thm "sprod3_lemma4";
+val sprod3_lemma5 = thm "sprod3_lemma5";
+val sprod3_lemma6 = thm "sprod3_lemma6";
+val contlub_Ispair2 = thm "contlub_Ispair2";
+val cont_Ispair1 = thm "cont_Ispair1";
+val cont_Ispair2 = thm "cont_Ispair2";
+val contlub_Isfst = thm "contlub_Isfst";
+val contlub_Issnd = thm "contlub_Issnd";
+val cont_Isfst = thm "cont_Isfst";
+val cont_Issnd = thm "cont_Issnd";
+val spair_eq = thm "spair_eq";
+val beta_cfun_sprod = thm "beta_cfun_sprod";
+val inject_spair = thm "inject_spair";
+val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
+val strict_spair = thm "strict_spair";
+val strict_spair1 = thm "strict_spair1";
+val strict_spair2 = thm "strict_spair2";
+val strict_spair_rev = thm "strict_spair_rev";
+val defined_spair_rev = thm "defined_spair_rev";
+val defined_spair = thm "defined_spair";
+val Exh_Sprod2 = thm "Exh_Sprod2";
+val sprodE = thm "sprodE";
+val strict_sfst = thm "strict_sfst";
+val strict_sfst1 = thm "strict_sfst1";
+val strict_sfst2 = thm "strict_sfst2";
+val strict_ssnd = thm "strict_ssnd";
+val strict_ssnd1 = thm "strict_ssnd1";
+val strict_ssnd2 = thm "strict_ssnd2";
+val sfst2 = thm "sfst2";
+val ssnd2 = thm "ssnd2";
+val defined_sfstssnd = thm "defined_sfstssnd";
+val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
+val lub_sprod2 = thm "lub_sprod2";
+val thelub_sprod2 = thm "thelub_sprod2";
+val ssplit1 = thm "ssplit1";
+val ssplit2 = thm "ssplit2";
+val ssplit3 = thm "ssplit3";
+val Sprod_rews = [strict_sfst1, strict_sfst2,
+                strict_ssnd1, strict_ssnd2, sfst2, ssnd2, defined_spair,
+                ssplit1, ssplit2]
 
-Goalw [ssnd_def] 
-        "p=UU==>ssnd$p=UU";
-by (stac beta_cfun 1);
-by (rtac cont_Issnd 1);
-by (rtac strict_Issnd 1);
-by (rtac (inst_sprod_pcpo RS subst) 1);
-by (atac 1);
-qed "strict_ssnd";
-
-Goalw [ssnd_def,spair_def] 
-        "ssnd$(:UU,y:) = UU";
-by (stac beta_cfun_sprod 1);
-by (stac beta_cfun 1);
-by (rtac cont_Issnd 1);
-by (rtac strict_Issnd1 1);
-qed "strict_ssnd1";
-
-Goalw [ssnd_def,spair_def] 
-        "ssnd$(:x,UU:) = UU";
-by (stac beta_cfun_sprod 1);
-by (stac beta_cfun 1);
-by (rtac cont_Issnd 1);
-by (rtac strict_Issnd2 1);
-qed "strict_ssnd2";
-
-Goalw [sfst_def,spair_def] 
-        "y~=UU ==>sfst$(:x,y:)=x";
-by (stac beta_cfun_sprod 1);
-by (stac beta_cfun 1);
-by (rtac cont_Isfst 1);
-by (etac Isfst2 1);
-qed "sfst2";
-
-Goalw [ssnd_def,spair_def] 
-        "x~=UU ==>ssnd$(:x,y:)=y";
-by (stac beta_cfun_sprod 1);
-by (stac beta_cfun 1);
-by (rtac cont_Issnd 1);
-by (etac Issnd2 1);
-qed "ssnd2";
-
-
-Goalw [sfst_def,ssnd_def,spair_def]
-        "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU";
-by (stac beta_cfun 1);
-by (rtac cont_Issnd 1);
-by (stac beta_cfun 1);
-by (rtac cont_Isfst 1);
-by (rtac defined_IsfstIssnd 1);
-by (rtac (inst_sprod_pcpo RS subst) 1);
-by (atac 1);
-qed "defined_sfstssnd";
- 
-Goalw [sfst_def,ssnd_def,spair_def] "(:sfst$p , ssnd$p:) = p";
-by (stac beta_cfun_sprod 1);
-by (stac beta_cfun 1);
-by (rtac cont_Issnd 1);
-by (stac beta_cfun 1);
-by (rtac cont_Isfst 1);
-by (rtac (surjective_pairing_Sprod RS sym) 1);
-qed "surjective_pairing_Sprod2";
-
-Goalw [sfst_def,ssnd_def,spair_def]
-"chain(S) ==> range(S) <<| \
-\              (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)";
-by (stac beta_cfun_sprod 1);
-by (stac (beta_cfun RS ext) 1);
-by (rtac cont_Issnd 1);
-by (stac (beta_cfun RS ext) 1);
-by (rtac cont_Isfst 1);
-by (etac lub_sprod 1);
-qed "lub_sprod2";
-
-
-bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
-(*
- "chain ?S1 ==>
- lub (range ?S1) =
- (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
-*)
-
-Goalw [ssplit_def]
-        "ssplit$f$UU=UU";
-by (stac beta_cfun 1);
-by (Simp_tac 1);
-by (stac strictify1 1);
-by (rtac refl 1);
-qed "ssplit1";
-
-Goalw [ssplit_def]
-        "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y";
-by (stac beta_cfun 1);
-by (Simp_tac 1);
-by (stac strictify2 1);
-by (rtac defined_spair 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (stac beta_cfun 1);
-by (Simp_tac 1);
-by (stac sfst2 1);
-by (assume_tac 1);
-by (stac ssnd2 1);
-by (assume_tac 1);
-by (rtac refl 1);
-qed "ssplit2";
-
-
-Goalw [ssplit_def]
-  "ssplit$spair$z=z";
-by (stac beta_cfun 1);
-by (Simp_tac 1);
-by (case_tac "z=UU" 1);
-by (hyp_subst_tac 1);
-by (rtac strictify1 1);
-by (rtac trans 1);
-by (rtac strictify2 1);
-by (atac 1);
-by (stac beta_cfun 1);
-by (Simp_tac 1);
-by (rtac surjective_pairing_Sprod2 1);
-qed "ssplit3";
-
-(* ------------------------------------------------------------------------ *)
-(* install simplifier for Sprod                                             *)
-(* ------------------------------------------------------------------------ *)
-
-val Sprod_rews = [strict_sfst1,strict_sfst2,
-                strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
-                ssplit1,ssplit2];
-Addsimps Sprod_rews;
-
diff -r eb3b1a5c304e -r 60743edae74a src/HOLCF/Sprod3.thy
--- a/src/HOLCF/Sprod3.thy	Wed Mar 02 23:58:02 2005 +0100
+++ b/src/HOLCF/Sprod3.thy	Thu Mar 03 00:42:04 2005 +0100
@@ -1,13 +1,18 @@
 (*  Title:      HOLCF/sprod3.thy
     ID:         $Id$
     Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  ** for class pcpo
 *)
 
-Sprod3 = Sprod2 +
+theory Sprod3 = Sprod2:
 
-instance "**" :: (pcpo,pcpo)pcpo  (least_sprod,cpo_sprod)
+instance "**" :: (pcpo,pcpo)pcpo
+apply (intro_classes)
+apply (erule cpo_sprod)
+apply (rule least_sprod)
+done
 
 consts  
   spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
@@ -23,9 +28,538 @@
         "(:x, y:)"      == "spair$x$y"
 
 defs
-spair_def       "spair  == (LAM x y. Ispair x y)"
-sfst_def        "sfst   == (LAM p. Isfst p)"
-ssnd_def        "ssnd   == (LAM p. Issnd p)"     
-ssplit_def      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
+spair_def:       "spair  == (LAM x y. Ispair x y)"
+sfst_def:        "sfst   == (LAM p. Isfst p)"
+ssnd_def:        "ssnd   == (LAM p. Issnd p)"     
+ssplit_def:      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
+
+(*  Title:      HOLCF/Sprod3
+    ID:         $Id$
+    Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Class instance of  ** for class pcpo
+*)
+
+(* for compatibility with old HOLCF-Version *)
+lemma inst_sprod_pcpo: "UU = Ispair UU UU"
+apply (simp add: UU_def UU_sprod_def)
+done
+
+declare inst_sprod_pcpo [symmetric, simp]
+
+(* ------------------------------------------------------------------------ *)
+(* continuity of Ispair, Isfst, Issnd                                       *)
+(* ------------------------------------------------------------------------ *)
+
+lemma sprod3_lemma1: 
+"[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==> 
+  Ispair (lub(range Y)) x = 
+  Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))  
+         (lub(range(%i. Issnd(Ispair(Y i) x))))"
+apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
+apply (rule lub_equal)
+apply assumption
+apply (rule monofun_Isfst [THEN ch2ch_monofun])
+apply (rule ch2ch_fun)
+apply (rule monofun_Ispair1 [THEN ch2ch_monofun])
+apply assumption
+apply (rule allI)
+apply (simp (no_asm_simp))
+apply (rule sym)
+apply (drule chain_UU_I_inverse2)
+apply (erule exE)
+apply (rule lub_chain_maxelem)
+apply (erule Issnd2)
+apply (rule allI)
+apply (rename_tac "j")
+apply (case_tac "Y (j) =UU")
+apply auto
+done
+
+lemma sprod3_lemma2: 
+"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
+    Ispair (lub(range Y)) x = 
+    Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) 
+           (lub(range(%i. Issnd(Ispair(Y i) x))))"
+apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
+apply assumption
+apply (rule trans)
+apply (rule strict_Ispair1)
+apply (rule strict_Ispair [symmetric])
+apply (rule disjI1)
+apply (rule chain_UU_I_inverse)
+apply auto
+apply (erule chain_UU_I [THEN spec])
+apply assumption
+done
+
+
+lemma sprod3_lemma3: 
+"[| chain(Y); x = UU |] ==> 
+           Ispair (lub(range Y)) x = 
+           Ispair (lub(range(%i. Isfst(Ispair (Y i) x)))) 
+                  (lub(range(%i. Issnd(Ispair (Y i) x))))"
+apply (erule ssubst)
+apply (rule trans)
+apply (rule strict_Ispair2)
+apply (rule strict_Ispair [symmetric])
+apply (rule disjI1)
+apply (rule chain_UU_I_inverse)
+apply (rule allI)
+apply (simp add: Sprod0_ss)
+done
+
+lemma contlub_Ispair1: "contlub(Ispair)"
+apply (rule contlubI)
+apply (intro strip)
+apply (rule expand_fun_eq [THEN iffD2])
+apply (intro strip)
+apply (subst lub_fun [THEN thelubI])
+apply (erule monofun_Ispair1 [THEN ch2ch_monofun])
+apply (rule trans)
+apply (rule_tac [2] thelub_sprod [symmetric])
+apply (rule_tac [2] ch2ch_fun)
+apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun])
+apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
+apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
+apply (erule sprod3_lemma1)
+apply assumption
+apply assumption
+apply (erule sprod3_lemma2)
+apply assumption
+apply assumption
+apply (erule sprod3_lemma3)
+apply assumption
+done
+
+lemma sprod3_lemma4: 
+"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==> 
+          Ispair x (lub(range Y)) = 
+          Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
+                 (lub(range(%i. Issnd (Ispair x (Y i)))))"
+apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
+apply (rule sym)
+apply (drule chain_UU_I_inverse2)
+apply (erule exE)
+apply (rule lub_chain_maxelem)
+apply (erule Isfst2)
+apply (rule allI)
+apply (rename_tac "j")
+apply (case_tac "Y (j) =UU")
+apply auto
+done
+
+lemma sprod3_lemma5: 
+"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
+          Ispair x (lub(range Y)) = 
+          Ispair (lub(range(%i. Isfst(Ispair x (Y i))))) 
+                 (lub(range(%i. Issnd(Ispair x (Y i)))))"
+apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
+apply assumption
+apply (rule trans)
+apply (rule strict_Ispair2)
+apply (rule strict_Ispair [symmetric])
+apply (rule disjI2)
+apply (rule chain_UU_I_inverse)
+apply (rule allI)
+apply (simp add: Sprod0_ss)
+apply (erule chain_UU_I [THEN spec])
+apply assumption
+done
+
+lemma sprod3_lemma6: 
+"[| chain(Y); x = UU |] ==> 
+          Ispair x (lub(range Y)) = 
+          Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
+                 (lub(range(%i. Issnd (Ispair x (Y i)))))"
+apply (rule_tac s = "UU" and t = "x" in ssubst)
+apply assumption
+apply (rule trans)
+apply (rule strict_Ispair1)
+apply (rule strict_Ispair [symmetric])
+apply (rule disjI1)
+apply (rule chain_UU_I_inverse)
+apply (rule allI)
+apply (simp add: Sprod0_ss)
+done
+
+lemma contlub_Ispair2: "contlub(Ispair(x))"
+apply (rule contlubI)
+apply (intro strip)
+apply (rule trans)
+apply (rule_tac [2] thelub_sprod [symmetric])
+apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun])
+apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
+apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
+apply (erule sprod3_lemma4)
+apply assumption
+apply assumption
+apply (erule sprod3_lemma5)
+apply assumption
+apply assumption
+apply (erule sprod3_lemma6)
+apply assumption
+done
+
+lemma cont_Ispair1: "cont(Ispair)"
+apply (rule monocontlub2cont)
+apply (rule monofun_Ispair1)
+apply (rule contlub_Ispair1)
+done
+
+
+lemma cont_Ispair2: "cont(Ispair(x))"
+apply (rule monocontlub2cont)
+apply (rule monofun_Ispair2)
+apply (rule contlub_Ispair2)
+done
+
+lemma contlub_Isfst: "contlub(Isfst)"
+apply (rule contlubI)
+apply (intro strip)
+apply (subst lub_sprod [THEN thelubI])
+apply assumption
+apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE])
+apply (simp add: Sprod0_ss)
+apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst)
+apply assumption
+apply (rule trans)
+apply (simp add: Sprod0_ss)
+apply (rule sym)
+apply (rule chain_UU_I_inverse)
+apply (rule allI)
+apply (rule strict_Isfst)
+apply (rule contrapos_np)
+apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2])
+apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
+done
+
+lemma contlub_Issnd: "contlub(Issnd)"
+apply (rule contlubI)
+apply (intro strip)
+apply (subst lub_sprod [THEN thelubI])
+apply assumption
+apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE])
+apply (simp add: Sprod0_ss)
+apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst)
+apply assumption
+apply (simp add: Sprod0_ss)
+apply (rule sym)
+apply (rule chain_UU_I_inverse)
+apply (rule allI)
+apply (rule strict_Issnd)
+apply (rule contrapos_np)
+apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1])
+apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
+done
+
+lemma cont_Isfst: "cont(Isfst)"
+apply (rule monocontlub2cont)
+apply (rule monofun_Isfst)
+apply (rule contlub_Isfst)
+done
+
+lemma cont_Issnd: "cont(Issnd)"
+apply (rule monocontlub2cont)
+apply (rule monofun_Issnd)
+apply (rule contlub_Issnd)
+done
+
+lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
+apply fast
+done
+
+(* ------------------------------------------------------------------------ *)
+(* convert all lemmas to the continuous versions                            *)
+(* ------------------------------------------------------------------------ *)
+
+lemma beta_cfun_sprod: 
+        "(LAM x y. Ispair x y)$a$b = Ispair a b"
+apply (subst beta_cfun)
+apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L)
+apply (subst beta_cfun)
+apply (rule cont_Ispair2)
+apply (rule refl)
+done
+
+declare beta_cfun_sprod [simp]
+
+lemma inject_spair: 
+        "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
+apply (unfold spair_def)
+apply (erule inject_Ispair)
+apply assumption
+apply (erule box_equals)
+apply (rule beta_cfun_sprod)
+apply (rule beta_cfun_sprod)
+done
+
+lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
+apply (unfold spair_def)
+apply (rule sym)
+apply (rule trans)
+apply (rule beta_cfun_sprod)
+apply (rule sym)
+apply (rule inst_sprod_pcpo)
+done
+
+lemma strict_spair: 
+        "(a=UU | b=UU) ==> (:a,b:)=UU"
+apply (unfold spair_def)
+apply (rule trans)
+apply (rule beta_cfun_sprod)
+apply (rule trans)
+apply (rule_tac [2] inst_sprod_pcpo [symmetric])
+apply (erule strict_Ispair)
+done
+
+lemma strict_spair1: "(:UU,b:) = UU"
+apply (unfold spair_def)
+apply (subst beta_cfun_sprod)
+apply (rule trans)
+apply (rule_tac [2] inst_sprod_pcpo [symmetric])
+apply (rule strict_Ispair1)
+done
+
+lemma strict_spair2: "(:a,UU:) = UU"
+apply (unfold spair_def)
+apply (subst beta_cfun_sprod)
+apply (rule trans)
+apply (rule_tac [2] inst_sprod_pcpo [symmetric])
+apply (rule strict_Ispair2)
+done
+
+declare strict_spair1 [simp] strict_spair2 [simp]
+
+lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
+apply (unfold spair_def)
+apply (rule strict_Ispair_rev)
+apply auto
+done
+
+lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)"
+apply (unfold spair_def)
+apply (rule defined_Ispair_rev)
+apply auto
+done
+
+lemma defined_spair: 
+        "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
+apply (unfold spair_def)
+apply (subst beta_cfun_sprod)
+apply (subst inst_sprod_pcpo)
+apply (erule defined_Ispair)
+apply assumption
+done
+
+lemma Exh_Sprod2:
+        "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
+apply (unfold spair_def)
+apply (rule Exh_Sprod [THEN disjE])
+apply (rule disjI1)
+apply (subst inst_sprod_pcpo)
+apply assumption
+apply (rule disjI2)
+apply (erule exE)
+apply (erule exE)
+apply (rule exI)
+apply (rule exI)
+apply (rule conjI)
+apply (subst beta_cfun_sprod)
+apply fast
+apply fast
+done
+
+
+lemma sprodE:
+assumes prem1: "p=UU ==> Q"
+assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
+shows "Q"
+apply (rule IsprodE)
+apply (rule prem1)
+apply (subst inst_sprod_pcpo)
+apply assumption
+apply (rule prem2)
+prefer 2 apply (assumption)
+prefer 2 apply (assumption)
+apply (unfold spair_def)
+apply (subst beta_cfun_sprod)
+apply assumption
+done
+
+
+lemma strict_sfst: 
+        "p=UU==>sfst$p=UU"
+apply (unfold sfst_def)
+apply (subst beta_cfun)
+apply (rule cont_Isfst)
+apply (rule strict_Isfst)
+apply (rule inst_sprod_pcpo [THEN subst])
+apply assumption
+done
+
+lemma strict_sfst1: 
+        "sfst$(:UU,y:) = UU"
+apply (unfold sfst_def spair_def)
+apply (subst beta_cfun_sprod)
+apply (subst beta_cfun)
+apply (rule cont_Isfst)
+apply (rule strict_Isfst1)
+done
+ 
+lemma strict_sfst2: 
+        "sfst$(:x,UU:) = UU"
+apply (unfold sfst_def spair_def)
+apply (subst beta_cfun_sprod)
+apply (subst beta_cfun)
+apply (rule cont_Isfst)
+apply (rule strict_Isfst2)
+done
+
+lemma strict_ssnd: 
+        "p=UU==>ssnd$p=UU"
+apply (unfold ssnd_def)
+apply (subst beta_cfun)
+apply (rule cont_Issnd)
+apply (rule strict_Issnd)
+apply (rule inst_sprod_pcpo [THEN subst])
+apply assumption
+done
+
+lemma strict_ssnd1: 
+        "ssnd$(:UU,y:) = UU"
+apply (unfold ssnd_def spair_def)
+apply (subst beta_cfun_sprod)
+apply (subst beta_cfun)
+apply (rule cont_Issnd)
+apply (rule strict_Issnd1)
+done
+
+lemma strict_ssnd2: 
+        "ssnd$(:x,UU:) = UU"
+apply (unfold ssnd_def spair_def)
+apply (subst beta_cfun_sprod)
+apply (subst beta_cfun)
+apply (rule cont_Issnd)
+apply (rule strict_Issnd2)
+done
+
+lemma sfst2: 
+        "y~=UU ==>sfst$(:x,y:)=x"
+apply (unfold sfst_def spair_def)
+apply (subst beta_cfun_sprod)
+apply (subst beta_cfun)
+apply (rule cont_Isfst)
+apply (erule Isfst2)
+done
+
+lemma ssnd2: 
+        "x~=UU ==>ssnd$(:x,y:)=y"
+apply (unfold ssnd_def spair_def)
+apply (subst beta_cfun_sprod)
+apply (subst beta_cfun)
+apply (rule cont_Issnd)
+apply (erule Issnd2)
+done
+
+
+lemma defined_sfstssnd: 
+        "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
+apply (unfold sfst_def ssnd_def spair_def)
+apply (simplesubst beta_cfun)
+apply (rule cont_Issnd)
+apply (subst beta_cfun)
+apply (rule cont_Isfst)
+apply (rule defined_IsfstIssnd)
+apply (rule inst_sprod_pcpo [THEN subst])
+apply assumption
+done
+ 
+lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p"
+ 
+apply (unfold sfst_def ssnd_def spair_def)
+apply (subst beta_cfun_sprod)
+apply (simplesubst beta_cfun)
+apply (rule cont_Issnd)
+apply (subst beta_cfun)
+apply (rule cont_Isfst)
+apply (rule surjective_pairing_Sprod [symmetric])
+done
+
+lemma lub_sprod2: 
+"chain(S) ==> range(S) <<|  
+               (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"
+apply (unfold sfst_def ssnd_def spair_def)
+apply (subst beta_cfun_sprod)
+apply (simplesubst beta_cfun [THEN ext])
+apply (rule cont_Issnd)
+apply (subst beta_cfun [THEN ext])
+apply (rule cont_Isfst)
+apply (erule lub_sprod)
+done
+
+
+lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
+(*
+ "chain ?S1 ==>
+ lub (range ?S1) =
+ (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
+*)
+
+lemma ssplit1: 
+        "ssplit$f$UU=UU"
+
+apply (unfold ssplit_def)
+apply (subst beta_cfun)
+apply (simp (no_asm))
+apply (subst strictify1)
+apply (rule refl)
+done
+
+lemma ssplit2: 
+        "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
+apply (unfold ssplit_def)
+apply (subst beta_cfun)
+apply (simp (no_asm))
+apply (subst strictify2)
+apply (rule defined_spair)
+apply assumption
+apply assumption
+apply (subst beta_cfun)
+apply (simp (no_asm))
+apply (subst sfst2)
+apply assumption
+apply (subst ssnd2)
+apply assumption
+apply (rule refl)
+done
+
+
+lemma ssplit3: 
+  "ssplit$spair$z=z"
+
+apply (unfold ssplit_def)
+apply (subst beta_cfun)
+apply (simp (no_asm))
+apply (case_tac "z=UU")
+apply (erule ssubst)
+apply (rule strictify1)
+apply (rule trans)
+apply (rule strictify2)
+apply assumption
+apply (subst beta_cfun)
+apply (simp (no_asm))
+apply (rule surjective_pairing_Sprod2)
+done
+
+(* ------------------------------------------------------------------------ *)
+(* install simplifier for Sprod                                             *)
+(* ------------------------------------------------------------------------ *)
+
+lemmas Sprod_rews = strict_sfst1 strict_sfst2
+                strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
+                ssplit1 ssplit2
+declare Sprod_rews [simp]
 
 end