src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
author bulwahn
Thu Sep 30 10:48:12 2010 +0200 (2010-09-30)
changeset 39799 fdbea66eae4b
parent 39463 7ce0ed8dc4d6
child 40104 82873a6f2b81
permissions -rw-r--r--
finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)
bulwahn@38730
     1
theory Hotel_Example
bulwahn@38730
     2
imports Predicate_Compile_Alternative_Defs Code_Prolog
bulwahn@38730
     3
begin
bulwahn@38730
     4
bulwahn@38730
     5
datatype guest = Guest0 | Guest1
bulwahn@38730
     6
datatype key = Key0 | Key1 | Key2 | Key3
bulwahn@38730
     7
datatype room = Room0
bulwahn@38730
     8
bulwahn@38730
     9
types card = "key * key"
bulwahn@38730
    10
bulwahn@38730
    11
datatype event =
bulwahn@38730
    12
   Check_in guest room card | Enter guest room card | Exit guest room
bulwahn@38730
    13
bulwahn@38730
    14
definition initk :: "room \<Rightarrow> key"
bulwahn@38730
    15
  where "initk = (%r. Key0)"
bulwahn@38730
    16
bulwahn@38730
    17
declare initk_def[code_pred_def, code]
bulwahn@38730
    18
bulwahn@38730
    19
primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
bulwahn@38730
    20
where
bulwahn@38730
    21
  "owns [] r = None"
bulwahn@38730
    22
| "owns (e#s) r = (case e of
bulwahn@38730
    23
    Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
bulwahn@38730
    24
    Enter g r' c \<Rightarrow> owns s r |
bulwahn@38730
    25
    Exit g r' \<Rightarrow> owns s r)"
bulwahn@38730
    26
bulwahn@38730
    27
primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
bulwahn@38730
    28
where
bulwahn@38730
    29
  "currk [] r = initk r"
bulwahn@38730
    30
| "currk (e#s) r = (let k = currk s r in
bulwahn@38730
    31
    case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
bulwahn@38730
    32
            | Enter g r' c \<Rightarrow> k
bulwahn@38730
    33
            | Exit g r \<Rightarrow> k)"
bulwahn@38730
    34
bulwahn@38730
    35
primrec issued :: "event list \<Rightarrow> key set"
bulwahn@38730
    36
where
bulwahn@38730
    37
  "issued [] = range initk"
bulwahn@38730
    38
| "issued (e#s) = issued s \<union>
bulwahn@38730
    39
  (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
bulwahn@38730
    40
bulwahn@38730
    41
primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
bulwahn@38730
    42
where
bulwahn@38730
    43
  "cards [] g = {}"
bulwahn@38730
    44
| "cards (e#s) g = (let C = cards s g in
bulwahn@38730
    45
                    case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
bulwahn@38730
    46
                                                else C
bulwahn@38730
    47
                            | Enter g r c \<Rightarrow> C
bulwahn@38730
    48
                            | Exit g r \<Rightarrow> C)"
bulwahn@38730
    49
bulwahn@38730
    50
primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
bulwahn@38730
    51
where
bulwahn@38730
    52
  "roomk [] r = initk r"
bulwahn@38730
    53
| "roomk (e#s) r = (let k = roomk s r in
bulwahn@38730
    54
    case e of Check_in g r' c \<Rightarrow> k
bulwahn@38730
    55
            | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
bulwahn@38730
    56
            | Exit g r \<Rightarrow> k)"
bulwahn@38730
    57
bulwahn@38730
    58
primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
bulwahn@38730
    59
where
bulwahn@38730
    60
  "isin [] r = {}"
bulwahn@38730
    61
| "isin (e#s) r = (let G = isin s r in
bulwahn@38730
    62
                 case e of Check_in g r c \<Rightarrow> G
bulwahn@38730
    63
                 | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
bulwahn@38730
    64
                 | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
bulwahn@38730
    65
bulwahn@38730
    66
primrec hotel :: "event list \<Rightarrow> bool"
bulwahn@38730
    67
where
bulwahn@38730
    68
  "hotel []  = True"
bulwahn@38730
    69
| "hotel (e # s) = (hotel s & (case e of
bulwahn@38730
    70
  Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
bulwahn@38730
    71
  Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
bulwahn@38734
    72
  Exit g r \<Rightarrow> g : isin s r))"
bulwahn@38730
    73
bulwahn@38730
    74
lemma issued_nil: "issued [] = {Key0}"
bulwahn@38730
    75
by (auto simp add: initk_def)
bulwahn@38730
    76
bulwahn@38730
    77
lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
bulwahn@38730
    78
bulwahn@38730
    79
declare Let_def[code_pred_inline]
bulwahn@38730
    80
bulwahn@38730
    81
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
nipkow@39302
    82
by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
bulwahn@38730
    83
bulwahn@38730
    84
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
nipkow@39302
    85
by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
bulwahn@38730
    86
bulwahn@38950
    87
setup {* Code_Prolog.map_code_options (K
bulwahn@38949
    88
  {ensure_groundness = true,
bulwahn@39799
    89
  limit_globally = NONE,
bulwahn@38949
    90
  limited_types = [],
bulwahn@38949
    91
  limited_predicates = [],
bulwahn@38949
    92
  replacing = [],
bulwahn@39463
    93
  manual_reorder = []}) *}
bulwahn@38730
    94
bulwahn@38734
    95
values 40 "{s. hotel s}"
bulwahn@38730
    96
bulwahn@38731
    97
