src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40924 a9be7f26b4e6
child 41413 64cd30d6b0b8
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 theory Hotel_Example_Prolog
     2 imports Hotel_Example Predicate_Compile_Alternative_Defs Code_Prolog
     3 begin
     4 
     5 declare Let_def[code_pred_inline]
     6 
     7 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
     8 by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
     9 
    10 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    11 by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    12 
    13 setup {* Code_Prolog.map_code_options (K
    14   {ensure_groundness = true,
    15   limit_globally = NONE,
    16   limited_types = [],
    17   limited_predicates = [],
    18   replacing = [],
    19   manual_reorder = []}) *}
    20 
    21 values 40 "{s. hotel s}"
    22 
    23 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    24 
    25 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    26 quickcheck[tester = random, iterations = 10000, report]
    27 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
    28 oops
    29 
    30 section {* Manual setup to find the counterexample *}
    31 
    32 setup {* Code_Prolog.map_code_options (K 
    33   {ensure_groundness = true,
    34    limit_globally = NONE,
    35    limited_types = [],
    36    limited_predicates = [(["hotel"], 4)],
    37    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    38    manual_reorder = []}) *}
    39 
    40 lemma
    41   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    42 quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
    43 oops
    44 
    45 setup {* Code_Prolog.map_code_options (K 
    46   {ensure_groundness = true,
    47    limit_globally = NONE,
    48    limited_types = [],
    49    limited_predicates = [(["hotel"], 5)],
    50    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    51    manual_reorder = []}) *}
    52 
    53 lemma
    54   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    55 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
    56 oops
    57 
    58 section {* Simulating a global depth limit manually by limiting all predicates *}
    59 
    60 setup {*
    61   Code_Prolog.map_code_options (K
    62   {ensure_groundness = true,
    63   limit_globally = NONE,
    64   limited_types = [],
    65   limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
    66     "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
    67   replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
    68   manual_reorder = []})
    69 *}
    70 
    71 lemma
    72   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    73 quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
    74 oops
    75 
    76 setup {*
    77   Code_Prolog.map_code_options (K
    78   {ensure_groundness = true,
    79   limit_globally = NONE,
    80   limited_types = [],
    81   limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
    82     "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
    83   replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
    84   manual_reorder = []})
    85 *}
    86 
    87 lemma
    88   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    89 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
    90 oops
    91 
    92 section {* Using a global limit for limiting the execution *} 
    93 
    94 text {* A global depth limit of 13 does not suffice to find the counterexample. *}
    95 
    96 setup {*
    97   Code_Prolog.map_code_options (K
    98   {ensure_groundness = true,
    99   limit_globally = SOME 13,
   100   limited_types = [],
   101   limited_predicates = [],
   102   replacing = [],
   103   manual_reorder = []})
   104 *}
   105 
   106 lemma
   107   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   108 quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
   109 oops
   110 
   111 text {* But a global depth limit of 14 does. *}
   112 
   113 setup {*
   114   Code_Prolog.map_code_options (K
   115   {ensure_groundness = true,
   116   limit_globally = SOME 14,
   117   limited_types = [],
   118   limited_predicates = [],
   119   replacing = [],
   120   manual_reorder = []})
   121 *}
   122 
   123 lemma
   124   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   125 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
   126 oops
   127 
   128 end