# HG changeset patch # User Christian Urban # Date 1242570147 -7200 # Node ID ab9e09076462883a8634baba4bb89151222b4803 # Parent 5c211dd7e5add052a85d6edf4bdbf72e01821262 some polishing; added together with Jasmin more examples to the pretty printing section diff -r 5c211dd7e5ad -r ab9e09076462 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sat May 09 18:50:01 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Sun May 17 16:22:27 2009 +0200 @@ -9,14 +9,14 @@ in Isabelle is part of a theory. If you want to follow the code given in this chapter, we assume you are working inside the theory starting with - \begin{center} + \begin{quote} \begin{tabular}{@ {}l} \isacommand{theory} FirstSteps\\ \isacommand{imports} Main\\ \isacommand{begin}\\ \ldots \end{tabular} - \end{center} + \end{quote} We also generally assume you are working with HOL. The given examples might need to be adapted if you work in a different logic. @@ -59,7 +59,7 @@ to a separate ML-file. Such files can then be included somewhere inside a theory by using the command \isacommand{use}. For example - \begin{center} + \begin{quote} \begin{tabular}{@ {}l} \isacommand{theory} FirstSteps\\ \isacommand{imports} Main\\ @@ -69,13 +69,13 @@ \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\ \ldots \end{tabular} - \end{center} + \end{quote} The \isacommand{uses}-command in the header of the theory is needed in order to indicate the dependency of the theory on the ML-file. Alternatively, the file can be included by just writing in the header - \begin{center} + \begin{quote} \begin{tabular}{@ {}l} \isacommand{theory} FirstSteps\\ \isacommand{imports} Main\\ @@ -83,7 +83,7 @@ \isacommand{begin}\\ \ldots \end{tabular} - \end{center} + \end{quote} Note that no parentheses are given this time. *} @@ -181,7 +181,7 @@ A @{ML_type cterm} can be transformed into a string by the following function. *} -ML{*fun str_of_cterm ctxt t = +ML{*fun string_of_cterm ctxt t = Syntax.string_of_term ctxt (term_of t)*} text {* @@ -190,23 +190,23 @@ printed, you can use the function @{ML commas} to separate them. *} -ML{*fun str_of_cterms ctxt ts = - commas (map (str_of_cterm ctxt) ts)*} +ML{*fun string_of_cterms ctxt ts = + commas (map (string_of_cterm ctxt) ts)*} text {* The easiest way to get the string of a theorem is to transform it into a @{ML_type cterm} using the function @{ML crep_thm}. *} -ML{*fun str_of_thm ctxt thm = - str_of_cterm ctxt (#prop (crep_thm thm))*} +ML{*fun string_of_thm ctxt thm = + string_of_cterm ctxt (#prop (crep_thm thm))*} text {* Theorems also include schematic variables, such as @{text "?P"}, @{text "?Q"} and so on. @{ML_response_fake [display, gray] - "writeln (str_of_thm @{context} @{thm conjI})" + "writeln (string_of_thm @{context} @{thm conjI})" "\?P; ?Q\ \ ?P \ ?Q"} In order to improve the readability of theorems we convert @@ -221,30 +221,28 @@ thm' end -fun str_of_thm_no_vars ctxt thm = - str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*} +fun string_of_thm_no_vars ctxt thm = + string_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*} text {* Theorem @{thm [source] conjI} is now printed as follows: @{ML_response_fake [display, gray] - "writeln (str_of_thm_no_vars @{context} @{thm conjI})" + "writeln (string_of_thm_no_vars @{context} @{thm conjI})" "\P; Q\ \ P \ Q"} Again the function @{ML commas} helps with printing more than one theorem. *} -ML{*fun str_of_thms ctxt thms = - commas (map (str_of_thm ctxt) thms) +ML{*fun string_of_thms ctxt thms = + commas (map (string_of_thm ctxt) thms) -fun str_of_thms_no_vars ctxt thms = - commas (map (str_of_thm_no_vars ctxt) thms) *} +fun string_of_thms_no_vars ctxt thms = + commas (map (string_of_thm_no_vars ctxt) thms) *} section {* Combinators\label{sec:combinators} *} text {* - (FIXME: Calling convention) - For beginners perhaps the most puzzling parts in the existing code of Isabelle are the combinators. At first they seem to greatly obstruct the comprehension of the code, but after getting familiar with them, they @@ -287,8 +285,8 @@ common when dealing with theories (for example by adding a definition, followed by lemmas and so on). The reverse application allows you to read what happens in a top-down manner. This kind of coding should also be familiar, - if you have been exposed to Haskell's do-notation. Writing the function @{ML inc_by_five} using - the reverse application is much clearer than writing + if you have been exposed to Haskell's {\it do}-notation. Writing the function + @{ML inc_by_five} using the reverse application is much clearer than writing *} ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*} @@ -481,6 +479,7 @@ contains further information about combinators. \end{readmore} + (FIXME: say something abou calling conventions) *} @@ -543,7 +542,7 @@ text {* The function @{ML dest_ss in MetaSimplifier} returns a record containing all information stored in the simpset, but we are only interested in the names of the - simp-rules. So now you can feed in the current simpset into this function. + simp-rules. Now you can feed in the current simpset into this function. The current simpset can be referred to using the antiquotation @{text "@{simpset}"}. @{ML_response_fake [display,gray] @@ -555,7 +554,7 @@ On the ML-level of Isabelle, you often have to work with qualified names; these are strings with some additional information, such as positional information - and qualifiers. Such bindings can be generated with the antiquotation + and qualifiers. Such qualified names can be generated with the antiquotation @{text "@{binding \}"}. @{ML_response [display,gray] @@ -582,7 +581,8 @@ \end{isabelle} (FIXME give a better example why bindings are important; maybe - give a pointer to \isacommand{local\_setup}) + give a pointer to \isacommand{local\_setup}; if not, then explain + why @{ML snd} is needed) While antiquotations have many applications, they were originally introduced in order to avoid explicit bindings of theorems such as: @@ -605,7 +605,7 @@ text {* One way to construct Isabelle terms, is by using the antiquotation - \mbox{@{text "@{term \}"}}. For example: + \mbox{@{text "@{term \}"}}. For example @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" @@ -613,18 +613,67 @@ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} will show the term @{term "(a::nat) + b = c"}, but printed using the internal - representation corresponding to the data type @{ML_type "term"}. - - This internal representation uses the usual de Bruijn index mechanism---where - bound variables are represented by the constructor @{ML Bound}. The index in + representation corresponding to the datatype @{ML_type "term"}. Since Isabelle + uses Church-style terms, the datatype @{ML_type term} must be defined in + conjunction with types, that is the datatype @{ML_type typ}: +*} + +ML_val{*datatype typ = + Type of string * typ list +| TFree of string * sort +| TVar of indexname * sort +datatype term = + Const of string * typ +| Free of string * typ +| Var of indexname * typ +| Bound of int +| Abs of string * typ * term +| $ of term * term *} + +text {* + The datatype for terms uses the usual de Bruijn index mechanism---where + bound variables are represented by the constructor @{ML Bound}. + + @{ML_response_fake [display, gray] + "@{term \"\x y. x y\"}" + "Abs (\"x\", \"'a \ 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"} + + The index in @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that binds the corresponding variable. Note that the names of bound variables are kept at abstractions for printing purposes, and so should be treated only as ``comments''. Application in Isabelle is - realised with the term-constructor @{ML $}. + realised with the term-constructor @{ML $}. + + Isabelle makes a distinction between \emph{free} variables (term-constructor @{ML Free}) + and variables (term-constructor @{ML Var}). The latter correspond to the schematic + variables that show up with a question mark in front of them. Consider the following + two examples + + @{ML_response_fake [display, gray] +"let + val v1 = Var ((\"x\", 3), @{typ bool}) + val v2 = Var ((\"x1\",3), @{typ bool}) +in + writeln (Syntax.string_of_term @{context} v1); + writeln (Syntax.string_of_term @{context} v2) +end" +"?x3 +?x1.3"} + + This is different from a free variable + + @{ML_response_fake [display, gray] + "@{term \"x\"}" + "x"} + + When constructing terms, you are usually concerned with free variables (for example + you cannot construct schematic variables using the antiquotation @{text "@{term \}"}). + If you deal with theorems, you have to observe the distinction. The same holds + for types. \begin{readmore} - Terms are described in detail in \isccite{sec:terms}. Their + Terms and types are described in detail in \isccite{sec:terms}. Their definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. \end{readmore} @@ -632,8 +681,8 @@ terms can be constructed. For example @{ML_response_fake_both [display,gray] - "@{term \"(x::nat) x\"}" - "Type unification failed \"} + "@{term \"x x\"}" + "Type unification failed: Occurs check!"} raises a typing error, while it perfectly ok to construct the term @@ -689,7 +738,6 @@ \end{readmore} *} - section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} text {* @@ -865,7 +913,7 @@ @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \)"} the name of the constant @{text "Nil"} depends on the theory in which the - term constructor is defined (@{text "List"}) and also in which data type + term constructor is defined (@{text "List"}) and also in which datatype (@{text "list"}). Even worse, some constants have a name involving type-classes. Consider for example the constants for @{term "zero"} and \mbox{@{text "(op *)"}}: @@ -877,7 +925,7 @@ While you could use the complete name, for example @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or matching against @{text "Nil"}, this would make the code rather brittle. - The reason is that the theory and the name of the data type can easily change. + The reason is that the theory and the name of the datatype can easily change. To make the code more robust, it is better to use the antiquotation @{text "@{const_name \}"}. With this antiquotation you can harness the variable parts of the constant's name. Therefore a function for @@ -918,11 +966,11 @@ *} -ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *} +ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *} text {* This can be equally written with the combinator @{ML "-->"} as: *} -ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} +ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *} text {* A handy function for manipulating terms is @{ML map_types}: it takes a @@ -945,6 +993,8 @@ $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} (FIXME: a readmore about types) + + (Explain @{ML Term.add_tvarsT} and @{ML Term.add_tfreesT}) *} @@ -1663,6 +1713,9 @@ text {* @{ML PureThy.add_thms_dynamic} *} +local_setup {* + LocalTheory.note Thm.theoremK + ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *} (* FIXME: some code below *) @@ -1910,7 +1963,7 @@ "The term \"min (Suc 0)\" has type \"nat \ nat\"."} To see the proper linebreaking, you can try out the function on a bigger term - and type. + and type. For example: @{ML_response_fake [display,gray] "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}" @@ -1919,26 +1972,75 @@ *} +ML {* pprint (Pretty.big_list "header" (map (Pretty.str o string_of_int) (4 upto 10))) *} + +text {* +chunks inserts forced breaks (unlike blk where you have to do this yourself) +*} + +ML {* (Pretty.chunks [Pretty.str "a", Pretty.str "b"], + Pretty.blk (0, [Pretty.str "a", Pretty.str "b"])) *} + +ML {* +fun setmp_show_all_types f = + setmp show_all_types + (! show_types orelse ! show_sorts orelse ! show_all_types) f; + +val ctxt = @{context}; +val t1 = @{term "undefined::nat"}; +val t2 = @{term "Suc y"}; +val pty = Pretty.block (Pretty.breaks + [(setmp show_question_marks false o setmp_show_all_types) + (Syntax.pretty_term ctxt) t1, + Pretty.str "=", Syntax.pretty_term ctxt t2]); +pty |> Pretty.string_of |> priority +*} + +text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely *} + + +ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> writeln *} +ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *} + + +ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of |> writeln *} +ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *} + text {* Still to be done: - @{ML Pretty.big_list}, - - @{ML Pretty.chunks} - - equations - - colours - What happens with big formulae? \begin{readmore} The general infrastructure for pretty-printing is implemented in the file @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"} contains pretty-printing functions for terms, types, theorems and so on. + + @{ML_file "Pure/General/markup.ML"} \end{readmore} *} +text {* + printing into the goal buffer as part of the proof state +*} + + +ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> writeln *} +ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *} + +text {* writing into the goal buffer *} + +ML {* fun my_hook interactive state = + (interactive ? Proof.goal_message (fn () => Pretty.str +"foo")) state +*} + +setup {* Context.theory_map (Specification.add_theorem_hook my_hook) *} + +lemma "False" +oops + + section {* Misc (TBD) *} ML {*DatatypePackage.get_datatype @{theory} "List.list"*} diff -r 5c211dd7e5ad -r ab9e09076462 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Sat May 09 18:50:01 2009 +0200 +++ b/ProgTutorial/Package/Ind_Code.thy Sun May 17 16:22:27 2009 +0200 @@ -50,7 +50,7 @@ val arg = ((@{binding "My_True"}, NoSyn), @{term True}) val (def, lthy') = make_defn arg lthy in - writeln (str_of_thm_no_vars lthy' def); lthy' + writeln (string_of_thm_no_vars lthy' def); lthy' end *} text {* @@ -182,7 +182,7 @@ val (defs, lthy') = defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy in - writeln (str_of_thms_no_vars lthy' defs); lthy + writeln (string_of_thms_no_vars lthy' defs); lthy end *} text {* @@ -391,7 +391,7 @@ val intro = prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys) in - writeln (str_of_thm lthy intro); lthy + writeln (string_of_thm lthy intro); lthy end *} text {* @@ -450,7 +450,7 @@ let val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy in - writeln (str_of_thms lthy ind_thms); lthy + writeln (string_of_thms lthy ind_thms); lthy end *} @@ -516,7 +516,7 @@ val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] val new_thm = all_elims ctrms @{thm all_elims_test} in - writeln (str_of_thm_no_vars @{context} new_thm) + writeln (string_of_thm_no_vars @{context} new_thm) end" "P a b c"} @@ -529,7 +529,7 @@ @{thm [source] imp_elims_test}: @{ML_response_fake [display, gray] -"writeln (str_of_thm_no_vars @{context} +"writeln (string_of_thm_no_vars @{context} (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))" "C"} @@ -604,10 +604,10 @@ *} ML{*fun chop_print params1 params2 prems1 prems2 ctxt = let - val s = ["Params1 from the rule:", str_of_cterms ctxt params1] - @ ["Params2 from the predicate:", str_of_cterms ctxt params2] - @ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1) - @ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2) + val s = ["Params1 from the rule:", string_of_cterms ctxt params1] + @ ["Params2 from the predicate:", string_of_cterms ctxt params2] + @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) + @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) in s |> separate "\n" |> implode diff -r 5c211dd7e5ad -r ab9e09076462 ProgTutorial/Package/Ind_Extensions.thy --- a/ProgTutorial/Package/Ind_Extensions.thy Sat May 09 18:50:01 2009 +0200 +++ b/ProgTutorial/Package/Ind_Extensions.thy Sun May 17 16:22:27 2009 +0200 @@ -188,6 +188,12 @@ \end{readmore} *} +section {* Definitional Packages *} + +text {* Type declarations *} + +ML{*TypedefPackage.add_typedef false NONE (@{binding test},[],NoSyn) + @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *} (*<*)end(*>*) \ No newline at end of file diff -r 5c211dd7e5ad -r ab9e09076462 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Sat May 09 18:50:01 2009 +0200 +++ b/ProgTutorial/Parsing.thy Sun May 17 16:22:27 2009 +0200 @@ -1333,7 +1333,7 @@ Input text is split up into tokens, and the input source type for many parsing functions is \texttt{token list}. - The data type definition (which is not published in the signature) is + The datatype definition (which is not published in the signature) is \begin{verbatim} datatype token = Token of Position.T * (token_kind * string); \end{verbatim} @@ -1518,7 +1518,7 @@ text {* The source file is \texttt{src/Pure/Isar/args.ML}. - The primary type of this structure is the \texttt{src} data type; + The primary type of this structure is the \texttt{src} datatype; the single constructors not published in the signature, but \texttt{Args.src} and \texttt{Args.dest\_src} are in fact the constructor and destructor functions. diff -r 5c211dd7e5ad -r ab9e09076462 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Sat May 09 18:50:01 2009 +0200 +++ b/ProgTutorial/Tactical.thy Sun May 17 16:22:27 2009 +0200 @@ -212,7 +212,7 @@ ML{*fun my_print_tac ctxt thm = let - val _ = writeln (str_of_thm_no_vars ctxt thm) + val _ = writeln (string_of_thm_no_vars ctxt thm) in Seq.single thm end*} @@ -538,17 +538,17 @@ *} ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = let - val str_of_params = str_of_cterms context params - val str_of_asms = str_of_cterms context asms - val str_of_concl = str_of_cterm context concl - val str_of_prems = str_of_thms_no_vars context prems - val str_of_schms = str_of_cterms context (snd schematics) + val string_of_params = string_of_cterms context params + val string_of_asms = string_of_cterms context asms + val string_of_concl = string_of_cterm context concl + val string_of_prems = string_of_thms_no_vars context prems + val string_of_schms = string_of_cterms context (snd schematics) - val _ = (writeln ("params: " ^ str_of_params); - writeln ("schematics: " ^ str_of_schms); - writeln ("assumptions: " ^ str_of_asms); - writeln ("conclusion: " ^ str_of_concl); - writeln ("premises: " ^ str_of_prems)) + val _ = (writeln ("params: " ^ string_of_params); + writeln ("schematics: " ^ string_of_schms); + writeln ("assumptions: " ^ string_of_asms); + writeln ("conclusion: " ^ string_of_concl); + writeln ("premises: " ^ string_of_prems)) in no_tac end*} @@ -1182,9 +1182,9 @@ val {simps, congs, procs, ...} = Simplifier.dest_ss ss fun name_thm (nm, thm) = - " " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm) + " " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm) fun name_ctrm (nm, ctrm) = - " " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm) + " " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm) val s = ["Simplification rules:"] @ map name_thm simps @ ["Congruences rules:"] @ map name_thm congs @ @@ -1497,6 +1497,8 @@ (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy) + (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.) + *} section {* Simprocs *} @@ -1516,7 +1518,7 @@ ML %linenosgray{*fun fail_simproc simpset redex = let val ctxt = Simplifier.the_context simpset - val _ = writeln ("The redex: " ^ (str_of_cterm ctxt redex)) + val _ = writeln ("The redex: " ^ (string_of_cterm ctxt redex)) in NONE end*} diff -r 5c211dd7e5ad -r ab9e09076462 progtutorial.pdf Binary file progtutorial.pdf has changed