bulwahn@39463
    98
setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
bulwahn@38733
    99
bulwahn@38733
   100
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
bulwahn@39799
   101
(*quickcheck[generator = code, iterations = 100000, report]*)
bulwahn@38949
   102
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
bulwahn@38733
   103
oops
bulwahn@38733
   104
bulwahn@38731
   105
bulwahn@38953
   106
definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
bulwahn@38953
   107
[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
bulwahn@38953
   108
bulwahn@38953
   109
bulwahn@38953
   110
definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
bulwahn@38953
   111
where
bulwahn@38953
   112
  "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
bulwahn@38953
   113
   s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
bulwahn@38953
   114
   no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
bulwahn@38953
   115
bulwahn@39799
   116
section {* Manual setup to find the counterexample *}
bulwahn@39799
   117
bulwahn@38953
   118
setup {* Code_Prolog.map_code_options (K 
bulwahn@38953
   119
  {ensure_groundness = true,
bulwahn@39799
   120
   limit_globally = NONE,
bulwahn@39799
   121
   limited_types = [],
bulwahn@39799
   122
   limited_predicates = [(["hotel"], 4)],
bulwahn@39799
   123
   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
bulwahn@39799
   124
   manual_reorder = []}) *}
bulwahn@39799
   125
bulwahn@39799
   126
lemma
bulwahn@39799
   127
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
bulwahn@39799
   128
quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
bulwahn@39799
   129
oops
bulwahn@39799
   130
bulwahn@39799
   131
setup {* Code_Prolog.map_code_options (K 
bulwahn@39799
   132
  {ensure_groundness = true,
bulwahn@39799
   133
   limit_globally = NONE,
bulwahn@38953
   134
   limited_types = [],
bulwahn@38963
   135
   limited_predicates = [(["hotel"], 5)],
bulwahn@38953
   136
   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
bulwahn@39463
   137
   manual_reorder = []}) *}
bulwahn@38953
   138
bulwahn@38953
   139
lemma
bulwahn@38954
   140
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
bulwahn@38954
   141
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
bulwahn@38953
   142
oops
bulwahn@38953
   143
bulwahn@39799
   144
section {* Simulating a global depth limit manually by limiting all predicates *}
bulwahn@39799
   145
bulwahn@39799
   146
setup {*
bulwahn@39799
   147
  Code_Prolog.map_code_options (K
bulwahn@39799
   148
  {ensure_groundness = true,
bulwahn@39799
   149
  limit_globally = NONE,
bulwahn@39799
   150
  limited_types = [],
bulwahn@39799
   151
  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
bulwahn@39799
   152
    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
bulwahn@39799
   153
  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
bulwahn@39799
   154
  manual_reorder = []})
bulwahn@39799
   155
*}
bulwahn@39799
   156
bulwahn@39799
   157
lemma
bulwahn@39799
   158
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
bulwahn@39799
   159
quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
bulwahn@39799
   160
oops
bulwahn@39799
   161
bulwahn@39799
   162
bulwahn@39799
   163
setup {*
bulwahn@39799
   164
  Code_Prolog.map_code_options (K
bulwahn@39799
   165
  {ensure_groundness = true,
bulwahn@39799
   166
  limit_globally = NONE,
bulwahn@39799
   167
  limited_types = [],
bulwahn@39799
   168
  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
bulwahn@39799
   169
    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
bulwahn@39799
   170
  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
bulwahn@39799
   171
  manual_reorder = []})
bulwahn@39799
   172
*}
bulwahn@39799
   173
bulwahn@39799
   174
lemma
bulwahn@39799
   175
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
bulwahn@39799
   176
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
bulwahn@39799
   177
oops
bulwahn@39799
   178
bulwahn@39799
   179
section {* Using a global limit for limiting the execution *} 
bulwahn@39799
   180
bulwahn@39799
   181
text {* A global depth limit of 13 does not suffice to find the counterexample. *}
bulwahn@39799
   182
bulwahn@39799
   183
setup {*
bulwahn@39799
   184
  Code_Prolog.map_code_options (K
bulwahn@39799
   185
  {ensure_groundness = true,
bulwahn@39799
   186
  limit_globally = SOME 13,
bulwahn@39799
   187
  limited_types = [],
bulwahn@39799
   188
  limited_predicates = [],
bulwahn@39799
   189
  replacing = [],
bulwahn@39799
   190
  manual_reorder = []})
bulwahn@39799
   191
*}
bulwahn@39799
   192
bulwahn@39799
   193
lemma
bulwahn@39799
   194
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
bulwahn@39799
   195
quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
bulwahn@39799
   196
oops
bulwahn@39799
   197
bulwahn@39799
   198
text {* But a global depth limit of 14 does. *}
bulwahn@39799
   199
bulwahn@39799
   200
setup {*
bulwahn@39799
   201
  Code_Prolog.map_code_options (K
bulwahn@39799
   202
  {ensure_groundness = true,
bulwahn@39799
   203
  limit_globally = SOME 14,
bulwahn@39799
   204
  limited_types = [],
bulwahn@39799
   205
  limited_predicates = [],
bulwahn@39799
   206
  replacing = [],
bulwahn@39799
   207
  manual_reorder = []})
bulwahn@39799
   208
*}
bulwahn@39799
   209
bulwahn@39799
   210
lemma
bulwahn@39799
   211
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
bulwahn@39799
   212
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
bulwahn@39799
   213
oops
bulwahn@39799
   214
bulwahn@38730
   215
end