theory FirstStepsimports Mainuses "antiquote_setup.ML"begin(*<*)ML {*local structure O = ThyOutputin fun check_exists f = if File.exists (Path.explode ("~~/src/" ^ f)) then () else error ("Source file " ^ quote f ^ " does not exist.") val _ = O.add_commands [("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name => (check_exists name; Pretty.str name))))];end*}(*>*)chapter {* First Steps *}text {* Isabelle programming is done in Standard ML. Just like lemmas and proofs, code in Isabelle is part of a theory. If you want to follow the code written in this chapter, we assume you are working inside the theory defined by \begin{center} \begin{tabular}{@ {}l} \isacommand{theory} CookBook\\ \isacommand{imports} Main\\ \isacommand{begin}\\ \ldots \end{tabular} \end{center} The easiest and quickest way to include code in a theory is by using the \isacommand{ML} command. For example*}ML {* 3 + 4*}text {* The expression inside \isacommand{ML} commands is immediately evaluated, like ``normal'' Isabelle proof scripts, 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. However on such ML-commands the undo operation behaves slightly counter-intuitive, because if you define*}ML {* val foo = true*}text {* then Isabelle's undo operation has no effect on the definition of @{ML "foo"}. During developments you might find it necessary to quickly inspect some data in your code. This can be done in a ``quick-and-dirty'' fashion using the function @{ML "warning"}. For example *}ML {* val _ = warning "any string"*}text {* will print out @{ML "\"any string\""} inside the response buffer of Isabelle. PolyML provides a convenient, though quick-and-dirty, method for converting arbitrary values into strings, for example: *}ML {* val _ = warning (makestring 1)*}text {* However this only works if the type of what is printed is monomorphic and not a function.*}text {* (FIXME: add comment about including ML-files) *}section {* Antiquotations *}text {* The main advantage of embedding all code in a theory is that the code can contain references to entities defined on the logical level of Isabelle. This is done using antiquotations. For example, one can print out the name of the current theory by typing*}ML {* Context.theory_name @{theory} *}text {* where @{text "@{theory}"} is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory CookBook). The name of this theory can be extrated using the function @{ML "Context.theory_name"}. So the code above returns the string @{ML "\"CookBook\""}. Note, however, that antiquotations are statically scoped, that is the value is determined at ``compile-time'', not ``run-time''. For example the function*}ML {* fun current_thyname () = Context.theory_name @{theory}*}text {* does \emph{not} return the name of the current theory, if it is run in a different theory. Instead, the code above defines the constant function that always returns the string @{ML "\"CookBook\""}, no matter where the function is called. Operationally speaking, @{text "@{theory}"} is \emph{not} replaced with code that will look up the current theory in some data structure and return it. Instead, it is literally replaced with the value representing the theory name. In a similar way you can use antiquotations to refer to types and theorems:*}ML {* @{typ "(int * nat) list"} *}ML {* @{thm allI} *}text {* In the course of this introduction, we will learn more about these antoquotations: they greatly simplify Isabelle programming since one can directly access all kinds of logical elements from ML.*}section {* Terms *}text {* One way to construct terms of Isabelle on the ML-level is by using the antiquotation @{text "@{term \<dots>}"}:*}ML {* @{term "(a::nat) + b = c"} *}text {* This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal representation of this term. This internal represenation corresponds to the datatype defined in @{ML_file "Pure/term.ML"}. The internal representation of terms uses the usual de-Bruijn index mechanism where bound variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that binds the corresponding variable. However, in Isabelle the names of bound variables are kept at abstractions for printing purposes, and so should be treated only as comments. \begin{readmore} Terms are described in detail in \ichcite{ch:logic}. Their definition and many useful operations can be found in @{ML_file "Pure/term.ML"}. \end{readmore} Sometimes the internal representation can be surprisingly different from what you see at the user level, because the layers of parsing/type checking/pretty printing can be quite elaborate. \begin{exercise} Look at the internal term representation of the following terms, and find out why they are represented like this. \begin{itemize} \item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"} \item @{term "\<lambda>(x,y). P y x"} \item @{term "{ [x::int] | x. x \<le> -2 }"} \end{itemize} Hint: The third term is already quite big, and the pretty printer may omit parts of it by default. If you want to see all of it, you can use @{ML "print_depth 50"} to set the limit to a value high enough. \end{exercise} The anti-quotation @{text "@prop"} constructs terms of proposition type, inserting the invisible @{text "Trueprop"} coercion when necessary. Consider for example*}ML {* @{term "P x"} *}ML {* @{prop "P x"} *}text {* and *}ML {* @{term "P x \<Longrightarrow> Q x"} *}ML {* @{prop "P x \<Longrightarrow> Q x"} *}section {* Construting Terms Manually *} text {* While antiquotations are very convenient for constructing terms, they can only construct fixed terms. However, one often needs to construct terms dynamially. For example in order to write the function that returns the implication @{term "\<And>x. P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments, one can only write*}ML {* fun make_PQ_imp P Q = let val nat = HOLogic.natT val x = Free ("x", nat) in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), HOLogic.mk_Trueprop (Q $ x))) end*}text {* The reason is that one cannot pass the arguments @{term P} and @{term Q} into an antiquotation. *}text {* The internal names of constants like @{term "zero"} or @{text "+"} are often more complex than one first expects. Here, the extra prefixes @{text zero_class} and @{text plus_class} are present because the constants are defined within a type class. Guessing such internal names can be extremely hard, which is why the system provides another antiquotation: @{ML "@{const_name plus}"} gives just this name. For example *}ML {* @{const_name plus} *}text {* produes the fully qualyfied name of the constant plus. *}text {* There are many funtions in @{ML_file "Pure/logic.ML"} and @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms easier. Have a look ther and try to solve the following exercises:*}text {* \begin{exercise} Write a function @{ML_text "rev_sum : term -> term"} that takes a term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero) and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} associates to the left. Try your function on some examples, and see if the result typechecks. \end{exercise}*}ML {* fun rev_sum t = let fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u | dest_sum u = [u] in foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) end;*}text {* \begin{exercise} Write a function which takes two terms representing natural numbers in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary number representing their sum. \end{exercise}*}ML {* fun make_sum t1 t2 = HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)*}section {* Type checking *}text {* We can freely construct and manipulate terms, since they are just arbitrary unchecked trees. However, we eventually want to see if a term is wellformed, or type checks, relative to a theory. Type checking is done via the function @{ML cterm_of}, which turns a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are abstract objects that are guaranteed to be type-correct, and can only be constructed via the official interfaces. Type checking is always relative to a theory context. For now we can use the @{ML "@{theory}"} antiquotation to get hold of the current theory. For example we can write:*}ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}ML {* let val natT = @{typ "nat"} val zero = @{term "0::nat"} in cterm_of @{theory} (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) end*}section {* Theorems *}text {* Just like @{ML_type cterm}s, theorems (of type @{ML_type thm}) are abstract objects that can only be built by going through the kernel interfaces, which means that all your proofs will be checked. The basic rules of the Isabelle/Pure logical framework are defined in @{ML_file "Pure/thm.ML"}. Using these rules, which are just ML functions, you can do simple natural deduction proofs on the ML level. For example, the statement*} lemma assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" and assm\<^isub>2: "P t" shows "Q t" (*<*)oops(*>*) text {* can be proved in ML like this\footnote{Note that @{text "|>"} is just reverse application. This combinator, and several variants are defined in @{ML_file "Pure/General/basics.ML"}}:*}ML {*let val thy = @{theory} val assm1 = cterm_of thy @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} val assm2 = cterm_of thy @{prop "((P::nat\<Rightarrow>bool) t)"} val Pt_implies_Qt = assume assm1 |> forall_elim (cterm_of thy @{term "t::nat"}); val Qt = implies_elim Pt_implies_Qt (assume assm2);in Qt |> implies_intr assm2 |> implies_intr assm1end*}text {* For how the functions @{text "assume"}, @{text "forall_elim"} and so on work see \ichcite{sec:thms}. (FIXME correct name)*}section {* Tactical Reasoning *}text {* The goal-oriented tactical style is similar to the @{text apply} style at the user level. Reasoning is centered around a \emph{goal}, which is modified in a sequence of proof steps until it is solved. A goal (or goal state) is a special @{ML_type thm}, which by convention is an implication of the form: @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"} Since the formula @{term C} could potentially be an implication, there is a @{text "#"} wrapped around it, which prevents that premises are misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow> prop"} is just the identity function and used as a syntactic marker. For more on this goals see \ichcite{sec:tactical-goals}. (FIXME name) Tactics are functions that map a goal state to a (lazy) sequence of successor states, hence the type of a tactic is @{ML_type[display] "thm -> thm Seq.seq"} \begin{readmore} See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy sequences. However one rarly onstructs sequences manually, but uses the predefined tactic combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}). \end{readmore} Note, however, that tactics are expected to behave nicely and leave the final conclusion @{term C} intact (that is only work on the @{text "A\<^isub>i"} representing the subgoals to be proved) with the exception of possibly instantiating schematic variables. To see how tactics work, let us transcribe a simple apply-style proof from the tutorial \cite{isa-tutorial} into ML:*}lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"apply (erule disjE) apply (rule disjI2) apply assumptionapply (rule disjI1)apply assumptiondonetext {* To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"} sets up a goal state for proving @{text goal} under the assumptions @{text assms} with additional variables @{text params} (the variables that are generalised once the goal is proved); @{text "tac"} is a function that returns a tactic (FIXME see non-existing explanation in the imp-manual). *}ML {*let val ctxt = @{context} val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}in Goal.prove ctxt ["P", "Q"] [] goal (fn _ => eresolve_tac [disjE] 1 THEN resolve_tac [disjI2] 1 THEN assume_tac 1 THEN resolve_tac [disjI1] 1 THEN assume_tac 1)end*}text {* An alternative way to transcribe this proof is as follows *}ML {*let val ctxt = @{context} val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}in Goal.prove ctxt ["P", "Q"] [] goal (fn _ => (eresolve_tac [disjE] THEN' resolve_tac [disjI2] THEN' assume_tac THEN' resolve_tac [disjI1] THEN' assume_tac) 1)end*}section {* Storing and Changing Theorems and so on *}end