35 notation (latex output) |
35 notation (latex output) |
36 square ("(_\<twosuperior>)" [1000] 999) |
36 square ("(_\<twosuperior>)" [1000] 999) |
37 |
37 |
38 notation (HTML output) |
38 notation (HTML output) |
39 square ("(_\<twosuperior>)" [1000] 999) |
39 square ("(_\<twosuperior>)" [1000] 999) |
|
40 |
|
41 |
|
42 subsection {* Predicate for negative binary numbers *} |
|
43 |
|
44 definition |
|
45 neg :: "int \<Rightarrow> bool" |
|
46 where |
|
47 "neg Z \<longleftrightarrow> Z < 0" |
|
48 |
|
49 lemma not_neg_int [simp]: "~ neg (of_nat n)" |
|
50 by (simp add: neg_def) |
|
51 |
|
52 lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))" |
|
53 by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc) |
|
54 |
|
55 lemmas neg_eq_less_0 = neg_def |
|
56 |
|
57 lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)" |
|
58 by (simp add: neg_def linorder_not_less) |
|
59 |
|
60 text{*To simplify inequalities when Numeral1 can get simplified to 1*} |
|
61 |
|
62 lemma not_neg_0: "~ neg 0" |
|
63 by (simp add: One_int_def neg_def) |
|
64 |
|
65 lemma not_neg_1: "~ neg 1" |
|
66 by (simp add: neg_def linorder_not_less zero_le_one) |
|
67 |
|
68 lemma neg_nat: "neg z ==> nat z = 0" |
|
69 by (simp add: neg_def order_less_imp_le) |
|
70 |
|
71 lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z" |
|
72 by (simp add: linorder_not_less neg_def) |
|
73 |
|
74 text {* |
|
75 If @{term Numeral0} is rewritten to 0 then this rule can't be applied: |
|
76 @{term Numeral0} IS @{term "number_of Pls"} |
|
77 *} |
|
78 |
|
79 lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)" |
|
80 by (simp add: neg_def) |
|
81 |
|
82 lemma neg_number_of_Min: "neg (number_of Int.Min)" |
|
83 by (simp add: neg_def) |
|
84 |
|
85 lemma neg_number_of_Bit0: |
|
86 "neg (number_of (Int.Bit0 w)) = neg (number_of w)" |
|
87 by (simp add: neg_def) |
|
88 |
|
89 lemma neg_number_of_Bit1: |
|
90 "neg (number_of (Int.Bit1 w)) = neg (number_of w)" |
|
91 by (simp add: neg_def) |
|
92 |
|
93 lemmas neg_simps [simp] = |
|
94 not_neg_0 not_neg_1 |
|
95 not_neg_number_of_Pls neg_number_of_Min |
|
96 neg_number_of_Bit0 neg_number_of_Bit1 |
40 |
97 |
41 |
98 |
42 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*} |
99 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*} |
43 |
100 |
44 declare nat_0 [simp] nat_1 [simp] |
101 declare nat_0 [simp] nat_1 [simp] |