1461
|
1 |
(* Title: ZF/IMP/Equiv.ML
|
482
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM
|
482
|
4 |
Copyright 1994 TUM
|
|
5 |
*)
|
|
6 |
|
4298
|
7 |
val prems = goal Equiv.thy
|
|
8 |
"!!a. [| a: aexp; sigma: loc -> nat |] ==> \
|
|
9 |
\ <a,sigma> -a-> n <-> A(a,sigma) = n";
|
511
|
10 |
by (res_inst_tac [("x","n")] spec 1); (* quantify n *)
|
4298
|
11 |
by (etac aexp.induct 1);
|
|
12 |
by (ALLGOALS (fast_tac (claset() addSIs evala.intrs
|
|
13 |
addSEs aexp_elim_cases
|
|
14 |
addss (simpset()))));
|
760
|
15 |
qed "aexp_iff";
|
482
|
16 |
|
|
17 |
|
4298
|
18 |
val aexp1 = aexp_iff RS iffD1;
|
482
|
19 |
val aexp2 = aexp_iff RS iffD2;
|
|
20 |
|
|
21 |
|
511
|
22 |
val bexp_elim_cases =
|
482
|
23 |
[
|
511
|
24 |
evalb.mk_cases bexp.con_defs "<true,sigma> -b-> x",
|
|
25 |
evalb.mk_cases bexp.con_defs "<false,sigma> -b-> x",
|
|
26 |
evalb.mk_cases bexp.con_defs "<ROp(f,a0,a1),sigma> -b-> x",
|
|
27 |
evalb.mk_cases bexp.con_defs "<noti(b),sigma> -b-> x",
|
|
28 |
evalb.mk_cases bexp.con_defs "<b0 andi b1,sigma> -b-> x",
|
|
29 |
evalb.mk_cases bexp.con_defs "<b0 ori b1,sigma> -b-> x"
|
482
|
30 |
];
|
|
31 |
|
|
32 |
|
4298
|
33 |
val prems = goal Equiv.thy
|
|
34 |
"!!b. [| b: bexp; sigma: loc -> nat |] ==> \
|
|
35 |
\ <b,sigma> -b-> w <-> B(b,sigma) = w";
|
|
36 |
by (res_inst_tac [("x","w")] spec 1);
|
|
37 |
by (etac bexp.induct 1);
|
|
38 |
by (ALLGOALS (fast_tac (claset() addSIs evalb.intrs
|
|
39 |
addSEs bexp_elim_cases
|
|
40 |
addss (simpset() addsimps [aexp_iff]))));
|
760
|
41 |
qed "bexp_iff";
|
482
|
42 |
|
4298
|
43 |
val bexp1 = bexp_iff RS iffD1;
|
518
|
44 |
val bexp2 = bexp_iff RS iffD2;
|
482
|
45 |
|
4298
|
46 |
|
518
|
47 |
goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
|
1742
|
48 |
by (etac evalc.induct 1);
|
4298
|
49 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bexp1])));
|
482
|
50 |
(* skip *)
|
2469
|
51 |
by (Fast_tac 1);
|
482
|
52 |
(* assign *)
|
4298
|
53 |
by (asm_full_simp_tac (simpset() addsimps
|
|
54 |
[aexp1, assign_type] @ op_type_intrs) 1);
|
482
|
55 |
(* comp *)
|
2469
|
56 |
by (Fast_tac 1);
|
482
|
57 |
(* while *)
|
4298
|
58 |
by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1);
|
|
59 |
by (asm_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
|
|
60 |
by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
|
|
61 |
(* recursive case of while *)
|
|
62 |
by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1);
|
|
63 |
by (asm_full_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
|
|
64 |
by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
|
500
|
65 |
val com1 = result();
|
482
|
66 |
|
|
67 |
|
2469
|
68 |
AddSIs [aexp2,bexp2,B_type,A_type];
|
4298
|
69 |
AddIs evalc.intrs;
|
|
70 |
AddEs [C_type,C_type_fst];
|
|
71 |
|
482
|
72 |
|
4298
|
73 |
goal Equiv.thy "!!c. c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
|
|
74 |
by (etac com.induct 1);
|
|
75 |
(* skip *)
|
|
76 |
by (fast_tac (claset() addss (simpset())) 1);
|
|
77 |
(* assign *)
|
|
78 |
by (fast_tac (claset() addss (simpset())) 1);
|
|
79 |
(* comp *)
|
|
80 |
by (best_tac (claset() addss (simpset())) 1);
|
|
81 |
(* while *)
|
4152
|
82 |
by Safe_tac;
|
2469
|
83 |
by (ALLGOALS Asm_full_simp_tac);
|
518
|
84 |
by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]);
|
808
|
85 |
by (rewtac Gamma_def);
|
4152
|
86 |
by Safe_tac;
|
518
|
87 |
by (EVERY1 [dtac bspec, atac]);
|
2469
|
88 |
by (ALLGOALS Asm_full_simp_tac);
|
511
|
89 |
(* while, if *)
|
4298
|
90 |
by (ALLGOALS Blast_tac);
|
482
|
91 |
val com2 = result();
|
|
92 |
|
|
93 |
|
511
|
94 |
(**** Proof of Equivalence ****)
|
482
|
95 |
|
511
|
96 |
goal Equiv.thy
|
|
97 |
"ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
|
4091
|
98 |
by (fast_tac (claset() addIs [C_subset RS subsetD]
|
4298
|
99 |
addEs [com2 RS bspec]
|
|
100 |
addDs [com1]
|
|
101 |
addss (simpset())) 1);
|
511
|
102 |
val com_equivalence = result();
|