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 how to prove characteristic properties about them, such as 
  introduction rules and an induction principle. From these examples, we will 
  figure out a 
  general method for defining inductive predicates.  The 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, let us 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}. Note that we have to use the
  object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for stating
  this definition. 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 theorem for the transitive
  closure 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 (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 goals @{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 goal, 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 introduction rule has premises, its proof 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 corresponds 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 in
  Isabelle in order to prove the lemmas we are after. After all @{text "blast"}
  would easily dispense of the lemmas.
*}

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 @{term blast}
  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. Therefore whenever possible, automatic tactics
  should be avoided or constrained. 
  

  This method of defining inductive predicates generalises also to mutually inductive
  predicates. The next example defines the predicates @{text even} and @{text odd} 
  characterised by the following 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 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 rule, we use exactly the same technique as in the transitive
  closure example:
*}

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 rule having @{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 definethe 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 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 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 proof 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 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.
*}

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 {*
  Now the point is to figure out what the automatic proofs should do. For
  this it might be instructive to look at the general construction principle
  of inductive definitions, which we shall do next.
*}

end