src/HOL/Nitpick_Examples/Manual_Nits.thy

 imports Main Coinductive_List Quotient_Product RealDef
 begin
 
 chapter {* 3. First Steps *}
 
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 15 s]
 
 subsection {* 3.1. Propositional Logic *}
 
 lemma "P \<longleftrightarrow> Q"
 nitpick

 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
 nitpick [card nat = 100, check_potential]
 oops
 
 lemma "P Suc"
-nitpick [card = 1-6]
+nitpick
 oops
 
 lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
 nitpick [card nat = 1]
 nitpick [card nat = 2]

 "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, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
+nitpick [card nat = 10, unary_ints, verbose, show_consts]
 oops
 
 lemma "even' (n - 2) \<Longrightarrow> even' n"
 nitpick [card nat = 10, show_consts]
 oops

 "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]
+(* 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
+nitpick [card = 1\<midarrow>6]
 sorry
 
 subsection {* 3.11. Scope Monotonicity *}
 
 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"

 "(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
+nitpick [unary_ints]
 apply (induct set: reach)
   apply auto
  nitpick
  apply (thin_tac "n \<in> reach")
  nitpick
 oops
 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
-nitpick
+nitpick [unary_ints]
 apply (induct set: reach)
   apply auto
  nitpick
  apply (thin_tac "n \<in> reach")
  nitpick

 lemma "labels (swap t a b) =
        (if a \<in> labels t then
           if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
         else
           if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
-nitpick
+(* nitpick *)
 proof (induct t)
   case Leaf thus ?case by simp
 next
   case (Branch t u) thus ?case
-  nitpick [non_std "'a bin_tree", show_consts]
+  nitpick [non_std, show_all]
   by auto
 qed
 
 section {* 4. Case Studies *}