equal
deleted
inserted
replaced
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 = (~ (EX 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\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'. |
66 (EX s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'. |
67 s = |
67 s = |
68 s\<^isub>3 @ |
68 s\<^sub>3 @ |
69 [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 & |
69 [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 & |
70 no_Check_in (s\<^isub>3 @ s\<^isub>2) r & |
70 no_Check_in (s\<^sub>3 @ s\<^sub>2) r & |
71 (\<not> (\<exists> g'. isinp (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r g')))" |
71 (\<not> (\<exists> g'. isinp (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r g')))" |
72 unfolding feels_safe_def isinp_def by auto |
72 unfolding feels_safe_def isinp_def by auto |
73 |
73 |
74 setup {* Code_Prolog.map_code_options (K |
74 setup {* Code_Prolog.map_code_options (K |
75 {ensure_groundness = true, |
75 {ensure_groundness = true, |
76 limit_globally = NONE, |
76 limit_globally = NONE, |