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