diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Package/Ind_Prelims.thy --- a/ProgTutorial/Package/Ind_Prelims.thy Tue Mar 31 20:31:18 2009 +0100 +++ b/ProgTutorial/Package/Ind_Prelims.thy Wed Apr 01 12:26:56 2009 +0100 @@ -1,5 +1,5 @@ theory Ind_Prelims -imports Main LaTeXsugar"../Base" Simple_Inductive_Package +imports Main LaTeXsugar "../Base" begin section{* Preliminaries *} @@ -9,55 +9,25 @@ 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 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. + 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. - \begin{figure}[t] - \begin{boxedminipage}{\textwidth} + + + 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 \ trcl R y z \ trcl R x z"} \end{center} - \begin{center}\small - @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm} - @{prop[mode=Rule] "odd n \ even (Suc n)"} \hspace{5mm} - @{prop[mode=Rule] "even n \ odd (Suc n)"} - \end{center} - \begin{center}\small - \mbox{\inferrule{@{term "\y. R y x \ accpart R y"}}{@{term "accpart R x"}}} - \end{center} - \begin{center}\small - @{prop[mode=Rule] "a\b \ fresh a (Var b)"}\hspace{5mm} - @{prop[mode=Rule] "\fresh a t; fresh a s\ \ fresh a (App t s)"}\\[2mm] - @{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm} - @{prop[mode=Rule] "\a\b; fresh a t\ \ 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} - We first consider the transitive closure of a relation @{text R}. The user will - state for @{term trcl\} the specification: -*} - -simple_inductive - trcl\ :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" -where - base: "trcl\ R x x" -| step: "trcl\ R x y \ R y z \ trcl\ R x z" - -text {* - The package has to make an appropriate definition and provide - lemmas to reason about the predicate @{term trcl\}. Since an inductively + The package has to make an appropriate definition. 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 @@ -79,7 +49,7 @@ 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 @{text assumption} (Line 8). @@ -124,7 +94,7 @@ 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). + solve the goal by @{text assumption} (Line 6). *} text {* @@ -160,8 +130,8 @@ 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 the assumption to be applicable as a rule, we + 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: @@ -211,28 +181,24 @@ 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}. The user will state for this - inductive definition the specification: -*} + the predicates @{text even} and @{text odd} given by -simple_inductive - even and odd -where - even0: "even 0" -| evenS: "odd n \ even (Suc n)" -| oddS: "even n \ odd (Suc n)" + \begin{center}\small + @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm} + @{prop[mode=Rule] "odd n \ even (Suc n)"} \hspace{5mm} + @{prop[mode=Rule] "even n \ odd (Suc n)"} + \end{center} -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\ \ +definition "even \ \n. \P Q. P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" -definition "odd\ \ +definition "odd \ \n. \P Q. P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ Q n" @@ -280,7 +246,7 @@ qed text {* - The interesting lines are 7 to 15. The assumptions fall into to categories: + 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 @@ -290,10 +256,14 @@ 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} - (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: + Next we define the accessible part of a relation @{text R} given by + the single rule: + + \begin{center}\small + \mbox{\inferrule{@{term "\y. R y x \ accpart R y"}}{@{term "accpart R x"}}} + \end{center} + + The definition of @{text "accpart"} is: *} definition "accpart \ \R x. \P. (\x. (\y. R y x \ P y) \ P x) \ P x" @@ -325,15 +295,32 @@ qed text {* - 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"}. + 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"}. + - 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 + \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\b \ fresh a (Var b)"}\hspace{5mm} + @{prop[mode=Rule] "\fresh a t; fresh a s\ \ fresh a (App t s)"}\\[2mm] + @{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm} + @{prop[mode=Rule] "\a\b; fresh a t\ \ 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. *}