91 |
91 |
92 (* Simpler: use zabs_def as rewrite rule |
92 (* Simpler: use zabs_def as rewrite rule |
93 but arith_tac is not parameterized by such simp rules |
93 but arith_tac is not parameterized by such simp rules |
94 *) |
94 *) |
95 |
95 |
96 lemma zabs_split: "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))" |
96 lemma zabs_split [arith_split]: |
|
97 "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))" |
97 by (simp add: zabs_def) |
98 by (simp add: zabs_def) |
98 |
99 |
99 lemma zero_le_zabs [iff]: "0 \<le> abs (z::int)" |
100 lemma zero_le_zabs [iff]: "0 \<le> abs (z::int)" |
100 by (simp add: zabs_def) |
101 by (simp add: zabs_def) |
101 |
102 |
102 |
103 |
103 text{*This simplifies expressions of the form @{term "int n = z"} where |
104 text{*This simplifies expressions of the form @{term "int n = z"} where |
104 z is an integer literal.*} |
105 z is an integer literal.*} |
105 declare int_eq_iff [of _ "number_of v", standard, simp] |
106 declare int_eq_iff [of _ "number_of v", standard, simp] |
106 |
107 |
107 declare zabs_split [arith_split] |
|
108 |
|
109 lemma zabs_eq_iff: |
108 lemma zabs_eq_iff: |
110 "(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)" |
109 "(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)" |
111 by (auto simp add: zabs_def) |
110 by (auto simp add: zabs_def) |
112 |
111 |
113 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)" |
112 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)" |
114 by simp |
113 by simp |
115 |
114 |
116 lemma split_nat[arith_split]: |
115 lemma split_nat [arith_split]: |
117 "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" |
116 "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" |
118 (is "?P = (?L & ?R)") |
117 (is "?P = (?L & ?R)") |
119 proof (cases "i < 0") |
118 proof (cases "i < 0") |
120 case True thus ?thesis by simp |
119 case True thus ?thesis by simp |
121 next |
120 next |