theory Ind_Examples+
−
imports Main LaTeXsugar+
−
begin+
−
+
−
section{* Examples of Inductive Definitions \label{sec:ind-examples} *}+
−
+
−
text {*+
−
+
−
  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.  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 transitive+
−
  closure of a relation @{text R}. It is an inductive predicate characterized+
−
  by the two introduction rules+
−
+
−
  \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 {*+
−
  where we quantify over the predicate @{text P}.+
−
+
−
  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 {*+
−
+
−
  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 {*+
−
+
−
  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 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+
−