Theory Hotel_Example_Prolog

theory Hotel_Example_Prolog
imports
  Hotel_Example
  "HOL-Library.Predicate_Compile_Alternative_Defs"
  "HOL-Library.Code_Prolog"
begin

declare Let_def[code_pred_inline]
(*
thm hotel_def
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)

lemma [code_pred_inline]: "(-) == (%A B x. A x ∧ ¬ B x)"
by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
*)

definition issuedp :: "event list => key => bool"
where
  "issuedp evs k = (k ∈ issued evs)"

lemma [code_pred_def]:
  "issuedp [] Key0 = True"
  "issuedp (e # s) k = (issuedp s k ∨ (case e of Check_in g r (k1, k2) => k = k2 | _ => False))"
unfolding issuedp_def issued.simps initk_def
by (auto split: event.split)

definition cardsp
where
 "cardsp s g k = (k ∈ cards s g)"

lemma [code_pred_def]:
  "cardsp [] g k = False"
  "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 ∨ C k else C k | _ => C k)"
unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)

definition
  "isinp evs r g = (g ∈ isin evs r)"

lemma [code_pred_def]:
  "isinp [] r g = False"
  "isinp (e # s) r g =
  (let G = isinp s r
   in case e of Check_in g' r c => G g
    | Enter g' r' c => if r' = r then g = g' ∨ G g else G g
    | Exit g' r' => if r' = r then ((g ≠ g') ∧ G g) else G g)"
unfolding isinp_def [abs_def] isin.simps by (auto simp add: Let_def split: event.split)

declare hotel.simps(1)[code_pred_def]
lemma [code_pred_def]:
"hotel (e # s) =
  (hotel s & (case e of Check_in g r (k, k') => k = currk s r & ¬ issuedp s k'
  | Enter g r (k, k') => cardsp s g (k, k') & (roomk s r = k ∨ roomk s r = k')
  | Exit g r => isinp s r g))"
unfolding hotel.simps issuedp_def cardsp_def isinp_def
by (auto split: event.split)

declare List.member_code [code_pred_def]

lemma [code_pred_def]: "no_Check_in s r = (¬ (∃g c. List.member s (Check_in g r c)))"
  by (simp add: no_Check_in_def)

lemma [code_pred_def]: "feels_safe s r =
(∃s⇩1 s⇩2 s⇩3 g c c'.
    s =
    s⇩3 @
    [Enter g r c] @ s⇩2 @ [Check_in g r c'] @ s⇩1 &
    no_Check_in (s⇩3 @ s⇩2) r &
    (¬ (∃ g'. isinp (s⇩2 @ [Check_in g r c] @ s⇩1) r g')))"
unfolding feels_safe_def isinp_def by auto

setup ‹Code_Prolog.map_code_options (K
  {ensure_groundness = true,
  limit_globally = NONE,
  limited_types = [],
  limited_predicates = [],
  replacing = [],
  manual_reorder = []})›

values_prolog 40 "{s. hotel s}"

setup ‹
  Context.theory_map
    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
›

lemma "⟦ hotel s; isinp s r g ⟧ ⟹ owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

section ‹Manual setup to find the counterexample›

setup ‹Code_Prolog.map_code_options (K 
  {ensure_groundness = true,
   limit_globally = NONE,
   limited_types = [],
   limited_predicates = [(["hotel"], 4)],
   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
   manual_reorder = []})›

lemma
  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops

setup ‹Code_Prolog.map_code_options (K 
  {ensure_groundness = true,
   limit_globally = NONE,
   limited_types = [],
   limited_predicates = [(["hotel"], 5)],
   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
   manual_reorder = []})›

lemma
  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

section ‹Using a global limit for limiting the execution› 

text ‹A global depth limit of 10 does not suffice to find the counterexample.›

setup ‹
  Code_Prolog.map_code_options (K
  {ensure_groundness = true,
  limit_globally = SOME 10,
  limited_types = [],
  limited_predicates = [],
  replacing = [],
  manual_reorder = []})
›

lemma
  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops

text ‹But a global depth limit of 11 does.›

setup ‹
  Code_Prolog.map_code_options (K
  {ensure_groundness = true,
  limit_globally = SOME 11,
  limited_types = [],
  limited_predicates = [],
  replacing = [],
  manual_reorder = []})
›

lemma
  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

end