# HG changeset patch
# User blanchet
# Date 1256317164 -7200
# Node ID de6285ebcc05d4b0587c291c17f277e2fecf4f9f
# Parent  5fe67e108651e1222f6218126d014dec6e2fa574
continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.

diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/GCD.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -1702,4 +1702,12 @@
   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
 qed
 
+lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
+apply (rule eq_reflection)
+apply (induct x y rule: nat_gcd.induct)
+by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
+
+lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
+by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
+
 end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/Induct/LList.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -905,4 +905,9 @@
 lemma lappend_assoc': "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
 by (rule_tac l = l1 in llist_fun_equalityI, auto)
 
+setup {*
+Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+                            (map dest_Const [@{term LNil}, @{term LCons}])
+*}
+
 end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 23 18:59:24 2009 +0200
@@ -34,6 +34,7 @@
   HOL-Mirabelle \
   HOL-Modelcheck \
   HOL-NanoJava \
+  HOL-Nitpick_Examples \
   HOL-Nominal-Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
@@ -43,9 +44,9 @@
   HOL-SMT-Examples \
   HOL-Statespace \
   HOL-Subst \
-      TLA-Buffer \
-      TLA-Inc \
-      TLA-Memory \
+  TLA-Buffer \
+  TLA-Inc \
+  TLA-Memory \
   HOL-UNITY \
   HOL-Unix \
   HOL-W0 \
@@ -584,6 +585,21 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
 
 
+## HOL-Nitpick_Examples
+
+HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
+
+$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
+  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
+  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \
+  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
+  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
+  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
+  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
+  Nitpick_Examples/Typedef_Nits.thy
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
+
+
 ## HOL-Algebra
 
 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -200,6 +200,7 @@
   [code del]: "llist_case c d l =
     List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)"
 
+
 syntax  (* FIXME? *)
   LNil :: logic
   LCons :: logic
@@ -848,4 +849,9 @@
   qed
 qed
 
+setup {*
+Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+                            (map dest_Const [@{term LNil}, @{term LCons}])
+*}
+
 end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Core_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,1123 @@
