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