src/HOL/Nitpick_Examples/Manual_Nits.thy

 lemma "\<exists>n. even n \<and> even (Suc n)"
 nitpick [card nat = 50, unary_ints, verbose, expect = potential]
 oops
 
 lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
-nitpick [card nat = 50, unary_ints, verbose, expect = genuine]
+nitpick [card nat = 50, unary_ints, expect = genuine]
 oops
 
 inductive even' where
 "even' (0\<Colon>nat)" |
 "even' 2" |

 oops
 
 subsection {* 3.9. Coinductive Datatypes *}
 
 (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
-we cannot rely on its presence, we expediently provide our own axiomatization.
-The examples also work unchanged with Lochbihler's "Coinductive_List" theory. *)
+   we cannot rely on its presence, we expediently provide our own
+   axiomatization. The examples also work unchanged with Lochbihler's
+   "Coinductive_List" theory. *)
 
 typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
 
 definition LNil where
 "LNil = Abs_llist (Inl [])"

 nitpick [verbose, expect = genuine]
 oops
 
 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
 nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
 sorry
 
 subsection {* 3.10. Boxing *}
 
 datatype tm = Var nat | Lam tm | App tm tm

 
 subsection {* 3.11. Scope Monotonicity *}
 
 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
 nitpick [verbose, expect = genuine]
-nitpick [card = 8, verbose, expect = genuine]
 oops
 
 lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
 nitpick [mono, expect = none]
 nitpick [expect = genuine]

 "(4\<Colon>nat) \<in> reach" |
 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
-nitpick [card = 1\<midarrow>5, bits = 1\<midarrow>5, expect = none]
+(* nitpick *)
 apply (induct set: reach)
   apply auto
- nitpick [card = 1\<midarrow>5, bits = 1\<midarrow>5, expect = none]
+ nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
  apply (thin_tac "n \<in> reach")
  nitpick [expect = genuine]
 oops
 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
-nitpick [card = 1\<midarrow>5, bits = 1\<midarrow>5, expect = none]
+(* nitpick *)
 apply (induct set: reach)
   apply auto
- nitpick [card = 1\<midarrow>5, bits = 1\<midarrow>5, expect = none]
+ nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
  apply (thin_tac "n \<in> reach")
  nitpick [expect = genuine]
 oops
 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"

 (* nitpick *)
 proof (induct t)
   case Leaf thus ?case by simp
 next
   case (Branch t u) thus ?case
-  nitpick [non_std, card = 1\<midarrow>5, expect = none]
+  nitpick [non_std, card = 1\<midarrow>4, expect = none]
   by auto
 qed
 
 section {* 4. Case Studies *}