--- a/CookBook/Package/Ind_Prelims.thy Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,352 +0,0 @@
-theory Ind_Prelims
-imports Main LaTeXsugar"../Base" Simple_Inductive_Package
-begin
-
-section{* Preliminaries *}
-
-text {*
- The user will just give a specification of an inductive predicate 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
- 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:
-*}
-
-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
- 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.
-
- 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).
-
-*}
-
-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 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 {*
- 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; the assumptions @{text "r1"} and @{text "r2"}
- correspond to the introduction rules. 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
- 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 sufficiently constrained.
-
- 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:
-*}
-
-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>
- \<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>
- \<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 @{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 {*
- 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.
-
-
- 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
- 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.
-*}
-
-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 {*
- 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
- 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
- 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(*>*)