wenzelm@7046

1 

wenzelm@7297

2 
\chapter{Basic Concepts}\label{ch:basics}

wenzelm@7297

3 

wenzelm@7895

4 
\section{Isabelle/Isar theories}

wenzelm@7895

5 

wenzelm@7297

6 
Isabelle/Isar offers two main improvements over classic Isabelle:

wenzelm@7297

7 
\begin{enumerate}

wenzelm@7466

8 
\item A new \emph{theory format}, occasionally referred to as ``newstyle

wenzelm@7895

9 
theories'', supporting interactive development and unlimited undo operation.

wenzelm@7895

10 
\item A \emph{formal proof document language} designed to support intelligible

wenzelm@7895

11 
semiautomated reasoning. Instead of putting together unreadable tactic

wenzelm@7895

12 
scripts, the author is enabled to express the reasoning in way that is close

wenzelm@7895

13 
to mathematical practice.

wenzelm@7297

14 
\end{enumerate}

wenzelm@7046

15 

wenzelm@7297

16 
The Isar proof language is embedded into the new theory format as a proper

wenzelm@7297

17 
sublanguage. Proof mode is entered by stating some $\THEOREMNAME$ or

wenzelm@7895

18 
$\LEMMANAME$ at the theory level, and left again with the final conclusion

wenzelm@7895

19 
(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as

wenzelm@7466

20 
well, such as the HOL $\isarkeyword{typedef}$ which demands nonemptiness of

wenzelm@7466

21 
the representing sets.

wenzelm@7297

22 

wenzelm@7297

23 
Newstyle theory files may still be associated with an ML file consisting of

wenzelm@7315

24 
plain old tactic scripts. There is no longer any ML binding generated for the

wenzelm@7466

25 
theory and theorems, though. ML functions \texttt{theory}, \texttt{thm}, and

wenzelm@7466

26 
\texttt{thms} retrieve this information \cite{isabelleref}. Nevertheless,

wenzelm@7466

27 
migration between classic Isabelle and Isabelle/Isar is relatively easy. Thus

wenzelm@7466

28 
users may start to benefit from interactive theory development even before

wenzelm@7466

29 
they have any idea of the Isar proof language.

wenzelm@7315

30 

wenzelm@7315

31 
\begin{warn}

wenzelm@7466

32 
Currently Proof~General does \emph{not} support mixed interactive

wenzelm@7895

33 
development of classic Isabelle theory files and tactic scripts, together

wenzelm@7466

34 
with Isar documents at the same time. The ``\texttt{isa}'' and

wenzelm@7466

35 
``\texttt{isar}'' versions of Proof~General are handled as two different

wenzelm@7895

36 
theorem proving systems, only one of these may be active.

wenzelm@7315

37 
\end{warn}

wenzelm@7297

38 

wenzelm@7466

39 
Porting of existing tactic scripts is best done by running two separate

wenzelm@7466

40 
Proof~General sessions, one for replaying the old script and the other for the

wenzelm@7466

41 
emerging Isabelle/Isar document.

wenzelm@7466

42 

wenzelm@7046

43 

wenzelm@7046

44 
\section{The Isar proof language}

wenzelm@7046

45 

wenzelm@7466

46 
Sorry, this important section has not been written yet! Refer to

wenzelm@7297

47 
\cite{Wenzel:1999:TPHOL} for the time being.

wenzelm@7297

48 

wenzelm@7297

49 
\subsection{Commands}

wenzelm@7297

50 

wenzelm@7297

51 
\subsubsection{Isar primitives}

wenzelm@7297

52 

wenzelm@7297

53 
\subsubsection{Derived elements}

wenzelm@7297

54 

wenzelm@7135

55 

wenzelm@7135

56 
\subsection{Methods}

wenzelm@7046

57 

wenzelm@7046

58 
\subsection{Attributes}

wenzelm@7046

59 

wenzelm@7046

60 
%%% Local Variables:

wenzelm@7046

61 
%%% mode: latex

wenzelm@7046

62 
%%% TeXmaster: "isarref"

wenzelm@7046

63 
%%% End:
