--- a/src/HOLCF/Cfun3.ML Thu Mar 16 00:00:30 1995 +0100
+++ b/src/HOLCF/Cfun3.ML Fri Mar 17 15:35:09 1995 +0100
@@ -205,7 +205,7 @@
(* function application _[_] is strict in its first arguments *)
(* ------------------------------------------------------------------------ *)
-qed_goal "strict_fapp1" Cfun3.thy "UU[x] = UU"
+qed_goal "strict_fapp1" Cfun3.thy "(UU::'a->'b)[x] = (UU::'b)"
(fn prems =>
[
(rtac (inst_cfun_pcpo RS ssubst) 1),
@@ -221,7 +221,7 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "Istrictify1" Cfun3.thy [Istrictify_def]
- "Istrictify(f)(UU)=UU"
+ "Istrictify(f)(UU)= (UU)"
(fn prems =>
[
(rtac select_equality 1),
@@ -305,12 +305,12 @@
(rtac (refl RS allI) 1)
]);
-qed_goal "contlub_Istrictify2" Cfun3.thy "contlub(Istrictify(f))"
+qed_goal "contlub_Istrictify2" Cfun3.thy "contlub(Istrictify(f::'a -> 'b))"
(fn prems =>
[
(rtac contlubI 1),
(strip_tac 1),
- (res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
+ (res_inst_tac [("Q","lub(range(Y))=(UU::'a)")] classical2 1),
(res_inst_tac [("t","lub(range(Y))")] subst 1),
(rtac sym 1),
(atac 1),
@@ -318,7 +318,7 @@
(rtac sym 1),
(rtac chain_UU_I_inverse 1),
(strip_tac 1),
- (res_inst_tac [("t","Y(i)"),("s","UU")] subst 1),
+ (res_inst_tac [("t","Y(i)"),("s","UU::'a")] subst 1),
(rtac sym 1),
(rtac (chain_UU_I RS spec) 1),
(atac 1),
@@ -347,7 +347,7 @@
]);
-val contX_Istrictify1 = (contlub_Istrictify1 RS
+val contX_Istrictify1 = (contlub_Istrictify1 RS
(monofun_Istrictify1 RS monocontlub2contX));
val contX_Istrictify2 = (contlub_Istrictify2 RS
--- a/src/HOLCF/Dlist.ML Thu Mar 16 00:00:30 1995 +0100
+++ b/src/HOLCF/Dlist.ML Fri Mar 17 15:35:09 1995 +0100
@@ -197,8 +197,8 @@
val dlist_constrdef = [
-prover "is_dnil[UU] ~= UU" "dnil~=UU",
-prover "is_dcons[UU] ~= UU" "[|x~=UU;xl~=UU|] ==> dcons[x][xl]~=UU"
+prover "is_dnil[UU::'a dlist] ~= UU" "dnil~=(UU::'a dlist)",
+prover "is_dcons[UU::'a dlist] ~= UU" "[|x~=UU;xl~=UU|]==>dcons[x::'a][xl]~=UU"
];
@@ -220,7 +220,7 @@
(* Distinctness wrt. << and = *)
(* ------------------------------------------------------------------------*)
-val temp = prove_goal Dlist.thy "~dnil << dcons[x][xl]"
+val temp = prove_goal Dlist.thy "~dnil << dcons[x::'a][xl]"
(fn prems =>
[
(res_inst_tac [("P1","TT << FF")] classical3 1),
@@ -228,9 +228,9 @@
(dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (res_inst_tac [("Q","(x::'a)=UU")] classical2 1),
(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (res_inst_tac [("Q","(xl ::'a dlist)=UU")] classical2 1),
(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
]);
--- a/src/HOLCF/ROOT.ML Thu Mar 16 00:00:30 1995 +0100
+++ b/src/HOLCF/ROOT.ML Fri Mar 17 15:35:09 1995 +0100
@@ -60,6 +60,7 @@
use_thy "Dnat";
use_thy "Dnat2";
+
use_thy "Stream";
use_thy "Stream2";
use_thy "Dlist";
--- a/src/HOLCF/Sprod1.ML Thu Mar 16 00:00:30 1995 +0100
+++ b/src/HOLCF/Sprod1.ML Fri Mar 17 15:35:09 1995 +0100
@@ -146,8 +146,8 @@
]);
qed_goal "trans_less_sprod" Sprod1.thy
- "[|less_sprod(p1,p2);less_sprod(p2,p3)|] ==> less_sprod(p1,p3)"
-(fn prems =>
+ "[|less_sprod(p1::'a**'b,p2);less_sprod(p2,p3)|] ==> less_sprod(p1,p3)"
+ (fn prems =>
[
(cut_facts_tac prems 1),
(res_inst_tac [("p","p1")] IsprodE 1),
@@ -155,40 +155,34 @@
(hyp_subst_tac 1),
(res_inst_tac [("p","p3")] IsprodE 1),
(hyp_subst_tac 1),
- (res_inst_tac [("s","p2"),("t","Ispair(UU,UU)")] subst 1),
+ (res_inst_tac [("s","p2"),("t","Ispair(UU::'a,UU::'b)")] subst 1),
(etac less_sprod2b 1),
(atac 1),
(hyp_subst_tac 1),
- (res_inst_tac [("Q","p2=Ispair(UU,UU)")]
- (excluded_middle RS disjE) 1),
+ (res_inst_tac [("Q","p2=Ispair(UU::'a,UU::'b)")]
+ (excluded_middle RS disjE) 1),
(rtac (defined_Ispair RS less_sprod1b RS ssubst) 1),
- (atac 1),
- (atac 1),
+ (REPEAT (atac 1)),
(rtac conjI 1),
(res_inst_tac [("y","Isfst(p2)")] trans_less 1),
(rtac conjunct1 1),
(rtac (less_sprod1b RS subst) 1),
(rtac defined_Ispair 1),
- (atac 1),
- (atac 1),
- (atac 1),
+ (REPEAT (atac 1)),
(rtac conjunct1 1),
(rtac (less_sprod1b RS subst) 1),
- (atac 1),
- (atac 1),
+ (REPEAT (atac 1)),
(res_inst_tac [("y","Issnd(p2)")] trans_less 1),
(rtac conjunct2 1),
(rtac (less_sprod1b RS subst) 1),
(rtac defined_Ispair 1),
- (atac 1),
- (atac 1),
- (atac 1),
+ (REPEAT (atac 1)),
(rtac conjunct2 1),
(rtac (less_sprod1b RS subst) 1),
- (atac 1),
- (atac 1),
+ (REPEAT (atac 1)),
(hyp_subst_tac 1),
- (res_inst_tac [("s","Ispair(UU,UU)"),("t","Ispair(x,y)")] subst 1),
+ (res_inst_tac [("s","Ispair(UU::'a,UU::'b)"),("t","Ispair(x,y)")]
+ subst 1),
(etac (less_sprod2b RS sym) 1),
(atac 1)
]);
--- a/src/HOLCF/Ssum1.ML Thu Mar 16 00:00:30 1995 +0100
+++ b/src/HOLCF/Ssum1.ML Fri Mar 17 15:35:09 1995 +0100
@@ -41,7 +41,7 @@
in
val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinl(x); s2=Isinl(y)|] ==> less_ssum(s1,s2) = (x << y)"
+"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less_ssum(s1,s2) = (x << y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -70,7 +70,7 @@
(UU_left "y"),
(rtac iffI 1),
(etac UU_I 1),
- (res_inst_tac [("s","x"),("t","UU")] subst 1),
+ (res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
(atac 1),
(rtac refl_less 1),
(strip_tac 1),
@@ -82,7 +82,7 @@
val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinr(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x << y)"
+"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less_ssum(s1,s2) = (x << y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -117,14 +117,14 @@
(UU_right "y"),
(rtac iffI 1),
(etac UU_I 1),
- (res_inst_tac [("s","UU"),("t","x")] subst 1),
+ (res_inst_tac [("s","UU::'b"),("t","x")] subst 1),
(etac sym 1),
(rtac refl_less 1)
]);
val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinl(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x = UU)"
+"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less_ssum(s1,s2) = ((x::'a) = UU)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -135,7 +135,7 @@
(eq_left "x" "u"),
(UU_left "xa"),
(rtac iffI 1),
- (res_inst_tac [("s","x"),("t","UU")] subst 1),
+ (res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
(atac 1),
(rtac refl_less 1),
(etac UU_I 1),
--- a/src/HOLCF/Ssum2.ML Thu Mar 16 00:00:30 1995 +0100
+++ b/src/HOLCF/Ssum2.ML Fri Mar 17 15:35:09 1995 +0100
@@ -190,7 +190,8 @@
qed_goal "ssum_lemma3" Ssum2.thy
-"[|is_chain(Y);(? i x. Y(i)=Isinr(x) & ~x=UU)|] ==> (!i.? y.Y(i)=Isinr(y))"
+"[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
+\ (!i.? y.Y(i)=Isinr(y))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -207,22 +208,16 @@
(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
(hyp_subst_tac 2),
(etac exI 2),
- (res_inst_tac [("P","x=UU")] notE 1),
- (atac 1),
+ (eres_inst_tac [("P","x=UU")] notE 1),
(rtac (less_ssum3d RS iffD1) 1),
- (res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1),
- (atac 1),
- (res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1),
- (atac 1),
+ (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1),
+ (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1),
(etac (chain_mono RS mp) 1),
(atac 1),
- (res_inst_tac [("P","xa=UU")] notE 1),
- (atac 1),
+ (eres_inst_tac [("P","xa=UU")] notE 1),
(rtac (less_ssum3c RS iffD1) 1),
- (res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1),
- (atac 1),
- (res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1),
- (atac 1),
+ (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1),
+ (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1),
(etac (chain_mono RS mp) 1),
(atac 1)
]);