by hand and then how to prove characteristic properties about them, such as 

  introduction rules and an induction principle. From these examples, we will 

  figure out a 

  general method for defining inductive predicates.  The aim in this section is 

  not to write proofs that are as beautiful as possible, but as close as 

  possible to the ML-code producing the proofs that we will develop later.

  As a first example, let us consider the transitive closure of a relation @{text

  this definition. The introduction rules and induction principles derived later

  should use the corresponding meta-connectives since they simplify the reasoning for

  the user.

  With this definition, the proof of the induction theorem for the transitive

  closure is almost immediate. It suffices to convert all the meta-level

  connectives in the induction rule to object-level connectives using the

  @{text atomize} proof method (Line 4), expand the definition of @{text trcl}

  (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7),

  and then solve the goal by assumption (Line 8).

  The proofs for the introduction are slightly more complicated. We need to prove

  the goals @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}.

  In order to prove the first goal, we again unfold the definition and

  We then end up in the goal state

apply (unfold trcl_def)

apply (rule allI impI)+(*>*)

  goal by assumption. Thus the proof is:

  Since the second introduction rule has premises, its proof is not as easy. After unfolding 

  the definitions and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we 

  get the goal state

apply (unfold trcl_def)

apply (rule allI impI)+(*>*)

  The third and fourth assumption corresponds to the first and second

  introduction rule, respectively, whereas the first and second assumption

  corresponds to the pre\-mises of the introduction rule. Since we want to prove

  the second introduction rule, we apply the fourth assumption to the goal

  @{term "P x z"}. In order for the assumption to be applicable as a rule, we have to

  eliminate the universal quantifier and turn the object-level implications

  into meta-level ones. This can be accomplished using the @{text rule_format}

  attribute. Applying the assumption produces the two new subgoals

*}

(*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

apply (unfold trcl_def)

apply (rule allI impI)+

proof -

  case (goal1 P)

  have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact

  show ?case

    apply (rule a4[rule_format])(*>*)

txt {*@{subgoals [display]} *}

(*<*)oops(*>*)

text {* 

  which can be

  solved using the first and second assumption. The second assumption again

  involves a quantifier and an implications that have to be eliminated before it

  can be applied. To avoid potential problems with higher-order unification, 

  we should explcitly instantiate the universally quantified

  predicate variable to @{text "P"} and also match explicitly the implications

  with the the third and fourth assumption. This gives the proof:

apply(unfold trcl_def)

apply(rule allI impI)+

proof -

  case (goal1 P)

  have a1: "R x y" by fact

  have a2: "\<forall>P. (\<forall>x. P x x) 

                  \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact

  have a3: "\<forall>x. P x x" by fact

  have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact

  show "P x z"

    apply(rule a4[rule_format])

    apply(rule a1)

    apply(rule a2 [THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4])

    done

qed

  It might be surprising that we are not using the automatic tactics in

  Isabelle in order to prove the lemmas we are after. After all @{text "blast"}

  would easily dispense of the lemmas.

*}

lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

apply(unfold trcl_def)

apply(blast)

done

text {*

  Experience has shown that it is generally a bad idea to rely heavily on @{term blast}

  and the like in automated proofs. The reason is that you do not have precise control 

  over them (the user can, for example, declare new intro- or simplification rules that 

  can throw automatic tactics off course) and also it is very hard to debug

  proofs involving automatic tactics. Therefore whenever possible, automatic tactics

  should be avoided or constrained. 

  This method of defining inductive predicates generalises also to mutually inductive

  predicates. The next example defines the predicates @{text even} and @{text odd} 

  characterised by the following rules:

  Since the predicates are mutually inductive, each definition 

  quantifies over both predicates, below named @{text P} and @{text Q}.

  assumes asm: "even n"

apply(atomize (full))

apply(cut_tac asm)

apply(unfold even_def)

apply(drule spec[where x=P])

apply(drule spec[where x=Q])

apply(assumption)

done

  We omit the other induction rule having @{term "Q n"} as conclusion.

  @{text "trcl"}-example. We only show the proof of the second introduction rule:

apply (unfold odd_def even_def)

apply (rule allI impI)+

proof -

  case (goal1 P)

  have a1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 

                             \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact

  have a2: "P 0" by fact

  have a3: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact

  have a4: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact

  show "P (Suc m)"

    apply(rule a3[rule_format])

    apply(rule a1[THEN spec[where x=P], THEN spec[where x=Q],

	THEN mp, THEN mp, THEN mp, OF a2, OF a3, OF a4])

    done

qed

  As a final example, we definethe accessible part of a relation @{text R} characterised 

  by the introduction rule

  The proof of the induction theorem is again straightforward.

  assumes asm: "accpart R x"

  shows "(\<And>x. (\<forall>y. R y x \<longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"

apply(atomize (full))

apply(cut_tac asm)

apply(unfold accpart_def)

apply(drule spec[where x=P])

apply(assumption)

done

text {*

  Proving the introduction rule is a little more complicated, because the quantifier

*}

(*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

apply (unfold accpart_def)

apply (rule allI impI)+(*>*)

txt {* @{subgoals [display]} *}

(*<*)oops(*>*)

text {*

lemma %small accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

apply (unfold accpart_def)

apply (rule allI impI)+

proof -

  case (goal1 P)

  have a1: "\<forall>y. R y x \<longrightarrow> 

                   (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact

  have a2: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact

  show "P x"

    apply(rule a2[rule_format])

    proof -

      case (goal1 y)

      have a3: "R y x" by fact

      show "P y"

      apply(rule a1[THEN spec[where x=y], THEN mp, OF a3, 

            THEN spec[where x=P], THEN mp, OF a2])

      done

  qed

qed

text {*

  Now the point is to figure out what the automatic proofs should do. For

  this it might be instructive to look at the general construction principle

  of inductive definitions, which we shall do next.

*}