--- a/src/HOLCF/Up1.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Up1.ML Wed Jun 28 10:54:21 2000 +0200
@@ -4,13 +4,9 @@
Copyright 1993 Technische Universitaet Muenchen
*)
-open Up1;
-
-qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y"
- (fn prems =>
- [
- (simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1)
- ]);
+Goal "Rep_Up (Abs_Up y) = y";
+by (simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1);
+qed "Abs_Up_inverse2";
qed_goalw "Exh_Up" thy [Iup_def ]
"z = Abs_Up(Inl ()) | (? x. z = Iup x)"
@@ -28,19 +24,15 @@
(atac 1)
]);
-qed_goal "inj_Abs_Up" thy "inj(Abs_Up)"
- (fn prems =>
- [
- (rtac inj_inverseI 1),
- (rtac Abs_Up_inverse2 1)
- ]);
+Goal "inj(Abs_Up)";
+by (rtac inj_inverseI 1);
+by (rtac Abs_Up_inverse2 1);
+qed "inj_Abs_Up";
-qed_goal "inj_Rep_Up" thy "inj(Rep_Up)"
- (fn prems =>
- [
- (rtac inj_inverseI 1),
- (rtac Rep_Up_inverse 1)
- ]);
+Goal "inj(Rep_Up)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_Up_inverse 1);
+qed "inj_Rep_Up";
qed_goalw "inject_Iup" thy [Iup_def] "Iup x=Iup y ==> x=y"
(fn prems =>
@@ -51,6 +43,8 @@
(atac 1)
]);
+AddSDs [inject_Iup];
+
qed_goalw "defined_Iup" thy [Iup_def] "Iup x~=Abs_Up(Inl ())"
(fn prems =>
[
@@ -62,15 +56,12 @@
]);
-qed_goal "upE" thy
- "[| p=Abs_Up(Inl ()) ==> 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)
- ]);
+val prems = Goal "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q";
+by (rtac (Exh_Up RS disjE) 1);
+by (eresolve_tac prems 1);
+by (etac exE 1);
+by (eresolve_tac prems 1);
+qed "upE";
qed_goalw "Ifup1" thy [Ifup_def]
"Ifup(f)(Abs_Up(Inl ()))=UU"
@@ -93,6 +84,8 @@
val Up0_ss = (simpset_of Cfun3.thy) delsimps [range_composition]
addsimps [Ifup1,Ifup2];
+Addsimps [Ifup1,Ifup2];
+
qed_goalw "less_up1a" thy [less_up_def]
"Abs_Up(Inl ())<< z"
(fn prems =>
@@ -117,7 +110,7 @@
]);
qed_goalw "less_up1c" thy [Iup_def,less_up_def]
- " (Iup x) << (Iup y)=(x<<y)"
+ "(Iup x) << (Iup y)=(x<<y)"
(fn prems =>
[
(stac Abs_Up_inverse2 1),
@@ -127,67 +120,43 @@
(rtac refl 1)
]);
+AddIffs [less_up1a, less_up1b, less_up1c];
-qed_goal "refl_less_up" thy "(p::'a u) << 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)
- ]);
+Goal "(p::'a u) << p";
+by (res_inst_tac [("p","p")] upE 1);
+by Auto_tac;
+qed "refl_less_up";
-qed_goal "antisym_less_up" thy
- "!!p1.[|(p1::'a u) << p2;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","(Iup x) << (Abs_Up(Inl ()))")] 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","(Iup x) << (Abs_Up(Inl ()))")] 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)
- ]);
+Goal "[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2";
+by (res_inst_tac [("p","p1")] upE 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p2")] upE 1);
+by (etac sym 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1);
+by (rtac less_up1b 1);
+by (atac 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p2")] upE 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1);
+by (rtac less_up1b 1);
+by (atac 1);
+by (blast_tac (claset() addIs [arg_cong, antisym_less, less_up1c RS iffD1]) 1);
+qed "antisym_less_up";
-qed_goal "trans_less_up" thy
- "[|(p1::'a u) << p2;p2 << p3|] ==> 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)
- ]);
+Goal "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3";
+by (res_inst_tac [("p","p1")] upE 1);
+by (hyp_subst_tac 1);
+by (rtac less_up1a 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("p","p2")] upE 1);
+by (hyp_subst_tac 1);
+by (rtac notE 1);
+by (rtac less_up1b 1);
+by (atac 1);
+by (res_inst_tac [("p","p3")] upE 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [trans_less]) 1);
+qed "trans_less_up";