src/HOL/Nitpick_Examples/Integer_Nits.thy
author nipkow
Mon Jan 30 21:49:41 2012 +0100 (2012-01-30)
changeset 46372 6fa9cdb8b850
parent 46090 f1796596ef60
child 47108 2a1953f0d20d
permissions -rw-r--r--
added "'a rel"
blanchet@34126
     1
(*  Title:      HOL/Nitpick_Examples/Integer_Nits.thy
blanchet@34126
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@45035
     3
    Copyright   2009-2011
blanchet@34126
     4
blanchet@34126
     5
Examples featuring Nitpick applied to natural numbers and integers.
blanchet@34126
     6
*)
blanchet@34126
     7
blanchet@46090
     8
header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}
blanchet@34126
     9
blanchet@34126
    10
theory Integer_Nits
blanchet@46090
    11
imports Main
blanchet@34126
    12
begin
blanchet@34126
    13
blanchet@42959
    14
nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
krauss@42208
    15
                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
blanchet@34126
    16
blanchet@34126
    17
lemma "Suc x = x + 1"
blanchet@34126
    18
nitpick [unary_ints, expect = none]
blanchet@34126
    19
nitpick [binary_ints, expect = none]
blanchet@34126
    20
sorry
blanchet@34126
    21
blanchet@34126
    22
lemma "x < Suc x"
blanchet@34126
    23
nitpick [unary_ints, expect = none]
blanchet@34126
    24
nitpick [binary_ints, expect = none]
blanchet@34126
    25
sorry
blanchet@34126
    26
blanchet@34126
    27
lemma "x + y \<ge> (x::nat)"
blanchet@34126
    28
nitpick [unary_ints, expect = none]
blanchet@34126
    29
nitpick [binary_ints, expect = none]
blanchet@34126
    30
sorry
blanchet@34126
    31
blanchet@34126
    32
lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::nat)"
blanchet@34126
    33
nitpick [unary_ints, expect = none]
blanchet@34126
    34
nitpick [binary_ints, expect = none]
blanchet@34126
    35
sorry
blanchet@34126
    36
blanchet@34126
    37
lemma "x + y = y + (x::nat)"
blanchet@34126
    38
nitpick [unary_ints, expect = none]
blanchet@34126
    39
nitpick [binary_ints, expect = none]
blanchet@34126
    40
sorry
blanchet@34126
    41
blanchet@34126
    42
lemma "x > y \<Longrightarrow> x - y \<noteq> (0::nat)"
blanchet@34126
    43
nitpick [unary_ints, expect = none]
blanchet@34126
    44
nitpick [binary_ints, expect = none]
blanchet@34126
    45
sorry
blanchet@34126
    46
blanchet@34126
    47
lemma "x \<le> y \<Longrightarrow> x - y = (0::nat)"
blanchet@34126
    48
nitpick [unary_ints, expect = none]
blanchet@34126
    49
nitpick [binary_ints, expect = none]
blanchet@34126
    50
sorry
blanchet@34126
    51
blanchet@34126
    52
lemma "x - (0::nat) = x"
blanchet@34126
    53
nitpick [unary_ints, expect = none]
blanchet@34126
    54
nitpick [binary_ints, expect = none]
blanchet@34126
    55
sorry
blanchet@34126
    56
blanchet@34126
    57
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::nat)"
blanchet@34126
    58
nitpick [unary_ints, expect = none]
blanchet@34126
    59
nitpick [binary_ints, expect = none]
blanchet@34126
    60
sorry
blanchet@34126
    61
blanchet@34126
    62
lemma "0 * y = (0::nat)"
blanchet@34126
    63
nitpick [unary_ints, expect = none]
blanchet@34126
    64
nitpick [binary_ints, expect = none]
blanchet@34126
    65
sorry
blanchet@34126
    66
blanchet@34126
    67
lemma "y * 0 = (0::nat)"
blanchet@34126
    68
nitpick [unary_ints, expect = none]
blanchet@34126
    69
nitpick [binary_ints, expect = none]
blanchet@34126
    70
sorry
blanchet@34126
    71
blanchet@34126
    72
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::nat)"
blanchet@34126
    73
nitpick [unary_ints, expect = none]
blanchet@34126
    74
nitpick [binary_ints, expect = none]
blanchet@34126
    75
sorry
blanchet@34126
    76
blanchet@34126
    77
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::nat)"
blanchet@34126
    78
nitpick [unary_ints, expect = none]
blanchet@34126
    79
nitpick [binary_ints, expect = none]
blanchet@34126
    80
