equal
deleted
inserted
replaced
14 none can have been present before *) |
14 none can have been present before *) |
15 lemma eval_evals_exec_xcpt: |
15 lemma eval_evals_exec_xcpt: |
16 "(G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and> |
16 "(G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and> |
17 (G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and> |
17 (G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and> |
18 (G \<turnstile> xs -st-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)" |
18 (G \<turnstile> xs -st-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)" |
19 by (induct rule: eval_evals_exec.induct, auto) |
19 by (induct rule: eval_evals_exec.induct) auto |
20 |
20 |
21 |
21 |
22 (* instance of eval_evals_exec_xcpt for eval *) |
22 (* instance of eval_evals_exec_xcpt for eval *) |
23 lemma eval_xcpt: "G \<turnstile> xs -ex\<succ>val-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None" |
23 lemma eval_xcpt: "G \<turnstile> xs -ex\<succ>val-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None" |
24 (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T") |
24 (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T") |