src/HOL/Quickcheck_Examples/Hotel_Example.thy
changeset 48222 fcca68383808
child 48255 968602739b54
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon Jul 09 10:04:07 2012 +0200
     1.3 @@ -0,0 +1,193 @@
     1.4 +theory Hotel_Example
     1.5 +imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     1.6 +begin
     1.7 +
     1.8 +datatype guest = Guest0 | Guest1
     1.9 +datatype key = Key0 | Key1 | Key2 | Key3
    1.10 +datatype room = Room0
    1.11 +
    1.12 +type_synonym card = "key * key"
    1.13 +
    1.14 +datatype event =
    1.15 +   Check_in guest room card | Enter guest room card | Exit guest room
    1.16 +
    1.17 +definition initk :: "room \<Rightarrow> key"
    1.18 +  where "initk = (%r. Key0)"
    1.19 +
    1.20 +declare initk_def[code_pred_def, code]
    1.21 +
    1.22 +primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
    1.23 +where
    1.24 +  "owns [] r = None"
    1.25 +| "owns (e#s) r = (case e of
    1.26 +    Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
    1.27 +    Enter g r' c \<Rightarrow> owns s r |
    1.28 +    Exit g r' \<Rightarrow> owns s r)"
    1.29 +
    1.30 +primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
    1.31 +where
    1.32 +  "currk [] r = initk r"
    1.33 +| "currk (e#s) r = (let k = currk s r in
    1.34 +    case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
    1.35 +            | Enter g r' c \<Rightarrow> k
    1.36 +            | Exit g r \<Rightarrow> k)"
    1.37 +
    1.38 +primrec issued :: "event list \<Rightarrow> key set"
    1.39 +where
    1.40 +  "issued [] = range initk"
    1.41 +| "issued (e#s) = issued s \<union>
    1.42 +  (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
    1.43 +
    1.44 +primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
    1.45 +where
    1.46 +  "cards [] g = {}"
    1.47 +| "cards (e#s) g = (let C = cards s g in
    1.48 +                    case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
    1.49 +                                                else C
    1.50 +                            | Enter g r c \<Rightarrow> C
    1.51 +                            | Exit g r \<Rightarrow> C)"
    1.52 +
    1.53 +primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
    1.54 +where
    1.55 +  "roomk [] r = initk r"
    1.56 +| "roomk (e#s) r = (let k = roomk s r in
    1.57 +    case e of Check_in g r' c \<Rightarrow> k
    1.58 +            | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
    1.59 +            | Exit g r \<Rightarrow> k)"
    1.60 +
    1.61 +primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
    1.62 +where
    1.63 +  "isin [] r = {}"
    1.64 +| "isin (e#s) r = (let G = isin s r in
    1.65 +                 case e of Check_in g r c \<Rightarrow> G
    1.66 +                 | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
    1.67 +                 | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
    1.68 +
    1.69 +primrec hotel :: "event list \<Rightarrow> bool"
    1.70 +where
    1.71 +  "hotel []  = True"
    1.72 +| "hotel (e # s) = (hotel s & (case e of
    1.73 +  Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
    1.74 +  Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    1.75 +  Exit g r \<Rightarrow> g : isin s r))"
    1.76 +
    1.77 +definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
    1.78 +[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
    1.79 +
    1.80 +definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
    1.81 +where
    1.82 +  "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
    1.83 +   s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
    1.84 +   no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
    1.85 +
    1.86 +
    1.87 +section {* Some setup *}
    1.88 +
    1.89 +lemma issued_nil: "issued [] = {Key0}"
    1.90 +by (auto simp add: initk_def)
    1.91 +
    1.92 +lemmas issued_simps[code] = issued_nil issued.simps(2)
    1.93 +
    1.94 +
    1.95 +setup {*  Predicate_Compile_Data.ignore_consts [@{const_name Set.member},
    1.96 +  @{const_name "issued"}, @{const_name "cards"}, @{const_name "isin"},
    1.97 +  @{const_name Collect}, @{const_name insert}] *}
    1.98 +ML {* Core_Data.force_modes_and_compilations *}
    1.99 +
   1.100 +fun find_first :: "('a => 'b option) => 'a list => 'b option"
   1.101 +where
   1.102 +  "find_first f [] = None"
   1.103 +| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
   1.104 +
   1.105 +consts cps_of_set :: "'a set => ('a => term list option) => term list option"
   1.106 +
   1.107 +lemma
   1.108 +  [code]: "cps_of_set (set xs) f = find_first f xs"
   1.109 +sorry
   1.110 +
   1.111 +consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option"
   1.112 +consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued"
   1.113 +
   1.114 +lemma
   1.115 +  [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
   1.116 +sorry
   1.117 +
   1.118 +consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
   1.119 +    => 'b list => 'a Quickcheck_Exhaustive.three_valued"
   1.120 +
   1.121 +lemma [code]:
   1.122 +  "find_first' f [] = Quickcheck_Exhaustive.No_value"
   1.123 +  "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))"
   1.124 +sorry
   1.125 +
   1.126 +lemma
   1.127 +  [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
   1.128 +sorry
   1.129 +
   1.130 +setup {*
   1.131 +let
   1.132 +  val Fun = Predicate_Compile_Aux.Fun
   1.133 +  val Input = Predicate_Compile_Aux.Input
   1.134 +  val Output = Predicate_Compile_Aux.Output
   1.135 +  val Bool = Predicate_Compile_Aux.Bool
   1.136 +  val oi = Fun (Output, Fun (Input, Bool))
   1.137 +  val ii = Fun (Input, Fun (Input, Bool))
   1.138 +  fun of_set compfuns (Type ("fun", [T, _])) =
   1.139 +    case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
   1.140 +      Type ("Quickcheck_Exhaustive.three_valued", _) => 
   1.141 +        Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
   1.142 +    | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
   1.143 +  fun member compfuns (U as Type ("fun", [T, _])) =
   1.144 +    (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
   1.145 +      (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
   1.146 + 
   1.147 +in
   1.148 +  Core_Data.force_modes_and_compilations @{const_name Set.member}
   1.149 +    [(oi, (of_set, false)), (ii, (member, false))]
   1.150 +end
   1.151 +*}
   1.152 +section {* Property *}
   1.153 +
   1.154 +lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
   1.155 +quickcheck[tester = exhaustive, size = 6, expect = counterexample]
   1.156 +quickcheck[tester = smart_exhaustive, depth = 6, expect = counterexample]
   1.157 +oops
   1.158 +
   1.159 +lemma
   1.160 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   1.161 +quickcheck[smart_exhaustive, depth = 10, allow_function_inversion, expect = counterexample]
   1.162 +oops
   1.163 +
   1.164 +section {* Refinement *}
   1.165 +
   1.166 +fun split_list
   1.167 +where
   1.168 +  "split_list [] = [([], [])]"
   1.169 +| "split_list (z # zs) = (([], z # zs) # [(z # xs', ys'). (xs', ys') <- split_list zs])"
   1.170 +
   1.171 +lemma split_list: "((xs, ys) \<in> set (split_list zs)) = (zs = xs @ ys)"
   1.172 +apply (induct zs arbitrary: xs ys)
   1.173 +apply fastforce
   1.174 +apply (case_tac xs)
   1.175 +apply auto
   1.176 +done
   1.177 +
   1.178 +lemma [code]: "no_Check_in s r = list_all (%x. case x of Check_in g r' c => r \<noteq> r' | _ => True) s"
   1.179 +unfolding no_Check_in_def list_all_iff
   1.180 +apply auto
   1.181 +apply (case_tac x)
   1.182 +apply auto
   1.183 +done
   1.184 +
   1.185 +lemma [code]: "feels_safe s r = list_ex (%(s3, s2, s1, g, c, c'). no_Check_in (s3 @ s2) r &
   1.186 +    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'])"
   1.187 +unfolding feels_safe_def list_ex_iff
   1.188 +by auto (metis split_list)+
   1.189 +
   1.190 +lemma
   1.191 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   1.192 +(* quickcheck[exhaustive, size = 9, timeout = 2000] -- maybe possible with a lot of time *)
   1.193 +quickcheck[narrowing, size = 7, expect = counterexample]
   1.194 +oops
   1.195 +
   1.196 +ebd
   1.197 \ No newline at end of file