src/ZF/Resid/Cube.ML

 (*         Prism theorem                                                     *)
 (*         =============                                                     *)
 (* ------------------------------------------------------------------------- *)
 
 (* Having more assumptions than needed -- removed below  *)
-goal Cube.thy 
+Goal 
     "!!u. v<==u ==> \
 \   regular(u)-->(ALL w. w~v-->w~u-->  \
 \             w |> u = (w|>v) |> (u|>v))";
 by (etac Ssub.induct 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);
 qed_spec_mp "prism_l";
 
-goal Cube.thy 
+Goal 
     "!!u.[|v <== u; regular(u); w~v|]==> \
 \       w |> u = (w|>v) |> (u|>v)";
 by (rtac prism_l 1);
 by (rtac comp_trans 4);
 by (assume_tac 4);

 
 (* ------------------------------------------------------------------------- *)
 (*    Levy's Cube Lemma                                                      *)
 (* ------------------------------------------------------------------------- *)
 
-goal Cube.thy 
+Goal 
     "!!u.[|u~v; regular(v); regular(u); w~u|]==>  \
 \          (w|>u) |> (v|>u) = (w|>v) |> (u|>v)";
 by (stac preservation 1 
     THEN assume_tac 1 THEN assume_tac 1);
 by (stac preservation 1 

 
 (* ------------------------------------------------------------------------- *)
 (*           paving theorem                                                  *)
 (* ------------------------------------------------------------------------- *)
 
-goal Cube.thy 
+Goal 
     "!!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 (subgoal_tac "u~v" 1);
 by (safe_tac (claset() addSIs [exI]));