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

src/Doc/Isar_Ref/Preface.thy

author | wenzelm |

Mon Oct 09 21:12:22 2017 +0200 (23 months ago) | |

changeset 66822 | 4642cf4a7ebb |

parent 63531 | 847eefdca90d |

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

tuned signature;

1 (*:maxLineLen=78:*)

3 theory Preface

4 imports Main Base

5 begin

7 text \<open>

8 The \<^emph>\<open>Isabelle\<close> system essentially provides a generic

9 infrastructure for building deductive systems (programmed in

10 Standard ML), with a special focus on interactive theorem proving in

11 higher-order logics. Many years ago, even end-users would refer to

12 certain ML functions (goal commands, tactics, tacticals etc.) to

13 pursue their everyday theorem proving tasks.

15 In contrast \<^emph>\<open>Isar\<close> provides an interpreted language environment

16 of its own, which has been specifically tailored for the needs of

17 theory and proof development. Compared to raw ML, the Isabelle/Isar

18 top-level provides a more robust and comfortable development

19 platform, with proper support for theory development graphs, managed

20 transactions with unlimited undo etc.

22 In its pioneering times, the Isabelle/Isar version of the

23 \<^emph>\<open>Proof~General\<close> user interface @{cite proofgeneral and

24 "Aspinall:TACAS:2000"} has contributed to the

25 success of for interactive theory and proof development in this

26 advanced theorem proving environment, even though it was somewhat

27 biased towards old-style proof scripts. The more recent

28 Isabelle/jEdit Prover IDE @{cite "Wenzel:2012"} emphasizes the

29 document-oriented approach of Isabelle/Isar again more explicitly.

31 \<^medskip>

32 Apart from the technical advances over bare-bones ML

33 programming, the main purpose of the Isar language is to provide a

34 conceptually different view on machine-checked proofs

35 @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}. \<^emph>\<open>Isar\<close> stands for

36 \<^emph>\<open>Intelligible semi-automated reasoning\<close>. Drawing from both the

37 traditions of informal mathematical proof texts and high-level

38 programming languages, Isar offers a versatile environment for

39 structured formal proof documents. Thus properly written Isar

40 proofs become accessible to a broader audience than unstructured

41 tactic scripts (which typically only provide operational information

42 for the machine). Writing human-readable proof texts certainly

43 requires some additional efforts by the writer to achieve a good

44 presentation, both of formal and informal parts of the text. On the

45 other hand, human-readable formal texts gain some value in their own

46 right, independently of the mechanic proof-checking process.

48 Despite its grand design of structured proof texts, Isar is able to

49 assimilate the old tactical style as an ``improper'' sub-language.

50 This provides an easy upgrade path for existing tactic scripts, as

51 well as some means for interactive experimentation and debugging of

52 structured proofs. Isabelle/Isar supports a broad range of proof

53 styles, both readable and unreadable ones.

55 \<^medskip>

56 The generic Isabelle/Isar framework (see

57 \chref{ch:isar-framework}) works reasonably well for any Isabelle

58 object-logic that conforms to the natural deduction view of the

59 Isabelle/Pure framework. Specific language elements introduced by

60 Isabelle/HOL are described in \partref{part:hol}. Although the main

61 language elements are already provided by the Isabelle/Pure

62 framework, examples given in the generic parts will usually refer to

63 Isabelle/HOL.

65 \<^medskip>

66 Isar commands may be either \<^emph>\<open>proper\<close> document

67 constructors, or \<^emph>\<open>improper commands\<close>. Some proof methods and

68 attributes introduced later are classified as improper as well.

69 Improper Isar language elements, which are marked by ``\<open>\<^sup>*\<close>'' in the subsequent chapters; they are often helpful

70 when developing proof documents, but their use is discouraged for

71 the final human-readable outcome. Typical examples are diagnostic

72 commands that print terms or theorems according to the current

73 context; other commands emulate old-style tactical theorem proving.

74 \<close>

76 end