# HG changeset patch # User Christian Urban # Date 1238585216 -3600 # Node ID 98d43270024f7c359b6159d43704707dd5f8c81c # Parent 7ff7325e3b4eed6fc73e4275752fdf8f1fab469f more work on the simple inductive chapter diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Tue Mar 31 20:31:18 2009 +0100 +++ b/ProgTutorial/Package/Ind_Code.thy Wed Apr 01 12:26:56 2009 +0100 @@ -1,5 +1,5 @@ theory Ind_Code -imports "../Base" "../FirstSteps" Ind_General_Scheme +imports "../Base" "../FirstSteps" Ind_Interface Ind_General_Scheme begin section {* The Gory Details\label{sec:code} *} @@ -798,7 +798,7 @@ *} lemma accpartI: - shows "\x. (\y. R y x \ accpart R y) \ accpart R x" + shows "\R x. (\y. R y x \ accpart R y) \ accpart R x" apply(tactic {* expand_tac @{thms accpart_def} *}) apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *}) apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *}) @@ -879,7 +879,7 @@ *} lemma accpartI: - shows "\x. (\y. R y x \ accpart R y) \ accpart R x" + shows "\R x. (\y. R y x \ accpart R y) \ accpart R x" apply(tactic {* expand_tac @{thms accpart_def} *}) apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *}) done @@ -1058,7 +1058,7 @@ ML{*val specification = spec_parser >> - (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*} + (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*} ML{*val _ = OuterSyntax.local_theory "simple_inductive" "define inductive predicates" @@ -1083,6 +1083,7 @@ *} +(* simple_inductive Even and Odd where @@ -1100,19 +1101,25 @@ 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 @@ -1132,14 +1139,15 @@ 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} + + %\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 @@ -1151,7 +1159,7 @@ to write *} - +*) (* simple_inductive trcl'' for R :: "'a \ 'a \ bool" @@ -1164,5 +1172,4 @@ where accpartI: "(\y. R y x \ accpart'' R y) \ accpart'' R x" *) - -end +(*<*)end(*>*) \ No newline at end of file diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Package/Ind_General_Scheme.thy --- a/ProgTutorial/Package/Ind_General_Scheme.thy Tue Mar 31 20:31:18 2009 +0100 +++ b/ProgTutorial/Package/Ind_General_Scheme.thy Wed Apr 01 12:26:56 2009 +0100 @@ -1,23 +1,10 @@ theory Ind_General_Scheme -imports Simple_Inductive_Package Ind_Prelims +imports Ind_Interface begin -(*<*) -datatype trm = - Var "string" -| App "trm" "trm" -| Lam "string" "trm" +section {* The Code in a Nutshell\label{sec:nutshell} *} -simple_inductive - fresh :: "string \ trm \ bool" -where - fresh_var: "a\b \ fresh a (Var b)" -| fresh_app: "\fresh a t; fresh a s\ \ fresh a (App t s)" -| fresh_lam1: "fresh a (Lam a t)" -| fresh_lam2: "\a\b; fresh a t\ \ fresh a (Lam b t)" -(*>*) -section {* The Code in a Nutshell\label{sec:nutshell} *} text {* The inductive package will generate the reasoning infrastructure for diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Tue Mar 31 20:31:18 2009 +0100 +++ b/ProgTutorial/Package/Ind_Interface.thy Wed Apr 01 12:26:56 2009 +0100 @@ -1,15 +1,106 @@ theory Ind_Interface -imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package +imports "../Base" "../Parsing" Simple_Inductive_Package begin section {* Parsing and Typing the Specification\label{sec:interface} *} +text_raw {* +\begin{figure}[p] +\begin{boxedminipage}{\textwidth} +\begin{isabelle} +*} +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" + +simple_inductive + even and odd +where + even0: "even 0" +| evenS: "odd n \ even (Suc n)" +| oddS: "even n \ odd (Suc n)" + +simple_inductive + accpart :: "('a \ 'a \ bool) \ 'a \ bool" +where + accpartI: "(\y. R y x \ accpart R y) \ accpart R x" + +(*<*) +datatype trm = + Var "string" +| App "trm" "trm" +| Lam "string" "trm" +(*>*) + +simple_inductive + fresh :: "string \ trm \ bool" +where + fresh_var: "a\b \ fresh a (Var b)" +| fresh_app: "\fresh a t; fresh a s\ \ fresh a (App t s)" +| fresh_lam1: "fresh a (Lam a t)" +| fresh_lam2: "\a\b; fresh a t\ \ fresh a (Lam b t)" +text_raw {* +\end{isabelle} +\end{boxedminipage} +\caption{Specification given by the user for the inductive predicates +@{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and +@{text "fresh"}.\label{fig:specs}} +\end{figure} +*} + +text {* + \begin{figure}[p] + \begin{boxedminipage}{\textwidth} + \begin{isabelle} + \railnontermfont{\rmfamily\itshape} + \railterm{simpleinductive,where,for} + \railalias{simpleinductive}{\simpleinductive{}} + \railalias{where}{\isacommand{where}} + \railalias{for}{\isacommand{for}} + \begin{rail} + simpleinductive target?\\ fixes + (where (thmdecl? prop + '|'))? + ; + \end{rail} + \end{isabelle} + \end{boxedminipage} + \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); \emph{prop} stands for a + introduction rule with an optional theorem declaration (\emph{thmdecl}). + \label{fig:railroad}} + \end{figure} +*} + 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{}. The ``infrastructure'' already - provides an ``advanced'' feature for this command. For example we will - be able to declare the locale + new command we chose \simpleinductive{}. Examples of specifications we expect + the user gives for the inductive predicates from the previous section are + shown in Figure~ref{fig:specs}. The general syntax we will parse is specified + in 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{*val spec_parser = + OuterParse.fixes -- + Scan.optional + (OuterParse.$$$ "where" |-- + OuterParse.!!! + (OuterParse.enum1 "|" + (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} + +text {* + which we explaind in Section~\ref{sec:parsingspecs}. + If you look closely, there is no code for parsing the optional + target in Figure~\ref{fig:railroad}. This is an ``advanced'' feature + which we will inherit for ``free'' from the infrastructure on which + we build the package. The target stands for a locale and allows us + to specify *} locale rel = @@ -32,44 +123,8 @@ accpartI: "(\y. R y x \ accpart' y) \ accpart' x" text {* - \begin{figure}[t] - \begin{isabelle} - \railnontermfont{\rmfamily\itshape} - \railterm{simpleinductive,where,for} - \railalias{simpleinductive}{\simpleinductive{}} - \railalias{where}{\isacommand{where}} - \railalias{for}{\isacommand{for}} - \begin{rail} - simpleinductive target?\\ fixes - (where (thmdecl? prop + '|'))? - ; - \end{rail} - \end{isabelle} - \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); \emph{prop} stands for a - introduction rule with an optional theorem declaration (\emph{thmdecl}). - \label{fig:railroad}} - \end{figure} -*} - -text {* - 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 %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 + Note that in these definitions the parameter @{text R} for the + relation is left implicit. If we feed into the parser the string (which corresponds to our definition of @{term even} and @{term odd}): @@ -88,22 +143,37 @@ [((even0,\), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} + + then we get back the predicates (with type + and syntax annotations), and the specifications of the introduction + rules. This is all the information we + need for calling the package and setting up the keyword. The latter is + done in Lines 6 and 7 in the code below. *} +(*<*) +ML{* fun add_inductive pred_specs rule_specs lthy = lthy *} +(*>*) + +ML{*fun add_inductive_cmd pred_specs rule_specs lthy = +let + val ((pred_specs', rule_specs'), _) = + Specification.read_spec pred_specs rule_specs lthy +in + add_inductive pred_specs' rule_specs' lthy +end*} + + +ML{*val specification = + spec_parser >> + (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*} + +ML{*val _ = OuterSyntax.local_theory "simple_inductive" + "definition of simple inductive predicates" + OuterKeyword.thy_decl specification*} + text {* - then we get back a locale (in this case @{ML NONE}), the predicates (with type - and syntax annotations), the parameters (similar as the predicates) and - the specifications of the introduction rules. - - - - This is all the information we - need for calling the package and setting up the keyword. The latter is - done in Lines 6 and 7 in the code below. - - @{ML_chunk [display,gray,linenos] syntax} - We call @{ML OuterSyntax.command} with the kind-indicator @{ML OuterKeyword.thy_decl} since the package does not need to open up any goal state (see Section~\ref{sec:newcommand}). Note that the predicates and @@ -399,8 +469,4 @@ the third with the introduction rules. *} - - -(*<*) -end -(*>*) +(*<*)end(*>*) \ No newline at end of file diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Package/Ind_Intro.thy --- a/ProgTutorial/Package/Ind_Intro.thy Tue Mar 31 20:31:18 2009 +0100 +++ b/ProgTutorial/Package/Ind_Intro.thy Wed Apr 01 12:26:56 2009 +0100 @@ -17,9 +17,9 @@ \medskip HOL is based on just a few primitive constants, like equality and implication, whose properties are described by axioms. All other concepts, - such as inductive predicates, datatypes, or recursive functions have to be defined + such as inductive predicates, datatypes or recursive functions, have to be defined in terms of those constants, and the desired properties, for example - induction theorems, or recursion equations have to be derived from the definitions + induction theorems or recursion equations, have to be derived from the definitions by a formal proof. Since it would be very tedious for a user to define complex inductive predicates or datatypes ``by hand'' just using the primitive operators of higher order logic, \emph{definitional packages} have @@ -29,7 +29,7 @@ definitions and proofs behind the scenes. In this chapter we explain how such a package can be implemented. - As a running example, we have chosen a rather simple package for defining + As the running example we have chosen a rather simple package for defining inductive predicates. To keep things really simple, we will not use the general Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis of Isabelle's standard inductive definition package. Instead, we 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. *} diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Tue Mar 31 20:31:18 2009 +0100 +++ b/ProgTutorial/Parsing.thy Wed Apr 01 12:26:56 2009 +0100 @@ -195,7 +195,7 @@ @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))" "Exception Error \"foo\" raised"} - This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} + This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.local_theory"} (see Section~\ref{sec:newcommand} which explains this function in more detail). Let us now return to our example of parsing @{ML "(p -- q) || r" for p q @@ -349,8 +349,6 @@ section {* Parsing Theory Syntax *} text {* - (FIXME: context parser) - Most of the time, however, Isabelle developers have to deal with parsing tokens, not strings. These token parsers have the type: *} @@ -619,12 +617,14 @@ for inductive predicates of the form: *} +(* simple_inductive even and odd where even0: "even 0" | evenS: "odd n \ even (Suc n)" | oddS: "even n \ odd (Suc n)" +*) text {* For this we are going to use the parser: @@ -679,7 +679,7 @@ val input = filtered_input \"foo::\\\"int \ bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\" in - parse OuterParse.fixes input + parse OuterParse.fixes input end" "([(foo, SOME \"\\^E\\^Ftoken\\^Eint \ bool\\^E\\^F\\^E\", NoSyn), (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), @@ -699,10 +699,10 @@ \end{readmore} Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a - list of introduction rules, that is propositions with theorem - annotations. The introduction rules are propositions parsed by @{ML - OuterParse.prop}. However, they can include an optional theorem name plus - some attributes. For example + list of introduction rules, that is propositions with theorem annotations + such as rule names and attributes. The introduction rules are propositions + parsed by @{ML OuterParse.prop}. However, they can include an optional + theorem name plus some attributes. For example @{ML_response [display,gray] "let val input = filtered_input \"foo_lemma[intro,dest!]:\" @@ -752,8 +752,6 @@ section {* New Commands and Keyword Files\label{sec:newcommand} *} text {* - (FIXME: update to the right command setup --- is this still needed?) - Often new commands, for example for providing new definitional principles, need to be implemented. While this is not difficult on the ML-level, new commands, in order to be useful, need to be recognised by @@ -766,16 +764,16 @@ *} ML{*let - val do_nothing = Scan.succeed (Toplevel.theory I) + val do_nothing = Scan.succeed (LocalTheory.theory I) val kind = OuterKeyword.thy_decl in - OuterSyntax.command "foobar" "description of foobar" kind do_nothing + OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing end *} text {* - The crucial function @{ML OuterSyntax.command} expects a name for the command, a - short description, a kind indicator (which we will explain later on more thoroughly) and a - parser producing a top-level transition function (its purpose will also explained + The crucial function @{ML OuterSyntax.local_theory} expects a name for the command, a + short description, a kind indicator (which we will explain later more thoroughly) and a + parser producing a local theory transition (its purpose will also explained later). While this is everything you have to do on the ML-level, you need a keyword @@ -803,15 +801,15 @@ \isacommand{ML}~@{text "\"}\\ @{ML "let - val do_nothing = Scan.succeed (Toplevel.theory I) + val do_nothing = Scan.succeed (LocalTheory.theory I) val kind = OuterKeyword.thy_decl in - OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing + OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing end"}\\ @{text "\"}\\ \isacommand{end} \end{graybox} - \caption{\small The file @{text "Command.thy"} is necessary for generating a log + \caption{The file @{text "Command.thy"} is necessary for generating a log file. This log file enables Isabelle to generate a keyword file containing the command \isacommand{foobar}.\label{fig:commandtheory}} \end{figure} @@ -909,25 +907,24 @@ The crucial part of a command is the function that determines the behaviour of the command. In the code above we used a ``do-nothing''-function, which because of @{ML Scan.succeed} does not parse any argument, but immediately - returns the simple toplevel function @{ML "Toplevel.theory I"}. We can + returns the simple function @{ML "LocalTheory.theory I"}. We can replace this code by a function that first parses a proposition (using the parser @{ML OuterParse.prop}), then prints out the tracing - information (using a new top-level function @{text trace_top_lvl}) and + information (using a new function @{text trace_prop}) and finally does nothing. For this you can write: *} ML{*let - fun trace_top_lvl str = + fun trace_prop str = LocalTheory.theory (fn lthy => (tracing str; lthy)) - val trace_prop = OuterParse.prop >> trace_top_lvl - + val trace_prop_parser = OuterParse.prop >> trace_prop val kind = OuterKeyword.thy_decl in - OuterSyntax.local_theory "foobar" "traces a proposition" kind trace_prop + OuterSyntax.local_theory "foobar" "traces a proposition" + kind trace_prop_parser end *} - text {* Now you can type @@ -938,17 +935,19 @@ and see the proposition in the tracing buffer. - Note that so far we used @{ML thy_decl in OuterKeyword} as the kind indicator - for the command. This means that the command finishes as soon as the - arguments are processed. Examples of this kind of commands are - \isacommand{definition} and \isacommand{declare}. In other cases, - commands are expected to parse some arguments, for example a proposition, - and then ``open up'' a proof in order to prove the proposition (for example + Note that so far we used @{ML thy_decl in OuterKeyword} as the kind + indicator for the command. This means that the command finishes as soon as + the arguments are processed. Examples of this kind of commands are + \isacommand{definition} and \isacommand{declare}. In other cases, commands + are expected to parse some arguments, for example a proposition, and then + ``open up'' a proof in order to prove the proposition (for example \isacommand{lemma}) or prove some other properties (for example - \isacommand{function}). To achieve this kind of behaviour, you have to use the kind - indicator @{ML thy_goal in OuterKeyword}. Note, however, once you change the - ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword} - then the keyword file needs to be re-created! + \isacommand{function}). To achieve this kind of behaviour, you have to use + the kind indicator @{ML thy_goal in OuterKeyword} and the function @{ML + "local_theory_to_proof" in OuterSyntax} to set up the command. Note, + however, once you change the ``kind'' of a command from @{ML thy_decl in + OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs + to be re-created! Below we change \isacommand{foobar} so that it takes a proposition as argument and then starts a proof in order to prove it. Therefore in Line 13, @@ -956,34 +955,32 @@ *} ML%linenosgray{*let - fun set_up_thm str ctxt = + fun prove_prop str ctxt = let val prop = Syntax.read_prop ctxt str in Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt end; - val prove_prop = OuterParse.prop >> - (fn str => Toplevel.print o - Toplevel.local_theory_to_proof NONE (set_up_thm str)) - + val prove_prop_parser = OuterParse.prop >> prove_prop val kind = OuterKeyword.thy_goal in - OuterSyntax.command "foobar" "proving a proposition" kind prove_prop + OuterSyntax.local_theory_to_proof "foobar" "proving a proposition" + kind prove_prop_parser end *} text {* - The function @{text set_up_thm} in Lines 2 to 7 takes a string (the proposition to be + The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be proved) and a context as argument. The context is necessary in order to be able to use @{ML Syntax.read_prop}, which converts a string into a proper proposition. In Line 6 the function @{ML Proof.theorem_i} starts the proof for the proposition. Its argument @{ML NONE} stands for a locale (which we chose to omit); the argument @{ML "(K I)"} stands for a function that determines what should be done with the theorem once it is proved (we chose to just forget - about it). Lines 9 to 11 contain the parser for the proposition. + about it). Line 9 contains the parser for the proposition. If you now type \isacommand{foobar}~@{text [quotes] "True \ True"}, you obtain the following - proof state: + proof state \begin{isabelle} \isacommand{foobar}~@{text [quotes] "True \ True"}\\ @@ -991,7 +988,7 @@ @{text "1. True \ True"} \end{isabelle} - and you can build the proof + and you can build the following proof \begin{isabelle} \isacommand{foobar}~@{text [quotes] "True \ True"}\\ @@ -1000,12 +997,6 @@ \isacommand{done} \end{isabelle} - - - (FIXME What do @{ML "Toplevel.theory"} - @{ML "Toplevel.print"} - @{ML Toplevel.local_theory} do?) - (FIXME read a name and show how to store theorems) *} diff -r 7ff7325e3b4e -r 98d43270024f ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Tue Mar 31 20:31:18 2009 +0100 +++ b/ProgTutorial/Tactical.thy Wed Apr 01 12:26:56 2009 +0100 @@ -1652,11 +1652,10 @@ @{text num} (Line 3), and then generates the meta-equation @{text "t \ num"} (Line 4), which it proves by the arithmetic tactic in Line 6. - For our purpose at the moment, proving the meta-equation using - @{ML Arith_Data.arith_tac} is - fine, but there is also an alternative employing the simplifier with a very - restricted simpset. For the kind of lemmas we want to prove, the simpset - @{text "num_ss"} in the code will suffice. + For our purpose at the moment, proving the meta-equation using @{ML + arith_tac in Arith_Data} is fine, but there is also an alternative employing + the simplifier with a special simpset. For the kind of lemmas we + want to prove here, the simpset @{text "num_ss"} should suffice. *} ML{*fun get_thm_alt ctxt (t, n) = @@ -1672,7 +1671,7 @@ text {* The advantage of @{ML get_thm_alt} is that it leaves very little room for something to go wrong; in contrast it is much more difficult to predict - what happens with @{ML Arith_Data.arith_tac}, especially in more complicated + what happens with @{ML arith_tac in Arith_Data}, especially in more complicated circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset that is sufficiently powerful to solve every instance of the lemmas we like to prove. This requires careful tuning, but is often necessary in diff -r 7ff7325e3b4e -r 98d43270024f progtutorial.pdf Binary file progtutorial.pdf has changed