author | wenzelm |
Wed, 15 Oct 1997 15:12:59 +0200 | |
changeset 3872 | a5839ecee7b8 |
parent 3840 | e0baea4d485a |
child 4091 | 771b1f6422a8 |
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 |
||
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
19 |
(* Having more assumptions than needed -- removed below *) |
1048 | 20 |
goal Cube.thy |
3840 | 21 |
"!!u. v<==u ==> \ |
22 |
\ regular(u)-->(ALL w. w~v-->w~u--> \ |
|
1048 | 23 |
\ w |> u = (w|>v) |> (u|>v))"; |
1732 | 24 |
by (etac Ssub.induct 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
25 |
by (ALLGOALS (asm_simp_tac prism_ss)); |
1048 | 26 |
by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1 |
27 |
THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1))); |
|
2469 | 28 |
by (asm_full_simp_tac prism_ss 1); |
1048 | 29 |
by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1 |
30 |
THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1))); |
|
2469 | 31 |
by (asm_full_simp_tac prism_ss 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
32 |
qed_spec_mp "prism_l"; |
1048 | 33 |
|
34 |
goal Cube.thy |
|
35 |
"!!u.[|v <== u; regular(u); w~v|]==> \ |
|
36 |
\ w |> u = (w|>v) |> (u|>v)"; |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
37 |
by (resolve_tac [prism_l] 1); |
1461 | 38 |
by (rtac comp_trans 4); |
1048 | 39 |
by (assume_tac 4); |
2469 | 40 |
by (ALLGOALS(asm_simp_tac prism_ss)); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
41 |
qed "prism"; |
1048 | 42 |
|
43 |
||
44 |
(* ------------------------------------------------------------------------- *) |
|
45 |
(* Levy's Cube Lemma *) |
|
46 |
(* ------------------------------------------------------------------------- *) |
|
47 |
||
48 |
goal Cube.thy |
|
49 |
"!!u.[|u~v; regular(v); regular(u); w~u|]==> \ |
|
50 |
\ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"; |
|
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
51 |
by (rtac (preservation RS ssubst) 1 |
1048 | 52 |
THEN assume_tac 1 THEN assume_tac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
53 |
by (rtac (preservation RS ssubst) 1 |
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
54 |
THEN etac comp_sym 1 THEN assume_tac 1); |
2034 | 55 |
by (stac (prism RS sym) 1); |
2469 | 56 |
by (asm_full_simp_tac (!simpset addsimps |
57 |
[prism RS sym,union_l,union_preserve_regular, |
|
58 |
comp_sym_iff, union_sym]) 4); |
|
59 |
by (asm_full_simp_tac (!simpset addsimps [union_r, comp_sym_iff]) 1); |
|
60 |
by (asm_full_simp_tac (!simpset addsimps |
|
61 |
[union_preserve_regular, comp_sym_iff]) 1); |
|
1677
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
62 |
by (etac comp_trans 1); |
99044cda4ef3
repaired critical proofs depending on the order inside non-confluent SimpSets,
oheimb
parents:
1461
diff
changeset
|
63 |
by (atac 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
64 |
qed "cube"; |
1048 | 65 |
|
66 |
||
67 |
(* ------------------------------------------------------------------------- *) |
|
68 |
(* paving theorem *) |
|
69 |
(* ------------------------------------------------------------------------- *) |
|
70 |
||
71 |
goal Cube.thy |
|
72 |
"!!u.[|w~u; w~v; regular(u); regular(v)|]==> \ |
|
2493 | 73 |
\ EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\ |
1048 | 74 |
\ regular(vu) & (w|>v)~uv & regular(uv) "; |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
75 |
by (subgoal_tac "u~v" 1); |
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
76 |
by (safe_tac (!claset addSIs [exI])); |
1461 | 77 |
by (rtac cube 1); |
3734
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
78 |
by (ALLGOALS (asm_simp_tac (prism_ss addsimps [comp_sym_iff]))); |
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
79 |
by (ALLGOALS (blast_tac (!claset addIs [residuals_preserve_comp, |
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
80 |
comp_trans, comp_sym]))); |
33f355f56f82
Much tidying including "qed" instead of result(), and even qed_spec_mp,
paulson
parents:
2493
diff
changeset
|
81 |
qed "paving"; |
1048 | 82 |