theory Advanced

imports Base First_Steps

begin

chapter \<open>Advanced Isabelle\label{chp:advanced}\<close>

text \<open>

   \begin{flushright}

  {\em All things are difficult before they are easy.} \\[1ex]

  proverb\\[2ex]

  {\em Programming is not just an act of telling a computer what 

  to do: it is also an act of telling other programmers what you 

  wished the computer to do. Both are important, and the latter 

  deserves care.}\\[1ex]

  ---Andrew Morton, Linux Kernel mailinglist, 13 March 2012

  \end{flushright}

  \medskip

  While terms, types and theorems are the most basic data structures in

  Isabelle, there are a number of layers built on top of them. Most of these

  layers are concerned with storing and manipulating data. Handling them

  properly is an essential skill for programming on the ML-level of Isabelle. 

  The most basic layer are theories. They contain global data and

  can be seen as the ``long-term memory'' of Isabelle. There is usually only

  one theory active at each moment. Proof contexts and local theories, on the

  other hand, store local data for a task at hand. They act like the

  ``short-term memory'' and there can be many of them that are active in

  parallel.

\<close>

section \<open>Theories\label{sec:theories}\<close>

text \<open>

  Theories, as said above, are the most basic layer of abstraction in

  Isabelle. They record information about definitions, syntax declarations, axioms,

  theorems and much more.  For example, if a definition is made, it

  must be stored in a theory in order to be usable later on. Similar

  with proofs: once a proof is finished, the proved theorem needs to

  be stored in the theorem database of the theory in order to be

  usable. All relevant data of a theory can be queried with the

  Isabelle command \isacommand{print\_theory}.

  \begin{isabelle}

  \isacommand{print\_theory}\\

  \<open>> names: Pure Code_Generator HOL \<dots>\<close>\\

  \<open>> classes: Inf < type \<dots>\<close>\\

  \<open>> default sort: type\<close>\\

  \<open>> syntactic types: #prop \<dots>\<close>\\

  \<open>> logical types: 'a \<times> 'b \<dots>\<close>\\

  \<open>> type arities: * :: (random, random) random \<dots>\<close>\\

  \<open>> logical constants: == :: 'a \<Rightarrow> 'a \<Rightarrow> prop \<dots>\<close>\\

  \<open>> abbreviations: \<dots>\<close>\\

  \<open>> axioms: \<dots>\<close>\\

  \<open>> oracles: \<dots>\<close>\\

  \<open>> definitions: \<dots>\<close>\\

  \<open>> theorems: \<dots>\<close>

  \end{isabelle}

  Functions acting on theories often end with the suffix \<open>_global\<close>,

  for example the function @{ML read_term_global in Syntax} in the structure

  @{ML_structure Syntax}. The reason is to set them syntactically apart from

  functions acting on contexts or local theories, which will be discussed in

  the next sections. There is a tendency amongst Isabelle developers to prefer

  ``non-global'' operations, because they have some advantages, as we will also

  discuss later. However, some basic understanding of theories is still necessary

  for effective Isabelle programming.

  An important Isabelle command with theories is \isacommand{setup}. In the

  previous chapters we used it already to make a theorem attribute known

  to Isabelle and to register a theorem under a name. What happens behind the

  scenes is that \isacommand{setup} expects a function of type @{ML_type

  "theory -> theory"}: the input theory is the current theory and the output

  the theory where the attribute has been registered or the theorem has been

  stored.  This is a fundamental principle in Isabelle. A similar situation

  arises with declaring a constant, which can be done on the ML-level with 

  function @{ML_ind declare_const in Sign} from the structure @{ML_structure

  Sign}. To see how \isacommand{setup} works, consider the following code:

\<close>  

ML %grayML\<open>let

  val thy = @{theory}

  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)

in 

  Sign.declare_const @{context} bar_const thy  

end\<close>

text \<open>

  If you simply run this code\footnote{Recall that ML-code needs to be enclosed in

  \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>.} with the

  intention of declaring a constant \<open>BAR\<close> having type @{typ nat}, then 

  indeed you obtain a theory as result. But if you query the

  constant on the Isabelle level using the command \isacommand{term}

  \begin{isabelle}

  \isacommand{term}~\<open>BAR\<close>\\

  \<open>> "BAR" :: "'a"\<close>

  \end{isabelle}

  you can see that you do \emph{not} obtain the expected constant of type @{typ nat}, but a free 

  variable (printed in blue) of polymorphic type. The problem is that the 

  ML-expression above did not ``register'' the declaration with the current theory. 

  This is what the command \isacommand{setup} is for. The constant is properly 

  declared with

\<close>

setup %gray \<open>fn thy => 

