src/HOL/Nitpick_Examples/Manual_Nits.thy

 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009-2013
+    Copyright   2009-2014
 
 Examples from the Nitpick manual.
 *)
 
 header {* Examples from the Nitpick Manual *}

 
 theory Manual_Nits
 imports Main Real "~~/src/HOL/Library/Quotient_Product"
 begin
 
-chapter {* 2. First Steps *}
+
+section {* 2. First Steps *}
 
 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
+
 
 subsection {* 2.1. Propositional Logic *}
 
 lemma "P \<longleftrightarrow> Q"
 nitpick [expect = genuine]
 apply auto
 nitpick [expect = genuine] 1
 nitpick [expect = genuine] 2
 oops
 
+
 subsection {* 2.2. Type Variables *}
 
 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [verbose, expect = genuine]
 oops
+
 
 subsection {* 2.3. Constants *}
 
 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [show_consts, expect = genuine]

 nitpick [expect = none]
 nitpick [card 'a = 1\<emdash>50, expect = none]
 (* sledgehammer *)
 by (metis the_equality)
 
+
 subsection {* 2.4. Skolemization *}
 
 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
 nitpick [expect = genuine]
 oops

 oops
 
 lemma "refl r \<Longrightarrow> sym r"
 nitpick [expect = genuine]
 oops
+
 
 subsection {* 2.5. Natural Numbers and Integers *}
 
 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
 nitpick [expect = genuine]

 lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
 nitpick [card nat = 1, expect = genuine]
 nitpick [card nat = 2, expect = none]
 oops
 
+
 subsection {* 2.6. Inductive Datatypes *}
 
 lemma "hd (xs @ [y, y]) = hd xs"
 nitpick [expect = genuine]
 nitpick [show_consts, show_datatypes, expect = genuine]
 oops
 
 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
 nitpick [show_datatypes, expect = genuine]
 oops
+
 
 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
 
 definition "three = {0\<Colon>nat, 1, 2}"
 typedef three = three

 
 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
 nitpick [show_datatypes, expect = genuine]
 oops
 
+
 subsection {* 2.8. Inductive and Coinductive Predicates *}
 
 inductive even where
 "even 0" |
 "even n \<Longrightarrow> even (Suc (Suc n))"

 
 lemma "odd n \<Longrightarrow> odd (n - 2)"
 nitpick [card nat = 4, show_consts, expect = genuine]
 oops
 
+
 subsection {* 2.9. Coinductive Datatypes *}
 
 codatatype 'a llist = LNil | LCons 'a "'a llist"
 
 primcorec iterates where

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

 
 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>2 \<sigma> t = t"
 nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
+
 subsection {* 2.11. Scope Monotonicity *}
 
 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
 nitpick [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]
 oops
+
 
 subsection {* 2.12. Inductive Properties *}
 
 inductive_set reach where
 "(4\<Colon>nat) \<in> reach" |

 oops
 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
 by (induct set: reach) arith+
 
-datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
-
-primrec labels where
-"labels (Leaf a) = {a}" |
-"labels (Branch t u) = labels t \<union> labels u"
-
-primrec swap where
-"swap (Leaf c) a b =
- (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
-"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
-
-lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
-(* nitpick *)
-proof (induct t)
-  case Leaf thus ?case by simp
-next
-  case (Branch t u) thus ?case
-  (* nitpick *)
-  nitpick [non_std, show_all, expect = genuine]
-oops
-
-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 *)
-proof (induct t)
-  case Leaf thus ?case by simp
-next
-  case (Branch t u) thus ?case
-  nitpick [non_std, card = 1\<emdash>4, expect = none]
-  by auto
-qed
 
 section {* 3. Case Studies *}
 
 nitpick_params [max_potential = 0]
+
 
 subsection {* 3.1. A Context-Free Grammar *}
 
 datatype alphabet = a | b
 

 "w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
 "w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
 nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
+
 subsection {* 3.2. AA Trees *}
 
 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
 
 primrec data where