author | oheimb |
Tue, 04 Jul 2000 10:54:46 +0200 | |
changeset 9241 | f961c1fdff50 |
parent 8442 | 96023903c2df |
child 9556 | dcdcfb0545e0 |
permissions | -rw-r--r-- |
1700 | 1 |
(* Title: HOL/IMP/Transition.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow & Robert Sandner, TUM |
|
4 |
Copyright 1996 TUM |
|
5 |
||
6 |
Equivalence of Natural and Transition semantics |
|
7 |
*) |
|
8 |
||
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
9 |
section "Winskel's Proof"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
10 |
|
1973 | 11 |
AddSEs [rel_pow_0_E]; |
1700 | 12 |
|
6141 | 13 |
val evalc1_SEs = |
14 |
map evalc1.mk_cases |
|
15 |
["(SKIP,s) -1-> t", |
|
9241 | 16 |
"(x:==a,s) -1-> t", |
6141 | 17 |
"(c1;c2, s) -1-> t", |
8016 | 18 |
"(IF b THEN c1 ELSE c2, s) -1-> t", |
19 |
"(WHILE b DO c, s) -1-> t"]; |
|
6141 | 20 |
|
21 |
val evalc1_E = evalc1.mk_cases "(WHILE b DO c,s) -1-> t"; |
|
1700 | 22 |
|
1973 | 23 |
AddSEs evalc1_SEs; |
24 |
||
25 |
AddIs evalc1.intrs; |
|
1700 | 26 |
|
5117 | 27 |
Goal "(SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0"; |
2031 | 28 |
by (etac rel_pow_E2 1); |
1700 | 29 |
by (Asm_full_simp_tac 1); |
2031 | 30 |
by (Fast_tac 1); |
1973 | 31 |
val hlemma = result(); |
1700 | 32 |
|
33 |
||
5278 | 34 |
Goal "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \ |
1700 | 35 |
\ (c;d, s) -*-> (SKIP, u)"; |
5183 | 36 |
by (induct_tac "n" 1); |
4089 | 37 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1); |
4772
8c7e7eaffbdf
split_all_tac now fails if there is nothing to split
oheimb
parents:
4746
diff
changeset
|
38 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1); |
1700 | 39 |
qed_spec_mp "lemma1"; |
40 |
||
41 |
||
5117 | 42 |
Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
2031 | 43 |
by (etac evalc.induct 1); |
1700 | 44 |
|
45 |
(* SKIP *) |
|
2031 | 46 |
by (rtac rtrancl_refl 1); |
1700 | 47 |
|
48 |
(* ASSIGN *) |
|
4089 | 49 |
by (fast_tac (claset() addSIs [r_into_rtrancl]) 1); |
1700 | 50 |
|
51 |
(* SEMI *) |
|
4089 | 52 |
by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1); |
1700 | 53 |
|
54 |
(* IF *) |
|
4089 | 55 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
56 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
|
1700 | 57 |
|
58 |
(* WHILE *) |
|
4089 | 59 |
by (fast_tac (claset() addSIs [r_into_rtrancl]) 1); |
60 |
by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow] |
|
1700 | 61 |
addIs [rtrancl_into_rtrancl2,lemma1]) 1); |
62 |
||
1730 | 63 |
qed "evalc_impl_evalc1"; |
1700 | 64 |
|
65 |
||
5278 | 66 |
Goal "!c d s u. (c;d,s) -n-> (SKIP,u) --> \ |
1701 | 67 |
\ (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)"; |
4897 | 68 |
by (induct_tac "n" 1); |
1700 | 69 |
(* case n = 0 *) |
4089 | 70 |
by (fast_tac (claset() addss simpset()) 1); |
1700 | 71 |
(* induction step *) |
4089 | 72 |
by (fast_tac (claset() addSIs [le_SucI,le_refl] |
1700 | 73 |
addSDs [rel_pow_Suc_D2] |
1973 | 74 |
addSEs [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2]) 1); |
1700 | 75 |
qed_spec_mp "lemma2"; |
76 |
||
5069 | 77 |
Goal "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t"; |
4897 | 78 |
by (induct_tac "c" 1); |
4089 | 79 |
by (safe_tac (claset() addSDs [rtrancl_imp_UN_rel_pow])); |
1700 | 80 |
|
81 |
(* SKIP *) |
|
4089 | 82 |
by (fast_tac (claset() addSEs [rel_pow_E2]) 1); |
1700 | 83 |
|
84 |
(* ASSIGN *) |
|
4897 | 85 |
by (fast_tac (claset() addSDs [hlemma] addSEs [rel_pow_E2]) 1); |
1700 | 86 |
|
87 |
(* SEMI *) |
|
4089 | 88 |
by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1); |
1700 | 89 |
|
90 |
(* IF *) |
|
2031 | 91 |
by (etac rel_pow_E2 1); |
1700 | 92 |
by (Asm_full_simp_tac 1); |
4089 | 93 |
by (fast_tac (claset() addSDs [rel_pow_imp_rtrancl]) 1); |
1700 | 94 |
|
95 |
(* WHILE, induction on the length of the computation *) |
|
4153 | 96 |
by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1); |
1700 | 97 |
by (res_inst_tac [("x","s")] spec 1); |
2031 | 98 |
by (res_inst_tac [("n","n")] less_induct 1); |
1700 | 99 |
by (strip_tac 1); |
2031 | 100 |
by (etac rel_pow_E2 1); |
1700 | 101 |
by (Asm_full_simp_tac 1); |
6141 | 102 |
by (etac evalc1_E 1); |
1700 | 103 |
|
104 |
(* WhileFalse *) |
|
4089 | 105 |
by (fast_tac (claset() addSDs [hlemma]) 1); |
1700 | 106 |
|
107 |
(* WhileTrue *) |
|
4089 | 108 |
by (fast_tac(claset() addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1); |
1700 | 109 |
|
110 |
qed_spec_mp "evalc1_impl_evalc"; |
|
111 |
||
112 |
||
113 |
(**** proof of the equivalence of evalc and evalc1 ****) |
|
114 |
||
5069 | 115 |
Goal "((c, s) -*-> (SKIP, t)) = (<c,s> -c-> t)"; |
1700 | 116 |
by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1); |
117 |
qed "evalc1_eq_evalc"; |
|
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
118 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
119 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
120 |
section "A Proof Without -n->"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
121 |
|
5278 | 122 |
Goal "(c1,s1) -*-> (SKIP,s2) ==> \ |
1939 | 123 |
\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3"; |
4746 | 124 |
by (etac converse_rtrancl_induct2 1); |
4089 | 125 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
126 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
|
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
127 |
qed_spec_mp "my_lemma1"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
128 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
129 |
|
5117 | 130 |
Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
2031 | 131 |
by (etac evalc.induct 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
132 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
133 |
(* SKIP *) |
2031 | 134 |
by (rtac rtrancl_refl 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
135 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
136 |
(* ASSIGN *) |
4089 | 137 |
by (fast_tac (claset() addSIs [r_into_rtrancl]) 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
138 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
139 |
(* SEMI *) |
4089 | 140 |
by (fast_tac (claset() addIs [my_lemma1]) 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
141 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
142 |
(* IF *) |
4089 | 143 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
144 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
|
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
145 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
146 |
(* WHILE *) |
4089 | 147 |
by (fast_tac (claset() addSIs [r_into_rtrancl]) 1); |
148 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2,my_lemma1]) 1); |
|
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
149 |
|
1730 | 150 |
qed "evalc_impl_evalc1"; |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
151 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
152 |
(* The opposite direction is based on a Coq proof done by Ranan Fraer and |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
153 |
Yves Bertot. The following sketch is from an email by Ranan Fraer. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
154 |
*) |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
155 |
(* |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
156 |
First we've broke it into 2 lemmas: |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
157 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
158 |
Lemma 1 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
159 |
((c,s) --> (SKIP,t)) => (<c,s> -c-> t) |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
160 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
161 |
This is a quick one, dealing with the cases skip, assignment |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
162 |
and while_false. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
163 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
164 |
Lemma 2 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
165 |
((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
166 |
=> |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
167 |
<c,s> -c-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
168 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
169 |
This is proved by rule induction on the -*-> relation |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
170 |
and the induction step makes use of a third lemma: |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
171 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
172 |
Lemma 3 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
173 |
((c,s) --> (c',s')) /\ <c',s'> -c'-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
174 |
=> |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
175 |
<c,s> -c-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
176 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
177 |
This captures the essence of the proof, as it shows that <c',s'> |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
178 |
behaves as the continuation of <c,s> with respect to the natural |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
179 |
semantics. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
180 |
The proof of Lemma 3 goes by rule induction on the --> relation, |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
181 |
dealing with the cases sequence1, sequence2, if_true, if_false and |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
182 |
while_true. In particular in the case (sequence1) we make use again |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
183 |
of Lemma 1. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
184 |
*) |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
185 |
|
4897 | 186 |
(*Delsimps [update_apply];*) |
5278 | 187 |
Goal "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)"; |
2031 | 188 |
by (etac evalc1.induct 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4153
diff
changeset
|
189 |
by Auto_tac; |
1730 | 190 |
qed_spec_mp "FB_lemma3"; |
4897 | 191 |
(*Addsimps [update_apply];*) |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
192 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
193 |
val [major] = goal Transition.thy |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
194 |
"(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t"; |
2031 | 195 |
by (rtac (major RS rtrancl_induct2) 1); |
4897 | 196 |
by (Fast_tac 1); |
4651 | 197 |
by (fast_tac (claset() addIs [FB_lemma3]) 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
198 |
qed_spec_mp "FB_lemma2"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
199 |
|
5117 | 200 |
Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t"; |
4089 | 201 |
by (fast_tac (claset() addEs [FB_lemma2]) 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
202 |
qed "evalc1_impl_evalc"; |
8016 | 203 |
|
204 |
||
205 |
section "The proof in Nielson and Nielson"; |
|
206 |
||
207 |
(* The more precise n=i1+i2+1 is proved by the same script but complicates |
|
208 |
life further down, where i1,i2 < n is needed. |
|
209 |
*) |
|
210 |
Goal "!c1 s. (c1;c2,s) -n-> (SKIP,t) --> \ |
|
211 |
\ (? i1 i2 u. (c1,s) -i1-> (SKIP,u) & (c2,u) -i2-> (SKIP,t) & i1<n & i2<n)"; |
|
8064 | 212 |
by (induct_tac "n" 1); |
8016 | 213 |
by (fast_tac (claset() addSDs [hlemma]) 1); |
8064 | 214 |
by (fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2] |
8016 | 215 |
addSDs [rel_pow_Suc_D2] addss simpset()) 1); |
216 |
qed_spec_mp "comp_decomp_lemma"; |
|
217 |
||
218 |
Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t"; |
|
8064 | 219 |
by (res_inst_tac [("n","n")] less_induct 1); |
220 |
by (Clarify_tac 1); |
|
221 |
by (etac rel_pow_E2 1); |
|
8016 | 222 |
by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
223 |
by (case_tac "c" 1); |
8016 | 224 |
by (fast_tac (claset() addSDs [hlemma]) 1); |
8064 | 225 |
by (Blast_tac 1); |
226 |
by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1); |
|
227 |
by (Blast_tac 1); |
|
228 |
by (Blast_tac 1); |
|
8016 | 229 |
qed_spec_mp "evalc1_impl_evalc"; |