src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 48891 c0eafbd55de3
child 62390 842917225d56
permissions -rw-r--r--
specialized specification: avoid trivial instances
bulwahn@40104
     1
theory Hotel_Example_Small_Generator
wenzelm@41413
     2
imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
bulwahn@40104
     3
begin
bulwahn@40104
     4
wenzelm@48891
     5
ML_file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
wenzelm@48891
     6
bulwahn@40104
     7
declare Let_def[code_pred_inline]
bulwahn@40104
     8
bulwahn@40137
     9
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
bulwahn@40137
    10
by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
bulwahn@40137
    11
bulwahn@40137
    12
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
bulwahn@40137
    13
by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
bulwahn@40137
    14
bulwahn@40104
    15
instantiation room :: small_lazy
bulwahn@40104
    16
begin
bulwahn@40104
    17
bulwahn@40104
    18
definition
bulwahn@40104
    19
  "small_lazy i = Lazy_Sequence.single Room0"
bulwahn@40104
    20
bulwahn@40104
    21
instance ..
bulwahn@40104
    22
bulwahn@40104
    23
end
bulwahn@40104
    24
bulwahn@40104
    25
instantiation key :: small_lazy
bulwahn@40104
    26
begin
bulwahn@40104
    27
bulwahn@40104
    28
definition
bulwahn@40104
    29
  "small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Key0) (Lazy_Sequence.append (Lazy_Sequence.single Key1) (Lazy_Sequence.append (Lazy_Sequence.single Key2) (Lazy_Sequence.single Key3)))"
bulwahn@40104
    30
bulwahn@40104
    31
instance ..
bulwahn@40104
    32
bulwahn@40104
    33
end
bulwahn@40104
    34
bulwahn@40104
    35
instantiation guest :: small_lazy
bulwahn@40104
    36
begin
bulwahn@40104
    37
bulwahn@40104
    38
definition
bulwahn@40104
    39
  "small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)"
bulwahn@40104
    40
bulwahn@40104
    41
instance ..
bulwahn@40104
    42
bulwahn@40104
    43
end
bulwahn@40104
    44
bulwahn@43888
    45
ML {* 
bulwahn@43888
    46
val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false);
bulwahn@43888
    47
val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false);
bulwahn@43888
    48
*}
bulwahn@40104
    49
bulwahn@43888
    50
setup {*
bulwahn@43888
    51
  Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14",
bulwahn@43888
    52
    (small_14_active, Predicate_Compile_Quickcheck.test_goals
bulwahn@43888
    53
      (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14))))
bulwahn@43888
    54
  #> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15",
bulwahn@43888
    55
    (small_15_active, Predicate_Compile_Quickcheck.test_goals
bulwahn@43888
    56
      (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15))))
bulwahn@43888
    57
*}
bulwahn@40104
    58
bulwahn@40104
    59
lemma
bulwahn@40104
    60
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
krauss@42291
    61
(*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample]*)
krauss@42397
    62
quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 2400.0, expect = counterexample]
bulwahn@40104
    63
oops
bulwahn@40104
    64
bulwahn@40104
    65
bulwahn@40104
    66
end