29755
|
1 |
theory Isar
|
|
2 |
imports Base
|
|
3 |
begin
|
20472
|
4 |
|
29759
|
5 |
chapter {* Isar language elements *}
|
|
6 |
|
39842
|
7 |
text {* The Isar proof language (see also
|
|
8 |
\cite[\S2]{isabelle-isar-ref}) consists of three main categories of
|
29759
|
9 |
language elements:
|
|
10 |
|
|
11 |
\begin{enumerate}
|
|
12 |
|
39842
|
13 |
\item Proof \emph{commands} define the primary language of
|
|
14 |
transactions of the underlying Isar/VM interpreter. Typical
|
|
15 |
examples are @{command "fix"}, @{command "assume"}, @{command
|
|
16 |
"show"}, and @{command "by"}.
|
|
17 |
|
|
18 |
Composing proof commands according to the rules of the Isar/VM
|
|
19 |
essentially leads to expressions of structured proof text, such that
|
|
20 |
both the machine and the human reader can give it a meaning as
|
|
21 |
formal reasoning.
|
20472
|
22 |
|
39842
|
23 |
\item Proof \emph{methods} define a secondary language of mixed
|
|
24 |
forward-backward refinement steps involving facts and goals.
|
|
25 |
Typical example methods are @{method rule}, @{method unfold}, or
|
|
26 |
@{text simp}. %FIXME proper formal markup!?
|
29759
|
27 |
|
39842
|
28 |
Methods can occur in certain well-defined parts of the Isar proof
|
|
29 |
language, say as arguments to @{command "proof"}, @{command "qed"},
|
|
30 |
or @{command "by"}.
|
|
31 |
|
|
32 |
\item \emph{Attributes} define a tertiary language of small
|
|
33 |
annotations to facts: facts being defined or referenced may always
|
|
34 |
be decorated with attribute expressions. Attributes can modify both
|
|
35 |
the fact and the context.
|
|
36 |
|
|
37 |
Typical example attributes are @{attribute intro} (which affects the
|
|
38 |
context), or @{attribute symmetric} (which affects the fact).
|
29759
|
39 |
|
|
40 |
\end{enumerate}
|
|
41 |
*}
|
|
42 |
|
|
43 |
|
|
44 |
section {* Proof commands *}
|
20520
|
45 |
|
39842
|
46 |
text {* In principle, Isar proof commands could be defined in
|
|
47 |
user-space as well. The system is built like that in the first
|
|
48 |
place: part of the commands are primitive, the other part is defined
|
|
49 |
as derived elements. Adding to the genuine structured proof
|
|
50 |
language requires profound understanding of the Isar/VM machinery,
|
|
51 |
though, so this is far beyond the scope of this manual.
|
|
52 |
|
|
53 |
What can be done realistically is to define some diagnostic commands
|
|
54 |
that merely inspect the general state of the Isar/VM, and report
|
|
55 |
some feedback to the user. Typically this involves checking of the
|
|
56 |
linguistic \emph{mode} of a proof state, or peeking at the pending
|
|
57 |
goals (if available).
|
|
58 |
*}
|
|
59 |
|
|
60 |
text %mlref {*
|
|
61 |
\begin{mldecls}
|
|
62 |
@{index_ML_type Proof.state} \\
|
|
63 |
@{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\
|
|
64 |
@{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\
|
|
65 |
@{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\
|
|
66 |
@{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\
|
|
67 |
@{index_ML Proof.goal: "Proof.state ->
|
|
68 |
{context: Proof.context, facts: thm list, goal: thm}"} \\
|
|
69 |
@{index_ML Proof.raw_goal: "Proof.state ->
|
|
70 |
{context: Proof.context, facts: thm list, goal: thm}"} \\
|
|
71 |
\end{mldecls}
|
|
72 |
|
|
73 |
\begin{description}
|
|
74 |
|
|
75 |
\item @{ML_type Proof.state} represents Isar proof states. This is
|
|
76 |
a block-structured configuration with proof context, linguistic
|
|
77 |
mode, and optional goal state. An Isar goal consists of goal
|
|
78 |
context, goal facts (``@{text "using"}''), and tactical goal state
|
|
79 |
(see \secref{sec:tactical-goals}).
|
|
80 |
|
|
81 |
The general idea is that the facts shall contribute to the
|
|
82 |
refinement of the goal state --- how exactly is defined by the proof
|
|
83 |
method that is applied in that situation.
|
|
84 |
|
|
85 |
\item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML
|
|
86 |
Proof.assert_backward} are partial identity functions that fail
|
|
87 |
unless a certain linguistic mode is active, namely ``@{text
|
|
88 |
"proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text
|
|
89 |
"proof(prove)"}'', respectively (using the terminology of
|
|
90 |
\cite{isabelle-isar-ref}).
|
|
91 |
|
|
92 |
It is advisable study the implementations of existing proof commands
|
|
93 |
for suitable modes to be asserted.
|
|
94 |
|
|
95 |
\item @{ML Proof.simple_goal}~@{text "state"} returns the structured
|
|
96 |
Isar goal (if available) in the form seen by ``simple'' methods
|
|
97 |
(like @{text simp} or @{text blast}). The Isar goal facts are
|
|
98 |
already inserted as premises into the subgoals, which are presented
|
|
99 |
separately as in @{ML Proof.goal}.
|
|
100 |
|
|
101 |
\item @{ML Proof.goal}~@{text "state"} returns the structured Isar
|
|
102 |
goal (if available) in the form seen by regular methods (like
|
|
103 |
@{method rule}). The auxiliary internal encoding of Pure
|
|
104 |
conjunctions is split into individual subgoals as usual.
|
|
105 |
|
|
106 |
\item @{ML Proof.raw_goal}~@{text "state"} returns the structured
|
|
107 |
Isar goal (if available) in the raw internal form seen by ``raw''
|
|
108 |
methods (like @{text induct}). This form is very rarely appropriate
|
|
109 |
for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal}
|
|
110 |
should be used in most situations.
|
|
111 |
|
|
112 |
\end{description}
|
|
113 |
*}
|
|
114 |
|
20520
|
115 |
|
|
116 |
|
20472
|
117 |
section {* Proof methods *}
|
|
118 |
|
|
119 |
text FIXME
|
|
120 |
|
29759
|
121 |
|
20472
|
122 |
section {* Attributes *}
|
|
123 |
|
29759
|
124 |
text FIXME
|
30272
|
125 |
|
20472
|
126 |
end
|