theory tut04 imports Main begin inductive star :: "('a => 'a => bool) => 'a => 'a => bool" for R where star_refl: "star R x x" | star_append: "star R x y ==> R y z ==> star R x z" inductive star' :: "('a => 'a => bool) => 'a => 'a => bool" for R where star'_refl: "star' R x x" | star'_prepend: "R x y ==> star' R y z ==> star' R x z" lemma star_prepend: assumes "star R y z" assumes "R x y" shows "star R x z" using assms by (induction rule: star.induct) (auto intro: star.intros) lemma star_prepend_isar: assumes "star R y z" assumes "R x y" shows "star R x z" using assms proof induction case (star_refl y) thus ?case by (rule star.star_append[OF star.star_refl]) next case (star_append y z z') (*from star_append.IH `R x y` have "star R x z" . also note `R z z'` finally (star.star_append) have ?case .*) from star_append.IH `R x y` have 1: "star R x z" . from 1 `R z z'` show ?case by (metis star.star_append) qed notepad begin fix x y z :: nat assume "x R y z ==> star' R x z" by (induction rule: star'.induct) (auto intro: star'.intros) lemma "star R x y = star' R x y" proof assume "star R x y" thus "star' R x y" by induction (auto intro: star'_append star'_refl) next assume "star' R x y" thus "star R x y" by induction (auto intro: star_prepend star_refl) qed inductive ev where ev0: "ev 0" | evSS: "ev n ==> ev (Suc (Suc n))" lemma assumes A: "ev (Suc (Suc n))" shows "ev n" using A proof (cases) qed lemma "ev (Suc (Suc (Suc (Suc n)))) ==> ev n" proof - assume "ev (Suc (Suc (Suc (Suc n))))" then show "ev n" proof cases case evSS thus ?thesis by cases qed qed lemma "\ev (Suc (Suc (Suc 0)))" proof assume "ev (Suc (Suc (Suc 0)))" thus False proof cases assume "ev (Suc 0)" thus False by cases qed qed end