theory Ind_Examples

imports Main LaTeXsugar

begin

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

text {*

  Let us first give three examples showing how to define inductive

  predicates by hand and then also how to prove by hand characteristic properties

  about them, such as introduction rules and induction principles. From

  these examples, we will figure out a general method for defining inductive

  predicates.  The aim in this section is \emph{not} to write proofs that are as

  beautiful as possible, but as close as possible to the ML-code we will 

  develop later.

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

  R}. It is an inductive predicate characterised by the two introduction rules:

  \begin{center}

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

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

  \end{center}

  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''. This will

  become important later on when we deal with fixed parameters and locales. 

  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 {*

  where we quantify over the predicate @{text P}. Note that we have to use the

  object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for

  stating this definition (there is no other way for definitions in

  HOL). However, 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 principle for the transitive

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

  connectives in the lemma to object-level connectives using the

  proof method @{text atomize} (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).

*}

lemma %linenos trcl_induct:

  assumes asm: "trcl R x y"

  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"

apply(atomize (full))

apply(cut_tac asm)

apply(unfold trcl_def)

apply(drule spec[where x=P])

apply(assumption)

done

text {*

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

  the facs @{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 fact, 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 the goal state:

*}

(*<*)lemma "trcl R x x"

apply (unfold trcl_def)

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

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

(*<*)oops(*>*)

text {*

  The two assumptions correspond to the introduction rules, where @{text "trcl

  R"} has been replaced by P. Thus, all we have to do is to eliminate the

  universal quantifier in front of the first assumption, and then solve the

  goal by assumption. Thus the proof is:

*}

lemma trcl_base: "trcl R x x"

apply(unfold trcl_def)

apply(rule allI impI)+

apply(drule spec)

apply(assumption)

done

text {*

  Since the second @{text trcl}-rule has premises, the proof of its

  introduction rule is not as easy. After unfolding the definitions and

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

  goal state:

*}

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

apply (unfold trcl_def)

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

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

(*<*)oops(*>*)

text {*

  The third and fourth assumption correspond 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:

*}

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 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

text {*

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

  Isabelle for proving this lemmas. After all @{text "blast"} would easily 

  dispense of it.

*}

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

  @{text blast}, @{text auto} 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 whenever something goes wrong. Therefore if possible, automatic 

  tactics should be avoided or sufficiently constrained.

  The method of defining inductive predicates by impredicative quantification

  also generalises to mutually inductive predicates. The next example defines

  the predicates @{text even} and @{text odd} characterised by the following

  rules:

  \begin{center}

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

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

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

  \end{center}

  Since the predicates are mutually inductive, each definition 

  quantifies over both predicates, below named @{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 principles, we use exactly the same technique 

  as in the transitive closure example, namely:

*}

lemma even_induct:

  assumes asm: "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 asm)

apply(unfold even_def)

apply(drule spec[where x=P])

apply(drule spec[where x=Q])

apply(assumption)

done

text {*

  We omit the other induction principle that has @{term "Q n"} as conclusion.

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

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

*}

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

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

text {*

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

  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:

*}

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 principle is again straightforward.

*}

lemma accpart_induct:

  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

  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 goal state:

*}

(*<*)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 {*

  Applying the second assumption produces a goal 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.

*}

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 {*

  The point of these examples is to get a feeling what the automatic proofs 

  should do in order to solve all inductive definitions we throw at them. For this 

  it is instructive to look at the general construction principle 

  of inductive definitions, which we shall do in the next section.

*}

end