# HG changeset patch # User Christian Urban # Date 1238527878 -3600 # Node ID 7ff7325e3b4eed6fc73e4275752fdf8f1fab469f # Parent 75154f4d4e2f0526cd56792dba2574e7c6ae03d3 started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section) diff -r 75154f4d4e2f -r 7ff7325e3b4e ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Tue Mar 31 16:50:13 2009 +0100 +++ b/ProgTutorial/Package/Ind_Code.thy Tue Mar 31 20:31:18 2009 +0100 @@ -1101,4 +1101,68 @@ thm Even_def thm Odd_def +text {* + Second, we want that the user can specify fixed parameters. + Remember in the previous section we stated that the user can give the + specification for the transitive closure of a relation @{text R} as +*} + +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 {* + Note that there is no locale given in this specification---the parameter + @{text "R"} therefore needs to be included explicitly in @{term trcl\\}, but + stays fixed throughout the specification. The problem with this way of + stating the specification for the transitive closure is that it derives the + following induction principle. + + \begin{center}\small + \mprset{flushleft} + \mbox{\inferrule{ + @{thm_style prem1 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ + @{thm_style prem2 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ + @{thm_style prem3 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}} + {@{thm_style concl trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}}} + \end{center} + + But this does not correspond to the induction principle we derived by hand, which + was + + \begin{center}\small + \mprset{flushleft} + \mbox{\inferrule{ + @{thm_style prem1 trcl_induct[no_vars]}\\\\ + @{thm_style prem2 trcl_induct[no_vars]}\\\\ + @{thm_style prem3 trcl_induct[no_vars]}} + {@{thm_style concl trcl_induct[no_vars]}}} + \end{center} + + The difference is that in the one derived by hand the relation @{term R} is not + a parameter of the proposition @{term P} to be proved and it is also not universally + qunatified in the second and third premise. The point is that the parameter @{term R} + stays fixed thoughout the definition and we do not want to regard it as an ``ordinary'' + argument of the transitive closure, but one that can be freely instantiated. + In order to recognise such parameters, we have to extend the specification + to include a mechanism to state fixed parameters. The user should be able + to write + +*} + +(* +simple_inductive + trcl'' for R :: "'a \ 'a \ bool" +where + base: "trcl'' R x x" +| step: "trcl'' R x y \ R y z \ trcl'' R x z" + +simple_inductive + accpart'' for R :: "'a \ 'a \ bool" +where + accpartI: "(\y. R y x \ accpart'' R y) \ accpart'' R x" +*) + end diff -r 75154f4d4e2f -r 7ff7325e3b4e ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Tue Mar 31 16:50:13 2009 +0100 +++ b/ProgTutorial/Package/Ind_Interface.thy Tue Mar 31 20:31:18 2009 +0100 @@ -7,19 +7,19 @@ text {* To be able to write down the specification in Isabelle, we have to introduce a new command (see Section~\ref{sec:newcommand}). As the keyword for the - new command we chose \simpleinductive{}. In the package we want to support - some ``advanced'' features: First, we want that the package can cope with - specifications inside locales. For example it should be possible to declare + new command we chose \simpleinductive{}. The ``infrastructure'' already + provides an ``advanced'' feature for this command. For example we will + be able to declare the locale *} locale rel = fixes R :: "'a \ 'a \ bool" text {* - and then define the transitive closure and the accessible part as follows: + and then define the transitive closure and the accessible part of this + locale as follows: *} - simple_inductive (in rel) trcl' where @@ -31,68 +31,6 @@ where accpartI: "(\y. R y x \ accpart' y) \ accpart' x" -text {* - Second, we want that the user can specify fixed parameters. - Remember in the previous section we stated that the user can give the - specification for the transitive closure of a relation @{text R} as -*} - -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 {* - Note that there is no locale given in this specification---the parameter - @{text "R"} therefore needs to be included explicitly in @{term trcl\\}, but - stays fixed throughout the specification. The problem with this way of - stating the specification for the transitive closure is that it derives the - following induction principle. - - \begin{center}\small - \mprset{flushleft} - \mbox{\inferrule{ - @{thm_style prem1 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ - @{thm_style prem2 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ - @{thm_style prem3 trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}} - {@{thm_style concl trcl\\.induct[where P=P, where z=R, where za=x, where zb=y]}}} - \end{center} - - But this does not correspond to the induction principle we derived by hand, which - was - - \begin{center}\small - \mprset{flushleft} - \mbox{\inferrule{ - @{thm_style prem1 trcl_induct[no_vars]}\\\\ - @{thm_style prem2 trcl_induct[no_vars]}\\\\ - @{thm_style prem3 trcl_induct[no_vars]}} - {@{thm_style concl trcl_induct[no_vars]}}} - \end{center} - - The difference is that in the one derived by hand the relation @{term R} is not - a parameter of the proposition @{term P} to be proved and it is also not universally - qunatified in the second and third premise. The point is that the parameter @{term R} - stays fixed thoughout the definition and we do not want to regard it as an ``ordinary'' - argument of the transitive closure, but one that can be freely instantiated. - In order to recognise such parameters, we have to extend the specification - to include a mechanism to state fixed parameters. The user should be able - to write - -*} - -simple_inductive - trcl'' for R :: "'a \ 'a \ bool" -where - base: "trcl'' R x x" -| step: "trcl'' R x y \ R y z \ trcl'' R x z" - -simple_inductive - accpart'' for R :: "'a \ 'a \ bool" -where - accpartI: "(\y. R y x \ accpart'' R y) \ accpart'' R x" - text {* \begin{figure}[t] \begin{isabelle} @@ -102,7 +40,7 @@ \railalias{where}{\isacommand{where}} \railalias{for}{\isacommand{for}} \begin{rail} - simpleinductive target? fixes (for fixes)? \\ + simpleinductive target?\\ fixes (where (thmdecl? prop + '|'))? ; \end{rail} @@ -110,8 +48,7 @@ \caption{A railroad diagram describing the syntax of \simpleinductive{}. The \emph{target} indicates an optional locale; the \emph{fixes} are an \isacommand{and}-separated list of names for the inductive predicates (they - can also contain typing- and syntax anotations); similarly the \emph{fixes} - after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a + can also contain typing- and syntax anotations); \emph{prop} stands for a introduction rule with an optional theorem declaration (\emph{thmdecl}). \label{fig:railroad}} \end{figure} @@ -121,9 +58,17 @@ This leads directly to the railroad diagram shown in Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram more or less translates directly into the parser: +*} - @{ML_chunk [display,gray] parser} +ML %linenosgray{*val spec_parser = + OuterParse.fixes -- + Scan.optional + (OuterParse.$$$ "where" |-- + OuterParse.!!! + (OuterParse.enum1 "|" + (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} +text {* which we described in Section~\ref{sec:parsingspecs}. If we feed into the parser the string (which corresponds to our definition of @{term even} and @{term odd}): diff -r 75154f4d4e2f -r 7ff7325e3b4e ProgTutorial/Package/Ind_Prelims.thy --- 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 \ 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} - In Isabelle, the user will state for @{term trcl\} the specification: + We first consider the transitive closure of a relation @{text R}. The user will + state for @{term trcl\} the specification: *} simple_inductive @@ -45,7 +56,7 @@ | step: "trcl\ R x y \ R y z \ trcl\ 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\}. 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 @@ \ (\x y z. R x y \ P y z \ P x z) \ P x y" text {* - where we quantify over the predicate @{text P}. We have to use the - object implication @{text "\"} and object quantification @{text "\"} 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 "\"} and object quantification + @{text "\"} 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 "(\x. P x x) \ (\x y z. R x y \ P y z \ P x z) \ P x y" +assumes "trcl R x y" +shows "(\x. P x x) \ (\x y z. R x y \ P y z \ P x z) \ 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 \ trcl R y z \ trcl R x z" +shows "R x y \ trcl R y z \ 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 \ trcl R y z \ trcl R x z" +shows "R x y \ trcl R y z \ 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 \ even (Suc n)"} \hspace{5mm} - @{prop[mode=Rule] "even n \ 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 \ - (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" +assumes "even n" +shows "P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ 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 \ even (Suc m)" +shows "odd m \ 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 "\y. R y x \ 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 \ \R x. \P. (\x. (\y. R y x \ P y) \ P x) \ P x" text {* - The proof of the induction principle is again straightforward. -*} - -lemma accpart_induct: - assumes "accpart R x" - shows "(\x. (\y. R y x \ P y) \ P x) \ 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 "(\y. R y x \ accpart R y) \ accpart R x" +shows "(\y. R y x \ accpart R y) \ 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 diff -r 75154f4d4e2f -r 7ff7325e3b4e ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Tue Mar 31 16:50:13 2009 +0100 +++ b/ProgTutorial/Parsing.thy Tue Mar 31 20:31:18 2009 +0100 @@ -918,15 +918,16 @@ ML{*let fun trace_top_lvl str = - Toplevel.theory (fn thy => (tracing str; thy)) + LocalTheory.theory (fn lthy => (tracing str; lthy)) val trace_prop = OuterParse.prop >> trace_top_lvl val kind = OuterKeyword.thy_decl in - OuterSyntax.command "foobar" "traces a proposition" kind trace_prop + OuterSyntax.local_theory "foobar" "traces a proposition" kind trace_prop end *} + text {* Now you can type diff -r 75154f4d4e2f -r 7ff7325e3b4e ProgTutorial/document/root.rao --- a/ProgTutorial/document/root.rao Tue Mar 31 16:50:13 2009 +0100 +++ b/ProgTutorial/document/root.rao Tue Mar 31 20:31:18 2009 +0100 @@ -1,8 +1,8 @@ -% This file was generated by 'rail' from 'CookBook/generated/root.rai' +% This file was generated by 'rail' from 'ProgTutorial/generated/root.rai' \rail@t {simpleinductive} \rail@t {where} \rail@t {for} -\rail@i {1}{ simpleinductive target? fixes (for fixes)? \\ (where (thmdecl? prop + '|'))? ; } +\rail@i {1}{ simpleinductive target?\\ fixes (where (thmdecl? prop + '|'))? ; } \rail@o {1}{ \rail@begin{7}{} \rail@token{simpleinductive}[] @@ -10,14 +10,9 @@ \rail@nextbar{1} \rail@nont{target}[] \rail@endbar +\rail@cr{3} \rail@nont{fixes}[] \rail@bar -\rail@nextbar{1} -\rail@token{for}[] -\rail@nont{fixes}[] -\rail@endbar -\rail@cr{3} -\rail@bar \rail@nextbar{4} \rail@token{where}[] \rail@plus diff -r 75154f4d4e2f -r 7ff7325e3b4e ProgTutorial/document/root.tex --- a/ProgTutorial/document/root.tex Tue Mar 31 16:50:13 2009 +0100 +++ b/ProgTutorial/document/root.tex Tue Mar 31 20:31:18 2009 +0100 @@ -14,6 +14,7 @@ \usepackage{framed} \usepackage{boxedminipage} \usepackage{mathpartir} +\usepackage{flafter} \usepackage{pdfsetup} \urlstyle{rm} diff -r 75154f4d4e2f -r 7ff7325e3b4e progtutorial.pdf Binary file progtutorial.pdf has changed