make the Nitpick examples work again
authorblanchet
Fri Oct 23 20:13:33 2009 +0200 (2009-10-23)
changeset 331996c9b2a94a69c
parent 33198 bfb9a790d1e7
child 33200 c56c627dae19
make the Nitpick examples work again
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
     1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Oct 23 19:00:36 2009 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Oct 23 20:13:33 2009 +0200
     1.3 @@ -714,7 +714,7 @@
     1.4  
     1.5  lemma "{} = (\<lambda>x. False)"
     1.6  nitpick [expect = none]
     1.7 -by (metis Collect_def bot_set_eq empty_def)
     1.8 +by (metis Collect_def empty_def)
     1.9  
    1.10  lemma "x \<in> {}"
    1.11  nitpick [expect = genuine]
     2.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Oct 23 19:00:36 2009 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Oct 23 20:13:33 2009 +0200
     2.3 @@ -40,15 +40,15 @@
     2.4  nitpick [card = 2, max Nibble3 = 0, expect = none]
     2.5  oops
     2.6  
     2.7 -lemma "fun_pow 15 rot n \<noteq> n"
     2.8 +lemma "(rot ^^ 15) n \<noteq> n"
     2.9  nitpick [card = 17, expect = none]
    2.10  sorry
    2.11  
    2.12 -lemma "fun_pow 15 rot n = n"
    2.13 +lemma "(rot ^^ 15) n = n"
    2.14  nitpick [card = 17, expect = genuine]
    2.15  oops
    2.16  
    2.17 -lemma "fun_pow 16 rot n = n"
    2.18 +lemma "(rot ^^ 16) n = n"
    2.19  nitpick [card = 17, expect = none]
    2.20  oops
    2.21  
     3.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 23 19:00:36 2009 +0200
     3.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 23 20:13:33 2009 +0200
     3.3 @@ -157,11 +157,11 @@
     3.4  by (rule Rep_Nat_inverse)
     3.5  
     3.6  lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
     3.7 -nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = unknown]
     3.8 +nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
     3.9  by (rule Zero_int_def_raw)
    3.10  
    3.11  lemma "Abs_Integ (Rep_Integ a) = a"
    3.12 -nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = none]
    3.13 +nitpick [card = 1, timeout = 30 s, max_potential = 0, expect = none]
    3.14  by (rule Rep_Integ_inverse)
    3.15  
    3.16  lemma "Abs_list (Rep_list a) = a"
    3.17 @@ -173,15 +173,15 @@
    3.18    Ycoord :: int
    3.19  
    3.20  lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
    3.21 -nitpick [expect = none]
    3.22 +nitpick [expect = unknown]
    3.23  by (rule Rep_point_ext_type_inverse)
    3.24  
    3.25  lemma "Fract a b = of_int a / of_int b"
    3.26 -nitpick [card = 1\<midarrow>2, expect = potential]
    3.27 +nitpick [card = 1\<midarrow>2, expect = unknown]
    3.28  by (rule Fract_of_int_quotient)
    3.29  
    3.30  lemma "Abs_Rat (Rep_Rat a) = a"
    3.31 -nitpick [card = 1\<midarrow>2, expect = none]
    3.32 +nitpick [card = 1\<midarrow>2, expect = unknown]
    3.33  by (rule Rep_Rat_inverse)
    3.34  
    3.35  end