src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 53015 a1119cf551e8
child 55447 aa41ecbdc205
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
bulwahn@40104
     1
theory Hotel_Example_Prolog
wenzelm@41956
     2
imports
wenzelm@41956
     3
  Hotel_Example
wenzelm@41956
     4
  "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
wenzelm@41956
     5
  "~~/src/HOL/Library/Code_Prolog"
bulwahn@40104
     6
begin
bulwahn@40104
     7
bulwahn@40104
     8
declare Let_def[code_pred_inline]
haftmann@45970
     9
(*
haftmann@45970
    10
thm hotel_def
bulwahn@40104
    11
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
bulwahn@40104
    12
by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
bulwahn@40104
    13
bulwahn@40104
    14
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
bulwahn@40104
    15
by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
haftmann@45970
    16
*)
haftmann@45970
    17
haftmann@45970
    18
definition issuedp :: "event list => key => bool"
haftmann@45970
    19
where
haftmann@45970
    20
  "issuedp evs k = (k \<in> issued evs)"
haftmann@45970
    21
haftmann@45970
    22
lemma [code_pred_def]:
haftmann@45970
    23
  "issuedp [] Key0 = True"
haftmann@45970
    24
  "issuedp (e # s) k = (issuedp s k \<or> (case e of Check_in g r (k1, k2) => k = k2 | _ => False))"
haftmann@45970
    25
unfolding issuedp_def issued.simps initk_def
haftmann@45970
    26
by (auto split: event.split)
haftmann@45970
    27
haftmann@45970
    28
definition cardsp
haftmann@45970
    29
where
haftmann@45970
    30
 "cardsp s g k = (k \<in> cards s g)"
haftmann@45970
    31
haftmann@45970
    32
lemma [code_pred_def]:
haftmann@45970
    33
  "cardsp [] g k = False"
wenzelm@52666
    34
  "cardsp (e # s) g k =
