1 
1 
2 \chapter{Basic Concepts}\label{ch:basics} 
2 %FIXME 
3 
3 %\chapter{Basic Concepts}\label{ch:basics} 
4 \section{Isabelle/Isar theories} 
4 %\section{The Isar proof language} 
5 

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

7 \begin{enumerate} 

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

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

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

11 semiautomated reasoning. Instead of putting together unreadable tactic 

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

13 to mathematical practice. 

14 \end{enumerate} 

15 

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

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

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

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

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

21 the representing sets. 

22 

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

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

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

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

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

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

29 they have any idea of the Isar proof language. 

30 

31 \begin{warn} 

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

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

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

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

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

37 \end{warn} 

38 

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

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

41 emerging Isabelle/Isar document. 

42 

43 

44 \section{The Isar proof language} 

45 

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

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

48 

49 \subsection{Commands} 

50 

51 \subsubsection{Isar primitives} 

52 

53 \subsubsection{Derived elements} 

54 

55 

56 \subsection{Methods} 

57 

58 \subsection{Attributes} 

59 
5 
60 %%% Local Variables: 
6 %%% Local Variables: 
61 %%% mode: latex 
7 %%% mode: latex 
62 %%% TeXmaster: "isarref" 
8 %%% TeXmaster: "isarref" 
63 %%% End: 
9 %%% End: 