src/HOL/Nitpick_Examples/Special_Nits.thy
 author hoelzl Tue Jan 18 21:37:23 2011 +0100 (2011-01-18) changeset 41654 32fe42892983 parent 41278 8e1cde88aae6 child 42208 02513eb26eb7 permissions -rw-r--r--
Gauge measure removed
 blanchet@33197  1 (* Title: HOL/Nitpick_Examples/Special_Nits.thy  blanchet@33197  2  Author: Jasmin Blanchette, TU Muenchen  blanchet@35076  3  Copyright 2009, 2010  blanchet@33197  4 blanchet@33197  5 Examples featuring Nitpick's "specialize" optimization.  blanchet@33197  6 *)  blanchet@33197  7 blanchet@33197  8 header {* Examples Featuring Nitpick's \textit{specialize} Optimization *}  blanchet@33197  9 blanchet@33197  10 theory Special_Nits  blanchet@33197  11 imports Main  blanchet@33197  12 begin  blanchet@33197  13 blanchet@41278  14 nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,  blanchet@40341  15  timeout = 60]  blanchet@33197  16 blanchet@33197  17 fun f1 :: "nat \ nat \ nat \ nat \ nat \ nat" where  blanchet@33197  18 "f1 a b c d e = a + b + c + d + e"  blanchet@33197  19 blanchet@33197  20 lemma "f1 0 0 0 0 0 = f1 0 0 0 0 (1 - 1)"  blanchet@33197  21 nitpick [expect = none]  blanchet@33197  22 nitpick [dont_specialize, expect = none]  blanchet@33197  23 sorry  blanchet@33197  24 blanchet@33197  25 lemma "f1 u v w x y = f1 y x w v u"  blanchet@33197  26 nitpick [expect = none]  blanchet@33197  27 nitpick [dont_specialize, expect = none]  blanchet@33197  28 sorry  blanchet@33197  29 blanchet@33197  30 fun f2 :: "nat \ nat \ nat \ nat \ nat \ nat" where  blanchet@33197  31 "f2 a b c d (Suc e) = a + b + c + d + e"  blanchet@33197  32 blanchet@33197  33 lemma "f2 0 0 0 0 0 = f2 (1 - 1) 0 0 0 0"  blanchet@33197  34 nitpick [expect = none]  blanchet@33197  35 nitpick [dont_specialize, expect = none]  blanchet@33197  36 sorry  blanchet@33197  37 blanchet@33197  38 lemma "f2 0 (v - v) 0 (x - x) 0 = f2 (u - u) 0 (w - w) 0 (y - y)"  blanchet@33197  39 nitpick [expect = none]  blanchet@33197  40 nitpick [dont_specialize, expect = none]  blanchet@33197  41 sorry  blanchet@33197  42 blanchet@33197  43 lemma "f2 1 0 0 0 0 = f2 0 1 0 0 0"  blanchet@33197  44 nitpick [expect = genuine]  blanchet@33197  45 nitpick [dont_specialize, expect = genuine]  blanchet@33197  46 oops  blanchet@33197  47 blanchet@33197  48 lemma "f2 0 0 0 0 0 = f2 0 0 0 0 0"  blanchet@33197  49 nitpick [expect = none]  blanchet@33197  50 nitpick [dont_specialize, expect = none]  blanchet@33197  51 sorry  blanchet@33197  52 blanchet@33197  53 fun f3 :: "nat \ nat \ nat \ nat \ nat \ nat" where  blanchet@33197  54 "f3 (Suc a) b 0 d (Suc e) = a + b + d + e" |  blanchet@33197  55 "f3 0 b 0 d 0 = b + d"  blanchet@33197  56 blanchet@33197  57 lemma "f3 a b c d e = f3 e d c b a"  blanchet@33197  58 nitpick [expect = genuine]  blanchet@33197  59 nitpick [dont_specialize, expect = genuine]  blanchet@33197  60 oops  blanchet@33197  61 blanchet@33197  62 lemma "f3 a b c d a = f3 a d c d a"  blanchet@33197  63 nitpick [expect = genuine]  blanchet@33197  64 nitpick [dont_specialize, expect = genuine]  blanchet@33197  65 oops  blanchet@33197  66 blanchet@33197  67 lemma "\c < 1; a \ e; e \ a\ \ f3 a b c d a = f3 e d c b e"  blanchet@33197  68 nitpick [expect = none]  blanchet@33197  69 nitpick [dont_specialize, expect = none]  blanchet@33197  70 sorry  blanchet@33197  71 blanchet@33197  72 lemma "(\u. a = u \ f3 a a a a a = f3 u u u u u)  blanchet@33197  73  \ (\u. b = u \ f3 b b u b b = f3 u u b u u)"  blanchet@33197  74 nitpick [expect = none]  blanchet@33197  75 nitpick [dont_specialize, expect = none]  blanchet@33197  76 sorry  blanchet@33197  77 blanchet@33197  78 function f4 :: "nat \ nat \ nat" where  blanchet@33197  79 "f4 x x = 1" |  blanchet@33197  80 "f4 y z = (if y = z then 1 else 0)"  blanchet@33197  81 by auto  blanchet@33197  82 termination by lexicographic_order  blanchet@33197  83 blanchet@33197  84 lemma "f4 a b = f4 b a"  blanchet@33197  85 nitpick [expect = none]  blanchet@33197  86 nitpick [dont_specialize, expect = none]  blanchet@33197  87 sorry  blanchet@33197  88 blanchet@33197  89 lemma "f4 a (Suc a) = f4 a a"  blanchet@33197  90 nitpick [expect = genuine]  blanchet@33197  91 nitpick [dont_specialize, expect = genuine]  blanchet@33197  92 oops  blanchet@33197  93 blanchet@33197  94 fun f5 :: "(nat \ nat) \ nat \ nat" where  blanchet@33197  95 "f5 f (Suc a) = f a"  blanchet@33197  96 blanchet@33197  97 lemma "\one \ {1}. \two \ {2}.  blanchet@33197  98  f5 (\a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"  blanchet@33197  99 nitpick [expect = none]  blanchet@33197  100 nitpick [dont_specialize, expect = none]  blanchet@33197  101 sorry  blanchet@33197  102 blanchet@33197  103 lemma "\two \ {2}. \one \ {1}.  blanchet@33197  104  f5 (\a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"  blanchet@33197  105 nitpick [expect = none]  blanchet@33197  106 nitpick [dont_specialize, expect = none]  blanchet@33197  107 sorry  blanchet@33197  108 blanchet@33197  109 lemma "\one \ {1}. \two \ {2}.  blanchet@33197  110  f5 (\a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"  blanchet@35312  111 nitpick [expect = genuine]  blanchet@33737  112 oops  blanchet@33197  113 blanchet@33197  114 lemma "\two \ {2}. \one \ {1}.  blanchet@33197  115  f5 (\a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"  blanchet@35312  116 nitpick [expect = genuine]  blanchet@33737  117 oops  blanchet@33197  118 blanchet@33197  119 lemma "\a. g a = a  blanchet@33197  120  \ \one \ {1}. \two \ {2}. f5 g x =  blanchet@33197  121  f5 (\a. if a = one then 1 else if a = two then 2 else a) x"  blanchet@33197  122 nitpick [expect = none]  blanchet@33197  123 nitpick [dont_specialize, expect = none]  blanchet@33197  124 sorry  blanchet@33197  125 blanchet@33197  126 lemma "\a. g a = a  blanchet@33197  127  \ \one \ {2}. \two \ {1}. f5 g x =  blanchet@33197  128  f5 (\a. if a = one then 1 else if a = two then 2 else a) x"  blanchet@33197  129 nitpick [expect = potential]  blanchet@33197  130 nitpick [dont_specialize, expect = potential]  blanchet@33197  131 sorry  blanchet@33197  132 blanchet@33197  133 lemma "\a. g a = a  blanchet@33197  134  \ \b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\nat).  blanchet@33197  135  b\<^isub>1 < b\<^isub>11 \ f5 g x = f5 (\a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"  blanchet@34126  136 nitpick [expect = potential]  blanchet@33197  137 nitpick [dont_specialize, expect = none]  blanchet@33197  138 nitpick [dont_box, expect = none]  blanchet@33197  139 nitpick [dont_box, dont_specialize, expect = none]  blanchet@33197  140 sorry  blanchet@33197  141 blanchet@33197  142 lemma "\a. g a = a  blanchet@33197  143  \ \b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\nat).  blanchet@33197  144  b\<^isub>1 < b\<^isub>11  blanchet@33197  145  \ f5 g x = f5 (\a. if b\<^isub>1 < b\<^isub>11 then  blanchet@33197  146  a  blanchet@33197  147  else  blanchet@33197  148  h b\<^isub>2 + h b\<^isub>3 + h b\<^isub>4 + h b\<^isub>5 + h b\<^isub>6 + h b\<^isub>7 + h b\<^isub>8  blanchet@33197  149  + h b\<^isub>9 + h b\<^isub>10) x"  blanchet@33197  150 nitpick [card nat = 2, card 'a = 1, expect = none]  blanchet@33197  151 nitpick [card nat = 2, card 'a = 1, dont_box, expect = none]  blanchet@33197  152 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = none]  blanchet@33197  153 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, expect = none]  blanchet@33197  154 sorry  blanchet@33197  155 blanchet@33197  156 lemma "\a. g a = a  blanchet@33197  157  \ \b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\nat).  blanchet@33197  158  b\<^isub>1 < b\<^isub>11  blanchet@33197  159  \ f5 g x = f5 (\a. if b\<^isub>1 \ b\<^isub>11 then  blanchet@33197  160  a  blanchet@33197  161  else  blanchet@33197  162  h b\<^isub>2 + h b\<^isub>3 + h b\<^isub>4 + h b\<^isub>5 + h b\<^isub>6 + h b\<^isub>7 + h b\<^isub>8  blanchet@33197  163  + h b\<^isub>9 + h b\<^isub>10) x"  blanchet@34124  164 nitpick [card nat = 2, card 'a = 1, expect = potential]  blanchet@33197  165 nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]  blanchet@33197  166 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]  blanchet@33197  167 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,  blanchet@33197  168  expect = potential]  blanchet@33197  169 oops  blanchet@33197  170 blanchet@33197  171 end