(*

/usr/local/isabisac/bin/isabelle jedit -l Isac T1_Basics.thy &

*)

theory T1_Basics imports Isac begin

chapter {* Basics on Linux, Isabelle and ISAC *}

text {*This is an Isabelle/Isar theory, that means: in between the text there are parts which 

  can be evaluated by the theorem prover Isabelle if installed properly.

  The goal of the sequence beginning with this theory is to give a quick introduction to

  authoring the mathematics knowledge for the math assistant ISAC www.ist.tugraz.at/projects/isac.

  The course is self-contained for mathematics teachers, and probably for interested students.

*}

section {* Linux *}

text {* Isabelle is a computer theorem prover (CTP) under ongoing development. This

  development is done using Linux. However, now Isabelle supports cygwin and thus also can

  be run on Microsoft Windows.

  ISAC uses Isabelle as 'logical operating system'. You get both, ISAC and Isabelle

  installed into cygwin on an USB-stick at the beginning of the course.

  Authoring mathematics knowledge for ISAC (for instance, extending) requires basics

  in handling Linux (cygwin is Linux-like). Please notethat ISAC is an experimental system 

  and as such usability has not yet been considered.

  Having started cygwin you see a prompt '$' at the beginning of a line

  where you can input commands ('#' is the begin of a comment not interpreted by cygwin),

  for instance:

  \begin{itemize}

  \item $ cd /usr/local/Isabelle             # changes to directory of Isabelle

  \item $ ls -l                              # lists all files and subdirectories

  \item $ cd test/Tools/isac/ADDTESTS/course # go on to start the course

  \item $ /usr/local/isabisac/bin/isabelle jedit -l Isac T1_Basics.thy &

  \item $                                    # starts the first exercise

  \end{itemize}

  The arguments required for starting the first exercise tell about the underlying technology:

  \begin{itemize}

  \item $ \emph{jedit} is the editor to be used. jEdit www.jedit.org will be introduced to 

          Isabelle users within the next few years (so we are front-of-the-wave ;-).

  \item $ \emph{-l Isac} loads all functionality and knowledge of ISAC

  \item $ \emph{T1_Basics.thy} is the file name of the first exercise

  \item $ \emph{&} allows to use the same command line for further commands.

  \end{itemize}

  Furhter useful Linus commands are:

  \begin{itemize}

  \item $ TODO      # 

  \end{itemize}

*}

section {* Isabelle terms *}

text {* One basic kind of data required for mathematics are terms. ISAC uses Isabelle's terms.

  In order to allow for 'symbolic computation' terms require representation in an 

  appropriate data structure, which is defined at [ISABELLE_HOME]/src/Pure/term.ML.

  Let us give an example:

*}

ML {* @{term "a + b * 9"}*}

text {* In the 'Output' window below you see what the above command produces, the internal

  representation of "a + b * 3". The '...' indicate that some details are still hidden;

  further details are received this way:

*}

ML {* print_depth 99;

  @{term "a + b * 9"}

*}

text {* The internal representation is too comprehensive for several kinds of inspection.

  Thus ISAC provides additional features, as we see below. First let us store the term

  in a variable 't':

*}

ML {* 

  val t = @{term "a + b * 9"};

  atomwy t;

*}

text {* Please, observe that in this case (whenever 'writeln' is involved, even invisibly)

  the output of 'atomwy t' is placed on top of the 'Output' window.

  Presently, ISAC uses a slightly different representation for terms (which soon will disappear),

  which does not encode numerals as binary numbers:

*}

ML {* val SOME t = parse (theory "Isac") "a + b * 3";

  atomwy (term_of t);

*}

text {* From the above we see: the internal representation of a term contains all the 

  knowledge it is built from, see

  http://isabelle.in.tum.de/dist/library/HOL/Groups.html for the definitions

  \begin{itemize}

  \item plus  :: "'a => 'a => 'a"  (infixl "+" 65)

  \item times :: "'a => 'a => 'a"  (infixl "*" 70)

  \end{itemize}

  together with relevant theorems about + and *.

  In the near future you will just click in order to get the requested knowledge. (The

  present experimental state of Isabelle/jEdit already shows the signature of the function

  under the cursor, if kept on place for a second.)

*}

section {* Isabelle theories *}

text {* As just mentioned, (almost) all the math knowledge used in a theorem prover is

  explicitly defined (and not built into the code like in a CAS). The knowledge is

  organised in \emph{theories}.

  Without these theories Isabelle cannot do any thing, it even does not understand '+' or '*'.

  For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is 

  defined ('=' etc), but not yet '+' and '*', so you get 'NONE':

*}

ML {*  parse (theory "HOL") "a + b * 3";

*}

text {* ISAC uses comparatively few definitions and theorems from Isabelle, see 

  \begin{itemize}

  \item http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html

  \end{itemize}

  We call this the dimension of 'deductive knowledge'.

  \bigskip However, ISAC provides two additional dimensions of knowledge, 'application

  oriented knowledge' (simply called \emph{problems}) and 'algorithmic knowledge' 

  (simply called \emph{methods}); See

  \begin{itemize}

  \item problems http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html

  \item methods http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html

  \end{itemize}

  \bigskip The three dimensions of knowledge together provide all what a 

  \emph{mechanized math assistant} like ISAC requires for autonomously solving problems.

  So, in ISAC too, is (almost) nothing built into the program code, rather, all

  is up to authoring.

  This coures intends to provide basic knowledge for authoring new examples in ISAC.

*}

end