*** empty log message ***
authoroheimb
Fri, 29 Nov 1996 12:22:22 +0100
changeset 2278 d63ffafce255
parent 2277 9174de6c7143
child 2279 2f337bf81085
*** empty log message ***
src/HOLCF/Cfun1.thy
src/HOLCF/Cprod3.thy
src/HOLCF/Lift1.ML
src/HOLCF/Lift1.thy
src/HOLCF/Lift2.ML
src/HOLCF/Lift2.thy
src/HOLCF/Lift3.ML
src/HOLCF/Lift3.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
src/HOLCF/Porder0.thy
src/HOLCF/ROOT.ML
src/HOLCF/Sprod0.thy
src/HOLCF/Sprod3.thy
src/HOLCF/Ssum0.thy
src/HOLCF/Ssum3.thy
src/HOLCF/Tr1.thy
src/HOLCF/Up1.ML
src/HOLCF/Up1.thy
src/HOLCF/Up2.ML
src/HOLCF/Up2.thy
src/HOLCF/Up3.ML
src/HOLCF/Up3.thy
--- a/src/HOLCF/Cfun1.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Cfun1.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -65,4 +65,9 @@
 end
 
 (* start 8bit 2 *)
+ML
+val parse_ast_translation = ("",    fn asts => Appl (Constant "LAM " :: asts)) ::
+			    parse_ast_translation;
+val print_ast_translation = ("LAM ", fn asts => Appl (Constant ""    :: asts)) ::
+			    print_ast_translation;
 (* end 8bit 2 *)
--- a/src/HOLCF/Cprod3.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Cprod3.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -82,6 +82,9 @@
   (* reverse translation <= does not work yet !! *)
 
 (* start 8bit 1 *)
+translations
+  "Let x = a in e"          == "CLet`a`( x.e)"
+
 (* end 8bit 1 *)
 end
 
