equal
deleted
inserted
replaced
1711 "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" |
1711 "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" |
1712 "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" |
1712 "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" |
1713 "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" |
1713 "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" |
1714 "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" |
1714 "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" |
1715 "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" |
1715 "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" |
1716 apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM) |
1716 by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM) |
1717 apply (simp_all only: algebra_simps minus_diff_eq) |
|
1718 apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"]) |
|
1719 apply (simp_all only: minus_add add.assoc left_minus) |
|
1720 done |
|
1721 |
1717 |
1722 text \<open>Implementations.\<close> |
1718 text \<open>Implementations.\<close> |
1723 |
1719 |
1724 lemma one_int_code [code]: "1 = Pos Num.One" |
1720 lemma one_int_code [code]: "1 = Pos Num.One" |
1725 by simp |
1721 by simp |