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