sorry
blanchet@34126
    81
blanchet@34126
    82
lemma "x * y div y = (x::nat)"
blanchet@34126
    83
nitpick [unary_ints, expect = genuine]
blanchet@34126
    84
nitpick [binary_ints, expect = genuine]
blanchet@34126
    85
oops
blanchet@34126
    86
blanchet@34126
    87
lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::nat)"
blanchet@34126
    88
nitpick [unary_ints, expect = none]
blanchet@34126
    89
nitpick [binary_ints, expect = none]
blanchet@34126
    90
sorry
blanchet@34126
    91
blanchet@34126
    92
lemma "5 * 55 < (260::nat)"
blanchet@34126
    93
nitpick [unary_ints, expect = none]
blanchet@34126
    94
nitpick [binary_ints, expect = none]
blanchet@34126
    95
nitpick [binary_ints, bits = 9, expect = genuine]
blanchet@34126
    96
oops
blanchet@34126
    97
blanchet@34126
    98
lemma "nat (of_nat n) = n"
blanchet@34126
    99
nitpick [unary_ints, expect = none]
blanchet@34126
   100
nitpick [binary_ints, expect = none]
blanchet@34126
   101
sorry
blanchet@34126
   102
blanchet@34126
   103
lemma "x + y \<ge> (x::int)"
blanchet@34126
   104
nitpick [unary_ints, expect = genuine]
blanchet@34126
   105
nitpick [binary_ints, expect = genuine]
blanchet@34126
   106
oops
blanchet@34126
   107
blanchet@34126
   108
lemma "\<lbrakk>x \<ge> 0; y \<ge> 0\<rbrakk> \<Longrightarrow> x + y \<ge> (0::int)"
blanchet@34126
   109
nitpick [unary_ints, expect = none]
blanchet@34126
   110
nitpick [binary_ints, expect = none]
blanchet@34126
   111
sorry
blanchet@34126
   112
blanchet@34126
   113
lemma "y \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
blanchet@34126
   114
nitpick [unary_ints, expect = none]
blanchet@34126
   115
nitpick [binary_ints, expect = none]
blanchet@34126
   116
sorry
blanchet@34126
   117
blanchet@34126
   118
lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (y::int)"
blanchet@34126
   119
nitpick [unary_ints, expect = none]
blanchet@34126
   120
nitpick [binary_ints, expect = none]
blanchet@34126
   121
sorry
blanchet@34126
   122
blanchet@34126
   123
lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
blanchet@34126
   124
nitpick [unary_ints, expect = genuine]
blanchet@34126
   125
nitpick [binary_ints, expect = genuine]
blanchet@34126
   126
oops
blanchet@34126
   127
blanchet@34126
   128
lemma "\<lbrakk>x \<le> 0; y \<le> 0\<rbrakk> \<Longrightarrow> x + y \<le> (0::int)"
blanchet@34126
   129
nitpick [unary_ints, expect = none]
blanchet@34126
   130
nitpick [binary_ints, expect = none]
blanchet@34126
   131
sorry
blanchet@34126
   132
blanchet@34126
   133
lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::int)"
blanchet@34126
   134
nitpick [unary_ints, expect = genuine]
blanchet@34126
   135
nitpick [binary_ints, expect = genuine]
blanchet@34126
   136
oops
blanchet@34126
   137
blanchet@34126
   138
lemma "x + y = y + (x::int)"
blanchet@34126
   139
nitpick [unary_ints, expect = none]
blanchet@34126
   140
nitpick [binary_ints, expect = none]
blanchet@34126
   141
sorry
blanchet@34126
   142
blanchet@34126
   143
lemma "x > y \<Longrightarrow> x - y \<noteq> (0::int)"
blanchet@34126
   144
nitpick [unary_ints, expect = none]
blanchet@34126
   145
nitpick [binary_ints, expect = none]
blanchet@34126
   146
sorry
blanchet@34126
   147
blanchet@34126
   148
lemma "x \<le> y \<Longrightarrow> x - y = (0::int)"
blanchet@34126
   149
nitpick [unary_ints, expect = genuine]
blanchet@34126
   150
nitpick [binary_ints, expect = genuine]
blanchet@34126
   151
oops
blanchet@34126
   152
blanchet@34126
   153
lemma "x - (0::int) = x"
blanchet@34126
   154
nitpick [unary_ints, expect = none]
blanchet@34126
   155
nitpick [binary_ints, expect = none]
blanchet@34126
   156
sorry
blanchet@34126
   157
blanchet@34126
   158
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::int)"
blanchet@34126
   159
