# HG changeset patch
# User blanchet
# Date 1275407128 -7200
# Node ID c0f36d44de3339a086bc55c5549724709fef8c7b
# Parent  49c45156c9e17ad9f475ac7ec635fe20dd0cbbde
added examples/tests for THE and SOME

diff -r 49c45156c9e1 -r c0f36d44de33 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 01 17:28:16 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 01 17:45:28 2010 +0200
@@ -1051,6 +1051,52 @@
 nitpick [expect = none]
 sorry
 
+lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
+nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
+nitpick [card nat = 14, full_descrs, unary_ints, expect = potential] (* unfortunate *)
+oops
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
+nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
+nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+sorry
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
+nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
+nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+sorry
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
+nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
+oops
+
+lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
+nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
+oops
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
+nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
+nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
+oops
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
+nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
+nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+oops
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
+nitpick [card nat = 4, full_descrs, unary_ints, expect = potential]
+nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+sorry
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
+nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine]
+oops
+
+lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
+nitpick [card nat = 14, full_descrs, unary_ints, expect = none]
+sorry
+
 subsection {* Destructors and Recursors *}
 
 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"