author | berghofe |
Fri, 24 Jul 1998 13:03:20 +0200 | |
changeset 5183 | 89f162de39cf |
parent 5117 | 7b5efef2ca74 |
child 5223 | 4cb05273f764 |
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 |
|
5117 | 25 |
Goal "(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 |
||
5069 | 32 |
Goal |
1701 | 33 |
"!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \ |
1700 | 34 |
\ (c;d, s) -*-> (SKIP, u)"; |
5183 | 35 |
by (induct_tac "n" 1); |
4089 | 36 |
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
|
37 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1); |
1700 | 38 |
qed_spec_mp "lemma1"; |
39 |
||
40 |
||
5117 | 41 |
Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
2031 | 42 |
by (etac evalc.induct 1); |
1700 | 43 |
|
44 |
(* SKIP *) |
|
2031 | 45 |
by (rtac rtrancl_refl 1); |
1700 | 46 |
|
47 |
(* ASSIGN *) |
|
4089 | 48 |
by (fast_tac (claset() addSIs [r_into_rtrancl]) 1); |
1700 | 49 |
|
50 |
(* SEMI *) |
|
4089 | 51 |
by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1); |
1700 | 52 |
|
53 |
(* IF *) |
|
4089 | 54 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
55 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
|
1700 | 56 |
|
57 |
(* WHILE *) |
|
4089 | 58 |
by (fast_tac (claset() addSIs [r_into_rtrancl]) 1); |
59 |
by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow] |
|
1700 | 60 |
addIs [rtrancl_into_rtrancl2,lemma1]) 1); |
61 |
||
1730 | 62 |
qed "evalc_impl_evalc1"; |
1700 | 63 |
|
64 |
||
5069 | 65 |
Goal |
1701 | 66 |
"!c d s u. (c;d,s) -n-> (SKIP,u) --> \ |
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); |
1973 | 102 |
by (eresolve_tac evalc1_Es 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 |
|
5069 | 122 |
Goal |
5117 | 123 |
"(c1,s1) -*-> (SKIP,s2) ==> \ |
1939 | 124 |
\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3"; |
4746 | 125 |
by (etac converse_rtrancl_induct2 1); |
4089 | 126 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
127 |
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
|
128 |
qed_spec_mp "my_lemma1"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
129 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
130 |
|
5117 | 131 |
Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)"; |
2031 | 132 |
by (etac evalc.induct 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
133 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
134 |
(* SKIP *) |
2031 | 135 |
by (rtac rtrancl_refl 1); |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
136 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
137 |
(* ASSIGN *) |
4089 | 138 |
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
|
139 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
140 |
(* SEMI *) |
4089 | 141 |
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
|
142 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
143 |
(* IF *) |
4089 | 144 |
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
145 |
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
|
146 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
147 |
(* WHILE *) |
4089 | 148 |
by (fast_tac (claset() addSIs [r_into_rtrancl]) 1); |
149 |
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
|
150 |
|
1730 | 151 |
qed "evalc_impl_evalc1"; |
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 |
(* 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
|
154 |
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
|
155 |
*) |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
156 |
(* |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
157 |
First we've broke it into 2 lemmas: |
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 |
Lemma 1 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
160 |
((c,s) --> (SKIP,t)) => (<c,s> -c-> t) |
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 |
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
|
163 |
and while_false. |
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 2 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
166 |
((c,s) -*-> (c',s')) /\ <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 |
<c,s> -c-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
169 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
170 |
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
|
171 |
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
|
172 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
173 |
Lemma 3 |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
174 |
((c,s) --> (c',s')) /\ <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 |
<c,s> -c-> t |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
177 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
178 |
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
|
179 |
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
|
180 |
semantics. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
181 |
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
|
182 |
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
|
183 |
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
|
184 |
of Lemma 1. |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
185 |
*) |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
186 |
|
4897 | 187 |
(*Delsimps [update_apply];*) |
5069 | 188 |
Goal |
5117 | 189 |
"((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)"; |
2031 | 190 |
by (etac evalc1.induct 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4153
diff
changeset
|
191 |
by Auto_tac; |
1730 | 192 |
qed_spec_mp "FB_lemma3"; |
4897 | 193 |
(*Addsimps [update_apply];*) |
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
194 |
|
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
195 |
val [major] = goal Transition.thy |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
196 |
"(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t"; |
2031 | 197 |
by (rtac (major RS rtrancl_induct2) 1); |
4897 | 198 |
by (Fast_tac 1); |
4651 | 199 |
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
|
200 |
qed_spec_mp "FB_lemma2"; |
e1a64a6c454d
Added an equivalence proof which avoids the use of -n->
nipkow
parents:
1701
diff
changeset
|
201 |
|
5117 | 202 |
Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t"; |
4089 | 203 |
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
|
204 |
qed "evalc1_impl_evalc"; |