(*

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

####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.

0         1         2         3         4         5         6         7         8

*)

theory T1_Basics imports Isac.Isac_Knowledge

begin

chapter \<open>Basics on Linux, Isabelle and ISAC\<close>

text \<open>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 course 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.

\<close>

section \<open>Linux\<close>

text \<open>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 note that ISAC is an 

  experimental system and as such usability in authoring 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/Isabelle/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}

  Since paths are long, we abbreviate '/usr/local/Isabelle/' to '~~' below.

\<close>

section \<open>Isabelle terms\<close>

text \<open>The most 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 ~~/src/Pure/term.ML

  ().

  Let us give an example:

\<close>

ML \<open>@{term "a + b * 9"}\<close>

text \<open>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:

\<close>

ML \<open>(*default_print_depth 99;*) @{term "a + b * 9"}; (*default_print_depth 5;*)

\<close>

text \<open>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':

\<close>

ML \<open>

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

  TermC.atom_write_detail @{context} t;

\<close>

text \<open>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:

\<close>

ML \<open>

  val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";

\<close>

text \<open>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.)

\<close>

section \<open>Isabelle theories\<close>

text \<open>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':

\<close>

ML \<open>

  val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";

\<close>

text \<open>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.

\<close>

end