|
8264
|
1 |
(* Title: HOL/Numeral.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
(*Unfold all "let"s involving constants*)
|
|
|
7 |
Goalw [Let_def] "Let (number_of v) f == f (number_of v)";
|
|
|
8 |
by(Simp_tac 1);
|
|
|
9 |
qed "Let_number_of";
|
|
|
10 |
Addsimps [Let_number_of];
|
|
10707
|
11 |
|
|
|
12 |
(*The condition "True" is a hack to prevent looping.
|
|
|
13 |
Conditional rewrite rules are tried after unconditional ones, so a rule
|
|
|
14 |
like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
|
|
|
15 |
Goal "True ==> (number_of w = x) = (x = number_of w)";
|
|
|
16 |
by Auto_tac;
|
|
|
17 |
qed "number_of_reorient";
|
|
|
18 |
Addsimps [number_of_reorient];
|