equal
deleted
inserted
replaced
42 |
42 |
43 |
43 |
44 (** Successor **) |
44 (** Successor **) |
45 |
45 |
46 Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)"; |
46 Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)"; |
47 br sym 1; |
47 by (rtac sym 1); |
48 by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
48 by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
49 qed "Suc_nat_eq_nat_zadd1"; |
49 qed "Suc_nat_eq_nat_zadd1"; |
50 |
50 |
51 Goal "Suc (number_of v) = \ |
51 Goal "Suc (number_of v) = \ |
52 \ (if neg (number_of v) then #1 else number_of (bin_succ v))"; |
52 \ (if neg (number_of v) then #1 else number_of (bin_succ v))"; |