src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
author bulwahn
Fri Oct 22 18:38:59 2010 +0200 (2010-10-22)
changeset 40104 82873a6f2b81
child 40137 9eabcb1bfe50
permissions -rw-r--r--
splitting Hotel Key card example into specification and the two tests for counter example generation
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@40104
     8
instantiation room :: small_lazy
bulwahn@40104
     9
begin
bulwahn@40104
    10
bulwahn@40104
    11
definition
bulwahn@40104
    12
  "small_lazy i = Lazy_Sequence.single Room0"
bulwahn@40104
    13
bulwahn@40104
    14
instance ..
bulwahn@40104
    15
bulwahn@40104
    16
end
bulwahn@40104
    17
bulwahn@40104
    18
instantiation key :: small_lazy
bulwahn@40104
    19
begin
bulwahn@40104
    20
bulwahn@40104
    21
definition
bulwahn@40104
    22
  "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
    23
bulwahn@40104
    24
instance ..
bulwahn@40104
    25
bulwahn@40104
    26
end
bulwahn@40104
    27
bulwahn@40104
    28
instantiation guest :: small_lazy
bulwahn@40104
    29
begin
bulwahn@40104
    30
bulwahn@40104
    31
definition
bulwahn@40104
    32
  "small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)"
bulwahn@40104
    33
bulwahn@40104
    34
instance ..
bulwahn@40104
    35
bulwahn@40104
    36
end
bulwahn@40104
    37
bulwahn@40104
    38
setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
bulwahn@40104
    39
  Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *}
bulwahn@40104
    40
bulwahn@40104
    41
bulwahn@40104
    42
setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
bulwahn@40104
    43
  Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *}
bulwahn@40104
    44
bulwahn@40104
    45
lemma
bulwahn@40104
    46
  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
bulwahn@40104
    47
quickcheck[generator = small_generators_depth_14, iterations = 1, expect = no_counterexample]
bulwahn@40104
    48
quickcheck[generator = small_generators_depth_15, iterations = 1, expect = counterexample]
bulwahn@40104
    49
oops
bulwahn@40104
    50
bulwahn@40104
    51
bulwahn@40104
    52
end