author | oheimb |
Tue, 23 Apr 1996 17:11:44 +0200 | |
changeset 1677 | 99044cda4ef3 |
parent 1461 | 6bcb44e4d6e5 |
child 1732 | 38776e927da8 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: Cube.ML |
1048 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Ole Rasmussen |
1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
8 |
open Cube; |
|
9 |
||
10 |
val prism_ss = (res1L_ss addsimps |
|
1461 | 11 |
[commutation,residuals_preserve_comp,sub_preserve_reg, |
12 |
residuals_preserve_reg,sub_comp,sub_comp RS comp_sym]); |
|
1048 | 13 |
|
14 |
(* ------------------------------------------------------------------------- *) |
|
15 |
(* Prism theorem *) |
|
16 |
(* ============= *) |
|
17 |
(* ------------------------------------------------------------------------- *) |
|
18 |
||
19 |
(* Having more ssumptions than needed -- removed below *) |
|
20 |
goal Cube.thy |
|
21 |
"!!u.v<==u ==> \ |
|
22 |
\ regular(u)-->(ALL w.w~v-->w~u--> \ |
|
23 |
\ w |> u = (w|>v) |> (u|>v))"; |
|
1461 | 24 |
by (etac sub_induct 1); |
1048 | 25 |
by (asm_simp_tac (prism_ss) 1); |
26 |
by (asm_simp_tac (prism_ss ) 1); |
|
27 |
by (asm_simp_tac (prism_ss ) 1); |
|
28 |
by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1 |
|
29 |
THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1))); |
|
30 |
by (asm_full_simp_tac (prism_ss ) 1); |
|
31 |
by (asm_simp_tac (prism_ss ) 1); |
|
32 |
by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1 |
|
33 |
THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1))); |
|
34 |
by (asm_full_simp_tac (prism_ss ) 1); |
|
35 |
val prism_l = result(); |
|
36 |
||
37 |
goal Cube.thy |
|
38 |
"!!u.[|v <== u; regular(u); w~v|]==> \ |
|
39 |
\ w |> u = (w|>v) |> (u|>v)"; |
|
40 |
by (resolve_tac [prism_l RS mp RS spec RS mp RS mp ] 1); |
|
1461 | 41 |
by (rtac comp_trans 4); |
1048 | 42 |
by (assume_tac 4); |
43 |
by (ALLGOALS(asm_simp_tac (prism_ss))); |
|
44 |
val prism = result(); |
|
45 |
||
46 |
||
47 |
(* ------------------------------------------------------------------------- *) |
|
48 |
(* Levy's Cube Lemma *) |
|
49 |
(* ------------------------------------------------------------------------- *) |
|
50 |
||
51 |
goal Cube.thy |
|
52 |
"!!u.[|u~v; regular(v); regular(u); w~u|]==> \ |
|
53 |
\ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"; |
|
54 |
by (res_inst_tac [("u2","u"),("v2","v")](preservation RS ssubst) 1 |
|
55 |
THEN assume_tac 1 THEN assume_tac 1); |
|
56 |
by (res_inst_tac [("u2","v"),("v2","u")](preservation RS ssubst) 1); |
|
1677
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
57 |
by (etac comp_sym 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
58 |
by (atac 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
59 |
by(rtac (prism RS sym RS ssubst) 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
60 |
by (asm_full_simp_tac (res1_ss addsimps |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
61 |
[prism RS sym,union_l,union_preserve_regular, |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
62 |
comp_sym_iff, union_sym]) 4); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
63 |
by (asm_full_simp_tac (res1_ss addsimps [union_r, comp_sym_iff]) 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
64 |
by (asm_full_simp_tac (res1_ss addsimps |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
65 |
[union_preserve_regular, comp_sym_iff]) 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
66 |
by (etac comp_trans 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
67 |
by (atac 1); |
1048 | 68 |
val cube = result(); |
69 |
||
70 |
||
71 |
(* ------------------------------------------------------------------------- *) |
|
72 |
(* paving theorem *) |
|
73 |
(* ------------------------------------------------------------------------- *) |
|
74 |
||
75 |
goal Cube.thy |
|
76 |
"!!u.[|w~u; w~v; regular(u); regular(v)|]==> \ |
|
77 |
\ EX uv.EX vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\ |
|
78 |
\ regular(vu) & (w|>v)~uv & regular(uv) "; |
|
79 |
by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1); |
|
80 |
by (REPEAT(step_tac ZF_cs 1)); |
|
1461 | 81 |
by (rtac cube 1); |
1677
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
82 |
by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
83 |
by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
84 |
by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
85 |
by (atac 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
86 |
by (etac (residuals_preserve_comp RS spec RS mp RS mp RS mp) 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
87 |
by(atac 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
88 |
by(etac comp_sym 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
89 |
by(atac 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
90 |
by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
91 |
by (asm_simp_tac prism_ss 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
92 |
by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1); |
1048 | 93 |
val paving = result(); |
94 |