167 lemma trcl_step_blast: 

   167 lemma trcl_step_blast: 

   168 shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   168 shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   169 apply(unfold trcl_def)

   169 apply(unfold trcl_def)

   170 apply(blast)

   170 apply(blast)

   171 done

   171 done

   173 text {*

   173 text {*

   174   Experience has shown that it is generally a bad idea to rely heavily on

   174   Experience has shown that it is generally a bad idea to rely heavily on

   175   @{text blast}, @{text auto} and the like in automated proofs. The reason is

   175   @{text blast}, @{text auto} and the like in automated proofs. The reason is

   176   that you do not have precise control over them (the user can, for example,

   176   that you do not have precise control over them (the user can, for example,

   177   declare new intro- or simplification rules that can throw automatic tactics

   177   declare new intro- or simplification rules that can throw automatic tactics

   192   Since the predicates @{term even} and @{term odd} are mutually inductive, each 

   192   Since the predicates @{term even} and @{term odd} are mutually inductive, each 

   193   corresponding definition must quantify over both predicates (we name them 

   193   corresponding definition must quantify over both predicates (we name them 

   194   below @{text "P"} and @{text "Q"}).

   194   below @{text "P"} and @{text "Q"}).

   195 *}

   195 *}

   196 

   196 

   198   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 

   201   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 

   199                  \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"

   202                  \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"

   200 

   203 

   201 definition "odd \<equiv>

   204 definition "odd \<equiv>

   202   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 

   205   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))