src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa
permissions -rw-r--r--
more robust sorted_entries;
     1 theory Hotel_Example_Prolog
     2 imports
     3   Hotel_Example
     4   "HOL-Library.Predicate_Compile_Alternative_Defs"
     5   "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 \<open>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 = []})\<close>
    81 
    82 values_prolog 40 "{s. hotel s}"
    83 
    84 setup \<open>
    85   Context.theory_map
    86     (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    87 \<close>
    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 \<open>Manual setup to find the counterexample\<close>
    94 
    95 setup \<open>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 = []})\<close>
   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 \<open>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 = []})\<close>
   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 \<open>Using a global limit for limiting the execution\<close> 
   122 
   123 text \<open>A global depth limit of 10 does not suffice to find the counterexample.\<close>
   124 
   125 setup \<open>
   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 \<close>
   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 \<open>But a global depth limit of 11 does.\<close>
   141 
   142 setup \<open>
   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 \<close>
   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