author blanchet Fri, 23 Sep 2011 10:31:12 +0200 changeset 45053 54c832311598 parent 45052 d51bc5756650 child 45054 73accf69135d child 45059 28d3e387f22e
synchronized section names with manual
```--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Sep 23 00:11:29 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Sep 23 10:31:12 2011 +0200
@@ -15,12 +15,12 @@
imports Main "~~/src/HOL/Library/Quotient_Product" RealDef
begin

-chapter {* 3. First Steps *}
+chapter {* 2. First Steps *}

nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
timeout = 240]

-subsection {* 3.1. Propositional Logic *}
+subsection {* 2.1. Propositional Logic *}

lemma "P \<longleftrightarrow> Q"
nitpick [expect = genuine]
@@ -29,13 +29,13 @@
nitpick [expect = genuine] 2
oops

-subsection {* 3.2. Type Variables *}
+subsection {* 2.2. Type Variables *}

lemma "P x \<Longrightarrow> P (THE y. P y)"
nitpick [verbose, expect = genuine]
oops

-subsection {* 3.3. Constants *}
+subsection {* 2.3. Constants *}

lemma "P x \<Longrightarrow> P (THE y. P y)"
nitpick [show_consts, expect = genuine]
@@ -49,7 +49,7 @@
apply (metis the_equality)
done

-subsection {* 3.4. Skolemization *}
+subsection {* 2.4. Skolemization *}

lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
nitpick [expect = genuine]
@@ -63,7 +63,7 @@
nitpick [expect = genuine]
oops

-subsection {* 3.5. Natural Numbers and Integers *}
+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]
@@ -82,7 +82,7 @@
nitpick [card nat = 2, expect = none]
oops

-subsection {* 3.6. Inductive Datatypes *}
+subsection {* 2.6. Inductive Datatypes *}

lemma "hd (xs @ [y, y]) = hd xs"
nitpick [expect = genuine]
@@ -93,7 +93,7 @@
nitpick [show_datatypes, expect = genuine]
oops

-subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
+subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}

typedef three = "{0\<Colon>nat, 1, 2}"
by blast
@@ -148,7 +148,7 @@
nitpick [show_datatypes, expect = genuine]
oops

-subsection {* 3.8. Inductive and Coinductive Predicates *}
+subsection {* 2.8. Inductive and Coinductive Predicates *}

inductive even where
"even 0" |
@@ -190,7 +190,7 @@
nitpick [card nat = 10, show_consts, expect = genuine]
oops

-subsection {* 3.9. Coinductive Datatypes *}
+subsection {* 2.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
@@ -230,7 +230,7 @@
nitpick [card = 1\<emdash>5, expect = none]
sorry

-subsection {* 3.10. Boxing *}
+subsection {* 2.10. Boxing *}

datatype tm = Var nat | Lam tm | App tm tm

@@ -266,7 +266,7 @@
nitpick [card = 1\<emdash>5, expect = none]
sorry

-subsection {* 3.11. Scope Monotonicity *}
+subsection {* 2.11. Scope Monotonicity *}

lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
nitpick [verbose, expect = genuine]
@@ -277,7 +277,7 @@
nitpick [expect = genuine]
oops

-subsection {* 3.12. Inductive Properties *}
+subsection {* 2.12. Inductive Properties *}

inductive_set reach where
"(4\<Colon>nat) \<in> reach" |
@@ -340,11 +340,11 @@
by auto
qed

-section {* 4. Case Studies *}
+section {* 3. Case Studies *}

nitpick_params [max_potential = 0]

-subsection {* 4.1. A Context-Free Grammar *}
+subsection {* 3.1. A Context-Free Grammar *}

datatype alphabet = a | b

@@ -418,7 +418,7 @@
nitpick [card = 1\<emdash>5, expect = none]
sorry

-subsection {* 4.2. AA Trees *}
+subsection {* 3.2. AA Trees *}

datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
```