theory Ind_Prelims

imports Ind_Intro 

begin

  The user will just give a specification of inductive predicate(s) and

  expects from the package to produce a convenient reasoning

  infrastructure. This infrastructure needs to be derived from the definition

  that correspond to the specified predicate(s). Before we start with

  explaining all parts of the package, let us first give some examples showing

  how to define inductive predicates and then also how to generate a reasoning

  infrastructure for them. From the examples we will figure out a general

  method for defining inductive predicates. This is usually the first step in

  writing a package for Isabelle. 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-implementation we will develop in later sections.

  ``pencil-and-paper'' specification for the transitive closure is:

  \begin{center}\small

  @{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}

  As mentioned before, the package has to make an appropriate definition for

  @{term "trcl"}. Since an inductively defined predicate is the least

  predicate closed under a collection of introduction rules, the predicate

  above. This gives rise to the definition

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"

  way for definitions in HOL). However, the introduction rules and induction

  principles associated with the transitive closure should use the

  meta-connectives, since they simplify the reasoning for the user.

  With this definition, the proof of the induction principle for @{term trcl}

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

  connectives in the lemma to object-level connectives using the

  (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),

lemma %linenos trcl_induct:

assumes "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 assms)

apply(unfold trcl_def)

apply(drule spec[where x=P])

apply(assumption)

done

  The proofs for the introduction rules are slightly more complicated. 

  For the first one, we need to prove the following lemma:

lemma %linenos trcl_base: 

shows "trcl R x x"

apply(unfold trcl_def)

apply(rule allI impI)+

apply(drule spec)

apply(assumption)

done

  We again unfold first the definition and apply introduction rules 

  We then end up in the goal state:

(*<*)lemma "trcl R x x"

apply (unfold trcl_def)

apply (rule allI impI)+(*>*)

(*<*)oops(*>*)

  The two assumptions come from the definition of @{term trcl} and correspond

  to the introduction rules. Thus, all we have to do is to eliminate the

  universal quantifier in front of the first assumption (Line 5), and then

  Next we have to show that the second introduction rule also follows from the

  definition.  Since this rule has premises, the proof is a bit more

  involved. After unfolding the definitions and applying the introduction

lemma trcl_step: 

shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

apply (unfold trcl_def)

apply (rule allI impI)+

  we obtain the goal state

  @{subgoals [display]} 

  To see better where we are, let us explicitly name the assumptions 

  by starting a subproof.

proof -

  case (goal1 P)

  have p1: "R x y" by fact

  have p2: "\<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 r1: "\<forall>x. P x x" by fact

  have r2: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact

  show "P x z"

  @{term "P x z"}. In order for this assumption to be applicable as a rule, we

  have to eliminate the universal quantifier and turn the object-level

    apply (rule r2[rule_format])

  This gives us two new subgoals

  @{subgoals [display]} 

  involves a quantifier and implications that have to be eliminated before it

  can be applied. To avoid potential problems with higher-order unification,

  the proof:

    apply(rule p1)

    apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])

    done

qed

  Now we are done. It might be surprising that we are not using the automatic

lemma trcl_step_blast: 

shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

apply(unfold trcl_def)

apply(blast)

done

term "even"

  Experience has shown that it is generally a bad idea to rely heavily on

  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 in packages should be avoided or be constrained sufficiently.

  The method of defining inductive predicates by impredicative quantification

  also generalises to mutually inductive predicates. The next example defines

  \begin{center}\small

  @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}

  @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm}

  @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"}

  \end{center}

  Since the predicates @{term even} and @{term odd} are mutually inductive, each 

  corresponding definition must quantify over both predicates (we name them 

hide_const even

hide_const odd

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"

  For proving the induction principles, we use exactly the same technique 

  as in the transitive closure example, namely:

lemma even_induct:

assumes "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 assms)

apply(unfold even_def)

apply(drule spec[where x=P])

apply(drule spec[where x=Q])

apply(assumption)

done

  instantiate here two universal quantifiers.  We omit the other induction

  principle that has @{prop "even n"} as premise and @{term "Q n"} as conclusion.  

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

  rule.

lemma %linenos evenS: 

shows "odd m \<Longrightarrow> even (Suc m)"

apply (unfold odd_def even_def)

apply (rule allI impI)+

proof -

  case (goal1 P Q)

  have p1: "\<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 r1: "P 0" by fact

  have r2: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact

  have r3: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact

  show "P (Suc m)"

    apply(rule r2[rule_format])

    apply(rule p1[THEN spec[where x=P], THEN spec[where x=Q],

	           THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])

    done

qed

  The interesting lines are 7 to 15. Again, the assumptions fall into two categories:

  the second introduction rule had more premises we have to do that for all

  of them). In order for this assumption to be applicable, the quantifiers

  need to be instantiated and then also the implications need to be resolved

  with the other rules.

  the single rule:

  \begin{center}\small

  \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}

  \end{center}

  The interesting point of this definition is that it contains a quantification

  that ranges only over the premise and the premise has also a precondition.

definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"

  The proof of the induction principle is again straightforward and omitted.

  Proving the introduction rule is a little more complicated, because the 

  quantifier and the implication in the premise. The proof is as follows.

lemma %linenos accpartI: 

shows "(\<And>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 p1: "\<And>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 r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact

  show "P x"

    apply(rule r1[rule_format])

    proof -

      case (goal1 y)

      have r1_prem: "R y x" by fact

      show "P y"

	apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])

      done

  qed

qed

  As you can see, there are now two subproofs. The assumptions fall as usual into

  \begin{exercise}

  Give the definition for the freshness predicate for lambda-terms. The rules

  for this predicate are:

  \begin{center}\small

  @{prop[mode=Rule] "a\<noteq>b \<Longrightarrow> fresh a (Var b)"}\hspace{5mm}

  @{prop[mode=Rule] "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"}\\[2mm]

  @{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm}

  @{prop[mode=Rule] "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}

  \end{center}

  From the definition derive the induction principle and the introduction 

  rules. 

  \end{exercise}

  The point of all these examples is to get a feeling what the automatic

  proofs should do in order to solve all inductive definitions we throw at

  them.  This is usually the first step in writing a package. We next explain

  the parsing and typing part of the package.

(*<*)end(*>*)