57 

    57 

    58 lemma %linenos trcl_induct:

    58 lemma %linenos trcl_induct:

    59 assumes "trcl R x y"

    59 assumes "trcl R x y"

    60 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"

    60 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"

    61 apply(atomize (full))

    61 apply(atomize (full))

    63 apply(unfold trcl_def)

    63 apply(unfold trcl_def)

    64 apply(drule spec[where x=P])

    64 apply(drule spec[where x=P])

    65 apply(assumption)

    65 apply(assumption)

    66 done

    66 done

    67 

    67 

   209 

   209 

   210 lemma even_induct:

   210 lemma even_induct:

   211 assumes "even n"

   211 assumes "even n"

   212 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   212 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   213 apply(atomize (full))

   213 apply(atomize (full))

   215 apply(unfold even_def)

   215 apply(unfold even_def)

   216 apply(drule spec[where x=P])

   216 apply(drule spec[where x=P])

   217 apply(drule spec[where x=Q])

   217 apply(drule spec[where x=Q])

   218 apply(assumption)

   218 apply(assumption)

   219 done

   219 done