1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 01 17:28:16 2010 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 01 17:45:28 2010 +0200
     1.3 @@ -1051,6 +1051,52 @@
     1.4  nitpick [expect = none]
     1.5  sorry
     1.6  
     1.7 +lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
     1.8 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
     1.9 +nitpick [card nat = 14, full_descrs, unary_ints, expect = potential] (* unfortunate *)
    1.10 +oops
    1.11 +
    1.12 +lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
    1.13 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.14 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.15 +sorry
    1.16 +
    1.17 +lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
    1.18 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.19 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.20 +sorry
    1.21 +
    1.22 +lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
    1.23 +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
    1.24 +oops
    1.25 +
    1.26 +lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
    1.27 +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
    1.28 +oops
    1.29 +
    1.30 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
    1.31 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.32 +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
    1.33 +oops
    1.34 +
    1.35 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
    1.36 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.37 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.38 +oops
    1.39 +
    1.40 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
    1.41 +nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
    1.42 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.43 +sorry
    1.44 +
    1.45 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
    1.46 +nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
    1.47 +oops
    1.48 +
    1.49 +lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
    1.50 +nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
    1.51 +sorry
    1.52 +
    1.53  subsection {* Destructors and Recursors *}
    1.54  
    1.55  lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"