--- 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
+
+
+