--- a/ProgTutorial/Package/Ind_Prelims.thy Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/Package/Ind_Prelims.thy Tue Mar 31 20:31:18 2009 +0100
@@ -5,37 +5,48 @@
section{* Preliminaries *}
text {*
- The user will just give a specification of an inductive predicate and
+ 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. This will roughly mean that the
- package has three main parts, namely:
-
-
- \begin{itemize}
- \item parsing the specification and typing the parsed input,
- \item making the definitions and deriving the reasoning infrastructure, and
- \item storing the results in the theory.
- \end{itemize}
-
- Before we start with explaining all parts, let us first give three examples
- showing how to define inductive predicates by hand and then also how to
- prove by hand important properties about them. From these examples, we will
+ that correspond to the specified predicate(s). Before we start with
+ explaining all parts of the package, let us first give four examples showing
+ how to define inductive predicates by hand and then also how to prove by
+ hand properties about them. See Figure \ref{fig:paperpreds} for their usual
+ ``pencil-and-paper'' definitions. From these 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}. It is
- an inductive predicate characterised by the two introduction rules:
-
+ \begin{figure}[t]
+ \begin{boxedminipage}{\textwidth}
\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}
+ \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}
+ \begin{center}\small
+ \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
+ \end{center}
+ \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}
+ \end{boxedminipage}
+ \caption{Examples of four ``Pencil-and-paper'' definitions of inductively defined
+ predicates. In formal reasoning with Isabelle, the user just wants to give such
+ definitions and expects that the reasoning structure is derived automatically.
+ For this definitional packages need to be implemented.\label{fig:paperpreds}}
+ \end{figure}
- In Isabelle, the user will state for @{term trcl\<iota>} the specification:
+ We first consider the transitive closure of a relation @{text R}. The user will
+ state for @{term trcl\<iota>} the specification:
*}
simple_inductive
@@ -45,7 +56,7 @@
| step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z"
text {*
- As said above the package has to make an appropriate definition and provide
+ The package has to make an appropriate definition and provide
lemmas to reason about the predicate @{term trcl\<iota>}. 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
@@ -58,25 +69,25 @@
\<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}. 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
- should use the meta-connectives since they simplify the
- reasoning for the user.
+ 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), 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 assumption (Line 8).
+ 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"
+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)
@@ -90,7 +101,7 @@
*}
lemma %linenos trcl_base:
- shows "trcl R x x"
+shows "trcl R x x"
apply(unfold trcl_def)
apply(rule allI impI)+
apply(drule spec)
@@ -110,9 +121,10 @@
(*<*)oops(*>*)
text {*
- The two assumptions 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 assumption (Line 6).
+ 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 assumption (Line 6).
*}
text {*
@@ -123,7 +135,7 @@
*}
lemma trcl_step:
- shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
apply (unfold trcl_def)
apply (rule allI impI)+
@@ -147,8 +159,8 @@
txt {*
The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of
- the second introduction rule; the assumptions @{text "r1"} and @{text "r2"}
- correspond to the introduction rules. We apply @{text "r2"} to the goal
+ 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 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
@@ -183,7 +195,7 @@
*}
lemma trcl_step_blast:
- shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
apply(unfold trcl_def)
apply(blast)
done
@@ -195,20 +207,12 @@
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 sufficiently constrained.
+ 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} characterised by the following
- rules:
-
- \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}
-
- The user will state for this inductive definition the specification:
+ the predicates @{text even} and @{text odd}. The user will state for this
+ inductive definition the specification:
*}
simple_inductive
@@ -238,9 +242,8 @@
*}
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"
+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)
@@ -252,14 +255,14 @@
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 @{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.
-
+ 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)"
+shows "odd m \<Longrightarrow> even (Suc m)"
apply (unfold odd_def even_def)
apply (rule allI impI)+
proof -
@@ -277,6 +280,9 @@
qed
text {*
+ The interesting lines are 7 to 15. The assumptions fall into to 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
@@ -284,41 +290,22 @@
need to be instantiated and then also the implications need to be resolved
with the other rules.
-
- As a final example, we define the accessible part of a relation @{text R} characterised
- by the introduction rule
-
- \begin{center}\small
- \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
- \end{center}
-
- whose premise involves a universal quantifier and an implication. The
+ As a final example, we define the accessible part of a relation @{text R}
+ (see Figure~\ref{fig:paperpreds}). There the premsise of the introduction
+ rule involves a universal quantifier and an implication. 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.
-*}
-
-lemma accpart_induct:
- assumes "accpart R x"
- shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
-apply(atomize (full))
-apply(cut_tac prems)
-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. The proof is as follows.
+ 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"
+shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
apply (unfold accpart_def)
apply (rule allI impI)+
proof -
@@ -338,9 +325,10 @@
qed
text {*
- 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
- proof above (Line 14). This local assumption is used to solve
+ 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
+ proof (Line 14). This local assumption is used to solve
the goal @{term "P y"} with the help of assumption @{text "p1"}.
The point of these examples is to get a feeling what the automatic proofs