equal
deleted
inserted
replaced
597 abbreviation (input) |
597 abbreviation (input) |
598 store :: "state \<Rightarrow> st" |
598 store :: "state \<Rightarrow> st" |
599 where "store == snd" |
599 where "store == snd" |
600 |
600 |
601 lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False" |
601 lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False" |
602 apply (erule_tac x = "(Some k,y)" in all_dupE) |
602 apply (erule_tac x = "(Some k,y)" for k y in all_dupE) |
603 apply (erule_tac x = "(None,y)" in allE) |
603 apply (erule_tac x = "(None,y)" for y in allE) |
604 apply clarify |
604 apply clarify |
605 done |
605 done |
606 |
606 |
607 lemma state_not_single: "All (op = (x::state)) \<Longrightarrow> R" |
607 lemma state_not_single: "All (op = (x::state)) \<Longrightarrow> R" |
608 apply (drule_tac x = "(if abrupt x = None then Some ?x else None,?y)" in spec) |
608 apply (drule_tac x = "(if abrupt x = None then Some x' else None, y)" for x' y in spec) |
609 apply clarsimp |
609 apply clarsimp |
610 done |
610 done |
611 |
611 |
612 definition |
612 definition |
613 normal :: "state \<Rightarrow> bool" |
613 normal :: "state \<Rightarrow> bool" |
821 \<Longrightarrow> error_free (x, set_locals l s')" |
821 \<Longrightarrow> error_free (x, set_locals l s')" |
822 by (simp add: error_free_def) |
822 by (simp add: error_free_def) |
823 |
823 |
824 |
824 |
825 end |
825 end |
826 |
|