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