src/HOL/Nitpick_Examples/Pattern_Nits.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
@@ -0,0 +1,138 @@
+(*  Title:      HOL/Nitpick_Examples/Pattern_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2009
+
+Examples featuring Nitpick's "destroy_constrs" optimization.
+*)
+
+header {* Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization *}
+
+theory Pattern_Nits
+imports Main
+begin
+
+nitpick_params [card = 14]
+
+lemma "x = (case u of () \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case b of True \<Rightarrow> x | False \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case p of (x, y) \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> n)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case opt of None \<Rightarrow> x | Some y \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case xs of [] \<Rightarrow> x | y # ys \<Rightarrow> y)"
+nitpick [expect = genuine]
+oops
+
+lemma "x = (case xs of
+              [] \<Rightarrow> x
+            | y # ys \<Rightarrow>
+              (case ys of
+                 [] \<Rightarrow> x
+               | z # zs \<Rightarrow>
+                 (case z of
+                    None \<Rightarrow> x
+                  | Some p \<Rightarrow>
+                    (case p of
+                       (a, b) \<Rightarrow> b))))"
+nitpick [expect = genuine]
+oops
+
+fun f1 where
+"f1 x () = x"
+
+lemma "x = f1 y u"
+nitpick [expect = genuine]
+oops
+
+fun f2 where
+"f2 x _ True = x" |
+"f2 _ y False = y"
+
+lemma "x = f2 x y b"
+nitpick [expect = genuine]
+oops
+
+fun f3 where
+"f3 (_, y) = y"
+
+lemma "x = f3 p"
+nitpick [expect = genuine]
+oops
+
+fun f4 where
+"f4 x 0 = x" |
+"f4 _ (Suc n) = n"
+
+lemma "x = f4 x n"
+nitpick [expect = genuine]
+oops
+
+fun f5 where
+"f5 x None = x" |
+"f5 _ (Some y) = y"
+
+lemma "x = f5 x opt"
+nitpick [expect = genuine]
+oops
+
+fun f6 where
+"f6 x [] = x" |
+"f6 _ (y # ys) = y"
+
+lemma "x = f6 x xs"
+nitpick [expect = genuine]
+oops
+
+fun f7 where
+"f7 _ (y # Some (a, b) # zs) = b" |
+"f7 x (y # None # zs) = x" |
+"f7 x [y] = x" |
+"f7 x [] = x"
+
+lemma "x = f7 x xs"
+nitpick [expect = genuine]
+oops
+
+lemma "u = ()"
+nitpick [expect = none]
+sorry
+
+lemma "\<exists>y. (b::bool) = y"
+nitpick [expect = none]
+sorry
+
+lemma "\<exists>x y. p = (x, y)"
+nitpick [expect = none]
+sorry
+
+lemma "\<exists>x. n = Suc x"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>y. x = Some y"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>y ys. xs = y # ys"
+nitpick [expect = genuine]
+oops
+
+lemma "\<exists>y a b zs. x = (y # Some (a, b) # zs)"
+nitpick [expect = genuine]
+oops
+
+end