equal
deleted
inserted
replaced
37 by (res_inst_tac [("u","n")] fib.induct 1); |
37 by (res_inst_tac [("u","n")] fib.induct 1); |
38 by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules))); |
38 by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules))); |
39 qed "fib_Suc_neq_0"; |
39 qed "fib_Suc_neq_0"; |
40 Addsimps [fib_Suc_neq_0]; |
40 Addsimps [fib_Suc_neq_0]; |
41 |
41 |
|
42 goal thy "0 < fib (Suc n)"; |
|
43 by (res_inst_tac [("u","n")] fib.induct 1); |
|
44 by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules))); |
|
45 qed "fib_Suc_gr_0"; |
|
46 Addsimps [fib_Suc_gr_0]; |
|
47 |
42 |
48 |
43 |
49 |
44 (*Concrete Mathematics, page 278: Cassini's identity*) |
50 (*Concrete Mathematics, page 278: Cassini's identity*) |
45 goal thy "fib (Suc (Suc n)) * fib n = \ |
51 goal thy "fib (Suc (Suc n)) * fib n = \ |
46 \ (if n mod 2 = 0 then pred(fib(Suc n) * fib(Suc n)) \ |
52 \ (if n mod 2 = 0 then pred(fib(Suc n) * fib(Suc n)) \ |