# HG changeset patch # User Christian Urban # Date 1257162420 -3600 # Node ID 2494b5b7a85df395dc7098470cdd8ed3e57d9635 # Parent 74ba778b09c9687f25da57732ca7c7e0563c3ae2 added something about show_types references diff -r 74ba778b09c9 -r 2494b5b7a85d ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sun Nov 01 10:49:25 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Mon Nov 02 12:47:00 2009 +0100 @@ -254,6 +254,38 @@ commas (map (string_of_term ctxt) ts)*} text {* + Sometimes you want to print out a term together with some type information. + This can be achieved by setting the reference + @{ML_ind show_types}\footnote{\bf FIXME: ``forgotten'' structure Printer, Mixfix etc.} + to @{ML true}. +*} + +ML{*show_types := true*} + +text {* + Now @{ML string_of_term} prints out + + @{ML_response_fake [display, gray] + "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" + "(1::nat, x::'a)"} + + where @{text 1} and @{text x} are displayed with their type. + Even more type information can be printed by setting + @{ML_ind show_all_types} to @{ML true}. We obtain +*} +(*<*)ML %linenos {*show_all_types := true*} +(*>*) +text {* + @{ML_response_fake [display, gray] + "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})" + "(Pair::nat \ 'a \ nat \ 'a) (1::nat) (x::'a)"} + + Other references that influence printing are @{ML_ind show_brackets} + and @{ML_ind show_sorts}. +*} +(*<*)ML %linenos {*show_types := false; show_all_types := false*} +(*>*) +text {* A @{ML_type cterm} can be transformed into a string by the following function. *} @@ -321,6 +353,13 @@ commas (map (string_of_thm_no_vars ctxt) thms) *} text {* + \begin{readmore} + The simple conversion functions from Isabelle's main datatypes to + @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. + The references that change the printing information are declared in + @{ML_file "Pure/Syntax/printer.ML"}. + \end{readmore} + Note that when printing out several ``parcels'' of information that semantically belong together, like a warning message consisting of a term and its type, you should try to keep this information together in a @@ -1303,7 +1342,7 @@ \begin{conventions} \begin{itemize} - \item Print messages that belong together as a single string. + \item Print messages that belong together in a single string. \item Do not use references in Isabelle code. \end{itemize} \end{conventions} diff -r 74ba778b09c9 -r 2494b5b7a85d ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Sun Nov 01 10:49:25 2009 +0100 +++ b/ProgTutorial/Tactical.thy Mon Nov 02 12:47:00 2009 +0100 @@ -1253,12 +1253,12 @@ text {* \begin{exercise}\label{ex:dyckhoff} - Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent + Dyckhoff presents in \cite{Dyckhoff92} inference rules of a sequent calculus, called G4ip, for intuitionistic propositional logic. The interesting feature of this calculus is that no contraction rule is needed - in order to be complete. As a result applying the rules exhaustively leads - to simple decision procedure for propositional intuitionistic logic. The task - is to implement this decision procedure as a tactic. His rules are + in order to be complete. As a result the rules can be applied exhaustively, which + in turn leads to simple decision procedure for propositional intuitionistic logic. + The task is to implement this decision procedure as a tactic. His rules are \begin{center} \def\arraystretch{2.3} @@ -1298,17 +1298,19 @@ \end{tabular} \end{center} - Note that in Isabelle the left-rules need to be implemented as elimination - rules. You need to prove separate lemmas corresponding to - $\longrightarrow_{L_{1..4}}$. The tactic should explore all possibilites of - applying these rules to a propositional formula until a goal state is - reached in which all subgoals are discharged. For this you can use the tactic - combinator @{ML_ind DEPTH_SOLVE in Search}. + Note that in Isabelle right rules need to be implemented as + introduction rule, the left rules as elimination rules. You have to to + prove separate theorems corresponding to $\longrightarrow_{L_{1..4}}$. The + tactic should explore all possibilites of applying these rules to a + propositional formula until a goal state is reached in which all subgoals + are discharged. For this you can use the tactic combinator @{ML_ind + DEPTH_SOLVE in Search} in the structure @{ML_struct Search}. \end{exercise} \begin{exercise} - Add to the previous exercise also rules for equality and run your tactic on - the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. + Add to the sequent calculus from the previous exercise also rules for + equality and run your tactic on the de Bruijn formulae discussed + in Exercise~\ref{ex:debruijn}. \end{exercise} *} @@ -1316,8 +1318,8 @@ text {* A lot of convenience in reasoning with Isabelle derives from its - powerful simplifier. We will describe it in this section, whereby - we can, however, only scratch the surface due to its complexity. + powerful simplifier. We will describe it in this section. However, + due to its complexity, we can mostly only scratch the surface. The power of the simplifier is a strength and a weakness at the same time, because you can easily make the simplifier run into a loop and in general @@ -1338,7 +1340,7 @@ \end{center} \end{isabelle} - All of the tactics take a simpset and an integer as argument (the latter as usual + All these tactics take a simpset and an integer as argument (the latter as usual to specify the goal to be analysed). So the proof *} @@ -1386,17 +1388,20 @@ with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"} and so on. Every simpset contains only one congruence rule for each term-constructor, which however can be overwritten. The user can declare - lemmas to be congruence rules using the attribute @{text "[cong]"}. In HOL, - the user usually states these lemmas as equations, which are then internally - transformed into meta-equations. + lemmas to be congruence rules using the attribute @{text "[cong]"}. Note that + in HOL these congruence theorems are usually stated as equations, which are + then internally transformed into meta-equations. The rewriting with theorems involving premises requires what is in Isabelle called a subgoaler, a solver and a looper. These can be arbitrary tactics that can be installed in a simpset and which are executed at various stages - during simplification. However, simpsets also include simprocs, which can - produce rewrite rules on demand (see next section). Another component are - split-rules, which can simplify for example the ``then'' and ``else'' - branches of if-statements under the corresponding preconditions. + during simplification. + + Simpsets can also include simprocs, which produce rewrite rules on + demand according to a pattern (see next section for a detailed description + of simpsets). Another component are split-rules, which can simplify for + example the ``then'' and ``else'' branches of if-statements under the + corresponding preconditions. \begin{readmore} For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"} @@ -1408,10 +1413,10 @@ \footnote{\bf FIXME: Find the right place to mention this: Discrimination nets are implemented in @{ML_file "Pure/net.ML"}.} - The most common combinators to modify simpsets are: + The most common combinators for modifying simpsets are: \begin{isabelle} - \begin{tabular}{ll} + \begin{tabular}{l@ {\hspace{10mm}}l} @{ML_ind addsimps in MetaSimplifier} & @{ML_ind delsimps in MetaSimplifier}\\ @{ML_ind addcongs in MetaSimplifier} & @{ML_ind delcongs in MetaSimplifier}\\ @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\ @@ -1497,9 +1502,10 @@ Simproc patterns:"} Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} - expects this form of the simplification and congruence rules. However, even + expects this form of the simplification and congruence rules. This is + different, if we use for example the simpset @{ML HOL_basic_ss} (see below), + where rules are usually added as equation. However, even when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet. - In the context of HOL, the first really useful simpset is @{ML_ind HOL_basic_ss in Simpdata}. While printing out the components of this simpset @@ -1509,7 +1515,7 @@ Congruences rules: Simproc patterns:"} - also produces ``nothing'', the printout is misleading. In fact + also produces ``nothing'', the printout is somewhat misleading. In fact the @{ML HOL_basic_ss} is setup so that it can solve goals of the form @@ -1565,7 +1571,7 @@ definition "MyTrue \ True" text {* - then we can use this tactic to unfold the definition of the constant. + then we can use this tactic to unfold the definition of this constant. *} lemma @@ -1578,7 +1584,7 @@ (*<*)oops(*>*) text {* - If you want to unfold definitions in \emph{all} subgoals not just one, + If you want to unfold definitions in \emph{all} subgoals, not just one, then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}. *} diff -r 74ba778b09c9 -r 2494b5b7a85d progtutorial.pdf Binary file progtutorial.pdf has changed