--- a/src/HOLCF/Sprod3.ML Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Sprod3.ML Tue Oct 10 11:55:45 1995 +0100
@@ -28,7 +28,7 @@
(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
(atac 1),
(rtac allI 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
(rtac sym 1),
(rtac lub_chain_maxelem 1),
(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
@@ -41,11 +41,13 @@
(etac Issnd2 1),
(rtac allI 1),
(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
+ (rtac refl_less 1),
(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
(etac sym 1),
- (Asm_simp_tac 1)
- ]);
+ (asm_simp_tac Sprod0_ss 1),
+ (rtac minimal 1)
+ ]);
qed_goal "sprod3_lemma2" Sprod3.thy
"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
@@ -63,7 +65,7 @@
(rtac disjI1 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
(etac (chain_UU_I RS spec) 1),
(atac 1)
]);
@@ -85,7 +87,7 @@
(rtac disjI1 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
- (Simp_tac 1)
+ (simp_tac Sprod0_ss 1)
]);
@@ -136,17 +138,19 @@
(etac Isfst2 1),
(rtac allI 1),
(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
- (Asm_simp_tac 1),
- (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
+ (asm_simp_tac Sprod0_ss 1),
+ (rtac refl_less 1),
+ (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
(etac sym 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
+ (rtac minimal 1),
(rtac lub_equal 1),
(atac 1),
(rtac (monofun_Issnd RS ch2ch_monofun) 1),
(rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
(atac 1),
(rtac allI 1),
- (Asm_simp_tac 1)
+ (asm_simp_tac Sprod0_ss 1)
]);
qed_goal "sprod3_lemma5" Sprod3.thy
@@ -165,7 +169,7 @@
(rtac disjI2 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
(etac (chain_UU_I RS spec) 1),
(atac 1)
]);
@@ -186,7 +190,7 @@
(rtac disjI1 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
- (Simp_tac 1)
+ (simp_tac Sprod0_ss 1)
]);
qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))"
@@ -237,12 +241,12 @@
(atac 1),
(res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]
(excluded_middle RS disjE) 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
(res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
ssubst 1),
(atac 1),
(rtac trans 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
(rtac sym 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
@@ -266,11 +270,11 @@
(atac 1),
(res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
(excluded_middle RS disjE) 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
(res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")]
ssubst 1),
(atac 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
(rtac sym 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
@@ -680,5 +684,5 @@
ssplit1,ssplit2];
Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
- strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
+ strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
ssplit1,ssplit2];