equal
deleted
inserted
replaced
72 (* paving theorem *) |
72 (* paving theorem *) |
73 (* ------------------------------------------------------------------------- *) |
73 (* ------------------------------------------------------------------------- *) |
74 |
74 |
75 goal Cube.thy |
75 goal Cube.thy |
76 "!!u.[|w~u; w~v; regular(u); regular(v)|]==> \ |
76 "!!u.[|w~u; w~v; regular(u); regular(v)|]==> \ |
77 \ EX uv.EX vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\ |
77 \ EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\ |
78 \ regular(vu) & (w|>v)~uv & regular(uv) "; |
78 \ regular(vu) & (w|>v)~uv & regular(uv) "; |
79 by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1); |
79 by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1); |
80 by (REPEAT(Step_tac 1)); |
80 by (step_tac (!claset addSIs [exI]) 1); |
81 by (rtac cube 1); |
81 by (rtac cube 1); |
82 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
82 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
83 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
83 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
84 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
84 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
85 by (atac 1); |
85 by (atac 1); |