src/HOL/Nitpick_Examples/Integer_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/Integer_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009-2012
     4 
     5 Examples featuring Nitpick applied to natural numbers and integers.
     6 *)
     7 
     8 section {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}
     9 
    10 theory Integer_Nits
    11 imports Main
    12 begin
    13 
    14 nitpick_params [verbose, card = 1-5, bits = 1,2,3,4,6,
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    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-4, bits = 1-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 oops
   218 
   219 lemma "labels (Node x t u) \<noteq> {}"
   220 nitpick [expect = none]
   221 oops
   222 
   223 lemma "card (labels t) > 0"
   224 nitpick [expect = potential] (* unfortunate *)
   225 oops
   226 
   227 lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
   228 nitpick [expect = potential] (* unfortunate *)
   229 oops
   230 
   231 lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
   232 nitpick [expect = potential] (* unfortunate *)
   233 sorry
   234 
   235 lemma "(\<Sum>i \<in> labels (Node x t u). f i::nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
   236 nitpick [expect = potential] (* unfortunate *)
   237 oops
   238 
   239 end