equal
deleted
inserted
replaced
76 fixes n :: nat and x :: 'a |
76 fixes n :: nat and x :: 'a |
77 assumes a: "A n x" |
77 assumes a: "A n x" |
78 shows "P n x" |
78 shows "P n x" |
79 using a -- {* make induct insert fact a *} |
79 using a -- {* make induct insert fact a *} |
80 proof (induct n fixing: x) -- {* generalize goal to "!!x. A n x ==> P n x" *} |
80 proof (induct n fixing: x) -- {* generalize goal to "!!x. A n x ==> P n x" *} |
81 case (0 x) |
81 case 0 |
82 show ?case sorry |
82 show ?case sorry |
83 next |
83 next |
84 case (Suc n x) |
84 case (Suc n) |
85 note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *} |
85 note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *} |
86 note `A (Suc n) x` -- {* induction premise, stemming from fact a *} |
86 note `A (Suc n) x` -- {* induction premise, stemming from fact a *} |
87 show ?case sorry |
87 show ?case sorry |
88 qed |
88 qed |
89 |
89 |