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 {*
  (FIXME check that the code works like as indicated)

  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