equal
deleted
inserted
replaced
38 |
38 |
39 (*Unfold all "let"s involving constants*) |
39 (*Unfold all "let"s involving constants*) |
40 lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)" |
40 lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)" |
41 by (simp add: Let_def) |
41 by (simp add: Let_def) |
42 |
42 |
43 (*The condition "True" is a hack to prevent looping. |
43 lemma Let_0 [simp]: "Let 0 f == f 0" |
44 Conditional rewrite rules are tried after unconditional ones, so a rule |
44 by (simp add: Let_def) |
45 like eq_nat_number_of will be tried first to eliminate #mm=#nn. *) |
45 |
46 lemma number_of_reorient [simp]: "True ==> (number_of w = x) = (x = number_of w)" |
46 lemma Let_1 [simp]: "Let 1 f == f 1" |
47 by auto |
47 by (simp add: Let_def) |
48 |
48 |
49 end |
49 end |