diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Tue May 14 16:59:53 2019 +0200 +++ b/ProgTutorial/Essential.thy Tue May 14 17:10:47 2019 +0200 @@ -2,9 +2,9 @@ imports Base First_Steps begin -chapter {* Isabelle Essentials *} - -text {* +chapter \Isabelle Essentials\ + +text \ \begin{flushright} {\em One man's obfuscation is another man's abstraction.} \\[1ex] Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ @@ -17,15 +17,15 @@ is a small trusted core and everything else is built on top of this trusted core. The fundamental data structures involved in this core are certified terms and certified types, as well as theorems. -*} - - -section {* Terms and Types *} - -text {* +\ + + +section \Terms and Types\ + +text \ In Isabelle, there are certified terms and uncertified terms (respectively types). Uncertified terms are often just called terms. One way to construct them is by - using the antiquotation \mbox{@{text "@{term \}"}}. For example + using the antiquotation \mbox{\@{term \}\}. For example @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" @@ -35,17 +35,17 @@ constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using the internal representation corresponding to the datatype @{ML_type_ind "term"}, which is defined as follows: -*} - -ML_val %linenosgray{*datatype term = +\ + +ML_val %linenosgray\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 {* +| $ of term * term\ + +text \ This datatype implements Church-style lambda-terms, where types are explicitly recorded in variables, constants and abstractions. The important point of having terms is that you can pattern-match against them; @@ -127,8 +127,8 @@ 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 + variables using the built-in antiquotation \mbox{\@{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 @@ -177,13 +177,13 @@ may omit parts of it by default. If you want to see all of it, you need to set the printing depth to a higher value by \end{exercise} -*} +\ declare [[ML_print_depth = 50]] -text {* - The antiquotation @{text "@{prop \}"} constructs terms by inserting the - usually invisible @{text "Trueprop"}-coercions whenever necessary. +text \ + The antiquotation \@{prop \}\ constructs terms by inserting the + usually invisible \Trueprop\-coercions whenever necessary. Consider for example the pairs @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" @@ -197,24 +197,24 @@ Const (\"Pure.imp\", \) $ \ $ \)"} where it is not (since it is already constructed by a meta-implication). - The purpose of the @{text "Trueprop"}-coercion is to embed formulae of + The purpose of the \Trueprop\-coercion is to embed formulae of an object logic, for example HOL, into the meta-logic of Isabelle. The coercion is needed whenever a term is constructed that will be proved as a theorem. As already seen above, types can be constructed using the antiquotation - @{text "@{typ \}"}. For example: + \@{typ \}\. For example: @{ML_response_fake [display,gray] "@{typ \"bool \ nat\"}" "bool \ nat"} The corresponding datatype is -*} +\ -ML_val %grayML{*datatype typ = +ML_val %grayML\datatype typ = Type of string * typ list | TFree of string * sort -| TVar of indexname * sort *} - -text {* +| TVar of indexname * sort\ + +text \ Like with terms, there is the distinction between free type variables (term-constructor @{ML "TFree"}) and schematic type variables (term-constructor @{ML "TVar"} and printed with @@ -222,19 +222,19 @@ like @{typ "int"} or @{typ bool}, are types with an empty list 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 + Using just the antiquotation \@{typ "bool"}\ we only see @{ML_response [display, gray] "@{typ \"bool\"}" "bool"} - which is the pretty printed version of @{text "bool"}. However, in PolyML - (version @{text "\"}5.3) it is easy to install your own pretty printer. With the + which is the pretty printed version of \bool\. However, in PolyML + (version \\\5.3) it is easy to install your own pretty printer. With the function below we mimic the behaviour of the usual pretty printer for datatypes (it uses pretty-printing functions which will be explained in more detail in Section~\ref{sec:pretty}). -*} - -ML %grayML{*local +\ + +ML %grayML\local fun pp_pair (x, y) = Pretty.list "(" ")" [x, y] fun pp_list xs = Pretty.list "[" "]" xs fun pp_str s = Pretty.str s @@ -249,18 +249,18 @@ pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S)) | raw_pp_typ (Type (a, tys)) = pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys))) -end*} - -text {* +end\ + +text \ We can install this pretty printer with the function @{ML_ind ML_system_pp} as follows. -*} - -ML %grayML{*ML_system_pp - (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)*} +\ + +ML %grayML\ML_system_pp + (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)\ ML \@{typ "bool"}\ -text {* +text \ Now the type bool is printed out in full detail. @{ML_response [display,gray] @@ -273,10 +273,10 @@ "@{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 + we can see the full name of the type is actually \List.list\, indicating + that it is defined in the theory \List\. However, one has to be careful with names of types, because even if - @{text "fun"} is defined in the theory @{text "HOL"}, it is + \fun\ is defined in the theory \HOL\, it is still represented by its simple name. @{ML_response [display,gray] @@ -285,12 +285,12 @@ We can restore the usual behaviour of Isabelle's pretty printer with the code -*} - -ML %grayML{*ML_system_pp - (fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)*} - -text {* +\ + +ML %grayML\ML_system_pp + (fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)\ + +text \ After that the types for booleans, lists and so on are printed out again the standard Isabelle way. @@ -305,36 +305,36 @@ definition and many useful operations are implemented in @{ML_file "Pure/type.ML"}. \end{readmore} -*} - -section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} - -text {* +\ + +section \Constructing Terms and Types Manually\label{sec:terms_types_manually}\ + +text \ While antiquotations are very convenient for constructing terms, they can only construct fixed terms (remember they are ``linked'' at compile-time). However, you often need to construct terms manually. For example, a - function that returns the implication @{text "\(x::nat). P x \ Q x"} taking + function that returns the implication \\(x::nat). P x \ Q x\ taking @{term P} and @{term Q} as arguments can only be written as: -*} - -ML %grayML{*fun make_imp P Q = +\ + +ML %grayML\fun make_imp P Q = let val x = Free ("x", @{typ nat}) in Logic.all x (Logic.mk_implies (P $ x, Q $ x)) -end *} - -text {* +end\ + +text \ The reason is that you cannot pass the arguments @{term P} and @{term Q} into an antiquotation.\footnote{At least not at the moment.} For example the following does \emph{not} work. -*} - -ML %grayML{*fun make_wrong_imp P Q = @{prop "\(x::nat). P x \ Q x"} *} - -text {* - To see this, apply @{text "@{term S}"} and @{text "@{term T}"} +\ + +ML %grayML\fun make_wrong_imp P Q = @{prop "\(x::nat). P x \ Q x"}\ + +text \ + To see this, apply \@{term S}\ and \@{term T}\ to both functions. With @{ML make_imp} you obtain the intended term involving the given arguments @@ -344,7 +344,7 @@ Const \ $ (Free (\"S\",\) $ \) $ (Free (\"T\",\) $ \))"} whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} - and @{text "Q"} from the antiquotation. + and \Q\ from the antiquotation. @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" "Const \ $ @@ -383,7 +383,7 @@ In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML "Bound 0"}), and an abstraction, where it also records the type of the abstracted variable and for printing purposes also its name. Note that because of the - typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"} + typing annotation on \P\, the variable \x\ in \P x\ is of the same type as the abstracted variable. If it is of different type, as in @@ -396,7 +396,7 @@ end" "Abs (\"x\", \"int\", Free (\"P\", \"nat \ bool\") $ Free (\"x\", \"nat\"))"} - then the variable @{text "Free (\"x\", \"nat\")"} is \emph{not} abstracted. + then the variable \Free ("x", "nat")\ 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. @@ -431,18 +431,18 @@ Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound variables with terms. To see how this function works, let us implement a function that strips off the outermost forall quantifiers in a term. -*} - -ML %grayML{*fun strip_alls t = +\ + +ML %grayML\fun strip_alls t = let fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T)) in case t of Const (@{const_name All}, _) $ Abs body => aux body | _ => ([], t) -end*} - -text {* +end\ + +text \ The function returns a pair consisting of the stripped off variables and the body of the universal quantification. For example @@ -454,14 +454,14 @@ Note that we produced in the body two dangling de Bruijn indices. Later on we will also use the inverse function that builds the quantification from a body and a list of (free) variables. -*} +\ -ML %grayML{*fun build_alls ([], t) = t +ML %grayML\fun build_alls ([], t) = t | build_alls (Free (x, T) :: vs, t) = Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) - $ Abs (x, T, build_alls (vs, t))*} - -text {* + $ Abs (x, T, build_alls (vs, t))\ + +text \ As said above, after calling @{ML strip_alls}, you obtain a term with loose bound variables. With the function @{ML subst_bounds}, you can replace these loose @{ML_ind Bound in Term}s with the stripped off variables. @@ -552,35 +552,35 @@ 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 %grayML{*fun is_true @{term True} = true - | is_true _ = false*} - -text {* - this does not work for picking out @{text "\"}-quantified terms. Because + \is_true\ as follows +\ + +ML %grayML\fun is_true @{term True} = true + | is_true _ = false\ + +text \ + this does not work for picking out \\\-quantified terms. Because the function -*} - -ML %grayML{*fun is_all (@{term All} $ _) = true - | is_all _ = false*} - -text {* +\ + +ML %grayML\fun is_all (@{term All} $ _) = true + | is_all _ = false\ + +text \ will not correctly match the formula @{prop[source] "\x::nat. P x"}: @{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "false"} - The problem is that the @{text "@term"}-antiquotation in the pattern + The problem is that the \@term\-antiquotation in the pattern fixes the type of the constant @{term "All"} to be @{typ "('a \ bool) \ bool"} for an arbitrary, but fixed type @{typ "'a"}. A properly working alternative for this function is -*} - -ML %grayML{*fun is_all (Const ("HOL.All", _) $ _) = true - | is_all _ = false*} - -text {* +\ + +ML %grayML\fun is_all (Const ("HOL.All", _) $ _) = true + | is_all _ = false\ + +text \ because now @{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "true"} @@ -589,13 +589,13 @@ second any term). However there is still a problem: consider the similar function that - attempts to pick out @{text "Nil"}-terms: -*} - -ML %grayML{*fun is_nil (Const ("Nil", _)) = true - | is_nil _ = false *} - -text {* + attempts to pick out \Nil\-terms: +\ + +ML %grayML\fun is_nil (Const ("Nil", _)) = true + | is_nil _ = false\ + +text \ Unfortunately, also this function does \emph{not} work as expected, since @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"} @@ -607,9 +607,9 @@ @{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 datatype - (@{text "list"}). Even worse, some constants have a name involving + the name of the constant \Nil\ depends on the theory in which the + term constructor is defined (\List\) and also in which datatype + (\list\). Even worse, some constants have a name involving type-classes. Consider for example the constants for @{term "zero"} and \mbox{@{term "times"}}: @@ -619,21 +619,21 @@ 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. + matching against \Nil\, this would make the code rather brittle. 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 + \@{const_name \}\. With this antiquotation you can harness the variable parts of the constant's name. Therefore a function for matching against constants that have a polymorphic type should be written as follows. -*} - -ML %grayML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true +\ + +ML %grayML\fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true - | is_nil_or_all _ = false *} - -text {* - The antiquotation for properly referencing type constants is @{text "@{type_name \}"}. + | is_nil_or_all _ = false\ + +text \ + The antiquotation for properly referencing type constants is \@{type_name \}\. For example @{ML_response [display,gray] @@ -644,34 +644,34 @@ when defining constants. For example the function returning a function type is as follows: -*} - -ML %grayML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *} - -text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *} - -ML %grayML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *} - -text {* +\ + +ML %grayML\fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2])\ + +text \This can be equally written with the combinator @{ML_ind "-->" in Term} as:\ + +ML %grayML\fun make_fun_type ty1 ty2 = ty1 --> ty2\ + +text \ If you want to construct a function type with more than one argument type, then you can use @{ML_ind "--->" in Term}. -*} - -ML %grayML{*fun make_fun_types tys ty = tys ---> ty *} - -text {* +\ + +ML %grayML\fun make_fun_types tys ty = tys ---> ty\ + +text \ A handy function for manipulating terms is @{ML_ind map_types in Term}: it takes a function and applies it to every type in a term. You can, for example, change every @{typ nat} in a term into an @{typ int} using the function: -*} - -ML %grayML{*fun nat_to_int ty = +\ + +ML %grayML\fun nat_to_int ty = (case ty of @{typ nat} => @{typ int} | Type (s, tys) => Type (s, map nat_to_int tys) - | _ => ty)*} - -text {* + | _ => ty)\ + +text \ Here is an example: @{ML_response_fake [display,gray] @@ -697,13 +697,13 @@ 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_*"} in @{ML_file "Pure/term.ML"}. + named \add_*\ in @{ML_file "Pure/term.ML"}. \begin{exercise}\label{fun:revsum} - Write a function @{text "rev_sum : term -> term"} that takes a - term of the form @{text "t\<^sub>1 + t\<^sub>2 + \ + t\<^sub>n"} (whereby @{text "n"} might be one) - and returns the reversed sum @{text "t\<^sub>n + \ + t\<^sub>2 + t\<^sub>1"}. Assume - the @{text "t\<^sub>i"} can be arbitrary expressions and also note that @{text "+"} + Write a function \rev_sum : term -> term\ that takes a + term of the form \t\<^sub>1 + t\<^sub>2 + \ + t\<^sub>n\ (whereby \n\ might be one) + and returns the reversed sum \t\<^sub>n + \ + t\<^sub>2 + t\<^sub>1\. Assume + the \t\<^sub>i\ can be arbitrary expressions and also note that \+\ associates to the left. Try your function on some examples. \end{exercise} @@ -722,8 +722,8 @@ \end{exercise} \begin{exercise}\label{fun:makelist} - Write a function that takes an integer @{text i} and - produces an Isabelle integer list from @{text 1} upto @{text i}, + Write a function that takes an integer \i\ and + produces an Isabelle integer list from \1\ upto \i\, and then builds the reverse of this list using @{const rev}. The relevant helper functions are @{ML upto}, @{ML HOLogic.mk_number} and @{ML HOLogic.mk_list}. @@ -756,11 +756,11 @@ for constructing the terms for the logical connectives.\footnote{Thanks to Roy Dyckhoff for suggesting this exercise and working out the details.} \end{exercise} -*} - -section {* Unification and Matching\label{sec:univ} *} - -text {* +\ + +section \Unification and Matching\label{sec:univ}\ + +text \ As seen earlier, Isabelle's terms and types may contain schematic term variables (term-constructor @{ML Var}) and schematic type variables (term-constructor @{ML TVar}). These variables stand for unknown entities, which can be made @@ -769,7 +769,7 @@ relatively straightforward, in case of terms the algorithms are substantially more complicated, because terms need higher-order versions of the unification and matching algorithms. Below we shall use the - antiquotations @{text "@{typ_pat \}"} and @{text "@{term_pat \}"} from + antiquotations \@{typ_pat \}\ and \@{term_pat \}\ from Section~\ref{sec:antiquote} in order to construct examples involving schematic variables. @@ -777,24 +777,24 @@ types. Both return type environments (ML-type @{ML_type "Type.tyenv"}) which map schematic type variables to types and sorts. Below we use the function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign} - for unifying the types @{text "?'a * ?'b"} and @{text "?'b list * - nat"}. This will produce the mapping, or type environment, @{text "[?'a := - ?'b list, ?'b := nat]"}. -*} - -ML %linenosgray{*val (tyenv_unif, _) = let + for unifying the types \?'a * ?'b\ and \?'b list * + nat\. This will produce the mapping, or type environment, \[?'a := + ?'b list, ?'b := nat]\. +\ + +ML %linenosgray\val (tyenv_unif, _) = let val ty1 = @{typ_pat "?'a * ?'b"} val ty2 = @{typ_pat "?'b list * nat"} in Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) -end*} - -text {* +end\ + +text \ The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type environment, which is needed for starting the unification without any - (pre)instantiations. The @{text 0} is an integer index that will be explained + (pre)instantiations. The \0\ is an integer index that will be explained below. In case of failure, @{ML typ_unify in Sign} will raise the exception - @{text TUNIFY}. We can print out the resulting type environment bound to + \TUNIFY\. We can print out the resulting type environment bound to @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the structure @{ML_struct Vartab}. @@ -802,13 +802,13 @@ "Vartab.dest tyenv_unif" "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"} -*} - -text_raw {* +\ + +text_raw \ \begin{figure}[t] \begin{minipage}{\textwidth} - \begin{isabelle}*} -ML %grayML{*fun pretty_helper aux env = + \begin{isabelle}\ +ML %grayML\fun pretty_helper aux env = env |> Vartab.dest |> map aux |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) @@ -821,19 +821,19 @@ val print = apply2 (pretty_typ ctxt) in pretty_helper (print o get_typs) tyenv -end*} -text_raw {* +end\ +text_raw \ \end{isabelle} \end{minipage} \caption{A pretty printing function for type environments, which are produced by unification and matching.\label{fig:prettyenv}} \end{figure} -*} - -text {* +\ + +text \ The first components in this list stand for the schematic type variables and the second are the associated sorts and types. In this example the sort is - the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will + the default sort \HOL.type\. Instead of @{ML "Vartab.dest"}, we will use in what follows our own pretty-printing function from Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type environment in the example this function prints out the more legible: @@ -846,38 +846,38 @@ The way the unification function @{ML typ_unify in Sign} is implemented using an initial type environment and initial index makes it easy to unify more than two terms. For example -*} - -ML %linenosgray{*val (tyenvs, _) = let +\ + +ML %linenosgray\val (tyenvs, _) = let val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"}) val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"}) in fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0) -end*} - -text {* - The index @{text 0} in Line 5 is the maximal index of the schematic type - variables occurring in @{text tys1} and @{text tys2}. This index will be +end\ + +text \ + The index \0\ in Line 5 is the maximal index of the schematic type + variables occurring in \tys1\ and \tys2\. This index will be increased whenever a new schematic type variable is introduced during unification. This is for example the case when two schematic type variables have different, incomparable sorts. Then a new schematic type variable is introduced with the combined sorts. To show this let us assume two sorts, - say @{text "s1"} and @{text "s2"}, which we attach to the schematic type - variables @{text "?'a"} and @{text "?'b"}. Since we do not make any + say \s1\ and \s2\, which we attach to the schematic type + variables \?'a\ and \?'b\. Since we do not make any assumption about the sorts, they are incomparable. -*} +\ class s1 class s2 -ML %grayML{*val (tyenv, index) = let +ML %grayML\val (tyenv, index) = let val ty1 = @{typ_pat "?'a::s1"} val ty2 = @{typ_pat "?'b::s2"} in Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) -end*} - -text {* +end\ + +text \ To print out the result type environment we switch on the printing of sort information by setting @{ML_ind show_sorts in Syntax} to true. This allows us to inspect the typing environment. @@ -886,17 +886,17 @@ "pretty_tyenv @{context} tyenv" "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"} - As can be seen, the type variables @{text "?'a"} and @{text "?'b"} are instantiated - with a new type variable @{text "?'a1"} with sort @{text "{s1, s2}"}. Since a new - type variable has been introduced the @{ML index}, originally being @{text 0}, - has been increased to @{text 1}. + As can be seen, the type variables \?'a\ and \?'b\ are instantiated + with a new type variable \?'a1\ with sort \{s1, s2}\. Since a new + type variable has been introduced the @{ML index}, originally being \0\, + has been increased to \1\. @{ML_response [display,gray] "index" "1"} - Let us now return to the unification problem @{text "?'a * ?'b"} and - @{text "?'b list * nat"} from the beginning of this section, and the + Let us now return to the unification problem \?'a * ?'b\ and + \?'b list * nat\ from the beginning of this section, and the calculated type environment @{ML tyenv_unif}: @{ML_response_fake [display, gray] @@ -904,13 +904,12 @@ "[?'a := ?'b list, ?'b := nat]"} Observe that the type environment which the function @{ML typ_unify in - Sign} returns is \emph{not} an instantiation in fully solved form: while @{text - "?'b"} is instantiated to @{typ nat}, this is not propagated to the - instantiation for @{text "?'a"}. In unification theory, this is often + Sign} returns is \emph{not} an instantiation in fully solved form: while \?'b\ is instantiated to @{typ nat}, this is not propagated to the + instantiation for \?'a\. In unification theory, this is often called an instantiation in \emph{triangular form}. These triangular instantiations, or triangular type environments, are used because of - performance reasons. To apply such a type environment to a type, say @{text "?'a * - ?'b"}, you should use the function @{ML_ind norm_type in Envir}: + performance reasons. To apply such a type environment to a type, say \?'a * + ?'b\, you should use the function @{ML_ind norm_type in Envir}: @{ML_response_fake [display, gray] "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}" @@ -918,18 +917,18 @@ Matching of types can be done with the function @{ML_ind typ_match in Sign} also from the structure @{ML_struct Sign}. This function returns a @{ML_type - Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case + Type.tyenv} as well, but might raise the exception \TYPE_MATCH\ in case of failure. For example -*} - -ML %grayML{*val tyenv_match = let +\ + +ML %grayML\val tyenv_match = let val pat = @{typ_pat "?'a * ?'b"} and ty = @{typ_pat "bool list * nat"} in Sign.typ_match @{theory} (pat, ty) Vartab.empty -end*} - -text {* +end\ + +text \ Printing out the calculated matcher gives @{ML_response_fake [display,gray] @@ -948,18 +947,18 @@ @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} for unifiers. To show the difference, let us calculate the following matcher: -*} - -ML %grayML{*val tyenv_match' = let +\ + +ML %grayML\val tyenv_match' = let val pat = @{typ_pat "?'a * ?'b"} and ty = @{typ_pat "?'b list * nat"} in Sign.typ_match @{theory} (pat, ty) Vartab.empty -end*} - -text {* +end\ + +text \ Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply - @{ML norm_type in Envir} to the type @{text "?'a * ?'b"} we obtain + @{ML norm_type in Envir} to the type \?'a * ?'b\ we obtain @{ML_response_fake [display, gray] "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}" @@ -983,43 +982,43 @@ which apply a type environment to a type. Type environments are lookup tables which are implemented in @{ML_file "Pure/term_ord.ML"}. \end{readmore} -*} - -text {* +\ + +text \ Unification and matching of terms is substantially more complicated than the type-case. The reason is that terms have abstractions and, in this context, unification or matching modulo plain equality is often not meaningful. Nevertheless, Isabelle implements the function @{ML_ind first_order_match in Pattern} for terms. This matching function returns a type environment and a term environment. To pretty print the latter we use - the function @{text "pretty_env"}: -*} - -ML %grayML{*fun pretty_env ctxt env = + the function \pretty_env\: +\ + +ML %grayML\fun pretty_env ctxt env = let fun get_trms (v, (T, t)) = (Var (v, T), t) val print = apply2 (pretty_term ctxt) in pretty_helper (print o get_trms) env -end*} - -text {* - As can be seen from the @{text "get_trms"}-function, a term environment associates +end\ + +text \ + As can be seen from the \get_trms\-function, a term environment associates a schematic term variable with a type and a term. An example of a first-order matching problem is the term @{term "P (\a b. Q b a)"} and the pattern - @{text "?X ?Y"}. -*} - -ML %grayML{*val (_, fo_env) = let + \?X ?Y\. +\ + +ML %grayML\val (_, fo_env) = let val fo_pat = @{term_pat "(?X::(nat\nat\nat)\bool) ?Y"} val trm_a = @{term "P::(nat\nat\nat)\bool"} val trm_b = @{term "\a b. (Q::nat\nat\nat) b a"} val init = (Vartab.empty, Vartab.empty) in Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init -end *} - -text {* +end\ + +text \ In this example we annotated types explicitly because then the type environment is empty and can be ignored. The resulting term environment is @@ -1048,8 +1047,8 @@ variables. It can also deal with abstractions and a limited form of alpha-equivalence, but this kind of matching should be used with care, since it is not clear whether the result is meaningful. A meaningful example is - matching @{text "\x. P x"} against the pattern @{text "\y. ?X y"}. In this - case, first-order matching produces @{text "[?X := P]"}. + matching \\x. P x\ against the pattern \\y. ?X y\. In this + case, first-order matching produces \[?X := P]\. @{ML_response_fake [display, gray] "let @@ -1062,9 +1061,9 @@ |> pretty_env @{context} end" "[?X := P]"} -*} - -text {* +\ + +text \ Unification of abstractions is more thoroughly studied in the context of higher-order pattern unification and higher-order pattern matching. A \emph{\index*{pattern}} is a well-formed term in which the arguments to @@ -1114,42 +1113,41 @@ "[?X := \y x. x, ?Y := \x. x]"} The function @{ML_ind "Envir.empty"} generates a record with a specified - max-index for the schematic variables (in the example the index is @{text - 0}) and empty type and term environments. The function @{ML_ind + max-index for the schematic variables (in the example the index is \0\) and empty type and term environments. The function @{ML_ind "Envir.term_env"} pulls out the term environment from the result record. The corresponding function for type environment is @{ML_ind "Envir.type_env"}. An assumption of this function is that the terms to be unified have already the same type. In case of failure, the exceptions that - are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}. + are raised are either \Pattern\, \MATCH\ or \Unif\. As mentioned before, unrestricted higher-order unification, respectively unrestricted higher-order matching, is in general undecidable and might also not possess a single most general solution. Therefore Isabelle implements the unification function @{ML_ind unifiers in Unify} so that it returns a lazy list of potentially infinite unifiers. An example is as follows -*} - -ML %grayML{*val uni_seq = +\ + +ML %grayML\val uni_seq = let val trm1 = @{term_pat "?X ?Y"} val trm2 = @{term "f a"} val init = Envir.empty 0 in Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)]) -end *} - -text {* +end\ + +text \ The unifiers can be extracted from the lazy sequence using the function @{ML_ind "Seq.pull"}. In the example we obtain three - unifiers @{text "un1\un3"}. -*} - -ML %grayML{*val SOME ((un1, _), next1) = Seq.pull uni_seq; + unifiers \un1\un3\. +\ + +ML %grayML\val SOME ((un1, _), next1) = Seq.pull uni_seq; val SOME ((un2, _), next2) = Seq.pull next1; val SOME ((un3, _), next3) = Seq.pull next2; -val NONE = Seq.pull next3 *} - -text {* +val NONE = Seq.pull next3\ + +text \ \footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?} We can print them out as follows. @@ -1207,20 +1205,20 @@ \begin{isabelle} \isacommand{thm}~@{thm [source] spec}\\ - @{text "> "}~@{thm spec} + \> \~@{thm spec} \end{isabelle} as an introduction rule. Applying it directly can lead to unexpected behaviour since the unification has more than one solution. One way round - this problem is to instantiate the schematic variables @{text "?P"} and - @{text "?x"}. Instantiation function for theorems is + this problem is to instantiate the schematic variables \?P\ and + \?x\. Instantiation function for theorems is @{ML_ind instantiate_normalize in Drule} from the structure @{ML_struct Drule}. One problem, however, is that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"} respective @{ML_type "(indexname * typ) * cterm"}: \begin{isabelle} - @{ML instantiate_normalize in Drule}@{text ":"} + @{ML instantiate_normalize in Drule}\:\ @{ML_type "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm"} \end{isabelle} @@ -1230,23 +1228,23 @@ from an environment the corresponding variable mappings for schematic type and term variables. These mappings can be turned into proper @{ML_type ctyp}-pairs with the function -*} - -ML %grayML{*fun prep_trm ctxt (x, (T, t)) = - ((x, T), Thm.cterm_of ctxt t)*} - -text {* +\ + +ML %grayML\fun prep_trm ctxt (x, (T, t)) = + ((x, T), Thm.cterm_of ctxt t)\ + +text \ and into proper @{ML_type cterm}-pairs with -*} - -ML %grayML{*fun prep_ty ctxt (x, (S, ty)) = - ((x, S), Thm.ctyp_of ctxt ty)*} - -text {* +\ + +ML %grayML\fun prep_ty ctxt (x, (S, ty)) = + ((x, S), Thm.ctyp_of ctxt ty)\ + +text \ We can now calculate the instantiations from the matching function. -*} - -ML %linenosgray{*fun matcher_inst ctxt pat trm i = +\ + +ML %linenosgray\fun matcher_inst ctxt pat trm i = let val univ = Unify.matchers (Context.Proof ctxt) [(pat, trm)] val env = nth (Seq.list_of univ) i @@ -1254,13 +1252,13 @@ val tyenv = Vartab.dest (Envir.type_env env) in (map (prep_ty ctxt) tyenv, map (prep_trm ctxt) tenv) -end*} +end\ ML \Context.get_generic_context\ -text {* +text \ In Line 3 we obtain the higher-order matcher. We assume there is a finite number of them and select the one we are interested in via the parameter - @{text i} in the next line. In Lines 5 and 6 we destruct the resulting + \i\ in the next line. In Lines 5 and 6 we destruct the resulting environments using the function @{ML_ind dest in Vartab}. Finally, we need to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective environments (Line 8). As a simple example we instantiate the @@ -1278,7 +1276,7 @@ end" "\x. Q x \ Q True"} - Note that we had to insert a @{text "Trueprop"}-coercion in Line 3 since the + Note that we had to insert a \Trueprop\-coercion in Line 3 since the conclusion of @{thm [source] spec} contains one. \begin{readmore} @@ -1288,11 +1286,11 @@ in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented in @{ML_file "Pure/General/seq.ML"}. \end{readmore} -*} - -section {* Sorts (TBD)\label{sec:sorts} *} - -text {* +\ + +section \Sorts (TBD)\label{sec:sorts}\ + +text \ Type classes are formal names in the type system which are linked to predicates of one type variable (via the axclass mechanism) and thereby express extra properties on types, to be propagated by the type system. @@ -1320,14 +1318,14 @@ Free and schematic type variables are always annotated with sorts, thereby restricting the domain of types they quantify over and corresponding to an implicit hypothesis about the type variable. -*} - - -ML {* Sign.classes_of @{theory} *} - -ML {* Sign.of_sort @{theory} *} - -text {* +\ + + +ML \Sign.classes_of @{theory}\ + +ML \Sign.of_sort @{theory}\ + +text \ \begin{readmore} Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}. @@ -1344,12 +1342,12 @@ functionality. It also provides the most needed functionality from individual underlying modules. \end{readmore} -*} - - -section {* Type-Checking\label{sec:typechecking} *} - -text {* +\ + + +section \Type-Checking\label{sec:typechecking}\ + +text \ Remember Isabelle follows the Church-style typing for terms, i.e.\ a term contains enough typing information (constants, free variables and abstractions all have typing information) so that it is always clear what the type of a term is. @@ -1400,8 +1398,8 @@ "Const (\"HOL.plus_class.plus\", \"nat \ nat \ nat\") $ Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} - Instead of giving explicitly the type for the constant @{text "plus"} and the free - variable @{text "x"}, type-inference fills in the missing information. + Instead of giving explicitly the type for the constant \plus\ and the free + variable \x\, type-inference fills in the missing information. \begin{readmore} See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, @@ -1417,11 +1415,11 @@ exercise given in Appendix \ref{ch:solutions} when they receive an ill-typed term as input. \end{exercise} -*} - -section {* Certified Terms and Certified Types *} - -text {* +\ + +section \Certified Terms and Certified Types\ + +text \ You can freely construct and manipulate @{ML_type "term"}s and @{ML_type typ}es, since they are just arbitrary unchecked trees. However, you eventually want to see if a term is well-formed, or type-checks, relative to @@ -1502,11 +1500,11 @@ the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. \end{readmore} -*} - -section {* Theorems\label{sec:theorems} *} - -text {* +\ + +section \Theorems\label{sec:theorems}\ + +text \ Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} that can only be built by going through interfaces. As a consequence, every proof in Isabelle is correct by construction. This follows the tradition of the LCF-approach. @@ -1514,18 +1512,18 @@ To see theorems in ``action'', let us give a proof on the ML-level for the following statement: -*} +\ lemma assumes assm\<^sub>1: "\(x::nat). P x \ Q x" and assm\<^sub>2: "P t" shows "Q t"(*<*)oops(*>*) -text {* +text \ The corresponding ML-code is as follows: -*} - -ML %linenosgray{*val my_thm = +\ + +ML %linenosgray\val my_thm = let val assm1 = @{cprop "\(x::nat). P x \ Q x"} val assm2 = @{cprop "(P::nat \ bool) t"} @@ -1539,11 +1537,11 @@ Qt |> Thm.implies_intr assm2 |> Thm.implies_intr assm1 -end*} - -text {* - Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \}"}, which - inserts necessary @{text "Trueprop"}s. +end\ + +text \ + Note that in Line 3 and 4 we use the antiquotation \@{cprop \}\, which + inserts necessary \Trueprop\s. If we print out the value of @{ML my_thm} then we see only the final statement of the theorem. @@ -1556,10 +1554,10 @@ proof. \[ - \infer[(@{text "\"}$-$intro)]{\vdash @{prop "(\x. P x \ Q x) \ P t \ Q t"}} - {\infer[(@{text "\"}$-$intro)]{@{prop "\x. P x \ Q x"} \vdash @{prop "P t \ Q t"}} - {\infer[(@{text "\"}$-$elim)]{@{prop "\x. P x \ Q x"}, @{prop "P t"} \vdash @{prop "Q t"}} - {\infer[(@{text "\"}$-$elim)]{@{prop "\x. P x \ Q x"} \vdash @{prop "P t \ Q t"}} + \infer[(\\\$-$intro)]{\vdash @{prop "(\x. P x \ Q x) \ P t \ Q t"}} + {\infer[(\\\$-$intro)]{@{prop "\x. P x \ Q x"} \vdash @{prop "P t \ Q t"}} + {\infer[(\\\$-$elim)]{@{prop "\x. P x \ Q x"}, @{prop "P t"} \vdash @{prop "Q t"}} + {\infer[(\\\$-$elim)]{@{prop "\x. P x \ Q x"} \vdash @{prop "P t \ Q t"}} {\infer[(assume)]{@{prop "\x. P x \ Q x"} \vdash @{prop "\x. P x \ Q x"}}{}} & \infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{} @@ -1575,22 +1573,22 @@ @{ML_struct Local_Theory} (the Isabelle command \isacommand{local\_setup} will be explained in more detail in Section~\ref{sec:local}). -*} +\ (*FIXME: add forward reference to Proof_Context.export *) -ML %linenosgray{*val my_thm_vars = +ML %linenosgray\val my_thm_vars = let val ctxt0 = @{context} val (_, ctxt1) = Variable.add_fixes ["P", "Q", "t"] ctxt0 in singleton (Proof_Context.export ctxt1 ctxt0) my_thm -end*} - -local_setup %gray {* - Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd *} - - -text {* +end\ + +local_setup %gray \ + Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd\ + + +text \ The third argument of @{ML note in Local_Theory} is the list of theorems we want to store under a name. We can store more than one under a single name. The first argument of @{ML note in Local_Theory} is the name under @@ -1598,13 +1596,13 @@ list of theorem attributes, which we will explain in detail in Section~\ref{sec:attributes}. Below we just use one such attribute, @{ML_ind simp_add in Simplifier}, for adding the theorem to the simpset: -*} - -local_setup %gray {* +\ + +local_setup %gray \ Local_Theory.note ((@{binding "my_thm_simp"}, - [Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd *} - -text {* + [Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd\ + +text \ Note that we have to use another name under which the theorem is stored, since Isabelle does not allow us to call @{ML_ind note in Local_Theory} twice with the same name. The attribute needs to be wrapped inside the function @{ML_ind @@ -1628,12 +1626,12 @@ \begin{isabelle} - \isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline - @{text ">"}~@{prop "\\x. P x \ Q x; P t\ \ Q t"}\isanewline - @{text ">"}~@{prop "\\x. P x \ Q x; P t\ \ Q t"} + \isacommand{thm}~\my_thm my_thm_simp\\isanewline + \>\~@{prop "\\x. P x \ Q x; P t\ \ Q t"}\isanewline + \>\~@{prop "\\x. P x \ Q x; P t\ \ Q t"} \end{isabelle} - or with the @{text "@{thm \}"}-antiquotation on the ML-level. Otherwise the + or with the \@{thm \}\-antiquotation on the ML-level. Otherwise the user has no access to these theorems. Recall that Isabelle does not let you call @{ML note in Local_Theory} twice @@ -1644,78 +1642,78 @@ dynamically expanding list of theorems (like a simpset). Therefore Isabelle also implements a mechanism where a theorem name can refer to a custom theorem list. For this you can use the function @{ML_ind add_thms_dynamic in Global_Theory}. - To see how it works let us assume we defined our own theorem list @{text MyThmList}. -*} - -ML %grayML{*structure MyThmList = Generic_Data + To see how it works let us assume we defined our own theorem list \MyThmList\. +\ + +ML %grayML\structure MyThmList = Generic_Data (type T = thm list val empty = [] val extend = I val merge = merge Thm.eq_thm_prop) -fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*} - -text {* +fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))\ + +text \ The function @{ML update} allows us to update the theorem list, for example by adding the theorem @{thm [source] TrueI}. -*} - -setup %gray {* update @{thm TrueI} *} +\ + +setup %gray \update @{thm TrueI}\ -text {* +text \ We can now install the theorem list so that it is visible to the user and can be refered to by a theorem name. For this need to call @{ML_ind add_thms_dynamic in Global_Theory} -*} - -setup %gray {* +\ + +setup %gray \ Global_Theory.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) -*} - -text {* +\ + +text \ with a name and a function that accesses the theorem list. Now if the user issues the command \begin{isabelle} - \isacommand{thm}~@{text "mythmlist"}\\ - @{text "> True"} + \isacommand{thm}~\mythmlist\\\ + \> True\ \end{isabelle} the current content of the theorem list is displayed. If more theorems are stored in the list, say -*} - -setup %gray {* update @{thm FalseE} *} - -text {* +\ + +setup %gray \update @{thm FalseE}\ + +text \ then the same command produces \begin{isabelle} - \isacommand{thm}~@{text "mythmlist"}\\ - @{text "> False \ ?P"}\\ - @{text "> True"} + \isacommand{thm}~\mythmlist\\\ + \> False \ ?P\\\ + \> True\ \end{isabelle} Note that if we add the theorem @{thm [source] FalseE} again to the list -*} - -setup %gray {* update @{thm FalseE} *} - -text {* +\ + +setup %gray \update @{thm FalseE}\ + +text \ we still obtain the same list. The reason is that we used the function @{ML_ind add_thm in Thm} in our update function. This is a dedicated function which tests whether the theorem is already in the list. This test is done according to alpha-equivalence of the proposition of the theorem. The corresponding testing function is @{ML_ind eq_thm_prop in Thm}. Suppose you proved the following three theorems. -*} +\ lemma shows thm1: "\x. P x" and thm2: "\y. P y" and thm3: "\y. Q y" sorry -text {* +text \ Testing them for alpha equality produces: @{ML_response [display,gray] @@ -1738,13 +1736,13 @@ Other function produce terms that can be pattern-matched. Suppose the following two theorems. -*} +\ lemma shows foo_test1: "A \ B \ C" and foo_test2: "A \ B \ C" sorry -text {* +text \ We can destruct them into premises and conclusions as follows. @{ML_response_fake [display,gray] @@ -1765,8 +1763,8 @@ Premises: Conclusion: ?A \ ?B \ ?C"} - Note that in the second case, there is no premise. The reason is that @{text "\"} - separates premises and conclusion, while @{text "\"} is the object implication + Note that in the second case, there is no premise. The reason is that \\\ + separates premises and conclusion, while \\\ is the object implication from HOL, which just constructs a formula. \begin{readmore} @@ -1788,8 +1786,8 @@ "(\x. x) = (\x. x) \ (\x. x) = (\x. x)"} Often it is necessary to transform theorems to and from the object - logic, that is replacing all @{text "\"} and @{text "\"} by @{text "\"} - and @{text "\"}, or the other way around. A reason for such a transformation + logic, that is replacing all \\\ and \\\ by \\\ + and \\\, or the other way around. A reason for such a transformation might be stating a definition. The reason is that definitions can only be stated using object logic connectives, while theorems using the connectives from the meta logic are more convenient for reasoning. Therefore there are @@ -1822,21 +1820,21 @@ @{thm [display] list.induct} - we have to first abstract over the meta variables @{text "?P"} and - @{text "?list"}. For this we can use the function + we have to first abstract over the meta variables \?P\ and + \?list\. For this we can use the function @{ML_ind forall_intr_vars in Drule}. This allows us to implement the following function for atomizing a theorem. -*} - -ML %grayML{*fun atomize_thm ctxt thm = +\ + +ML %grayML\fun atomize_thm ctxt thm = let val thm' = forall_intr_vars thm val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm') in Raw_Simplifier.rewrite_rule ctxt [thm''] thm' -end*} - -text {* +end\ + +text \ This function produces for the theorem @{thm [source] list.induct} @{ML_response_fake [display, gray] @@ -1859,7 +1857,7 @@ This function takes first a context and second a list of strings. This list specifies which variables should be turned into schematic variables once the term - is proved (in this case only @{text "\"P\""}). The fourth argument is the term to be + is proved (in this case only \"P"\). The fourth argument is the term to be proved. The fifth is a corresponding proof given in form of a tactic (we explain tactics in Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem by assumption. @@ -1867,16 +1865,16 @@ There is also the possibility of proving multiple goals at the same time using the function @{ML_ind prove_common in Goal}. For this let us define the following three helper functions. -*} - -ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"} +\ + +ML %grayML\fun rep_goals i = replicate i @{prop "f x = f x"} fun rep_tacs i = replicate i (resolve_tac @{context} [@{thm refl}]) fun multi_test ctxt i = Goal.prove_common ctxt NONE ["f", "x"] [] (rep_goals i) - (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*} - -text {* + (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))\ + +text \ With them we can now produce three theorem instances of the proposition. @@ -1885,19 +1883,19 @@ "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"} However you should be careful with @{ML prove_common in Goal} and very - large goals. If you increase the counter in the code above to @{text 3000}, + large goals. If you increase the counter in the code above to \3000\, you will notice that takes approximately ten(!) times longer than using @{ML map} and @{ML prove in Goal}. -*} +\ -ML %grayML{*let +ML %grayML\let fun test_prove ctxt thm = Goal.prove ctxt ["P", "x"] [] thm (K (resolve_tac @{context} [@{thm refl}] 1)) in map (test_prove @{context}) (rep_goals 3000) -end*} - -text {* +end\ + +text \ While the LCF-approach of going through interfaces ensures soundness in Isabelle, there is the function @{ML_ind make_thm in Skip_Proof} in the structure @{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem. @@ -1919,12 +1917,12 @@ kind, the names for cases and so on. This data is stored in a string-string list and can be retrieved with the function @{ML_ind get_tags in Thm}. Assume you prove the following lemma. -*} +\ lemma foo_data: shows "P \ P \ P" by assumption -text {* +text \ The auxiliary data of this lemma can be retrieved using the function @{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is @@ -1936,14 +1934,14 @@ 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 Rule_Cases} from the structure @{ML_struct Rule_Cases}. -*} - -local_setup %gray {* +\ + +local_setup %gray \ Local_Theory.note ((@{binding "foo_data'"}, []), [(Rule_Cases.name ["foo_case_one", "foo_case_two"] - @{thm foo_data})]) #> snd *} - -text {* + @{thm foo_data})]) #> snd\ + +text \ The data of the theorem @{thm [source] foo_data'} is then as follows: @{ML_response_fake [display,gray] @@ -1952,63 +1950,62 @@ (\"case_names\", \"foo_case_one;foo_case_two\")]"} You can observe the case names of this lemma on the user level when using - the proof methods @{text cases} and @{text induct}. In the proof below -*} + the proof methods \cases\ and \induct\. In the proof below +\ lemma shows "Q \ Q \ Q" proof (cases rule: foo_data') (*<*)oops(*>*) -text_raw{* +text_raw\ \begin{tabular}{@ {}l} \isacommand{print\_cases}\\ -@{text "> cases:"}\\ -@{text "> foo_case_one:"}\\ -@{text "> let \"?case\" = \"?P\""}\\ -@{text "> foo_case_two:"}\\ -@{text "> let \"?case\" = \"?P\""} -\end{tabular}*} - -text {* - we can proceed by analysing the cases @{text "foo_case_one"} and - @{text "foo_case_two"}. While if the theorem has no names, then - the cases have standard names @{text 1}, @{text 2} and so +\> cases:\\\ +\> foo_case_one:\\\ +\> let "?case" = "?P"\\\ +\> foo_case_two:\\\ +\> let "?case" = "?P"\ +\end{tabular}\ + +text \ + we can proceed by analysing the cases \foo_case_one\ and + \foo_case_two\. While if the theorem has no names, then + the cases have standard names \1\, \2\ and so on. This can be seen in the proof below. -*} +\ lemma shows "Q \ Q \ Q" proof (cases rule: foo_data) (*<*)oops(*>*) -text_raw{* +text_raw\ \begin{tabular}{@ {}l} \isacommand{print\_cases}\\ -@{text "> cases:"}\\ -@{text "> 1:"}\\ -@{text "> let \"?case\" = \"?P\""}\\ -@{text "> 2:"}\\ -@{text "> let \"?case\" = \"?P\""} -\end{tabular}*} +\> cases:\\\ +\> 1:\\\ +\> let "?case" = "?P"\\\ +\> 2:\\\ +\> let "?case" = "?P"\ +\end{tabular}\ -text {* +text \ Sometimes one wants to know the theorems that are involved in - proving a theorem, especially when the proof is by @{text - auto}. These theorems can be obtained by introspecting the proved theorem. + proving a theorem, especially when the proof is by \auto\. These theorems can be obtained by introspecting the proved theorem. To introspect a theorem, let us define the following three functions that analyse the @{ML_type_ind proof_body} data-structure from the structure @{ML_struct Proofterm}. -*} - -ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms +\ + +ML %grayML\fun pthms_of (PBody {thms, ...}) = map #2 thms val get_names = (map Proofterm.thm_node_name) o pthms_of -val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *} - -text {* +val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\ + +text \ To see what their purpose is, consider the following three short proofs. -*} +\ lemma my_conjIa: shows "A \ B \ A \ B" @@ -2030,10 +2027,10 @@ done -text {* +text \ While the information about which theorems are used is obvious in the first two proofs, it is not obvious in the third, because of the - @{text auto}-step. Fortunately, ``behind'' every proved theorem is + \auto\-step. Fortunately, ``behind'' every proved theorem is a proof-tree that records all theorems that are employed for establishing this theorem. We can traverse this proof-tree extracting this information. Let us first extract the name of the @@ -2045,7 +2042,7 @@ |> get_names" "[\"Essential.my_conjIa\"]"} - whereby @{text "Essential"} refers to the theory name in which + whereby \Essential\ refers to the theory name in which we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind proof_body_of in Thm} returns a part of the data that is stored in a theorem. Notice that the first proof above references @@ -2064,7 +2061,7 @@ The theorems @{thm [source] Pure.protectD} and @{thm [source] Pure.protectI} that are internal theorems are always part of a - proof in Isabelle. Note also that applications of @{text assumption} do not + proof in Isabelle. Note also that applications of \assumption\ do not count as a separate theorem, as you can see in the following code. @{ML_response_fake [display,gray] @@ -2126,54 +2123,54 @@ styles}}. These are, roughly speaking, functions from terms to terms. The input term stands for the theorem to be presented; the output can be constructed to ones wishes. Let us, for example, assume we want to quote theorems without - leading @{text \}-quantifiers. For this we can implement the following function - that strips off @{text "\"}s. -*} - -ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = + leading \\\-quantifiers. For this we can implement the following function + that strips off \\\s. +\ + +ML %linenosgray\fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = Term.dest_abs body |> snd |> strip_allq | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = strip_allq t - | strip_allq t = t*} - -text {* + | strip_allq t = t\ + +text \ We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions, since this function deals correctly with potential name clashes. This function produces a pair consisting of the variable and the body of the abstraction. We are only interested in the body, which we feed into the recursive call. In Line 3 and 4, we also have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can - install this function as the theorem style named @{text "my_strip_allq"}. -*} - -setup %gray{* + install this function as the theorem style named \my_strip_allq\. +\ + +setup %gray\ Term_Style.setup @{binding "my_strip_allq"} (Scan.succeed (K strip_allq)) -*} - -text {* +\ + +text \ We can test this theorem style with the following theorem -*} +\ theorem style_test: shows "\x y z. (x, x) = (y, z)" sorry -text {* +text \ Now printing out in a document the theorem @{thm [source] style_test} normally - using @{text "@{thm \}"} produces + using \@{thm \}\ produces \begin{isabelle} \begin{graybox} - @{text "@{thm style_test}"}\\ - @{text ">"}~@{thm style_test} + \@{thm style_test}\\\ + \>\~@{thm style_test} \end{graybox} \end{isabelle} - as expected. But with the theorem style @{text "@{thm (my_strip_allq) \}"} + as expected. But with the theorem style \@{thm (my_strip_allq) \}\ we obtain \begin{isabelle} \begin{graybox} - @{text "@{thm (my_strip_allq) style_test}"}\\ - @{text ">"}~@{thm (my_strip_allq) style_test} + \@{thm (my_strip_allq) style_test}\\\ + \>\~@{thm (my_strip_allq) style_test} \end{graybox} \end{isabelle} @@ -2181,43 +2178,43 @@ giving a list of strings that should be used for the replacement of the variables. For this we implement the function which takes a list of strings and uses them as name in the outermost abstractions. -*} - -ML %grayML{*fun rename_allq [] t = t +\ + +ML %grayML\fun rename_allq [] t = t | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t) | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) = rename_allq xs t - | rename_allq _ t = t*} - -text {* + | rename_allq _ t = t\ + +text \ We can now install a the modified theorem style as follows -*} - -setup %gray {* let +\ + +setup %gray \let val parser = Scan.repeat Args.name fun action xs = K (rename_allq xs #> strip_allq) in Term_Style.setup @{binding "my_strip_allq2"} (parser >> action) -end *} - -text {* - The parser reads a list of names. In the function @{text action} we first +end\ + +text \ + The parser reads a list of names. In the function \action\ we first call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq} on the resulting term. We can now suggest, for example, two variables for - stripping off the first two @{text \}-quantifiers. + stripping off the first two \\\-quantifiers. \begin{isabelle} \begin{graybox} - @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\ - @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test} + \@{thm (my_strip_allq2 x' x'') style_test}\\\ + \>\~@{thm (my_strip_allq2 x' x'') style_test} \end{graybox} \end{isabelle} Such styles allow one to print out theorems in documents formatted to ones heart content. The styles can also be used in the document - antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"} - and @{text "@{typeof ...}"}. + antiquotations \@{prop ...}\, \@{term_type ...}\ + and \@{typeof ...}\. Next we explain theorem attributes, which is another mechanism for dealing with theorems. @@ -2225,13 +2222,12 @@ \begin{readmore} Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}. \end{readmore} -*} - -section {* Theorem Attributes\label{sec:attributes} *} - -text {* - Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \]"}, @{text - "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags +\ + +section \Theorem Attributes\label{sec:attributes}\ + +text \ + Theorem attributes are \[symmetric]\, \[THEN \]\, \[simp]\ and so on. Such attributes are \emph{neither} tags \emph{nor} flags annotated to theorems, but functions that do further processing of theorems. In particular, it is not possible to find out what are all theorems that have a given attribute in common, unless of course @@ -2243,121 +2239,121 @@ \begin{isabelle} \isacommand{print\_attributes}\\ - @{text "> COMP: direct composition with rules (no lifting)"}\\ - @{text "> HOL.dest: declaration of Classical destruction rule"}\\ - @{text "> HOL.elim: declaration of Classical elimination rule"}\\ - @{text "> \"} + \> COMP: direct composition with rules (no lifting)\\\ + \> HOL.dest: declaration of Classical destruction rule\\\ + \> HOL.elim: declaration of Classical elimination rule\\\ + \> \\ \end{isabelle} The theorem attributes fall roughly into two categories: the first category manipulates - theorems (for example @{text "[symmetric]"} and @{text "[THEN \]"}), and the second - stores theorems somewhere as data (for example @{text "[simp]"}, which adds + theorems (for example \[symmetric]\ and \[THEN \]\), and the second + stores theorems somewhere as data (for example \[simp]\, which adds theorems to the current simpset). To explain how to write your own attribute, let us start with an extremely simple - version of the attribute @{text "[symmetric]"}. The purpose of this attribute is + version of the attribute \[symmetric]\. The purpose of this attribute is to produce the ``symmetric'' version of an equation. The main function behind this attribute is -*} - -ML %grayML{*val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})*} - -text {* +\ + +ML %grayML\val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})\ + +text \ where the function @{ML_ind rule_attribute in Thm} expects a function taking a - context (which we ignore in the code above) and a theorem (@{text thm}), and - returns another theorem (namely @{text thm} resolved with the theorem + context (which we ignore in the code above) and a theorem (\thm\), and + returns another theorem (namely \thm\ resolved with the theorem @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind RS in Drule} is explained in Section~\ref{sec:simpletacs}). The function @{ML rule_attribute in Thm} then returns an attribute. Before we can use the attribute, we need to set it up. This can be done using the Isabelle command \isacommand{attribute\_setup} as follows: -*} +\ attribute_setup %gray my_sym = - {* Scan.succeed my_symmetric *} "applying the sym rule" - -text {* - Inside the @{text "\ \ \"}, we have to specify a parser + \Scan.succeed my_symmetric\ "applying the sym rule" + +text \ + Inside the \\ \ \\, we have to specify a parser for the theorem attribute. Since the attribute does not expect any further - arguments (unlike @{text "[THEN \]"}, for instance), we use the parser @{ML - Scan.succeed}. An example for the attribute @{text "[my_sym]"} is the proof -*} + arguments (unlike \[THEN \]\, for instance), we use the parser @{ML + Scan.succeed}. An example for the attribute \[my_sym]\ is the proof +\ lemma test[my_sym]: "2 = Suc (Suc 0)" by simp -text {* +text \ which stores the theorem @{thm test} under the name @{thm [source] test}. You can see this, if you query the lemma: \begin{isabelle} - \isacommand{thm}~@{text "test"}\\ - @{text "> "}~@{thm test} + \isacommand{thm}~\test\\\ + \> \~@{thm test} \end{isabelle} We can also use the attribute when referring to this theorem: \begin{isabelle} - \isacommand{thm}~@{text "test[my_sym]"}\\ - @{text "> "}~@{thm test[my_sym]} + \isacommand{thm}~\test[my_sym]\\\ + \> \~@{thm test[my_sym]} \end{isabelle} An alternative for setting up an attribute is the function @{ML_ind setup in Attrib}. So instead of using \isacommand{attribute\_setup}, you can also set up the attribute as follows: -*} - -ML %grayML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric) - "applying the sym rule" *} - -text {* +\ + +ML %grayML\Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric) + "applying the sym rule"\ + +text \ This gives a function from @{ML_type "theory -> theory"}, which can be used for example with \isacommand{setup} or with @{ML "Context.>> o Context.map_theory"}.\footnote{\bf FIXME: explain what happens here.} As an example of a slightly more complicated theorem attribute, we implement - our own version of @{text "[THEN \]"}. This attribute will take a list of theorems + our own version of \[THEN \]\. This attribute will take a list of theorems as argument and resolve the theorem with this list (one theorem after another). The code for this attribute is -*} - -ML %grayML{*fun MY_THEN thms = +\ + +ML %grayML\fun MY_THEN thms = let fun RS_rev thm1 thm2 = thm2 RS thm1 in Thm.rule_attribute [] (fn _ => fn thm => fold RS_rev thms thm) -end*} - -text {* +end\ + +text \ where for convenience we define the reverse and curried version of @{ML RS}. The setup of this theorem attribute uses the parser @{ML thms in Attrib}, which parses a list of theorems. -*} - -attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} +\ + +attribute_setup %gray MY_THEN = \Attrib.thms >> MY_THEN\ "resolving the list of theorems with the theorem" -text {* +text \ You can, for example, use this theorem attribute to turn an equation into a meta-equation: \begin{isabelle} - \isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\ - @{text "> "}~@{thm test[MY_THEN eq_reflection]} + \isacommand{thm}~\test[MY_THEN eq_reflection]\\\ + \> \~@{thm test[MY_THEN eq_reflection]} \end{isabelle} If you need the symmetric version as a meta-equation, you can write \begin{isabelle} - \isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\ - @{text "> "}~@{thm test[MY_THEN sym eq_reflection]} + \isacommand{thm}~\test[MY_THEN sym eq_reflection]\\\ + \> \~@{thm test[MY_THEN sym eq_reflection]} \end{isabelle} It is also possible to combine different theorem attributes, as in: \begin{isabelle} - \isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\ - @{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]} + \isacommand{thm}~\test[my_sym, MY_THEN eq_reflection]\\\ + \> \~@{thm test[my_sym, MY_THEN eq_reflection]} \end{isabelle} However, here also a weakness of the concept @@ -2365,8 +2361,8 @@ arbitrary functions, they do not commute in general. If you try \begin{isabelle} - \isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\ - @{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"} + \isacommand{thm}~\test[MY_THEN eq_reflection, my_sym]\\\ + \> \~\exception THM 1 raised: RSN: no unifiers\ \end{isabelle} you get an exception indicating that the theorem @{thm [source] sym} @@ -2374,42 +2370,42 @@ The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate theorems. Another usage of theorem attributes is to add and delete theorems - from stored data. For example the theorem attribute @{text "[simp]"} adds + from stored data. For example the theorem attribute \[simp]\ adds or deletes a theorem from the current simpset. For these applications, you can use @{ML_ind declaration_attribute in Thm}. To illustrate this function, let us introduce a theorem list. -*} - -ML %grayML{*structure MyThms = Named_Thms +\ + +ML %grayML\structure MyThms = Named_Thms (val name = @{binding "attr_thms"} - val description = "Theorems for an Attribute") *} - -text {* + val description = "Theorems for an Attribute")\ + +text \ We are going to modify this list by adding and deleting theorems. For this we use the two functions @{ML MyThms.add_thm} and @{ML MyThms.del_thm}. You can turn them into attributes with the code -*} - -ML %grayML{*val my_add = Thm.declaration_attribute MyThms.add_thm -val my_del = Thm.declaration_attribute MyThms.del_thm *} - -text {* +\ + +ML %grayML\val my_add = Thm.declaration_attribute MyThms.add_thm +val my_del = Thm.declaration_attribute MyThms.del_thm\ + +text \ and set up the attributes as follows -*} - -attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *} +\ + +attribute_setup %gray my_thms = \Attrib.add_del my_add my_del\ "maintaining a list of my_thms" -text {* +text \ The parser @{ML_ind add_del in Attrib} is a predefined parser for adding and deleting lemmas. Now if you prove the next lemma - and attach to it the attribute @{text "[my_thms]"} -*} + and attach to it the attribute \[my_thms]\ +\ lemma trueI_2[my_thms]: "True" by simp -text {* +text \ then you can see it is added to the initially empty list. @{ML_response_fake [display,gray] @@ -2417,12 +2413,12 @@ "[\"True\"]"} You can also add theorems using the command \isacommand{declare}. -*} +\ declare test[my_thms] trueI_2[my_thms add] -text {* - With this attribute, the @{text "add"} operation is the default and does +text \ + With this attribute, the \add\ operation is the default and does not need to be explicitly given. These three declarations will cause the theorem list to be updated as: @@ -2433,11 +2429,11 @@ The theorem @{thm [source] trueI_2} only appears once, since the function @{ML_ind add_thm in Thm} tests for duplicates, before extending the list. Deletion from the list works as follows: -*} +\ declare test[my_thms del] -text {* After this, the theorem list is again: +text \After this, the theorem list is again: @{ML_response_fake [display,gray] "MyThms.get @{context}" @@ -2447,7 +2443,7 @@ declaration_attribute in Thm}, but there can be any number of them. We just have to change the parser for reading the arguments accordingly. - \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?} + \footnote{\bf FIXME What are: \theory_attributes\, \proof_attributes\?} \footnote{\bf FIXME readmore} \begin{readmore} @@ -2455,11 +2451,11 @@ @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about parsing. \end{readmore} -*} - -section {* Pretty-Printing\label{sec:pretty} *} - -text {* +\ + +section \Pretty-Printing\label{sec:pretty}\ + +text \ So far we printed out only plain strings without any formatting except for occasional explicit line breaks using @{text [quotes] "\\n"}. This is sufficient for ``quick-and-dirty'' printouts. For something more @@ -2483,26 +2479,26 @@ string}. This can be done with the function @{ML_ind string_of in Pretty}. In what follows we will use the following wrapper function for printing a pretty type: -*} - -ML %grayML{*fun pprint prt = tracing (Pretty.string_of prt)*} - -text {* +\ + +ML %grayML\fun pprint prt = tracing (Pretty.string_of prt)\ + +text \ The point of the pretty-printing infrastructure is to give hints about how to layout text and let Isabelle do the actual layout. Let us first explain how you can insert places where a line break can occur. For this assume the following function that replicates a string n times: -*} - -ML %grayML{*fun rep n str = implode (replicate n str) *} - -text {* +\ + +ML %grayML\fun rep n str = implode (replicate n str)\ + +text \ and suppose we want to print out the string: -*} - -ML %grayML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} - -text {* +\ + +ML %grayML\val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "\ + +text \ We deliberately chose a large string so that it spans over more than one line. If we print out the string using the usual ``quick-and-dirty'' method, then we obtain the ugly output: @@ -2590,9 +2586,9 @@ list as a ``set'', that means enclosed inside @{text [quotes] "{"} and @{text [quotes] "}"}, and separated by commas using the function @{ML_ind enum in Pretty}. For example -*} - -text {* +\ + +text \ @{ML_response_fake [display,gray] "let @@ -2613,9 +2609,9 @@ the last two items are separated by @{text [quotes] "and"}. For this you can write the function -*} - -ML %linenosgray{*fun and_list [] = [] +\ + +ML %linenosgray\fun and_list [] = [] | and_list [x] = [x] | and_list xs = let @@ -2623,9 +2619,9 @@ in (Pretty.commas front) @ [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last] - end *} - -text {* + end\ + +text \ where Line 7 prints the beginning of the list and Line 8 the last item. We have to use @{ML "Pretty.brk 1"} in order to insert a space (of length 1) before the @@ -2695,10 +2691,10 @@ We use the function @{ML_ind pretty_term in Syntax} for pretty-printing terms. Next we like to pretty-print a term and its type. For this we use the - function @{text "tell_type"}. -*} - -ML %linenosgray{*fun tell_type ctxt trm = + function \tell_type\. +\ + +ML %linenosgray\fun tell_type ctxt trm = let fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s)) val ptrm = Pretty.quote (Syntax.pretty_term ctxt trm) @@ -2707,9 +2703,9 @@ pprint (Pretty.blk (0, (pstr "The term " @ [ptrm] @ pstr " has type " @ [pty, Pretty.str "."]))) -end*} - -text {* +end\ + +text \ In Line 3 we define a function that inserts possible linebreaks in places where a space is. In Lines 4 and 5 we pretty-print the term and its type using the functions @{ML pretty_term in Syntax} and @{ML_ind @@ -2738,17 +2734,17 @@ @{ML_file "Pure/PIDE/markup.ML"} \end{readmore} -*} - -section {* Summary *} - -text {* +\ + +section \Summary\ + +text \ \begin{conventions} \begin{itemize} \item Start with a proper context and then pass it around through all your functions. \end{itemize} \end{conventions} -*} +\ end