theory Ind_Prelims+ −
imports Ind_Intro + −
begin+ −
+ −
section\<open>Preliminaries\<close>+ −
+ −
text \<open>+ −
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.+ −
+ −
+ −
We first consider the transitive closure of a relation \<open>R\<close>. The + −
``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+ −
\<open>trcl R x y\<close> can be defined so that it holds if and only if \<open>P x y\<close> holds for every predicate \<open>P\<close> closed under the rules+ −
above. This gives rise to the definition+ −
\<close>+ −
+ −
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"+ −
+ −
text \<open>+ −
Note we have to use the object implication \<open>\<longrightarrow>\<close> and object+ −
quantification \<open>\<forall>\<close> for stating this definition (there is no other+ −
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+ −
proof method \<open>atomize\<close> (Line 4 below), expand the definition of @{term trcl}+ −
(Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),+ −
and then solve the goal by \<open>assumption\<close> (Line 8).+ −
+ −
\<close>+ −
+ −
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+ −
+ −
text \<open>+ −
The proofs for the introduction rules are slightly more complicated. + −
For the first one, we need to prove the following lemma:+ −
\<close>+ −
+ −
lemma %linenos trcl_base: + −
shows "trcl R x x"+ −
apply(unfold trcl_def)+ −
apply(rule allI impI)++ −
apply(drule spec)+ −
apply(assumption)+ −
done+ −
+ −
text \<open>+ −
We again unfold first the definition and apply introduction rules + −
for \<open>\<forall>\<close> and \<open>\<longrightarrow>\<close> as often as possible (Lines 3 and 4).+ −
We then end up in the goal state:+ −
\<close>+ −
+ −
(*<*)lemma "trcl R x x"+ −
apply (unfold trcl_def)+ −
apply (rule allI impI)+(*>*)+ −
txt \<open>@{subgoals [display]}\<close>+ −
(*<*)oops(*>*)+ −
+ −
text \<open>+ −
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+ −
solve the goal by \<open>assumption\<close> (Line 6).+ −
\<close>+ −
+ −
text \<open>+ −
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+ −
rules for \<open>\<forall>\<close> and \<open>\<longrightarrow>\<close>+ −
\<close>+ −
+ −
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)++ −
+ −
txt \<open>+ −
we obtain the goal state+ −
+ −
@{subgoals [display]} + −
+ −
To see better where we are, let us explicitly name the assumptions + −
by starting a subproof.+ −
\<close>+ −
+ −
subgoal premises for P+ −
proof -+ −
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"+ −
+ −
txt \<open>+ −
The assumptions \<open>p1\<close> and \<open>p2\<close> correspond to the premises of+ −
the second introduction rule (unfolded); the assumptions \<open>r1\<close> and \<open>r2\<close>+ −
come from the definition of @{term trcl}. We apply \<open>r2\<close> to the goal+ −
@{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+ −
implications into meta-level ones. This can be accomplished using the \<open>rule_format\<close> attribute. So we continue the proof with:+ −
+ −
\<close>+ −
+ −
apply (rule r2[rule_format])+ −
+ −
txt \<open>+ −
This gives us two new subgoals+ −
+ −
@{subgoals [display]} + −
+ −
which can be solved using assumptions \<open>p1\<close> and \<open>p2\<close>. The latter+ −
involves a quantifier and implications that have to be eliminated before it+ −
can be applied. To avoid potential problems with higher-order unification,+ −
we explicitly instantiate the quantifier to \<open>P\<close> and also match+ −
explicitly the implications with \<open>r1\<close> and \<open>r2\<close>. This gives+ −
the proof:+ −
\<close>+ −
+ −
apply(rule p1)+ −
apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])+ −
done+ −
qed+ −
done+ −
+ −
text \<open>+ −
Now we are done. It might be surprising that we are not using the automatic+ −
tactics available in Isabelle/HOL for proving this lemmas. After all \<open>blast\<close> would easily dispense of it.+ −
\<close>+ −
+ −
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"+ −
text \<open>+ −
Experience has shown that it is generally a bad idea to rely heavily on+ −
\<open>blast\<close>, \<open>auto\<close> 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 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+ −
the predicates \<open>even\<close> and \<open>odd\<close> given by+ −
+ −
\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 + −
below \<open>P\<close> and \<open>Q\<close>).+ −
\<close>+ −
+ −
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"+ −
+ −
text \<open>+ −
For proving the induction principles, we use exactly the same technique + −
as in the transitive closure example, namely:+ −
\<close>+ −
+ −
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+ −
+ −
text \<open>+ −
The only difference with the proof \<open>trcl_induct\<close> is that we have to+ −
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 + −
the \<open>trcl\<close>-example. We only show the proof of the second introduction + −
rule.+ −
\<close>+ −
+ −
lemma %linenos evenS: + −
shows "odd m \<Longrightarrow> even (Suc m)"+ −
apply (unfold odd_def even_def)+ −
apply (rule allI impI)++ −
subgoal premises for P Q+ −
proof -+ −
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+ −
done+ −
+ −
text \<open>+ −
The interesting lines are 7 to 15. Again, the assumptions fall into two categories:+ −
\<open>p1\<close> corresponds to the premise of the introduction rule; \<open>r1\<close>+ −
to \<open>r3\<close> come from the definition of \<open>even\<close>.+ −
In Line 13, we apply the assumption \<open>r2\<close> (since we prove the second+ −
introduction rule). In Lines 14 and 15 we apply assumption \<open>p1\<close> (if+ −
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.+ −
+ −
Next we define the accessible part of a relation \<open>R\<close> given by+ −
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.+ −
The definition of \<open>accpart\<close> is:+ −
\<close>+ −
+ −
definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"+ −
+ −
text \<open>+ −
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.+ −
\<close>+ −
+ −
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)++ −
subgoal premises for P+ −
proof -+ −
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])+ −
subgoal premises for y+ −
proof -+ −
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+ −
done+ −
qed+ −
done+ −
+ −
text \<open>+ −
As you can see, there are now two subproofs. The assumptions fall as usual into+ −
two categories (Lines 7 to 9). In Line 11, applying the assumption \<open>r1\<close> generates a goal state with the new local assumption @{term "R y x"},+ −
named \<open>r1_prem\<close> in the second subproof (Line 14). This local assumption is+ −
used to solve the goal @{term "P y"} with the help of assumption \<open>p1\<close>.+ −
+ −
+ −
\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.+ −
+ −
\<close>+ −
(*<*)end(*>*)+ −