# HG changeset patch
# User regensbu
# Date 795450909 -3600
# Node ID 932784dfa67138dff32af655f9088289213653f8
# Parent  358a19a91d52e7ef9f301f5d1c15501a3dac9e95
Removed bugs which occurred due to new generation mechanism for type variables

diff -r 358a19a91d52 -r 932784dfa671 src/HOLCF/Cfun3.ML
--- 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 
diff -r 358a19a91d52 -r 932784dfa671 src/HOLCF/Dlist.ML
--- 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)
 	]);
diff -r 358a19a91d52 -r 932784dfa671 src/HOLCF/ROOT.ML
--- 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";
diff -r 358a19a91d52 -r 932784dfa671 src/HOLCF/Sprod1.ML
--- 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)
 	]);
diff -r 358a19a91d52 -r 932784dfa671 src/HOLCF/Ssum1.ML
--- 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),
diff -r 358a19a91d52 -r 932784dfa671 src/HOLCF/Ssum2.ML
--- 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)
 	]);