# HG changeset patch # User Christian Urban # Date 1249195481 -7200 # Node ID d0b81d6e1b2864590e3853f9b4713705efd6bc95 # Parent 8057d65607eba4b2f21325bb8f8ed3181506b9d3 updated to Isabelle changes and merged sections in the FirstSteps chapter diff -r 8057d65607eb -r d0b81d6e1b28 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sat Aug 01 08:59:41 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Sun Aug 02 08:44:41 2009 +0200 @@ -852,7 +852,7 @@ \end{readmore} *} -section {* Constructing Terms Manually\label{sec:terms_types_manually} *} +section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} text {* While antiquotations are very convenient for constructing terms, they can @@ -904,18 +904,23 @@ @{ML_response_fake [display,gray] "let - val t = @{term \"P::nat\"} + val trm = @{term \"P::nat\"} val args = [@{term \"True\"}, @{term \"False\"}] in - list_comb (t, args) + list_comb (trm, args) end" "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"} Another handy function is @{ML [index] lambda}, which abstracts a variable in a term. For example - + @{ML_response_fake [display,gray] - "lambda @{term \"x::nat\"} @{term \"(P::nat \ bool) x\"}" +"let + val x_nat = @{term \"x::nat\"} + val trm = @{term \"(P::nat \ bool) x\"} +in + lambda x_nat trm +end" "Abs (\"x\", \"nat\", Free (\"P\", \"bool \ bool\") $ Bound 0)"} In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), @@ -926,10 +931,15 @@ as in @{ML_response_fake [display,gray] - "lambda @{term \"x::nat\"} @{term \"(P::bool \ bool) x\"}" - "Abs (\"x\", \"nat\", Free (\"P\", \"bool \ bool\") $ Free (\"x\", \"bool\"))"} - - then the variable @{text "Free (\"x\", \"bool\")"} is \emph{not} abstracted. +"let + val x_int = @{term \"x::int\"} + val trm = @{term \"(P::nat \ bool) x\"} +in + lambda x_int trm +end" + "Abs (\"x\", \"int\", Free (\"P\", \"nat \ bool\") $ Free (\"x\", \"nat\"))"} + + then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. This is a fundamental principle of Church-style typing, where variables with the same name still differ, if they have different type. @@ -943,7 +953,7 @@ "let val s1 = (@{term \"(f::nat \ nat \ nat) 0\"}, @{term \"y::nat \ nat\"}) val s2 = (@{term \"x::nat\"}, @{term \"True\"}) - val trm = @{term \"((f::nat \ nat \ nat) 0) x\"} + val trm = @{term \"((f::nat \ nat \ nat) 0) x\"} in subst_free [s1, s2] trm end" @@ -967,8 +977,11 @@ arguments. For example @{ML_response_fake [gray,display] - "writeln (Syntax.string_of_term @{context} - (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))" +"let + val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"}) +in + writeln (Syntax.string_of_term @{context} eq) +end" "True = False"} *} @@ -977,14 +990,11 @@ Most of the HOL-specific operations on terms and types are defined in @{ML_file "HOL/Tools/hologic.ML"}. \end{readmore} -*} - -section {* Constants *} - -text {* - There are a few subtle issues with constants. They usually crop up when - pattern matching terms or types, or when constructing them. While it is perfectly ok - to write the function @{text is_true} as follows + + When constructing terms manually, there are a few subtle issues with + constants. They usually crop up when pattern matching terms or types, or + when constructing them. While it is perfectly ok to write the function + @{text is_true} as follows *} ML{*fun is_true @{term True} = true @@ -1108,11 +1118,7 @@ Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; functions about signatures in @{ML_file "Pure/sign.ML"}. \end{readmore} -*} - -section {* Constructing Types Manually *} - -text {* + Although types of terms can often be inferred, there are many situations where you need to construct types manually, especially when defining constants. For example the function returning a function @@ -1166,12 +1172,12 @@ call them as follows @{ML_response [gray,display] - "Term.add_tfrees @{term \"(a,b)\"} []" + "Term.add_tfrees @{term \"(a, b)\"} []" "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"} The reason for this definition is that @{ML add_tfrees in Term} can be easily folded over a list of terms. Similarly for all functions - named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}. + named @{text "add_*"} in @{ML_file "Pure/term.ML"}. *} @@ -2252,4 +2258,6 @@ ML {*Datatype.get_info @{theory} "List.list"*} +section {* Name Space(TBD) *} + end diff -r 8057d65607eb -r d0b81d6e1b28 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Sat Aug 01 08:59:41 2009 +0200 +++ b/ProgTutorial/Package/Ind_Code.thy Sun Aug 02 08:44:41 2009 +0200 @@ -598,7 +598,8 @@ The problem with @{ML SUBPROOF}, however, is that it always expects us to completely discharge the goal (see Section~\ref{sec:simpletacs}). This is a bit inconvenient for our gradual explanation of the proof here. Therefore - we use first the function @{ML [index] FOCUS}, which does same as @{ML SUBPROOF} + we use first the function @{ML [index] FOCUS in Subgoal}, which does s + ame as @{ML SUBPROOF} but does not require us to completely discharge the goal. *} (*<*)oops(*>*) @@ -630,13 +631,13 @@ First we calculate the values for @{text "params1/2"} and @{text "prems1/2"} from @{text "params"} and @{text "prems"}, respectively. To better see what is going in our example, we will print out these values using the printing - function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS} will + function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS in Subgoal} will supply us the @{text "params"} and @{text "prems"} as lists, we can separate them using the function @{ML [index] chop}. *} ML %linenosgray{*fun chop_test_tac preds rules = - FOCUS (fn {params, prems, context, ...} => + Subgoal.FOCUS (fn {params, prems, context, ...} => let val cparams = map snd params val (params1, params2) = chop (length cparams - length preds) cparams @@ -704,7 +705,7 @@ *} ML %linenosgray{*fun apply_prem_tac i preds rules = - FOCUS (fn {params, prems, context, ...} => + Subgoal.FOCUS (fn {params, prems, context, ...} => let val cparams = map snd params val (params1, params2) = chop (length cparams - length preds) cparams @@ -788,7 +789,7 @@ end) *} text {* - Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS} anymore. + Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. The full proof of the introduction rule is as follows: *} diff -r 8057d65607eb -r d0b81d6e1b28 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Sat Aug 01 08:59:41 2009 +0200 +++ b/ProgTutorial/Parsing.thy Sun Aug 02 08:44:41 2009 +0200 @@ -625,7 +625,7 @@ text {* There is usually no need to write your own parser for parsing inner syntax, that is for terms and types: you can just call the predefined parsers. Terms can - be parsed using the function @{ML OuterParse.term}. For example: + be parsed using the function @{ML [index] term in OuterParse}. For example: @{ML_response [display,gray] "let @@ -635,10 +635,10 @@ end" "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"} - The function @{ML OuterParse.prop} is similar, except that it gives a different + The function @{ML [index] prop in OuterParse} is similar, except that it gives a different error message, when parsing fails. As you can see, the parser not just returns the parsed string, but also some encoded information. You can decode the - information with the function @{ML YXML.parse}. For example + information with the function @{ML [index] parse in YXML}. For example @{ML_response [display,gray] "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" diff -r 8057d65607eb -r d0b81d6e1b28 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Sat Aug 01 08:59:41 2009 +0200 +++ b/ProgTutorial/Tactical.thy Sun Aug 02 08:44:41 2009 +0200 @@ -525,8 +525,8 @@ Often proofs on the ML-level involve elaborate operations on assumptions and @{text "\"}-quantified variables. To do such operations using the basic tactics shown so far is very unwieldy and brittle. Some convenience and - safety is provided by the functions @{ML [index] FOCUS} and @{ML [index] SUBPROOF}. - These tactics fix the parameters + safety is provided by the functions @{ML [index] FOCUS in Subgoal} and + @{ML [index] SUBPROOF}. These tactics fix the parameters and bind the various components of a goal state to a record. To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which takes a record and just prints out the content of this record (using the @@ -547,7 +547,7 @@ 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 string_of_schms = string_of_cterms context (map fst (snd schematics)) val _ = (writeln ("params: " ^ string_of_params); writeln ("schematics: " ^ string_of_schms); @@ -557,17 +557,19 @@ in all_tac end*} + text_raw{* \end{isabelle} \end{minipage} \caption{A function that prints out the various parameters provided by - @{ML FOCUS} and @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for - extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}} + @{ML FOCUS in Subgoal} and @{ML SUBPROOF}. It uses the functions defined + in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s + and @{ML_type thm}s.\label{fig:sptac}} \end{figure} *} lemma shows "\x y. A x y \ B y x \ C (?z y) x" -apply(tactic {* FOCUS foc_tac @{context} 1 *}) +apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *}) txt {* The tactic produces the following printout: @@ -582,6 +584,8 @@ \end{tabular} \end{quote} + (FIXME: find out how nowadays the schmetics are handled) + Notice in the actual output the brown colour of the variables @{term x} and @{term y}. Although they are parameters in the original goal, they are fixed inside the subproof. By convention these fixed variables are printed in brown colour. @@ -593,7 +597,7 @@ *} apply(rule impI) -apply(tactic {* FOCUS foc_tac @{context} 1 *}) +apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *}) txt {* then the tactic prints out: @@ -613,9 +617,9 @@ text {* Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}. - The difference between @{ML SUBPROOF} and @{ML FOCUS} is that the former + The difference between @{ML SUBPROOF} and @{ML FOCUS in Subgoal} is that the former expects that the goal is solved completely, which the latter does not. One - convenience of both @{ML FOCUS} and @{ML SUBPROOF} is that we can apply the + convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we can apply the assumptions using the usual tactics, because the parameter @{text prems} contains them as theorems. With this you can easily implement a tactic that behaves almost like @{ML atac}: @@ -657,13 +661,14 @@ text {* \begin{readmore} - The functions @{ML FOCUS} and @{ML SUBPROOF} are defined in + The functions @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in @{ML_file "Pure/subgoal.ML"} and also described in \isccite{sec:results}. \end{readmore} - Similar but less powerful functions than @{ML FOCUS} are @{ML [index] SUBGOAL} - and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former + Similar but less powerful functions than @{ML FOCUS in Subgoal} are + @{ML [index] SUBGOAL} and @{ML [index] CSUBGOAL}. They allow you to + inspect a given subgoal (the former presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type cterm}). With this you can implement a tactic that applies a rule according to the topmost logic connective in the subgoal (to illustrate this we only @@ -1053,12 +1058,11 @@ will solve all trivial subgoals involving @{term True} or @{term "False"}. (FIXME: say something about @{ML [index] COND} and COND') - - (FIXME: say something about @{ML [index] FOCUS}) \begin{readmore} Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}. Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}. + The function @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in @{ML_file "Pure/subgoal.ML"} \end{readmore} *} diff -r 8057d65607eb -r d0b81d6e1b28 progtutorial.pdf Binary file progtutorial.pdf has changed