src/HOL/Quickcheck_Examples/Hotel_Example.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63177 6c05c4632949
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
executable domain membership checks
     1 theory Hotel_Example
     2 imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     3 begin
     4 
     5 datatype guest = Guest0 | Guest1
     6 datatype key = Key0 | Key1 | Key2 | Key3
     7 datatype room = Room0
     8 
     9 type_synonym card = "key * key"
    10 
    11 datatype event =
    12   Check_in guest room card
    13 | Enter guest room card
    14 | Exit guest room
    15 
    16 definition initk :: "room \<Rightarrow> key"
    17   where "initk = (%r. Key0)"
    18 
    19 declare initk_def[code_pred_def, code]
    20 
    21 primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
    22 where
    23   "owns [] r = None"
    24 | "owns (e#s) r = (case e of
    25     Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
    26     Enter g r' c \<Rightarrow> owns s r |
    27     Exit g r' \<Rightarrow> owns s r)"
    28 
    29 primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
    30 where
    31   "currk [] r = initk r"
    32 | "currk (e#s) r = (let k = currk s r in
    33     case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
    34             | Enter g r' c \<Rightarrow> k
    35             | Exit g r \<Rightarrow> k)"
    36 
    37 primrec issued :: "event list \<Rightarrow> key set"
    38 where
    39   "issued [] = range initk"
    40 | "issued (e#s) = issued s \<union>
    41   (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
    42 
    43 primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
    44 where
    45   "cards [] g = {}"
    46 | "cards (e#s) g = (let C = cards s g in
    47                     case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
    48                                                 else C
    49                             | Enter g r c \<Rightarrow> C
    50                             | Exit g r \<Rightarrow> C)"
    51 
    52 primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
    53 where
    54   "roomk [] r = initk r"
    55 | "roomk (e#s) r = (let k = roomk s r in
    56     case e of Check_in g r' c \<Rightarrow> k
    57             | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
    58             | Exit g r \<Rightarrow> k)"
    59 
    60 primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
    61 where
    62   "isin [] r = {}"
    63 | "isin (e#s) r = (let G = isin s r in
    64                  case e of Check_in g r c \<Rightarrow> G
    65                  | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
    66                  | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
    67 
    68 primrec hotel :: "event list \<Rightarrow> bool"
    69 where
    70   "hotel []  = True"
    71 | "hotel (e # s) = (hotel s & (case e of
    72   Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
    73   Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    74   Exit g r \<Rightarrow> g : isin s r))"
    75 
    76 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
    77 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
    78 
    79 definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
    80 where
    81   "feels_safe s r = (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
    82    s = s\<^sub>3 @ [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 \<and>
    83    no_Check_in (s\<^sub>3 @ s\<^sub>2) r \<and> isin (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r = {})"
    84 
    85 
    86 section \<open>Some setup\<close>
    87 
    88 lemma issued_nil: "issued [] = {Key0}"
    89 by (auto simp add: initk_def)
    90 
    91 lemmas issued_simps[code] = issued_nil issued.simps(2)
    92 
    93 
    94 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Set.member},
    95   @{const_name "issued"}, @{const_name "cards"}, @{const_name "isin"},
    96   @{const_name Collect}, @{const_name insert}]\<close>
    97 ML_val \<open>Core_Data.force_modes_and_compilations\<close>
    98 
    99 fun find_first :: "('a => 'b option) => 'a list => 'b option"
   100 where
   101   "find_first f [] = None"
   102 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
   103 
   104 axiomatization cps_of_set :: "'a set => ('a => term list option) => term list option"
   105 where cps_of_set_code [code]: "cps_of_set (set xs) f = find_first f xs"
   106 
   107 axiomatization pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
   108 where pos_cps_of_set_code [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
   109 
   110 axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
   111     => 'b list => 'a Quickcheck_Exhaustive.three_valued"
   112 where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
   113   and find_first'_Cons: "find_first' f (x # xs) =
   114     (case f (Quickcheck_Exhaustive.Known x) of
   115       Quickcheck_Exhaustive.No_value => find_first' f xs
   116     | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x
   117     | Quickcheck_Exhaustive.Unknown_value =>
   118         (case find_first' f xs of Quickcheck_Exhaustive.Value x =>
   119           Quickcheck_Exhaustive.Value x
   120         | _ => Quickcheck_Exhaustive.Unknown_value))"
   121 
   122 lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons
   123 
   124 axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
   125 where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
   126 
   127 setup \<open>
   128 let
   129   val Fun = Predicate_Compile_Aux.Fun
   130   val Input = Predicate_Compile_Aux.Input
   131   val Output = Predicate_Compile_Aux.Output
   132   val Bool = Predicate_Compile_Aux.Bool
   133   val oi = Fun (Output, Fun (Input, Bool))
   134   val ii = Fun (Input, Fun (Input, Bool))
   135   fun of_set compfuns (Type ("fun", [T, _])) =
   136     case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
   137       Type ("Quickcheck_Exhaustive.three_valued", _) => 
   138         Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
   139     | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
   140   fun member compfuns (U as Type ("fun", [T, _])) =
   141     (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
   142       (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
   143  
   144 in
   145   Core_Data.force_modes_and_compilations @{const_name Set.member}
   146     [(oi, (of_set, false)), (ii, (member, false))]
   147 end
   148 \<close>
   149 section \<open>Property\<close>
   150 
   151 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
   152 quickcheck[tester = exhaustive, size = 6, expect = counterexample]
   153 quickcheck[tester = smart_exhaustive, depth = 6, expect = counterexample]
   154 oops
   155 
   156 lemma
   157   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   158 quickcheck[smart_exhaustive, depth = 10, allow_function_inversion, expect = counterexample]
   159 oops
   160 
   161 section \<open>Refinement\<close>
   162 
   163 fun split_list
   164 where
   165   "split_list [] = [([], [])]"
   166 | "split_list (z # zs) = (([], z # zs) # [(z # xs', ys'). (xs', ys') <- split_list zs])"
   167 
   168 lemma split_list: "((xs, ys) \<in> set (split_list zs)) = (zs = xs @ ys)"
   169 apply (induct zs arbitrary: xs ys)
   170 apply fastforce
   171 apply (case_tac xs)
   172 apply auto
   173 done
   174 
   175 lemma [code]: "no_Check_in s r = list_all (%x. case x of Check_in g r' c => r \<noteq> r' | _ => True) s"
   176 unfolding no_Check_in_def list_all_iff
   177 apply auto
   178 apply (case_tac x)
   179 apply auto
   180 done
   181 
   182 lemma [code]: "feels_safe s r = list_ex (%(s3, s2, s1, g, c, c'). no_Check_in (s3 @ s2) r &
   183     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'])"
   184 unfolding feels_safe_def list_ex_iff
   185 by auto (metis split_list)+
   186 
   187 lemma
   188   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   189 (* quickcheck[exhaustive, size = 9, timeout = 2000] -- maybe possible with a lot of time *)
   190 quickcheck[narrowing, size = 7, expect = counterexample]
   191 oops
   192 
   193 end