--- a/src/HOLCF/Up2.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Up2.ML Mon Feb 17 10:57:11 1997 +0100
@@ -3,52 +3,69 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for up2.thy
+Lemmas for Up2.thy
*)
open Up2;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_up_po" thy "(op <<)=(%x1 x2.case Rep_Up(x1) of \
+\ Inl(y1) => True \
+\ | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False \
+\ | Inr(z2) => y2<<z2))"
+ (fn prems =>
+ [
+ (fold_goals_tac [po_def,less_up_def]),
+ (rtac refl 1)
+ ]);
+
(* -------------------------------------------------------------------------*)
(* type ('a)u is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_up" Up2.thy "UU_up << z"
+qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
(fn prems =>
[
- (stac inst_up_po 1),
- (rtac less_up1a 1)
+ (simp_tac (!simpset addsimps [po_def,less_up1a]) 1)
+ ]);
+
+bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
+
+qed_goal "least_up" thy "? x::'a u.!y.x<<y"
+(fn prems =>
+ [
+ (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1),
+ (rtac (minimal_up RS allI) 1)
]);
(* -------------------------------------------------------------------------*)
(* access to less_up in class po *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_up2b" Up2.thy "~ Iup(x) << UU_up"
+qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
(fn prems =>
[
- (stac inst_up_po 1),
- (rtac less_up1b 1)
+ (simp_tac (!simpset addsimps [po_def,less_up1b]) 1)
]);
-qed_goal "less_up2c" Up2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
+qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
(fn prems =>
[
- (stac inst_up_po 1),
- (rtac less_up1c 1)
+ (simp_tac (!simpset addsimps [po_def,less_up1c]) 1)
]);
(* ------------------------------------------------------------------------ *)
(* Iup and Ifup are monotone *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_Iup" Up2.thy [monofun] "monofun(Iup)"
+qed_goalw "monofun_Iup" thy [monofun] "monofun(Iup)"
(fn prems =>
[
(strip_tac 1),
(etac (less_up2c RS iffD2) 1)
]);
-qed_goalw "monofun_Ifup1" Up2.thy [monofun] "monofun(Ifup)"
+qed_goalw "monofun_Ifup1" thy [monofun] "monofun(Ifup)"
(fn prems =>
[
(strip_tac 1),
@@ -60,7 +77,7 @@
(etac monofun_cfun_fun 1)
]);
-qed_goalw "monofun_Ifup2" Up2.thy [monofun] "monofun(Ifup(f))"
+qed_goalw "monofun_Ifup2" thy [monofun] "monofun(Ifup(f))"
(fn prems =>
[
(strip_tac 1),
@@ -82,8 +99,7 @@
(* Some kind of surjectivity lemma *)
(* ------------------------------------------------------------------------ *)
-
-qed_goal "up_lemma1" Up2.thy "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z"
+qed_goal "up_lemma1" thy "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -94,7 +110,7 @@
(* ('a)u is a cpo *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_up1a" Up2.thy
+qed_goal "lub_up1a" thy
"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x.x) (Y(i))))))"
(fn prems =>
@@ -105,7 +121,7 @@
(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),
+ (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] subst 1),
(etac sym 1),
(rtac minimal_up 1),
(res_inst_tac [("t","Y(i)")] (up_lemma1 RS subst) 1),
@@ -117,7 +133,7 @@
(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 [("P","Y(i)<<Abs_Up (Inl ())")] notE 1),
(res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
(atac 1),
(rtac less_up2b 1),
@@ -131,9 +147,9 @@
(etac (monofun_Ifup2 RS ub2ub_monofun) 1)
]);
-qed_goal "lub_up1b" Up2.thy
+qed_goal "lub_up1b" thy
"[|is_chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
-\ range(Y) <<| UU_up"
+\ range(Y) <<| Abs_Up (Inl ())"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -142,7 +158,7 @@
(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),
+ (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] ssubst 1),
(atac 1),
(rtac refl_less 1),
(rtac notE 1),
@@ -166,7 +182,7 @@
lub (range ?Y1) = UU_up
*)
-qed_goal "cpo_up" Up2.thy
+qed_goal "cpo_up" thy
"is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
(fn prems =>
[