equal
deleted
inserted
replaced
170 Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n"; |
170 Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n"; |
171 by Auto_tac; |
171 by Auto_tac; |
172 qed "zmagnitude_int_of"; |
172 qed "zmagnitude_int_of"; |
173 |
173 |
174 Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n"; |
174 Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n"; |
175 by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset())); |
175 by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1); |
176 qed "zmagnitude_zminus_int_of"; |
176 qed "zmagnitude_zminus_int_of"; |
177 |
177 |
178 Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of]; |
178 Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of]; |
179 |
179 |
180 Goalw [zmagnitude_def] "zmagnitude(z) : nat"; |
180 Goalw [zmagnitude_def] "zmagnitude(z) : nat"; |