equal
deleted
inserted
replaced
298 \<not> normal s0 holds, |
298 \<not> normal s0 holds, |
299 I can chain "\<not> normal s0" as fact number 6 and apply the rule with |
299 I can chain "\<not> normal s0" as fact number 6 and apply the rule with |
300 cases. Auto will then solve premise 6 and 7. |
300 cases. Auto will then solve premise 6 and 7. |
301 *) |
301 *) |
302 |
302 |
303 lemma all_empty: "(!x. P) = P" |
303 lemma all_empty: "(\<forall>x. P) = P" |
304 by simp |
304 by simp |
305 |
305 |
306 corollary evaln_type_sound: |
306 corollary evaln_type_sound: |
307 assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and |
307 assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and |
308 wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and |
308 wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and |