src/HOL/Nitpick_Examples/Special_Nits.thy
 author wenzelm Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) changeset 35115 446c5063e4fd parent 35078 6fd1052fe463 child 35284 9edc2bd6d2bd permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/Nitpick_Examples/Special_Nits.thy

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2009, 2010

     4

     5 Examples featuring Nitpick's "specialize" optimization.

     6 *)

     7

     8 header {* Examples Featuring Nitpick's \textit{specialize} Optimization *}

     9

    10 theory Special_Nits

    11 imports Main

    12 begin

    13

    14 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,

    15                 card = 4]

    16

    17 fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

    18 "f1 a b c d e = a + b + c + d + e"

    19

    20 lemma "f1 0 0 0 0 0 = f1 0 0 0 0 (1 - 1)"

    21 nitpick [expect = none]

    22 nitpick [dont_specialize, expect = none]

    23 sorry

    24

    25 lemma "f1 u v w x y = f1 y x w v u"

    26 nitpick [expect = none]

    27 nitpick [dont_specialize, expect = none]

    28 sorry

    29

    30 fun f2 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

    31 "f2 a b c d (Suc e) = a + b + c + d + e"

    32

    33 lemma "f2 0 0 0 0 0 = f2 (1 - 1) 0 0 0 0"

    34 nitpick [expect = none]

    35 nitpick [dont_specialize, expect = none]

    36 sorry

    37

    38 lemma "f2 0 (v - v) 0 (x - x) 0 = f2 (u - u) 0 (w - w) 0 (y - y)"

    39 nitpick [expect = none]

    40 nitpick [dont_specialize, expect = none]

    41 sorry

    42

    43 lemma "f2 1 0 0 0 0 = f2 0 1 0 0 0"

    44 nitpick [expect = genuine]

    45 nitpick [dont_specialize, expect = genuine]

    46 oops

    47

    48 lemma "f2 0 0 0 0 0 = f2 0 0 0 0 0"

    49 nitpick [expect = none]

    50 nitpick [dont_specialize, expect = none]

    51 sorry

    52

    53 fun f3 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

    54 "f3 (Suc a) b 0 d (Suc e) = a + b + d + e" |

    55 "f3 0 b 0 d 0 = b + d"

    56

    57 lemma "f3 a b c d e = f3 e d c b a"

    58 nitpick [expect = genuine]

    59 nitpick [dont_specialize, expect = genuine]

    60 oops

    61

    62 lemma "f3 a b c d a = f3 a d c d a"

    63 nitpick [expect = genuine]

    64 nitpick [dont_specialize, expect = genuine]

    65 oops

    66

    67 lemma "\<lbrakk>c < 1; a \<ge> e; e \<ge> a\<rbrakk> \<Longrightarrow> f3 a b c d a = f3 e d c b e"

    68 nitpick [expect = none]

    69 nitpick [dont_specialize, expect = none]

    70 sorry

    71

    72 lemma "(\<forall>u. a = u \<longrightarrow> f3 a a a a a = f3 u u u u u)

    73        \<and> (\<forall>u. b = u \<longrightarrow> f3 b b u b b = f3 u u b u u)"

    74 nitpick [expect = none]

    75 nitpick [dont_specialize, expect = none]

    76 nitpick [dont_skolemize, expect = none]

    77 nitpick [dont_specialize, dont_skolemize, expect = none]

    78 sorry

    79

    80 function f4 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

    81 "f4 x x = 1" |

    82 "f4 y z = (if y = z then 1 else 0)"

    83 by auto

    84 termination by lexicographic_order

    85

    86 lemma "f4 a b = f4 b a"

    87 nitpick [expect = none]

    88 nitpick [dont_specialize, expect = none]

    89 sorry

    90

    91 lemma "f4 a (Suc a) = f4 a a"

    92 nitpick [expect = genuine]

    93 nitpick [dont_specialize, expect = genuine]

    94 oops

    95

    96 fun f5 :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where

    97 "f5 f (Suc a) = f a"

    98

    99 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.

   100        f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"

   101 nitpick [expect = none]

   102 nitpick [dont_specialize, expect = none]

   103 sorry

   104

   105 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.

   106        f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"

   107 nitpick [expect = none]

   108 nitpick [dont_specialize, expect = none]

   109 sorry

   110

   111 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.

   112        f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"

   113 nitpick [expect = potential] (* unfortunate *)

   114 oops

   115

   116 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.

   117        f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"

   118 nitpick [expect = potential] (* unfortunate *)

   119 oops

   120

   121 lemma "\<forall>a. g a = a

   122        \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =

   123                       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"

   124 nitpick [expect = none]

   125 nitpick [dont_specialize, expect = none]

   126 sorry

   127

   128 lemma "\<forall>a. g a = a

   129        \<Longrightarrow> \<exists>one \<in> {2}. \<exists>two \<in> {1}. f5 g x =

   130                       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"

   131 nitpick [expect = potential]

   132 nitpick [dont_specialize, expect = potential]

   133 sorry

   134

   135 lemma "\<forall>a. g a = a

   136        \<Longrightarrow> \<exists>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\<Colon>nat).

   137            b\<^isub>1 < b\<^isub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"

   138 nitpick [expect = potential]

   139 nitpick [dont_specialize, expect = none]

   140 nitpick [dont_box, expect = none]

   141 nitpick [dont_box, dont_specialize, expect = none]

   142 sorry

   143

   144 lemma "\<forall>a. g a = a

   145        \<Longrightarrow> \<exists>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\<Colon>nat).

   146            b\<^isub>1 < b\<^isub>11

   147            \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then

   148                                 a

   149                               else

   150                                 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

   151                                 + h b\<^isub>9 + h b\<^isub>10) x"

   152 nitpick [card nat = 2, card 'a = 1, expect = none]

   153 nitpick [card nat = 2, card 'a = 1, dont_box, expect = none]

   154 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = none]

   155 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, expect = none]

   156 sorry

   157

   158 lemma "\<forall>a. g a = a

   159        \<Longrightarrow> \<exists>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\<Colon>nat).

   160            b\<^isub>1 < b\<^isub>11

   161            \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 \<ge> b\<^isub>11 then

   162                                 a

   163                               else

   164                                 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

   165                                 + h b\<^isub>9 + h b\<^isub>10) x"

   166 nitpick [card nat = 2, card 'a = 1, expect = potential]

   167 nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]

   168 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]

   169 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,

   170          expect = potential]

   171 oops

   172

   173 end