let

  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)

  val (_, thy') = Sign.declare_const @{context} bar_const thy

in 

  thy'

end\<close>

text \<open>

  where the declaration is actually applied to the current theory and

  \begin{isabelle}

  \isacommand{term}~@{text [quotes] "BAR"}\\

  \<open>> "BAR" :: "nat"\<close>

  \end{isabelle}

  now returns a (black) constant with the type @{typ nat}, as expected.

  In a sense, \isacommand{setup} can be seen as a transaction that

  takes the current theory \<open>thy\<close>, applies an operation, and

  produces a new current theory \<open>thy'\<close>. This means that we have

  to be careful to apply operations always to the most current theory,

  not to a \emph{stale} one. Consider again the function inside the

  \isacommand{setup}-command:

  \begin{isabelle}

  \begin{graybox}

  \isacommand{setup}~\<open>\<verbopen>\<close> @{ML \<open>fn thy => 

let

  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)

  val (_, thy') = Sign.declare_const @{context} bar_const thy

in

  thy

end\<close>}~\<open>\<verbclose>\<close>\isanewline

  \<open>> ERROR: "Stale theory encountered"\<close>

  \end{graybox}

  \end{isabelle}

  This time we erroneously return the original theory \<open>thy\<close>, instead of

  the modified one \<open>thy'\<close>. Such buggy code will always result into 

  a runtime error message about stale theories.

  \begin{readmore}

  Most of the functions about theories are implemented in

  @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}.

  \end{readmore}

\<close>

section \<open>Contexts\<close>

text \<open>

  Contexts are arguably more important than theories, even though they only 

  contain ``short-term memory data''. The reason is that a vast number of

  functions in Isabelle depend in one way or another on contexts. Even such

  mundane operations like printing out a term make essential use of contexts.

  For this consider the following contrived proof-snippet whose purpose is to 

  fix two variables:

\<close>

lemma "True"

proof -

  ML_prf \<open>Variable.dest_fixes @{context}\<close> 

  fix x y  

  ML_prf \<open>Variable.dest_fixes @{context}\<close>(*<*)oops(*>*)

text \<open>

  The interesting point is that we injected ML-code before and after

  the variables are fixed. For this remember that ML-code inside a proof

  needs to be enclosed inside \isacommand{ML\_prf}~\<open>\<verbopen> \<dots> \<verbclose>\<close>,

  not \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>. The function 

  @{ML_ind dest_fixes in Variable} from the structure @{ML_structure Variable} takes 

  a context and returns all its currently fixed variable (names). That 

  means a context has a dataslot containing information about fixed variables.

  The ML-antiquotation \<open>@{context}\<close> points to the context that is

  active at that point of the theory. Consequently, in the first call to 

  @{ML dest_fixes in Variable} this dataslot is  empty; in the second it is 

  filled with \<open>x\<close> and \<open>y\<close>. What is interesting is that contexts

  can be stacked. For this consider the following proof fragment:

\<close>

lemma "True"

proof -

  fix x y

  { fix z w

    ML_prf \<open>Variable.dest_fixes @{context}\<close> 

  }

  ML_prf \<open>Variable.dest_fixes @{context}\<close>(*<*)oops(*>*)

text \<open>

  Here the first time we call @{ML dest_fixes in Variable} we have four fixes variables;

  the second time we get only the fixes variables \<open>x\<close> and \<open>y\<close> as answer, since

  \<open>z\<close> and \<open>w\<close> are not anymore in the scope of the context. 

  This means the curly-braces act on the Isabelle level as opening and closing statements 

  for a context. The above proof fragment corresponds roughly to the following ML-code

\<close>

ML %grayML\<open>val ctxt0 = @{context};

val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0;

val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1\<close>

text \<open>

  where the function @{ML_ind add_fixes in Variable} fixes a list of variables

  specified by strings. Let us come back to the point about printing terms. Consider

  printing out the term \mbox{\<open>(x, y, z, w)\<close>} using our function @{ML_ind pretty_term}.

  This function takes a term and a context as argument. Notice how the printing

  of the term changes according to which context is used.

  \begin{isabelle}

  \begin{graybox}

  @{ML \<open>let

  val trm = @{term "(x, y, z, w)"}

in

  pwriteln (Pretty.chunks 

    [ pretty_term ctxt0 trm,

      pretty_term ctxt1 trm,

      pretty_term ctxt2 trm ])

end\<close>}\\

  \setlength{\fboxsep}{0mm}

  \<open>>\<close>~\<open>(\<close>\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}\<open>,\<close>~%

  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}\<open>,\<close>~%

  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>z\<close>}}\<open>,\<close>~%

  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>w\<close>}}\<open>)\<close>\\

  \<open>>\<close>~\<open>(\<close>\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}\<open>,\<close>~%

  \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}\<open>,\<close>~%

  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>z\<close>}}\<open>,\<close>~%

  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>w\<close>}}\<open>)\<close>\\

  \<open>>\<close>~\<open>(\<close>\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}\<open>,\<close>~%

  \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}\<open>,\<close>~%

  \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{\<open>z\<close>}}\<open>,\<close>~%

  \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{\<open>w\<close>}}\<open>)\<close>

  \end{graybox}

  \end{isabelle}

  The term we are printing is in all three cases the same---a tuple containing

  four free variables. As you can see, however, in case of @{ML \<open>ctxt0\<close>} all

  variables are highlighted indicating a problem, while in case of @{ML \<open>ctxt1\<close>} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free

  variables, but not \<open>z\<close> and \<open>w\<close>. In the last case all variables

  are printed as expected. The point of this example is that the context

  contains the information which variables are fixed, and designates all other

  free variables as being alien or faulty.  Therefore the highlighting. 

  While this seems like a minor detail, the concept of making the context aware 

  of fixed variables is actually quite useful. For example it prevents us from 

  fixing a variable twice

  \<open>@{context}

