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