|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Framework}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Framework\isanewline |
|
12 \isakeyword{imports}\ Main\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupchapter{The Isabelle/Isar Framework \label{ch:isar-framework}% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \begin{isamarkuptext}% |
|
26 Isabelle/Isar |
|
27 \cite{Wenzel:1999:TPHOL,Wenzel-PhD,Nipkow-TYPES02,Wenzel-Paulson:2006,Wenzel:2006:Festschrift} |
|
28 is intended as a generic framework for developing formal |
|
29 mathematical documents with full proof checking. Definitions and |
|
30 proofs are organized as theories; an assembly of theory sources may |
|
31 be presented as a printed document; see also |
|
32 \chref{ch:document-prep}. |
|
33 |
|
34 The main objective of Isar is the design of a human-readable |
|
35 structured proof language, which is called the ``primary proof |
|
36 format'' in Isar terminology. Such a primary proof language is |
|
37 somewhere in the middle between the extremes of primitive proof |
|
38 objects and actual natural language. In this respect, Isar is a bit |
|
39 more formalistic than Mizar |
|
40 \cite{Trybulec:1993:MizarFeatures,Rudnicki:1992:MizarOverview,Wiedijk:1999:Mizar}, |
|
41 using logical symbols for certain reasoning schemes where Mizar |
|
42 would prefer English words; see \cite{Wenzel-Wiedijk:2002} for |
|
43 further comparisons of these systems. |
|
44 |
|
45 So Isar challenges the traditional way of recording informal proofs |
|
46 in mathematical prose, as well as the common tendency to see fully |
|
47 formal proofs directly as objects of some logical calculus (e.g.\ |
|
48 \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-terms in a version of type theory). In fact, Isar is |
|
49 better understood as an interpreter of a simple block-structured |
|
50 language for describing data flow of local facts and goals, |
|
51 interspersed with occasional invocations of proof methods. |
|
52 Everything is reduced to logical inferences internally, but these |
|
53 steps are somewhat marginal compared to the overall bookkeeping of |
|
54 the interpretation process. Thanks to careful design of the syntax |
|
55 and semantics of Isar language elements, a formal record of Isar |
|
56 instructions may later appear as an intelligible text to the |
|
57 attentive reader. |
|
58 |
|
59 The Isar proof language has emerged from careful analysis of some |
|
60 inherent virtues of the existing logical framework of Isabelle/Pure |
|
61 \cite{paulson-found,paulson700}, notably composition of higher-order |
|
62 natural deduction rules, which is a generalization of Gentzen's |
|
63 original calculus \cite{Gentzen:1935}. The approach of generic |
|
64 inference systems in Pure is continued by Isar towards actual proof |
|
65 texts. |
|
66 |
|
67 Concrete applications require another intermediate layer: an |
|
68 object-logic. Isabelle/HOL \cite{isa-tutorial} (simply-typed |
|
69 set-theory) is being used most of the time; Isabelle/ZF |
|
70 \cite{isabelle-ZF} is less extensively developed, although it would |
|
71 probably fit better for classical mathematics.% |
|
72 \end{isamarkuptext}% |
|
73 \isamarkuptrue% |
|
74 % |
|
75 \isadelimtheory |
|
76 % |
|
77 \endisadelimtheory |
|
78 % |
|
79 \isatagtheory |
|
80 \isacommand{end}\isamarkupfalse% |
|
81 % |
|
82 \endisatagtheory |
|
83 {\isafoldtheory}% |
|
84 % |
|
85 \isadelimtheory |
|
86 % |
|
87 \endisadelimtheory |
|
88 \isanewline |
|
89 \end{isabellebody}% |
|
90 %%% Local Variables: |
|
91 %%% mode: latex |
|
92 %%% TeX-master: "root" |
|
93 %%% End: |