theory Ind_Examples
imports Main
begin

section{* Examples of inductive definitions *}

text {*
\label{sec:ind-examples}
In this section, we will give three examples showing how to define inductive
predicates by hand and prove characteristic properties such as introduction
rules and an induction rule. From these examples, we will then figure out a
general method for defining inductive predicates, which will be described in
\S\ref{sec:ind-general-method}. This description will serve as a basis for the
actual implementation to be developed in \S\ref{sec:ind-interface} -- \S\ref{sec:ind-proofs}.
It should be noted that our 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, we consider the \emph{transitive closure} @{text "trcl R"}
of a relation @{text R}. It is characterized by the following
two introduction rules
\[
\begin{array}{l}
@{term "trcl R x x"} \\
@{term [mode=no_brackets] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
\end{array}
\]
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 \emph{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 above rules. This gives rise to a definition containing
a universal quantifier over the predicate @{text P}:
*}

definition "trcl \<equiv> \<lambda>R x y.
  \<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 {*
\noindent
Since the predicate @{term "trcl R x y"} yields an element of the type of object
level truth values @{text bool}, the meta-level implications @{text "\<Longrightarrow>"} in the
above introduction rules have to be converted to object-level implications
@{text "\<longrightarrow>"}. Moreover, we use object-level universal quantifiers @{text "\<forall>"}
rather than meta-level universal quantifiers @{text "\<And>"} for quantifying over
the variable parameters of the introduction rules. Isabelle already offers some
infrastructure for converting between meta-level and object-level connectives,
which we will use later on.

With this definition of the transitive closure, the proof of the (weak) induction
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:
  assumes trcl: "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 trcl)
  apply (unfold trcl_def)
  apply (drule spec [where x=P])
  apply assumption
  done
(*<*)
lemma "trcl R x x"
  apply (unfold trcl_def)
  apply (rule allI impI)+
(*>*)
txt {*
\noindent
The above induction rule is \emph{weak} in the sense that the induction step may
only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not
using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule
containing this additional assumption can be derived from the weaker one with the
help of the introduction rules for @{text trcl}.

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:
@{subgoals [display]}
The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been
replaced by @{term "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:
*}
(*<*)oops(*>*)
lemma trcl_base: "trcl R x x"
  apply (unfold trcl_def)
  apply (rule allI impI)+
  apply (drule spec)
  apply assumption
  done
(*<*)
lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
  apply (unfold trcl_def)
  apply (rule allI impI)+
(*>*)
txt {*
\noindent
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
@{subgoals [display]}
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.
*}
(*<*)oops(*>*)
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
    show ?case
      apply (rule goal1(4) [rule_format])
      apply (rule goal1(1))
      apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp,
	OF goal1(3-4)])
      done
  qed

text {*
\noindent
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{array}{l}
@{term "even (0::nat)"} \\
@{term "odd m \<Longrightarrow> even (Suc m)"} \\
@{term "even m \<Longrightarrow> odd (Suc m)"}
\end{array}
\]
Since the predicates are mutually inductive, each of the definitions contain two
quantifiers over the predicates @{text P} and @{text Q}.
*}

definition "even \<equiv> \<lambda>n.
  \<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 \<equiv> \<lambda>n.
  \<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 {*
\noindent
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 {*
\noindent
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 {*
\noindent
As a final example, we will consider the definition of the accessible
part of a relation @{text R} characterized by the introduction rule
\[
@{term "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}
\]
whose premise involves a universal quantifier and an implication. The
definition of @{text accpart} is as follows:
*}

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

text {*
\noindent
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 {*
\noindent
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