equal
deleted
inserted
replaced
51 by (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2]) 3); |
51 by (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2]) 3); |
52 by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3); |
52 by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3); |
53 by (ALLGOALS (*using fib.rules here results in a longer proof!*) |
53 by (ALLGOALS (*using fib.rules here results in a longer proof!*) |
54 (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, |
54 (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, |
55 mod_less, mod_Suc] |
55 mod_less, mod_Suc] |
56 setloop split_tac[expand_if]))); |
56 addsplits [expand_if]))); |
57 by (safe_tac (!claset addSDs [mod2_neq_0])); |
57 by (safe_tac (!claset addSDs [mod2_neq_0])); |
58 by (ALLGOALS |
58 by (ALLGOALS |
59 (asm_full_simp_tac |
59 (asm_full_simp_tac |
60 (!simpset addsimps (fib.rules @ add_ac @ mult_ac @ |
60 (!simpset addsimps (fib.rules @ add_ac @ mult_ac @ |
61 [add_mult_distrib, add_mult_distrib2, |
61 [add_mult_distrib, add_mult_distrib2, |