equal
deleted
inserted
replaced
834 lemma word_of_nat: "of_nat n = word_of_int (int n)" |
834 lemma word_of_nat: "of_nat n = word_of_int (int n)" |
835 by (induct n) (auto simp add : word_of_int_hom_syms) |
835 by (induct n) (auto simp add : word_of_int_hom_syms) |
836 |
836 |
837 lemma word_of_int: "of_int = word_of_int" |
837 lemma word_of_int: "of_int = word_of_int" |
838 apply (rule ext) |
838 apply (rule ext) |
839 apply (unfold of_int_def) |
839 apply (case_tac x rule: int_diff_cases) |
840 apply (rule contentsI) |
840 apply (simp add: word_of_nat word_of_int_sub_hom) |
841 apply safe |
|
842 apply (simp_all add: word_of_nat word_of_int_homs) |
|
843 defer |
|
844 apply (rule Rep_Integ_ne [THEN nonemptyE]) |
|
845 apply (rule bexI) |
|
846 prefer 2 |
|
847 apply assumption |
|
848 apply (auto simp add: RI_eq_diff) |
|
849 done |
841 done |
850 |
842 |
851 lemma word_of_int_nat: |
843 lemma word_of_int_nat: |
852 "0 <= x ==> word_of_int x = of_nat (nat x)" |
844 "0 <= x ==> word_of_int x = of_nat (nat x)" |
853 by (simp add: of_nat_nat word_of_int) |
845 by (simp add: of_nat_nat word_of_int) |