theory Demo9 imports Main begin

inductive Ev :: "nat \<Rightarrow> bool"
where
ZeroI: "Ev 0" |
Add2I: "Ev n \<Longrightarrow> Ev (Suc(Suc n))"

text {* Cases (rule inversion) in Isar *}

lemma "Ev n \<Longrightarrow> n = 0 \<or> (\<exists>Ev n'. n = Suc (Suc n'))"
proof -
  assume "Ev n"
  from this show "n = 0 \<or> (\<exists>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 \<or> (\<exists>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 \<Longrightarrow> \<exists>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 "\<exists>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 "\<exists>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 "\<exists>k. Suc (Suc m) = 2*k" ..
qed


end