src/HOL/Nitpick_Examples/Pattern_Nits.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 54680 93f6d33a754e child 63167 0909deb8059b permissions -rw-r--r--
modernized header uniformly as section;
 blanchet@33197  1 (* Title: HOL/Nitpick_Examples/Pattern_Nits.thy  blanchet@33197  2  Author: Jasmin Blanchette, TU Muenchen  blanchet@45035  3  Copyright 2009-2011  blanchet@33197  4 blanchet@33197  5 Examples featuring Nitpick's "destroy_constrs" optimization.  blanchet@33197  6 *)  blanchet@33197  7 wenzelm@58889  8 section {* Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization *}  blanchet@33197  9 blanchet@33197  10 theory Pattern_Nits  blanchet@33197  11 imports Main  blanchet@33197  12 begin  blanchet@33197  13 blanchet@54680  14 nitpick_params [verbose, card = 8, max_potential = 0, sat_solver = MiniSat_JNI,  krauss@42208  15  max_threads = 1, timeout = 240]  blanchet@33197  16 blanchet@33197  17 lemma "x = (case u of () \ y)"  blanchet@33197  18 nitpick [expect = genuine]  blanchet@33197  19 oops  blanchet@33197  20 blanchet@33197  21 lemma "x = (case b of True \ x | False \ y)"  blanchet@33197  22 nitpick [expect = genuine]  blanchet@33197  23 oops  blanchet@33197  24 blanchet@33197  25 lemma "x = (case p of (x, y) \ y)"  blanchet@33197  26 nitpick [expect = genuine]  blanchet@33197  27 oops  blanchet@33197  28 blanchet@33197  29 lemma "x = (case n of 0 \ x | Suc n \ n)"  blanchet@33197  30 nitpick [expect = genuine]  blanchet@33197  31 oops  blanchet@33197  32 blanchet@33197  33 lemma "x = (case opt of None \ x | Some y \ y)"  blanchet@33197  34 nitpick [expect = genuine]  blanchet@33197  35 oops  blanchet@33197  36 blanchet@33197  37 lemma "x = (case xs of [] \ x | y # ys \ y)"  blanchet@33197  38 nitpick [expect = genuine]  blanchet@33197  39 oops  blanchet@33197  40 blanchet@33197  41 lemma "x = (case xs of  blanchet@33197  42  [] \ x  blanchet@33197  43  | y # ys \  blanchet@33197  44  (case ys of  blanchet@33197  45  [] \ x  blanchet@33197  46  | z # zs \  blanchet@33197  47  (case z of  blanchet@33197  48  None \ x  blanchet@33197  49  | Some p \  blanchet@33197  50  (case p of  blanchet@33197  51  (a, b) \ b))))"  blanchet@33197  52 nitpick [expect = genuine]  blanchet@33197  53 oops  blanchet@33197  54 blanchet@33197  55 fun f1 where  blanchet@33197  56 "f1 x () = x"  blanchet@33197  57 blanchet@33197  58 lemma "x = f1 y u"  blanchet@33197  59 nitpick [expect = genuine]  blanchet@33197  60 oops  blanchet@33197  61 blanchet@33197  62 fun f2 where  blanchet@33197  63 "f2 x _ True = x" |  blanchet@33197  64 "f2 _ y False = y"  blanchet@33197  65 blanchet@33197  66 lemma "x = f2 x y b"  blanchet@33197  67 nitpick [expect = genuine]  blanchet@33197  68 oops  blanchet@33197  69 blanchet@33197  70 fun f3 where  blanchet@33197  71 "f3 (_, y) = y"  blanchet@33197  72 blanchet@33197  73 lemma "x = f3 p"  blanchet@33197  74 nitpick [expect = genuine]  blanchet@33197  75 oops  blanchet@33197  76 blanchet@33197  77 fun f4 where  blanchet@33197  78 "f4 x 0 = x" |  blanchet@33197  79 "f4 _ (Suc n) = n"  blanchet@33197  80 blanchet@33197  81 lemma "x = f4 x n"  blanchet@33197  82 nitpick [expect = genuine]  blanchet@33197  83 oops  blanchet@33197  84 blanchet@33197  85 fun f5 where  blanchet@33197  86 "f5 x None = x" |  blanchet@33197  87 "f5 _ (Some y) = y"  blanchet@33197  88 blanchet@33197  89 lemma "x = f5 x opt"  blanchet@33197  90 nitpick [expect = genuine]  blanchet@33197  91 oops  blanchet@33197  92 blanchet@33197  93 fun f6 where  blanchet@33197  94 "f6 x [] = x" |  blanchet@33197  95 "f6 _ (y # ys) = y"  blanchet@33197  96 blanchet@33197  97 lemma "x = f6 x xs"  blanchet@33197  98 nitpick [expect = genuine]  blanchet@33197  99 oops  blanchet@33197  100 blanchet@33197  101 fun f7 where  blanchet@33197  102 "f7 _ (y # Some (a, b) # zs) = b" |  blanchet@33197  103 "f7 x (y # None # zs) = x" |  blanchet@33197  104 "f7 x [y] = x" |  blanchet@33197  105 "f7 x [] = x"  blanchet@33197  106 blanchet@33197  107 lemma "x = f7 x xs"  blanchet@33197  108 nitpick [expect = genuine]  blanchet@33197  109 oops  blanchet@33197  110 blanchet@33197  111 lemma "u = ()"  blanchet@33197  112 nitpick [expect = none]  blanchet@33197  113 sorry  blanchet@33197  114 blanchet@33197  115 lemma "\y. (b::bool) = y"  blanchet@33197  116 nitpick [expect = none]  blanchet@33197  117 sorry  blanchet@33197  118 blanchet@33197  119 lemma "\x y. p = (x, y)"  blanchet@33197  120 nitpick [expect = none]  blanchet@33197  121 sorry  blanchet@33197  122 blanchet@33197  123 lemma "\x. n = Suc x"  blanchet@33197  124 nitpick [expect = genuine]  blanchet@33197  125 oops  blanchet@33197  126 blanchet@33197  127 lemma "\y. x = Some y"  blanchet@33197  128 nitpick [expect = genuine]  blanchet@33197  129 oops  blanchet@33197  130 blanchet@33197  131 lemma "\y ys. xs = y # ys"  blanchet@33197  132 nitpick [expect = genuine]  blanchet@33197  133 oops  blanchet@33197  134 blanchet@35284  135 lemma "\y a b zs. x = y # Some (a, b) # zs"  blanchet@33197  136 nitpick [expect = genuine]  blanchet@33197  137 oops  blanchet@33197  138 blanchet@33197  139 end