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