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