src/HOL/Nitpick_Examples/Integer_Nits.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35078 6fd1052fe463
child 35695 80b2c22f8f00
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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 [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
    15                 card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
    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, expect = none, card = 1\<midarrow>5, bits = 1\<midarrow>5]
   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 end