isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:a9eb69749c93
+:1dc03eaa7cb9
 theory Ind_Prelims
-imports Main LaTeXsugar"../Base" Simple_Inductive_Package
+imports Main LaTeXsugar "../Base"
 begin
 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
+that correspond to the specified predicate(s). Before we start with
-package has three main parts, namely:
+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
-\begin{itemize}
+we will figure out a general method for
-\item parsing the specification and typing the parsed input,
+defining inductive predicates.  The aim in this section is \emph{not} to
-\item making the definitions and deriving the reasoning infrastructure, and
+write proofs that are as beautiful as possible, but as close as possible to
-\item storing the results in the theory.
+the ML-code we will develop in later sections.
-\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
+We first consider the transitive closure of a relation @{text R}. The
-prove by hand important properties about them. From these examples, we will
+``pencil-and-paper'' specification for the transitive closure is:
-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{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}
-In Isabelle, the user will state for @{term trcl\<iota>} the specification:
+The package has to make an appropriate definition. Since an inductively
-*}
-simple_inductive
-trcl\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-base: "trcl\<iota> R x x"
-| 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
-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
 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 {*
-where we quantify over the predicate @{text P}. We have to use the
+We have to use the object implication @{text "\<longrightarrow>"} and object quantification
-object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for
+@{text "\<forall>"} for stating this definition (there is no other way for
-stating this definition (there is no other way for definitions in
+definitions in HOL). However, the introduction rules and induction
-HOL). However, the introduction rules and induction principles
+principles associated with the transitive closure should use the meta-connectives,
-should use the meta-connectives since they simplify the
+since they simplify the reasoning for the user.
-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}
+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 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"
 apply(atomize (full))
 apply(cut_tac prems)
 apply(unfold trcl_def)
 apply(drule spec[where x=P])
 apply(assumption)
 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
 apply (rule allI impI)+(*>*)
 txt {* @{subgoals [display]} *}
 (*<*)oops(*>*)
 text {*
-The two assumptions correspond to the introduction rules. Thus, all we have
+The two assumptions come from the definition of @{term trcl} and correspond
-to do is to eliminate the universal quantifier in front of the first
+to the introduction rules. Thus, all we have to do is to eliminate the
-assumption (Line 5), and then solve the goal by assumption (Line 6).
+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
 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; the assumptions @{text "r1"} and @{text "r2"}
+the second introduction rule (unfolded); the assumptions @{text "r1"} and @{text "r2"}
-correspond to the introduction rules. We apply @{text "r2"} to the goal
+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
+@{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:
 *}
 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 {*
 @{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 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
+the predicates @{text even} and @{text odd} given by
-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:
-*}
-simple_inductive
-even and odd
-where
-even0: "even 0"
-| evenS: "odd n \<Longrightarrow> even (Suc n)"
-| oddS: "even n \<Longrightarrow> odd (Suc n)"
-text {*
 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\<iota> \<equiv>
+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\<iota> \<equiv>
+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>
+shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
-(\<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])
 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 @{term "Q n"} as conclusion.  The proofs of the
+principle that has @{prop "even n"} as premise and @{term "Q n"} as conclusion.
-introduction rules are also very similar to the ones in the @{text
+The proofs of the introduction rules are also very similar to the ones in
-"trcl"}-example. We only show the proof of the second introduction rule.
+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))
 	           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
-As a final example, we define the accessible part of a relation @{text R} characterised
+the single rule:
-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
+The definition of @{text "accpart"} is:
-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.
+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 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.
 *}
 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>
 done
 qed
 qed
 text {*
-In Line 11, applying the assumption @{text "r1"} generates a goal state with
+As you can see, there are now two subproofs. The assumptions fall again into
-the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the
+two categories (Lines 7 to 9). In Line 11, applying the assumption @{text
-proof above (Line 14). This local assumption is used to solve
+"r1"} generates a goal state with the new local assumption @{term "R y x"},
-the goal @{term "P y"} with the help of assumption @{text "p1"}.
+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
-The point of these examples is to get a feeling what the automatic proofs
+"p1"}.
-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
+\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(*>*)

changeset 222	1dc03eaa7cb9
parent 219	98d43270024f
child 224	647cab4a72c2