8 |
8 |
9 open Transition; |
9 open Transition; |
10 |
10 |
11 section "Winskel's Proof"; |
11 section "Winskel's Proof"; |
12 |
12 |
13 val relpow_cs = rel_cs addSEs [rel_pow_0_E]; |
13 AddSEs [rel_pow_0_E]; |
14 |
14 |
15 val evalc1_elim_cases = map (evalc1.mk_cases com.simps) |
15 val evalc1_SEs = map (evalc1.mk_cases com.simps) |
16 ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t", "(c1;c2, s) -1-> t", |
16 ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t","(c1;c2, s) -1-> t", |
17 "(IF b THEN c1 ELSE c2, s) -1-> t", "(WHILE b DO c,s) -1-> t"]; |
17 "(IF b THEN c1 ELSE c2, s) -1-> t"]; |
18 |
18 val evalc1_Es = map (evalc1.mk_cases com.simps) |
19 val evalc1_cs = relpow_cs addIs (evalc.intrs@evalc1.intrs); |
19 ["(WHILE b DO c,s) -1-> t"]; |
20 |
20 |
21 goal Transition.thy "!!c. (c,s) -0-> (SKIP,u) ==> c = SKIP & s = u"; |
21 AddSEs evalc1_SEs; |
22 by(fast_tac evalc1_cs 1); |
22 |
23 val hlemma1 = result(); |
23 AddIs evalc1.intrs; |
24 |
24 |
25 goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0"; |
25 goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0"; |
26 be rel_pow_E2 1; |
26 be rel_pow_E2 1; |
27 by (Asm_full_simp_tac 1); |
27 by (Asm_full_simp_tac 1); |
28 by (eresolve_tac evalc1_elim_cases 1); |
28 by(Fast_tac 1); |
29 val hlemma2 = result(); |
29 val hlemma = result(); |
30 |
30 |
31 |
31 |
32 goal Transition.thy |
32 goal Transition.thy |
33 "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \ |
33 "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \ |
34 \ (c;d, s) -*-> (SKIP, u)"; |
34 \ (c;d, s) -*-> (SKIP, u)"; |
35 by(nat_ind_tac "n" 1); |
35 by(nat_ind_tac "n" 1); |
36 (* case n = 0 *) |
36 (* case n = 0 *) |
37 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2])1); |
37 by(fast_tac (!claset addIs [rtrancl_into_rtrancl2])1); |
38 (* induction step *) |
38 (* induction step *) |
39 by (safe_tac (HOL_cs addSDs [rel_pow_Suc_D2])); |
39 by (safe_tac (!claset addSDs [rel_pow_Suc_D2])); |
40 by(split_all_tac 1); |
40 by(split_all_tac 1); |
41 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); |
41 by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
42 qed_spec_mp "lemma1"; |
42 qed_spec_mp "lemma1"; |
43 |
43 |
44 |
44 |
45 goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
45 goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
46 be evalc.induct 1; |
46 be evalc.induct 1; |
47 |
47 |
48 (* SKIP *) |
48 (* SKIP *) |
49 br rtrancl_refl 1; |
49 br rtrancl_refl 1; |
50 |
50 |
51 (* ASSIGN *) |
51 (* ASSIGN *) |
52 by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1); |
52 by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); |
53 |
53 |
54 (* SEMI *) |
54 (* SEMI *) |
55 by (fast_tac (set_cs addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1); |
55 by (fast_tac (!claset addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1); |
56 |
56 |
57 (* IF *) |
57 (* IF *) |
58 by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); |
58 by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
59 by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); |
59 by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
60 |
60 |
61 (* WHILE *) |
61 (* WHILE *) |
62 by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1); |
62 by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); |
63 by (fast_tac (evalc1_cs addDs [rtrancl_imp_UN_rel_pow] |
63 by (fast_tac (!claset addDs [rtrancl_imp_UN_rel_pow] |
64 addIs [rtrancl_into_rtrancl2,lemma1]) 1); |
64 addIs [rtrancl_into_rtrancl2,lemma1]) 1); |
65 |
65 |
66 qed "evalc_impl_evalc1"; |
66 qed "evalc_impl_evalc1"; |
67 |
67 |
68 |
68 |
69 goal Transition.thy |
69 goal Transition.thy |
70 "!c d s u. (c;d,s) -n-> (SKIP,u) --> \ |
70 "!c d s u. (c;d,s) -n-> (SKIP,u) --> \ |
71 \ (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)"; |
71 \ (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)"; |
72 by(nat_ind_tac "n" 1); |
72 by(nat_ind_tac "n" 1); |
73 (* case n = 0 *) |
73 (* case n = 0 *) |
74 by (fast_tac (HOL_cs addSDs [hlemma1] addss !simpset) 1); |
74 by (fast_tac (!claset addss !simpset) 1); |
75 (* induction step *) |
75 (* induction step *) |
76 by (fast_tac (HOL_cs addSIs [rtrancl_refl,le_SucI,le_refl] |
76 by (fast_tac (!claset addSIs [le_SucI,le_refl] |
77 addSDs [rel_pow_Suc_D2] |
77 addSDs [rel_pow_Suc_D2] |
78 addSEs (evalc1_elim_cases@ |
78 addSEs [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2]) 1); |
79 [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2])) 1); |
|
80 qed_spec_mp "lemma2"; |
79 qed_spec_mp "lemma2"; |
81 |
80 |
82 goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t"; |
81 goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t"; |
83 by (com.induct_tac "c" 1); |
82 by (com.induct_tac "c" 1); |
84 by (safe_tac (evalc1_cs addSDs [rtrancl_imp_UN_rel_pow])); |
83 by (safe_tac (!claset addSDs [rtrancl_imp_UN_rel_pow])); |
85 |
84 |
86 (* SKIP *) |
85 (* SKIP *) |
87 by (fast_tac (evalc1_cs addSEs rel_pow_E2::evalc1_elim_cases) 1); |
86 by (fast_tac (!claset addSEs [rel_pow_E2]) 1); |
88 |
87 |
89 (* ASSIGN *) |
88 (* ASSIGN *) |
90 by (fast_tac (evalc1_cs addSDs [hlemma2] |
89 by (fast_tac (!claset addSDs [hlemma] addSEs [rel_pow_E2] |
91 addSEs rel_pow_E2::evalc1_elim_cases |
90 addss !simpset) 1); |
92 addss !simpset) 1); |
|
93 |
91 |
94 (* SEMI *) |
92 (* SEMI *) |
95 by (fast_tac (evalc1_cs addSDs [lemma2,rel_pow_imp_rtrancl]) 1); |
93 by (fast_tac (!claset addSDs [lemma2,rel_pow_imp_rtrancl]) 1); |
96 |
94 |
97 (* IF *) |
95 (* IF *) |
98 be rel_pow_E2 1; |
96 be rel_pow_E2 1; |
99 by (Asm_full_simp_tac 1); |
97 by (Asm_full_simp_tac 1); |
100 by (fast_tac (evalc1_cs addSDs[rel_pow_imp_rtrancl]addEs evalc1_elim_cases) 1); |
98 by (fast_tac (!claset addSDs [rel_pow_imp_rtrancl]) 1); |
101 |
99 |
102 (* WHILE, induction on the length of the computation *) |
100 (* WHILE, induction on the length of the computation *) |
103 by(rotate_tac 1 1); |
101 by(rotate_tac 1 1); |
104 by (etac rev_mp 1); |
102 by (etac rev_mp 1); |
105 by (res_inst_tac [("x","s")] spec 1); |
103 by (res_inst_tac [("x","s")] spec 1); |
106 by(res_inst_tac [("n","n")] less_induct 1); |
104 by(res_inst_tac [("n","n")] less_induct 1); |
107 by (strip_tac 1); |
105 by (strip_tac 1); |
108 be rel_pow_E2 1; |
106 be rel_pow_E2 1; |
109 by (Asm_full_simp_tac 1); |
107 by (Asm_full_simp_tac 1); |
110 by (eresolve_tac evalc1_elim_cases 1); |
108 by (eresolve_tac evalc1_Es 1); |
111 |
109 |
112 (* WhileFalse *) |
110 (* WhileFalse *) |
113 by (fast_tac (evalc1_cs addSDs [hlemma2]) 1); |
111 by (fast_tac (!claset addSDs [hlemma]) 1); |
114 |
112 |
115 (* WhileTrue *) |
113 (* WhileTrue *) |
116 by(fast_tac(evalc1_cs addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1); |
114 by(fast_tac(!claset addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1); |
117 |
115 |
118 qed_spec_mp "evalc1_impl_evalc"; |
116 qed_spec_mp "evalc1_impl_evalc"; |
119 |
117 |
120 |
118 |
121 (**** proof of the equivalence of evalc and evalc1 ****) |
119 (**** proof of the equivalence of evalc and evalc1 ****) |
129 |
127 |
130 goal Transition.thy |
128 goal Transition.thy |
131 "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \ |
129 "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \ |
132 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3"; |
130 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3"; |
133 be converse_rtrancl_induct2 1; |
131 be converse_rtrancl_induct2 1; |
134 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); |
132 by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
135 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); |
133 by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
136 qed_spec_mp "my_lemma1"; |
134 qed_spec_mp "my_lemma1"; |
137 |
135 |
138 |
136 |
139 goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
137 goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
140 be evalc.induct 1; |
138 be evalc.induct 1; |
141 |
139 |
142 (* SKIP *) |
140 (* SKIP *) |
143 br rtrancl_refl 1; |
141 br rtrancl_refl 1; |
144 |
142 |
145 (* ASSIGN *) |
143 (* ASSIGN *) |
146 by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1); |
144 by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); |
147 |
145 |
148 (* SEMI *) |
146 (* SEMI *) |
149 by (fast_tac (HOL_cs addIs [my_lemma1]) 1); |
147 by (fast_tac (!claset addIs [my_lemma1]) 1); |
150 |
148 |
151 (* IF *) |
149 (* IF *) |
152 by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); |
150 by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
153 by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); |
151 by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
154 |
152 |
155 (* WHILE *) |
153 (* WHILE *) |
156 by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1); |
154 by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); |
157 by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2,my_lemma1]) 1); |
155 by (fast_tac (!claset addIs [rtrancl_into_rtrancl2,my_lemma1]) 1); |
158 |
156 |
159 qed "evalc_impl_evalc1"; |
157 qed "evalc_impl_evalc1"; |
160 |
158 |
161 (* The opposite direction is based on a Coq proof done by Ranan Fraer and |
159 (* The opposite direction is based on a Coq proof done by Ranan Fraer and |
162 Yves Bertot. The following sketch is from an email by Ranan Fraer. |
160 Yves Bertot. The following sketch is from an email by Ranan Fraer. |
194 |
192 |
195 |
193 |
196 goal Transition.thy |
194 goal Transition.thy |
197 "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)"; |
195 "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)"; |
198 be evalc1.induct 1; |
196 be evalc1.induct 1; |
199 by(ALLGOALS(fast_tac (evalc1_cs addEs (evalc_elim_cases@evalc1_elim_cases) |
197 auto(); |
200 addss !simpset))); |
|
201 qed_spec_mp "FB_lemma3"; |
198 qed_spec_mp "FB_lemma3"; |
202 |
199 |
203 val [major] = goal Transition.thy |
200 val [major] = goal Transition.thy |
204 "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t"; |
201 "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t"; |
205 br (major RS rtrancl_induct2) 1; |
202 br (major RS rtrancl_induct2) 1; |
206 by(fast_tac prod_cs 1); |
203 by(Fast_tac 1); |
207 by(fast_tac (prod_cs addIs [FB_lemma3] addbefore (split_all_tac 1)) 1); |
204 by(fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1); |
208 qed_spec_mp "FB_lemma2"; |
205 qed_spec_mp "FB_lemma2"; |
209 |
206 |
210 goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t"; |
207 goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t"; |
211 by (fast_tac (evalc1_cs addEs [FB_lemma2]) 1); |
208 by (fast_tac (!claset addEs [FB_lemma2]) 1); |
212 qed "evalc1_impl_evalc"; |
209 qed "evalc1_impl_evalc"; |