equal
deleted
inserted
replaced
186 |
186 |
187 lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m" |
187 lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m" |
188 by (rule type_definition.Abs_inverse [OF type]) |
188 by (rule type_definition.Abs_inverse [OF type]) |
189 |
189 |
190 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n" |
190 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n" |
191 by (simp add: Abs_inverse IntDiv.pos_mod_conj [OF size0]) |
191 by (simp add: Abs_inverse pos_mod_conj [OF size0]) |
192 |
192 |
193 lemma Rep_Abs_0: "Rep (Abs 0) = 0" |
193 lemma Rep_Abs_0: "Rep (Abs 0) = 0" |
194 by (simp add: Abs_inverse size0) |
194 by (simp add: Abs_inverse size0) |
195 |
195 |
196 lemma Rep_0: "Rep 0 = 0" |
196 lemma Rep_0: "Rep 0 = 0" |