author | paulson |
Wed, 23 Apr 1997 11:18:29 +0200 | |
changeset 3023 | 01364e2f30ad |
parent 2637 | e9b203f854ae |
child 3439 | 54785105178c |
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 |
||
9 |
open Transition; |
|
10 |
||
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
11 |
section "Winskel's Proof"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
12 |
|
1973 | 13 |
AddSEs [rel_pow_0_E]; |
1700 | 14 |
|
1973 | 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", |
|
17 |
"(IF b THEN c1 ELSE c2, s) -1-> t"]; |
|
18 |
val evalc1_Es = map (evalc1.mk_cases com.simps) |
|
19 |
["(WHILE b DO c,s) -1-> t"]; |
|
1700 | 20 |
|
1973 | 21 |
AddSEs evalc1_SEs; |
22 |
||
23 |
AddIs evalc1.intrs; |
|
1700 | 24 |
|
1701 | 25 |
goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0"; |
2031 | 26 |
by (etac rel_pow_E2 1); |
1700 | 27 |
by (Asm_full_simp_tac 1); |
2031 | 28 |
by (Fast_tac 1); |
1973 | 29 |
val hlemma = result(); |
1700 | 30 |
|
31 |
||
32 |
goal Transition.thy |
|
1701 | 33 |
"!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \ |
1700 | 34 |
\ (c;d, s) -*-> (SKIP, u)"; |
2031 | 35 |
by (nat_ind_tac "n" 1); |
1700 | 36 |
(* case n = 0 *) |
2055 | 37 |
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2])1); |
1700 | 38 |
(* induction step *) |
1973 | 39 |
by (safe_tac (!claset addSDs [rel_pow_Suc_D2])); |
2031 | 40 |
by (split_all_tac 1); |
41 |
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
|
1700 | 42 |
qed_spec_mp "lemma1"; |
43 |
||
44 |
||
1730 | 45 |
goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
2031 | 46 |
by (etac evalc.induct 1); |
1700 | 47 |
|
48 |
(* SKIP *) |
|
2031 | 49 |
by (rtac rtrancl_refl 1); |
1700 | 50 |
|
51 |
(* ASSIGN *) |
|
1973 | 52 |
by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); |
1700 | 53 |
|
54 |
(* SEMI *) |
|
1973 | 55 |
by (fast_tac (!claset addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1); |
1700 | 56 |
|
57 |
(* IF *) |
|
1973 | 58 |
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
59 |
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
|
1700 | 60 |
|
61 |
(* WHILE *) |
|
1973 | 62 |
by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); |
63 |
by (fast_tac (!claset addDs [rtrancl_imp_UN_rel_pow] |
|
1700 | 64 |
addIs [rtrancl_into_rtrancl2,lemma1]) 1); |
65 |
||
1730 | 66 |
qed "evalc_impl_evalc1"; |
1700 | 67 |
|
68 |
||
69 |
goal Transition.thy |
|
1701 | 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)"; |
|
2031 | 72 |
by (nat_ind_tac "n" 1); |
1700 | 73 |
(* case n = 0 *) |
1973 | 74 |
by (fast_tac (!claset addss !simpset) 1); |
1700 | 75 |
(* induction step *) |
1973 | 76 |
by (fast_tac (!claset addSIs [le_SucI,le_refl] |
1700 | 77 |
addSDs [rel_pow_Suc_D2] |
1973 | 78 |
addSEs [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2]) 1); |
1700 | 79 |
qed_spec_mp "lemma2"; |
80 |
||
81 |
goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t"; |
|
82 |
by (com.induct_tac "c" 1); |
|
1973 | 83 |
by (safe_tac (!claset addSDs [rtrancl_imp_UN_rel_pow])); |
1700 | 84 |
|
85 |
(* SKIP *) |
|
1973 | 86 |
by (fast_tac (!claset addSEs [rel_pow_E2]) 1); |
1700 | 87 |
|
88 |
(* ASSIGN *) |
|
1973 | 89 |
by (fast_tac (!claset addSDs [hlemma] addSEs [rel_pow_E2] |
90 |
addss !simpset) 1); |
|
1700 | 91 |
|
92 |
(* SEMI *) |
|
1973 | 93 |
by (fast_tac (!claset addSDs [lemma2,rel_pow_imp_rtrancl]) 1); |
1700 | 94 |
|
95 |
(* IF *) |
|
2031 | 96 |
by (etac rel_pow_E2 1); |
1700 | 97 |
by (Asm_full_simp_tac 1); |
1973 | 98 |
by (fast_tac (!claset addSDs [rel_pow_imp_rtrancl]) 1); |
1700 | 99 |
|
100 |
(* WHILE, induction on the length of the computation *) |
|
2031 | 101 |
by (rotate_tac 1 1); |
1700 | 102 |
by (etac rev_mp 1); |
103 |
by (res_inst_tac [("x","s")] spec 1); |
|
2031 | 104 |
by (res_inst_tac [("n","n")] less_induct 1); |
1700 | 105 |
by (strip_tac 1); |
2031 | 106 |
by (etac rel_pow_E2 1); |
1700 | 107 |
by (Asm_full_simp_tac 1); |
1973 | 108 |
by (eresolve_tac evalc1_Es 1); |
1700 | 109 |
|
110 |
(* WhileFalse *) |
|
1973 | 111 |
by (fast_tac (!claset addSDs [hlemma]) 1); |
1700 | 112 |
|
113 |
(* WhileTrue *) |
|
2031 | 114 |
by (fast_tac(!claset addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1); |
1700 | 115 |
|
116 |
qed_spec_mp "evalc1_impl_evalc"; |
|
117 |
||
118 |
||
119 |
(**** proof of the equivalence of evalc and evalc1 ****) |
|
120 |
||
121 |
goal Transition.thy "((c, s) -*-> (SKIP, t)) = (<c,s> -c-> t)"; |
|
122 |
by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1); |
|
123 |
qed "evalc1_eq_evalc"; |
|
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
124 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
125 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
126 |
section "A Proof Without -n->"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
127 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
128 |
goal Transition.thy |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
129 |
"!!c1. (c1,s1) -*-> (SKIP,s2) ==> \ |
1939 | 130 |
\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3"; |
2031 | 131 |
by (etac converse_rtrancl_induct2 1); |
132 |
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
|
133 |
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
|
134 |
qed_spec_mp "my_lemma1"; |
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 |
|
1730 | 137 |
goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
2031 | 138 |
by (etac evalc.induct 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
139 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
140 |
(* SKIP *) |
2031 | 141 |
by (rtac rtrancl_refl 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
142 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
143 |
(* ASSIGN *) |
1973 | 144 |
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
|
145 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
146 |
(* SEMI *) |
1973 | 147 |
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
|
148 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
149 |
(* IF *) |
1973 | 150 |
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
151 |
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
|
152 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
153 |
(* WHILE *) |
1973 | 154 |
by (fast_tac (!claset addSIs [r_into_rtrancl]) 1); |
155 |
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
|
156 |
|
1730 | 157 |
qed "evalc_impl_evalc1"; |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
158 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
159 |
(* 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
|
160 |
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
|
161 |
*) |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
162 |
(* |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
163 |
First we've broke it into 2 lemmas: |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
164 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
165 |
Lemma 1 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
166 |
((c,s) --> (SKIP,t)) => (<c,s> -c-> t) |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
167 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
168 |
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
|
169 |
and while_false. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
170 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
171 |
Lemma 2 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
172 |
((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
173 |
=> |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
174 |
<c,s> -c-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
175 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
176 |
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
|
177 |
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
|
178 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
179 |
Lemma 3 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
180 |
((c,s) --> (c',s')) /\ <c',s'> -c'-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
181 |
=> |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
182 |
<c,s> -c-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
183 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
184 |
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
|
185 |
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
|
186 |
semantics. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
187 |
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
|
188 |
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
|
189 |
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
|
190 |
of Lemma 1. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
191 |
*) |
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 |
|
1730 | 194 |
goal Transition.thy |
195 |
"!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)"; |
|
2031 | 196 |
by (etac evalc1.induct 1); |
3023 | 197 |
by (Auto_tac()); |
1730 | 198 |
qed_spec_mp "FB_lemma3"; |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
199 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
200 |
val [major] = goal Transition.thy |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
201 |
"(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t"; |
2031 | 202 |
by (rtac (major RS rtrancl_induct2) 1); |
203 |
by (Fast_tac 1); |
|
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2055
diff
changeset
|
204 |
by (fast_tac (!claset addIs [FB_lemma3] addbefore split_all_tac) 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
205 |
qed_spec_mp "FB_lemma2"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
206 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
207 |
goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t"; |
1973 | 208 |
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
|
209 |
qed "evalc1_impl_evalc"; |