src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40924 a9be7f26b4e6
child 41231 2e901158675e
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 theory Hotel_Example_Small_Generator
     2 imports Hotel_Example Predicate_Compile_Alternative_Defs
     3 uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
     4 begin
     5 
     6 declare Let_def[code_pred_inline]
     7 
     8 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
     9 by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    10 
    11 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    12 by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    13 
    14 instantiation room :: small_lazy
    15 begin
    16 
    17 definition
    18   "small_lazy i = Lazy_Sequence.single Room0"
    19 
    20 instance ..
    21 
    22 end
    23 
    24 instantiation key :: small_lazy
    25 begin
    26 
    27 definition
    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)))"
    29 
    30 instance ..
    31 
    32 end
    33 
    34 instantiation guest :: small_lazy
    35 begin
    36 
    37 definition
    38   "small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)"
    39 
    40 instance ..
    41 
    42 end
    43 
    44 setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
    45   Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *}
    46 
    47 
    48 setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
    49   Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *}
    50 
    51 lemma
    52   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    53 quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
    54 quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
    55 oops
    56 
    57 
    58 end