summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

5 Examples featuring Nitpick applied to natural numbers and integers.

6 *)

8 section {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}

10 theory Integer_Nits

11 imports Main

12 begin

14 nitpick_params [verbose, card = 1-5, bits = 1,2,3,4,6,

15 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]

17 lemma "Suc x = x + 1"

18 nitpick [unary_ints, expect = none]

19 nitpick [binary_ints, expect = none]

20 sorry

22 lemma "x < Suc x"

23 nitpick [unary_ints, expect = none]

24 nitpick [binary_ints, expect = none]

25 sorry

27 lemma "x + y \<ge> (x::nat)"

28 nitpick [unary_ints, expect = none]

29 nitpick [binary_ints, expect = none]

30 sorry

32 lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::nat)"

33 nitpick [unary_ints, expect = none]

34 nitpick [binary_ints, expect = none]

35 sorry

37 lemma "x + y = y + (x::nat)"

38 nitpick [unary_ints, expect = none]

39 nitpick [binary_ints, expect = none]

40 sorry

42 lemma "x > y \<Longrightarrow> x - y \<noteq> (0::nat)"

43 nitpick [unary_ints, expect = none]

44 nitpick [binary_ints, expect = none]

45 sorry

47 lemma "x \<le> y \<Longrightarrow> x - y = (0::nat)"

48 nitpick [unary_ints, expect = none]

49 nitpick [binary_ints, expect = none]

50 sorry

52 lemma "x - (0::nat) = x"

53 nitpick [unary_ints, expect = none]

54 nitpick [binary_ints, expect = none]

55 sorry

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

62 lemma "0 * y = (0::nat)"

63 nitpick [unary_ints, expect = none]

64 nitpick [binary_ints, expect = none]

65 sorry

67 lemma "y * 0 = (0::nat)"

68 nitpick [unary_ints, expect = none]

69 nitpick [binary_ints, expect = none]

70 sorry

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

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

82 lemma "x * y div y = (x::nat)"

83 nitpick [unary_ints, expect = genuine]

84 nitpick [binary_ints, expect = genuine]

85 oops

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

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

98 lemma "nat (of_nat n) = n"

99 nitpick [unary_ints, expect = none]

100 nitpick [binary_ints, expect = none]

101 sorry

103 lemma "x + y \<ge> (x::int)"

104 nitpick [unary_ints, expect = genuine]

105 nitpick [binary_ints, expect = genuine]

106 oops

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

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

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

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

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

133 lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::int)"

134 nitpick [unary_ints, expect = genuine]

135 nitpick [binary_ints, expect = genuine]

136 oops

138 lemma "x + y = y + (x::int)"

139 nitpick [unary_ints, expect = none]

140 nitpick [binary_ints, expect = none]

141 sorry

143 lemma "x > y \<Longrightarrow> x - y \<noteq> (0::int)"

144 nitpick [unary_ints, expect = none]

145 nitpick [binary_ints, expect = none]

146 sorry

148 lemma "x \<le> y \<Longrightarrow> x - y = (0::int)"

149 nitpick [unary_ints, expect = genuine]

150 nitpick [binary_ints, expect = genuine]

151 oops

153 lemma "x - (0::int) = x"

154 nitpick [unary_ints, expect = none]

155 nitpick [binary_ints, expect = none]

156 sorry

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

163 lemma "0 * y = (0::int)"

164 nitpick [unary_ints, expect = none]

165 nitpick [binary_ints, expect = none]

166 sorry

168 lemma "y * 0 = (0::int)"

169 nitpick [unary_ints, expect = none]

170 nitpick [binary_ints, expect = none]

171 sorry

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

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

183 lemma "x * y div y = (x::int)"

184 nitpick [unary_ints, expect = genuine]

185 nitpick [binary_ints, expect = genuine]

186 oops

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

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

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

204 lemma "nat (of_nat n) = n"

205 nitpick [unary_ints, expect = none]

206 nitpick [binary_ints, expect = none]

207 sorry

209 datatype tree = Null | Node nat tree tree

211 primrec labels where

212 "labels Null = {}" |

213 "labels (Node x t u) = {x} \<union> labels t \<union> labels u"

215 lemma "labels (Node x t u) \<noteq> labels (Node y v w)"

216 nitpick [expect = potential] (* unfortunate *)

217 oops

219 lemma "labels (Node x t u) \<noteq> {}"

220 nitpick [expect = none]

221 oops

223 lemma "card (labels t) > 0"

224 nitpick [expect = potential] (* unfortunate *)

225 oops

227 lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"

228 nitpick [expect = potential] (* unfortunate *)

229 oops

231 lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"

232 nitpick [expect = potential] (* unfortunate *)

233 sorry

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

239 end