src/HOL/Nitpick_Examples/Manual_Nits.thy
changeset 55888 cac1add157e8
parent 55072 8488fdc4ddc0
child 55889 6bfbec3dff62
     1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 16:44:46 2014 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     1.5      Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2009-2013
     1.7 +    Copyright   2009-2014
     1.8  
     1.9  Examples from the Nitpick manual.
    1.10  *)
    1.11 @@ -15,10 +15,12 @@
    1.12  imports Main Real "~~/src/HOL/Library/Quotient_Product"
    1.13  begin
    1.14  
    1.15 -chapter {* 2. First Steps *}
    1.16 +
    1.17 +section {* 2. First Steps *}
    1.18  
    1.19  nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    1.20  
    1.21 +
    1.22  subsection {* 2.1. Propositional Logic *}
    1.23  
    1.24  lemma "P \<longleftrightarrow> Q"
    1.25 @@ -28,12 +30,14 @@
    1.26  nitpick [expect = genuine] 2
    1.27  oops
    1.28  
    1.29 +
    1.30  subsection {* 2.2. Type Variables *}
    1.31  
    1.32  lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
    1.33  nitpick [verbose, expect = genuine]
    1.34  oops
    1.35  
    1.36 +
    1.37  subsection {* 2.3. Constants *}
    1.38  
    1.39  lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
    1.40 @@ -47,6 +51,7 @@
    1.41  (* sledgehammer *)
    1.42  by (metis the_equality)
    1.43  
    1.44 +
    1.45  subsection {* 2.4. Skolemization *}
    1.46  
    1.47  lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
    1.48 @@ -61,6 +66,7 @@
    1.49  nitpick [expect = genuine]
    1.50  oops
    1.51  
    1.52 +
    1.53  subsection {* 2.5. Natural Numbers and Integers *}
    1.54  
    1.55  lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    1.56 @@ -81,6 +87,7 @@
    1.57  nitpick [card nat = 2, expect = none]
    1.58  oops
    1.59  
    1.60 +
    1.61  subsection {* 2.6. Inductive Datatypes *}
    1.62  
    1.63  lemma "hd (xs @ [y, y]) = hd xs"
    1.64 @@ -92,6 +99,7 @@
    1.65  nitpick [show_datatypes, expect = genuine]
    1.66  oops
    1.67  
    1.68 +
    1.69  subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
    1.70  
    1.71  definition "three = {0\<Colon>nat, 1, 2}"
    1.72 @@ -149,6 +157,7 @@
    1.73  nitpick [show_datatypes, expect = genuine]
    1.74  oops
    1.75  
    1.76 +
    1.77  subsection {* 2.8. Inductive and Coinductive Predicates *}
    1.78  
    1.79  inductive even where
    1.80 @@ -191,6 +200,7 @@
    1.81  nitpick [card nat = 4, show_consts, expect = genuine]
    1.82  oops
    1.83  
    1.84 +
    1.85  subsection {* 2.9. Coinductive Datatypes *}
    1.86  
    1.87  codatatype 'a llist = LNil | LCons 'a "'a llist"
    1.88 @@ -211,6 +221,7 @@
    1.89  nitpick [card = 1\<emdash>5, expect = none]
    1.90  sorry
    1.91  
    1.92 +
    1.93  subsection {* 2.10. Boxing *}
    1.94  
    1.95  datatype tm = Var nat | Lam tm | App tm tm
    1.96 @@ -247,6 +258,7 @@
    1.97  nitpick [card = 1\<emdash>5, expect = none]
    1.98  sorry
    1.99  
   1.100 +
   1.101  subsection {* 2.11. Scope Monotonicity *}
   1.102  
   1.103  lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
   1.104 @@ -258,6 +270,7 @@
   1.105  nitpick [expect = genuine]
   1.106  oops
   1.107  
   1.108 +
   1.109  subsection {* 2.12. Inductive Properties *}
   1.110  
   1.111  inductive_set reach where
   1.112 @@ -286,45 +299,12 @@
   1.113  lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
   1.114  by (induct set: reach) arith+
   1.115  
   1.116 -datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
   1.117 -
   1.118 -primrec labels where
   1.119 -"labels (Leaf a) = {a}" |
   1.120 -"labels (Branch t u) = labels t \<union> labels u"
   1.121 -
   1.122 -primrec swap where
   1.123 -"swap (Leaf c) a b =
   1.124 - (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
   1.125 -"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
   1.126 -
   1.127 -lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
   1.128 -(* nitpick *)
   1.129 -proof (induct t)
   1.130 -  case Leaf thus ?case by simp
   1.131 -next
   1.132 -  case (Branch t u) thus ?case
   1.133 -  (* nitpick *)
   1.134 -  nitpick [non_std, show_all, expect = genuine]
   1.135 -oops
   1.136 -
   1.137 -lemma "labels (swap t a b) =
   1.138 -       (if a \<in> labels t then
   1.139 -          if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
   1.140 -        else
   1.141 -          if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
   1.142 -(* nitpick *)
   1.143 -proof (induct t)
   1.144 -  case Leaf thus ?case by simp
   1.145 -next
   1.146 -  case (Branch t u) thus ?case
   1.147 -  nitpick [non_std, card = 1\<emdash>4, expect = none]
   1.148 -  by auto
   1.149 -qed
   1.150  
   1.151  section {* 3. Case Studies *}
   1.152  
   1.153  nitpick_params [max_potential = 0]
   1.154  
   1.155 +
   1.156  subsection {* 3.1. A Context-Free Grammar *}
   1.157  
   1.158  datatype alphabet = a | b
   1.159 @@ -399,6 +379,7 @@
   1.160  nitpick [card = 1\<emdash>5, expect = none]
   1.161  sorry
   1.162  
   1.163 +
   1.164  subsection {* 3.2. AA Trees *}
   1.165  
   1.166  datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"