wenzelm@7046

1 

wenzelm@7297

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

wenzelm@7297

3 

wenzelm@7297

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

wenzelm@7297

5 
\begin{enumerate}

wenzelm@7297

6 
\item A new \emph{theory format}, often referred to as ``newstyle theories'',

wenzelm@7315

7 
supporting interactive development and unlimited undo operation.

wenzelm@7315

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

wenzelm@7315

9 
semiautomated reasoning. Rather than putting together tactic scripts, the

wenzelm@7315

10 
author is enabled to express the reasoning in way that is close to

wenzelm@7315

11 
mathematical practice.

wenzelm@7297

12 
\end{enumerate}

wenzelm@7046

13 

wenzelm@7297

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

wenzelm@7297

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

wenzelm@7315

16 
$\LEMMANAME$ at the theory levels, and left with the final end of proof (e.g.\

wenzelm@7315

17 
via $\QEDNAME$). Some theory extension mechanisms require proof as well, such

wenzelm@7315

18 
as the HOL $\isarkeyword{typedef}$ mechanism that only works for nonempty

wenzelm@7315

19 
representing sets.

wenzelm@7297

20 

wenzelm@7297

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

wenzelm@7315

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

wenzelm@7315

23 
theory and theorems, though. Functions \texttt{theory}, \texttt{thm}, and

wenzelm@7315

24 
\texttt{thms} may be used to retrieve this information from ML (see also

wenzelm@7315

25 
\cite{isabelleref}). Nevertheless, migration between classic Isabelle and

wenzelm@7315

26 
Isabelle/Isar is relatively easy. Thus users may start to benefit from

wenzelm@7315

27 
interactive theory development even before they have any idea of the Isar

wenzelm@7315

28 
proof language.

wenzelm@7315

29 

wenzelm@7315

30 
\begin{warn}

wenzelm@7315

31 
Proof~General does \emph{not} support mixed interactive development of

wenzelm@7315

32 
classic Isabelle theory files and tactic scripts together with Isar

wenzelm@7315

33 
documents at the same time. The \texttt{isa} and \texttt{isar} versions of

wenzelm@7315

34 
Proof~General appear as two different theorem proving systems; only one

wenzelm@7315

35 
prover may be active at any time.

wenzelm@7315

36 
\end{warn}

wenzelm@7297

37 

wenzelm@7046

38 

wenzelm@7046

39 
\section{The Isar proof language}

wenzelm@7046

40 

wenzelm@7297

41 
This rather important section has not been written yet! Refer to

wenzelm@7297

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

wenzelm@7297

43 

wenzelm@7297

44 
\subsection{Commands}

wenzelm@7297

45 

wenzelm@7297

46 
\subsubsection{Isar primitives}

wenzelm@7297

47 

wenzelm@7297

48 
\subsubsection{Derived elements}

wenzelm@7297

49 

wenzelm@7135

50 

wenzelm@7135

51 
\subsection{Methods}

wenzelm@7046

52 

wenzelm@7046

53 
\subsection{Attributes}

wenzelm@7046

54 

wenzelm@7046

55 

wenzelm@7046

56 
%%% Local Variables:

wenzelm@7046

57 
%%% mode: latex

wenzelm@7046

58 
%%% TeXmaster: "isarref"

wenzelm@7046

59 
%%% End:
