equal
deleted
inserted
replaced
64 lemma expand_BIT: |
64 lemma expand_BIT: |
65 "numeral (Num.Bit0 w) = numeral w BIT False" |
65 "numeral (Num.Bit0 w) = numeral w BIT False" |
66 "numeral (Num.Bit1 w) = numeral w BIT True" |
66 "numeral (Num.Bit1 w) = numeral w BIT True" |
67 "- numeral (Num.Bit0 w) = (- numeral w) BIT False" |
67 "- numeral (Num.Bit0 w) = (- numeral w) BIT False" |
68 "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True" |
68 "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True" |
69 by (simp_all add: add_One BitM_inc) |
69 by (simp_all add: BitM_inc_eq add_One) |
70 |
70 |
71 lemma less_Bits: "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c" |
71 lemma less_Bits: "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c" |
72 by (auto simp: Bit_def) |
72 by (auto simp: Bit_def) |
73 |
73 |
74 lemma le_Bits: "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)" |
74 lemma le_Bits: "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)" |