equal
deleted
inserted
replaced
397 by (case_tac "y \<le> x", simp_all add: zdiff_int) |
397 by (case_tac "y \<le> x", simp_all add: zdiff_int) |
398 |
398 |
399 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)" |
399 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)" |
400 by simp |
400 by simp |
401 lemma number_of2: "(0::int) <= Numeral0" by simp |
401 lemma number_of2: "(0::int) <= Numeral0" by simp |
402 lemma Suc_plus1: "Suc n = n + 1" by simp |
|
403 |
402 |
404 text {* |
403 text {* |
405 \medskip Specific instances of congruence rules, to prevent |
404 \medskip Specific instances of congruence rules, to prevent |
406 simplifier from looping. *} |
405 simplifier from looping. *} |
407 |
406 |