equal
deleted
inserted
replaced
1322 |
1322 |
1323 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y" |
1323 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y" |
1324 unfolding dvd_def udvd_nat_alt by force |
1324 unfolding dvd_def udvd_nat_alt by force |
1325 |
1325 |
1326 lemmas unat_mono = word_less_nat_alt [THEN iffD1] |
1326 lemmas unat_mono = word_less_nat_alt [THEN iffD1] |
1327 |
|
1328 lemma no_no [simp] : "number_of (number_of b) = number_of b" |
|
1329 by (simp add: number_of_eq) |
|
1330 |
1327 |
1331 lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1" |
1328 lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1" |
1332 apply (unfold unat_def) |
1329 apply (unfold unat_def) |
1333 apply (simp only: int_word_uint word_arith_alts rdmods) |
1330 apply (simp only: int_word_uint word_arith_alts rdmods) |
1334 apply (subgoal_tac "uint x >= 1") |
1331 apply (subgoal_tac "uint x >= 1") |