52 "!!u.[|u~v; regular(v); regular(u); w~u|]==> \ |
52 "!!u.[|u~v; regular(v); regular(u); w~u|]==> \ |
53 \ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"; |
53 \ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"; |
54 by (res_inst_tac [("u2","u"),("v2","v")](preservation RS ssubst) 1 |
54 by (res_inst_tac [("u2","u"),("v2","v")](preservation RS ssubst) 1 |
55 THEN assume_tac 1 THEN assume_tac 1); |
55 THEN assume_tac 1 THEN assume_tac 1); |
56 by (res_inst_tac [("u2","v"),("v2","u")](preservation RS ssubst) 1); |
56 by (res_inst_tac [("u2","v"),("v2","u")](preservation RS ssubst) 1); |
57 by (ALLGOALS(asm_full_simp_tac (res1_ss addsimps |
57 by (etac comp_sym 1); |
58 [prism RS sym,union_r,union_l,union_preserve_comp,union_preserve_regular, |
58 by (atac 1); |
59 read_instantiate [("u2","w"),("x1","v")] comp_trans,comp_sym_iff, |
59 by(rtac (prism RS sym RS ssubst) 1); |
60 union_sym]))); |
60 by (asm_full_simp_tac (res1_ss addsimps |
|
61 [prism RS sym,union_l,union_preserve_regular, |
|
62 comp_sym_iff, union_sym]) 4); |
|
63 by (asm_full_simp_tac (res1_ss addsimps [union_r, comp_sym_iff]) 1); |
|
64 by (asm_full_simp_tac (res1_ss addsimps |
|
65 [union_preserve_regular, comp_sym_iff]) 1); |
|
66 by (etac comp_trans 1); |
|
67 by (atac 1); |
61 val cube = result(); |
68 val cube = result(); |
62 |
69 |
63 |
70 |
64 (* ------------------------------------------------------------------------- *) |
71 (* ------------------------------------------------------------------------- *) |
65 (* paving theorem *) |
72 (* paving theorem *) |
70 \ EX uv.EX vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\ |
77 \ EX uv.EX vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\ |
71 \ regular(vu) & (w|>v)~uv & regular(uv) "; |
78 \ regular(vu) & (w|>v)~uv & regular(uv) "; |
72 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); |
73 by (REPEAT(step_tac ZF_cs 1)); |
80 by (REPEAT(step_tac ZF_cs 1)); |
74 by (rtac cube 1); |
81 by (rtac cube 1); |
75 by (ALLGOALS(asm_simp_tac (prism_ss addsimps [comp_sym_iff]))); |
82 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); |
|
85 by (atac 1); |
|
86 by (etac (residuals_preserve_comp RS spec RS mp RS mp RS mp) 1); |
|
87 by(atac 1); |
|
88 by(etac comp_sym 1); |
|
89 by(atac 1); |
|
90 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
|
91 by (asm_simp_tac prism_ss 1); |
|
92 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
76 val paving = result(); |
93 val paving = result(); |
77 |
94 |