equal
deleted
inserted
replaced
62 oops |
62 oops |
63 |
63 |
64 subsection {* 2.5. Natural Numbers and Integers *} |
64 subsection {* 2.5. Natural Numbers and Integers *} |
65 |
65 |
66 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n" |
66 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n" |
67 (* FIXME |
|
68 nitpick [expect = genuine] |
67 nitpick [expect = genuine] |
69 nitpick [binary_ints, bits = 16, expect = genuine] |
68 nitpick [binary_ints, bits = 16, expect = genuine] |
70 *) |
|
71 oops |
69 oops |
72 |
70 |
73 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P" |
71 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P" |
74 nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine] |
72 nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine] |
75 oops |
73 oops |
141 record point = |
139 record point = |
142 Xcoord :: int |
140 Xcoord :: int |
143 Ycoord :: int |
141 Ycoord :: int |
144 |
142 |
145 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)" |
143 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)" |
146 (* FIXME: Invalid intermediate term |
|
147 nitpick [show_datatypes, expect = genuine] |
144 nitpick [show_datatypes, expect = genuine] |
148 *) |
|
149 oops |
145 oops |
150 |
146 |
151 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2" |
147 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2" |
152 (* FIXME: Invalid intermediate term |
|
153 nitpick [show_datatypes, expect = genuine] |
148 nitpick [show_datatypes, expect = genuine] |
154 *) |
|
155 oops |
149 oops |
156 |
150 |
157 subsection {* 2.8. Inductive and Coinductive Predicates *} |
151 subsection {* 2.8. Inductive and Coinductive Predicates *} |
158 |
152 |
159 inductive even where |
153 inductive even where |