wenzelm@52666
    35
    (let C = cardsp s g
wenzelm@52666
    36
     in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
wenzelm@46905
    37
unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
haftmann@45970
    38
haftmann@45970
    39
definition
haftmann@45970
    40
  "isinp evs r g = (g \<in> isin evs r)"
haftmann@45970
    41
haftmann@45970
    42
lemma [code_pred_def]:
haftmann@45970
    43
  "isinp [] r g = False"
haftmann@45970
    44
  "isinp (e # s) r g =
haftmann@45970
    45
  (let G = isinp s r
haftmann@45970
    46
   in case e of Check_in g' r c => G g
haftmann@45970
    47
    | Enter g' r' c => if r' = r then g = g' \<or> G g else G g
haftmann@45970
    48
    | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)"
wenzelm@46905
    49
unfolding isinp_def [abs_def] isin.simps by (auto simp add: Let_def split: event.split)
haftmann@45970
    50
haftmann@45970
    51
declare hotel.simps(1)[code_pred_def]
haftmann@45970
    52
lemma [code_pred_def]:
haftmann@45970
    53
"hotel (e # s) =
haftmann@45970
    54
  (hotel s & (case e of Check_in g r (k, k') => k = currk s r & \<not> issuedp s k'
haftmann@45970
    55
  | Enter g r (k, k') => cardsp s g (k, k') & (roomk s r = k \<or> roomk s r = k')
haftmann@45970
    56
  | Exit g r => isinp s r g))"
haftmann@45970
    57
unfolding hotel.simps issuedp_def cardsp_def isinp_def
haftmann@45970
    58
by (auto split: event.split)
haftmann@45970
    59
haftmann@45970
    60
declare List.member_rec[code_pred_def]
haftmann@45970
    61
haftmann@45970
    62
lemma [code_pred_def]: "no_Check_in s r = (~ (EX g c. List.member s (Check_in g r c)))"
haftmann@45970
    63
unfolding no_Check_in_def member_def by auto
haftmann@45970
    64
haftmann@45970
    65
lemma [code_pred_def]: "feels_safe s r =
wenzelm@53015
    66
(EX s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
haftmann@45970
    67
    s =
wenzelm@53015
    68
    s\<^sub>3 @
wenzelm@53015
    69
    [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 &
wenzelm@53015
    70
    no_Check_in (s\<^sub>3 @ s\<^sub>2) r &
wenzelm@53015
    71
    (\<not> (\<exists> g'. isinp (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r g')))"
haftmann@45970
    72
unfolding feels_safe_def isinp_def by auto
bulwahn@40104
    73
bulwahn@40104
    74
setup {* Code_Prolog.map_code_options (K
bulwahn@40104
    75
  {ensure_groundness = true,
bulwahn@40104
    76
  limit_globally = NONE,
bulwahn@40104
    77
  limited_types = [],
bulwahn@40104
    78
  limited_predicates = [],
bulwahn@40104
    79
  replacing = [],
bulwahn@40104
    80
  manual_reorder = []}) *}
bulwahn@40104
    81
bulwahn@40104
    82
values 40 "{s. hotel s}"
bulwahn@40104
    83
wenzelm@52666
    84
setup {*
wenzelm@52666
    85
  Context.theory_map
wenzelm@52666
    86
    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
wenzelm@52666
    87
*}
bulwahn@40104
    88
haftmann@45970
    89
lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
bulwahn@40924
    90
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
bulwahn@40104
    91
oops
bulwahn@40104
    92
bulwahn@40104
    93
section {* Manual setup to find the counterexample *}
bulwahn@40104
    94
bulwahn@40104
    95
setup {* Code_Prolog.map_code_options (K 
bulwahn@40104
    96
  {ensure_groundness = true,
bulwahn@40104
    97
   limit_globally = NONE,
bulwahn@40104
    98
   limited_types = [],
bulwahn@40104
    99
   limited_predicates = [(["hotel"], 4)],
bulwahn@40104
   100
   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
bulwahn@40104
   101
   manual_reorder = []}) *}
bulwahn@40104
   102
bulwahn@40104
   103
lemma
haftmann@45970
   104
  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
bulwahn@40924
   105
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
bulwahn@40104
   106
oops
bulwahn@40104
   107
bulwahn@40104
   108
setup {* Code_Prolog.map_code_options (K 
bulwahn@40104
   109
  {ensure_groundness = true,
bulwahn@40104
   110
   limit_globally = NONE,
bulwahn@40104
   111
   limited_types = [],
bulwahn@40104
   112
   limited_predicates = [(["hotel"], 5)],
bulwahn@40104
   113
   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
bulwahn@40104
   114
   manual_reorder = []}) *}
bulwahn@40104
   115
bulwahn@40104
   116
lemma
haftmann@45970
   117
  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
bulwahn@40924
   118
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
bulwahn@40104
   119
oops
bulwahn@40104
   120
bulwahn@40104
   121
section {* Using a global limit for limiting the execution *} 
bulwahn@40104
   122
haftmann@45970
   123
text {* A global depth limit of 10 does not suffice to find the counterexample. *}
bulwahn@40104
   124
bulwahn@40104
   125
setup {*
bulwahn@40104
   126
  Code_Prolog.map_code_options (K
bulwahn@40104
   127
  {ensure_groundness = true,
haftmann@45970
   128
  limit_globally = SOME 10,
bulwahn@40104
   129
  limited_types = [],
bulwahn@40104
   130
  limited_predicates = [],
bulwahn@40104
   131
  replacing = [],
bulwahn@40104
   132
  manual_reorder = []})
bulwahn@40104
   133
*}
bulwahn@40104
   134
bulwahn@40104
   135
lemma
haftmann@45970
   136
  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
bulwahn@40924
   137
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
bulwahn@40104
   138
oops
bulwahn@40104
   139
haftmann@45970
   140
text {* But a global depth limit of 11 does. *}
bulwahn@40104
   141
bulwahn@40104
   142
setup {*
bulwahn@40104
   143
  Code_Prolog.map_code_options (K
bulwahn@40104
   144
  {ensure_groundness = true,
haftmann@45970
   145
  limit_globally = SOME 11,
bulwahn@40104
   146
  limited_types = [],
bulwahn@40104
   147
  limited_predicates = [],
bulwahn@40104
   148
  replacing = [],
bulwahn@40104
   149
  manual_reorder = []})
bulwahn@40104
   150
*}
bulwahn@40104
   151
bulwahn@40104
   152
lemma
haftmann@45970
   153
  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
bulwahn@40924
   154
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
bulwahn@40104
   155
oops
bulwahn@40104
   156
bulwahn@40104
   157
end