nitpick [unary_ints, expect = none]
blanchet@34126
   160
nitpick [binary_ints, expect = none]
blanchet@34126
   161
sorry
blanchet@34126
   162
blanchet@34126
   163
lemma "0 * y = (0::int)"
blanchet@34126
   164
nitpick [unary_ints, expect = none]
blanchet@34126
   165
nitpick [binary_ints, expect = none]
blanchet@34126
   166
sorry
blanchet@34126
   167
blanchet@34126
   168
lemma "y * 0 = (0::int)"
blanchet@34126
   169
nitpick [unary_ints, expect = none]
blanchet@34126
   170
nitpick [binary_ints, expect = none]
blanchet@34126
   171
sorry
blanchet@34126
   172
blanchet@34126
   173
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::int)"
blanchet@34126
   174
nitpick [unary_ints, expect = genuine]
blanchet@34126
   175
nitpick [binary_ints, expect = genuine]
blanchet@34126
   176
oops
blanchet@34126
   177
blanchet@34126
   178
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::int)"
blanchet@34126
   179
nitpick [unary_ints, expect = genuine]
blanchet@34126
   180
nitpick [binary_ints, expect = genuine]
blanchet@34126
   181
oops
blanchet@34126
   182
blanchet@34126
   183
lemma "x * y div y = (x::int)"
blanchet@34126
   184
nitpick [unary_ints, expect = genuine]
blanchet@34126
   185
nitpick [binary_ints, expect = genuine]
blanchet@34126
   186
oops
blanchet@34126
   187
blanchet@34126
   188
lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
blanchet@34126
   189
nitpick [unary_ints, expect = none]
blanchet@42959
   190
nitpick [binary_ints, card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
blanchet@34126
   191
sorry
blanchet@34126
   192
blanchet@34126
   193
lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
blanchet@34126
   194
nitpick [unary_ints, expect = none]
blanchet@34126
   195
nitpick [binary_ints, expect = none]
blanchet@34126
   196
sorry
blanchet@34126
   197
blanchet@34126
   198
lemma "-5 * 55 > (-260::int)"
blanchet@34126
   199
nitpick [unary_ints, expect = none]
blanchet@34126
   200
nitpick [binary_ints, expect = none]
blanchet@34126
   201
nitpick [binary_ints, bits = 9, expect = genuine]
blanchet@34126
   202
oops
blanchet@34126
   203
blanchet@34126
   204
lemma "nat (of_nat n) = n"
blanchet@34126
   205
nitpick [unary_ints, expect = none]
blanchet@34126
   206
nitpick [binary_ints, expect = none]
blanchet@34126
   207
sorry
blanchet@34126
   208
blanchet@35695
   209
datatype tree = Null | Node nat tree tree
blanchet@35695
   210
blanchet@35695
   211
primrec labels where
blanchet@35695
   212
"labels Null = {}" |
blanchet@35695
   213
"labels (Node x t u) = {x} \<union> labels t \<union> labels u"
blanchet@35695
   214
blanchet@35695
   215
lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
blanchet@37477
   216
nitpick [expect = potential] (* unfortunate *)
blanchet@35695
   217
nitpick [dont_finitize, expect = potential]
blanchet@35695
   218
oops
blanchet@35695
   219
blanchet@35695
   220
lemma "labels (Node x t u) \<noteq> {}"
blanchet@35695
   221
nitpick [expect = none]
blanchet@35695
   222
oops
blanchet@35695
   223
blanchet@35695
   224
lemma "card (labels t) > 0"
blanchet@37477
   225
nitpick [expect = potential] (* unfortunate *)
blanchet@35695
   226
nitpick [dont_finitize, expect = potential]
blanchet@35695
   227
oops
blanchet@35695
   228
blanchet@35695
   229
lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
blanchet@37477
   230
nitpick [expect = potential] (* unfortunate *)
blanchet@35695
   231
nitpick [dont_finitize, expect = potential]
blanchet@35695
   232
oops
blanchet@35695
   233
blanchet@35695
   234
lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
blanchet@39362
   235
nitpick [expect = potential] (* unfortunate *)
blanchet@39362
   236
nitpick [dont_finitize, expect = potential]
blanchet@35695
   237
sorry
blanchet@35695
   238
blanchet@35695
   239
lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
blanchet@39362
   240
nitpick [expect = potential] (* unfortunate *)
blanchet@39362
   241
nitpick [dont_finitize, expect = potential]
blanchet@35695
   242
oops
blanchet@35695
   243
blanchet@34126
   244
end