1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Fri Dec 18 12:00:29 2009 +0100
1.3 @@ -0,0 +1,209 @@
1.4 +(* Title: HOL/Nitpick_Examples/Integer_Nits.thy
1.5 + Author: Jasmin Blanchette, TU Muenchen
1.6 + Copyright 2009
1.7 +
1.8 +Examples featuring Nitpick applied to natural numbers and integers.
1.9 +*)
1.10 +
1.11 +header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}
1.12 +
1.13 +theory Integer_Nits
1.14 +imports Nitpick
1.15 +begin
1.16 +
1.17 +nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
1.18 + card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
1.19 +
1.20 +lemma "Suc x = x + 1"
1.21 +nitpick [unary_ints, expect = none]
1.22 +nitpick [binary_ints, expect = none]
1.23 +sorry
1.24 +
1.25 +lemma "x < Suc x"
1.26 +nitpick [unary_ints, expect = none]
1.27 +nitpick [binary_ints, expect = none]
1.28 +sorry
1.29 +
1.30 +lemma "x + y \<ge> (x::nat)"
1.31 +nitpick [unary_ints, expect = none]
1.32 +nitpick [binary_ints, expect = none]
1.33 +sorry
1.34 +
1.35 +lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::nat)"
1.36 +nitpick [unary_ints, expect = none]
1.37 +nitpick [binary_ints, expect = none]
1.38 +sorry
1.39 +
1.40 +lemma "x + y = y + (x::nat)"
1.41 +nitpick [unary_ints, expect = none]
1.42 +nitpick [binary_ints, expect = none]
1.43 +sorry
1.44 +
1.45 +lemma "x > y \<Longrightarrow> x - y \<noteq> (0::nat)"
1.46 +nitpick [unary_ints, expect = none]
1.47 +nitpick [binary_ints, expect = none]
1.48 +sorry
1.49 +
1.50 +lemma "x \<le> y \<Longrightarrow> x - y = (0::nat)"
1.51 +nitpick [unary_ints, expect = none]
1.52 +nitpick [binary_ints, expect = none]
1.53 +sorry
1.54 +
1.55 +lemma "x - (0::nat) = x"
1.56 +nitpick [unary_ints, expect = none]
1.57 +nitpick [binary_ints, expect = none]
1.58 +sorry
1.59 +
1.60 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::nat)"
1.61 +nitpick [unary_ints, expect = none]
1.62 +nitpick [binary_ints, expect = none]
1.63 +sorry
1.64 +
1.65 +lemma "0 * y = (0::nat)"
1.66 +nitpick [unary_ints, expect = none]
1.67 +nitpick [binary_ints, expect = none]
1.68 +sorry
1.69 +
1.70 +lemma "y * 0 = (0::nat)"
1.71 +nitpick [unary_ints, expect = none]
1.72 +nitpick [binary_ints, expect = none]
1.73 +sorry
1.74 +
1.75 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::nat)"
1.76 +nitpick [unary_ints, expect = none]
1.77 +nitpick [binary_ints, expect = none]
1.78 +sorry
1.79 +
1.80 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::nat)"
1.81 +nitpick [unary_ints, expect = none]
1.82 +nitpick [binary_ints, expect = none]
1.83 +sorry
1.84 +
1.85 +lemma "x * y div y = (x::nat)"
1.86 +nitpick [unary_ints, expect = genuine]
1.87 +nitpick [binary_ints, expect = genuine]
1.88 +oops
1.89 +
1.90 +lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::nat)"
1.91 +nitpick [unary_ints, expect = none]
1.92 +nitpick [binary_ints, expect = none]
1.93 +sorry
1.94 +
1.95 +lemma "5 * 55 < (260::nat)"
1.96 +nitpick [unary_ints, expect = none]
1.97 +nitpick [binary_ints, expect = none]
1.98 +nitpick [binary_ints, bits = 9, expect = genuine]
1.99 +oops
1.100 +
1.101 +lemma "nat (of_nat n) = n"
1.102 +nitpick [unary_ints, expect = none]
1.103 +nitpick [binary_ints, expect = none]
1.104 +sorry
1.105 +
1.106 +lemma "x + y \<ge> (x::int)"
1.107 +nitpick [unary_ints, expect = genuine]
1.108 +nitpick [binary_ints, expect = genuine]
1.109 +oops
1.110 +
1.111 +lemma "\<lbrakk>x \<ge> 0; y \<ge> 0\<rbrakk> \<Longrightarrow> x + y \<ge> (0::int)"
1.112 +nitpick [unary_ints, expect = none]
1.113 +nitpick [binary_ints, expect = none]
1.114 +sorry
1.115 +
1.116 +lemma "y \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
1.117 +nitpick [unary_ints, expect = none]
1.118 +nitpick [binary_ints, expect = none]
1.119 +sorry
1.120 +
1.121 +lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (y::int)"
1.122 +nitpick [unary_ints, expect = none]
1.123 +nitpick [binary_ints, expect = none]
1.124 +sorry
1.125 +
1.126 +lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
1.127 +nitpick [unary_ints, expect = genuine]
1.128 +nitpick [binary_ints, expect = genuine]
1.129 +oops
1.130 +
1.131 +lemma "\<lbrakk>x \<le> 0; y \<le> 0\<rbrakk> \<Longrightarrow> x + y \<le> (0::int)"
1.132 +nitpick [unary_ints, expect = none]
1.133 +nitpick [binary_ints, expect = none]
1.134 +sorry
1.135 +
1.136 +lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::int)"
1.137 +nitpick [unary_ints, expect = genuine]
1.138 +nitpick [binary_ints, expect = genuine]
1.139 +oops
1.140 +
1.141 +lemma "x + y = y + (x::int)"
1.142 +nitpick [unary_ints, expect = none]
1.143 +nitpick [binary_ints, expect = none]
1.144 +sorry
1.145 +
1.146 +lemma "x > y \<Longrightarrow> x - y \<noteq> (0::int)"
1.147 +nitpick [unary_ints, expect = none]
1.148 +nitpick [binary_ints, expect = none]
1.149 +sorry
1.150 +
1.151 +lemma "x \<le> y \<Longrightarrow> x - y = (0::int)"
1.152 +nitpick [unary_ints, expect = genuine]
1.153 +nitpick [binary_ints, expect = genuine]
1.154 +oops
1.155 +
1.156 +lemma "x - (0::int) = x"
1.157 +nitpick [unary_ints, expect = none]
1.158 +nitpick [binary_ints, expect = none]
1.159 +sorry
1.160 +
1.161 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::int)"
1.162 +nitpick [unary_ints, expect = none]
1.163 +nitpick [binary_ints, expect = none]
1.164 +sorry
1.165 +
1.166 +lemma "0 * y = (0::int)"
1.167 +nitpick [unary_ints, expect = none]
1.168 +nitpick [binary_ints, expect = none]
1.169 +sorry
1.170 +
1.171 +lemma "y * 0 = (0::int)"
1.172 +nitpick [unary_ints, expect = none]
1.173 +nitpick [binary_ints, expect = none]
1.174 +sorry
1.175 +
1.176 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::int)"
1.177 +nitpick [unary_ints, expect = genuine]
1.178 +nitpick [binary_ints, expect = genuine]
1.179 +oops
1.180 +
1.181 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::int)"
1.182 +nitpick [unary_ints, expect = genuine]
1.183 +nitpick [binary_ints, expect = genuine]
1.184 +oops
1.185 +
1.186 +lemma "x * y div y = (x::int)"
1.187 +nitpick [unary_ints, expect = genuine]
1.188 +nitpick [binary_ints, expect = genuine]
1.189 +oops
1.190 +
1.191 +lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
1.192 +nitpick [unary_ints, expect = none]
1.193 +nitpick [binary_ints, expect = none, card = 1\<midarrow>5, bits = 1\<midarrow>5]
1.194 +sorry
1.195 +
1.196 +lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
1.197 +nitpick [unary_ints, expect = none]
1.198 +nitpick [binary_ints, expect = none]
1.199 +sorry
1.200 +
1.201 +lemma "-5 * 55 > (-260::int)"
1.202 +nitpick [unary_ints, expect = none]
1.203 +nitpick [binary_ints, expect = none]
1.204 +nitpick [binary_ints, bits = 9, expect = genuine]
1.205 +oops
1.206 +
1.207 +lemma "nat (of_nat n) = n"
1.208 +nitpick [unary_ints, expect = none]
1.209 +nitpick [binary_ints, expect = none]
1.210 +sorry
1.211 +
1.212 +end