Theory Hotel_Example

theory Hotel_Example
imports Main "HOL-Library.Predicate_Compile_Quickcheck"
begin

datatype guest = Guest0 | Guest1
datatype key = Key0 | Key1 | Key2 | Key3
datatype room = Room0

type_synonym card = "key * key"

datatype event =
  Check_in guest room card
| Enter guest room card
| Exit guest room

definition initk :: "room ⇒ key"
  where "initk = (%r. Key0)"

declare initk_def[code_pred_def, code]

primrec owns :: "event list ⇒ room ⇒ guest option"
where
  "owns [] r = None"
| "owns (e#s) r = (case e of
    Check_in g r' c ⇒ if r' = r then Some g else owns s r |
    Enter g r' c ⇒ owns s r |
    Exit g r' ⇒ owns s r)"

primrec currk :: "event list ⇒ room ⇒ key"
where
  "currk [] r = initk r"
| "currk (e#s) r = (let k = currk s r in
    case e of Check_in g r' (k1, k2) ⇒ if r' = r then k2 else k
            | Enter g r' c ⇒ k
            | Exit g r ⇒ k)"

primrec issued :: "event list ⇒ key set"
where
  "issued [] = range initk"
| "issued (e#s) = issued s ∪
  (case e of Check_in g r (k1, k2) ⇒ {k2} | Enter g r c ⇒ {} | Exit g r ⇒ {})"

primrec cards :: "event list ⇒ guest ⇒ card set"
where
  "cards [] g = {}"
| "cards (e#s) g = (let C = cards s g in
                    case e of Check_in g' r c ⇒ if g' = g then insert c C
                                                else C
                            | Enter g r c ⇒ C
                            | Exit g r ⇒ C)"

primrec roomk :: "event list ⇒ room ⇒ key"
where
  "roomk [] r = initk r"
| "roomk (e#s) r = (let k = roomk s r in
    case e of Check_in g r' c ⇒ k
            | Enter g r' (x,y) ⇒ if r' = r ⌦‹∧ x = k› then y else k
            | Exit g r ⇒ k)"

primrec isin :: "event list ⇒ room ⇒ guest set"
where
  "isin [] r = {}"
| "isin (e#s) r = (let G = isin s r in
                 case e of Check_in g r c ⇒ G
                 | Enter g r' c ⇒ if r' = r then {g} ∪ G else G
                 | Exit g r' ⇒ if r'=r then G - {g} else G)"

primrec hotel :: "event list ⇒ bool"
where
  "hotel []  = True"
| "hotel (e # s) = (hotel s & (case e of
  Check_in g r (k,k') ⇒ k = currk s r ∧ k' ∉ issued s |
  Enter g r (k,k') ⇒ (k,k') ∈ cards s g & (roomk s r ∈ {k, k'}) |
  Exit g r ⇒ g ∈ isin s r))"

definition no_Check_in :: "event list ⇒ room ⇒ bool" where(*>*)
[code del]: "no_Check_in s r ≡ ¬(∃g c. Check_in g r c ∈ set s)"

definition feels_safe :: "event list ⇒ room ⇒ bool"
where
  "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 ∧ isin (s⇩2 @ [Check_in g r c] @ s⇩1) r = {})"


section ‹Some setup›

lemma issued_nil: "issued [] = {Key0}"
by (auto simp add: initk_def)

lemmas issued_simps[code] = issued_nil issued.simps(2)


setup ‹Predicate_Compile_Data.ignore_consts [\<^const_name>‹Set.member›,
  \<^const_name>‹issued›, \<^const_name>‹cards›, \<^const_name>‹isin›,
  \<^const_name>‹Collect›, \<^const_name>‹insert›]›
ML_val ‹Core_Data.force_modes_and_compilations›

fun find_first :: "('a => 'b option) => 'a list => 'b option"
where
  "find_first f [] = None"
| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"

axiomatization cps_of_set :: "'a set => ('a => term list option) => term list option"
where cps_of_set_code [code]: "cps_of_set (set xs) f = find_first f xs"

axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"

axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
    => 'b list => 'a Quickcheck_Exhaustive.three_valued"
where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
  and find_first'_Cons: "find_first' f (x # xs) =
    (case f (Quickcheck_Exhaustive.Known x) of
      Quickcheck_Exhaustive.No_value => find_first' f xs
    | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x
    | Quickcheck_Exhaustive.Unknown_value =>
        (case find_first' f xs of Quickcheck_Exhaustive.Value x =>
          Quickcheck_Exhaustive.Value x
        | _ => Quickcheck_Exhaustive.Unknown_value))"

lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons

axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"

setup ‹
let
  val Fun = Predicate_Compile_Aux.Fun
  val Input = Predicate_Compile_Aux.Input
  val Output = Predicate_Compile_Aux.Output
  val Bool = Predicate_Compile_Aux.Bool
  val oi = Fun (Output, Fun (Input, Bool))
  val ii = Fun (Input, Fun (Input, Bool))
  fun of_set compfuns (Type ("fun", [T, _])) =
    case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
      Type ("Quickcheck_Exhaustive.three_valued", _) => 
        Const(\<^const_name>‹neg_cps_of_set›, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
    | _ => Const(\<^const_name>‹pos_cps_of_set›, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
  fun member compfuns (U as Type ("fun", [T, _])) =
    (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
      (Const (\<^const_name>‹Set.member›, T --> HOLogic.mk_setT T --> \<^typ>‹bool›) $ Bound 1 $ Bound 0))))
 
in
  Core_Data.force_modes_and_compilations \<^const_name>‹Set.member›
    [(oi, (of_set, false)), (ii, (member, false))]
end
›
section ‹Property›

lemma "⟦ hotel s; g ∈ isin s r ⟧ ⟹ owns s r = Some g"
quickcheck[tester = exhaustive, size = 6, expect = counterexample]
quickcheck[tester = smart_exhaustive, depth = 6, expect = counterexample]
oops

lemma
  "hotel s ==> feels_safe s r ==> g ∈ isin s r ==> owns s r = Some g"
quickcheck[smart_exhaustive, depth = 10, allow_function_inversion, expect = counterexample]
oops

section ‹Refinement›

fun split_list
where
  "split_list [] = [([], [])]"
| "split_list (z # zs) = (([], z # zs) # [(z # xs', ys'). (xs', ys') <- split_list zs])"

lemma split_list: "((xs, ys) ∈ set (split_list zs)) = (zs = xs @ ys)"
apply (induct zs arbitrary: xs ys)
apply fastforce
apply (case_tac xs)
apply auto
done

lemma [code]: "no_Check_in s r = list_all (%x. case x of Check_in g r' c => r ≠ r' | _ => True) s"
unfolding no_Check_in_def list_all_iff
apply auto
apply (case_tac x)
apply auto
done

lemma [code]: "feels_safe s r = list_ex (%(s3, s2, s1, g, c, c'). no_Check_in (s3 @ s2) r &
    isin (s2 @ [Check_in g r c] @ s1) r = {}) ([(s3, s2, s1, g, c, c'). (s3, Enter g' r' c # r3) <- split_list s, r' = r, (s2, Check_in g r'' c' # s1) <- split_list r3, r'' = r, g = g'])"
unfolding feels_safe_def list_ex_iff
by auto (metis split_list)+

lemma
  "hotel s ==> feels_safe s r ==> g ∈ isin s r ==> owns s r = Some g"
(* quickcheck[exhaustive, size = 9, timeout = 2000] -- maybe possible with a lot of time *)
quickcheck[narrowing, size = 7, expect = counterexample]
oops

end