+(*  Title:      HOL/Nitpick_Examples/Core_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick's functional core.
+*)
+
+header {* Examples Featuring Nitpick's Functional Core *}
+
+theory Core_Nits
+imports Main
+begin
+
+subsection {* Curry in a Hurry *}
+
+lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 100, expect = none, timeout = none]
+by auto
+
+lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
+nitpick [card = 2]
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 10, expect = none]
+by auto
+
+lemma "split (curry f) = f"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 10, expect = none]
+nitpick [card = 40, expect = none]
+by auto
+
+lemma "curry (split f) = f"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 40, expect = none]
+by auto
+
+lemma "(split o curry) f = f"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 40, expect = none]
+by auto
+
+lemma "(curry o split) f = f"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1000, expect = none]
+by auto
+
+lemma "(split o curry) f = (\<lambda>x. x) f"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 40, expect = none]
+by auto
+
+lemma "(curry o split) f = (\<lambda>x. x) f"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 40, expect = none]
+by auto
+
+lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 40, expect = none]
+by auto
+
+lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1000, expect = none]
+by auto
+
+lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1000, expect = none]
+by auto
+
+lemma "split o curry = (\<lambda>x. x)"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 40, expect = none]
+apply (rule ext)+
+by auto
+
+lemma "curry o split = (\<lambda>x. x)"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 100, expect = none]
+apply (rule ext)+
+by auto
+
+lemma "split (\<lambda>x y. f (x, y)) = f"
+nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 40, expect = none]
+by auto
+
+subsection {* Representations *}
+
+lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"
+nitpick [expect = none]
+by auto
+
+lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
+nitpick [card 'a = 35, card 'b = 34, expect = genuine]
+nitpick [card = 1\<midarrow>15, mono, expect = none]
+oops
+
+lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
+nitpick [card = 1, expect = genuine]
+nitpick [card = 2, expect = genuine]
+nitpick [card = 5, expect = genuine]
+oops
+
+lemma "P (\<lambda>x. x)"
+nitpick [card = 1, expect = genuine]
+nitpick [card = 5, expect = genuine]
+oops
+
+lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
+nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 20, expect = none]
+by auto
+
+lemma "fst (a, b) = a"
+nitpick [card = 1\<midarrow>20, expect = none]
+by auto
+
+lemma "\<exists>P. P = Id"
+nitpick [card = 1\<midarrow>4, expect = none]
+by auto
+
+lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
+nitpick [card = 1\<midarrow>3, expect = none]
+by auto
+
+lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
+nitpick [card = 1\<midarrow>6, expect = none]
+by auto
+
+lemma "Id (a, a)"
+nitpick [card = 1\<midarrow>100, expect = none]
+by (auto simp: Id_def Collect_def)
+
+lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
+nitpick [card = 1\<midarrow>20, expect = none]
+by (auto simp: Id_def Collect_def)
+
+lemma "UNIV (x\<Colon>'a\<times>'a)"
+nitpick [card = 1\<midarrow>50, expect = none]
+sorry
+
+lemma "{} = A - A"
+nitpick [card = 1\<midarrow>100, expect = none]
+by auto
+
+lemma "g = Let (A \<or> B)"
+nitpick [card = 1, expect = none]
+nitpick [card = 2, expect = genuine]
+nitpick [card = 20, expect = genuine]
+oops
+
+lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
+nitpick [expect = none]
+by auto
+
+lemma "A \<subseteq> B"
+nitpick [card = 100, expect = genuine]
+oops
+
+lemma "A = {b}"
+nitpick [card = 100, expect = genuine]
+oops
+
+lemma "{a, b} = {b}"
+nitpick [card = 100, expect = genuine]
+oops
+
+lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
+nitpick [card = 1, expect = genuine]
+nitpick [card = 2, expect = genuine]
+nitpick [card = 4, expect = genuine]
+nitpick [card = 20, expect = genuine]
+nitpick [card = 10, dont_box, expect = genuine]
+oops
+
+lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
+nitpick [card = 3, expect = genuine]
+nitpick [card = 3, dont_box, expect = genuine]
+nitpick [card = 5, expect = genuine]
+nitpick [card = 10, expect = genuine]
+oops
+
+lemma "f (a, b) = x"
+nitpick [card = 3, expect = genuine]
+nitpick [card = 10, expect = genuine]
+nitpick [card = 16, expect = genuine]
+nitpick [card = 30, expect = genuine]
+oops
+
+lemma "f (a, a) = f (c, d)"
+nitpick [card = 4, expect = genuine]
+nitpick [card = 20, expect = genuine]
+oops
+
+lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
+nitpick [card = 2, expect = none]
+by auto
+
+lemma "\<exists>F. F a b = G a b"
+nitpick [card = 3, expect = none]
+by auto
+
+lemma "f = split"
+nitpick [card = 1, expect = none]
+nitpick [card = 2, expect = genuine]
+oops
+
+lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R"
+nitpick [card = 20, expect = none]
+by auto
+
+lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
+       A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
+nitpick [card = 1\<midarrow>50, expect = none]
+by auto
+
+lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
+nitpick [card = 3, expect = genuine]
+nitpick [card = 4, expect = genuine]
+nitpick [card = 8, expect = genuine]
+oops
+
+subsection {* Quantifiers *}
+
+lemma "x = y"
+nitpick [card 'a = 1, expect = none]
+nitpick [card 'a = 2, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
+nitpick [card 'a = 1000, expect = genuine]
+oops
+
+lemma "\<forall>x. x = y"
+nitpick [card 'a = 1, expect = none]
+nitpick [card 'a = 2, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
+nitpick [card 'a = 1000, expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
+nitpick [card 'a = 1, expect = genuine]
+nitpick [card 'a = 2, expect = genuine]
+nitpick [card 'a = 100, expect = genuine]
+nitpick [card 'a = 1000, expect = genuine]
+oops
+
+lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
+nitpick [card 'a = 1\<midarrow>10, expect = none]
+by auto
+
+lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
+nitpick [card = 1\<midarrow>40, expect = none]
+by auto
+
+lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
+nitpick [card = 1\<midarrow>2, expect = genuine]
+nitpick [card = 3, expect = genuine]
+oops
+
+lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
+       f u v w x y z = f u (g u) w (h u w) y (k u w y)"
+nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 3, expect = none]
+nitpick [card = 4, expect = none]
+sorry
+
+lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
+       f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
+nitpick [card = 1\<midarrow>2, expect = genuine]
+oops
+
+lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
+       f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
+nitpick [card = 1\<midarrow>2, expect = genuine]
+oops
+
+lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
+       f u v w x = f u (g u) w (h u w)"
+nitpick [card = 1\<midarrow>2, expect = none]
+sorry
+
+lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
+       f u v w x = f u (g u w) w (h u)"
+nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
+oops
+
+lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
+       f u v w x = f u (g u) w (h u w)"
+nitpick [card = 1\<midarrow>2, dont_box, expect = none]
+sorry
+
+lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
+       f u v w x = f u (g u w) w (h u)"
+nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
+oops
+
+lemma "\<forall>x. if (\<forall>y. x = y) then False else True"
+nitpick [card = 1, expect = genuine]
+nitpick [card = 2\<midarrow>5, expect = none]
+oops
+
+lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True"
+nitpick [card = 1, expect = genuine]
+nitpick [card = 2, expect = none]
+oops
+
+lemma "\<forall>x. if (\<exists>y. x = y) then True else False"
+nitpick [expect = none]
+sorry
+
+lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"
+nitpick [expect = none]
+sorry
+
+lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
+nitpick [expect = none]
+by auto
+
+lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
+nitpick [expect = none]
+by auto
+
+lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
+nitpick [card 'a = 1, expect = genuine]
+nitpick [card 'a = 2, expect = genuine]
+nitpick [card 'a = 3, expect = genuine]
+nitpick [card 'a = 4, expect = genuine]
+nitpick [card 'a = 5, expect = genuine]
+oops
+
+lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x)
+           else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
+nitpick [expect = none]
+by auto
+
+lemma "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x)
+           else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
+nitpick [expect = none]
+by auto
+
+lemma "let x = (\<forall>x. P x) in if x then x else \<not> x"
+nitpick [expect = none]
+by auto
+
+lemma "let x = (\<forall>x\<Colon>'a \<times> 'b. P x) in if x then x else \<not> x"
+nitpick [expect = none]
+by auto
+
+subsection {* Schematic Variables *}
+
+lemma "x = ?x"
+nitpick [expect = none]
+by auto
+
+lemma "\<forall>x. x = ?x"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>x. x = ?x"
+nitpick [expect = none]
+by auto
+
+lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
+nitpick [expect = none]
+by auto
+
+lemma "\<forall>x. ?x = ?y"
+nitpick [expect = none]
+by auto
+
+lemma "\<exists>x. ?x = ?y"
+nitpick [expect = none]
+by auto
+
+subsection {* Known Constants *}
+
+lemma "x \<equiv> all \<Longrightarrow> False"
+nitpick [card = 1, expect = genuine]
+nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
+nitpick [card = 2, expect = genuine]
+nitpick [card = 8, expect = genuine]
+nitpick [card = 10, expect = unknown]
+oops
+
+lemma "\<And>x. f x y = f x y"
+nitpick [expect = none]
+oops
+
+lemma "\<And>x. f x y = f y x"
+nitpick [expect = genuine]
+oops
+
+lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
+nitpick [expect = none]
+by auto
+
+lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
+nitpick [expect = genuine]
+oops
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"
+nitpick [expect = none]
+by auto
+
+lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
+nitpick [card = 1, expect = genuine]
+nitpick [card = 2, expect = genuine]
+nitpick [card = 3, expect = genuine]
+nitpick [card = 4, expect = genuine]
+nitpick [card = 5, expect = genuine]
+nitpick [card = 100, expect = genuine]
+oops
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
+nitpick [expect = none]
+by auto
+
+lemma "P x \<equiv> P x"
+nitpick [card = 1\<midarrow>10, expect = none]
+by auto
+
+lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x"
+nitpick [card = 1\<midarrow>10, expect = none]
+by auto
+
+lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x"
+nitpick [card = 1\<midarrow>10, expect = none]
+by auto
+
+lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"
+nitpick [expect = genuine]
+oops
+
+lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> (op \<Longrightarrow> x) \<equiv> (\<lambda>y. (op \<Longrightarrow> x (I y)))"
+nitpick [expect = none]
+by auto
+
+lemma "P x \<Longrightarrow> P x"
+nitpick [card = 1\<midarrow>10, expect = none]
+by auto
+
+lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False"
+nitpick [expect = none]
+by auto
+
+lemma "True \<Longrightarrow> False"
+nitpick [expect = genuine]
+oops
+
+lemma "x = Not"
+nitpick [expect = genuine]
+oops
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> Not = (\<lambda>x. Not (I x))"
+nitpick [expect = none]
+by auto
+
+lemma "x = True"
+nitpick [expect = genuine]
+oops
+
+lemma "x = False"
+nitpick [expect = genuine]
+oops
+
+lemma "x = undefined"
+nitpick [expect = genuine]
+oops
+
+lemma "(False, ()) = undefined \<Longrightarrow> ((), False) = undefined"
+nitpick [expect = genuine]
+oops
+
+lemma "undefined = undefined"
+nitpick [expect = none]
+by auto
+
+lemma "f undefined = f undefined"
+nitpick [expect = none]
+by auto
+
+lemma "f undefined = g undefined"
+nitpick [card = 33, expect = genuine]
+oops
+
+lemma "\<exists>!x. x = undefined"
+nitpick [card = 30, expect = none]
+by auto
+
+lemma "x = All \<Longrightarrow> False"
+nitpick [card = 1, dont_box, expect = genuine]
+nitpick [card = 2, dont_box, expect = genuine]
+nitpick [card = 8, dont_box, expect = genuine]
+nitpick [card = 10, dont_box, expect = unknown]
+oops
+
+lemma "\<forall>x. f x y = f x y"
+nitpick [expect = none]
+oops
+
+lemma "\<forall>x. f x y = f y x"
+nitpick [expect = genuine]
+oops
+
+lemma "All (\<lambda>x. f x y = f x y) = True"
+nitpick [expect = none]
+by auto
+
+lemma "All (\<lambda>x. f x y = f x y) = False"
+nitpick [expect = genuine]
+oops
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"
+nitpick [expect = none]
+by auto
+
+lemma "x = Ex \<Longrightarrow> False"
+nitpick [card = 1, dont_box, expect = genuine]
+nitpick [card = 2, dont_box, expect = genuine]
+nitpick [card = 8, dont_box, expect = genuine]
+nitpick [card = 10, dont_box, expect = unknown]
+oops
+
+lemma "\<exists>x. f x y = f x y"
+nitpick [expect = none]
+oops
+
+lemma "\<exists>x. f x y = f y x"
+nitpick [expect = none]
+oops
+
+lemma "Ex (\<lambda>x. f x y = f x y) = True"
+nitpick [expect = none]
+by auto
+
+lemma "Ex (\<lambda>x. f x y = f y x) = True"
+nitpick [expect = none]
+by auto
+
+lemma "Ex (\<lambda>x. f x y = f x y) = False"
+nitpick [expect = genuine]
+oops
+
+lemma "Ex (\<lambda>x. f x y = f y x) = False"
+nitpick [expect = genuine]
+oops
+
+lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> Ex P = Ex (\<lambda>x. P (I x))"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))"
+      "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))"
+nitpick [expect = none]
+by auto
+
+lemma "x = y \<Longrightarrow> y = x"
+nitpick [expect = none]
+by auto
+
+lemma "x = y \<Longrightarrow> f x = f y"
+nitpick [expect = none]
+by auto
+
+lemma "x = y \<and> y = z \<Longrightarrow> x = z"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))"
+      "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))"
+nitpick [expect = none]
+by auto
+
+lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))"
+nitpick [expect = none]
+by auto
+
+lemma "a \<and> b \<Longrightarrow> a" "a \<and> b \<Longrightarrow> b"
+nitpick [expect = none]
+by auto
+
+lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))"
+      "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))"
+nitpick [expect = none]
+by auto
+
+lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"
+nitpick [expect = none]
+by auto
+
+lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"
+nitpick [expect = none]
+by auto
+
+lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
+nitpick [expect = none]
+by auto
+
+lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"
+nitpick [expect = none]
+by auto
+
+lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"
+nitpick [expect = none]
+by auto
+
+lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
+nitpick [expect = none]
+by auto
+
+lemma "(if a then b else c) = (THE d. (a \<longrightarrow> (d = b)) \<and> (\<not> a \<longrightarrow> (d = c)))"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))"
+      "J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))"
+      "K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))"
+nitpick [expect = none]
+by auto
+
+lemma "fst (x, y) = x"
+nitpick [expect = none]
+by (simp add: fst_def)
+
+lemma "snd (x, y) = y"
+nitpick [expect = none]
+by (simp add: snd_def)
+
+lemma "fst (x\<Colon>'a\<Rightarrow>'b, y) = x"
+nitpick [expect = none]
+by (simp add: fst_def)
+
+lemma "snd (x\<Colon>'a\<Rightarrow>'b, y) = y"
+nitpick [expect = none]
+by (simp add: snd_def)
+
+lemma "fst (x, y\<Colon>'a\<Rightarrow>'b) = x"
+nitpick [expect = none]
+by (simp add: fst_def)
+
+lemma "snd (x, y\<Colon>'a\<Rightarrow>'b) = y"
+nitpick [expect = none]
+by (simp add: snd_def)
+
+lemma "fst (x\<Colon>'a\<times>'b, y) = x"
+nitpick [expect = none]
+by (simp add: fst_def)
+
+lemma "snd (x\<Colon>'a\<times>'b, y) = y"
+nitpick [expect = none]
+by (simp add: snd_def)
+
+lemma "fst (x, y\<Colon>'a\<times>'b) = x"
+nitpick [expect = none]
+by (simp add: fst_def)
+
+lemma "snd (x, y\<Colon>'a\<times>'b) = y"
+nitpick [expect = none]
+by (simp add: snd_def)
+
+lemma "fst p = (THE a. \<exists>b. p = Pair a b)"
+nitpick [expect = none]
+by (simp add: fst_def)
+
+lemma "snd p = (THE b. \<exists>a. p = Pair a b)"
+nitpick [expect = none]
+by (simp add: snd_def)
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"
+nitpick [expect = none]
+by auto
+
+lemma "fst (x, y) = snd (y, x)"
+nitpick [expect = none]
+by auto
+
+lemma "(x, x) \<in> Id"
+nitpick [expect = none]
+by auto
+
+lemma "(x, y) \<in> Id \<Longrightarrow> x = y"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))"
+nitpick [expect = none]
+by (simp add: curry_def)
+
+lemma "{} = (\<lambda>x. False)"
+nitpick [expect = none]
+by (metis Collect_def bot_set_eq empty_def)
+
+lemma "x \<in> {}"
+nitpick [expect = genuine]
+oops
+
+lemma "{a, b} = {b}"
+nitpick [expect = genuine]
+oops
+
+lemma "{a, b} \<noteq> {b}"
+nitpick [expect = genuine]
+oops
+
+lemma "{a} = {b}"
+nitpick [expect = genuine]
+oops
+
+lemma "{a} \<noteq> {b}"
+nitpick [expect = genuine]
+oops
+
+lemma "{a, b, c} = {c, b, a}"
+nitpick [expect = none]
+by auto
+
+lemma "UNIV = (\<lambda>x. True)"
+nitpick [expect = none]
+by (simp only: UNIV_def Collect_def)
+
+lemma "UNIV x = True"
+nitpick [expect = none]
+by (simp only: UNIV_def Collect_def)
+
+lemma "x \<notin> UNIV"
+nitpick [expect = genuine]
+oops
+
+lemma "op \<in> = (\<lambda>x P. P x)"
+nitpick [expect = none]
+apply (rule ext)
+apply (rule ext)
+by (simp add: mem_def)
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))"
+nitpick [expect = none]
+apply (rule ext)
+apply (rule ext)
+by (simp add: mem_def)
+
+lemma "P x = (x \<in> P)"
+nitpick [expect = none]
+by (simp add: mem_def)
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"
+nitpick [expect = none]
+by simp
+
+lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
+nitpick [expect = none]
+by simp
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))"
+nitpick [card = 1\<midarrow>2, expect = none]
+by auto
+
+lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply (rule ext)
+by auto
+
+lemma "(x, x) \<in> rtrancl {(y, y)}"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
+nitpick [card = 1\<midarrow>2, expect = none]
+by auto
+
+lemma "((x, x), (x, x)) \<in> rtrancl {}"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
+nitpick [expect = none]
+by auto
+
+lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B"
+nitpick [card = 5, expect = genuine]
+oops
+
+lemma "A \<subset> B \<Longrightarrow> A \<subseteq> B"
+nitpick [expect = none]
+by auto
+
+lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
+nitpick [expect = none]
+by auto
+
+lemma "A \<union> - A = UNIV"
+nitpick [expect = none]
+by auto
+
+lemma "A \<inter> - A = {}"
+nitpick [expect = none]
+by auto
+
+lemma "A = -(A\<Colon>'a set)"
+nitpick [card 'a = 10, expect = genuine]
+oops
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
+nitpick [expect = none]
+oops
+
+lemma "finite A"
+nitpick [expect = none]
+oops
+
+lemma "finite A \<Longrightarrow> finite B"
+nitpick [expect = none]
+oops
+
+lemma "All finite"
+nitpick [expect = none]
+oops
+
+subsection {* The and Eps *}
+
+lemma "x = The"
+nitpick [card = 5, expect = genuine]
+oops
+
+lemma "\<exists>x. x = The"
+nitpick [card = 1\<midarrow>3]
+by auto
+
+lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x"
+nitpick [expect = none]
+by auto
+
+lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = z"
+nitpick [expect = genuine]
+oops
+
+lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y"
+nitpick [card = 2, expect = none]
+nitpick [card = 3\<midarrow>5, expect = genuine]
+oops
+
+lemma "P x \<Longrightarrow> P (The P)"
+nitpick [card = 1, expect = none]
+nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [card = 3\<midarrow>5, expect = genuine]
+nitpick [card = 8, expect = genuine]
+oops
+
+lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y"
+nitpick [expect = genuine]
+oops
+
+lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))"
+nitpick [card = 1\<midarrow>5, expect = none]
+by auto
+
+lemma "x = Eps"
+nitpick [card = 5, expect = genuine]
+oops
+
+lemma "\<exists>x. x = Eps"
+nitpick [card = 1\<midarrow>3, expect = none]
+by auto
+
+lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x"
+nitpick [expect = none]
+by auto
+
+lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> Eps P = z"
+nitpick [expect = genuine]
+apply auto
+oops
+
+lemma "P x \<Longrightarrow> P (Eps P)"
+nitpick [card = 1\<midarrow>8, expect = none]
+by (metis exE_some)
+
+lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Eps P)"
+nitpick [expect = genuine]
+oops
+
+lemma "(P\<Colon>nat set) (Eps P)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<not> P (Eps P)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<not> (P\<Colon>nat set) (Eps P)"
+nitpick [expect = genuine]
+oops
+
+lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)"
+nitpick [expect = none]
+sorry
+
+lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)"
+nitpick [expect = none]
+sorry
+
+lemma "P (The P)"
+nitpick [expect = genuine]
+oops
+
+lemma "(P\<Colon>nat set) (The P)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<not> P (The P)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<not> (P\<Colon>nat set) (The P)"
+nitpick [expect = genuine]
+oops
+
+lemma "The P \<noteq> x"
+nitpick [expect = genuine]
+oops
+
+lemma "The P \<noteq> (x\<Colon>nat)"
+nitpick [expect = genuine]
+oops
+
+lemma "P x \<Longrightarrow> P (The P)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (x\<Colon>nat) \<Longrightarrow> P (The P)"
+nitpick [expect = genuine]
+oops
+
+lemma "P = {x} \<Longrightarrow> P (The P)"
+nitpick [expect = none]
+oops
+
+lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)"
+nitpick [expect = none]
+oops
+
+consts Q :: 'a
+
+lemma "Q (Eps Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "(Q\<Colon>nat set) (Eps Q)"
+nitpick [expect = none]
+oops
+
+lemma "\<not> Q (Eps Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<not> (Q\<Colon>nat set) (Eps Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)"
+nitpick [expect = none]
+sorry
+
+lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)"
+nitpick [expect = none]
+sorry
+
+lemma "Q (The Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "(Q\<Colon>nat set) (The Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<not> Q (The Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<not> (Q\<Colon>nat set) (The Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "The Q \<noteq> x"
+nitpick [expect = genuine]
+oops
+
+lemma "The Q \<noteq> (x\<Colon>nat)"
+nitpick [expect = genuine]
+oops
+
+lemma "Q x \<Longrightarrow> Q (The Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "Q (x\<Colon>nat) \<Longrightarrow> Q (The Q)"
+nitpick [expect = genuine]
+oops
+
+lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
+nitpick [expect = none]
+oops
+
+lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
+nitpick [expect = none]
+oops
+
+subsection {* Destructors and Recursors *}
+
+lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"
+nitpick [card = 2, expect = none]
+by auto
+
+lemma "bool_rec x y True = x"
+nitpick [card = 2, expect = none]
+by auto
+
+lemma "bool_rec x y False = y"
+nitpick [card = 2, expect = none]
+by auto
+
+lemma "(x\<Colon>bool) = bool_rec x x True"
+nitpick [card = 2, expect = none]
+by auto
+
+lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')"
+nitpick [expect = none]
+sorry
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,104 @@
+(*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick applied to datatypes.
+*)
+
+header {* Examples Featuring Nitpick Applied to Datatypes *}
+
+theory Datatype_Nits
+imports Main
+begin
+
+primrec rot where
+"rot Nibble0 = Nibble1" |
+"rot Nibble1 = Nibble2" |
+"rot Nibble2 = Nibble3" |
+"rot Nibble3 = Nibble4" |
+"rot Nibble4 = Nibble5" |
+"rot Nibble5 = Nibble6" |
+"rot Nibble6 = Nibble7" |
+"rot Nibble7 = Nibble8" |
+"rot Nibble8 = Nibble9" |
+"rot Nibble9 = NibbleA" |
+"rot NibbleA = NibbleB" |
+"rot NibbleB = NibbleC" |
+"rot NibbleC = NibbleD" |
+"rot NibbleD = NibbleE" |
+"rot NibbleE = NibbleF" |
+"rot NibbleF = Nibble0"
+
+lemma "rot n \<noteq> n"
+nitpick [card = 1\<midarrow>16, expect = none]
+sorry
+
+lemma "rot Nibble2 \<noteq> Nibble3"
+nitpick [card = 1, expect = none]
+nitpick [card = 2, expect = genuine]
+nitpick [card = 2, max Nibble2 = 0, expect = none]
+nitpick [card = 2, max Nibble3 = 0, expect = none]
+oops
+
+lemma "fun_pow 15 rot n \<noteq> n"
+nitpick [card = 17, expect = none]
+sorry
+
+lemma "fun_pow 15 rot n = n"
+nitpick [card = 17, expect = genuine]
+oops
+
+lemma "fun_pow 16 rot n = n"
+nitpick [card = 17, expect = none]
+oops
+
+datatype ('a, 'b) pd = Pd "'a \<times> 'b"
+
+fun fs where
+"fs (Pd (a, _)) = a"
+
+fun sn where
+"sn (Pd (_, b)) = b"
+
+lemma "fs (Pd p) = fst p"
+nitpick [card = 20, expect = none]
+sorry
+
+lemma "fs (Pd p) = snd p"
+nitpick [expect = genuine]
+oops
+
+lemma "sn (Pd p) = snd p"
+nitpick [card = 20, expect = none]
+sorry
+
+lemma "sn (Pd p) = fst p"
+nitpick [expect = genuine]
+oops
+
+lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
+nitpick [card = 1\<midarrow>12, expect = none]
+sorry
+
+lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
+nitpick [expect = genuine]
+oops
+
+datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
+
+fun app where
+"app (Fn f) x = f x"
+
+lemma "app (Fn g) y = g y"
+nitpick [card = 1\<midarrow>12, expect = none]
+sorry
+
+lemma "app (Fn g) y = g' y"
+nitpick [expect = genuine]
+oops
+
+lemma "app (Fn g) y = g y'"
+nitpick [expect = genuine]
+oops
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Induct_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,171 @@
+(*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick applied to (co)inductive definitions.
+*)
+
+header {* Examples Featuring Nitpick Applied to (Co)inductive Definitions *}
+
+theory Induct_Nits
+imports Main
+begin
+
+nitpick_params [show_all]
+
+inductive p1 :: "nat \<Rightarrow> bool" where
+"p1 0" |
+"p1 n \<Longrightarrow> p1 (n + 2)"
+
+coinductive q1 :: "nat \<Rightarrow> bool" where
+"q1 0" |
+"q1 n \<Longrightarrow> q1 (n + 2)"
+
+lemma "p1 = q1"
+nitpick [expect = none]
+nitpick [wf, expect = none]
+nitpick [non_wf, expect = none]
+nitpick [non_wf, dont_star_linear_preds, expect = none]
+oops
+
+lemma "p1 \<noteq> q1"
+nitpick [expect = potential]
+nitpick [wf, expect = potential]
+nitpick [non_wf, expect = potential]
+nitpick [non_wf, dont_star_linear_preds, expect = potential]
+oops
+
+lemma "p1 (n - 2) \<Longrightarrow> p1 n"
+nitpick [expect = genuine]
+nitpick [non_wf, expect = genuine]
+nitpick [non_wf, dont_star_linear_preds, expect = genuine]
+oops
+
+lemma "q1 (n - 2) \<Longrightarrow> q1 n"
+nitpick [expect = genuine]
+nitpick [non_wf, expect = genuine]
+nitpick [non_wf, dont_star_linear_preds, expect = genuine]
+oops
+
+inductive p2 :: "nat \<Rightarrow> bool" where
+"p2 n \<Longrightarrow> p2 n"
+
+coinductive q2 :: "nat \<Rightarrow> bool" where
+"q2 n \<Longrightarrow> q2 n"
+
+lemma "p2 = {}"
+nitpick [expect = none]
+nitpick [dont_star_linear_preds, expect = none]
+sorry
+
+lemma "q2 = {}"
+nitpick [expect = genuine]
+nitpick [dont_star_linear_preds, expect = genuine]
+nitpick [wf, expect = likely_genuine]
+oops
+
+lemma "p2 = UNIV"
+nitpick [expect = genuine]
+nitpick [dont_star_linear_preds, expect = genuine]
+oops
+
+lemma "q2 = UNIV"
+nitpick [expect = none]
+nitpick [dont_star_linear_preds, expect = none]
+nitpick [wf, expect = likely_genuine]
+sorry
+
+lemma "p2 = q2"
+nitpick [expect = genuine]
+nitpick [dont_star_linear_preds, expect = genuine]
+oops
+
+lemma "p2 n"
+nitpick [expect = genuine]
+nitpick [dont_star_linear_preds, expect = genuine]
+nitpick [dont_specialize, expect = genuine]
+oops
+
+lemma "q2 n"
+nitpick [expect = none]
+nitpick [dont_star_linear_preds, expect = none]
+sorry
+
+lemma "\<not> p2 n"
+nitpick [expect = none]
+nitpick [dont_star_linear_preds, expect = none]
+sorry
+
+lemma "\<not> q2 n"
+nitpick [expect = genuine]
+nitpick [dont_star_linear_preds, expect = genuine]
+nitpick [dont_specialize, expect = genuine]
+oops
+
+inductive p3 and p4 where
+"p3 0" |
+"p3 n \<Longrightarrow> p4 (Suc n)" |
+"p4 n \<Longrightarrow> p3 (Suc n)"
+
+coinductive q3 and q4 where
+"q3 0" |
+"q3 n \<Longrightarrow> q4 (Suc n)" |
+"q4 n \<Longrightarrow> q3 (Suc n)"
+
+lemma "p3 = q3"
+nitpick [expect = none]
+nitpick [dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = potential]
+nitpick [non_wf, dont_box, expect = none]
+nitpick [non_wf, dont_star_linear_preds, expect = none]
+sorry
+
+lemma "p4 = q4"
+nitpick [expect = none]
+nitpick [dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = potential]
+nitpick [non_wf, dont_box, expect = none]
+nitpick [non_wf, dont_star_linear_preds, expect = none]
+sorry
+
+lemma "p3 = UNIV - p4"
+nitpick [expect = none]
+nitpick [dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = potential]
+nitpick [non_wf, dont_box, expect = none]
+nitpick [non_wf, dont_star_linear_preds, expect = none]
+sorry
+
+lemma "q3 = UNIV - q4"
+nitpick [expect = none]
+nitpick [dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = none]
+nitpick [non_wf, dont_box, expect = none]
+nitpick [non_wf, dont_star_linear_preds, expect = none]
+sorry
+
+lemma "p3 \<inter> q4 \<noteq> {}"
+nitpick [expect = potential]
+nitpick [non_wf, expect = potential]
+nitpick [non_wf, dont_star_linear_preds, expect = potential]
+sorry
+
+lemma "q3 \<inter> p4 \<noteq> {}"
+nitpick [expect = potential]
+nitpick [non_wf, expect = potential]
+nitpick [non_wf, dont_star_linear_preds, expect = potential]
+sorry
+
+lemma "p3 \<union> q4 \<noteq> UNIV"
+nitpick [expect = potential]
+nitpick [non_wf, expect = potential]
+nitpick [non_wf, dont_star_linear_preds, expect = potential]
+sorry
+
+lemma "q3 \<union> p4 \<noteq> UNIV"
+nitpick [expect = potential]
+nitpick [non_wf, expect = potential]
+nitpick [non_wf, dont_star_linear_preds, expect = potential]
+sorry
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,389 @@
+(*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples from the Nitpick manual.
+*)
+
+header {* Examples from the Nitpick Manual *}
+
+theory Manual_Nits
+imports Main Coinductive_List RealDef
+begin
+
+chapter {* 3. First Steps *}
+
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
+
+subsection {* 3.1. Propositional Logic *}
+
+lemma "P \<longleftrightarrow> Q"
+nitpick
+apply auto
+nitpick 1
+nitpick 2
+oops
+
+subsection {* 3.2. Type Variables *}
+
+lemma "P x \<Longrightarrow> P (THE y. P y)"
+nitpick [verbose]
+oops
+
+subsection {* 3.3. Constants *}
+
+lemma "P x \<Longrightarrow> P (THE y. P y)"
+nitpick [show_consts]
+nitpick [full_descrs, show_consts]
+nitpick [dont_specialize, full_descrs, show_consts]
+oops
+
+lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
+nitpick
+nitpick [card 'a = 1-50]
+(* sledgehammer *)
+apply (metis the_equality)
+done
+
+subsection {* 3.4. Skolemization *}
+
+lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
+nitpick
+oops
+
+lemma "\<exists>x. \<forall>f. f x = x"
+nitpick
+oops
+
+lemma "refl r \<Longrightarrow> sym r"
+nitpick
+oops
+
+subsection {* 3.5. Numbers *}
+
+lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
+nitpick
+oops
+
+lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
+nitpick [card nat = 100, check_potential]
+oops
+
+lemma "P Suc"
+nitpick [card = 1-6]
+oops
+
+lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
+nitpick [card nat = 1]
+nitpick [card nat = 2]
+oops
+
+subsection {* 3.6. Inductive Datatypes *}
+
+lemma "hd (xs @ [y, y]) = hd xs"
+nitpick
+nitpick [show_consts, show_datatypes]
+oops
+
+lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
+nitpick [show_datatypes]
+oops
+
+subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
+
+typedef three = "{0\<Colon>nat, 1, 2}"
+by blast
+
+definition A :: three where "A \<equiv> Abs_three 0"
+definition B :: three where "B \<equiv> Abs_three 1"
+definition C :: three where "C \<equiv> Abs_three 2"
+
+lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
+nitpick [show_datatypes]
+oops
+
+record point =
+  Xcoord :: int
+  Ycoord :: int
+
+lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
+nitpick [show_datatypes]
+oops
+
+lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
+nitpick [show_datatypes]
+oops
+
+subsection {* 3.8. Inductive and Coinductive Predicates *}
+
+inductive even where
+"even 0" |
+"even n \<Longrightarrow> even (Suc (Suc n))"
+
+lemma "\<exists>n. even n \<and> even (Suc n)"
+nitpick [card nat = 100, verbose]
+oops
+
+lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
+nitpick [card nat = 100]
+oops
+
+inductive even' where
+"even' (0\<Colon>nat)" |
+"even' 2" |
+"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
+
+lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
+nitpick [card nat = 10, verbose, show_consts]
+oops
+
+lemma "even' (n - 2) \<Longrightarrow> even' n"
+nitpick [card nat = 10, show_consts]
+oops
+
+coinductive nats where
+"nats (x\<Colon>nat) \<Longrightarrow> nats x"
+
+lemma "nats = {0, 1, 2, 3, 4}"
+nitpick [card nat = 10, show_consts]
+oops
+
+inductive odd where
+"odd 1" |
+"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
+
+lemma "odd n \<Longrightarrow> odd (n - 2)"
+nitpick [card nat = 10, show_consts]
+oops
+
+subsection {* 3.9. Coinductive Datatypes *}
+
+lemma "xs \<noteq> LCons a xs"
+nitpick
+oops
+
+lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
+nitpick [verbose]
+nitpick [bisim_depth = -1, verbose]
+oops
+
+lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
+nitpick [bisim_depth = -1, show_datatypes]
+nitpick
+sorry
+
+subsection {* 3.10. Boxing *}
+
+datatype tm = Var nat | Lam tm | App tm tm
+
+primrec lift where
+"lift (Var j) k = Var (if j < k then j else j + 1)" |
+"lift (Lam t) k = Lam (lift t (k + 1))" |
+"lift (App t u) k = App (lift t k) (lift u k)"
+
+primrec loose where
+"loose (Var j) k = (j \<ge> k)" |
+"loose (Lam t) k = loose t (Suc k)" |
+"loose (App t u) k = (loose t k \<or> loose u k)"
+
+primrec subst\<^isub>1 where
+"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
+"subst\<^isub>1 \<sigma> (Lam t) =
+ Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
+"subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
+
+lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
+nitpick [verbose]
+nitpick [eval = "subst\<^isub>1 \<sigma> t"]
+nitpick [dont_box]
+oops
+
+primrec subst\<^isub>2 where
+"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
+"subst\<^isub>2 \<sigma> (Lam t) =
+ Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
+"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
+
+lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
+nitpick
+sorry
+
+subsection {* 3.11. Scope Monotonicity *}
+
+lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
+nitpick [verbose]
+nitpick [card = 8, verbose]
+oops
+
+lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
+nitpick [mono]
+nitpick
+oops
+
+section {* 4. Case Studies *}
+
+nitpick_params [max_potential = 0, max_threads = 2]
+
+subsection {* 4.1. A Context-Free Grammar *}
+
+datatype alphabet = a | b
+
+inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
+  "[] \<in> S\<^isub>1"
+| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
+
+theorem S\<^isub>1_sound:
+"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+nitpick
+oops
+
+inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
+  "[] \<in> S\<^isub>2"
+| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
+| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
+| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
+| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
+| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
+
+theorem S\<^isub>2_sound:
+"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+nitpick
+oops
+
+inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
+  "[] \<in> S\<^isub>3"
+| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
+| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
+| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
+| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
+| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
+
+theorem S\<^isub>3_sound:
+"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+nitpick
+sorry
+
+theorem S\<^isub>3_complete:
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
+nitpick
+oops
+
+inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
+  "[] \<in> S\<^isub>4"
+| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
+| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
+| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
+| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
+| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
+| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
+
+theorem S\<^isub>4_sound:
+"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+nitpick
+sorry
+
+theorem S\<^isub>4_complete:
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
+nitpick
+sorry
+
+theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
+"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
+"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
+nitpick
+sorry
+
+subsection {* 4.2. AA Trees *}
+
+datatype 'a tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a tree" "'a tree"
+
+primrec data where
+"data \<Lambda> = undefined" |
+"data (N x _ _ _) = x"
+
+primrec dataset where
+"dataset \<Lambda> = {}" |
+"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
+
+primrec level where
+"level \<Lambda> = 0" |
+"level (N _ k _ _) = k"
+
+primrec left where
+"left \<Lambda> = \<Lambda>" |
+"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
+
+primrec right where
+"right \<Lambda> = \<Lambda>" |
+"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
+
+fun wf where
+"wf \<Lambda> = True" |
+"wf (N _ k t u) =
+ (if t = \<Lambda> then
+    k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
+  else
+    wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
+
+fun skew where
+"skew \<Lambda> = \<Lambda>" |
+"skew (N x k t u) =
+ (if t \<noteq> \<Lambda> \<and> k = level t then
+    N (data t) k (left t) (N x k (right t) u)
+  else
+    N x k t u)"
+
+fun split where
+"split \<Lambda> = \<Lambda>" |
+"split (N x k t u) =
+ (if u \<noteq> \<Lambda> \<and> k = level (right u) then
+    N (data u) (Suc k) (N x k t (left u)) (right u)
+  else
+    N x k t u)"
+
+theorem dataset_skew_split:
+"dataset (skew t) = dataset t"
+"dataset (split t) = dataset t"
+nitpick
+sorry
+
+theorem wf_skew_split:
+"wf t \<Longrightarrow> skew t = t"
+"wf t \<Longrightarrow> split t = t"
+nitpick
+sorry
+
+primrec insort\<^isub>1 where
+"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
+"insort\<^isub>1 (N y k t u) x =
+ (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
+                             (if x > y then insort\<^isub>1 u x else u))"
+
+theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
+nitpick
+oops
+
+theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
+nitpick [eval = "insort\<^isub>1 t x"]
+oops
+
+primrec insort\<^isub>2 where
+"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
+"insort\<^isub>2 (N y k t u) x =
+ (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
+                       (if x > y then insort\<^isub>2 u x else u))"
+
+theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
+nitpick
+sorry
+
+theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
+nitpick
+sorry
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Mini_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,107 @@
+(*  Title:      HOL/Nitpick_Examples/Mini_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Minipick, the minimalistic version of Nitpick.
+*)
+
+header {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
+
+theory Mini_Nits
+imports Main
+begin
+
+ML {*
+exception FAIL
+
+(* int -> term -> string *)
+fun minipick 0 _ = "none"
+  | minipick n t =
+    case minipick (n - 1) t of
+      "none" => Minipick.pick_nits_in_term @{context} (K n) t
+    | outcome_code => outcome_code
+(* int -> term -> bool *)
+fun none n t = (minipick n t = "none" orelse raise FAIL)
+fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
+fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
+*}
+
+ML {* minipick 1 @{prop "\<forall>x\<Colon>'a. \<exists>y\<Colon>'b. f x = y"} *}
+
+ML {* genuine 1 @{prop "x = Not"} *}
+ML {* none 1 @{prop "\<exists>x. x = Not"} *}
+ML {* none 1 @{prop "\<not> False"} *}
+ML {* genuine 1 @{prop "\<not> True"} *}
+ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
+ML {* none 1 @{prop True} *}
+ML {* genuine 1 @{prop False} *}
+ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
+ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
+ML {* none 5 @{prop "\<forall>x. x = x"} *}
+ML {* none 5 @{prop "\<exists>x. x = x"} *}
+ML {* none 1 @{prop "\<forall>x. x = y"} *}
+ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
+ML {* none 1 @{prop "\<exists>x. x = y"} *}
+ML {* none 2 @{prop "\<exists>x. x = y"} *}
+ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
+ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
+ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
+ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
+ML {* none 1 @{prop "All = Ex"} *}
+ML {* genuine 2 @{prop "All = Ex"} *}
+ML {* none 1 @{prop "All P = Ex P"} *}
+ML {* genuine 2 @{prop "All P = Ex P"} *}
+ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
+ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
+ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
+ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
+ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
+ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
+ML {* genuine 1 @{prop "(op =) X = Ex"} *}
+ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
+ML {* none 1 @{prop "x = y"} *}
+ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
+ML {* genuine 2 @{prop "x = y"} *}
+ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
+ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
+ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
+ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
+ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
+ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
+ML {* none 5 @{prop "{a} = {a, a}"} *}
+ML {* genuine 2 @{prop "{a} = {a, b}"} *}
+ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
+ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
+ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
+ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
+ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
+ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
+ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
+ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
+ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
+ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
+ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
+ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
+ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
+ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
+ML {* none 8 @{prop "fst (a, b) = a"} *}
+ML {* none 1 @{prop "fst (a, b) = b"} *}
+ML {* genuine 2 @{prop "fst (a, b) = b"} *}
+ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
+ML {* none 8 @{prop "snd (a, b) = b"} *}
+ML {* none 1 @{prop "snd (a, b) = a"} *}
+ML {* genuine 2 @{prop "snd (a, b) = a"} *}
+ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
+ML {* genuine 1 @{prop P} *}
+ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
+ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
+ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
+ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
+ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
+ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
+ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,98 @@
+(*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick's monotonicity check.
+*)
+
+header {* Examples Featuring Nitpick's Monotonicity Check *}
+
+theory Mono_Nits
+imports Main
+begin
+
+ML {*
+exception FAIL
+
+val defs = NitpickHOL.all_axioms_of @{theory} |> #1
+val def_table = NitpickHOL.const_def_table @{context} defs
+val ext_ctxt =
+  {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
+   user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false,
+   specialize = false, skolemize = false, star_linear_preds = false,
+   uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [],
+   case_names = [], def_table = def_table, nondef_table = Symtab.empty,
+   user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty,
+   psimp_table = Symtab.empty, intro_table = Symtab.empty,
+   ground_thm_table = Inttab.empty, ersatz_table = [],
+   skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
+   unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
+(* term -> bool *)
+val is_mono = NitpickMono.formulas_monotonic ext_ctxt @{typ 'a} [] []
+fun is_const t =
+  let val T = fastype_of t in
+    is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
+                               @{const False}))
+  end
+fun mono t = is_mono t orelse raise FAIL
+fun nonmono t = not (is_mono t) orelse raise FAIL
+fun const t = is_const t orelse raise FAIL
+fun nonconst t = not (is_const t) orelse raise FAIL
+*}
+
+ML {* const @{term "A::('a\<Rightarrow>'b)"} *}
+ML {* const @{term "(A::'a set) = A"} *}
+ML {* const @{term "(A::'a set set) = A"} *}
+ML {* const @{term "(\<lambda>x::'a set. x a)"} *}
+ML {* const @{term "{{a}} = C"} *}
+ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
+ML {* const @{term "A \<union> B"} *}
+ML {* const @{term "P (a::'a)"} *}
+ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
+ML {* const @{term "\<forall>A::'a set. A a"} *}
+ML {* const @{term "\<forall>A::'a set. P A"} *}
+ML {* const @{term "P \<or> Q"} *}
+ML {* const @{term "A \<union> B = C"} *}
+ML {* const @{term "(if P then (A::'a set) else B) = C"} *}
+ML {* const @{term "let A = C in A \<union> B"} *}
+ML {* const @{term "THE x::'b. P x"} *}
+ML {* const @{term "{}::'a set"} *}
+ML {* const @{term "(\<lambda>x::'a. True)"} *}
+ML {* const @{term "Let a A"} *}
+ML {* const @{term "A (a::'a)"} *}
+ML {* const @{term "insert a A = B"} *}
+ML {* const @{term "- (A::'a set)"} *}
+ML {* const @{term "finite A"} *}
+ML {* const @{term "\<not> finite A"} *}
+ML {* const @{term "finite (A::'a set set)"} *}
+ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
+ML {* const @{term "A < (B::'a set)"} *}
+ML {* const @{term "A \<le> (B::'a set)"} *}
+ML {* const @{term "[a::'a]"} *}
+ML {* const @{term "[a::'a set]"} *}
+ML {* const @{term "[A \<union> (B::'a set)]"} *}
+ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
+ML {* const @{term "\<forall>P. P a"} *}
+
+ML {* nonconst @{term "{%x. True}"} *}
+ML {* nonconst @{term "{(%x. x = a)} = C"} *}
+ML {* nonconst @{term "\<forall>P (a::'a). P a"} *}
+ML {* nonconst @{term "\<forall>a::'a. P a"} *}
+ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *}
+ML {* nonconst @{term "THE x. P x"} *}
+ML {* nonconst @{term "SOME x. P x"} *}
+
+ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
+ML {* mono @{prop "P (a::'a)"} *}
+ML {* mono @{prop "{a} = {b}"} *}
+ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *}
+ML {* mono @{prop "\<forall>F::'a set set. P"} *}
+ML {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *}
+ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *}
+ML {* mono @{prop "\<not> (\<forall>x. P x)"} *}
+
+ML {* nonmono @{prop "\<forall>x. P x"} *}
+ML {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
+ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *}
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Nitpick_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/Nitpick_Examples/Nitpick_Examples.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Nitpick examples.
+*)
+
+theory Nitpick_Examples
+imports Core_Nits Datatype_Nits Induct_Nits Manual_Nits Mini_Nits Mono_Nits
+        Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
+        Typedef_Nits
+begin
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Pattern_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,138 @@
+(*  Title:      HOL/Nitpick_Examples/Pattern_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick's "destroy_constrs" optimization.
+*)
+
+header {* Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization *}
+
+theory Pattern_Nits
+imports Main
+begin
+
+nitpick_params [card = 14]
+
+lemma "x = (case u of () \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case b of True \<Rightarrow> x | False \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case p of (x, y) \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> n)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case opt of None \<Rightarrow> x | Some y \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case xs of [] \<Rightarrow> x | y # ys \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case xs of
+              [] \<Rightarrow> x
+            | y # ys \<Rightarrow>
+              (case ys of
+                 [] \<Rightarrow> x
+               | z # zs \<Rightarrow>
+                 (case z of
+                    None \<Rightarrow> x
+                  | Some p \<Rightarrow>
+                    (case p of
+                       (a, b) \<Rightarrow> b))))"
+nitpick [expect = genuine]
+oops
+
+fun f1 where
+"f1 x () = x"
+
+lemma "x = f1 y u"
+nitpick [expect = genuine]
+oops
+
+fun f2 where
+"f2 x _ True = x" |
+"f2 _ y False = y"
+
+lemma "x = f2 x y b"
+nitpick [expect = genuine]
+oops
+
+fun f3 where
+"f3 (_, y) = y"
+
+lemma "x = f3 p"
+nitpick [expect = genuine]
+oops
+
+fun f4 where
+"f4 x 0 = x" |
+"f4 _ (Suc n) = n"
+
+lemma "x = f4 x n"
+nitpick [expect = genuine]
+oops
+
+fun f5 where
+"f5 x None = x" |
+"f5 _ (Some y) = y"
+
+lemma "x = f5 x opt"
+nitpick [expect = genuine]
+oops
+
+fun f6 where
+"f6 x [] = x" |
+"f6 _ (y # ys) = y"
+
+lemma "x = f6 x xs"
+nitpick [expect = genuine]
+oops
+
+fun f7 where
+"f7 _ (y # Some (a, b) # zs) = b" |
+"f7 x (y # None # zs) = x" |
+"f7 x [y] = x" |
+"f7 x [] = x"
+
+lemma "x = f7 x xs"
+nitpick [expect = genuine]
+oops
+
+lemma "u = ()"
+nitpick [expect = none]
+sorry
+
+lemma "\<exists>y. (b::bool) = y"
+nitpick [expect = none]
+sorry
+
+lemma "\<exists>x y. p = (x, y)"
+nitpick [expect = none]
+sorry
+
+lemma "\<exists>x. n = Suc x"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>y. x = Some y"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>y ys. xs = y # ys"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>y a b zs. x = (y # Some (a, b) # zs)"
+nitpick [expect = genuine]
+oops
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/ROOT.ML	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,8 @@
+(*  Title:      HOL/Nitpick_Examples/ROOT.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Nitpick examples.
+*)
+
+setmp_noncritical quick_and_dirty true (try use_thy) "Nitpick_Examples";
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Record_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,84 @@
+(*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick applied to records.
+*)
+
+header {* Examples Featuring Nitpick Applied to Records *}
+
+theory Record_Nits
+imports Main
+begin
+
+record point2d =
+  xc :: int
+  yc :: int
+
+lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
+nitpick [expect = none]
+sorry
+
+lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
+nitpick [expect = genuine]
+oops
+
+lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
+nitpick [expect = genuine]
+oops
+
+lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
+nitpick [expect = genuine]
+oops
+
+record point3d = point2d +
+  zc :: int
+
+lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
+nitpick [expect = none]
+sorry
+
+lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
+nitpick [expect = genuine]
+oops
+
+lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
+nitpick [expect = genuine]
+oops
+
+lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
+nitpick [expect = genuine]
+oops
+
+lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
+nitpick [expect = genuine]
+oops
+
+record point4d = point3d +
+  wc :: int
+
+lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
+nitpick [expect = none]
+sorry
+
+lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
+nitpick [expect = genuine]
+oops
+
+lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
+nitpick [expect = genuine]
+oops
+
+lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
+nitpick [expect = genuine]
+oops
+
+lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
+nitpick [expect = genuine]
+oops
+
+lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
+nitpick [expect = genuine]
+oops
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,1476 @@
+(*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Refute examples adapted to Nitpick.
+*)
+
+header {* Refute Examples Adapted to Nitpick *}
+
+theory Refute_Nits
+imports Main
+begin
+
+lemma "P \<and> Q"
+apply (rule conjI)
+nitpick [expect = genuine] 1
+nitpick [expect = genuine] 2
+nitpick [expect = genuine]
+nitpick [card = 5, expect = genuine]
+nitpick [sat_solver = MiniSat, expect = genuine] 2
+oops
+
+subsection {* Examples and Test Cases *}
+
+subsubsection {* Propositional logic *}
+
+lemma "True"
+nitpick [expect = none]
+apply auto
+done
+
+lemma "False"
+nitpick [expect = genuine]
+oops
+
+lemma "P"
+nitpick [expect = genuine]
+oops
+
+lemma "\<not> P"
+nitpick [expect = genuine]
+oops
+
+lemma "P \<and> Q"
+nitpick [expect = genuine]
+oops
+
+lemma "P \<or> Q"
+nitpick [expect = genuine]
+oops
+
+lemma "P \<longrightarrow> Q"
+nitpick [expect = genuine]
+oops
+
+lemma "(P\<Colon>bool) = Q"
+nitpick [expect = genuine]
+oops
+
+lemma "(P \<or> Q) \<longrightarrow> (P \<and> Q)"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Predicate logic *}
+
+lemma "P x y z"
+nitpick [expect = genuine]
+oops
+
+lemma "P x y \<longrightarrow> P y x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Equality *}
+
+lemma "P = True"
+nitpick [expect = genuine]
+oops
+
+lemma "P = False"
+nitpick [expect = genuine]
+oops
+
+lemma "x = y"
+nitpick [expect = genuine]
+oops
+
+lemma "f x = g x"
+nitpick [expect = genuine]
+oops
+
+lemma "(f\<Colon>'a\<Rightarrow>'b) = g"
+nitpick [expect = genuine]
+oops
+
+lemma "(f\<Colon>('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
+nitpick [expect = genuine]
+oops
+
+lemma "distinct [a, b]"
+nitpick [expect = genuine]
+apply simp
+nitpick [expect = genuine]
+oops
+
+subsubsection {* First-Order Logic *}
+
+lemma "\<exists>x. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>!x. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "Ex P"
+nitpick [expect = genuine]
+oops
+
+lemma "All P"
+nitpick [expect = genuine]
+oops
+
+lemma "Ex1 P"
+nitpick [expect = genuine]
+oops
+
+lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
+nitpick [expect = genuine]
+oops
+
+lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
+nitpick [expect = genuine]
+oops
+
+lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
+nitpick [expect = genuine]
+oops
+
+text {* A true statement (also testing names of free and bound variables being identical) *}
+
+lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
+nitpick [expect = none]
+apply fast
+done
+
+text {* "A type has at most 4 elements." *}
+
+lemma "\<not> distinct [a, b, c, d, e]"
+nitpick [expect = genuine]
+apply simp
+nitpick [expect = genuine]
+oops
+
+lemma "distinct [a, b, c, d]"
+nitpick [expect = genuine]
+apply simp
+nitpick [expect = genuine]
+oops
+
+text {* "Every reflexive and symmetric relation is transitive." *}
+
+lemma "\<lbrakk>\<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x\<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
+nitpick [expect = genuine]
+oops
+
+text {* The "Drinker's theorem" ... *}
+
+lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
+nitpick [expect = none]
+apply (auto simp add: ext)
+done
+
+text {* ... and an incorrect version of it *}
+
+lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
+nitpick [expect = genuine]
+oops
+
+text {* "Every function has a fixed point." *}
+
+lemma "\<exists>x. f x = x"
+nitpick [expect = genuine]
+oops
+
+text {* "Function composition is commutative." *}
+
+lemma "f (g x) = g (f x)"
+nitpick [expect = genuine]
+oops
+
+text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
+
+lemma "((P\<Colon>('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Higher-Order Logic *}
+
+lemma "\<exists>P. P"
+nitpick [expect = none]
+apply auto
+done
+
+lemma "\<forall>P. P"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>!P. P"
+nitpick [expect = none]
+apply auto
+done
+
+lemma "\<exists>!P. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P Q \<or> Q x"
+nitpick [expect = genuine]
+oops
+
+lemma "x \<noteq> All"
+nitpick [expect = genuine]
+oops
+
+lemma "x \<noteq> Ex"
+nitpick [expect = genuine]
+oops
+
+lemma "x \<noteq> Ex1"
+nitpick [expect = genuine]
+oops
+
+text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
+
+constdefs
+"trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+"trans P \<equiv> (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
+"subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+"subset P Q \<equiv> (ALL x y. P x y \<longrightarrow> Q x y)"
+"trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+"trans_closure P Q \<equiv> (subset Q P) \<and> (trans P) \<and> (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
+
+lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
+nitpick [expect = genuine]
+oops
+
+text {* "The union of transitive closures is equal to the transitive closure of unions." *}
+
+lemma "(\<forall>x y. (P x y \<or> R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y \<or> R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
+ \<longrightarrow> trans_closure TP P
+ \<longrightarrow> trans_closure TR R
+ \<longrightarrow> (T x y = (TP x y \<or> TR x y))"
+nitpick [expect = genuine]
+oops
+
+text {* "Every surjective function is invertible." *}
+
+lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
+nitpick [expect = genuine]
+oops
+
+text {* "Every invertible function is surjective." *}
+
+lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
+nitpick [expect = genuine]
+oops
+
+text {* Every point is a fixed point of some function. *}
+
+lemma "\<exists>f. f x = x"
+nitpick [card = 1\<midarrow>7, expect = none]
+apply (rule_tac x = "\<lambda>x. x" in exI)
+apply simp
+done
+
+text {* Axiom of Choice: first an incorrect version ... *}
+
+lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
+nitpick [expect = genuine]
+oops
+
+text {* ... and now two correct ones *}
+
+lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
+nitpick [card = 1-5, expect = none]
+apply (simp add: choice)
+done
+
+lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
+nitpick [card = 1-4, expect = none]
+apply auto
+ apply (simp add: ex1_implies_ex choice)
+apply (fast intro: ext)
+done
+
+subsubsection {* Metalogic *}
+
+lemma "\<And>x. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "f x \<equiv> g x"
+nitpick [expect = genuine]
+oops
+
+lemma "P \<Longrightarrow> Q"
+nitpick [expect = genuine]
+oops
+
+lemma "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"
+nitpick [expect = genuine]
+oops
+
+lemma "(x \<equiv> all) \<Longrightarrow> False"
+nitpick [expect = genuine]
+oops
+
+lemma "(x \<equiv> (op \<equiv>)) \<Longrightarrow> False"
+nitpick [expect = genuine]
+oops
+
+lemma "(x \<equiv> (op \<Longrightarrow>)) \<Longrightarrow> False"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Schematic Variables *}
+
+lemma "?P"
+nitpick [expect = none]
+apply auto
+done
+
+lemma "x = ?y"
+nitpick [expect = none]
+apply auto
+done
+
+subsubsection {* Abstractions *}
+
+lemma "(\<lambda>x. x) = (\<lambda>x. y)"
+nitpick [expect = genuine]
+oops
+
+lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
+nitpick [expect = genuine]
+oops
+
+lemma "(\<lambda>x. x) = (\<lambda>y. y)"
+nitpick [expect = none]
+apply simp
+done
+
+subsubsection {* Sets *}
+
+lemma "P (A\<Colon>'a set)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (A\<Colon>'a set set)"
+nitpick [expect = genuine]
+oops
+
+lemma "{x. P x} = {y. P y}"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "x \<in> {x. P x}"
+nitpick [expect = genuine]
+oops
+
+lemma "P (op \<in>)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (op \<in> x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P Collect"
+nitpick [expect = genuine]
+oops
+
+lemma "A Un B = A Int B"
+nitpick [expect = genuine]
+oops
+
+lemma "(A Int B) Un C = (A Un C) Int B"
+nitpick [expect = genuine]
+oops
+
+lemma "Ball A P \<longrightarrow> Bex A P"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* @{const undefined} *}
+
+lemma "undefined"
+nitpick [expect = genuine]
+oops
+
+lemma "P undefined"
+nitpick [expect = genuine]
+oops
+
+lemma "undefined x"
+nitpick [expect = genuine]
+oops
+
+lemma "undefined undefined"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* @{const The} *}
+
+lemma "The P"
+nitpick [expect = genuine]
+oops
+
+lemma "P The"
+nitpick [expect = genuine]
+oops
+
+lemma "P (The P)"
+nitpick [expect = genuine]
+oops
+
+lemma "(THE x. x=y) = z"
+nitpick [expect = genuine]
+oops
+
+lemma "Ex P \<longrightarrow> P (The P)"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* @{const Eps} *}
+
+lemma "Eps P"
+nitpick [expect = genuine]
+oops
+
+lemma "P Eps"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Eps P)"
+nitpick [expect = genuine]
+oops
+
+lemma "(SOME x. x=y) = z"
+nitpick [expect = genuine]
+oops
+
+lemma "Ex P \<longrightarrow> P (Eps P)"
+nitpick [expect = none]
+apply (auto simp add: someI)
+done
+
+subsubsection {* Operations on Natural Numbers *}
+
+lemma "(x\<Colon>nat) + y = 0"
+nitpick [expect = genuine]
+oops
+
+lemma "(x\<Colon>nat) = x + x"
+nitpick [expect = genuine]
+oops
+
+lemma "(x\<Colon>nat) - y + y = x"
+nitpick [expect = genuine]
+oops
+
+lemma "(x\<Colon>nat) = x * x"
+nitpick [expect = genuine]
+oops
+
+lemma "(x\<Colon>nat) < x + y"
+nitpick [card = 1, expect = genuine]
+nitpick [card = 2-5, expect = genuine]
+oops
+
+text {* \<times> *}
+
+lemma "P (x\<Colon>'a\<times>'b)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a\<times>'b. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (x, y)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (fst x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (snd x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P Pair"
+nitpick [expect = genuine]
+oops
+
+lemma "prod_rec f p = f (fst p) (snd p)"
+nitpick [expect = none]
+by (case_tac p) auto
+
+lemma "prod_rec f (a, b) = f a b"
+nitpick [expect = none]
+by auto
+
+lemma "P (prod_rec f x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of Pair a b \<Rightarrow> f a b)"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Subtypes (typedef), typedecl *}
+
+text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
+
+typedef 'a myTdef = "insert (undefined\<Colon>'a) (undefined\<Colon>'a set)"
+by auto
+
+lemma "(x\<Colon>'a myTdef) = y"
+nitpick [expect = genuine]
+oops
+
+typedecl myTdecl
+
+typedef 'a T_bij = "{(f\<Colon>'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
+by auto
+
+lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Inductive Datatypes *}
+
+text {* unit *}
+
+lemma "P (x\<Colon>unit)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>unit. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P ()"
+nitpick [expect = genuine]
+oops
+
+lemma "unit_rec u x = u"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (unit_rec u x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of () \<Rightarrow> u)"
+nitpick [expect = genuine]
+oops
+
+text {* option *}
+
+lemma "P (x\<Colon>'a option)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a option. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P None"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Some x)"
+nitpick [expect = genuine]
+oops
+
+lemma "option_rec n s None = n"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "option_rec n s (Some x) = s x"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (option_rec n s x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
+nitpick [expect = genuine]
+oops
+
+text {* + *}
+
+lemma "P (x\<Colon>'a+'b)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a+'b. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Inl x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Inr x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P Inl"
+nitpick [expect = genuine]
+oops
+
+lemma "sum_rec l r (Inl x) = l x"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "sum_rec l r (Inr x) = r x"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (sum_rec l r x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
+nitpick [expect = genuine]
+oops
+
+text {* Non-recursive datatypes *}
+
+datatype T1 = A | B
+
+lemma "P (x\<Colon>T1)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>T1. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P A"
+nitpick [expect = genuine]
+oops
+
+lemma "P B"
+nitpick [expect = genuine]
+oops
+
+lemma "T1_rec a b A = a"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "T1_rec a b B = b"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (T1_rec a b x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
+nitpick [expect = genuine]
+oops
+
+datatype 'a T2 = C T1 | D 'a
+
+lemma "P (x\<Colon>'a T2)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a T2. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P D"
+nitpick [expect = genuine]
+oops
+
+lemma "T2_rec c d (C x) = c x"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "T2_rec c d (D x) = d x"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (T2_rec c d x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
+nitpick [expect = genuine]
+oops
+
+datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
+
+lemma "P (x\<Colon>('a, 'b) T3)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>('a, 'b) T3. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P E"
+nitpick [expect = genuine]
+oops
+
+lemma "T3_rec e (E x) = e x"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "P (T3_rec e x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of E f \<Rightarrow> e f)"
+nitpick [expect = genuine]
+oops
+
+text {* Recursive datatypes *}
+
+text {* nat *}
+
+lemma "P (x\<Colon>nat)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>nat. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Suc 0)"
+nitpick [expect = genuine]
+oops
+
+lemma "P Suc"
+nitpick [card = 1\<midarrow>7, expect = none]
+oops
+
+lemma "nat_rec zero suc 0 = zero"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (nat_rec zero suc x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
+nitpick [expect = genuine]
+oops
+
+text {* 'a list *}
+
+lemma "P (xs\<Colon>'a list)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>xs\<Colon>'a list. P xs"
+nitpick [expect = genuine]
+oops
+
+lemma "P [x, y]"
+nitpick [expect = genuine]
+oops
+
+lemma "list_rec nil cons [] = nil"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (list_rec nil cons xs)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
+nitpick [expect = genuine]
+oops
+
+lemma "(xs\<Colon>'a list) = ys"
+nitpick [expect = genuine]
+oops
+
+lemma "a # xs = b # xs"
+nitpick [expect = genuine]
+oops
+
+datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
+
+lemma "P (x\<Colon>BitList)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>BitList. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Bit0 (Bit1 BitListNil))"
+nitpick [expect = genuine]
+oops
+
+lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (BitList_rec nil bit0 bit1 x)"
+nitpick [expect = genuine]
+oops
+
+datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
+
+lemma "P (x\<Colon>'a BinTree)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a BinTree. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Node (Leaf x) (Leaf y))"
+nitpick [expect = genuine]
+oops
+
+lemma "BinTree_rec l n (Leaf x) = l x"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
+nitpick [card = 1\<midarrow>6, expect = none]
+apply simp
+done
+
+lemma "P (BinTree_rec l n x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
+nitpick [expect = genuine]
+oops
+
+text {* Mutually recursive datatypes *}
+
+datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
+ and 'a bexp = Equal "'a aexp" "'a aexp"
+
+lemma "P (x\<Colon>'a aexp)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a aexp. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (x\<Colon>'a bexp)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a bexp. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "P (aexp_bexp_rec_1 number ite equal x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
+nitpick [expect = genuine]
+oops
+
+lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "P (aexp_bexp_rec_2 number ite equal x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
+nitpick [expect = genuine]
+oops
+
+datatype X = A | B X | C Y
+     and Y = D X | E Y | F
+
+lemma "P (x\<Colon>X)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (y\<Colon>Y)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (B (B A))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (B (C F))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (C (D A))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (C (E F))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (D (B A))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (D (C F))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (E (D A))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (E (E F))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (C (D (C F)))"
+nitpick [expect = genuine]
+oops
+
+lemma "X_Y_rec_1 a b c d e f A = a"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "X_Y_rec_2 a b c d e f F = f"
+nitpick [expect = none]
+apply simp
+done
+
+lemma "P (X_Y_rec_1 a b c d e f x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (X_Y_rec_2 a b c d e f y)"
+nitpick [expect = genuine]
+oops
+
+text {* Other datatype examples *}
+
+text {* Indirect recursion is implemented via mutual recursion. *}
+
+datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
+
+lemma "P (x\<Colon>XOpt)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (CX None)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (CX (Some (CX None)))"
+nitpick [expect = genuine]
+oops
+
+lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
+nitpick [card = 1\<midarrow>6, expect = none]
+apply simp
+done
+
+lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+nitpick [card = 1\<midarrow>4, expect = none]
+apply simp
+done
+
+lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
+nitpick [expect = genuine]
+oops
+
+datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
+
+lemma "P (x\<Colon>'a YOpt)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (CY None)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (CY (Some (\<lambda>a. CY None)))"
+nitpick [expect = genuine]
+oops
+
+lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
+nitpick [card = 1\<midarrow>2, expect = none]
+apply simp
+done
+
+lemma "YOpt_rec_2 cy n s None = n"
+nitpick [card = 1\<midarrow>2, expect = none]
+apply simp
+done
+
+lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
+nitpick [card = 1\<midarrow>2, expect = none]
+apply simp
+done
+
+lemma "P (YOpt_rec_1 cy n s x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (YOpt_rec_2 cy n s x)"
+nitpick [expect = genuine]
+oops
+
+datatype Trie = TR "Trie list"
+
+lemma "P (x\<Colon>Trie)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>Trie. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (TR [TR []])"
+nitpick [expect = genuine]
+oops
+
+lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
+nitpick [card = 1\<midarrow>6, expect = none]
+apply simp
+done
+
+lemma "Trie_rec_2 tr nil cons [] = nil"
+nitpick [card = 1\<midarrow>6, expect = none]
+apply simp
+done
+
+lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
+nitpick [card = 1\<midarrow>6, expect = none]
+apply simp
+done
+
+lemma "P (Trie_rec_1 tr nil cons x)"
+nitpick [card = 1, expect = genuine]
+oops
+
+lemma "P (Trie_rec_2 tr nil cons x)"
+nitpick [card = 1, expect = genuine]
+oops
+
+datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
+
+lemma "P (x\<Colon>InfTree)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>InfTree. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Node (\<lambda>n. Leaf))"
+nitpick [expect = genuine]
+oops
+
+lemma "InfTree_rec leaf node Leaf = leaf"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "P (InfTree_rec leaf node x)"
+nitpick [expect = genuine]
+oops
+
+datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
+
+lemma "P (x\<Colon>'a lambda)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'a lambda. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (Lam (\<lambda>a. Var a))"
+nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
+oops
+
+lemma "lambda_rec var app lam (Var x) = var x"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "P (lambda_rec v a l x)"
+nitpick [expect = genuine]
+oops
+
+text {* Taken from "Inductive datatypes in HOL", p. 8: *}
+
+datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
+datatype 'c U = E "('c, 'c U) T"
+
+lemma "P (x\<Colon>'c U)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<forall>x\<Colon>'c U. P x"
+nitpick [expect = genuine]
+oops
+
+lemma "P (E (C (\<lambda>a. True)))"
+nitpick [expect = genuine]
+oops
+
+lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "U_rec_2 e c d nil cons (C x) = c x"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "U_rec_3 e c d nil cons [] = nil"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
+nitpick [card = 1\<midarrow>3, expect = none]
+apply simp
+done
+
+lemma "P (U_rec_1 e c d nil cons x)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (U_rec_2 e c d nil cons x)"
+nitpick [card = 1, expect = genuine]
+oops
+
+lemma "P (U_rec_3 e c d nil cons x)"
+nitpick [card = 1, expect = genuine]
+oops
+
+subsubsection {* Records *}
+
+record ('a, 'b) point =
+  xpos :: 'a
+  ypos :: 'b
+
+lemma "(x\<Colon>('a, 'b) point) = y"
+nitpick [expect = genuine]
+oops
+
+record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
+  ext :: 'c
+
+lemma "(x\<Colon>('a, 'b, 'c) extpoint) = y"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Inductively Defined Sets *}
+
+inductive_set undefinedSet :: "'a set" where
+"undefined \<in> undefinedSet"
+
+lemma "x \<in> undefinedSet"
+nitpick [expect = genuine]
+oops
+
+inductive_set evenCard :: "'a set set"
+where
+"{} \<in> evenCard" |
+"\<lbrakk>S \<in> evenCard; x \<notin> S; y \<notin> S; x \<noteq> y\<rbrakk> \<Longrightarrow> S \<union> {x, y} \<in> evenCard"
+
+lemma "S \<in> evenCard"
+nitpick [expect = genuine]
+oops
+
+inductive_set
+even :: "nat set"
+and odd :: "nat set"
+where
+"0 \<in> even" |
+"n \<in> even \<Longrightarrow> Suc n \<in> odd" |
+"n \<in> odd \<Longrightarrow> Suc n \<in> even"
+
+lemma "n \<in> odd"
+nitpick [expect = genuine]
+oops
+
+consts f :: "'a \<Rightarrow> 'a"
+
+inductive_set a_even :: "'a set" and a_odd :: "'a set" where
+"undefined \<in> a_even" |
+"x \<in> a_even \<Longrightarrow> f x \<in> a_odd" |
+"x \<in> a_odd \<Longrightarrow> f x \<in> a_even"
+
+lemma "x \<in> a_odd"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Examples Involving Special Functions *}
+
+lemma "card x = 0"
+nitpick [expect = genuine]
+oops
+
+lemma "finite x"
+nitpick [expect = none]
+oops
+
+lemma "xs @ [] = ys @ []"
+nitpick [expect = genuine]
+oops
+
+lemma "xs @ ys = ys @ xs"
+nitpick [expect = genuine]
+oops
+
+lemma "f (lfp f) = lfp f"
+nitpick [expect = genuine]
+oops
+
+lemma "f (gfp f) = gfp f"
+nitpick [expect = genuine]
+oops
+
+lemma "lfp f = gfp f"
+nitpick [expect = genuine]
+oops
+
+subsubsection {* Axiomatic Type Classes and Overloading *}
+
+text {* A type class without axioms: *}
+
+axclass classA
+
+lemma "P (x\<Colon>'a\<Colon>classA)"
+nitpick [expect = genuine]
+oops
+
+text {* The axiom of this type class does not contain any type variables: *}
+
+axclass classB
+classB_ax: "P \<or> \<not> P"
+
+lemma "P (x\<Colon>'a\<Colon>classB)"
+nitpick [expect = genuine]
+oops
+
+text {* An axiom with a type variable (denoting types which have at least two elements): *}
+
+axclass classC < type
+classC_ax: "\<exists>x y. x \<noteq> y"
+
+lemma "P (x\<Colon>'a\<Colon>classC)"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>x y. (x\<Colon>'a\<Colon>classC) \<noteq> y"
+nitpick [expect = none]
+sorry
+
+text {* A type class for which a constant is defined: *}
+
+consts
+classD_const :: "'a \<Rightarrow> 'a"
+
+axclass classD < type
+classD_ax: "classD_const (classD_const x) = classD_const x"
+
+lemma "P (x\<Colon>'a\<Colon>classD)"
+nitpick [expect = genuine]
+oops
+
+text {* A type class with multiple superclasses: *}
+
+axclass classE < classC, classD
+
+lemma "P (x\<Colon>'a\<Colon>classE)"
+nitpick [expect = genuine]
+oops
+
+lemma "P (x\<Colon>'a\<Colon>{classB, classE})"
+nitpick [expect = genuine]
+oops
+
+text {* OFCLASS: *}
+
+lemma "OFCLASS('a\<Colon>type, type_class)"
+nitpick [expect = none]
+apply intro_classes
+done
+
+lemma "OFCLASS('a\<Colon>classC, type_class)"
+nitpick [expect = none]
+apply intro_classes
+done
+
+lemma "OFCLASS('a, classB_class)"
+nitpick [expect = none]
+apply intro_classes
+apply simp
+done
+
+lemma "OFCLASS('a\<Colon>type, classC_class)"
+nitpick [expect = genuine]
+oops
+
+text {* Overloading: *}
+
+consts inverse :: "'a \<Rightarrow> 'a"
+
+defs (overloaded)
+inverse_bool: "inverse (b\<Colon>bool) \<equiv> \<not> b"
+inverse_set: "inverse (S\<Colon>'a set) \<equiv> -S"
+inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
+
+lemma "inverse b"
+nitpick [expect = genuine]
+oops
+
+lemma "P (inverse (S\<Colon>'a set))"
+nitpick [expect = genuine]
+oops
+
+lemma "P (inverse (p\<Colon>'a\<times>'b))"
+nitpick [expect = genuine]
+oops
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Special_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,172 @@
+(*  Title:      HOL/Nitpick_Examples/Special_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick's "specialize" optimization.
+*)
+
+header {* Examples Featuring Nitpick's \textit{specialize} Optimization *}
+
+theory Special_Nits
+imports Main
+begin
+
+nitpick_params [card = 4, debug, show_consts, timeout = 10 s]
+
+fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
+"f1 a b c d e = a + b + c + d + e"
+
+lemma "f1 0 0 0 0 0 = f1 0 0 0 0 (1 - 1)"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+lemma "f1 u v w x y = f1 y x w v u"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+fun f2 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
+"f2 a b c d (Suc e) = a + b + c + d + e"
+
+lemma "f2 0 0 0 0 0 = f2 (1 - 1) 0 0 0 0"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+lemma "f2 0 (v - v) 0 (x - x) 0 = f2 (u - u) 0 (w - w) 0 (y - y)"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+lemma "f2 1 0 0 0 0 = f2 0 1 0 0 0"
+nitpick [expect = genuine]
+nitpick [dont_specialize, expect = genuine]
+oops
+
+lemma "f2 0 0 0 0 0 = f2 0 0 0 0 0"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+fun f3 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
+"f3 (Suc a) b 0 d (Suc e) = a + b + d + e" |
+"f3 0 b 0 d 0 = b + d"
+
+lemma "f3 a b c d e = f3 e d c b a"
+nitpick [expect = genuine]
+nitpick [dont_specialize, expect = genuine]
+oops
+
+lemma "f3 a b c d a = f3 a d c d a"
+nitpick [expect = genuine]
+nitpick [dont_specialize, expect = genuine]
+oops
+
+lemma "\<lbrakk>c < 1; a \<ge> e; e \<ge> a\<rbrakk> \<Longrightarrow> f3 a b c d a = f3 e d c b e"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+lemma "(\<forall>u. a = u \<longrightarrow> f3 a a a a a = f3 u u u u u)
+       \<and> (\<forall>u. b = u \<longrightarrow> f3 b b u b b = f3 u u b u u)"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+nitpick [dont_skolemize, expect = none]
+nitpick [dont_specialize, dont_skolemize, expect = none]
+sorry
+
+function f4 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"f4 x x = 1" |
+"f4 y z = (if y = z then 1 else 0)"
+by auto
+termination by lexicographic_order
+
+lemma "f4 a b = f4 b a"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+lemma "f4 a (Suc a) = f4 a a"
+nitpick [expect = genuine]
+nitpick [dont_specialize, expect = genuine]
+oops
+
+fun f5 :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
+"f5 f (Suc a) = f a"
+
+lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
+       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
+       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
+       f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
+nitpick [expect = genuine]
+sorry
+
+lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
+       f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
+nitpick [expect = genuine]
+sorry
+
+lemma "\<forall>a. g a = a
+       \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =
+                      f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"
+nitpick [expect = none]
+nitpick [dont_specialize, expect = none]
+sorry
+
+lemma "\<forall>a. g a = a
+       \<Longrightarrow> \<exists>one \<in> {2}. \<exists>two \<in> {1}. f5 g x =
+                      f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"
+nitpick [expect = potential]
+nitpick [dont_specialize, expect = potential]
+sorry
+
+lemma "\<forall>a. g a = a
+       \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
+           b\<^isub>1 < b\<^isub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"
+nitpick [expect = potential]
+nitpick [dont_specialize, expect = none]
+nitpick [dont_box, expect = none]
+nitpick [dont_box, dont_specialize, expect = none]
+sorry
+
+lemma "\<forall>a. g a = a
+       \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
+           b\<^isub>1 < b\<^isub>11
+           \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then
+                                a
+                              else
+                                h b\<^isub>2 + h b\<^isub>3 + h b\<^isub>4 + h b\<^isub>5 + h b\<^isub>6 + h b\<^isub>7 + h b\<^isub>8
+                                + h b\<^isub>9 + h b\<^isub>10) x"
+nitpick [card nat = 2, card 'a = 1, expect = none]
+nitpick [card nat = 2, card 'a = 1, dont_box, expect = none]
+nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = none]
+nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, expect = none]
+sorry
+
+lemma "\<forall>a. g a = a
+       \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
+           b\<^isub>1 < b\<^isub>11
+           \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 \<ge> b\<^isub>11 then
+                                a
+                              else
+                                h b\<^isub>2 + h b\<^isub>3 + h b\<^isub>4 + h b\<^isub>5 + h b\<^isub>6 + h b\<^isub>7 + h b\<^isub>8
+                                + h b\<^isub>9 + h b\<^isub>10) x"
+nitpick [card nat = 2, card 'a = 1, expect = none]
+nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]
+nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]
+nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,
+         expect = potential]
+oops
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Tests_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Nitpick_Examples/Tests_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Nitpick tests.
+*)
+
+header {* Nitpick Tests *}
+
+theory Tests_Nits
+imports Main
+begin
+
+ML {* NitpickTests.run_all_tests () *}
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,187 @@
+(*  Title:      HOL/Nitpick_Examples/Typedef_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick applied to typedefs.
+*)
+
+header {* Examples Featuring Nitpick Applied to Typedefs *}
+
+theory Typedef_Nits
+imports Main Rational
+begin
+
+nitpick_params [card = 1\<midarrow>4, timeout = 5 s]
+
+typedef three = "{0\<Colon>nat, 1, 2}"
+by blast
+
+definition A :: three where "A \<equiv> Abs_three 0"
+definition B :: three where "B \<equiv> Abs_three 1"
+definition C :: three where "C \<equiv> Abs_three 2"
+
+lemma "x = (y\<Colon>three)"
+nitpick [expect = genuine]
+oops
+
+typedef 'a one_or_two = "{undefined False\<Colon>'a, undefined True}"
+by auto
+
+lemma "x = (y\<Colon>unit one_or_two)"
+nitpick [expect = none]
+sorry
+
+lemma "x = (y\<Colon>bool one_or_two)"
+nitpick [expect = genuine]
+oops
+
+lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> x = (y\<Colon>bool one_or_two)"
+nitpick [expect = none]
+sorry
+
+lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> \<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
+nitpick [card = 1, expect = potential] (* unfortunate *)
+oops
+
+lemma "\<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
+nitpick [card = 1, expect = potential] (* unfortunate *)
+nitpick [card = 2, expect = none]
+oops
+
+typedef 'a bounded =
+        "{n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
+apply (rule_tac x = 0 in exI)
+apply (case_tac "card UNIV = 0")
+by auto
+
+lemma "x = (y\<Colon>unit bounded)"
+nitpick [expect = none]
+sorry
+
+lemma "x = (y\<Colon>bool bounded)"
+nitpick [expect = genuine]
+oops
+
+lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
+nitpick [expect = none]
+sorry
+
+lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
+nitpick [card = 1\<midarrow>5, timeout = 10 s, expect = genuine]
+oops
+
+lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
+nitpick [expect = none]
+by (rule True_def)
+
+lemma "False \<equiv> \<forall>P. P"
+nitpick [expect = none]
+by (rule False_def)
+
+lemma "() = Abs_unit True"
+nitpick [expect = none]
+by (rule Unity_def)
+
+lemma "() = Abs_unit False"
+nitpick [expect = none]
+by simp
+
+lemma "Rep_unit () = True"
+nitpick [expect = none]
+by (insert Rep_unit) (simp add: unit_def)
+
+lemma "Rep_unit () = False"
+nitpick [expect = genuine]
+oops
+
+lemma "Pair a b \<equiv> Abs_Prod (Pair_Rep a b)"
+nitpick [card = 1\<midarrow>2, expect = none]
+by (rule Pair_def)
+
+lemma "Pair a b \<equiv> Abs_Prod (Pair_Rep b a)"
+nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [dont_box, expect = genuine]
+oops
+
+lemma "fst (Abs_Prod (Pair_Rep a b)) = a"
+nitpick [card = 2, expect = none]
+by (simp add: Pair_def [THEN symmetric])
+
+lemma "fst (Abs_Prod (Pair_Rep a b)) = b"
+nitpick [card = 1\<midarrow>2, expect = none]
+nitpick [dont_box, expect = genuine]
+oops
+
+lemma "a \<noteq> a' \<Longrightarrow> Pair_Rep a b \<noteq> Pair_Rep a' b"
+nitpick [expect = none]
+apply (rule ccontr)
+apply simp
+apply (drule subst [where P = "\<lambda>r. Abs_Prod r = Abs_Prod (Pair_Rep a b)"])
+ apply (rule refl)
+by (simp add: Pair_def [THEN symmetric])
+
+lemma "Abs_Prod (Rep_Prod a) = a"
+nitpick [card = 2, expect = none]
+by (rule Rep_Prod_inverse)
+
+lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inl_Rep a)"
+nitpick [card = 1, expect = none]
+by (rule Inl_def)
+
+lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inr_Rep a)"
+nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]
+oops
+
+lemma "Inl_Rep a \<noteq> Inr_Rep a"
+nitpick [expect = none]
+by (rule Inl_Rep_not_Inr_Rep)
+
+lemma "Abs_Sum (Rep_Sum a) = a"
+nitpick [card = 1\<midarrow>2, timeout = 30 s, expect = none]
+by (rule Rep_Sum_inverse)
+
+lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
+nitpick [expect = none]
+by (rule Zero_nat_def_raw)
+
+lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
+nitpick [expect = none]
+by (rule Suc_def)
+
+lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
+nitpick [expect = genuine]
+oops
+
+lemma "Abs_Nat (Rep_Nat a) = a"
+nitpick [expect = none]
+by (rule Rep_Nat_inverse)
+
+lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
+nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = unknown]
+by (rule Zero_int_def_raw)
+
+lemma "Abs_Integ (Rep_Integ a) = a"
+nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = none]
+by (rule Rep_Integ_inverse)
+
+lemma "Abs_list (Rep_list a) = a"
+nitpick [card = 1\<midarrow>2, timeout = 30 s, expect = none]
+by (rule Rep_list_inverse)
+
+record point =
+  Xcoord :: int
+  Ycoord :: int
+
+lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
+nitpick [expect = none]
+by (rule Rep_point_ext_type_inverse)
+
+lemma "Fract a b = of_int a / of_int b"
+nitpick [card = 1\<midarrow>2, expect = potential]
+by (rule Fract_of_int_quotient)
+
+lemma "Abs_Rat (Rep_Rat a) = a"
+nitpick [card = 1\<midarrow>2, expect = none]
+by (rule Rep_Rat_inverse)
+
+end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/Rational.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -1063,4 +1063,23 @@
 fun rat_of_int i = (i, 1);
 *}
 
