
neuper@38067: (*
neuper@38077: /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy &
neuper@38077: ####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.
neuper@38077: 0         1         2         3         4         5         6         7         8
neuper@38067: *)
neuper@38067: 
wneuper@59592: theory T1_Basics imports Isac.Isac_Knowledge
wneuper@59460: begin
neuper@38067: 
wneuper@59472: chapter \<open>Basics on Linux, Isabelle and ISAC\<close>
neuper@38067: 
wneuper@59472: text \<open>This is an Isabelle/Isar theory, that means: in between the text there 
neuper@38077:   are parts which can be evaluated by the theorem prover Isabelle, if installed 
neuper@38077:   properly.
neuper@38067: 
neuper@38077:   The goal of the course beginning with this theory is to give a quick 
neuper@38077:   introduction to authoring the mathematics knowledge for the math assistant 
neuper@38077:   ISAC www.ist.tugraz.at/projects/isac.
neuper@38067: 
neuper@38077:   The course is self-contained for mathematics teachers, and probably for 
neuper@38077:   interested students.
wneuper@59472: \<close>
neuper@38067: 
wneuper@59472: section \<open>Linux\<close>
wneuper@59472: text \<open>Isabelle is a computer theorem prover (CTP) under ongoing development. 
neuper@38077:   This development is done using Linux. However, now Isabelle supports cygwin 
neuper@38077:   and thus also can be run on Microsoft Windows.
neuper@38067: 
neuper@38077:   ISAC uses Isabelle as 'logical operating system'. You get both, ISAC and 
neuper@38077:   Isabelle installed into cygwin on an USB-stick at the beginning of the course.
neuper@38067: 
neuper@38077:   Authoring mathematics knowledge for ISAC (for instance, extending) requires 
neuper@38077:   basics in handling Linux (cygwin is Linux-like). Please note that ISAC is an 
neuper@38077:   experimental system and as such usability in authoring has not yet been considered.
neuper@38067: 
neuper@38077:   Having started cygwin you see a prompt '$' at the beginning of a line where 
neuper@38077:   you can input commands ('#' is the begin of a comment not interpreted by 
neuper@38077:   cygwin), for instance:
neuper@38067:   \begin{itemize}
neuper@38067:   \item $ cd /usr/local/Isabelle             # changes to directory of Isabelle
neuper@38067:   \item $ ls -l                              # lists all files and subdirectories
neuper@38067:   \item $ cd test/Tools/isac/ADDTESTS/course # go on to start the course
neuper@38077:   \item $ /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy &
neuper@38067:   \item $                                    # starts the first exercise
neuper@38067:   \end{itemize}
neuper@38067: 
neuper@38077:   The arguments required for starting the first exercise tell about the 
neuper@38077:   underlying technology:
neuper@38067:   \begin{itemize}
neuper@38067:   \item $ \emph{jedit} is the editor to be used. jEdit www.jedit.org will be introduced to 
neuper@38077:           Isabelle-users within the next few years (so we are front-of-the-wave ;-).
neuper@38067:   \item $ \emph{-l Isac} loads all functionality and knowledge of ISAC
neuper@38067:   \item $ \emph{T1_Basics.thy} is the file name of the first exercise
neuper@38067:   \item $ \emph{&} allows to use the same command line for further commands.
neuper@38067:   \end{itemize}
neuper@38067: 
neuper@38077:   Since paths are long, we abbreviate '/usr/local/Isabelle/' to '~~' below.
wneuper@59472: \<close>
neuper@38067: 
wneuper@59472: section \<open>Isabelle terms\<close>
wneuper@59472: text \<open>The most basic kind of data required for mathematics are terms. 
neuper@38077:   ISAC uses Isabelle's terms.
neuper@38077:   In order to allow for 'symbolic computation' terms require representation in 
neuper@38077:   an  appropriate data structure, which is defined at ~~/src/Pure/term.ML
neuper@38077:   ().
neuper@38067: 
neuper@38067:   Let us give an example:
wneuper@59472: \<close>
wneuper@59472: ML \<open>@{term "a + b * 9"}\<close>
neuper@38067: 
wneuper@59472: text \<open>In the 'Output' window below you see what the above command produces, 
neuper@38077:   the internal representation of "a + b * 3". The '...' indicate that some 
neuper@38077:   details are still hidden; further details are received this way:
wneuper@59472: \<close>
wneuper@59472: ML \<open>(*default_print_depth 99;*) @{term "a + b * 9"}; (*default_print_depth 5;*)
wneuper@59472: \<close>
wneuper@59472: text \<open>The internal representation is too comprehensive for several kinds of 
neuper@38077:   inspection. Thus ISAC provides additional features, as we see below. First 
neuper@38077:   let us store the term in a variable 't':
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@38067:   val t = @{term "a + b * 9"};
Walther@60650:   TermC.atom_write_detail @{context} t;
wneuper@59472: \<close>
wneuper@59472: text \<open>Please, observe that in this case (whenever 'writeln' is involved, even 
neuper@38077:   invisibly) the output of 'atomwy t' is placed on top of the 'Output' window.
neuper@38067: 
neuper@38077:   Presently, ISAC uses a slightly different representation for terms (which soon
neuper@38077:   will disappear), which does not encode numerals as binary numbers:
wneuper@59472: \<close>
Walther@60424: ML \<open>
Walther@60424:   val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
wneuper@59472: \<close>
wneuper@59472: text \<open>From the above we see: the internal representation of a term contains 
neuper@38077:   all the knowledge it is built from, see
neuper@38067:   http://isabelle.in.tum.de/dist/library/HOL/Groups.html for the definitions
neuper@38067:   \begin{itemize}
neuper@38067:   \item plus  :: "'a => 'a => 'a"  (infixl "+" 65)
neuper@38067:   \item times :: "'a => 'a => 'a"  (infixl "*" 70)
neuper@38067:   \end{itemize}
neuper@38067:   together with relevant theorems about + and *.
neuper@38067:   
neuper@38077:   In the near future you will just click in order to get the requested knowledge.
neuper@38077:   (The present experimental state of Isabelle/jEdit already shows the signature 
neuper@38077:   of the function under the cursor, if kept on place for a second.)
wneuper@59472: \<close>
neuper@38067: 
wneuper@59472: section \<open>Isabelle theories\<close>
wneuper@59472: text \<open>As just mentioned, (almost) all the math knowledge used in a theorem 
neuper@38077:   prover is explicitly defined (and not built into the code like in a CAS). The 
neuper@38077:   knowledge is organised in \emph{theories}.
neuper@38067: 
neuper@38067:   Without these theories Isabelle cannot do any thing, it even does not understand '+' or '*'.
neuper@38067:   For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is 
neuper@38067:   defined ('=' etc), but not yet '+' and '*', so you get 'NONE':
wneuper@59472: \<close>
Walther@60424: ML \<open>
Walther@60424:   val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
wneuper@59472: \<close>
wneuper@59472: text \<open>ISAC uses comparatively few definitions and theorems from Isabelle, see 
neuper@38067:   \begin{itemize}
neuper@38067:   \item http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html
neuper@38067:   \end{itemize}
neuper@38067:   We call this the dimension of 'deductive knowledge'.
neuper@38067: 
neuper@38067:   \bigskip However, ISAC provides two additional dimensions of knowledge, 'application
neuper@38067:   oriented knowledge' (simply called \emph{problems}) and 'algorithmic knowledge' 
neuper@38067:   (simply called \emph{methods}); See
neuper@38067:   \begin{itemize}
neuper@38067:   \item problems http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html
neuper@38067:   \item methods http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html
neuper@38067:   \end{itemize}
neuper@38067: 
neuper@38067:   \bigskip The three dimensions of knowledge together provide all what a 
neuper@38067:   \emph{mechanized math assistant} like ISAC requires for autonomously solving problems.
neuper@38067:   So, in ISAC too, is (almost) nothing built into the program code, rather, all
neuper@38067:   is up to authoring.
neuper@38067: 
neuper@38067:   This coures intends to provide basic knowledge for authoring new examples in ISAC.
wneuper@59472: \<close>
neuper@38067: end




