src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
author bulwahn
Mon Oct 25 21:17:12 2010 +0200 (2010-10-25)
changeset 40137 9eabcb1bfe50
parent 40104 82873a6f2b81
child 40658 5ccfc3ee7fe6
permissions -rw-r--r--
changing test parameters in examples to get to a result within the global timelimit
bulwahn@40104
     1
theory Hotel_Example_Small_Generator
bulwahn@40104
     2
imports Hotel_Example Predicate_Compile_Alternative_Defs
bulwahn@40104
     3
uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
bulwahn@40104
     4
begin
bulwahn@40104
     5
bulwahn@40104
     6
declare Let_def[code_pred_inline]
bulwahn@40104
     7
bulwahn@40137
     8
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
bulwahn@40137
     9
by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
bulwahn@40137
    10
bulwahn@40137
    11
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
bulwahn@40137
    12
by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
bulwahn@40137
    13
bulwahn@40104
    14
instantiation room :: small_lazy
bulwahn@40104
    15
begin
bulwahn@40104
    16
bulwahn@40104
    17
definition
bulwahn@40104
    18
  "small_lazy i = Lazy_Sequence.single Room0"
bulwahn@40104
    19
bulwahn@40104
    20
instance ..
bulwahn@40104
    21
bulwahn@40104
    22
end
bulwahn@40104
    23
bulwahn@40104
    24
instantiation key :: small_lazy
bulwahn@40104
    25
begin
bulwahn@40104
    26
bulwahn@40104
    27
definition
bulwahn@40104
    28
  "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
    29
bulwahn@40104
    30
instance ..
bulwahn@40104
    31
bulwahn@40104
    32
end
bulwahn@40104
    33
bulwahn@40104
    34
instantiation guest :: small_lazy
bulwahn@40104
    35
begin
bulwahn@40104
    36
bulwahn@40104
    37
definition
bulwahn@40104
    38
  "small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)"
bulwahn@40104
    39
bulwahn@40104
    40
instance ..
bulwahn@40104
    41
bulwahn@40104
    42
end
bulwahn@40104
    43
bulwahn@40104
    44
setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
bulwahn@40104
    45
  Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *}
bulwahn@40104
    46
bulwahn@40104
    47
bulwahn@40104
    48
setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
bulwahn@40104
    49
  Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *}
bulwahn@40104
    50
bulwahn@40104
    51
lemma
bulwahn@40104
    52
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
bulwahn@40137
    53
quickcheck[generator = small_generators_depth_14, iterations = 1, size = 1, expect = no_counterexample]
bulwahn@40137
    54
quickcheck[generator = small_generators_depth_15, iterations = 1, size = 1, expect = counterexample]
bulwahn@40104
    55
oops
bulwahn@40104
    56
bulwahn@40104
    57
bulwahn@40104
    58
end