diff -r d3fcc1a0272c -r 90bee31628dc CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Thu Feb 26 13:46:05 2009 +0100 +++ b/CookBook/FirstSteps.thy Thu Mar 12 08:11:02 2009 +0100 @@ -18,6 +18,9 @@ \ldots \end{tabular} \end{center} + + We also generally assume you are working with HOL. The given examples might + need to be adapted slightly if you work in a different logic. *} section {* Including ML-Code *} @@ -41,7 +44,7 @@ evaluated by using the advance and undo buttons of your Isabelle environment. The code inside the \isacommand{ML}-command can also contain value and function bindings, and even those can be undone when the proof - script is retracted. As mentioned earlier, we will drop the + script is retracted. As mentioned in the Introduction, we will drop the \isacommand{ML}~@{text "\ \ \"} scaffolding whenever we show code. The lines prefixed with @{text [quotes] ">"} are not part of the code, rather they indicate what the response is when the code is evaluated. @@ -151,15 +154,26 @@ text {* The easiest way to get the string of a theorem is to transform it - into a @{ML_type cterm} using the function @{ML crep_thm}. + into a @{ML_type cterm} using the function @{ML crep_thm}. Theorems + also include schematic variables, such as @{text "?P"}, @{text "?Q"} + and so on. In order to improve the readability of theorems we convert + these schematic variables into free variables using the + function @{ML Variable.import_thms}. *} -ML{*fun str_of_thm ctxt thm = - let - val {prop, ...} = crep_thm thm - in - str_of_cterm ctxt prop - end*} +ML{*fun no_vars ctxt thm = +let + val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt +in + thm' +end + +fun str_of_thm ctxt thm = +let + val {prop, ...} = crep_thm (no_vars ctxt thm) +in + str_of_cterm ctxt prop +end*} text {* Again the function @{ML commas} helps with printing more than one theorem. @@ -168,7 +182,6 @@ ML{*fun str_of_thms ctxt thms = commas (map (str_of_thm ctxt) thms)*} - section {* Combinators\label{sec:combinators} *} text {* @@ -395,29 +408,23 @@ ML{*fun get_thm_names_from_ss simpset = let - val ({rules,...}, _) = MetaSimplifier.rep_ss simpset + val {simps,...} = MetaSimplifier.dest_ss simpset in - map #name (Net.entries rules) + map #1 simps end*} text {* - The function @{ML rep_ss in MetaSimplifier} returns a record containing all - information about the simpset. The rules of a simpset are stored in a - \emph{discrimination net} (a data structure for fast indexing). From this - net you can extract the entries using the function @{ML Net.entries}. - You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored - in the current simpset---this simpset can be referred to using the antiquotation + The function @{ML dest_ss in MetaSimplifier} returns a record containing all + information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored + in the current simpset. This simpset can be referred to using the antiquotation @{text "@{simpset}"}. @{ML_response_fake [display,gray] "get_thm_names_from_ss @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} - \begin{readmore} - The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"} - and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented - in @{ML_file "Pure/net.ML"}. - \end{readmore} + Again, this way or referencing simpsets makes you independent from additions + of lemmas to the simpset by the user that potentially cause loops. While antiquotations have many applications, they were originally introduced in order to avoid explicit bindings for theorems such as: @@ -427,14 +434,13 @@ text {* These bindings are difficult to maintain and also can be accidentally - overwritten by the user. This often breakes Isabelle + overwritten by the user. This often broke Isabelle packages. Antiquotations solve this problem, since they are ``linked'' statically at compile-time. However, this static linkage also limits their usefulness in cases where data needs to be build up dynamically. In the course of this chapter you will learn more about these antiquotations: they can simplify Isabelle programming since one can directly access all kinds of logical elements from th ML-level. - *} section {* Terms and Types *} @@ -465,7 +471,7 @@ \end{readmore} Sometimes the internal representation of terms can be surprisingly different - from what you see at the user level, because the layers of + from what you see at the user-level, because the layers of parsing/type-checking/pretty printing can be quite elaborate. \begin{exercise} @@ -513,7 +519,7 @@ *} -section {* Constructing Terms and Types Manually *} +section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} text {* While antiquotations are very convenient for constructing terms, they can @@ -545,19 +551,18 @@ the given arguments @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" - "Const \ $ - Abs (\"x\", Type (\"nat\",[]), - Const \ $ (Free (\"S\",\) $ \) $ - (Free (\"T\",\) $ \))"} +"Const \ $ + Abs (\"x\", Type (\"nat\",[]), + Const \ $ (Free (\"S\",\) $ \) $ (Free (\"T\",\) $ \))"} whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} and @{text "Q"} from the antiquotation. @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" - "Const \ $ - Abs (\"x\", \, - Const \ $ (Const \ $ (Free (\"P\",\) $ \)) $ - (Const \ $ (Free (\"Q\",\) $ \)))"} +"Const \ $ + Abs (\"x\", \, + Const \ $ (Const \ $ (Free (\"P\",\) $ \)) $ + (Const \ $ (Free (\"Q\",\) $ \)))"} Although types of terms can often be inferred, there are many situations where you need to construct types manually, especially @@ -566,15 +571,15 @@ *} -ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *} +ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *} -text {* This can be equally written as: *} +text {* This can be equally written with the combinator @{ML "-->"} as: *} ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} text {* A handy function for manipulating terms is @{ML map_types}: it takes a - function and applies it to every type in the term. You can, for example, + 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: *} @@ -701,16 +706,18 @@ text {* Occasional you have to calculate what the ``base'' name of a given constant is. For this you can use the function @{ML Sign.extern_const} or - @{ML Sign.base_name}. For example: + @{ML Long_Name.base_name}. For example: @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} The difference between both functions is that @{ML extern_const in Sign} returns - the smallest name that is still unique, whereas @{ML base_name in Sign} always + the smallest name that is still unique, whereas @{ML base_name in Long_Name} always strips off all qualifiers. \begin{readmore} - FIXME + Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; + functions about signatures in @{ML_file "Pure/sign.ML"}. + \end{readmore} *} @@ -755,6 +762,19 @@ (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) end" "0 + 0"} + In Isabelle also types need can be certified. For example, you obtain + the certified type for the Isablle type @{typ "nat \ bool"} on the ML-level + as follows: + + @{ML_response_fake [display,gray] + "ctyp_of @{theory} (@{typ nat} --> @{typ bool})" + "nat \ bool"} + + \begin{readmore} + For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see + the file @{ML_file "Pure/thm.ML"}. + \end{readmore} + \begin{exercise} Check that the function defined in Exercise~\ref{fun:revsum} returns a result that type-checks. @@ -814,8 +834,12 @@ \begin{readmore} See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, - checking and pretty-printing of terms are defined. + checking and pretty-printing of terms are defined. Fuctions related to the + type inference are implemented in @{ML_file "Pure/type.ML"} and + @{ML_file "Pure/type_infer.ML"}. \end{readmore} + + (FIXME: say something about sorts) *} @@ -894,8 +918,7 @@ theorem is proven. In particular, it is not possible to find out what are all theorems that have a given attribute in common, unless of course the function behind the attribute stores the theorems in a retrivable - datastructure. This can be easily done by the recipe described in - \ref{rec:named}. + datastructure. If you want to print out all currently known attributes a theorem can have, you can use the function: @@ -919,7 +942,7 @@ context (which we ignore in the code above) and a theorem (@{text thm}), and returns another theorem (namely @{text thm} resolved with the lemma @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns - an attribute (of type @{ML_type "attribute"}). + an attribute. Before we can use the attribute, we need to set it up. This can be done using the function @{ML Attrib.add_attributes} as follows. @@ -927,8 +950,7 @@ setup {* Attrib.add_attributes - [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] -*} + [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *} text {* The attribute does not expect any further arguments (unlike @{text "[OF @@ -949,28 +971,183 @@ @{text "> "}~@{thm test[my_sym]} \end{isabelle} + The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems. + Another usage of attributes is to add and delete theorems from stored data. + For example the attribute @{text "[simp]"} adds or deletes a theorem from the + current simpset. For these applications, you can use @{ML Thm.declaration_attribute}. + To illustrate this function, let us introduce a reference containing a list + of theorems. *} +ML{*val my_thms = ref ([]:thm list)*} + +text {* + A word of warning: such references must not be used in any code that + is meant to be more than just for testing purposes! Here it is only used + to illustrate matters. We will show later how to store data properly without + using references. The function @{ML Thm.declaration_attribute} expects us to + provide two functions that add and delete theorems from this list. + For this we use the two functions: +*} + +ML{*fun my_thms_add thm ctxt = + (my_thms := Thm.add_thm thm (!my_thms); ctxt) + +fun my_thms_del thm ctxt = + (my_thms := Thm.del_thm thm (!my_thms); ctxt)*} + text {* -What are: + These functions take a theorem and a context and, for what we are explaining + here it is sufficient that they just return the context unchanged. They change + however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm} + adds a theorem if it is not already included in the list, and @{ML + Thm.del_thm} deletes one. Both functions use the predicate @{ML + Thm.eq_thm_prop} which compares theorems according to their proved + propositions (modulo alpha-equivalence). -@{text "declaration_attribute"} + You can turn both functions into attributes using +*} + +ML{*val my_add = Thm.declaration_attribute my_thms_add +val my_del = Thm.declaration_attribute my_thms_del *} + +text {* + and set up the attributes as follows +*} + +setup {* + Attrib.add_attributes + [("my_thms", Attrib.add_del_args my_add my_del, + "maintaining a list of my_thms")] *} + +text {* + Now if you prove the lemma attaching the attribute @{text "[my_thms]"} +*} + +lemma trueI_2[my_thms]: "True" by simp + +text {* + then you can see the lemma is added to the initially empty list. + + @{ML_response_fake [display,gray] + "!my_thms" "[\"True\"]"} + + You can also add theorems using the command \isacommand{declare}. +*} + +declare test[my_thms] trueI_2[my_thms add] + +text {* + The @{text "add"} is the default operation and does not need + to be given. This declaration will cause the theorem list to be + updated as follows. + + @{ML_response_fake [display,gray] + "!my_thms" + "[\"True\", \"Suc (Suc 0) = 2\"]"} + + The theorem @{thm [source] trueI_2} only appears once, since the + function @{ML Thm.add_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: + + @{ML_response_fake [display,gray] + "!my_thms" + "[\"True\"]"} + + We used in this example two functions declared as @{ML Thm.declaration_attribute}, + but there can be any number of them. We just have to change the parser for reading + the arguments accordingly. + + However, as said at the beginning of this example, using references for storing theorems is + \emph{not} the received way of doing such things. The received way is to + start a ``data slot'' in a context by using the functor @{text GenericDataFun}: +*} -@{text "theory_attributes"} +ML {*structure Data = GenericDataFun + (type T = thm list + val empty = [] + val extend = I + fun merge _ = Thm.merge_thms) *} + +text {* + To use this data slot, you only have to change @{ML my_thms_add} and + @{ML my_thms_del} to: +*} + +ML{*val thm_add = Data.map o Thm.add_thm +val thm_del = Data.map o Thm.del_thm*} + +text {* + where @{ML Data.map} updates the data appropriately in the context. Since storing + theorems in a special list is such a common task, there is the functor @{text NamedThmsFun}, + which does most of the work for you. To obtain such a named theorem lists, you just + declare +*} + +ML{*structure FooRules = NamedThmsFun + (val name = "foo" + val description = "Rules for foo"); *} + +text {* + and set up the @{ML_struct FooRules} with the command +*} + +setup {* FooRules.setup *} -@{text "proof_attributes"} +text {* + This code declares a data slot where the theorems are stored, + an attribute @{text foo} (with the @{text add} and @{text del} options + for adding and deleting theorems) and an internal ML interface to retrieve and + modify the theorems. + + Furthermore, the facts are made available on the user-level under the dynamic + fact name @{text foo}. For example you can declare three lemmas to be of the kind + @{text foo} by: +*} + +lemma rule1[foo]: "A" sorry +lemma rule2[foo]: "B" sorry +lemma rule3[foo]: "C" sorry + +text {* and undeclare the first one by: *} + +declare rule1[foo del] + +text {* and query the remaining ones with: + + \begin{isabelle} + \isacommand{thm}~@{text "foo"}\\ + @{text "> ?C"}\\ + @{text "> ?B"} + \end{isabelle} + + On the ML-level the rules marked with @{text "foo"} can be retrieved + using the function @{ML FooRules.get}: + + @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} + + \begin{readmore} + For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also + the recipe in Section~\ref{recipe:storingdata} about storing arbitrary + data. + \end{readmore} + + (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?) \begin{readmore} FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"} \end{readmore} - - *} -section {* Theories and Local Theories *} +section {* Theories, Contexts and Local Theories (TBD) *} text {* (FIXME: expand) @@ -992,7 +1169,7 @@ -section {* Storing Theorems\label{sec:storing} *} +section {* Storing Theorems\label{sec:storing} (TBD) *} text {* @{ML PureThy.add_thms_dynamic} *} @@ -1001,28 +1178,41 @@ (* FIXME: some code below *) (*<*) +(* setup {* - Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] + Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] *} - +*) lemma "bar = (1::nat)" oops +(* setup {* Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] #> PureThy.add_defs false [((Binding.name "foo_def", Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] #> snd *} - +*) +(* lemma "foo = (1::nat)" apply(simp add: foo_def) done thm foo_def +*) (*>*) -section {* Misc *} +section {* Pretty-Printing (TBD) *} + +text {* + @{ML Pretty.big_list}, + @{ML Pretty.brk}, + @{ML Pretty.block}, + @{ML Pretty.chunks} +*} + +section {* Misc (TBD) *} ML {*DatatypePackage.get_datatype @{theory} "List.list"*}