author  nipkow 
Fri, 23 Aug 1996 13:03:02 +0200  
changeset 1939  ad5bb12605fb 
parent 1730  1c7f793fc374 
child 1973  8c94c9a5be10 
permissions  rwrr 
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 

1700  13 
val relpow_cs = rel_cs addSEs [rel_pow_0_E]; 
14 

15 
val evalc1_elim_cases = 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", "(WHILE b DO c,s) 1> t"]; 

18 

19 
val evalc1_cs = relpow_cs addIs (evalc.intrs@evalc1.intrs); 

20 

1701  21 
goal Transition.thy "!!c. (c,s) 0> (SKIP,u) ==> c = SKIP & s = u"; 
1700  22 
by(fast_tac evalc1_cs 1); 
23 
val hlemma1 = result(); 

24 

1701  25 
goal Transition.thy "!!s. (SKIP,s) m> (SKIP,t) ==> s = t & m = 0"; 
1700  26 
be rel_pow_E2 1; 
27 
by (Asm_full_simp_tac 1); 

28 
by (eresolve_tac evalc1_elim_cases 1); 

29 
val hlemma2 = result(); 

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)"; 
35 
by(nat_ind_tac "n" 1); 

36 
(* case n = 0 *) 

37 
by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2])1); 

38 
(* induction step *) 

39 
by (safe_tac (HOL_cs addSDs [rel_pow_Suc_D2])); 

40 
by(split_all_tac 1); 

41 
by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); 

42 
qed_spec_mp "lemma1"; 

43 

44 

1730  45 
goal Transition.thy "!!c s s1. <c,s> c> s1 ==> (c,s) *> (SKIP,s1)"; 
46 
be evalc.induct 1; 

1700  47 

48 
(* SKIP *) 

49 
br rtrancl_refl 1; 

50 

51 
(* ASSIGN *) 

52 
by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1); 

53 

54 
(* SEMI *) 

55 
by (fast_tac (set_cs addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1); 

56 

57 
(* IF *) 

58 
by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); 

59 
by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); 

60 

61 
(* WHILE *) 

62 
by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1); 

