equal
deleted
inserted
replaced
41 proof (induct n rule: fib.induct) |
41 proof (induct n rule: fib.induct) |
42 case 1 show ?case by simp |
42 case 1 show ?case by simp |
43 next |
43 next |
44 case 2 show ?case by (simp add: fib_2) |
44 case 2 show ?case by (simp add: fib_2) |
45 next |
45 next |
46 case 3 thus ?case by (simp add: fib_2 add_mult_distrib2) |
46 case fib_2 thus ?case by (simp add: fib.simps add_mult_distrib2) |
47 qed |
47 qed |
48 |
48 |
49 lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0" |
49 lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0" |
50 apply (induct n rule: fib.induct) |
50 apply (induct n rule: fib.induct) |
51 apply (simp_all add: fib_2) |
51 apply (simp_all add: fib_2) |
70 proof(induct n rule: fib.induct) |
70 proof(induct n rule: fib.induct) |
71 case 1 thus ?case by (simp add: fib_2) |
71 case 1 thus ?case by (simp add: fib_2) |
72 next |
72 next |
73 case 2 thus ?case by (simp add: fib_2 mod_Suc) |
73 case 2 thus ?case by (simp add: fib_2 mod_Suc) |
74 next |
74 next |
75 case (3 x) |
75 case (fib_2 x) |
76 have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger |
76 have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger |
77 with "3.hyps" show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2) |
77 with "fib_2.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2) |
78 qed |
78 qed |
79 |
79 |
80 text{*We now obtain a version for the natural numbers via the coercion |
80 text{*We now obtain a version for the natural numbers via the coercion |
81 function @{term int}.*} |
81 function @{term int}.*} |
82 theorem fib_Cassini: |
82 theorem fib_Cassini: |