equal
deleted
inserted
replaced
57 unfolding hotel.simps issuedp_def cardsp_def isinp_def |
57 unfolding hotel.simps issuedp_def cardsp_def isinp_def |
58 by (auto split: event.split) |
58 by (auto split: event.split) |
59 |
59 |
60 declare List.member_rec[code_pred_def] |
60 declare List.member_rec[code_pred_def] |
61 |
61 |
62 lemma [code_pred_def]: "no_Check_in s r = (~ (EX g c. List.member s (Check_in g r c)))" |
62 lemma [code_pred_def]: "no_Check_in s r = (\<not> (\<exists>g c. List.member s (Check_in g r c)))" |
63 unfolding no_Check_in_def member_def by auto |
63 unfolding no_Check_in_def member_def by auto |
64 |
64 |
65 lemma [code_pred_def]: "feels_safe s r = |
65 lemma [code_pred_def]: "feels_safe s r = |
66 (EX s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'. |
66 (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'. |
67 s = |
67 s = |
68 s\<^sub>3 @ |
68 s\<^sub>3 @ |
69 [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 & |
69 [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 & |
70 no_Check_in (s\<^sub>3 @ s\<^sub>2) r & |
70 no_Check_in (s\<^sub>3 @ s\<^sub>2) r & |
71 (\<not> (\<exists> g'. isinp (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r g')))" |
71 (\<not> (\<exists> g'. isinp (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r g')))" |