|> Variable.add_fixes ["x", "x"]\<close> 

  More importantly it also allows us to easily create fresh names for

  fixed variables.  For this you have to use the function @{ML_ind

  variant_fixes in Variable} from the structure @{ML_structure Variable}.

  \<open>@{context}

|> Variable.variant_fixes ["y", "y", "z"]\<close> 

  Now a fresh variant for the second occurence of \<open>y\<close> is created

  avoiding any clash. In this way we can also create fresh free variables

  that avoid any clashes with fixed variables. In Line~3 below we fix

  the variable \<open>x\<close> in the context \<open>ctxt1\<close>. Next we want to

  create two fresh variables of type @{typ nat} as variants of the

  string @{text [quotes] "x"} (Lines 6 and 7).

  \<open>let

  val ctxt0 = @{context}

  val (_, ctxt1) = Variable.add_fixes ["x"] ctxt0

  val frees = replicate 2 ("x", @{typ nat})

in

  (Variable.variant_frees ctxt0 [] frees,

   Variable.variant_frees ctxt1 [] frees)

end\<close>

  As you can see, if we create the fresh variables with the context \<open>ctxt0\<close>,

  then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>

  and \<open>xb\<close> avoiding \<open>x\<close>, which was fixed in this context.

  Often one has the problem that given some terms, create fresh variables

  avoiding any variable occurring in those terms. For this you can use the

  function @{ML_ind declare_term in Variable} from the structure @{ML_structure Variable}.

  \<open>let

  val ctxt1 = Variable.declare_term @{term "(x, xa)"} @{context}

  val frees = replicate 2 ("x", @{typ nat})

in

  Variable.variant_frees ctxt1 [] frees

end\<close>

  The result is \<open>xb\<close> and \<open>xc\<close> for the names of the fresh

  variables, since \<open>x\<close> and \<open>xa\<close> occur in the term we declared. 

  Note that @{ML_ind declare_term in Variable} does not fix the

  variables; it just makes them ``known'' to the context. You can see

  that if you print out a declared term.

  \begin{isabelle}

  \begin{graybox}

  @{ML \<open>let

  val trm = @{term "P x y z"}

  val ctxt1 = Variable.declare_term trm @{context}

in

  pwriteln (pretty_term ctxt1 trm)

end\<close>}\\

  \setlength{\fboxsep}{0mm}

  \<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%

  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}~%

  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}~%

  \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>z\<close>}}

  \end{graybox}

  \end{isabelle}

  All variables are highligted, indicating that they are not

  fixed. However, declaring a term is helpful when parsing terms using

  the function @{ML_ind read_term in Syntax} from the structure

  @{ML_structure Syntax}. Consider the following code:

  \<open>let

  val ctxt0 = @{context}

  val ctxt1 = Variable.declare_term @{term "x::nat"} ctxt0

in

  (Syntax.read_term ctxt0 "x", 

   Syntax.read_term ctxt1 "x") 

end\<close>

  \<open>(Free ("x", "'a"), Free ("x", "nat"))\<close>}

  Parsing the string in the context \<open>ctxt0\<close> results in a free variable 

  with a default polymorphic type, but in case of \<open>ctxt1\<close> we obtain a

  free variable of type @{typ nat} as previously declared. Which

  type the parsed term receives depends upon the last declaration that

  is made, as the next example illustrates.

  \<open>let

  val ctxt1 = Variable.declare_term @{term "x::nat"} @{context}

  val ctxt2 = Variable.declare_term @{term "x::int"} ctxt1

in

  (Syntax.read_term ctxt1 "x", 

   Syntax.read_term ctxt2 "x") 