--- a/src/HOLCF/Lift1.ML	Fri Nov 29 12:17:30 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,186 +0,0 @@
-(*  Title:      HOLCF/lift1.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
-*)
-
-open Lift1;
-
-qed_goalw "Exh_Lift" Lift1.thy [UU_lift_def,Iup_def ]
-        "z = UU_lift | (? x. z = Iup(x))"
- (fn prems =>
-        [
-        (rtac (Rep_Lift_inverse RS subst) 1),
-        (res_inst_tac [("s","Rep_Lift(z)")] sumE 1),
-        (rtac disjI1 1),
-        (res_inst_tac [("f","Abs_Lift")] arg_cong 1),
-        (rtac (unique_void2 RS subst) 1),
-        (atac 1),
-        (rtac disjI2 1),
-        (rtac exI 1),
-        (res_inst_tac [("f","Abs_Lift")] arg_cong 1),
-        (atac 1)
-        ]);
-
-qed_goal "inj_Abs_Lift" Lift1.thy "inj(Abs_Lift)"
- (fn prems =>
-        [
-        (rtac inj_inverseI 1),
-        (rtac Abs_Lift_inverse 1)
-        ]);
-
-qed_goal "inj_Rep_Lift" Lift1.thy "inj(Rep_Lift)"
- (fn prems =>
-        [
-        (rtac inj_inverseI 1),
-        (rtac Rep_Lift_inverse 1)
-        ]);
-
-qed_goalw "inject_Iup" Lift1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac (inj_Inr RS injD) 1),
-        (rtac (inj_Abs_Lift RS injD) 1),
-        (atac 1)
-        ]);
-
-qed_goalw "defined_Iup" Lift1.thy [Iup_def,UU_lift_def] "Iup(x)~=UU_lift"
- (fn prems =>
-        [
-        (rtac notI 1),
-        (rtac notE 1),
-        (rtac Inl_not_Inr 1),
-        (rtac sym 1),
-        (etac (inj_Abs_Lift RS  injD) 1)
-        ]);
-
-
-qed_goal "liftE"  Lift1.thy
-        "[| p=UU_lift ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
- (fn prems =>
-        [
-        (rtac (Exh_Lift RS disjE) 1),
-        (eresolve_tac prems 1),
-        (etac exE 1),
-        (eresolve_tac prems 1)
-        ]);
-
-qed_goalw "Ilift1"  Lift1.thy [Ilift_def,UU_lift_def]
-        "Ilift(f)(UU_lift)=UU"
- (fn prems =>
-        [
-        (stac Abs_Lift_inverse 1),
-        (stac sum_case_Inl 1),
-        (rtac refl 1)
-        ]);
-
-qed_goalw "Ilift2"  Lift1.thy [Ilift_def,Iup_def]
-        "Ilift(f)(Iup(x))=f`x"
- (fn prems =>
-        [
-        (stac Abs_Lift_inverse 1),
-        (stac sum_case_Inr 1),
-        (rtac refl 1)
-        ]);
-
-val Lift0_ss = (simpset_of "Cfun3") addsimps [Ilift1,Ilift2];
-
-qed_goalw "less_lift1a"  Lift1.thy [less_lift_def,UU_lift_def]
-        "less_lift(UU_lift)(z)"
- (fn prems =>
-        [
-        (stac Abs_Lift_inverse 1),
-        (stac sum_case_Inl 1),
-        (rtac TrueI 1)
-        ]);
-
-qed_goalw "less_lift1b"  Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
-        "~less_lift (Iup x) UU_lift"
- (fn prems =>
-        [
-        (rtac notI 1),
-        (rtac iffD1 1),
-        (atac 2),
-        (stac Abs_Lift_inverse 1),
-        (stac Abs_Lift_inverse 1),
-        (stac sum_case_Inr 1),
-        (stac sum_case_Inl 1),
-        (rtac refl 1)
-        ]);
-
-qed_goalw "less_lift1c"  Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
-        "less_lift (Iup x) (Iup y)=(x<<y)"
- (fn prems =>
-        [
-        (stac Abs_Lift_inverse 1),
-        (stac Abs_Lift_inverse 1),
-        (stac sum_case_Inr 1),
-        (stac sum_case_Inr 1),
-        (rtac refl 1)
-        ]);
-
-
-qed_goal "refl_less_lift"  Lift1.thy "less_lift p p"
- (fn prems =>
-        [
-        (res_inst_tac [("p","p")] liftE 1),
-        (hyp_subst_tac 1),
-        (rtac less_lift1a 1),
-        (hyp_subst_tac 1),
-        (rtac (less_lift1c RS iffD2) 1),
-        (rtac refl_less 1)
-        ]);
-
-qed_goal "antisym_less_lift"  Lift1.thy 
-        "!!p1. [|less_lift p1 p2;less_lift p2 p1|] ==> p1=p2"
- (fn _ =>
-        [
-        (res_inst_tac [("p","p1")] liftE 1),
-        (hyp_subst_tac 1),
-        (res_inst_tac [("p","p2")] liftE 1),
-        (etac sym 1),
-        (hyp_subst_tac 1),
-        (res_inst_tac [("P","less_lift (Iup x) UU_lift")] notE 1),
-        (rtac less_lift1b 1),
-        (atac 1),
-        (hyp_subst_tac 1),
-        (res_inst_tac [("p","p2")] liftE 1),
-        (hyp_subst_tac 1),
-        (res_inst_tac [("P","less_lift (Iup x) UU_lift")] notE 1),
-        (rtac less_lift1b 1),
-        (atac 1),
-        (hyp_subst_tac 1),
-        (rtac arg_cong 1),
-        (rtac antisym_less 1),
-        (etac (less_lift1c RS iffD1) 1),
-        (etac (less_lift1c RS iffD1) 1)
-        ]);
-
-qed_goal "trans_less_lift"  Lift1.thy 
-        "[|less_lift p1 p2;less_lift p2 p3|] ==> less_lift p1 p3"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (res_inst_tac [("p","p1")] liftE 1),
-        (hyp_subst_tac 1),
-        (rtac less_lift1a 1),
-        (hyp_subst_tac 1),
-        (res_inst_tac [("p","p2")] liftE 1),
-        (hyp_subst_tac 1),
-        (rtac notE 1),
-        (rtac less_lift1b 1),
-        (atac 1),
-        (hyp_subst_tac 1),
-        (res_inst_tac [("p","p3")] liftE 1),
-        (hyp_subst_tac 1),
-        (rtac notE 1),
-        (rtac less_lift1b 1),
-        (atac 1),
-        (hyp_subst_tac 1),
-        (rtac (less_lift1c RS iffD2) 1),
-        (rtac trans_less 1),
-        (etac (less_lift1c RS iffD1) 1),
-        (etac (less_lift1c RS iffD1) 1)
-        ]);
-
--- a/src/HOLCF/Lift1.thy	Fri Nov 29 12:17:30 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(*  Title:      HOLCF/Lift1.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993  Technische Universitaet Muenchen
-
-
-Lifting
-
-*)
-
-Lift1 = Cfun3 + Sum + 
-
-(* new type for lifting *)
-
-types "u" 1
-
-arities "u" :: (pcpo)term       
-
-consts
-
-  Rep_Lift      :: "('a)u => (void + 'a)"
-  Abs_Lift      :: "(void + 'a) => ('a)u"
-
-  Iup           :: "'a => ('a)u"
-  UU_lift       :: "('a)u"
-  Ilift         :: "('a->'b)=>('a)u => 'b"
-  less_lift     :: "('a)u => ('a)u => bool"
-
-rules
-
-  (*faking a type definition... *)
-  (* ('a)u is isomorphic to void + 'a  *)
-
-  Rep_Lift_inverse      "Abs_Lift(Rep_Lift(p)) = p"     
-  Abs_Lift_inverse      "Rep_Lift(Abs_Lift(p)) = p"
-
-   (*defining the abstract constants*)
-
-defs
-  UU_lift_def   "UU_lift == Abs_Lift(Inl(UU))"
-  Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
-
-  Ilift_def     "Ilift(f)(x)== 
-                case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f`z"
- 
-  less_lift_def "less_lift(x1)(x2) ==           
-          (case Rep_Lift(x1) of                 
-               Inl(y1) => True          
-             | Inr(y2) =>                       
-                   (case Rep_Lift(x2) of Inl(z1) => False       
-                                       | Inr(z2) => y2<<z2))"
-
-end
-
-
-
--- a/src/HOLCF/Lift2.ML	Fri Nov 29 12:17:30 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-(*  Title:      HOLCF/lift2.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Lemmas for lift2.thy 
-*)
-
-open Lift2;
-
-(* -------------------------------------------------------------------------*)
-(* type ('a)u is pointed                                                    *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "minimal_lift" Lift2.thy "UU_lift << z"
- (fn prems =>
-        [
-        (stac inst_lift_po 1),
-        (rtac less_lift1a 1)
-        ]);
-
-(* -------------------------------------------------------------------------*)
-(* access to less_lift in class po                                          *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "less_lift2b" Lift2.thy "~ Iup(x) << UU_lift"
- (fn prems =>
-        [
-        (stac inst_lift_po 1),
-        (rtac less_lift1b 1)
-        ]);
-
-qed_goal "less_lift2c" Lift2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
- (fn prems =>
-        [
-        (stac inst_lift_po 1),
-        (rtac less_lift1c 1)
-        ]);
-
-(* ------------------------------------------------------------------------ *)
-(* Iup and Ilift are monotone                                               *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "monofun_Iup" Lift2.thy [monofun] "monofun(Iup)"
- (fn prems =>
-        [
-        (strip_tac 1),
-        (etac (less_lift2c RS iffD2) 1)
-        ]);
-
-qed_goalw "monofun_Ilift1" Lift2.thy [monofun] "monofun(Ilift)"
- (fn prems =>
-        [
-        (strip_tac 1),
-        (rtac (less_fun RS iffD2) 1),
-        (strip_tac 1),
-        (res_inst_tac [("p","xa")] liftE 1),
-        (asm_simp_tac Lift0_ss 1),
-        (asm_simp_tac Lift0_ss 1),
-        (etac monofun_cfun_fun 1)
-        ]);
-
-qed_goalw "monofun_Ilift2" Lift2.thy [monofun] "monofun(Ilift(f))"
- (fn prems =>
-        [
-        (strip_tac 1),
-        (res_inst_tac [("p","x")] liftE 1),
-        (asm_simp_tac Lift0_ss 1),
-        (asm_simp_tac Lift0_ss 1),
-        (res_inst_tac [("p","y")] liftE 1),
-        (hyp_subst_tac 1),
-        (rtac notE 1),
-        (rtac less_lift2b 1),
-        (atac 1),
-        (asm_simp_tac Lift0_ss 1),
-        (rtac monofun_cfun_arg 1),
-        (hyp_subst_tac 1),
-        (etac (less_lift2c  RS iffD1) 1)
-        ]);
-
-(* ------------------------------------------------------------------------ *)
-(* Some kind of surjectivity lemma                                          *)
-(* ------------------------------------------------------------------------ *)
-
-
-qed_goal "lift_lemma1" Lift2.thy  "z=Iup(x) ==> Iup(Ilift(LAM x.x)(z)) = z"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac Lift0_ss 1)
-        ]);
-
-(* ------------------------------------------------------------------------ *)
-(* ('a)u is a cpo                                                           *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "lub_lift1a" Lift2.thy 
-"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
-\ range(Y) <<| Iup(lub(range(%i.(Ilift (LAM x.x) (Y(i))))))"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac is_lubI 1),
-        (rtac conjI 1),
-        (rtac ub_rangeI 1),
-        (rtac allI 1),
-        (res_inst_tac [("p","Y(i)")] liftE 1),
-        (res_inst_tac [("s","UU_lift"),("t","Y(i)")] subst 1),
-        (etac sym 1),
-        (rtac minimal_lift 1),
-        (res_inst_tac [("t","Y(i)")] (lift_lemma1 RS subst) 1),
-        (atac 1),
-        (rtac (less_lift2c RS iffD2) 1),
-        (rtac is_ub_thelub 1),
-        (etac (monofun_Ilift2 RS ch2ch_monofun) 1),
-        (strip_tac 1),
-        (res_inst_tac [("p","u")] liftE 1),
-        (etac exE 1),
-        (etac exE 1),
-        (res_inst_tac [("P","Y(i)<<UU_lift")] notE 1),
-        (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
-        (atac 1),
-        (rtac less_lift2b 1),
-        (hyp_subst_tac 1),
-        (etac (ub_rangeE RS spec) 1),
-        (res_inst_tac [("t","u")] (lift_lemma1 RS subst) 1),
-        (atac 1),
-        (rtac (less_lift2c RS iffD2) 1),
-        (rtac is_lub_thelub 1),
-        (etac (monofun_Ilift2 RS ch2ch_monofun) 1),
-        (etac (monofun_Ilift2 RS ub2ub_monofun) 1)
-        ]);
-
-qed_goal "lub_lift1b" Lift2.thy 
-"[|is_chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
-\ range(Y) <<| UU_lift"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac is_lubI 1),
-        (rtac conjI 1),
-        (rtac ub_rangeI 1),
-        (rtac allI 1),
-        (res_inst_tac [("p","Y(i)")] liftE 1),
-        (res_inst_tac [("s","UU_lift"),("t","Y(i)")] ssubst 1),
-        (atac 1),
-        (rtac refl_less 1),
-        (rtac notE 1),
-        (dtac spec 1),
-        (dtac spec 1),
-        (atac 1),
-        (atac 1),
-        (strip_tac 1),
-        (rtac minimal_lift 1)
-        ]);
-
-bind_thm ("thelub_lift1a", lub_lift1a RS thelubI);
-(*
-[| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
- lub (range ?Y1) = Iup (lub (range (%i. Ilift (LAM x. x) (?Y1 i))))
-*)
-
-bind_thm ("thelub_lift1b", lub_lift1b RS thelubI);
-(*
-[| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
- lub (range ?Y1) = UU_lift
-*)
-
-qed_goal "cpo_lift" Lift2.thy 
-        "is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac disjE 1),
-        (rtac exI 2),
-        (etac lub_lift1a 2),
-        (atac 2),
-        (rtac exI 2),
-        (etac lub_lift1b 2),
-        (atac 2),
-        (fast_tac HOL_cs 1)
-        ]);
-
--- a/src/HOLCF/Lift2.thy	Fri Nov 29 12:17:30 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      HOLCF/lift2.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Class Instance u::(pcpo)po
-
-*)
-
-Lift2 = Lift1 + 
-
-(* Witness for the above arity axiom is lift1.ML *)
-
-arities "u" :: (pcpo)po
-
-rules
-
-(* instance of << for type ('a)u  *)
-
-inst_lift_po    "((op <<)::[('a)u,('a)u]=>bool) = less_lift"
-
-end
-
-
-
--- a/src/HOLCF/Lift3.ML	Fri Nov 29 12:17:30 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,347 +0,0 @@
-(*  Title:      HOLCF/lift3.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Lemmas for lift3.thy
-*)
-
-open Lift3;
-
-(* -------------------------------------------------------------------------*)
-(* some lemmas restated for class pcpo                                      *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "less_lift3b" Lift3.thy "~ Iup(x) << UU"
- (fn prems =>
-        [
-        (stac inst_lift_pcpo 1),
-        (rtac less_lift2b 1)
-        ]);
-
-qed_goal "defined_Iup2" Lift3.thy "Iup(x) ~= UU"
- (fn prems =>
-        [
-        (stac inst_lift_pcpo 1),
-        (rtac defined_Iup 1)
-        ]);
-
-(* ------------------------------------------------------------------------ *)
-(* continuity for Iup                                                       *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "contlub_Iup" Lift3.thy "contlub(Iup)"
- (fn prems =>
-        [
-        (rtac contlubI 1),
-        (strip_tac 1),
-        (rtac trans 1),
-        (rtac (thelub_lift1a RS sym) 2),
-        (fast_tac HOL_cs 3),
-        (etac (monofun_Iup RS ch2ch_monofun) 2),
-        (res_inst_tac [("f","Iup")] arg_cong  1),
-        (rtac lub_equal 1),
-        (atac 1),
-        (rtac (monofun_Ilift2 RS ch2ch_monofun) 1),
-        (etac (monofun_Iup RS ch2ch_monofun) 1),
-        (asm_simp_tac Lift0_ss 1)
-        ]);
-
-qed_goal "cont_Iup" Lift3.thy "cont(Iup)"
- (fn prems =>
-        [
-        (rtac monocontlub2cont 1),
-        (rtac monofun_Iup 1),
-        (rtac contlub_Iup 1)
-        ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* continuity for Ilift                                                     *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "contlub_Ilift1" Lift3.thy "contlub(Ilift)"
- (fn prems =>
-        [
-        (rtac contlubI 1),
-        (strip_tac 1),
-        (rtac trans 1),
-        (rtac (thelub_fun RS sym) 2),
-        (etac (monofun_Ilift1 RS ch2ch_monofun) 2),
-        (rtac ext 1),
-        (res_inst_tac [("p","x")] liftE 1),
-        (asm_simp_tac Lift0_ss 1),
-        (rtac (lub_const RS thelubI RS sym) 1),
-        (asm_simp_tac Lift0_ss 1),
-        (etac contlub_cfun_fun 1)
-        ]);
-
-
-qed_goal "contlub_Ilift2" Lift3.thy "contlub(Ilift(f))"
- (fn prems =>
-        [
-        (rtac contlubI 1),
-        (strip_tac 1),
-        (rtac disjE 1),
-        (stac thelub_lift1a 2),
-        (atac 2),
-        (atac 2),
-        (asm_simp_tac Lift0_ss 2),
-        (stac thelub_lift1b 3),
-        (atac 3),
-        (atac 3),
-        (fast_tac HOL_cs 1),
-        (asm_simp_tac Lift0_ss 2),
-        (rtac (chain_UU_I_inverse RS sym) 2),
-        (rtac allI 2),
-        (res_inst_tac [("p","Y(i)")] liftE 2),
-        (asm_simp_tac Lift0_ss 2),
-        (rtac notE 2),
-        (dtac spec 2),
-        (etac spec 2),
-        (atac 2),
-        (stac contlub_cfun_arg 1),
-        (etac (monofun_Ilift2 RS ch2ch_monofun) 1),
-        (rtac lub_equal2 1),
-        (rtac (monofun_fapp2 RS ch2ch_monofun) 2),
-        (etac (monofun_Ilift2 RS ch2ch_monofun) 2),
-        (etac (monofun_Ilift2 RS ch2ch_monofun) 2),
-        (rtac (chain_mono2 RS exE) 1),
-        (atac 2),
-        (etac exE 1),
-        (etac exE 1),
-        (rtac exI 1),
-        (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
-        (atac 1),
-        (rtac defined_Iup2 1),
-        (rtac exI 1),
-        (strip_tac 1),
-        (res_inst_tac [("p","Y(i)")] liftE 1),
-        (asm_simp_tac Lift0_ss 2),
-        (res_inst_tac [("P","Y(i) = UU")] notE 1),
-        (fast_tac HOL_cs 1),
-        (stac inst_lift_pcpo 1),
-        (atac 1)
-        ]);
-
-qed_goal "cont_Ilift1" Lift3.thy "cont(Ilift)"
- (fn prems =>
-        [
-        (rtac monocontlub2cont 1),
-        (rtac monofun_Ilift1 1),
-        (rtac contlub_Ilift1 1)
-        ]);
-
-qed_goal "cont_Ilift2" Lift3.thy "cont(Ilift(f))"
- (fn prems =>
-        [
-        (rtac monocontlub2cont 1),
-        (rtac monofun_Ilift2 1),
-        (rtac contlub_Ilift2 1)
-        ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* continuous versions of lemmas for ('a)u                                  *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "Exh_Lift1" Lift3.thy [up_def] "z = UU | (? x. z = up`x)"
- (fn prems =>
-        [
-        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
-        (stac inst_lift_pcpo 1),
-        (rtac Exh_Lift 1)
-        ]);
-
-qed_goalw "inject_up" Lift3.thy [up_def] "up`x=up`y ==> x=y"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac inject_Iup 1),
-        (etac box_equals 1),
-        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
-        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
-        ]);
-
-qed_goalw "defined_up" Lift3.thy [up_def] " up`x ~= UU"
- (fn prems =>
-        [
-        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
-        (rtac defined_Iup2 1)
-        ]);
-
-qed_goalw "liftE1" Lift3.thy [up_def] 
-        "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"
- (fn prems =>
-        [
-        (rtac liftE 1),
-        (resolve_tac prems 1),
-        (etac (inst_lift_pcpo RS ssubst) 1),
-        (resolve_tac (tl prems) 1),
-        (asm_simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
-        ]);
-
-
-qed_goalw "lift1" Lift3.thy [up_def,lift_def] "lift`f`UU=UU"
- (fn prems =>
-        [
-        (stac inst_lift_pcpo 1),
-        (stac beta_cfun 1),
-        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
-                cont_Ilift2,cont2cont_CF1L]) 1)),
-        (stac beta_cfun 1),
-        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
-                cont_Ilift2,cont2cont_CF1L]) 1)),
-        (simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
-        ]);
-
-qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x"
- (fn prems =>
-        [
-        (stac beta_cfun 1),
-        (rtac cont_Iup 1),
-        (stac beta_cfun 1),
-        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
-                cont_Ilift2,cont2cont_CF1L]) 1)),
-        (stac beta_cfun 1),
-        (rtac cont_Ilift2 1),
-        (simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
-        ]);
-
-qed_goalw "less_lift4b" Lift3.thy [up_def,lift_def] "~ up`x << UU"
- (fn prems =>
-        [
-        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
-        (rtac less_lift3b 1)
-        ]);
-
-qed_goalw "less_lift4c" Lift3.thy [up_def,lift_def]
-         "(up`x << up`y) = (x<<y)"
- (fn prems =>
-        [
-        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
-        (rtac less_lift2c 1)
-        ]);
-
-qed_goalw "thelub_lift2a" Lift3.thy [up_def,lift_def] 
-"[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\
-\      lub(range(Y)) = up`(lub(range(%i. lift`(LAM x. x)`(Y i))))"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (stac beta_cfun 1),
-        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
-                cont_Ilift2,cont2cont_CF1L]) 1)),
-        (stac beta_cfun 1),
-        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
-                cont_Ilift2,cont2cont_CF1L]) 1)),
-
-        (stac (beta_cfun RS ext) 1),
-        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
-                cont_Ilift2,cont2cont_CF1L]) 1)),
-        (rtac thelub_lift1a 1),
-        (atac 1),
-        (etac exE 1),
-        (etac exE 1),
-        (rtac exI 1),
-        (rtac exI 1),
-        (etac box_equals 1),
-        (rtac refl 1),
-        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
-        ]);
-
-
-
-qed_goalw "thelub_lift2b" Lift3.thy [up_def,lift_def] 
-"[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (stac inst_lift_pcpo 1),
-        (rtac thelub_lift1b 1),
-        (atac 1),
-        (strip_tac 1),
-        (dtac spec 1),
-        (dtac spec 1),
-        (rtac swap 1),
-        (atac 1),
-        (dtac notnotD 1),
-        (etac box_equals 1),
-        (rtac refl 1),
-        (simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
-        ]);
-
-
-qed_goal "lift_lemma2" Lift3.thy  " (? x.z = up`x) = (z~=UU)"
- (fn prems =>
-        [
-        (rtac iffI 1),
-        (etac exE 1),
-        (hyp_subst_tac 1),
-        (rtac defined_up 1),
-        (res_inst_tac [("p","z")] liftE1 1),
-        (etac notE 1),
-        (atac 1),
-        (etac exI 1)
-        ]);
-
-
-qed_goal "thelub_lift2a_rev" Lift3.thy  
-"[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac exE 1),
-        (rtac chain_UU_I_inverse2 1),
-        (rtac (lift_lemma2 RS iffD1) 1),
-        (etac exI 1),
-        (rtac exI 1),
-        (rtac (lift_lemma2 RS iffD2) 1),
-        (atac 1)
-        ]);
-
-qed_goal "thelub_lift2b_rev" Lift3.thy  
-"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac allI 1),
-        (rtac (not_ex RS iffD1) 1),
-        (rtac contrapos 1),
-        (etac (lift_lemma2 RS iffD1) 2),
-        (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
-        ]);
-
-
-qed_goal "thelub_lift3" Lift3.thy  
-"is_chain(Y) ==> lub(range(Y)) = UU |\
-\                lub(range(Y)) = up`(lub(range(%i. lift`(LAM x.x)`(Y i))))"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac disjE 1),
-        (rtac disjI1 2),
-        (rtac thelub_lift2b 2),
-        (atac 2),
-        (atac 2),
-        (rtac disjI2 2),
-        (rtac thelub_lift2a 2),
-        (atac 2),
-        (atac 2),
-        (fast_tac HOL_cs 1)
-        ]);
-
-qed_goal "lift3" Lift3.thy "lift`up`x=x"
- (fn prems =>
-        [
-        (res_inst_tac [("p","x")] liftE1 1),
-        (asm_simp_tac ((simpset_of "Cfun3") addsimps [lift1,lift2]) 1),
-        (asm_simp_tac ((simpset_of "Cfun3") addsimps [lift1,lift2]) 1)
-        ]);
-
-(* ------------------------------------------------------------------------ *)
-(* install simplifier for ('a)u                                             *)
-(* ------------------------------------------------------------------------ *)
-
-val lift_rews = [lift1,lift2,defined_up];
-
--- a/src/HOLCF/Lift3.thy	Fri Nov 29 12:17:30 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      HOLCF/lift3.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-
-Class instance of  ('a)u for class pcpo
-
-*)
-
-Lift3 = Lift2 +
-
-arities "u" :: (pcpo)pcpo                       (* Witness lift2.ML *)
-
-consts  
-        up           :: "'a -> ('a)u" 
-        lift         :: "('a->'c)-> ('a)u -> 'c"
-
-rules 
-
-        inst_lift_pcpo  "(UU::('a)u) = UU_lift"
-
-defs
-        up_def          "up     == (LAM x.Iup(x))"
-        lift_def        "lift   == (LAM f p.Ilift(f)(p))"
-
-translations
-"case l of up`x => t1" == "lift`(LAM x.t1)`l"
-
-(* start 8bit 1 *)
-(* end 8bit 1 *)
-
-end
-
-
-
--- a/src/HOLCF/Pcpo.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Pcpo.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -14,5 +14,11 @@
 inst_void_pcpo  "(UU::void) = UU_void"
 
 (* start 8bit 1 *)
+syntax
+	"GUU" :: "'a::pcpo"	("")	
+
+translations
+  ""		== "UU"
+
 (* end 8bit 1 *)
 end 
--- a/src/HOLCF/Porder.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Porder.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -43,6 +43,13 @@
 lub             "lub(S) = (@x. S <<| x)"
 
 (* start 8bit 1 *)
+
+syntax
+  "Glub"        :: "[pttrn, 'a] => 'a"               ("(3_./ _)" 10)
+
+translations
+  "x.t"	== "lub(range(%x.t))"
+
 (* end 8bit 1 *)
 
 end 
--- a/src/HOLCF/Porder0.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Porder0.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -40,6 +40,12 @@
 inst_void_po    "((op <<)::[void,void]=>bool) = less_void"
 
 (* start 8bit 1 *)
+syntax
+	""	::	"['a,'a::po] => bool"	(infixl 55)
+
+translations
+  "x  y"	== "x << y"
+
 (* end 8bit 1 *)
 
 end 
--- a/src/HOLCF/ROOT.ML	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/ROOT.ML	Fri Nov 29 12:22:22 1996 +0100
@@ -11,6 +11,8 @@
 init_thy_reader();
 
 (* start 8bit 1 *)
+val banner = 
+        "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
 (* end 8bit 1 *)
 
 writeln banner;
--- a/src/HOLCF/Sprod0.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Sprod0.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -51,6 +51,14 @@
                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
 
 (* start 8bit 1 *)
+types
+
+('a, 'b) ""          (infixr 20)
+
+translations
+
+(type)  "x  y"	== (type) "x ** y" 
+
 (* end 8bit 1 *)
 
 end
--- a/src/HOLCF/Sprod3.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Sprod3.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -34,6 +34,12 @@
 ssplit_def      "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
 
 (* start 8bit 1 *)
+syntax  
+	"@Gstuple"    :: "['a, args] => 'a ** 'b"	("(1_,/ _)")
+
+translations
+	"x, y, z"   == "x, y, z"
+	"x, y"      == "(|x,y|)"
 (* end 8bit 1 *)
 
 end
--- a/src/HOLCF/Ssum0.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Ssum0.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -52,6 +52,14 @@
                         &(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
 
 (* start 8bit 1 *)
+types
+
+('a, 'b) ""          (infixr 10)
+
+translations
+
+(type)  "x  y"	== (type) "x ++ y" 
+
 (* end 8bit 1 *)
 end
 
--- a/src/HOLCF/Ssum3.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Ssum3.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -30,6 +30,9 @@
 "case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"
 
 (* start 8bit 1 *)
+translations
+"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(x.t1)`(y.t2)`s"
+
 (* end 8bit 1 *)
 
 end
--- a/src/HOLCF/Tr1.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Tr1.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -43,6 +43,14 @@
         (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))"
 
 (* start 8bit 1 *)
+syntax
+  "GeqTT"        :: "tr => bool"               ("(_)")
+  "GeqFF"        :: "tr => bool"               ("(_)")
+
+translations
+  "x"	== "x = TT"
+  "x"	== "x = FF"
+
 (* end 8bit 1 *)
 
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Up1.ML	Fri Nov 29 12:22:22 1996 +0100
@@ -0,0 +1,186 @@
+(*  Title:      HOLCF/Up1.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993  Technische Universitaet Muenchen
+*)
+
+open Up1;
+
+qed_goalw "Exh_Up" Up1.thy [UU_up_def,Iup_def ]
+        "z = UU_up | (? x. z = Iup(x))"
+ (fn prems =>
+        [
+        (rtac (Rep_Up_inverse RS subst) 1),
+        (res_inst_tac [("s","Rep_Up(z)")] sumE 1),
+        (rtac disjI1 1),
+        (res_inst_tac [("f","Abs_Up")] arg_cong 1),
+        (rtac (unique_void2 RS subst) 1),
+        (atac 1),
+        (rtac disjI2 1),
+        (rtac exI 1),
+        (res_inst_tac [("f","Abs_Up")] arg_cong 1),
+        (atac 1)
+        ]);
+
+qed_goal "inj_Abs_Up" Up1.thy "inj(Abs_Up)"
+ (fn prems =>
+        [
+        (rtac inj_inverseI 1),
+        (rtac Abs_Up_inverse 1)
+        ]);
+
+qed_goal "inj_Rep_Up" Up1.thy "inj(Rep_Up)"
+ (fn prems =>
+        [
+        (rtac inj_inverseI 1),
+        (rtac Rep_Up_inverse 1)
+        ]);
+
+qed_goalw "inject_Iup" Up1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac (inj_Inr RS injD) 1),
+        (rtac (inj_Abs_Up RS injD) 1),
+        (atac 1)
+        ]);
+
+qed_goalw "defined_Iup" Up1.thy [Iup_def,UU_up_def] "Iup(x)~=UU_up"
+ (fn prems =>
+        [
+        (rtac notI 1),
+        (rtac notE 1),
+        (rtac Inl_not_Inr 1),
+        (rtac sym 1),
+        (etac (inj_Abs_Up RS  injD) 1)
+        ]);
+
+
+qed_goal "upE"  Up1.thy
+        "[| p=UU_up ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
+ (fn prems =>
+        [
+        (rtac (Exh_Up RS disjE) 1),
+        (eresolve_tac prems 1),
+        (etac exE 1),
+        (eresolve_tac prems 1)
+        ]);
+
+qed_goalw "Ifup1"  Up1.thy [Ifup_def,UU_up_def]
+        "Ifup(f)(UU_up)=UU"
+ (fn prems =>
+        [
+        (stac Abs_Up_inverse 1),
+        (stac sum_case_Inl 1),
+        (rtac refl 1)
+        ]);
+
+qed_goalw "Ifup2"  Up1.thy [Ifup_def,Iup_def]
+        "Ifup(f)(Iup(x))=f`x"
+ (fn prems =>
+        [
+        (stac Abs_Up_inverse 1),
+        (stac sum_case_Inr 1),
+        (rtac refl 1)
+        ]);
+
+val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2];
+
+qed_goalw "less_up1a"  Up1.thy [less_up_def,UU_up_def]
+        "less_up(UU_up)(z)"
+ (fn prems =>
+        [
+        (stac Abs_Up_inverse 1),
+        (stac sum_case_Inl 1),
+        (rtac TrueI 1)
+        ]);
+
+qed_goalw "less_up1b"  Up1.thy [Iup_def,less_up_def,UU_up_def]
+        "~less_up (Iup x) UU_up"
+ (fn prems =>
+        [
+        (rtac notI 1),
+        (rtac iffD1 1),
+        (atac 2),
+        (stac Abs_Up_inverse 1),
+        (stac Abs_Up_inverse 1),
+        (stac sum_case_Inr 1),
+        (stac sum_case_Inl 1),
+        (rtac refl 1)
+        ]);
+
+qed_goalw "less_up1c"  Up1.thy [Iup_def,less_up_def,UU_up_def]
+        "less_up (Iup x) (Iup y)=(x<<y)"
+ (fn prems =>
+        [
+        (stac Abs_Up_inverse 1),
+        (stac Abs_Up_inverse 1),
+        (stac sum_case_Inr 1),
+        (stac sum_case_Inr 1),
+        (rtac refl 1)
+        ]);
+
+
+qed_goal "refl_less_up"  Up1.thy "less_up p p"
+ (fn prems =>
+        [
+        (res_inst_tac [("p","p")] upE 1),
+        (hyp_subst_tac 1),
+        (rtac less_up1a 1),
+        (hyp_subst_tac 1),
+        (rtac (less_up1c RS iffD2) 1),
+        (rtac refl_less 1)
+        ]);
+
+qed_goal "antisym_less_up"  Up1.thy 
+        "!!p1. [|less_up p1 p2;less_up p2 p1|] ==> p1=p2"
+ (fn _ =>
+        [
+        (res_inst_tac [("p","p1")] upE 1),
+        (hyp_subst_tac 1),
+        (res_inst_tac [("p","p2")] upE 1),
+        (etac sym 1),
+        (hyp_subst_tac 1),
+        (res_inst_tac [("P","less_up (Iup x) UU_up")] notE 1),
+        (rtac less_up1b 1),
+        (atac 1),
+        (hyp_subst_tac 1),
+        (res_inst_tac [("p","p2")] upE 1),
+        (hyp_subst_tac 1),
+        (res_inst_tac [("P","less_up (Iup x) UU_up")] notE 1),
+        (rtac less_up1b 1),
+        (atac 1),
+        (hyp_subst_tac 1),
+        (rtac arg_cong 1),
+        (rtac antisym_less 1),
+        (etac (less_up1c RS iffD1) 1),
+        (etac (less_up1c RS iffD1) 1)
+        ]);
+
+qed_goal "trans_less_up"  Up1.thy 
+        "[|less_up p1 p2;less_up p2 p3|] ==> less_up p1 p3"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (res_inst_tac [("p","p1")] upE 1),
+        (hyp_subst_tac 1),
+        (rtac less_up1a 1),
+        (hyp_subst_tac 1),
+        (res_inst_tac [("p","p2")] upE 1),
+        (hyp_subst_tac 1),
+        (rtac notE 1),
+        (rtac less_up1b 1),
+        (atac 1),
+        (hyp_subst_tac 1),
+        (res_inst_tac [("p","p3")] upE 1),
+        (hyp_subst_tac 1),
+        (rtac notE 1),
+        (rtac less_up1b 1),
+        (atac 1),
+        (hyp_subst_tac 1),
+        (rtac (less_up1c RS iffD2) 1),
+        (rtac trans_less 1),
+        (etac (less_up1c RS iffD1) 1),
+        (etac (less_up1c RS iffD1) 1)
+        ]);
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Up1.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -0,0 +1,51 @@
+(*  Title:      HOLCF/Up1.thy
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993  Technische Universitaet Muenchen
+
+
+Lifting
+
+*)
+
+Up1 = Cfun3 + Sum + 
+
+(* new type for lifting *)
+
+types "u" 1
+
+arities "u" :: (pcpo)term       
+
+consts
+
+  Rep_Up      :: "('a)u => (void + 'a)"
+  Abs_Up      :: "(void + 'a) => ('a)u"
+
+  Iup         :: "'a => ('a)u"
+  UU_up       :: "('a)u"
+  Ifup        :: "('a->'b)=>('a)u => 'b"
+  less_up     :: "('a)u => ('a)u => bool"
+
+rules
+
+  (*faking a type definition... *)
+  (* ('a)u is isomorphic to void + 'a  *)
+
+  Rep_Up_inverse  "Abs_Up(Rep_Up(p)) = p"     
+  Abs_Up_inverse  "Rep_Up(Abs_Up(p)) = p"
+
+   (*defining the abstract constants*)
+
+defs
+
+  UU_up_def   "UU_up == Abs_Up(Inl(UU))"
+  Iup_def     "Iup x == Abs_Up(Inr(x))"
+
+  Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
+ 
+  less_up_def "less_up(x1)(x2) == (case Rep_Up(x1) of                 
+               Inl(y1) => True          
+             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
+                                            | Inr(z2) => y2<<z2))"
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Up2.ML	Fri Nov 29 12:22:22 1996 +0100
@@ -0,0 +1,183 @@
+(*  Title:      HOLCF/Up2.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Lemmas for up2.thy 
+*)
+
+open Up2;
+
+(* -------------------------------------------------------------------------*)
+(* type ('a)u is pointed                                                    *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "minimal_up" Up2.thy "UU_up << z"
+ (fn prems =>
+        [
+        (stac inst_up_po 1),
+        (rtac less_up1a 1)
+        ]);
+
+(* -------------------------------------------------------------------------*)
+(* access to less_up in class po                                          *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "less_up2b" Up2.thy "~ Iup(x) << UU_up"
+ (fn prems =>
+        [
+        (stac inst_up_po 1),
+        (rtac less_up1b 1)
+        ]);
+
+qed_goal "less_up2c" Up2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
+ (fn prems =>
+        [
+        (stac inst_up_po 1),
+        (rtac less_up1c 1)
+        ]);
+
+(* ------------------------------------------------------------------------ *)
+(* Iup and Ifup are monotone                                               *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goalw "monofun_Iup" Up2.thy [monofun] "monofun(Iup)"
+ (fn prems =>
+        [
+        (strip_tac 1),
+        (etac (less_up2c RS iffD2) 1)
+        ]);
+
+qed_goalw "monofun_Ifup1" Up2.thy [monofun] "monofun(Ifup)"
+ (fn prems =>
+        [
+        (strip_tac 1),
+        (rtac (less_fun RS iffD2) 1),
+        (strip_tac 1),
+        (res_inst_tac [("p","xa")] upE 1),
+        (asm_simp_tac Up0_ss 1),
+        (asm_simp_tac Up0_ss 1),
+        (etac monofun_cfun_fun 1)
+        ]);
+
+qed_goalw "monofun_Ifup2" Up2.thy [monofun] "monofun(Ifup(f))"
+ (fn prems =>
+        [
+        (strip_tac 1),
+        (res_inst_tac [("p","x")] upE 1),
+        (asm_simp_tac Up0_ss 1),
+        (asm_simp_tac Up0_ss 1),
+        (res_inst_tac [("p","y")] upE 1),
+        (hyp_subst_tac 1),
+        (rtac notE 1),
+        (rtac less_up2b 1),
+        (atac 1),
+        (asm_simp_tac Up0_ss 1),
+        (rtac monofun_cfun_arg 1),
+        (hyp_subst_tac 1),
+        (etac (less_up2c  RS iffD1) 1)
+        ]);
+
+(* ------------------------------------------------------------------------ *)
+(* Some kind of surjectivity lemma                                          *)
+(* ------------------------------------------------------------------------ *)
+
+
+qed_goal "up_lemma1" Up2.thy  "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (asm_simp_tac Up0_ss 1)
+        ]);
+
+(* ------------------------------------------------------------------------ *)
+(* ('a)u is a cpo                                                           *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "lub_up1a" Up2.thy 
+"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
+\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x.x) (Y(i))))))"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac is_lubI 1),
+        (rtac conjI 1),
+        (rtac ub_rangeI 1),
+        (rtac allI 1),
+        (res_inst_tac [("p","Y(i)")] upE 1),
+        (res_inst_tac [("s","UU_up"),("t","Y(i)")] subst 1),
+        (etac sym 1),
+        (rtac minimal_up 1),
+        (res_inst_tac [("t","Y(i)")] (up_lemma1 RS subst) 1),
+        (atac 1),
+        (rtac (less_up2c RS iffD2) 1),
+        (rtac is_ub_thelub 1),
+        (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
+        (strip_tac 1),
+        (res_inst_tac [("p","u")] upE 1),
+        (etac exE 1),
+        (etac exE 1),
+        (res_inst_tac [("P","Y(i)<<UU_up")] notE 1),
+        (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
+        (atac 1),
+        (rtac less_up2b 1),
+        (hyp_subst_tac 1),
+        (etac (ub_rangeE RS spec) 1),
+        (res_inst_tac [("t","u")] (up_lemma1 RS subst) 1),
+        (atac 1),
+        (rtac (less_up2c RS iffD2) 1),
+        (rtac is_lub_thelub 1),
+        (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
+        (etac (monofun_Ifup2 RS ub2ub_monofun) 1)
+        ]);
+
+qed_goal "lub_up1b" Up2.thy 
+"[|is_chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
+\ range(Y) <<| UU_up"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac is_lubI 1),
+        (rtac conjI 1),
+        (rtac ub_rangeI 1),
+        (rtac allI 1),
+        (res_inst_tac [("p","Y(i)")] upE 1),
+        (res_inst_tac [("s","UU_up"),("t","Y(i)")] ssubst 1),
+        (atac 1),
+        (rtac refl_less 1),
+        (rtac notE 1),
+        (dtac spec 1),
+        (dtac spec 1),
+        (atac 1),
+        (atac 1),
+        (strip_tac 1),
+        (rtac minimal_up 1)
+        ]);
+
+bind_thm ("thelub_up1a", lub_up1a RS thelubI);
+(*
+[| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
+ lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
+*)
+
+bind_thm ("thelub_up1b", lub_up1b RS thelubI);
+(*
+[| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
+ lub (range ?Y1) = UU_up
+*)
+
+qed_goal "cpo_up" Up2.thy 
+        "is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac disjE 1),
+        (rtac exI 2),
+        (etac lub_up1a 2),
+        (atac 2),
+        (rtac exI 2),
+        (etac lub_up1b 2),
+        (atac 2),
+        (fast_tac HOL_cs 1)
+        ]);
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Up2.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -0,0 +1,25 @@
+(*  Title:      HOLCF/Up2.thy
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Class Instance u::(pcpo)po
+
+*)
+
+Up2 = Up1 + 
+
+(* Witness for the above arity axiom is up1.ML *)
+
+arities "u" :: (pcpo)po
+
+rules
+
+(* instance of << for type ('a)u  *)
+
+inst_up_po    "((op <<)::[('a)u,('a)u]=>bool) = less_up"
+
+end
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Up3.ML	Fri Nov 29 12:22:22 1996 +0100
@@ -0,0 +1,347 @@
+(*  Title:      HOLCF/Up3.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Lemmas for Up3.thy
+*)
+
+open Up3;
+
+(* -------------------------------------------------------------------------*)
+(* some lemmas restated for class pcpo                                      *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "less_up3b" Up3.thy "~ Iup(x) << UU"
+ (fn prems =>
+        [
+        (stac inst_up_pcpo 1),
+        (rtac less_up2b 1)
+        ]);
+
+qed_goal "defined_Iup2" Up3.thy "Iup(x) ~= UU"
+ (fn prems =>
+        [
+        (stac inst_up_pcpo 1),
+        (rtac defined_Iup 1)
+        ]);
+
+(* ------------------------------------------------------------------------ *)
+(* continuity for Iup                                                       *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "contlub_Iup" Up3.thy "contlub(Iup)"
+ (fn prems =>
+        [
+        (rtac contlubI 1),
+        (strip_tac 1),
+        (rtac trans 1),
+        (rtac (thelub_up1a RS sym) 2),
+        (fast_tac HOL_cs 3),
+        (etac (monofun_Iup RS ch2ch_monofun) 2),
+        (res_inst_tac [("f","Iup")] arg_cong  1),
+        (rtac lub_equal 1),
+        (atac 1),
+        (rtac (monofun_Ifup2 RS ch2ch_monofun) 1),
+        (etac (monofun_Iup RS ch2ch_monofun) 1),
+        (asm_simp_tac Up0_ss 1)
+        ]);
+
+qed_goal "cont_Iup" Up3.thy "cont(Iup)"
+ (fn prems =>
+        [
+        (rtac monocontlub2cont 1),
+        (rtac monofun_Iup 1),
+        (rtac contlub_Iup 1)
+        ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* continuity for Ifup                                                     *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "contlub_Ifup1" Up3.thy "contlub(Ifup)"
+ (fn prems =>
+        [
+        (rtac contlubI 1),
+        (strip_tac 1),
+        (rtac trans 1),
+        (rtac (thelub_fun RS sym) 2),
+        (etac (monofun_Ifup1 RS ch2ch_monofun) 2),
+        (rtac ext 1),
+        (res_inst_tac [("p","x")] upE 1),
+        (asm_simp_tac Up0_ss 1),
+        (rtac (lub_const RS thelubI RS sym) 1),
+        (asm_simp_tac Up0_ss 1),
+        (etac contlub_cfun_fun 1)
+        ]);
+
+
+qed_goal "contlub_Ifup2" Up3.thy "contlub(Ifup(f))"
+ (fn prems =>
+        [
+        (rtac contlubI 1),
+        (strip_tac 1),
+        (rtac disjE 1),
+        (stac thelub_up1a 2),
+        (atac 2),
+        (atac 2),
+        (asm_simp_tac Up0_ss 2),
+        (stac thelub_up1b 3),
+        (atac 3),
+        (atac 3),
+        (fast_tac HOL_cs 1),
+        (asm_simp_tac Up0_ss 2),
+        (rtac (chain_UU_I_inverse RS sym) 2),
+        (rtac allI 2),
+        (res_inst_tac [("p","Y(i)")] upE 2),
+        (asm_simp_tac Up0_ss 2),
+        (rtac notE 2),
+        (dtac spec 2),
+        (etac spec 2),
+        (atac 2),
+        (stac contlub_cfun_arg 1),
+        (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
+        (rtac lub_equal2 1),
+        (rtac (monofun_fapp2 RS ch2ch_monofun) 2),
+        (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
+        (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
+        (rtac (chain_mono2 RS exE) 1),
+        (atac 2),
+        (etac exE 1),
+        (etac exE 1),
+        (rtac exI 1),
+        (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
+        (atac 1),
+        (rtac defined_Iup2 1),
+        (rtac exI 1),
+        (strip_tac 1),
+        (res_inst_tac [("p","Y(i)")] upE 1),
+        (asm_simp_tac Up0_ss 2),
+        (res_inst_tac [("P","Y(i) = UU")] notE 1),
+        (fast_tac HOL_cs 1),
+        (stac inst_up_pcpo 1),
+        (atac 1)
+        ]);
+
+qed_goal "cont_Ifup1" Up3.thy "cont(Ifup)"
+ (fn prems =>
+        [
+        (rtac monocontlub2cont 1),
+        (rtac monofun_Ifup1 1),
+        (rtac contlub_Ifup1 1)
+        ]);
+
+qed_goal "cont_Ifup2" Up3.thy "cont(Ifup(f))"
+ (fn prems =>
+        [
+        (rtac monocontlub2cont 1),
+        (rtac monofun_Ifup2 1),
+        (rtac contlub_Ifup2 1)
+        ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* continuous versions of lemmas for ('a)u                                  *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goalw "Exh_Up1" Up3.thy [up_def] "z = UU | (? x. z = up`x)"
+ (fn prems =>
+        [
+        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
+        (stac inst_up_pcpo 1),
+        (rtac Exh_Up 1)
+        ]);
+
+qed_goalw "inject_up" Up3.thy [up_def] "up`x=up`y ==> x=y"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac inject_Iup 1),
+        (etac box_equals 1),
+        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
+        (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
+        ]);
+
+qed_goalw "defined_up" Up3.thy [up_def] " up`x ~= UU"
+ (fn prems =>
+        [
+        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
+        (rtac defined_Iup2 1)
+        ]);
+
+qed_goalw "upE1" Up3.thy [up_def] 
+        "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"
+ (fn prems =>
+        [
+        (rtac upE 1),
+        (resolve_tac prems 1),
+        (etac (inst_up_pcpo RS ssubst) 1),
+        (resolve_tac (tl prems) 1),
+        (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1)
+        ]);
+
+
+qed_goalw "fup1" Up3.thy [up_def,fup_def] "fup`f`UU=UU"
+ (fn prems =>
+        [
+        (stac inst_up_pcpo 1),
+        (stac beta_cfun 1),
+        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
+                cont_Ifup2,cont2cont_CF1L]) 1)),
+        (stac beta_cfun 1),
+        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
+                cont_Ifup2,cont2cont_CF1L]) 1)),
+        (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
+        ]);
+
+qed_goalw "fup2" Up3.thy [up_def,fup_def] "fup`f`(up`x)=f`x"
+ (fn prems =>
+        [
+        (stac beta_cfun 1),
+        (rtac cont_Iup 1),
+        (stac beta_cfun 1),
+        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
+                cont_Ifup2,cont2cont_CF1L]) 1)),
+        (stac beta_cfun 1),
+        (rtac cont_Ifup2 1),
+        (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
+        ]);
+
+qed_goalw "less_up4b" Up3.thy [up_def,fup_def] "~ up`x << UU"
+ (fn prems =>
+        [
+        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
+        (rtac less_up3b 1)
+        ]);
+
+qed_goalw "less_up4c" Up3.thy [up_def,fup_def]
+         "(up`x << up`y) = (x<<y)"
+ (fn prems =>
+        [
+        (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
+        (rtac less_up2c 1)
+        ]);
+
+qed_goalw "thelub_up2a" Up3.thy [up_def,fup_def] 
+"[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\
+\      lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (stac beta_cfun 1),
+        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
+                cont_Ifup2,cont2cont_CF1L]) 1)),
+        (stac beta_cfun 1),
+        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
+                cont_Ifup2,cont2cont_CF1L]) 1)),
+
+        (stac (beta_cfun RS ext) 1),
+        (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
+                cont_Ifup2,cont2cont_CF1L]) 1)),
+        (rtac thelub_up1a 1),
+        (atac 1),
+        (etac exE 1),
+        (etac exE 1),
+        (rtac exI 1),
+        (rtac exI 1),
+        (etac box_equals 1),
+        (rtac refl 1),
+        (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
+        ]);
+
+
+
+qed_goalw "thelub_up2b" Up3.thy [up_def,fup_def] 
+"[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (stac inst_up_pcpo 1),
+        (rtac thelub_up1b 1),
+        (atac 1),
+        (strip_tac 1),
+        (dtac spec 1),
+        (dtac spec 1),
+        (rtac swap 1),
+        (atac 1),
+        (dtac notnotD 1),
+        (etac box_equals 1),
+        (rtac refl 1),
+        (simp_tac (Up0_ss addsimps [cont_Iup]) 1)
+        ]);
+
+
+qed_goal "up_lemma2" Up3.thy  " (? x.z = up`x) = (z~=UU)"
+ (fn prems =>
+        [
+        (rtac iffI 1),
+        (etac exE 1),
+        (hyp_subst_tac 1),
+        (rtac defined_up 1),
+        (res_inst_tac [("p","z")] upE1 1),
+        (etac notE 1),
+        (atac 1),
+        (etac exI 1)
+        ]);
+
+
+qed_goal "thelub_up2a_rev" Up3.thy  
+"[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac exE 1),
+        (rtac chain_UU_I_inverse2 1),
+        (rtac (up_lemma2 RS iffD1) 1),
+        (etac exI 1),
+        (rtac exI 1),
+        (rtac (up_lemma2 RS iffD2) 1),
+        (atac 1)
+        ]);
+
+qed_goal "thelub_up2b_rev" Up3.thy  
+"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac allI 1),
+        (rtac (not_ex RS iffD1) 1),
+        (rtac contrapos 1),
+        (etac (up_lemma2 RS iffD1) 2),
+        (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
+        ]);
+
+
+qed_goal "thelub_up3" Up3.thy  
+"is_chain(Y) ==> lub(range(Y)) = UU |\
+\                lub(range(Y)) = up`(lub(range(%i. fup`(LAM x.x)`(Y i))))"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac disjE 1),
+        (rtac disjI1 2),
+        (rtac thelub_up2b 2),
+        (atac 2),
+        (atac 2),
+        (rtac disjI2 2),
+        (rtac thelub_up2a 2),
+        (atac 2),
+        (atac 2),
+        (fast_tac HOL_cs 1)
+        ]);
+
+qed_goal "fup3" Up3.thy "fup`up`x=x"
+ (fn prems =>
+        [
+        (res_inst_tac [("p","x")] upE1 1),
+        (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1),
+        (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1)
+        ]);
+
+(* ------------------------------------------------------------------------ *)
+(* install simplifier for ('a)u                                             *)
+(* ------------------------------------------------------------------------ *)
+
+val up_rews = [fup1,fup2,defined_up];
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Up3.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -0,0 +1,40 @@
+(*  Title:      HOLCF/Up3.thy
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+
+Class instance of  ('a)u for class pcpo
+
+*)
+
+Up3 = Up2 +
+
+arities "u" :: (pcpo)pcpo                       (* Witness up2.ML *)
+
+consts  
+        up  :: "'a -> ('a)u" 
+        fup :: "('a->'c)-> ('a)u -> 'c"
+
+rules 
+
+        inst_up_pcpo  "(UU::('a)u) = UU_up"
+
+defs
+        up_def   "up  == (LAM x.Iup(x))"
+        fup_def  "fup == (LAM f p.Ifup(f)(p))"
+
+translations
+
+"case l of up`x => t1" == "fup`(LAM x.t1)`l"
+
+(* start 8bit 1 *)
+translations
+
+"case l of up`x => t1" == "fup`(x.t1)`l"
+(* end 8bit 1 *)
+
+end
+
+
+