theory Demo9 imports Main begin inductive Ev :: "nat \ bool" where ZeroI: "Ev 0" | Add2I: "Ev n \ Ev (Suc(Suc n))" text {* Cases (rule inversion) in Isar *} lemma "Ev n \ n = 0 \ (\Ev n'. n = Suc (Suc n'))" proof - assume "Ev n" from this show "n = 0 \ (\Ev n'. n = Suc (Suc n'))" proof cases assume "n = 0" thus ?thesis .. next fix n' assume "n = Suc (Suc n')" and "Ev n'" thus ?thesis by blast qed qed lemma assumes n: "Ev n" shows "n = 0 \ (\Ev n'. n = Suc (Suc n'))" using n proof cases case ZeroI thus ?thesis .. next case Add2I thus ?thesis by blast qed text {* Rule induction in Isar *} lemma "Ev n \ \k. n = 2*k" proof (induct rule: Ev.induct) case ZeroI thus ?case by simp next case Add2I thus ?case by arith qed lemma assumes n: "Ev n" shows "\k. n = 2*k" using n proof induct case ZeroI thus ?case by simp next case Add2I thus ?case by arith qed lemma assumes n: "Ev n" shows "\k. n = 2*k" using n proof induct case ZeroI thus ?case by simp next case (Add2I m) then obtain k where "m = 2*k" by blast hence "Suc (Suc m) = 2*(k+1)" by simp thus "\k. Suc (Suc m) = 2*k" .. qed end