end\<close>

  \<open>(Free ("x", "nat"), Free ("x", "int"))\<close>}

  The most useful feature of contexts is that one can export, or transfer, 

  terms and theorems between them. We show this first for terms. 

  \begin{isabelle}

  \begin{graybox}

  \begin{linenos}

  @{ML \<open>let

  val ctxt0 = @{context}

  val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 

  val foo_trm = @{term "P x y z"}

in

  singleton (Variable.export_terms ctxt1 ctxt0) foo_trm

  |> pretty_term ctxt0

  |> pwriteln

end\<close>}

  \end{linenos}

  \setlength{\fboxsep}{0mm}

  \<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%

  \<open>?x ?y ?z\<close>

  \end{graybox}

  \end{isabelle}

  In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in

  context \<open>ctxt1\<close>.  The function @{ML_ind export_terms in

  Variable} from the structure @{ML_structure Variable} can be used to transfer

  terms between contexts. Transferring means to turn all (free)

  variables that are fixed in one context, but not in the other, into

  schematic variables. In our example, we are transferring the term

  \<open>P x y z\<close> from context \<open>ctxt1\<close> to \<open>ctxt0\<close>,

  which means @{term x}, @{term y} and @{term z} become schematic

  variables (as can be seen by the leading question marks in the result). 

  Note that the variable \<open>P\<close> stays a free variable, since it not fixed in

  \<open>ctxt1\<close>; it is even highlighed, because \<open>ctxt0\<close> does

  not know about it. Note also that in Line 6 we had to use the

  function @{ML_ind singleton}, because the function @{ML_ind

  export_terms in Variable} normally works over lists of terms.

  The case of transferring theorems is even more useful. The reason is

  that the generalisation of fixed variables to schematic variables is

  not trivial if done manually. For illustration purposes we use in the 

  following code the function @{ML_ind make_thm in Skip_Proof} from the 

  structure @{ML_structure Skip_Proof}. This function will turn an arbitray 

  term, in our case @{term "P x y z x y z"}, into a theorem (disregarding 

  whether it is actually provable).

  \<open>let

  val thy = @{theory}

  val ctxt0 = @{context}

  val (_, ctxt1) = Variable.add_fixes ["P", "x", "y", "z"] ctxt0 

  val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z x y z"}

in

  singleton (Proof_Context.export ctxt1 ctxt0) foo_thm

end\<close>

  \<open>?P ?x ?y ?z ?x ?y ?z\<close>}

  Since we fixed all variables in \<open>ctxt1\<close>, in the exported

  result all of them are schematic. The great point of contexts is

  that exporting from one to another is not just restricted to

  variables, but also works with assumptions. For this we can use the

  function @{ML_ind export in Assumption} from the structure

  @{ML_structure Assumption}. Consider the following code.

  \<open>let

  val ctxt0 = @{context}

  val ([eq], ctxt1) = Assumption.add_assumes [@{cprop "x \<equiv> y"}] ctxt0

  val eq' = Thm.symmetric eq

in

  Assumption.export false ctxt1 ctxt0 eq'

end\<close>

  \<open>x \<equiv> y \<Longrightarrow> y \<equiv> x\<close>}

  The function @{ML_ind add_assumes in Assumption} from the structure

  @{ML_structure Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}

  to the context \<open>ctxt1\<close> (Line 3). This function expects a list

  of @{ML_type cterm}s and returns them as theorems, together with the

  new context in which they are ``assumed''. In Line 4 we use the

  function @{ML_ind symmetric in Thm} from the structure @{ML_structure

  Thm} in order to obtain the symmetric version of the assumed

  meta-equality. Now exporting the theorem \<open>eq'\<close> from \<open>ctxt1\<close> to \<open>ctxt0\<close> means @{term "y \<equiv> x"} will be prefixed with

  the assumed theorem. The boolean flag in @{ML_ind export in

  Assumption} indicates whether the assumptions should be marked with

  the goal marker (see Section~\ref{sec:basictactics}). In normal

  circumstances this is not necessary and so should be set to @{ML

  false}.  The result of the export is then the theorem \mbox{@{term

  "x \<equiv> y \<Longrightarrow> y \<equiv> x"}}.  As can be seen this is an easy way for obtaing

  simple theorems. We will explain this in more detail in

  Section~\ref{sec:structured}.

  The function @{ML_ind export in Proof_Context} from the structure 

  @{ML_structure Proof_Context} combines both export functions from 

  @{ML_structure Variable} and @{ML_structure Assumption}. This can be seen

  in the following example.

  \<open>let

  val ctxt0 = @{context}

  val ((fvs, [eq]), ctxt1) = ctxt0

    |> Variable.add_fixes ["x", "y"]

    ||>> Assumption.add_assumes [@{cprop "x \<equiv> y"}]

  val eq' = Thm.symmetric eq

in

  Proof_Context.export ctxt1 ctxt0 [eq']

end\<close>

\<close>

text \<open>

\<close>

(*

ML %grayML{*Proof_Context.debug := true*}

ML %grayML{*Proof_Context.verbose := true*}

*)

(*

lemma "True"

proof -