src/ZF/Resid/Cube.ML

--- a/src/ZF/Resid/Cube.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Cube.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -16,32 +16,29 @@
 (*         =============                                                     *)
 (* ------------------------------------------------------------------------- *)
 
-(* Having more ssumptions than needed -- removed below  *)
+(* Having more assumptions than needed -- removed below  *)
 goal Cube.thy 
     "!!u.v<==u ==> \
 \   regular(u)-->(ALL w.w~v-->w~u-->  \
 \             w |> u = (w|>v) |> (u|>v))";
 by (etac Ssub.induct 1);
-by (asm_simp_tac prism_ss 1);
-by (asm_simp_tac prism_ss 1);
-by (asm_simp_tac prism_ss 1);
+by (ALLGOALS (asm_simp_tac prism_ss));
 by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1 
     THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1)));
 by (asm_full_simp_tac prism_ss 1);
-by (asm_simp_tac prism_ss 1);
 by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1 
     THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1)));
 by (asm_full_simp_tac prism_ss 1);
-val prism_l = result();
+qed_spec_mp "prism_l";
 
 goal Cube.thy 
     "!!u.[|v <== u; regular(u); w~v|]==> \
 \       w |> u = (w|>v) |> (u|>v)";
-by (resolve_tac [prism_l RS mp RS spec RS mp RS mp ] 1);
+by (resolve_tac [prism_l] 1);
 by (rtac comp_trans 4);
 by (assume_tac 4);
 by (ALLGOALS(asm_simp_tac prism_ss));
-val prism = result();
+qed "prism";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -51,11 +48,10 @@
 goal Cube.thy 
     "!!u.[|u~v; regular(v); regular(u); w~u|]==>  \
 \          (w|>u) |> (v|>u) = (w|>v) |> (u|>v)";
-by (res_inst_tac [("u2","u"),("v2","v")](preservation RS ssubst) 1 
+by (rtac (preservation RS ssubst) 1 
     THEN assume_tac 1 THEN assume_tac 1);
-by (res_inst_tac [("u2","v"),("v2","u")](preservation RS ssubst) 1);
-by (etac comp_sym 1);
-by (atac 1);
+by (rtac (preservation RS ssubst) 1 
+    THEN etac comp_sym 1 THEN assume_tac 1);
 by (stac (prism RS sym) 1);
 by (asm_full_simp_tac (!simpset addsimps 
 		       [prism RS sym,union_l,union_preserve_regular,
@@ -65,7 +61,7 @@
 		       [union_preserve_regular, comp_sym_iff]) 1);
 by (etac comp_trans 1);
 by (atac 1);
-val cube = result();
+qed "cube";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -76,19 +72,11 @@
     "!!u.[|w~u; w~v; regular(u); regular(v)|]==> \
 \          EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
 \            regular(vu) & (w|>v)~uv & regular(uv) ";
-by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1);
-by (step_tac (!claset addSIs [exI]) 1);
+by (subgoal_tac "u~v" 1);
+by (safe_tac (!claset addSIs [exI]));
 by (rtac cube 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-by (atac 1);
-by (etac (residuals_preserve_comp RS spec RS mp RS mp RS mp) 1);
- by(atac 1);
- by(etac comp_sym 1);
- by(atac 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-by (asm_simp_tac prism_ss 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-val paving = result();
+by (ALLGOALS (asm_simp_tac (prism_ss addsimps [comp_sym_iff])));
+by (ALLGOALS (blast_tac (!claset addIs [residuals_preserve_comp, 
+					comp_trans, comp_sym])));
+qed "paving";