adding the hotel key card example in Quickcheck-Examples
authorbulwahn
Mon Jul 09 10:04:07 2012 +0200 (2012-07-09)
changeset 48222fcca68383808
parent 48221 e0ed7fab0d09
child 48223 b16d22bfad07
adding the hotel key card example in Quickcheck-Examples
src/HOL/IsaMakefile
src/HOL/Quickcheck_Examples/Hotel_Example.thy
src/HOL/Quickcheck_Examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Jul 09 09:47:59 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jul 09 10:04:07 2012 +0200
     1.3 @@ -1502,6 +1502,7 @@
     1.4  $(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL				\
     1.5    Quickcheck_Examples/Completeness.thy					\
     1.6    Quickcheck_Examples/Find_Unused_Assms_Examples.thy			\
     1.7 +  Quickcheck_Examples/Hotel_Example.thy					\
     1.8    Quickcheck_Examples/Quickcheck_Examples.thy				\
     1.9    Quickcheck_Examples/Quickcheck_Interfaces.thy				\
    1.10    Quickcheck_Examples/Quickcheck_Lattice_Examples.thy			\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon Jul 09 10:04:07 2012 +0200
     2.3 @@ -0,0 +1,193 @@
     2.4 +theory Hotel_Example
     2.5 +imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     2.6 +begin
     2.7 +
     2.8 +datatype guest = Guest0 | Guest1
     2.9 +datatype key = Key0 | Key1 | Key2 | Key3
    2.10 +datatype room = Room0
    2.11 +
    2.12 +type_synonym card = "key * key"
    2.13 +
    2.14 +datatype event =
    2.15 +   Check_in guest room card | Enter guest room card | Exit guest room
    2.16 +
    2.17 +definition initk :: "room \<Rightarrow> key"
    2.18 +  where "initk = (%r. Key0)"
    2.19 +
    2.20 +declare initk_def[code_pred_def, code]
    2.21 +
    2.22 +primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
    2.23 +where
    2.24 +  "owns [] r = None"
    2.25 +| "owns (e#s) r = (case e of
    2.26 +    Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
    2.27 +    Enter g r' c \<Rightarrow> owns s r |
    2.28 +    Exit g r' \<Rightarrow> owns s r)"
    2.29 +
    2.30 +primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
    2.31 +where
    2.32 +  "currk [] r = initk r"
    2.33 +| "currk (e#s) r = (let k = currk s r in
    2.34 +    case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
    2.35 +            | Enter g r' c \<Rightarrow> k
    2.36 +            | Exit g r \<Rightarrow> k)"
    2.37 +
    2.38 +primrec issued :: "event list \<Rightarrow> key set"
    2.39 +where
    2.40 +  "issued [] = range initk"
    2.41 +| "issued (e#s) = issued s \<union>
    2.42 +  (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
    2.43 +
    2.44 +primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
    2.45 +where
    2.46 +  "cards [] g = {}"
    2.47 +| "cards (e#s) g = (let C = cards s g in
    2.48 +                    case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
    2.49 +                                                else C
    2.50 +                            | Enter g r c \<Rightarrow> C
    2.51 +                            | Exit g r \<Rightarrow> C)"
    2.52 +
    2.53 +primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
    2.54 +where
    2.55 +  "roomk [] r = initk r"
    2.56 +| "roomk (e#s) r = (let k = roomk s r in
    2.57 +    case e of Check_in g r' c \<Rightarrow> k
    2.58 +            | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
    2.59 +            | Exit g r \<Rightarrow> k)"
    2.60 +
    2.61 +primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
    2.62 +where
    2.63 +  "isin [] r = {}"
    2.64 +| "isin (e#s) r = (let G = isin s r in
    2.65 +                 case e of Check_in g r c \<Rightarrow> G
    2.66 +                 | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
    2.67 +                 | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
    2.68 +
    2.69 +primrec hotel :: "event list \<Rightarrow> bool"
    2.70 +where
    2.71 +  "hotel []  = True"
    2.72 +| "hotel (e # s) = (hotel s & (case e of
    2.73 +  Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
    2.74 +  Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    2.75 +  Exit g r \<Rightarrow> g : isin s r))"
    2.76 +
    2.77 +definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
    2.78 +[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
    2.79 +
    2.80 +definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
    2.81 +where
    2.82 +  "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
    2.83 +   s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
    2.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 = {})"
    2.85 +
    2.86 +
    2.87 +section {* Some setup *}
    2.88 +
    2.89 +lemma issued_nil: "issued [] = {Key0}"
    2.90 +by (auto simp add: initk_def)
    2.91 +
    2.92 +lemmas issued_simps[code] = issued_nil issued.simps(2)
    2.93 +
    2.94 +
    2.95 +setup {*  Predicate_Compile_Data.ignore_consts [@{const_name Set.member},
    2.96 +  @{const_name "issued"}, @{const_name "cards"}, @{const_name "isin"},
    2.97 +  @{const_name Collect}, @{const_name insert}] *}
    2.98 +ML {* Core_Data.force_modes_and_compilations *}
    2.99 +
   2.100 +fun find_first :: "('a => 'b option) => 'a list => 'b option"
   2.101 +where
   2.102 +  "find_first f [] = None"
   2.103 +| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
   2.104 +
   2.105 +consts cps_of_set :: "'a set => ('a => term list option) => term list option"
   2.106 +
   2.107 +lemma
   2.108 +  [code]: "cps_of_set (set xs) f = find_first f xs"
   2.109 +sorry
   2.110 +
   2.111 +consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option"
   2.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"
   2.113 +
   2.114 +lemma
   2.115 +  [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
   2.116 +sorry
   2.117 +
   2.118 +consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
   2.119 +    => 'b list => 'a Quickcheck_Exhaustive.three_valued"
   2.120 +
   2.121 +lemma [code]:
   2.122 +  "find_first' f [] = Quickcheck_Exhaustive.No_value"
   2.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))"
   2.124 +sorry
   2.125 +
   2.126 +lemma
   2.127 +  [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
   2.128 +sorry
   2.129 +
   2.130 +setup {*
   2.131 +let
   2.132 +  val Fun = Predicate_Compile_Aux.Fun
   2.133 +  val Input = Predicate_Compile_Aux.Input
   2.134 +  val Output = Predicate_Compile_Aux.Output
   2.135 +  val Bool = Predicate_Compile_Aux.Bool
   2.136 +  val oi = Fun (Output, Fun (Input, Bool))
   2.137 +  val ii = Fun (Input, Fun (Input, Bool))
   2.138 +  fun of_set compfuns (Type ("fun", [T, _])) =
   2.139 +    case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
   2.140 +      Type ("Quickcheck_Exhaustive.three_valued", _) => 
   2.141 +        Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
   2.142 +    | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
   2.143 +  fun member compfuns (U as Type ("fun", [T, _])) =
   2.144 +    (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
   2.145 +      (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
   2.146 + 
   2.147 +in
   2.148 +  Core_Data.force_modes_and_compilations @{const_name Set.member}
   2.149 +    [(oi, (of_set, false)), (ii, (member, false))]
   2.150 +end
   2.151 +*}
   2.152 +section {* Property *}
   2.153 +
   2.154 +lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
   2.155 +quickcheck[tester = exhaustive, size = 6, expect = counterexample]
   2.156 +quickcheck[tester = smart_exhaustive, depth = 6, expect = counterexample]
   2.157 +oops
   2.158 +
   2.159 +lemma
   2.160 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   2.161 +quickcheck[smart_exhaustive, depth = 10, allow_function_inversion, expect = counterexample]
   2.162 +oops
   2.163 +
   2.164 +section {* Refinement *}
   2.165 +
   2.166 +fun split_list
   2.167 +where
   2.168 +  "split_list [] = [([], [])]"
   2.169 +| "split_list (z # zs) = (([], z # zs) # [(z # xs', ys'). (xs', ys') <- split_list zs])"
   2.170 +
   2.171 +lemma split_list: "((xs, ys) \<in> set (split_list zs)) = (zs = xs @ ys)"
   2.172 +apply (induct zs arbitrary: xs ys)
   2.173 +apply fastforce
   2.174 +apply (case_tac xs)
   2.175 +apply auto
   2.176 +done
   2.177 +
   2.178 +lemma [code]: "no_Check_in s r = list_all (%x. case x of Check_in g r' c => r \<noteq> r' | _ => True) s"
   2.179 +unfolding no_Check_in_def list_all_iff
   2.180 +apply auto
   2.181 +apply (case_tac x)
   2.182 +apply auto
   2.183 +done
   2.184 +
   2.185 +lemma [code]: "feels_safe s r = list_ex (%(s3, s2, s1, g, c, c'). no_Check_in (s3 @ s2) r &
   2.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'])"
   2.187 +unfolding feels_safe_def list_ex_iff
   2.188 +by auto (metis split_list)+
   2.189 +
   2.190 +lemma
   2.191 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   2.192 +(* quickcheck[exhaustive, size = 9, timeout = 2000] -- maybe possible with a lot of time *)
   2.193 +quickcheck[narrowing, size = 7, expect = counterexample]
   2.194 +oops
   2.195 +
   2.196 +ebd
   2.197 \ No newline at end of file
     3.1 --- a/src/HOL/Quickcheck_Examples/ROOT.ML	Mon Jul 09 09:47:59 2012 +0200
     3.2 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML	Mon Jul 09 10:04:07 2012 +0200
     3.3 @@ -3,7 +3,8 @@
     3.4    "Quickcheck_Examples",
     3.5    "Quickcheck_Lattice_Examples",
     3.6    "Completeness",
     3.7 -  "Quickcheck_Interfaces"
     3.8 +  "Quickcheck_Interfaces",
     3.9 +  "Hotel_Example"
    3.10  ];
    3.11  
    3.12  if getenv "ISABELLE_GHC" = "" then ()