src/HOL/Nitpick_Examples/Special_Nits.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61076 bdc1e2f0a86a
child 63167 0909deb8059b
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Nitpick_Examples/Special_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009-2011
     4 
     5 Examples featuring Nitpick's "specialize" optimization.
     6 *)
     7 
     8 section {* Examples Featuring Nitpick's \textit{specialize} Optimization *}
     9 
    10 theory Special_Nits
    11 imports Main
    12 begin
    13 
    14 nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
    15                 timeout = 240]
    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 sorry
    77 
    78 function f4 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    79 "f4 x x = 1" |
    80 "f4 y z = (if y = z then 1 else 0)"
    81 by auto
    82 termination by lexicographic_order
    83 
    84 lemma "f4 a b = f4 b a"
    85 nitpick [expect = none]
    86 nitpick [dont_specialize, expect = none]
    87 sorry
    88 
    89 lemma "f4 a (Suc a) = f4 a a"
    90 nitpick [expect = genuine]
    91 nitpick [dont_specialize, expect = genuine]
    92 oops
    93 
    94 fun f5 :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
    95 "f5 f (Suc a) = f a"
    96 
    97 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
    98        f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
    99 nitpick [expect = none]
   100 nitpick [dont_specialize, expect = none]
   101 sorry
   102 
   103 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
   104        f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
   105 nitpick [expect = none]
   106 nitpick [dont_specialize, expect = none]
   107 sorry
   108 
   109 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
   110        f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
   111 nitpick [expect = genuine]
   112 oops
   113 
   114 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
   115        f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
   116 nitpick [expect = genuine]
   117 oops
   118 
   119 lemma "\<forall>a. g a = a
   120        \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =
   121                       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"
   122 nitpick [expect = none]
   123 nitpick [dont_specialize, expect = none]
   124 sorry
   125 
   126 lemma "\<forall>a. g a = a
   127        \<Longrightarrow> \<exists>one \<in> {2}. \<exists>two \<in> {1}. f5 g x =
   128                       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"
   129 nitpick [expect = potential]
   130 nitpick [dont_specialize, expect = potential]
   131 sorry
   132 
   133 lemma "\<forall>a. g a = a
   134        \<Longrightarrow> \<exists>b\<^sub>1 b\<^sub>2 b\<^sub>3 b\<^sub>4 b\<^sub>5 b\<^sub>6 b\<^sub>7 b\<^sub>8 b\<^sub>9 b\<^sub>10 (b\<^sub>11::nat).
   135            b\<^sub>1 < b\<^sub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^sub>1 < b\<^sub>11 then a else h b\<^sub>2) x"
   136 nitpick [expect = potential]
   137 nitpick [dont_specialize, expect = none]
   138 nitpick [dont_box, expect = none]
   139 nitpick [dont_box, dont_specialize, expect = none]
   140 sorry
   141 
   142 lemma "\<forall>a. g a = a
   143        \<Longrightarrow> \<exists>b\<^sub>1 b\<^sub>2 b\<^sub>3 b\<^sub>4 b\<^sub>5 b\<^sub>6 b\<^sub>7 b\<^sub>8 b\<^sub>9 b\<^sub>10 (b\<^sub>11::nat).
   144            b\<^sub>1 < b\<^sub>11
   145            \<and> f5 g x = f5 (\<lambda>a. if b\<^sub>1 < b\<^sub>11 then
   146                                 a
   147                               else
   148                                 h b\<^sub>2 + h b\<^sub>3 + h b\<^sub>4 + h b\<^sub>5 + h b\<^sub>6 + h b\<^sub>7 + h b\<^sub>8
   149                                 + h b\<^sub>9 + h b\<^sub>10) x"
   150 nitpick [card nat = 2, card 'a = 1, expect = none]
   151 nitpick [card nat = 2, card 'a = 1, dont_box, expect = none]
   152 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = none]
   153 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, expect = none]
   154 sorry
   155 
   156 lemma "\<forall>a. g a = a
   157        \<Longrightarrow> \<exists>b\<^sub>1 b\<^sub>2 b\<^sub>3 b\<^sub>4 b\<^sub>5 b\<^sub>6 b\<^sub>7 b\<^sub>8 b\<^sub>9 b\<^sub>10 (b\<^sub>11::nat).
   158            b\<^sub>1 < b\<^sub>11
   159            \<and> f5 g x = f5 (\<lambda>a. if b\<^sub>1 \<ge> b\<^sub>11 then
   160                                 a
   161                               else
   162                                 h b\<^sub>2 + h b\<^sub>3 + h b\<^sub>4 + h b\<^sub>5 + h b\<^sub>6 + h b\<^sub>7 + h b\<^sub>8
   163                                 + h b\<^sub>9 + h b\<^sub>10) x"
   164 nitpick [card nat = 2, card 'a = 1, expect = potential]
   165 nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]
   166 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]
   167 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,
   168          expect = potential]
   169 oops
   170 
   171 end