theory FirstSteps

imports Main

uses "antiquote_setup.ML"

begin

(*<*)

ML {*

local structure O = ThyOutput

in

  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.

*}

ML {*

  val _ = warning (makestring 1)

*}

text {*

  However this only works if the type of what is printed is monomorphic and not 

  a function.

*}

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). 

  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 

  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

  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}

  definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.

  \end{readmore}

  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

  \end{exercise}

  Consider for example

*}

text {*

  While antiquotations are very convenient for constructing terms, they can

*}

ML {*

  let

  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 

*}

text {*

*}

text {*

  @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 

*}

text {*

  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 "+"} 

  \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

  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

*}

  lemma 

   assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 

   and     assm\<^isub>2: "P t"

text {*

  application. This combinator, and several variants are defined in

*}

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 assm1

end

*}

text {*

*}

section {* Tactical Reasoning *}

text {*

  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)"}

  @{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. 

  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

  \end{readmore}

*}

lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"

apply (erule disjE)

 apply (rule disjI2)

 apply assumption

apply (rule disjI1)

apply assumption

done

text {*

  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

*}

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 _ =>