theory Ind_Prelims+ −
imports Main LaTeXsugar "../Base" + −
begin+ −
+ −
section{* Preliminaries *}+ −
+ −
text {*+ −
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. 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 in later sections.+ −
+ −
+ −
+ −
We first consider the transitive closure of a relation @{text R}. 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}+ −
+ −
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 @{text "trcl R x y"} can be defined so+ −
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 \<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 {*+ −
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 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 @{text atomize} (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 @{text assumption} (Line 8).+ −
+ −
*}+ −
+ −
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 prems)+ −
apply(unfold trcl_def)+ −
apply(drule spec[where x=P])+ −
apply(assumption)+ −
done+ −
+ −
text {*+ −
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+ −
+ −
text {*+ −
We again unfold first the definition and apply introduction rules + −
for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible (Lines 3 and 4).+ −
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 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 @{text assumption} (Line 6).+ −
*}+ −
+ −
text {*+ −
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 @{text "\<forall>"} and @{text "\<longrightarrow>"}+ −
*}+ −
+ −
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 {* + −
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"+ −
+ −
txt {*+ −
The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of+ −
the second introduction rule (unfolded); the assumptions @{text "r1"} and @{text "r2"}+ −
come from the definition of @{term trcl}. We apply @{text "r2"} 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 @{text+ −
rule_format} attribute. So we continue the proof with:+ −
+ −
*}+ −
+ −
apply (rule r2[rule_format])+ −
+ −
txt {*+ −
This gives us two new subgoals+ −
+ −
@{subgoals [display]} + −
+ −
which can be solved using assumptions @{text p1} and @{text p2}. 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 @{text "P"} and also match+ −
explicitly the implications with @{text "r1"} and @{text "r2"}. This gives+ −
the proof:+ −
*}+ −
+ −
apply(rule p1)+ −
apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])+ −
done+ −
qed+ −
+ −
text {*+ −
Now we are done. 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: + −
shows "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 be constrained sufficiently.+ −
+ −
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} 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 @{text "P"} and @{text "Q"}).+ −
*}+ −
+ −
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 {*+ −
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 prems)+ −
apply(unfold even_def)+ −
apply(drule spec[where x=P])+ −
apply(drule spec[where x=Q])+ −
apply(assumption)+ −
done+ −
+ −
text {*+ −
The only difference with the proof @{text "trcl_induct"} 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 @{text "trcl"}-example. We only show the proof of the second introduction + −
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+ −
+ −
text {*+ −
The interesting lines are 7 to 15. The assumptions fall into two categories:+ −
@{text p1} corresponds to the premise of the introduction rule; @{text "r1"}+ −
to @{text "r3"} come from the definition of @{text "even"}.+ −
In Line 13, we apply the assumption @{text "r2"} (since we prove the second+ −
introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (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 @{text R} 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 definition of @{text "accpart"} is:+ −
*}+ −
+ −
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 {*+ −
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+ −
+ −
text {*+ −
As you can see, there are now two subproofs. The assumptions fall again into+ −
two categories (Lines 7 to 9). In Line 11, applying the assumption @{text+ −
"r1"} generates a goal state with the new local assumption @{term "R y x"},+ −
named @{text "r1_prem"} in the second subproof (Line 14). This local assumption is+ −
used to solve the goal @{term "P y"} with the help of assumption @{text+ −
"p1"}.+ −
+ −
+ −
\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(*>*)+ −