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