2 /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy &
3 ####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.
7 theory T1_Basics imports Isac.Isac_Knowledge
10 chapter \<open>Basics on Linux, Isabelle and ISAC\<close>
12 text \<open>This is an Isabelle/Isar theory, that means: in between the text there
13 are parts which can be evaluated by the theorem prover Isabelle, if installed
16 The goal of the course beginning with this theory is to give a quick
17 introduction to authoring the mathematics knowledge for the math assistant
18 ISAC www.ist.tugraz.at/projects/isac.
20 The course is self-contained for mathematics teachers, and probably for
24 section \<open>Linux\<close>
25 text \<open>Isabelle is a computer theorem prover (CTP) under ongoing development.
26 This development is done using Linux. However, now Isabelle supports cygwin
27 and thus also can be run on Microsoft Windows.
29 ISAC uses Isabelle as 'logical operating system'. You get both, ISAC and
30 Isabelle installed into cygwin on an USB-stick at the beginning of the course.
32 Authoring mathematics knowledge for ISAC (for instance, extending) requires
33 basics in handling Linux (cygwin is Linux-like). Please note that ISAC is an
34 experimental system and as such usability in authoring has not yet been considered.
36 Having started cygwin you see a prompt '$' at the beginning of a line where
37 you can input commands ('#' is the begin of a comment not interpreted by
38 cygwin), for instance:
40 \item $ cd /usr/local/Isabelle # changes to directory of Isabelle
41 \item $ ls -l # lists all files and subdirectories
42 \item $ cd test/Tools/isac/ADDTESTS/course # go on to start the course
43 \item $ /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy &
44 \item $ # starts the first exercise
47 The arguments required for starting the first exercise tell about the
48 underlying technology:
50 \item $ \emph{jedit} is the editor to be used. jEdit www.jedit.org will be introduced to
51 Isabelle-users within the next few years (so we are front-of-the-wave ;-).
52 \item $ \emph{-l Isac} loads all functionality and knowledge of ISAC
53 \item $ \emph{T1_Basics.thy} is the file name of the first exercise
54 \item $ \emph{&} allows to use the same command line for further commands.
57 Since paths are long, we abbreviate '/usr/local/Isabelle/' to '~~' below.
60 section \<open>Isabelle terms\<close>
61 text \<open>The most basic kind of data required for mathematics are terms.
62 ISAC uses Isabelle's terms.
63 In order to allow for 'symbolic computation' terms require representation in
64 an appropriate data structure, which is defined at ~~/src/Pure/term.ML
67 Let us give an example:
69 ML \<open>@{term "a + b * 9"}\<close>
71 text \<open>In the 'Output' window below you see what the above command produces,
72 the internal representation of "a + b * 3". The '...' indicate that some
73 details are still hidden; further details are received this way:
75 ML \<open>(*default_print_depth 99;*) @{term "a + b * 9"}; (*default_print_depth 5;*)
77 text \<open>The internal representation is too comprehensive for several kinds of
78 inspection. Thus ISAC provides additional features, as we see below. First
79 let us store the term in a variable 't':
82 val t = @{term "a + b * 9"};
83 TermC.atom_write_detail @{context} t;
85 text \<open>Please, observe that in this case (whenever 'writeln' is involved, even
86 invisibly) the output of 'atomwy t' is placed on top of the 'Output' window.
88 Presently, ISAC uses a slightly different representation for terms (which soon
89 will disappear), which does not encode numerals as binary numbers:
92 val t = ParseC.parse_test (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
94 text \<open>From the above we see: the internal representation of a term contains
95 all the knowledge it is built from, see
96 http://isabelle.in.tum.de/dist/library/HOL/Groups.html for the definitions
98 \item plus :: "'a => 'a => 'a" (infixl "+" 65)
99 \item times :: "'a => 'a => 'a" (infixl "*" 70)
101 together with relevant theorems about + and *.
103 In the near future you will just click in order to get the requested knowledge.
104 (The present experimental state of Isabelle/jEdit already shows the signature
105 of the function under the cursor, if kept on place for a second.)
108 section \<open>Isabelle theories\<close>
109 text \<open>As just mentioned, (almost) all the math knowledge used in a theorem
110 prover is explicitly defined (and not built into the code like in a CAS). The
111 knowledge is organised in \emph{theories}.
113 Without these theories Isabelle cannot do any thing, it even does not understand '+' or '*'.
114 For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is
115 defined ('=' etc), but not yet '+' and '*', so you get 'NONE':
118 val t = ParseC.parse_test (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
120 text \<open>ISAC uses comparatively few definitions and theorems from Isabelle, see
122 \item http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html
124 We call this the dimension of 'deductive knowledge'.
126 \bigskip However, ISAC provides two additional dimensions of knowledge, 'application
127 oriented knowledge' (simply called \emph{problems}) and 'algorithmic knowledge'
128 (simply called \emph{methods}); See
130 \item problems http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html
131 \item methods http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html
134 \bigskip The three dimensions of knowledge together provide all what a
135 \emph{mechanized math assistant} like ISAC requires for autonomously solving problems.
136 So, in ISAC too, is (almost) nothing built into the program code, rather, all
139 This coures intends to provide basic knowledge for authoring new examples in ISAC.