equal
deleted
inserted
replaced
165 proof |
165 proof |
166 fix s s' assume s: "s : P" |
166 fix s s' assume s: "s : P" |
167 assume "Sem (While b X c) s s'" |
167 assume "Sem (While b X c) s s'" |
168 then obtain n where "iter n b (Sem c) s s'" by auto |
168 then obtain n where "iter n b (Sem c) s s'" by auto |
169 from this and s show "s' : P Int -b" |
169 from this and s show "s' : P Int -b" |
170 proof (induct n fixing: s) |
170 proof (induct n arbitrary: s) |
171 case 0 |
171 case 0 |
172 thus ?case by auto |
172 thus ?case by auto |
173 next |
173 next |
174 case (Suc n) |
174 case (Suc n) |
175 then obtain s'' where b: "s : b" and sem: "Sem c s s''" |
175 then obtain s'' where b: "s : b" and sem: "Sem c s s''" |