# HG changeset patch # User Christian Urban # Date 1321547629 0 # Node ID 615780a701b6de75457159a1d2e2759961be94f5 # Parent f56fc3305a08c3186f6513f25477db0b37c3c5bb tuned diff -r f56fc3305a08 -r 615780a701b6 ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Thu Nov 17 12:20:19 2011 +0000 +++ b/ProgTutorial/Advanced.thy Thu Nov 17 16:33:49 2011 +0000 @@ -165,7 +165,8 @@ val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy val trm1 = Syntax.read_term_global tmp_thy' "FOO baz" val trm2 = Syntax.read_term_global thy "FOO baz" - val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2) + val _ = pwriteln + (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)) in thy end *} @@ -192,6 +193,11 @@ inference. This is relevant in situations where definitions are made later, but parsing and type inference has to take already proceed as if the definitions were already made. + + \begin{readmore} + Most of the functions about theories are implemented in + @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}. + \end{readmore} *} section {* Contexts *} @@ -315,7 +321,7 @@ "([\"y\", \"ya\", \"z\"], ...)"} Now a fresh variant for the second occurence of @{text y} is created - avoiding any clash. In this way we can also create free variables + avoiding any clash. In this way we can also create fresh free variables that avoid any clashes with fixed variables. In Line~3 below we fix the variable @{text x} in the context @{text ctxt1}. Next we want to create two fresh variables of type @{typ nat} as variants of the @@ -459,10 +465,11 @@ end" "?P ?x ?y ?z ?x ?y ?z"} - Since we fixed all variables in @{text ctxt1}, in the result all of them - are schematic. The great point of contexts is that exporting from one to - another is not just concerned with variables, but also assumptions. For this we - can use the function @{ML_ind export in Assumption} from the structure + Since we fixed all variables in @{text ctxt1}, in the exported + result all of them are schematic. The great point of contexts is + that exporting from one to another is not just restricted to + variables, but also works with assumptions. For this we can use the + function @{ML_ind export in Assumption} from the structure @{ML_struct Assumption}. Consider the following code. @{ML_response_fake [display, gray, linenos] @@ -552,7 +559,7 @@ oops *) -section {* Local Theories (TBD) *} +section {* Local Theories and Local Setups\label{sec:local} (TBD) *} text {* In contrast to an ordinary theory, which simply consists of a type diff -r f56fc3305a08 -r 615780a701b6 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Thu Nov 17 12:20:19 2011 +0000 +++ b/ProgTutorial/Essential.thy Thu Nov 17 16:33:49 2011 +0000 @@ -115,12 +115,13 @@ end" "?x3, ?x1.3, x"} - When constructing terms, you are usually concerned with free variables (as - mentioned earlier, you cannot construct schematic variables using the - antiquotation @{text "@{term \}"}). If you deal with theorems, you have to, - however, observe the distinction. The reason is that only schematic - variables can be instantiated with terms when a theorem is applied. A - similar distinction between free and schematic variables holds for types + When constructing terms, you are usually concerned with free + variables (as mentioned earlier, you cannot construct schematic + variables using the built in antiquotation \mbox{@{text "@{term + \}"}}). If you deal with theorems, you have to, however, observe the + distinction. The reason is that only schematic variables can be + instantiated with terms when a theorem is applied. A similar + distinction between free and schematic variables holds for types (see below). \begin{readmore} @@ -1555,8 +1556,10 @@ While we obtained a theorem as result, this theorem is not yet stored in Isabelle's theorem database. Consequently, it cannot be referenced on the user level. One way to store it in the theorem database is - by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer - to the section about local-setup is given here.} + by using the function @{ML_ind note in Local_Theory} from the structure + @{ML_struct Local_Theory} (the Isabelle command + \isacommand{local\_setup} will be explained in more detail in + Section~\ref{sec:local}). *} local_setup %gray {* @@ -1598,7 +1601,7 @@ [source] my_thm_simp} is that they can now also be referenced with the \isacommand{thm}-command on the user-level of Isabelle - + \begin{isabelle} \isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline @{text ">"}~@{prop "\\x. P x \ Q x; P t\ \ Q t"}\isanewline @@ -2009,16 +2012,20 @@ using @{text "@{thm \}"} produces \begin{isabelle} + \begin{graybox} @{text "@{thm style_test}"}\\ @{text ">"}~@{thm style_test} + \end{graybox} \end{isabelle} as expected. But with the theorem style @{text "@{thm (my_strip_allq) \}"} we obtain \begin{isabelle} + \begin{graybox} @{text "@{thm (my_strip_allq) style_test}"}\\ @{text ">"}~@{thm (my_strip_allq) style_test} + \end{graybox} \end{isabelle} without the leading quantifiers. We can improve this theorem style by explicitly @@ -2051,10 +2058,11 @@ on the resulting term. We can now suggest, for example, two variables for stripping off the first two @{text \}-quantifiers. - \begin{isabelle} + \begin{graybox} @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\ @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test} + \end{graybox} \end{isabelle} Such styles allow one to print out theorems in documents formatted to diff -r f56fc3305a08 -r 615780a701b6 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Thu Nov 17 12:20:19 2011 +0000 +++ b/ProgTutorial/First_Steps.thy Thu Nov 17 16:33:49 2011 +0000 @@ -76,8 +76,8 @@ \end{isabelle} \end{quote} - However, both commands will only play minor roles in this tutorial (we will - always arrange that the ML-code is defined outside proofs). + However, both commands will only play minor roles in this tutorial (we most of + the time make sure that the ML-code is defined outside proofs). @@ -211,11 +211,14 @@ where now even @{term Pair} is written with its type (@{term Pair} is the term-constructor for products). Other configuration values that influence - printing of terms include @{ML_ind show_brackets in Syntax}, @{ML_ind - show_sorts in Syntax} and @{ML_ind eta_contract in Syntax}. -*} + printing of terms include -text {* + \begin{itemize} + \item @{ML_ind show_brackets in Syntax} + \item @{ML_ind show_sorts in Syntax} + \item @{ML_ind eta_contract in Syntax} + \end{itemize} + A @{ML_type cterm} can be printed with the following function. *} @@ -689,8 +692,8 @@ pwriteln (pretty_term ctxt' one_trm); pwriteln (pretty_thm ctxt' one_thm) end" - "one -one \ 1"} + "One +One \ 1"} Recall that @{ML "|>"} is the reverse function application. Recall also that the related reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} @@ -701,8 +704,8 @@ *} ML{*val double = - (fn x => (x, x)) - #-> (fn x => fn y => x + y)*} + (fn x => (x, x)) #-> + (fn x => fn y => x + y)*} text {* diff -r f56fc3305a08 -r 615780a701b6 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Thu Nov 17 12:20:19 2011 +0000 +++ b/ProgTutorial/Intro.thy Thu Nov 17 16:33:49 2011 +0000 @@ -223,7 +223,7 @@ this. Still to keep them to a minimum, you can submit your changes first to a rather sophisticated \emph{testboard}, which will perform checks of your changes against the Isabelle repository and against the AFP. The advantage of the testboard is - that the testing is performed by rather powerful machines, saving you lengthy + that the testing is performed by rather powerful machines saving you lengthy tests on, for example, your own laptop. You can see the results of the testboard at @@ -241,7 +241,7 @@ where the dots need to be replaced by your login name. Note that for pushing changes to the testboard you need to add the option @{text "-f"}, - which however should \emph{never} be used with the main Isabelle + which should \emph{never} be used with the main Isabelle repository. While the testboard is a great system for supporting Isabelle developers, its disadvantage is that it needs login permissions for the computers in Munich. So in order to use it, you might have to ask other diff -r f56fc3305a08 -r 615780a701b6 progtutorial.pdf Binary file progtutorial.pdf has changed