theory Ind_Examples

imports Main LaTeXsugar

begin

section{* Examples of Inductive Definitions \label{sec:ind-examples} *}

text {*

  \begin{center}

  @{term[mode=Axiom] "trcl R x x"} \hspace{5mm}

  @{term[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}

  \end{center}

  (FIXME first rule should be an ``axiom'')

  Note that the @{text trcl} predicate has two different kinds of parameters: the

  first parameter @{text R} stays \emph{fixed} throughout the definition, whereas

  the second and third parameter changes in the ``recursive call''.

  Since an inductively defined predicate is the least predicate closed under

  a collection of introduction rules, we define the predicate @{text "trcl R x y"} in

  such a way that it holds if and only if @{text "P x y"} holds for every predicate

  @{text P} closed under the rules above. This gives rise to the definition 

*}

definition "trcl R x y \<equiv> 

      \<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 x y"

text {*

  theorem 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, expand the definition of @{text trcl}, eliminate the universal quantifier

  contained in it, and then solve the goal by assumption.

*}

lemma trcl_induct:

  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"

  We now turn to the proofs of the introduction rules, which are slightly more complicated.

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

  then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible.

  We then end up in a proof state of the following form:

(*<*)oops(*>*)

lemma trcl_base: "trcl R x x"

  Since the second introduction rule has premises, its proof is not as easy as the previous

  one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"}

  and @{text "\<longrightarrow>"}, we get the proof state

  The third and fourth assumption corresponds to the first and second introduction rule,

  respectively, whereas the first and second assumption corresponds to the premises 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, we have to eliminate the universal quantifiers and turn the object-level

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

  attribute. Applying the assumption produces two new subgoals, which can be solved using

  the first and second assumption. The second assumption again involves a quantifier and

  implications that have to be eliminated before it can be applied. To avoid problems

  with higher order unification, it is advisable to provide an instantiation for the

  universally quantified predicate variable in the assumption.

*}

lemma trcl_step: "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 g1: "R x y" by fact

    have g2: "\<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 g3: "\<forall>x. P x x" by fact

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

    show ?case

      apply (rule g4 [rule_format])

      apply (rule g1)

      apply (rule g2 [THEN spec [where x=P], THEN mp, THEN mp, OF g3, OF g4])

      done

  qed

text {*

  This method of defining inductive predicates easily generalizes to mutually inductive

  predicates, like the predicates @{text even} and @{text odd} characterized by the

  following introduction rules:

  \begin{center}

  @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm}

  @{term[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}

  @{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}

  \end{center}

  Since the predicates are mutually inductive, each of the definitions contain two

  quantifiers over the predicates @{text P} and @{text Q}.

*}

definition "even n \<equiv> 

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

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

definition "odd n \<equiv>

  \<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 n"

text {*

  For proving the induction rule, we use exactly the same technique as in the transitive

  closure example:

*}

lemma even_induct:

  assumes even: "even n"

  shows "P 0 \<Longrightarrow> 

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

  apply (atomize (full))

  apply (cut_tac even)

  apply (unfold even_def)

  apply (drule spec [where x=P])

  apply (drule spec [where x=Q])

  apply assumption

  done

text {*

  A similar induction rule having @{term "Q n"} as a conclusion can be proved for

  the @{text odd} predicate.

  The proofs of the introduction rules are also very similar to the ones in the

  previous example. We only show the proof of the second introduction rule,

  since it is almost the same as the one for the third introduction rule,

  and the proof of the first rule is trivial.

*}

lemma evenS: "odd m \<Longrightarrow> even (Suc m)"

  apply (unfold odd_def even_def)

  apply (rule allI impI)+

  proof -

    case goal1

    show ?case

      apply (rule goal1(3) [rule_format])

      apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],

	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])

      done

  qed

(*<*)

lemma even0: "even 0"

  apply (unfold even_def)

  apply (rule allI impI)+

  apply assumption

  done

lemma oddS: "even m \<Longrightarrow> odd (Suc m)"

  apply (unfold odd_def even_def)

  apply (rule allI impI)+

  proof -

    case goal1

    show ?case

      apply (rule goal1(4) [rule_format])

      apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],

	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])

      done

  qed

(*>*)

text {*

  As a final example, we will consider the definition of the accessible

  part of a relation @{text R} characterized by the introduction rule

  \begin{center}

  @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}

  \end{center}

  whose premise involves a universal quantifier and an implication. The

  definition of @{text accpart} is as follows:

*}

definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"

text {*

  The proof of the induction theorem is again straightforward:

*}

lemma accpart_induct:

  assumes acc: "accpart R x"

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

  apply (atomize (full))

  apply (cut_tac acc)

  apply (unfold accpart_def)

  apply (drule spec [where x=P])

  apply assumption

  done

(*<*)

lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

  apply (unfold accpart_def)

  apply (rule allI impI)+

(*>*)

txt {*

  Proving the introduction rule is a little more complicated, due to the quantifier

  and the implication in the premise. We first convert the meta-level universal quantifier

  and implication to their object-level counterparts. Unfolding the definition of

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

  yields the following proof state:

  @{subgoals [display]}

  Applying the second assumption produces a proof state with the new local assumption

  @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the

  first assumption.

*}

(*<*)oops(*>*)

lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

  apply (unfold accpart_def)

  apply (rule allI impI)+

  proof -

    case goal1

    note goal1' = this

    show ?case

      apply (rule goal1'(2) [rule_format])

      proof -

        case goal1

        show ?case

	  apply (rule goal1'(1) [OF goal1, THEN spec [where x=P],

            THEN mp, OF goal1'(2)])

	  done

      qed

    qed

end