63 
by (fast_tac (evalc1_cs addDs [rtrancl_imp_UN_rel_pow] 

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)"; 

1700  72 
by(nat_ind_tac "n" 1); 
73 
(* case n = 0 *) 

74 
by (fast_tac (HOL_cs addSDs [hlemma1] addss !simpset) 1); 

75 
(* induction step *) 

76 
by (fast_tac (HOL_cs addSIs [rtrancl_refl,le_SucI,le_refl] 

77 
addSDs [rel_pow_Suc_D2] 

78 
addSEs (evalc1_elim_cases@ 

79 
[rel_pow_imp_rtrancl,rtrancl_into_rtrancl2])) 1); 

80 
qed_spec_mp "lemma2"; 

81 

82 
goal Transition.thy "!s t. (c,s) *> (SKIP,t) > <c,s> c> t"; 

83 
by (com.induct_tac "c" 1); 

84 
by (safe_tac (evalc1_cs addSDs [rtrancl_imp_UN_rel_pow])); 

85 

86 
(* SKIP *) 

87 
by (fast_tac (evalc1_cs addSEs rel_pow_E2::evalc1_elim_cases) 1); 

88 

89 
(* ASSIGN *) 

90 
by (fast_tac (evalc1_cs addSDs [hlemma2] 

91 
addSEs rel_pow_E2::evalc1_elim_cases 

92 
addss !simpset) 1); 

93 

94 
(* SEMI *) 

95 
by (fast_tac (evalc1_cs addSDs [lemma2,rel_pow_imp_rtrancl]) 1); 

96 

97 
(* IF *) 

98 
be rel_pow_E2 1; 

99 
by (Asm_full_simp_tac 1); 

100 
by (fast_tac (evalc1_cs addSDs[rel_pow_imp_rtrancl]addEs evalc1_elim_cases) 1); 

101 

102 
(* WHILE, induction on the length of the computation *) 

103 
by(rotate_tac 1 1); 

104 
by (etac rev_mp 1); 

105 
by (res_inst_tac [("x","s")] spec 1); 

106 
by(res_inst_tac [("n","n")] less_induct 1); 

107 
by (strip_tac 1); 

108 
be rel_pow_E2 1; 

109 
by (Asm_full_simp_tac 1); 

110 
by (eresolve_tac evalc1_elim_cases 1); 

111 

112 
(* WhileFalse *) 

113 
by (fast_tac (evalc1_cs addSDs [hlemma2]) 1); 

114 

115 
(* WhileTrue *) 

116 
by(fast_tac(evalc1_cs addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1); 

117 

118 
qed_spec_mp "evalc1_impl_evalc"; 

119 

120 

121 
(**** proof of the equivalence of evalc and evalc1 ****) 

122 

123 
goal Transition.thy "((c, s) *> (SKIP, t)) = (<c,s> c> t)"; 

124 
by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1); 

125 
qed "evalc1_eq_evalc"; 

1707
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

126 

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 
section "A Proof Without n>"; 
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 
goal Transition.thy 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

131 
"!!c1. (c1,s1) *> (SKIP,s2) ==> \ 
1939  132 
\ (c2,s2) *> cs3 > (c1;c2,s1) *> cs3"; 
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

133 
be converse_rtrancl_induct2 1; 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

134 
by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

135 
by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

136 
qed_spec_mp "my_lemma1"; 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

137 

e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

138 

1730  139 
goal Transition.thy "!!c s s1. <c,s> c> s1 ==> (c,s) *> (SKIP,s1)"; 
140 
be evalc.induct 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 
(* SKIP *) 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

143 
br rtrancl_refl 1; 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

144 

e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

145 
(* ASSIGN *) 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

146 
by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

147 

e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

148 
(* SEMI *) 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

149 
by (fast_tac (HOL_cs addIs [my_lemma1]) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

150 

e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

151 
(* IF *) 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

152 
by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

153 
by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1); 
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 
(* WHILE *) 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

156 
by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

157 
by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2,my_lemma1]) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

158 

1730  159 
qed "evalc_impl_evalc1"; 
1707
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 
(* 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

162 
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

163 
*) 
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 
First we've broke it into 2 lemmas: 
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 
Lemma 1 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

168 
((c,s) > (SKIP,t)) => (<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 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

171 
and while_false. 
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 2 
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 is proved by rule induction on the *> relation 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

179 
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

180 

e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

181 
Lemma 3 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

182 
((c,s) > (c',s')) /\ <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 
<c,s> c> t 
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 
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

187 
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

188 
semantics. 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

189 
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

190 
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

191 
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

192 
of Lemma 1. 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

193 
*) 
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 

1730  196 
goal Transition.thy 
197 
"!!c s. ((c,s) 1> (c',s')) ==> (!t. <c',s'> c> t > <c,s> c> t)"; 

198 
be evalc1.induct 1; 

1707
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

199 
by(ALLGOALS(fast_tac (evalc1_cs addEs (evalc_elim_cases@evalc1_elim_cases) 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

200 
addss !simpset))); 
1730  201 
qed_spec_mp "FB_lemma3"; 
1707
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

202 

e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

203 
val [major] = goal Transition.thy 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

204 
"(c,s) *> (c',s') ==> <c',s'> c> t > <c,s> c> t"; 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

205 
br (major RS rtrancl_induct2) 1; 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

206 
by(fast_tac prod_cs 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

207 
by(fast_tac (prod_cs addIs [FB_lemma3] addbefore (split_all_tac 1)) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

208 
qed_spec_mp "FB_lemma2"; 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

209 

e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

210 
goal Transition.thy "!!c. (c,s) *> (SKIP,t) ==> <c,s> c> t"; 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

211 
by (fast_tac (evalc1_cs addEs [FB_lemma2]) 1); 
e1a64a6c454d
Added an equivalence proof which avoids the use of n>
nipkow
parents:
1701
diff
changeset

212 
qed "evalc1_impl_evalc"; 