equal
deleted
inserted
replaced
179 |
179 |
180 lemma DEF_MIN[import_const "MIN"]: |
180 lemma DEF_MIN[import_const "MIN"]: |
181 "min = (\<lambda>x y :: nat. if x \<le> y then x else y)" |
181 "min = (\<lambda>x y :: nat. if x \<le> y then x else y)" |
182 by (auto simp add: min.absorb_iff1 fun_eq_iff) |
182 by (auto simp add: min.absorb_iff1 fun_eq_iff) |
183 |
183 |
|
184 definition even |
|
185 where |
|
186 "even = Parity.even" |
|
187 |
184 lemma EVEN[import_const "EVEN" : even]: |
188 lemma EVEN[import_const "EVEN" : even]: |
185 "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))" |
189 "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))" |
186 by simp |
190 by (simp add: even_def) |
187 |
191 |
188 lemma SUB[import_const "-" : minus]: |
192 lemma SUB[import_const "-" : minus]: |
189 "(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))" |
193 "(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))" |
190 by simp |
194 by simp |
191 |
195 |