theory Ind_Examples

imports Main LaTeXsugar

begin

section{* Examples of Inductive Definitions \label{sec:ind-examples} *}

text {*

  As a first example, let us consider the transitive closure of a relation @{text

  \begin{center}

  \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

  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

  closure is almost immediate. It suffices to convert all the meta-level

  (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

  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.

*}

(*<*)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 {*

*}

(*<*)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 {*

  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)

    done

qed

text {*

*}

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 {*

  \begin{center}

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

*}

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 {*

  The proofs of the introduction rules are also very similar to the ones in the

*}

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 {*

  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 "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"

text {*

*}

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 {*

*}

end