equal
deleted
inserted
replaced
866 lemma uints_unats: "uints n = int ` unats n" |
866 lemma uints_unats: "uints n = int ` unats n" |
867 apply (unfold unats_def uints_num) |
867 apply (unfold unats_def uints_num) |
868 apply safe |
868 apply safe |
869 apply (rule_tac image_eqI) |
869 apply (rule_tac image_eqI) |
870 apply (erule_tac nat_0_le [symmetric]) |
870 apply (erule_tac nat_0_le [symmetric]) |
871 apply auto |
871 by auto |
872 apply (erule_tac nat_less_iff [THEN iffD2]) |
|
873 apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1]) |
|
874 apply (auto simp: nat_power_eq) |
|
875 done |
|
876 |
872 |
877 lemma unats_uints: "unats n = nat ` uints n" |
873 lemma unats_uints: "unats n = nat ` uints n" |
878 by (auto simp: uints_unats image_iff) |
874 by (auto simp: uints_unats image_iff) |
879 |
875 |
880 lemmas bintr_num = |
876 lemmas bintr_num = |