Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CookBook/FirstSteps.thy
changeset 13 2b07da8b310d
parent 12 2f1736cb8f26
child 14 1c17e99f6f66
equal deleted inserted replaced
12:2f1736cb8f26 13:2b07da8b310d 
    62 
    62 
    63 text {*
 
    63 text {*
 
    64   then Isabelle's undo operation has no effect on the definition of 
    64   then Isabelle's undo operation has no effect on the definition of 
    65   @{ML "foo"}. 
    65   @{ML "foo"}. 
    66 
    66 
       
    67   (FIXME: add comment about including whole ML-files) 
       
    68 
    67   During developments you might find it necessary to quickly inspect some data
 
    69   During developments you might find it necessary to quickly inspect some data
 
    68   in your code. This can be done in a ``quick-and-dirty'' fashion using 
    70   in your code. This can be done in a ``quick-and-dirty'' fashion using 
    69   the function @{ML "warning"}. For example 
    71   the function @{ML "warning"}. For example 
    70 *}
 
    72 *}
 
    71 
    73 
    73   val _ = warning "any string"
 
    75   val _ = warning "any string"
 
    74 *}
 
    76 *}
 
    75 
    77 
    76 text {*
 
    78 text {*
 
    77   will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
 
    79   will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
 
    78   PolyML provides a convenient, though quick-and-dirty, method for converting 
    80   PolyML provides a convenient, though again ``quick-and-dirty'', method for 
    79   arbitrary values into strings, for example: 
    81   converting arbitrary values into strings, for example: 
    80 *}
 
    82 *}
 
    81 
    83 
    82 ML {*
 
    84 ML {*
 
    83   val _ = warning (makestring 1)
 
    85   val _ = warning (makestring 1)
 
    84 *}
 
    86 *}
 
    86 text {*
 
    88 text {*
 
    87   However this only works if the type of what is printed is monomorphic and not 
    89   However this only works if the type of what is printed is monomorphic and not 
    88   a function.
 
    90   a function.
 
    89 *}
 
    91 *}
 
    90 
    92 
    91 text {* (FIXME: add comment about including ML-files) *}
 
    93 text {* (FIXME: add here or in the appendix a comment about tracing) *}
 
    92 
    94 text {* (FIXME: maybe a comment about redirecting the trace information) *}
 
    93 
    95 
    94 section {* Antiquotations *}
 
    96 section {* Antiquotations *}
 
    95 
    97 
    96 text {*
 
    98 text {*
 
    97   The main advantage of embedding all code 
    99   The main advantage of embedding all code 
   104 ML {* Context.theory_name @{theory} *}
 
   106 ML {* Context.theory_name @{theory} *}
 
   105 
   107 
   106 text {* 
   108 text {* 
   107   where @{text "@{theory}"} is an antiquotation that is substituted with the
 
   109   where @{text "@{theory}"} is an antiquotation that is substituted with the
 
   108   current theory (remember that we assumed we are inside the theory CookBook). 
   110   current theory (remember that we assumed we are inside the theory CookBook). 
   109   The name of this theory can be extrated using the function @{ML "Context.theory_name"}. 
   111   The name of this theory can be extracted using the function @{ML "Context.theory_name"}. 
   110   So the code above returns the string @{ML "\"CookBook\""}.
 
   112   So the code above returns the string @{ML "\"CookBook\""}.
 
   111 
   113 
   112   Note, however, that antiquotations are statically scoped, that is the value is
 
   114   Note, however, that antiquotations are statically scoped, that is the value is
 
   113   determined at ``compile-time'', not ``run-time''. For example the function
 
   115   determined at ``compile-time'', not ``run-time''. For example the function
 
   114 
   116 
   133 ML {* @{typ "(int * nat) list"} *}
 
   135 ML {* @{typ "(int * nat) list"} *}
 
   134 ML {* @{thm allI} *}
 
   136 ML {* @{thm allI} *}
 
   135 
   137 
   136 text {*
 
   138 text {*
 
   137   In the course of this introduction, we will learn more about 
   139   In the course of this introduction, we will learn more about 
   138   these antoquotations: they greatly simplify Isabelle programming since one
 
   140   these antiquotations: they greatly simplify Isabelle programming since one
 
   139   can directly access all kinds of logical elements from ML.
 
   141   can directly access all kinds of logical elements from ML.
 
   140 
   142 
   141 *}
 
   143 *}
 
   142 
   144 
   143 section {* Terms *}
 
   145 section {* Terms *}
 
   149 
   151 
   150 ML {* @{term "(a::nat) + b = c"} *}
 
   152 ML {* @{term "(a::nat) + b = c"} *}
 
   151 
   153 
   152 text {*
 
   154 text {*
 
   153   This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
 
   155   This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
 
   154   representation of this term. This internal represenation corresponds to the 
   156   representation of this term. This internal representation corresponds to the 
   155   datatype defined in @{ML_file "Pure/term.ML"}.
 
   157   datatype @{ML_text "term"}.
 
   156   
   158   
   157   The internal representation of terms uses the usual de-Bruijn index mechanism where bound 
   159   The internal representation of terms uses the usual de-Bruijn index mechanism where bound 
   158   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
 
   160   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
 
   159   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
 
   161   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
 
   160   binds the corresponding variable. However, in Isabelle the names of bound variables are 
   162   binds the corresponding variable. However, in Isabelle the names of bound variables are 
   161   kept at abstractions for printing purposes, and so should be treated only as comments. 
   163   kept at abstractions for printing purposes, and so should be treated only as comments. 
   162 
   164 
   163   \begin{readmore}
 
   165   \begin{readmore}
 
   164   Terms are described in detail in \ichcite{ch:logic}. Their
 
   166   Terms are described in detail in \isccite{sec:terms}. Their
 
   165   definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
 
   167   definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
 
   166   \end{readmore}
 
   168   \end{readmore}
 
   167 
   169 
   168   Sometimes the internal representation can be surprisingly different
 
   170   Sometimes the internal representation of terms can be surprisingly different
 
   169   from what you see at the user level, because the layers of
 
   171   from what you see at the user level, because the layers of
 
   170   parsing/type checking/pretty printing can be quite elaborate. 
   172   parsing/type checking/pretty printing can be quite elaborate. 
   171 
   173 *}
 
       
   174 
       
   175 text {*
 
   172   \begin{exercise}
 
   176   \begin{exercise}
 
   173   Look at the internal term representation of the following terms, and
 
   177   Look at the internal term representation of the following terms, and
 
   174   find out why they are represented like this.
 
   178   find out why they are represented like this.
 
   175 
   179 
   176   \begin{itemize}
 
   180   \begin{itemize}
 
   179   \item @{term "{ [x::int] | x. x \<le> -2 }"}  
   183   \item @{term "{ [x::int] | x. x \<le> -2 }"}  
   180   \end{itemize}
 
   184   \end{itemize}
 
   181 
   185 
   182   Hint: The third term is already quite big, and the pretty printer
 
   186   Hint: The third term is already quite big, and the pretty printer
 
   183   may omit parts of it by default. If you want to see all of it, you
 
   187   may omit parts of it by default. If you want to see all of it, you
 
   184   can use @{ML "print_depth 50"} to set the limit to a value high enough.
 
   188   can use the following ML funtion to set the limit to a value high 
       
   189   enough:
 
   185   \end{exercise}
 
   190   \end{exercise}
 
   186 
   191 *}
 
   187   The anti-quotation @{text "@prop"} constructs terms of proposition type, 
   192 ML {* print_depth 50 *} 
   188   inserting the invisible @{text "Trueprop"} coercion when necessary. 
   193 
       
   194 text {*
 
       
   195   
       
   196   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
       
   197   inserting the invisible @{text "Trueprop"} coercions whenever necessary. 
   189   Consider for example
 
   198   Consider for example
 
   190 
   199 
   191 *}
 
   200 *}
 
   192 
   201 
   193 ML {* @{term "P x"} *}
 
   202 ML {* @{term "P x"} ; @{prop "P x"} *}
 
   194 
   203 
   195 ML {* @{prop "P x"} *}
 
   204 text {* which needs the coercion and *}
 
   196 
   205 
   197 text {* and *}
 
   206 
   198 
   207 ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
 
   199 
   208 
   200 ML {* @{term "P x \<Longrightarrow> Q x"} *}
 
   209 text {* which does not. *}
 
   201 
   210 
   202 ML {* @{prop "P x \<Longrightarrow> Q x"} *}
 
   211 section {* Constructing Terms Manually *} 
   203 
       
   204 section {* Construting Terms Manually *} 
       
   205 
   212 
   206 text {*
 
   213 text {*
 
   207 
   214 
   208   While antiquotations are very convenient for constructing terms, they can
 
   215   While antiquotations are very convenient for constructing terms, they can
 
   209   only construct fixed terms. However, one often needs to construct terms dynamially. 
   216   only construct fixed terms. Unfortunately, one often needs to construct terms 
   210   For example in order to write the function that returns the implication 
   217   dynamically. For example, a function that returns the implication 
   211   @{term "\<And>x. P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments, one can 
   218   @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as input terms 
   212   only write
 
   219   can only be written as
 
   213 *}
 
   220 *}
 
   214 
   221 
   215 
   222 
   216 ML {*
 
   223 ML {*
 
   217   fun make_PQ_imp P Q =
 
   224   fun make_imp P Q =
 
   218   let
 
   225   let
 
   219     val nat = HOLogic.natT
 
   226     val x = @{term "x::nat"}
 
   220     val x = Free ("x", nat)
 
       
   221   in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
 
   227   in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
 
   222                                     HOLogic.mk_Trueprop (Q $ x)))
 
   228                                     HOLogic.mk_Trueprop (Q $ x)))
 
   223   end
 
   229   end
 
   224 *}
 
   230 *}
 
   225 
   231 
   226 text {*
 
   232 text {*
 
   227 
   233 
   228   The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
   234   The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
   229   an antiquotation. 
   235   an antiquotation, like   
   230 *}
 
   236 *}
 
   231 
   237 
   232 text {*
 
   238 ML {*
 
   233 
   239   fun make_imp_wrong P Q = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
   234    The internal names of constants like @{term "zero"} or @{text "+"} are
 
   240 *}
 
   235   often more complex than one first expects. Here, the extra prefixes
 
   241 
   236   @{text zero_class} and @{text plus_class} are present because the
 
   242 text {*
 
   237   constants are defined within a type class. Guessing such internal
 
   243 
   238   names can be extremely hard, which is why the system provides
 
   244   To see the difference apply @{text "@{term S}"} and 
   239   another antiquotation: @{ML "@{const_name plus}"} gives just this
 
   245   @{text "@{term T}"} to the functions.
 
   240   name. For example 
   246   
   241 
   247 
   242 *}
 
   248   One tricky point in constructing terms by hand is to obtain the fully qualified 
   243 
   249   names for constants. For example the names for @{text "zero"} or @{text "+"} are
 
   244 ML {* @{const_name plus} *}
 
   250   more complex than one first expects, namely @{ML_text "HOL.zero_class.zero"} 
   245 
   251   and @{ML_text "HOL.plus_class.plus"}. The extra prefixes @{ML_text zero_class} 
   246 text {* produes the fully qualyfied name of the constant plus. *}
 
   252   and @{ML_text plus_class} are present because these constants are defined 
   247 
   253   within type classes; the prefix @{text "HOL"} indicates in which theory they are 
   248 
   254   defined. Guessing such internal names can sometimes be quite hard. Therefore 
   249 
   255   Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} does the expansion 
   250 
   256   automatically, for example:
 
   251 text {*
 
   257 
   252 
   258 *}
 
   253   There are many funtions in @{ML_file "Pure/logic.ML"} and
 
   259 
       
   260 ML {* @{const_name HOL.zero}; @{const_name  plus} *}
 
       
   261 
       
   262 text {*
 
       
   263 
       
   264   \begin{readmore}
 
       
   265   There are many functions in @{ML_file "Pure/logic.ML"} and
 
   254   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
   266   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
   255   easier. Have a look ther and try to solve the following exercises:
 
   267   easier.\end{readmore}
 
   256 
   268 
   257 *}
 
   269   Have a look at these files and try to solve the following two exercises:
 
   258 
   270 
   259 text {*
 
   271 *}
 
   260 
   272 
   261   \begin{exercise}
 
   273 text {*
 
       
   274 
       
   275   \begin{exercise}\label{fun:revsum}
 
   262   Write a function @{ML_text "rev_sum : term -> term"} that takes a
 
   276   Write a function @{ML_text "rev_sum : term -> term"} that takes a
 
   263   term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
 
   277   term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
 
   264   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
 
   278   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
 
   265   the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
   279   the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
   266   associates to the left. Try your function on some examples, and see if 
   280   associates to the left. Try your function on some examples. 
   267   the result typechecks. 
       
   268   \end{exercise}
 
   281   \end{exercise}
 
   269 *}
 
   282 *}
 
   270 
   283 
   271 ML {* 
   284 ML {* 
   272   fun rev_sum t =
 
   285   fun rev_sum t =
 
   296 
   309 
   297 
   310 
   298 section {* Type checking *}
 
   311 section {* Type checking *}
 
   299 
   312 
   300 text {* 
   313 text {* 
       
   314   
       
   315   (FIXME: Should we say something about types?)
 
       
   316 
   301   We can freely construct and manipulate terms, since they are just
 
   317   We can freely construct and manipulate terms, since they are just
 
   302   arbitrary unchecked trees. However, we eventually want to see if a
 
   318   arbitrary unchecked trees. However, we eventually want to see if a
 
   303   term is wellformed, or type checks, relative to a theory.
 
   319   term is well-formed, or type checks, relative to a theory.
 
   304 
       
   305   Type checking is done via the function @{ML cterm_of}, which turns 
   320   Type checking is done via the function @{ML cterm_of}, which turns 
   306   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   321   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   307   Unlike @{ML_type term}s, which are just trees, @{ML_type
 
   322   Unlike @{ML_type term}s, which are just trees, @{ML_type
 
   308   "cterm"}s are abstract objects that are guaranteed to be
 
   323   "cterm"}s are abstract objects that are guaranteed to be
 
   309   type-correct, and can only be constructed via the official
 
   324   type-correct, and can only be constructed via the official
 
   325         (Const (@{const_name plus}, natT --> natT --> natT) 
   340         (Const (@{const_name plus}, natT --> natT --> natT) 
   326          $ zero $ zero)
 
   341          $ zero $ zero)
 
   327   end
 
   342   end
 
   328 *}
 
   343 *}
 
   329 
   344 
       
   345 text {*
 
       
   346   
       
   347   \begin{exercise}
 
       
   348   Check that the function defined in Exercise~\ref{fun:revsum} returns a
 
       
   349   result that type checks.
 
       
   350   \end{exercise}
 
       
   351 
       
   352 *}
 
       
   353 
   330 section {* Theorems *}
 
   354 section {* Theorems *}
 
   331 
   355 
   332 text {*
 
   356 text {*
 
   333   Just like @{ML_type cterm}s, theorems (of type @{ML_type thm}) are
 
   357   Just like @{ML_type cterm}s, theorems (of type @{ML_type thm}) are
 
   334   abstract objects that can only be built by going through the kernel
 
   358   abstract objects that can only be built by going through the kernel
 
   335   interfaces, which means that all your proofs will be checked. The
 
   359   interfaces, which means that all your proofs will be checked. 
   336   basic rules of the Isabelle/Pure logical framework are defined in
 
   360 
   337   @{ML_file "Pure/thm.ML"}. 
   361   To see theorems in ``action'', let us give a proof for the following statement
 
   338 
       
   339   Using these rules, which are just ML functions, you can do simple
 
       
   340   natural deduction proofs on the ML level. For example, the statement
 
       
   341 *}
 
   362 *}
 
   342 
   363 
   343   lemma 
   364   lemma 
   344    assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
   365    assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
   345    and     assm\<^isub>2: "P t"
 
   366    and     assm\<^isub>2: "P t"
 
   346    shows "Q t"
 
   367    shows "Q t" (*<*)oops(*>*) 
   347    (*<*)oops(*>*) 
   368 
   348 
   369 text {*
 
   349 text {*
 
   370   on the ML level:\footnote{Note that @{text "|>"} is just reverse
 
   350   can be proved in ML like 
       
   351   this\footnote{Note that @{text "|>"} is just reverse
 
       
   352   application. This combinator, and several variants are defined in
 
   371   application. This combinator, and several variants are defined in
 
   353   @{ML_file "Pure/General/basics.ML"}}:
 
   372   @{ML_file "Pure/General/basics.ML"}.}
 
   354 
   373 
   355 *}
 
   374 *}
 
   356 
   375 
   357 
   376 ML {*
 
   358 
       
   359 ML {*
 
       
   360 
       
   361 let
 
   377 let
 
   362   val thy = @{theory}
 
   378   val thy = @{theory}
 
   363 
   379 
   364   val assm1 = cterm_of thy @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
 
   380   val assm1 = cterm_of thy @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
 
   365   val assm2 = cterm_of thy @{prop "((P::nat\<Rightarrow>bool) t)"}
 
   381   val assm2 = cterm_of thy @{prop "((P::nat\<Rightarrow>bool) t)"}
 
   373 
   389 
   374   Qt 
   390   Qt 
   375   |> implies_intr assm2
 
   391   |> implies_intr assm2
 
   376   |> implies_intr assm1
 
   392   |> implies_intr assm1
 
   377 end
 
   393 end
 
   378 
   394 *}
 
   379 *}
 
   395 
   380 
   396 text {*
 
   381 text {*
 
   397 
   382   For how the functions @{text "assume"}, @{text "forall_elim"} and so on work
 
   398   \begin{readmore}
 
   383   see \ichcite{sec:thms}. (FIXME correct name)
 
   399   For how the functions @{text "assume"}, @{text "forall_elim"} etc work
 
   384 
   400   see \isccite{sec:thms}. The basic functions for theorems are defined in
 
       
   401   @{ML_file "Pure/thm.ML"}. 
       
   402   \end{readmore}
 
   385 
   403 
   386 *}
 
   404 *}
 
   387 
   405 
   388 
   406 
   389 section {* Tactical Reasoning *}
 
   407 section {* Tactical Reasoning *}
 
   390 
   408 
   391 text {*
 
   409 text {*
 
   392   The goal-oriented tactical style is similar to the @{text apply}
 
   410   The goal-oriented tactical style reasoning of the ML level is similar 
   393   style at the user level. Reasoning is centered around a \emph{goal},
 
   411   to the @{text apply}-style at the user level, i.e.~the reasoning is centred 
   394   which is modified in a sequence of proof steps until it is solved.
 
   412   around a \emph{goal}, which is modified in a sequence of proof steps 
       
   413   until it is solved.
 
   395 
   414 
   396   A goal (or goal state) is a special @{ML_type thm}, which by
 
   415   A goal (or goal state) is a special @{ML_type thm}, which by
 
   397   convention is an implication of the form:
 
   416   convention is an implication of the form:
 
   398 
   417 
   399   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
 
   418   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
 
   400 
   419 
   401   Since the formula @{term C} could potentially be an implication, there is a
 
   420   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals. 
       
   421 
       
   422   Since the goal @{term C} can potentially be an implication, there is a
 
   402   @{text "#"} wrapped around it, which prevents that premises are 
   423   @{text "#"} wrapped around it, which prevents that premises are 
   403   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
 
   424   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
 
   404   prop"} is just the identity function and used as a syntactic marker. 
   425   prop"} is just the identity function and used as a syntactic marker. 
   405   For more on this goals see \ichcite{sec:tactical-goals}. (FIXME name)
 
   426   
       
   427   \begin{readmore}
 
       
   428   For more on goals see \isccite{sec:tactical-goals}. 
       
   429   \end{readmore}
 
   406 
   430 
   407   Tactics are functions that map a goal state to a (lazy)
 
   431   Tactics are functions that map a goal state to a (lazy)
 
   408   sequence of successor states, hence the type of a tactic is
 
   432   sequence of successor states, hence the type of a tactic is
 
   409   @{ML_type[display] "thm -> thm Seq.seq"}
 
   433   @{ML_type[display] "thm -> thm Seq.seq"}
 
   410   
   434   
   411   \begin{readmore}
 
   435   \begin{readmore}
 
   412   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
 
   436   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
 
   413   sequences. However one rarly onstructs sequences manually, but uses
 
   437   sequences. However in day-to-day Isabelle programming, one rarely 
   414   the predefined tactic combinators (tacticals) instead 
   438   constructs sequences explicitly, but uses the predefined tactic 
   415   (see @{ML_file "Pure/tctical.ML"}).
 
   439   combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}). 
       
   440   (FIXME: Pointer to the old reference manual)
 
   416   \end{readmore}
 
   441   \end{readmore}
 
   417 
   442 
   418   Note, however, that tactics are expected to behave nicely and leave 
   443   While tatics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
   419   the final conclusion @{term C} intact (that is only work on the @{text "A\<^isub>i"} 
   444   are expected to leave the conclusion @{term C} intact, with the 
   420   representing the subgoals to be proved) with the exception of possibly 
   445   exception of possibly instantiating schematic variables. 
   421   instantiating schematic variables. 
       
   422  
   446  
   423   To see how tactics work, let us transcribe a simple apply-style proof from the
 
   447   To see how tactics work, let us transcribe a simple @{text apply}-style 
   424   tutorial \cite{isa-tutorial} into ML:
 
   448   proof from the tutorial \cite{isa-tutorial} into ML:
 
   425 *}
 
   449 *}
 
   426 
   450 
   427 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
 
   451 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
 
   428 apply (erule disjE)
 
   452 apply (erule disjE)
 
   429  apply (rule disjI2)
 
   453  apply (rule disjI2)
 
   435 
   459 
   436 text {*
 
   460 text {*
 
   437   
   461   
   438   To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"}
 
   462   To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"}
 
   439   sets up a goal state for proving @{text goal} under the assumptions @{text assms} with
 
   463   sets up a goal state for proving @{text goal} under the assumptions @{text assms} with
 
   440   additional variables @{text params} (the variables that are generalised once the
 
   464   the variables @{text params} that will be generalised once the
 
   441   goal is proved); @{text "tac"} is a function that returns a tactic (FIXME see non-existing
 
   465   goal is proved; @{text "tac"} is a function that returns a tactic having some funny 
   442   explanation in the imp-manual). 
   466   input parameters (FIXME by possibly having an explanation in the implementation-manual). 
   443 
   467 
   444 *}
 
   468 *}
 
   445 
   469 
   446 
   470 
   447 
   471
isabelle-cookbook