summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/basics.tex

author | wenzelm |

Thu Oct 21 17:42:21 1999 +0200 (1999-10-21) | |

changeset 7895 | 7c492d8bc8e3 |

parent 7466 | 7df66ce6508a |

child 7981 | 5120a2a15d06 |

permissions | -rw-r--r-- |

updated;

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

4 \section{Isabelle/Isar theories}

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

7 \begin{enumerate}

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

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

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

11 semi-automated 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}

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

17 sub-language. 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 non-emptiness of

21 the representing sets.

23 New-style 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{isabelle-ref}. 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.

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}

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.

44 \section{The Isar proof language}

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

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

49 \subsection{Commands}

51 \subsubsection{Isar primitives}

53 \subsubsection{Derived elements}

56 \subsection{Methods}

58 \subsection{Attributes}

60 %%% Local Variables:

61 %%% mode: latex

62 %%% TeX-master: "isar-ref"

63 %%% End: