equal
deleted
inserted
replaced
1612 qed |
1612 qed |
1613 |
1613 |
1614 context ring_1 |
1614 context ring_1 |
1615 begin |
1615 begin |
1616 |
1616 |
1617 lemma of_int_of_nat [nitpick_const_simp]: |
1617 lemma of_int_of_nat [nitpick_simp]: |
1618 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" |
1618 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" |
1619 proof (cases "k < 0") |
1619 proof (cases "k < 0") |
1620 case True then have "0 \<le> - k" by simp |
1620 case True then have "0 \<le> - k" by simp |
1621 then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat) |
1621 then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat) |
1622 with True show ?thesis by simp |
1622 with True show ?thesis by simp |