src/HOL/Nitpick_Examples/Special_Nits.thy
author blanchet
Thu Dec 17 15:22:11 2009 +0100 (2009-12-17)
changeset 34124 c4628a1dcf75
parent 34083 652719832159
child 34126 8a2c5d7aff51
permissions -rw-r--r--
added support for binary nat/int representation to Nitpick
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Special_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@33197
     3
    Copyright   2009
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@34083
    14
nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
blanchet@34083
    15
                card = 4]
blanchet@33197
    16
blanchet@33197
    17
fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 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 "\<lbrakk>c < 1; a \<ge> e; e \<ge> a\<rbrakk> \<Longrightarrow> 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 "(\<forall>u. a = u \<longrightarrow> f3 a a a a a = f3 u u u u u)
blanchet@33197
    73
       \<and> (\<forall>u. b = u \<longrightarrow> 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
nitpick [dont_skolemize, expect = none]
blanchet@33197
    77
nitpick [dont_specialize, dont_skolemize, expect = none]
blanchet@33197
    78
sorry
blanchet@33197
    79
blanchet@33197
    80
function f4 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
blanchet@33197
    81
"f4 x x = 1" |
blanchet@33197
    82
"f4 y z = (if y = z then 1 else 0)"
blanchet@33197
    83
by auto
blanchet@33197
    84
termination by lexicographic_order
blanchet@33197
    85
blanchet@33197
    86
lemma "f4 a b = f4 b a"
blanchet@33197
    87
nitpick [expect = none]
blanchet@33197
    88
nitpick [dont_specialize, expect = none]
blanchet@33197
    89
sorry
blanchet@33197
    90
blanchet@33197
    91
lemma "f4 a (Suc a) = f4 a a"
blanchet@33197
    92
nitpick [expect = genuine]
blanchet@33197
    93
nitpick [dont_specialize, expect = genuine]
blanchet@33197
    94
oops
blanchet@33197
    95
blanchet@33197
    96
fun f5 :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
blanchet@33197
    97
"f5 f (Suc a) = f a"
blanchet@33197
    98
blanchet@33197
    99
lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
blanchet@33197
   100
       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
blanchet@33197
   101
nitpick [expect = none]
blanchet@33197
   102
nitpick [dont_specialize, expect = none]
blanchet@33197
   103
sorry
blanchet@33197
   104
blanchet@33197
   105
lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
blanchet@33197
   106
       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
blanchet@33197
   107
nitpick [expect = none]
blanchet@33197
   108
nitpick [dont_specialize, expect = none]
blanchet@33197
   109
sorry
blanchet@33197
   110
blanchet@33197
   111
lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
blanchet@33197
   112
       f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
blanchet@33737
   113
nitpick [expect = potential] (* unfortunate *)
blanchet@33737
   114
oops
blanchet@33197
   115
blanchet@33197
   116
lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
blanchet@33197
   117
       f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
blanchet@33737
   118
nitpick [expect = potential] (* unfortunate *)
blanchet@33737
   119
oops
blanchet@33197
   120
blanchet@33197
   121
lemma "\<forall>a. g a = a
blanchet@33197
   122
       \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =
blanchet@33197
   123
                      f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"
blanchet@33197
   124
nitpick [expect = none]
blanchet@33197
   125
nitpick [dont_specialize, expect = none]
blanchet@33197
   126
sorry
blanchet@33197
   127
blanchet@33197
   128
lemma "\<forall>a. g a = a
blanchet@33197
   129
       \<Longrightarrow> \<exists>one \<in> {2}. \<exists>two \<in> {1}. f5 g x =
blanchet@33197
   130
                      f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"
blanchet@33197
   131
nitpick [expect = potential]
blanchet@33197
   132
nitpick [dont_specialize, expect = potential]
blanchet@33197
   133
sorry
blanchet@33197
   134
blanchet@33197
   135
lemma "\<forall>a. g a = a
blanchet@33197
   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).
blanchet@33197
   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"
blanchet@34124
   138
nitpick [expect = none]
blanchet@33197
   139
nitpick [dont_specialize, expect = none]
blanchet@33197
   140
nitpick [dont_box, expect = none]
blanchet@33197
   141
nitpick [dont_box, dont_specialize, expect = none]
blanchet@33197
   142
sorry
blanchet@33197
   143
blanchet@33197
   144
lemma "\<forall>a. g a = a
blanchet@33197
   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).
blanchet@33197
   146
           b\<^isub>1 < b\<^isub>11
blanchet@33197
   147
           \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then
blanchet@33197
   148
                                a
blanchet@33197
   149
                              else
blanchet@33197
   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
blanchet@33197
   151
                                + h b\<^isub>9 + h b\<^isub>10) x"
blanchet@33197
   152
nitpick [card nat = 2, card 'a = 1, expect = none]
blanchet@33197
   153
nitpick [card nat = 2, card 'a = 1, dont_box, expect = none]
blanchet@33197
   154
nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = none]
blanchet@33197
   155
nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, expect = none]
blanchet@33197
   156
sorry
blanchet@33197
   157
blanchet@33197
   158
lemma "\<forall>a. g a = a
blanchet@33197
   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).
blanchet@33197
   160
           b\<^isub>1 < b\<^isub>11
blanchet@33197
   161
           \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 \<ge> b\<^isub>11 then
blanchet@33197
   162
                                a
blanchet@33197
   163
                              else
blanchet@33197
   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
blanchet@33197
   165
                                + h b\<^isub>9 + h b\<^isub>10) x"
blanchet@34124
   166
nitpick [card nat = 2, card 'a = 1, expect = potential]
blanchet@33197
   167
nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]
blanchet@33197
   168
nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]
blanchet@33197
   169
nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,
blanchet@33197
   170
         expect = potential]
blanchet@33197
   171
oops
blanchet@33197
   172
blanchet@33197
   173
end