--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Mar 03 22:33:22 2014 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nitpick_Examples/Manual_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009-2013
+ Copyright 2009-2014
Examples from the Nitpick manual.
*)
@@ -15,10 +15,12 @@
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"
@@ -28,12 +30,14 @@
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"
@@ -47,6 +51,7 @@
(* 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"
@@ -61,6 +66,7 @@
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"
@@ -81,6 +87,7 @@
nitpick [card nat = 2, expect = none]
oops
+
subsection {* 2.6. Inductive Datatypes *}
lemma "hd (xs @ [y, y]) = hd xs"
@@ -92,6 +99,7 @@
nitpick [show_datatypes, expect = genuine]
oops
+
subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
definition "three = {0\<Colon>nat, 1, 2}"
@@ -149,6 +157,7 @@
nitpick [show_datatypes, expect = genuine]
oops
+
subsection {* 2.8. Inductive and Coinductive Predicates *}
inductive even where
@@ -191,6 +200,7 @@
nitpick [card nat = 4, show_consts, expect = genuine]
oops
+
subsection {* 2.9. Coinductive Datatypes *}
codatatype 'a llist = LNil | LCons 'a "'a llist"
@@ -211,6 +221,7 @@
nitpick [card = 1\<emdash>5, expect = none]
sorry
+
subsection {* 2.10. Boxing *}
datatype tm = Var nat | Lam tm | App tm tm
@@ -247,6 +258,7 @@
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)"
@@ -258,6 +270,7 @@
nitpick [expect = genuine]
oops
+
subsection {* 2.12. Inductive Properties *}
inductive_set reach where
@@ -286,45 +299,12 @@
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
@@ -399,6 +379,7 @@
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"