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