src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
changeset 40137 9eabcb1bfe50
parent 40104 82873a6f2b81
child 40658 5ccfc3ee7fe6
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Oct 25 21:17:11 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Oct 25 21:17:12 2010 +0200
     1.3 @@ -5,6 +5,12 @@
     1.4  
     1.5  declare Let_def[code_pred_inline]
     1.6  
     1.7 +lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
     1.8 +by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
     1.9 +
    1.10 +lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    1.11 +by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    1.12 +
    1.13  instantiation room :: small_lazy
    1.14  begin
    1.15  
    1.16 @@ -44,8 +50,8 @@
    1.17  
    1.18  lemma
    1.19    "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    1.20 -quickcheck[generator = small_generators_depth_14, iterations = 1, expect = no_counterexample]
    1.21 -quickcheck[generator = small_generators_depth_15, iterations = 1, expect = counterexample]
    1.22 +quickcheck[generator = small_generators_depth_14, iterations = 1, size = 1, expect = no_counterexample]
    1.23 +quickcheck[generator = small_generators_depth_15, iterations = 1, size = 1, expect = counterexample]
    1.24  oops
    1.25  
    1.26