+setup {*
+Nitpick.register_frac_type @{type_name rat}
+    [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
+     (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
+     (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
+     (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
+     (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
+     (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
+     (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
+     (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
+     (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
+     (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
+*}
+
+lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
+    number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
+    plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
+    zero_rat_inst.zero_rat
+
 end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/RealDef.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -1185,4 +1185,22 @@
 fun real_of_int i = (i, 1);
 *}
 
+setup {*
+Nitpick.register_frac_type @{type_name real}
+    [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
+     (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
+     (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
+     (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
+     (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
+     (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
+     (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
+     (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
+*}
+
+lemmas [nitpick_def] = inverse_real_inst.inverse_real
+    number_real_inst.number_of_real one_real_inst.one_real
+    ord_real_inst.less_eq_real plus_real_inst.plus_real
+    times_real_inst.times_real uminus_real_inst.uminus_real
+    zero_real_inst.zero_real
+
 end
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Tools/Nitpick/HISTORY
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/HISTORY	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,155 @@
+Version 2010
+
+  * Moved into Isabelle/HOL "Main"
+  * Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
+    "nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
+    "nitpick_ind_intro" to "nitpick_intro"
+  * Replaced "special_depth" and "skolemize_depth" options by "specialize"
+    and "skolemize"
+  * Fixed monotonicity check
+
+Version 1.2.2 (16 Oct 2009)
+
+  * Added and implemented "star_linear_preds" option
+  * Added and implemented "format" option
+  * Added and implemented "coalesce_type_vars" option
+  * Added and implemented "max_genuine" option
+  * Fixed soundness issues related to "set", "distinct", "image", "Sigma",
+    "-1::nat", subset, constructors, sort axioms, and partially applied
+    interpreted constants
+  * Fixed error in "show_consts" for boxed specialized constants
+  * Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
+  * Fixed display of Skolem constants
+  * Fixed error in "check_potential" and "check_genuine"
+  * Added boxing support for higher-order constructor parameters
+  * Changed notation used for coinductive datatypes
+  * Optimized Kodkod encoding of "If", "card", and "setsum"
+  * Improved the monotonicity check
+
+Version 1.2.1 (25 Sep 2009)
+
+  * Added explicit support for coinductive datatypes
+  * Added and implemented "box" option
+  * Added and implemented "fast_descrs" option
+  * Added and implemented "uncurry" option
+  * Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
+  * Fixed soundness issue related to nullary constructors
+  * Fixed soundness issue related to higher-order quantifiers
+  * Fixed soundness issue related to the "destroy_constrs" optimization
+  * Fixed soundness issues related to the "special_depth" optimization
+  * Added support for PicoSAT and incorporated it with the Nitpick package
+  * Added automatic detection of installed SAT solvers based on naming
+    convention
+  * Optimized handling of quantifiers by moving them inward whenever possible
+  * Optimized and improved precision of "wf" and "wfrec"
+  * Improved handling of definitions made in locales
+  * Fixed checked scope count in message shown upon interruption and timeout
+  * Added minimalistic Nitpick-like tool called Minipick
+
+Version 1.2.0 (27 Jul 2009)
+
+  * Optimized Kodkod encoding of datatypes and records
+  * Optimized coinductive definitions
+  * Fixed soundness issues related to pairs of functions
+  * Fixed soundness issue in the peephole optimizer
+  * Improved precision of non-well-founded predicates occurring positively in
+    the formula to falsify
+  * Added and implemented "destroy_constrs" option
+  * Changed semantics of "inductive_mood" option to ensure soundness
+  * Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
+    "sync_cards"
+  * Improved precision of "trancl" and "rtrancl"
+  * Optimized Kodkod encoding of "tranclp" and "rtranclp"
+  * Made detection of inconsistent scope specifications more robust
+  * Fixed a few Kodkod generation bugs that resulted in exceptions
+
+Version 1.1.1 (24 Jun 2009)
+
+  * Added "show_all" option
+  * Fixed soundness issues related to type classes
+  * Improved precision of some set constructs
+  * Fiddled with the automatic monotonicity check
+  * Fixed performance issues related to scope enumeration
+  * Fixed a few Kodkod generation bugs that resulted in exceptions or stack
+    overflows
+
+Version 1.1.0 (16 Jun 2009)
+
+  * Redesigned handling of datatypes to provide an interface baded on "card" and
+    "max", obsoleting "mult"
+  * Redesigned handling of typedefs, "rat", and "real"
+  * Made "lockstep" option a three-state option and added an automatic
+    monotonicity check
+  * Made "batch_size" a (n + 1)-state option whose default depends on whether
+    "debug" is enabled
+  * Made "debug" automatically enable "verbose"
+  * Added "destroy_equals" option
+  * Added "no_assms" option
+  * Fixed bug in computation of ground type 
+  * Fixed performance issue related to datatype acyclicity constraint generation
+  * Fixed performance issue related to axiom selection
+  * Improved precision of some well-founded inductive predicates
+  * Added more checks to guard against very large cardinalities
+  * Improved hit rate of potential counterexamples
+  * Fixed several soundness issues
+  * Optimized the Kodkod encoding to benefit more from symmetry breaking
+  * Optimized relational composition, cartesian product, and converse
+  * Added support for HaifaSat
+
+Version 1.0.3 (17 Mar 2009)
+
+  * Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
+  * Added "overlord" option to assist debugging
+  * Increased default value of "special_depth" option
+  * Fixed a bug that effectively disabled the "nitpick_const_def" attribute
+  * Ensured that no scopes are skipped when multithreading is enabled
+  * Fixed soundness issue in handling of "The", "Eps", and partial functions
+    defined using Isabelle's function package
+  * Fixed soundness issue in handling of non-definitional axioms
+  * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
+    "nat", "int", and "*"
+  * Fixed a few Kodkod generation bugs that resulted in exceptions
+  * Optimized "div", "mod", and "dvd" on "nat" and "int"
+
+Version 1.0.2 (12 Mar 2009)
+
+  * Added support for non-definitional axioms
+  * Improved Isar integration
+  * Added support for multiplicities of 0
+  * Added "max_threads" option and support for multithreaded Kodkodi
+  * Added "blocking" option to control whether Nitpick should be run
+    synchronously or asynchronously
+  * Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
+  * Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
+  * Introduced "auto_timeout" to specify Auto Nitpick's time limit
+  * Renamed the possible values for the "expect" option
+  * Renamed the "peephole" option to "peephole_optim"
+  * Added negative versions of all Boolean options and made "= true" optional
+  * Altered order of automatic SAT solver selection
+
+Version 1.0.1 (6 Mar 2009)
+
+  * Eliminated the need to import "Nitpick" to use "nitpick"
+  * Added "debug" option
+  * Replaced "specialize_funs" with the more general "special_depth" option
+  * Renamed "watch" option to "eval"
+  * Improved parsing of "card", "mult", and "iter" options
+  * Fixed a soundness bug in the "specialize_funs" optimization
+  * Increased the scope of the "specialize_funs" optimization
+  * Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
+  * Fixed a soundness bug in the "subterm property" optimization for types of
+    cardinality 1
+  * Improved the axiom selection for overloaded constants, which led to an
+    infinite loop for "Nominal.perm"
+  * Added support for multiple instantiations of non-well-founded inductive
+    predicates, which previously raised an exception
+  * Fixed a Kodkod generation bug that resulted in an exception
+  * Altered order of scope enumeration and automatic SAT solver selection
+  * Optimized "Eps", "nat_case", and "list_case"
+  * Improved output formatting
+  * Added checks to prevent infinite loops in axiom selector and constant
+    unfolding
+
+Version 1.0.0 (27 Feb 2009)
+
+  * First release
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 23 18:59:24 2009 +0200
@@ -970,15 +970,14 @@
                          $ Const (@{const_name TYPE}, _)) = true
   | is_arity_type_axiom _ = false
 (* theory -> bool -> term -> bool *)
-fun is_typedef_axiom thy only_boring (@{const "==>"} $ _ $ t2) =
-    is_typedef_axiom thy only_boring t2
-  | is_typedef_axiom thy only_boring
+fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
+    is_typedef_axiom thy boring t2
+  | is_typedef_axiom thy boring
         (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
-         $ Const (_, Type ("fun", [T as Type (s, _), _])) $ Const _ $ _)) =
-    is_typedef thy s
-    andalso not (only_boring andalso
-                 (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
-                  orelse is_frac_type thy T))
+         $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
+    boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
+               orelse is_frac_type thy (Type (s, [])))
+    andalso is_typedef thy s
   | is_typedef_axiom _ _ _ = false
 
 (* Distinguishes between (1) constant definition axioms, (2) type arity and
@@ -995,8 +994,8 @@
       |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
   in pairself (map snd) (defs, nondefs) end
 
-(* Ideally we would check against "Complex_Main", not "Quickcheck", but any
-   theory will do as long as it contains all the "axioms" and "axiomatization"
+(* Ideally we would check against "Complex_Main", not "Refute", but any theory
+   will do as long as it contains all the "axioms" and "axiomatization"
    commands. *)
 (* theory -> bool *)
 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
@@ -1040,18 +1039,20 @@
     (* theory list -> term list *)
     val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
     val specs = Defs.all_specifications_of (Theory.defs_of thy)
-    val def_names =
-      specs |> maps snd
-      |> filter #is_def |> map #name |> OrdList.make fast_string_ord
+    val def_names = specs |> maps snd |> filter #is_def |> map #name
+                    |> OrdList.make fast_string_ord
     val thys = thy :: Theory.ancestors_of thy
     val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
     val built_in_axioms = axioms_of_thys built_in_thys
     val user_axioms = axioms_of_thys user_thys
     val (built_in_defs, built_in_nondefs) =
       partition_axioms_by_definitionality thy built_in_axioms def_names
-      |> apsnd (filter (is_typedef_axiom thy false))
+      ||> filter (is_typedef_axiom thy false)
     val (user_defs, user_nondefs) =
       partition_axioms_by_definitionality thy user_axioms def_names
+    val (built_in_nondefs, user_nondefs) =
+      List.partition (is_typedef_axiom thy false) user_nondefs
+      |>> append built_in_nondefs
     val defs = built_in_built_in_defs @
                (thy |> PureThy.all_thms_of
                     |> filter (equal Thm.definitionK o Thm.get_kind o snd)
@@ -1230,30 +1231,31 @@
 (* Similar to "Refute.specialize_type" but returns all matches rather than only
    the first (preorder) match. *)
 (* theory -> styp -> term -> term list *)
-fun multi_specialize_type thy (x as (s, T)) t =
+fun multi_specialize_type thy slack (x as (s, T)) t =
   let
     (* term -> (typ * term) list -> (typ * term) list *)
     fun aux (Const (s', T')) ys =
         if s = s' then
-          (if AList.defined (op =) ys T' then
-             I
-           else if T = T' then
-             cons (T, t)
-           else
-             cons (T', Refute.monomorphic_term
-                           (Sign.typ_match thy (T', T) Vartab.empty) t)
-             handle Type.TYPE_MATCH => I) ys
+          ys |> (if AList.defined (op =) ys T' then
+                   I
+                else
+                  cons (T', Refute.monomorphic_term
+                                (Sign.typ_match thy (T', T) Vartab.empty) t)
+                  handle Type.TYPE_MATCH => I
+                       | Refute.REFUTE _ =>
+                         if slack then
+                           I
+                         else
+                           raise NOT_SUPPORTED ("too much polymorphism in \
+                                                \axiom involving " ^ quote s))
         else
           ys
       | aux _ ys = ys
   in map snd (fold_aterms aux t []) end
 
-(* theory -> const_table -> styp -> term list *)
-fun nondef_props_for_const thy table (x as (s, _)) =
-  these (Symtab.lookup table s) |> maps (multi_specialize_type thy x)
-  handle Refute.REFUTE _ =>
-         raise NOT_SUPPORTED ("too much polymorphism in axiom involving " ^
-                              quote s)
+(* theory -> bool -> const_table -> styp -> term list *)
+fun nondef_props_for_const thy slack table (x as (s, _)) =
+  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
 
 (* theory -> styp list -> term list *)
 fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
@@ -1680,7 +1682,7 @@
         (x as (s, _)) =
   case triple_lookup (const_match thy) wfs x of
     SOME (SOME b) => b
-  | _ => s = @{const_name fold_graph'}
+  | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}]
          orelse case AList.lookup (op =) (!wf_cache) x of
                   SOME (_, wf) => wf
                 | NONE =>
@@ -3025,15 +3027,15 @@
                     accum
              else if is_abs_fun thy x then
                accum |> fold (add_nondef_axiom depth)
-                             (nondef_props_for_const thy nondef_table x)
+                             (nondef_props_for_const thy false nondef_table x)
                      |> fold (add_def_axiom depth)
-                             (nondef_props_for_const thy
+                             (nondef_props_for_const thy true
                                                     (extra_table def_table s) x)
              else if is_rep_fun thy x then
                accum |> fold (add_nondef_axiom depth)
-                             (nondef_props_for_const thy nondef_table x)
+                             (nondef_props_for_const thy false nondef_table x)
                      |> fold (add_def_axiom depth)
-                             (nondef_props_for_const thy
+                             (nondef_props_for_const thy true
                                                     (extra_table def_table s) x)
                      |> add_axioms_for_term depth
                                             (Const (mate_of_rep_fun thy x))
@@ -3041,7 +3043,7 @@
              else
                accum |> user_axioms <> SOME false
                         ? fold (add_nondef_axiom depth)
-                               (nondef_props_for_const thy nondef_table x)
+                               (nondef_props_for_const thy false nondef_table x)
            end)
         |> add_axioms_for_type depth T
       | Free (_, T) => add_axioms_for_type depth T accum
diff -r 5fe67e108651 -r de6285ebcc05 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Oct 23 18:57:35 2009 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Oct 23 18:59:24 2009 +0200
@@ -55,11 +55,7 @@
    ("max_threads", ["0"]),
    ("verbose", ["false"]),
    ("debug", ["false"]),
-   ("overlord", [if exists (fn s => String.isSuffix s (getenv "HOME"))
-                           ["blanchet", "blanchette"] then
-                   "true"
-                 else
-                   "false"]),
+   ("overlord", ["false"]),
    ("show_all", ["false"]),
    ("show_skolems", ["true"]),
    ("show_datatypes", ["false"]),