equal
deleted
inserted
replaced
30 "cardsp s g k = (k \<in> cards s g)" |
30 "cardsp s g k = (k \<in> cards s g)" |
31 |
31 |
32 lemma [code_pred_def]: |
32 lemma [code_pred_def]: |
33 "cardsp [] g k = False" |
33 "cardsp [] g k = False" |
34 "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)" |
34 "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)" |
35 unfolding cardsp_def_raw cards.simps by (auto simp add: Let_def split: event.split) |
35 unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split) |
36 |
36 |
37 definition |
37 definition |
38 "isinp evs r g = (g \<in> isin evs r)" |
38 "isinp evs r g = (g \<in> isin evs r)" |
39 |
39 |
40 lemma [code_pred_def]: |
40 lemma [code_pred_def]: |
42 "isinp (e # s) r g = |
42 "isinp (e # s) r g = |
43 (let G = isinp s r |
43 (let G = isinp s r |
44 in case e of Check_in g' r c => G g |
44 in case e of Check_in g' r c => G g |
45 | Enter g' r' c => if r' = r then g = g' \<or> G g else G g |
45 | Enter g' r' c => if r' = r then g = g' \<or> G g else G g |
46 | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)" |
46 | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)" |
47 unfolding isinp_def_raw isin.simps by (auto simp add: Let_def split: event.split) |
47 unfolding isinp_def [abs_def] isin.simps by (auto simp add: Let_def split: event.split) |
48 |
48 |
49 declare hotel.simps(1)[code_pred_def] |
49 declare hotel.simps(1)[code_pred_def] |
50 lemma [code_pred_def]: |
50 lemma [code_pred_def]: |
51 "hotel (e # s) = |
51 "hotel (e # s) = |
52 (hotel s & (case e of Check_in g r (k, k') => k = currk s r & \<not> issuedp s k' |
52 (hotel s & (case e of Check_in g r (k, k') => k = currk s r & \<not> issuedp s k' |