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

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;

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

5 Examples featuring Nitpick applied to natural numbers and integers.

6 *)

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

10 theory Integer_Nits

11 imports Nitpick

12 begin

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]

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, expect = none, card = 1\<midarrow>5, bits = 1\<midarrow>5]

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 end