# HG changeset patch # User Christian Urban # Date 1257552217 -3600 # Node ID 92f7328dc5ccf5df9ab5917350f4e11470e207e2 # Parent 304426a9aecf057ab755d6f30e6b4c29ac7e1264 added type work and updated to Isabelle and poly 5.3 diff -r 304426a9aecf -r 92f7328dc5cc ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Thu Nov 05 10:30:59 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Sat Nov 07 01:03:37 2009 +0100 @@ -91,6 +91,9 @@ However, both commands will only play minor roles in this tutorial (we will always arrange that the ML-code is defined outside proofs). + + + Once a portion of code is relatively stable, you usually want to export it to a separate ML-file. Such files can then be included somewhere inside a theory by using the command \isacommand{use}. For example @@ -542,8 +545,27 @@ text {* which is the function composed of first the increment-by-one function and then increment-by-two, followed by increment-by-three. Again, the reverse function - composition allows you to read the code top-down. + composition allows you to read the code top-down. This combinator is often used + for setup function inside the \isacommand{setup}-command. These function have to be + of type @{ML_type "theory -> theory"} in order to install, for example, some new + data inside the current theory. More than one such setup function can be composed + with @{ML "#>"}. For example +*} +setup %gray {* let + val (ival1, setup_ival1) = Attrib.config_int "ival1" 1 + val (ival2, setup_ival2) = Attrib.config_int "ival2" 2 +in + setup_ival1 #> + setup_ival2 +end *} + +text {* + after this the configuration values @{text ival1} and @{text ival2} are known + in the current theory and can be manipulated by the user (for more information + about configuration values see Section~\ref{sec:storing}, for more about setup + functions see Section~\ref{sec:theories}). + The remaining combinators we describe in this section add convenience for the ``waterfall method'' of writing functions. The combinator @{ML_ind tap in Basics} allows you to get hold of an intermediate result (to do some @@ -814,6 +836,21 @@ under this name (this becomes especially important when you deal with theorem lists; see Section \ref{sec:storing}). + It is also possible to prove lemmas with the antiquotation @{text "@{lemma \ by \}"} + whose first argument is a statement (possibly many of them separated by @{text "and"}, + and the second is a proof. For example +*} + +ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *} + +text {* + which can be printed out as follows + + @{ML_response_fake [gray,display] +"foo_thm |> string_of_thms @{context} + |> tracing" + "True, True"} + You can also refer to the current simpset via an antiquotation. To illustrate this we implement the function that extracts the theorem names stored in a simpset. diff -r 304426a9aecf -r 92f7328dc5cc ProgTutorial/General.thy --- a/ProgTutorial/General.thy Thu Nov 05 10:30:59 2009 +0100 +++ b/ProgTutorial/General.thy Sat Nov 07 01:03:37 2009 +0100 @@ -174,15 +174,87 @@ text {* Like with terms, there is the distinction between free type variables (term-constructor @{ML "TFree"}) and schematic - type variables (term-constructor @{ML "TVar"}). A type constant, + type variables (term-constructor @{ML "TVar"} and printed with + a leading question mark). A type constant, like @{typ "int"} or @{typ bool}, are types with an empty list - of argument types. However, it is a bit difficult to show an - example, because Isabelle always pretty-prints types (unlike terms). - Here is a contrived example: + of argument types. However, it needs a bit of effort to show an + example, because Isabelle always pretty prints types (unlike terms). + Using just the antiquotation @{text "@{typ \"bool\"}"} we only see @{ML_response [display, gray] - "if Type (\"bool\", []) = @{typ \"bool\"} then true else false" - "true"} + "@{typ \"bool\"}" + "bool"} + + the pretty printed version of @{text "bool"}. However, in PolyML it is + easy to install your own pretty printer. With the function below we + mimic the behaviour of the usual pretty printer for + datatypes.\footnote{Thanks to David Matthews for providing this + code.} +*} + +ML{*fun typ_raw_pretty_printer depth _ ty = +let + fun cond str a = + if depth <= 0 + then PolyML.PrettyString "..." + else PolyML.PrettyBlock(1, false, [], + [PolyML.PrettyString str, PolyML.PrettyBreak(1, 0), a]) +in + case ty of + Type a => cond "Type" (PolyML.prettyRepresentation(a, depth - 1)) + | TFree a => cond "TFree" (PolyML.prettyRepresentation(a, depth - 1)) + | TVar a => cond "TVar" (PolyML.prettyRepresentation(a, depth - 1)) +end*} + +text {* + We can install this pretty printer with the function + @{ML_ind addPrettyPrinter in PolyML} as follows. +*} + +ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*} + +text {* + Now the type bool is printed out as expected. + + @{ML_response [display,gray] + "@{typ \"bool\"}" + "Type (\"bool\", [])"} + + When printing out a list-type + + @{ML_response [display,gray] + "@{typ \"'a list\"}" + "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"} + + we can see the full name of the type is actually @{text "List.list"}, indicating + that it is defined in the theory @{text "List"}. However, one has to be + careful with finding out the right name of a type, because even if + @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the + theories @{text "HOL"} and @{text "Nat"}, respectively, they are + still represented by their simple name. + + @{ML_response [display,gray] + "@{typ \"bool \ nat\"}" + "Type (\"fun\", [Type (\"bool\", []), Type (\"nat\", [])])"} + + We can restore the usual behaviour of Isabelle's pretty printer + with the code +*} + +ML{*fun stnd_pretty_printer _ _ = + ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy; + +PolyML.addPrettyPrinter stnd_pretty_printer*} + +text {* + After that the types for booleans, lists and so on are printed out again + the standard Isabelle way. + + @{ML_response_fake [display, gray] + "@{typ \"bool\"}; +@{typ \"'a list\"}" + "\"bool\" +\"'a List.list\""} \begin{readmore} Types are described in detail in \isccite{sec:types}. Their @@ -1119,14 +1191,14 @@ consisting of a name and a kind. When we store lemmas in the theorem database, we might want to explicitly extend this data by attaching case names to the - two premises of the lemma. This can be done with the function @{ML_ind name in RuleCases} - from the structure @{ML_struct RuleCases}. + two premises of the lemma. This can be done with the function @{ML_ind name in Rule_Cases} + from the structure @{ML_struct Rule_Cases}. *} local_setup %gray {* LocalTheory.note Thm.lemmaK ((@{binding "foo_data'"}, []), - [(RuleCases.name ["foo_case_one", "foo_case_two"] + [(Rule_Cases.name ["foo_case_one", "foo_case_two"] @{thm foo_data})]) #> snd *} text {* diff -r 304426a9aecf -r 92f7328dc5cc ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Thu Nov 05 10:30:59 2009 +0100 +++ b/ProgTutorial/Package/Ind_Code.thy Sat Nov 07 01:03:37 2009 +0100 @@ -1005,8 +1005,8 @@ ||>> note_many mut_name ((@{binding "inducts"}, []), ind_prins) ||>> fold_map (note_single1 mut_name) (namesattrs ~~ intro_rules) ||>> fold_map (note_single2 @{binding "induct"} - [Attrib.internal (K (RuleCases.case_names case_names)), - Attrib.internal (K (RuleCases.consumes 1)), + [Attrib.internal (K (Rule_Cases.case_names case_names)), + Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Induct.induct_pred ""))]) (prednames ~~ ind_prins) |> snd @@ -1043,9 +1043,9 @@ Line 20 add further every introduction rule under its own name (given by the user).\footnote{FIXME: what happens if the user did not give any name.} Line 21 registers the induction principles. For this we have - to use some specific attributes. The first @{ML_ind case_names in RuleCases} + to use some specific attributes. The first @{ML_ind case_names in Rule_Cases} corresponds to the case names that are used by Isar to reference the proof - obligations in the induction. The second @{ML "consumes 1" in RuleCases} + obligations in the induction. The second @{ML "consumes 1" in Rule_Cases} indicates that the first premise of the induction principle (namely the predicate over which the induction proceeds) is eliminated. diff -r 304426a9aecf -r 92f7328dc5cc ProgTutorial/Package/simple_inductive_package.ML --- a/ProgTutorial/Package/simple_inductive_package.ML Thu Nov 05 10:30:59 2009 +0100 +++ b/ProgTutorial/Package/simple_inductive_package.ML Sat Nov 07 01:03:37 2009 +0100 @@ -187,8 +187,8 @@ |>> snd ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), - [Attrib.internal (K (RuleCases.case_names case_names)), - Attrib.internal (K (RuleCases.consumes 1)), + [Attrib.internal (K (Rule_Cases.case_names case_names)), + Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) (preds ~~ inducts)) #>> maps snd) |> snd diff -r 304426a9aecf -r 92f7328dc5cc progtutorial.pdf Binary file progtutorial.pdf has changed