Removed bugs which occurred due to new generation mechanism for type variables
authorregensbu
Fri Mar 17 15:35:09 1995 +0100 (1995-03-17)
changeset 961932784dfa671
parent 960 358a19a91d52
child 962 136308504cd9
Removed bugs which occurred due to new generation mechanism for type variables
src/HOLCF/Cfun3.ML
src/HOLCF/Dlist.ML
src/HOLCF/ROOT.ML
src/HOLCF/Sprod1.ML
src/HOLCF/Ssum1.ML
src/HOLCF/Ssum2.ML
     1.1 --- a/src/HOLCF/Cfun3.ML	Thu Mar 16 00:00:30 1995 +0100
     1.2 +++ b/src/HOLCF/Cfun3.ML	Fri Mar 17 15:35:09 1995 +0100
     1.3 @@ -205,7 +205,7 @@
     1.4  (* function application _[_]  is strict in its first arguments              *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -qed_goal "strict_fapp1" Cfun3.thy "UU[x] = UU"
     1.8 +qed_goal "strict_fapp1" Cfun3.thy "(UU::'a->'b)[x] = (UU::'b)"
     1.9   (fn prems =>
    1.10  	[
    1.11  	(rtac (inst_cfun_pcpo RS ssubst) 1),
    1.12 @@ -221,7 +221,7 @@
    1.13  (* ------------------------------------------------------------------------ *)
    1.14  
    1.15  qed_goalw "Istrictify1" Cfun3.thy [Istrictify_def]
    1.16 -	"Istrictify(f)(UU)=UU"
    1.17 +	"Istrictify(f)(UU)= (UU)"
    1.18   (fn prems =>
    1.19  	[
    1.20  	(rtac select_equality 1),
    1.21 @@ -305,12 +305,12 @@
    1.22  	(rtac (refl RS allI) 1)
    1.23  	]);
    1.24  
    1.25 -qed_goal "contlub_Istrictify2" Cfun3.thy "contlub(Istrictify(f))"
    1.26 +qed_goal "contlub_Istrictify2" Cfun3.thy "contlub(Istrictify(f::'a -> 'b))"
    1.27   (fn prems =>
    1.28  	[
    1.29  	(rtac contlubI 1),
    1.30  	(strip_tac 1),
    1.31 -	(res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
    1.32 +	(res_inst_tac [("Q","lub(range(Y))=(UU::'a)")] classical2 1),
    1.33  	(res_inst_tac [("t","lub(range(Y))")] subst 1),
    1.34  	(rtac sym 1),
    1.35  	(atac 1),
    1.36 @@ -318,7 +318,7 @@
    1.37  	(rtac sym 1),
    1.38  	(rtac chain_UU_I_inverse 1),
    1.39  	(strip_tac 1),
    1.40 -	(res_inst_tac [("t","Y(i)"),("s","UU")] subst 1),
    1.41 +	(res_inst_tac [("t","Y(i)"),("s","UU::'a")] subst 1),
    1.42  	(rtac sym 1),
    1.43  	(rtac (chain_UU_I RS spec) 1),
    1.44  	(atac 1),
    1.45 @@ -347,7 +347,7 @@
    1.46  	]);
    1.47  
    1.48  
    1.49 -val contX_Istrictify1 =	(contlub_Istrictify1 RS 
    1.50 +val contX_Istrictify1 = (contlub_Istrictify1 RS 
    1.51  	(monofun_Istrictify1 RS monocontlub2contX)); 
    1.52  
    1.53  val contX_Istrictify2 = (contlub_Istrictify2 RS 
     2.1 --- a/src/HOLCF/Dlist.ML	Thu Mar 16 00:00:30 1995 +0100
     2.2 +++ b/src/HOLCF/Dlist.ML	Fri Mar 17 15:35:09 1995 +0100
     2.3 @@ -197,8 +197,8 @@
     2.4  
     2.5  
     2.6  val dlist_constrdef = [
     2.7 -prover "is_dnil[UU] ~= UU" "dnil~=UU",
     2.8 -prover "is_dcons[UU] ~= UU" "[|x~=UU;xl~=UU|] ==> dcons[x][xl]~=UU"
     2.9 +prover "is_dnil[UU::'a dlist] ~= UU" "dnil~=(UU::'a dlist)",
    2.10 +prover "is_dcons[UU::'a dlist] ~= UU" "[|x~=UU;xl~=UU|]==>dcons[x::'a][xl]~=UU"
    2.11   ];
    2.12  
    2.13  
    2.14 @@ -220,7 +220,7 @@
    2.15  (* Distinctness wrt. << and =                                              *)
    2.16  (* ------------------------------------------------------------------------*)
    2.17  
    2.18 -val temp = prove_goal Dlist.thy  "~dnil << dcons[x][xl]"
    2.19 +val temp = prove_goal Dlist.thy  "~dnil << dcons[x::'a][xl]"
    2.20   (fn prems =>
    2.21  	[
    2.22  	(res_inst_tac [("P1","TT << FF")] classical3 1),
    2.23 @@ -228,9 +228,9 @@
    2.24  	(dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
    2.25  	(etac box_less 1),
    2.26  	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    2.27 -	(res_inst_tac [("Q","x=UU")] classical2 1),
    2.28 +	(res_inst_tac [("Q","(x::'a)=UU")] classical2 1),
    2.29  	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    2.30 -	(res_inst_tac [("Q","xl=UU")] classical2 1),
    2.31 +	(res_inst_tac [("Q","(xl ::'a dlist)=UU")] classical2 1),
    2.32  	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
    2.33  	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
    2.34  	]);
     3.1 --- a/src/HOLCF/ROOT.ML	Thu Mar 16 00:00:30 1995 +0100
     3.2 +++ b/src/HOLCF/ROOT.ML	Fri Mar 17 15:35:09 1995 +0100
     3.3 @@ -60,6 +60,7 @@
     3.4  
     3.5  use_thy "Dnat";
     3.6  use_thy "Dnat2";
     3.7 +
     3.8  use_thy "Stream";
     3.9  use_thy "Stream2";
    3.10  use_thy "Dlist";
     4.1 --- a/src/HOLCF/Sprod1.ML	Thu Mar 16 00:00:30 1995 +0100
     4.2 +++ b/src/HOLCF/Sprod1.ML	Fri Mar 17 15:35:09 1995 +0100
     4.3 @@ -146,8 +146,8 @@
     4.4  	]);
     4.5  
     4.6  qed_goal "trans_less_sprod" Sprod1.thy 
     4.7 - "[|less_sprod(p1,p2);less_sprod(p2,p3)|] ==> less_sprod(p1,p3)"
     4.8 -(fn prems =>
     4.9 + "[|less_sprod(p1::'a**'b,p2);less_sprod(p2,p3)|] ==> less_sprod(p1,p3)"
    4.10 + (fn prems =>
    4.11  	[
    4.12  	(cut_facts_tac prems 1),
    4.13  	(res_inst_tac [("p","p1")] IsprodE 1),
    4.14 @@ -155,40 +155,34 @@
    4.15  	(hyp_subst_tac 1),
    4.16  	(res_inst_tac [("p","p3")] IsprodE 1),
    4.17  	(hyp_subst_tac 1),
    4.18 -	(res_inst_tac [("s","p2"),("t","Ispair(UU,UU)")] subst 1),
    4.19 +	(res_inst_tac [("s","p2"),("t","Ispair(UU::'a,UU::'b)")] subst 1),
    4.20  	(etac less_sprod2b 1),
    4.21  	(atac 1),
    4.22  	(hyp_subst_tac 1),
    4.23 -	(res_inst_tac [("Q","p2=Ispair(UU,UU)")]  
    4.24 -		(excluded_middle RS disjE) 1),
    4.25 +	(res_inst_tac [("Q","p2=Ispair(UU::'a,UU::'b)")]
    4.26 +		 (excluded_middle RS disjE) 1),
    4.27  	(rtac (defined_Ispair RS less_sprod1b RS ssubst) 1),
    4.28 -	(atac 1),
    4.29 -	(atac 1),
    4.30 +	(REPEAT (atac 1)),
    4.31  	(rtac conjI 1),
    4.32  	(res_inst_tac [("y","Isfst(p2)")] trans_less 1),
    4.33  	(rtac conjunct1 1),
    4.34  	(rtac (less_sprod1b RS subst) 1),
    4.35  	(rtac defined_Ispair 1),
    4.36 -	(atac 1),
    4.37 -	(atac 1),
    4.38 -	(atac 1),
    4.39 +	(REPEAT (atac 1)),
    4.40  	(rtac conjunct1 1),
    4.41  	(rtac (less_sprod1b RS subst) 1),
    4.42 -	(atac 1),
    4.43 -	(atac 1),
    4.44 +	(REPEAT (atac 1)),
    4.45  	(res_inst_tac [("y","Issnd(p2)")] trans_less 1),
    4.46  	(rtac conjunct2 1),
    4.47  	(rtac (less_sprod1b RS subst) 1),
    4.48  	(rtac defined_Ispair 1),
    4.49 -	(atac 1),
    4.50 -	(atac 1),
    4.51 -	(atac 1),
    4.52 +	(REPEAT (atac 1)),
    4.53  	(rtac conjunct2 1),
    4.54  	(rtac (less_sprod1b RS subst) 1),
    4.55 -	(atac 1),
    4.56 -	(atac 1),
    4.57 +	(REPEAT (atac 1)),
    4.58  	(hyp_subst_tac 1),
    4.59 -	(res_inst_tac [("s","Ispair(UU,UU)"),("t","Ispair(x,y)")] subst 1),
    4.60 +	(res_inst_tac [("s","Ispair(UU::'a,UU::'b)"),("t","Ispair(x,y)")] 
    4.61 +		subst 1),
    4.62  	(etac (less_sprod2b RS sym) 1),
    4.63  	(atac 1)
    4.64  	]);
     5.1 --- a/src/HOLCF/Ssum1.ML	Thu Mar 16 00:00:30 1995 +0100
     5.2 +++ b/src/HOLCF/Ssum1.ML	Fri Mar 17 15:35:09 1995 +0100
     5.3 @@ -41,7 +41,7 @@
     5.4  in
     5.5  
     5.6  val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def]
     5.7 -"[|s1=Isinl(x); s2=Isinl(y)|] ==> less_ssum(s1,s2) = (x << y)"
     5.8 +"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less_ssum(s1,s2) = (x << y)"
     5.9   (fn prems =>
    5.10  	[
    5.11  	(cut_facts_tac prems 1),
    5.12 @@ -70,7 +70,7 @@
    5.13  	(UU_left "y"),
    5.14  	(rtac iffI 1),
    5.15  	(etac UU_I 1),
    5.16 -	(res_inst_tac [("s","x"),("t","UU")] subst 1),
    5.17 +	(res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
    5.18  	(atac 1),
    5.19  	(rtac refl_less 1),
    5.20  	(strip_tac 1),
    5.21 @@ -82,7 +82,7 @@
    5.22  
    5.23  
    5.24  val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def]
    5.25 -"[|s1=Isinr(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x << y)"
    5.26 +"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less_ssum(s1,s2) = (x << y)"
    5.27   (fn prems =>
    5.28  	[
    5.29  	(cut_facts_tac prems 1),
    5.30 @@ -117,14 +117,14 @@
    5.31  	(UU_right "y"),
    5.32  	(rtac iffI 1),
    5.33  	(etac UU_I 1),
    5.34 -	(res_inst_tac [("s","UU"),("t","x")] subst 1),
    5.35 +	(res_inst_tac [("s","UU::'b"),("t","x")] subst 1),
    5.36  	(etac sym 1),
    5.37  	(rtac refl_less 1)
    5.38  	]);
    5.39  
    5.40  
    5.41  val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def]
    5.42 -"[|s1=Isinl(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x = UU)"
    5.43 +"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less_ssum(s1,s2) = ((x::'a) = UU)"
    5.44   (fn prems =>
    5.45  	[
    5.46  	(cut_facts_tac prems 1),
    5.47 @@ -135,7 +135,7 @@
    5.48  	(eq_left  "x" "u"),
    5.49  	(UU_left "xa"),
    5.50  	(rtac iffI 1),
    5.51 -	(res_inst_tac [("s","x"),("t","UU")] subst 1),
    5.52 +	(res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
    5.53  	(atac 1),
    5.54  	(rtac refl_less 1),
    5.55  	(etac UU_I 1),
     6.1 --- a/src/HOLCF/Ssum2.ML	Thu Mar 16 00:00:30 1995 +0100
     6.2 +++ b/src/HOLCF/Ssum2.ML	Fri Mar 17 15:35:09 1995 +0100
     6.3 @@ -190,7 +190,8 @@
     6.4  
     6.5  
     6.6  qed_goal "ssum_lemma3" Ssum2.thy 
     6.7 -"[|is_chain(Y);(? i x. Y(i)=Isinr(x) & ~x=UU)|] ==> (!i.? y.Y(i)=Isinr(y))"
     6.8 +"[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
     6.9 +\ (!i.? y.Y(i)=Isinr(y))"
    6.10   (fn prems =>
    6.11  	[
    6.12  	(cut_facts_tac prems 1),
    6.13 @@ -207,22 +208,16 @@
    6.14  	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
    6.15  	(hyp_subst_tac 2),
    6.16  	(etac exI 2),
    6.17 -	(res_inst_tac [("P","x=UU")] notE 1),
    6.18 -	(atac 1),
    6.19 +	(eres_inst_tac [("P","x=UU")] notE 1),
    6.20  	(rtac (less_ssum3d RS iffD1) 1),
    6.21 -	(res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1),
    6.22 -	(atac 1),
    6.23 -	(res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1),
    6.24 -	(atac 1),
    6.25 +	(eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1),
    6.26 +	(eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1),
    6.27  	(etac (chain_mono RS mp) 1),
    6.28  	(atac 1),
    6.29 -	(res_inst_tac [("P","xa=UU")] notE 1),
    6.30 -	(atac 1),
    6.31 +	(eres_inst_tac [("P","xa=UU")] notE 1),
    6.32  	(rtac (less_ssum3c RS iffD1) 1),
    6.33 -	(res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1),
    6.34 -	(atac 1),
    6.35 -	(res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1),
    6.36 -	(atac 1),
    6.37 +	(eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1),
    6.38 +	(eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1),
    6.39  	(etac (chain_mono RS mp) 1),
    6.40  	(atac 1)
    6.41  	]);