equal
deleted
inserted
replaced
74 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*) |
74 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*) |
75 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)" |
75 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)" |
76 |
76 |
77 definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool" |
77 definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool" |
78 where |
78 where |
79 "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'. |
79 "feels_safe s r = (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'. |
80 s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and> |
80 s = s\<^sub>3 @ [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 \<and> |
81 no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})" |
81 no_Check_in (s\<^sub>3 @ s\<^sub>2) r \<and> isin (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r = {})" |
82 |
82 |
83 |
83 |
84 section {* Some setup *} |
84 section {* Some setup *} |
85 |
85 |
86 lemma issued_nil: "issued [] = {Key0}" |
86 lemma issued_nil: "issued [] = {Key0}" |