author | haftmann |
Sat, 18 Feb 2012 20:53:39 +0100 | |
changeset 46525 | af3df09590f9 |
parent 46265 | b6ab3cdea163 |
permissions | -rw-r--r-- |
30296 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Proof}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Proof\isanewline |
|
12 |
\isakeyword{imports}\ Base\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Structured proofs% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\isamarkupsection{Variables \label{sec:variables}% |
|
26 |
} |
|
27 |
\isamarkuptrue% |
|
28 |
% |
|
29 |
\begin{isamarkuptext}% |
|
40406 | 30 |
Any variable that is not explicitly bound by \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-abstraction |
30296 | 31 |
is considered as ``free''. Logically, free variables act like |
40406 | 32 |
outermost universal quantification at the sequent level: \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}} means that the result |
30296 | 33 |
holds \emph{for all} values of \isa{x}. Free variables for |
40406 | 34 |
terms (not types) can be fully internalized into the logic: \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}} and \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}} are interchangeable, provided |
30296 | 35 |
that \isa{x} does not occur elsewhere in the context. |
40406 | 36 |
Inspecting \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}} more closely, we see that inside the |
30296 | 37 |
quantifier, \isa{x} is essentially ``arbitrary, but fixed'', |
38 |
while from outside it appears as a place-holder for instantiation |
|
40406 | 39 |
(thanks to \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} elimination). |
30296 | 40 |
|
41 |
The Pure logic represents the idea of variables being either inside |
|
42 |
or outside the current scope by providing separate syntactic |
|
43 |
categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\ |
|
40406 | 44 |
\emph{schematic variables} (e.g.\ \isa{{\isaliteral{3F}{\isacharquery}}x}). Incidently, a |
45 |
universal result \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}} has the HHF normal form \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{29}{\isacharparenright}}}, which represents its generality without requiring an |
|
35001 | 46 |
explicit quantifier. The same principle works for type variables: |
40406 | 47 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}} represents the idea of ``\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2E}{\isachardot}}\ B{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}}'' |
35001 | 48 |
without demanding a truly polymorphic framework. |
30296 | 49 |
|
50 |
\medskip Additional care is required to treat type variables in a |
|
51 |
way that facilitates type-inference. In principle, term variables |
|
52 |
depend on type variables, which means that type variables would have |
|
53 |
to be declared first. For example, a raw type-theoretic framework |
|
54 |
would demand the context to be constructed in stages as follows: |
|
40406 | 55 |
\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{3A}{\isacharcolon}}\ type{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}}. |
30296 | 56 |
|
57 |
We allow a slightly less formalistic mode of operation: term |
|
58 |
variables \isa{x} are fixed without specifying a type yet |
|
59 |
(essentially \emph{all} potential occurrences of some instance |
|
40406 | 60 |
\isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} are fixed); the first occurrence of \isa{x} |
30296 | 61 |
within a specific term assigns its most general type, which is then |
62 |
maintained consistently in the context. The above example becomes |
|
40406 | 63 |
\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{3A}{\isacharcolon}}\ term{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{3A}{\isacharcolon}}\ type{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}}, where type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} is fixed \emph{after} term \isa{x}, and the constraint |
64 |
\isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}} is an implicit consequence of the occurrence of |
|
65 |
\isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}} in the subsequent proposition. |
|
30296 | 66 |
|
67 |
This twist of dependencies is also accommodated by the reverse |
|
68 |
operation of exporting results from a context: a type variable |
|
40406 | 69 |
\isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} is considered fixed as long as it occurs in some fixed |
70 |
term variable of the context. For example, exporting \isa{x{\isaliteral{3A}{\isacharcolon}}\ term{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{3A}{\isacharcolon}}\ type\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}} produces in the first step \isa{x{\isaliteral{3A}{\isacharcolon}}\ term\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}} for fixed \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, and only in the second step |
|
71 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}} for schematic \isa{{\isaliteral{3F}{\isacharquery}}x} and \isa{{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
72 |
The following Isar source text illustrates this scenario.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
73 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
74 |
\isamarkuptrue% |
40964 | 75 |
\isacommand{notepad}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
76 |
\isanewline |
40964 | 77 |
\isakeyword{begin}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
78 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
79 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
80 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
81 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
82 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
83 |
\isatagproof |
40406 | 84 |
\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
85 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
86 |
\ \ \ \ \isacommand{fix}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
87 |
\ x\ \ % |
40406 | 88 |
\isamarkupcmt{all potential occurrences of some \isa{x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{5C3C7461753E}{\isasymtau}}} are fixed% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
89 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
90 |
\isanewline |
40406 | 91 |
\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
92 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
93 |
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse% |
40406 | 94 |
\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
95 |
\isamarkupcmt{implicit type assigment by concrete occurrence% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
96 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
97 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
98 |
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
40406 | 99 |
\ {\isaliteral{28}{\isacharparenleft}}rule\ reflexive{\isaliteral{29}{\isacharparenright}}\isanewline |
100 |
\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
101 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
102 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
103 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
104 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
105 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
106 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
107 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
108 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
109 |
\ \ \ \ \isacommand{thm}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
110 |
\ this\ \ % |
40406 | 111 |
\isamarkupcmt{result still with fixed type \isa{{\isaliteral{27}{\isacharprime}}a}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
112 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
113 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
114 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
115 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
116 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
117 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
118 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
119 |
\isatagproof |
40406 | 120 |
\isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
121 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
122 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
123 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
124 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
125 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
126 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
127 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
128 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
129 |
\ \ \isacommand{thm}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
130 |
\ this\ \ % |
40406 | 131 |
\isamarkupcmt{fully general result for arbitrary \isa{{\isaliteral{3F}{\isacharquery}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{27}{\isacharprime}}a}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
132 |
} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
133 |
\isanewline |
40964 | 134 |
\isacommand{end}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
135 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
136 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
137 |
The Isabelle/Isar proof context manages the details of term |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
138 |
vs.\ type variables, with high-level principles for moving the |
30296 | 139 |
frontier between fixed and schematic variables. |
140 |
||
40406 | 141 |
The \isa{add{\isaliteral{5F}{\isacharunderscore}}fixes} operation explictly declares fixed |
142 |
variables; the \isa{declare{\isaliteral{5F}{\isacharunderscore}}term} operation absorbs a term into |
|
30296 | 143 |
a context by fixing new type variables and adding syntactic |
144 |
constraints. |
|
145 |
||
146 |
The \isa{export} operation is able to perform the main work of |
|
147 |
generalizing term and type variables as sketched above, assuming |
|
148 |
that fixing variables and terms have been declared properly. |
|
149 |
||
150 |
There \isa{import} operation makes a generalized fact a genuine |
|
151 |
part of the context, by inventing fixed variables for the schematic |
|
152 |
ones. The effect can be reversed by using \isa{export} later, |
|
153 |
potentially with an extended context; the result is equivalent to |
|
154 |
the original modulo renaming of schematic variables. |
|
155 |
||
156 |
The \isa{focus} operation provides a variant of \isa{import} |
|
40406 | 157 |
for nested propositions (with explicit quantification): \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{2E}{\isachardot}}\ B{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} is |
158 |
decomposed by inventing fixed variables \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n} for the body.% |
|
30296 | 159 |
\end{isamarkuptext}% |
160 |
\isamarkuptrue% |
|
161 |
% |
|
162 |
\isadelimmlref |
|
163 |
% |
|
164 |
\endisadelimmlref |
|
165 |
% |
|
166 |
\isatagmlref |
|
167 |
% |
|
168 |
\begin{isamarkuptext}% |
|
169 |
\begin{mldecls} |
|
170 |
\indexdef{}{ML}{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline% |
|
171 |
\verb| string list -> Proof.context -> string list * Proof.context| \\ |
|
172 |
\indexdef{}{ML}{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline% |
|
173 |
\verb| string list -> Proof.context -> string list * Proof.context| \\ |
|
174 |
\indexdef{}{ML}{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\ |
|
175 |
\indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\ |
|
176 |
\indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ |
|
177 |
\indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ |
|
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30296
diff
changeset
|
178 |
\indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline% |
32302 | 179 |
\verb| (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\ |
42509 | 180 |
\indexdef{}{ML}{Variable.focus}\verb|Variable.focus: term -> Proof.context ->|\isasep\isanewline% |
181 |
\verb| ((string * (string * typ)) list * term) * Proof.context| \\ |
|
30296 | 182 |
\end{mldecls} |
183 |
||
184 |
\begin{description} |
|
185 |
||
186 |
\item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term |
|
187 |
variables \isa{xs}, returning the resulting internal names. By |
|
188 |
default, the internal representation coincides with the external |
|
189 |
one, which also means that the given variables must not be fixed |
|
190 |
already. There is a different policy within a local proof body: the |
|
191 |
given names are just hints for newly invented Skolem variables. |
|
192 |
||
193 |
\item \verb|Variable.variant_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given |
|
194 |
names. |
|
195 |
||
196 |
\item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term |
|
197 |
\isa{t} to belong to the context. This automatically fixes new |
|
198 |
type variables, but not term variables. Syntactic constraints for |
|
199 |
type and term variables are declared uniformly, though. |
|
200 |
||
201 |
\item \verb|Variable.declare_constraints|~\isa{t\ ctxt} declares |
|
202 |
syntactic constraints from term \isa{t}, without making it part |
|
203 |
of the context yet. |
|
204 |
||
205 |
\item \verb|Variable.export|~\isa{inner\ outer\ thms} generalizes |
|
206 |
fixed type and term variables in \isa{thms} according to the |
|
207 |
difference of the \isa{inner} and \isa{outer} context, |
|
208 |
following the principles sketched above. |
|
209 |
||
210 |
\item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type |
|
211 |
variables in \isa{ts} as far as possible, even those occurring |
|
212 |
in fixed term variables. The default policy of type-inference is to |
|
213 |
fix newly introduced type variables, which is essentially reversed |
|
214 |
with \verb|Variable.polymorphic|: here the given terms are detached |
|
215 |
from the context as far as possible. |
|
216 |
||
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents:
30296
diff
changeset
|
217 |
\item \verb|Variable.import|~\isa{open\ thms\ ctxt} invents fixed |
30296 | 218 |
type and term variables for the schematic ones occurring in \isa{thms}. The \isa{open} flag indicates whether the fixed names |
219 |
should be accessible to the user, otherwise newly introduced names |
|
220 |
are marked as ``internal'' (\secref{sec:names}). |
|
221 |
||
40406 | 222 |
\item \verb|Variable.focus|~\isa{B} decomposes the outermost \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} prefix of proposition \isa{B}. |
30296 | 223 |
|
224 |
\end{description}% |
|
225 |
\end{isamarkuptext}% |
|
226 |
\isamarkuptrue% |
|
227 |
% |
|
228 |
\endisatagmlref |
|
229 |
{\isafoldmlref}% |
|
230 |
% |
|
231 |
\isadelimmlref |
|
232 |
% |
|
233 |
\endisadelimmlref |
|
234 |
% |
|
35001 | 235 |
\isadelimmlex |
236 |
% |
|
237 |
\endisadelimmlex |
|
238 |
% |
|
239 |
\isatagmlex |
|
240 |
% |
|
241 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
242 |
The following example shows how to work with fixed term |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
243 |
and type parameters and with type-inference.% |
35001 | 244 |
\end{isamarkuptext}% |
245 |
\isamarkuptrue% |
|
246 |
% |
|
247 |
\endisatagmlex |
|
248 |
{\isafoldmlex}% |
|
249 |
% |
|
250 |
\isadelimmlex |
|
251 |
% |
|
252 |
\endisadelimmlex |
|
253 |
% |
|
254 |
\isadelimML |
|
255 |
% |
|
256 |
\endisadelimML |
|
257 |
% |
|
258 |
\isatagML |
|
259 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 260 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
261 |
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}static\ compile{\isaliteral{2D}{\isacharminus}}time\ context\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ for\ testing\ only{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
262 |
\ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ % |
|
35001 | 263 |
\isaantiq |
40406 | 264 |
context{}% |
35001 | 265 |
\endisaantiq |
40406 | 266 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
35001 | 267 |
\isanewline |
40406 | 268 |
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}locally\ fixed\ parameters\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ no\ type\ assignment\ yet{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
269 |
\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ctxt{\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Variable{\isaliteral{2E}{\isachardot}}add{\isaliteral{5F}{\isacharunderscore}}fixes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}y{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 270 |
\isanewline |
40406 | 271 |
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}t{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ most\ general\ fixed\ type{\isaliteral{3B}{\isacharsemicolon}}\ t{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3A}{\isacharcolon}}\ most\ general\ arbitrary\ type{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
272 |
\ \ val\ t{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Syntax{\isaliteral{2E}{\isachardot}}read{\isaliteral{5F}{\isacharunderscore}}term\ ctxt{\isadigit{1}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
273 |
\ \ val\ t{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ singleton\ {\isaliteral{28}{\isacharparenleft}}Variable{\isaliteral{2E}{\isachardot}}polymorphic\ ctxt{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 274 |
\isanewline |
40406 | 275 |
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}term\ u\ enforces\ specific\ type\ assignment{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
276 |
\ \ val\ u\ {\isaliteral{3D}{\isacharequal}}\ Syntax{\isaliteral{2E}{\isachardot}}read{\isaliteral{5F}{\isacharunderscore}}term\ ctxt{\isadigit{1}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ y{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 277 |
\isanewline |
40406 | 278 |
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}official\ declaration\ of\ u\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ propagates\ constraints\ etc{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
279 |
\ \ val\ ctxt{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ ctxt{\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Variable{\isaliteral{2E}{\isachardot}}declare{\isaliteral{5F}{\isacharunderscore}}term\ u{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
280 |
\ \ val\ t{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ Syntax{\isaliteral{2E}{\isachardot}}read{\isaliteral{5F}{\isacharunderscore}}term\ ctxt{\isadigit{2}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat\ is\ enforced{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
281 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
35001 | 282 |
\endisatagML |
283 |
{\isafoldML}% |
|
284 |
% |
|
285 |
\isadelimML |
|
286 |
% |
|
287 |
\endisadelimML |
|
288 |
% |
|
289 |
\begin{isamarkuptext}% |
|
40126 | 290 |
In the above example, the starting context is derived from the |
291 |
toplevel theory, which means that fixed variables are internalized |
|
40153 | 292 |
literally: \isa{x} is mapped again to \isa{x}, and |
40126 | 293 |
attempting to fix it again in the subsequent context is an error. |
294 |
Alternatively, fixed parameters can be renamed explicitly as |
|
295 |
follows:% |
|
35001 | 296 |
\end{isamarkuptext}% |
297 |
\isamarkuptrue% |
|
298 |
% |
|
299 |
\isadelimML |
|
300 |
% |
|
301 |
\endisadelimML |
|
302 |
% |
|
303 |
\isatagML |
|
304 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 305 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
306 |
\ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ % |
|
35001 | 307 |
\isaantiq |
40406 | 308 |
context{}% |
35001 | 309 |
\endisaantiq |
40406 | 310 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
311 |
\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ x{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ x{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
312 |
\ \ \ \ ctxt{\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Variable{\isaliteral{2E}{\isachardot}}variant{\isaliteral{5F}{\isacharunderscore}}fixes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
313 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
35001 | 314 |
\endisatagML |
315 |
{\isafoldML}% |
|
316 |
% |
|
317 |
\isadelimML |
|
318 |
% |
|
319 |
\endisadelimML |
|
320 |
% |
|
321 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
322 |
The following ML code can now work with the invented names of |
40153 | 323 |
\isa{x{\isadigit{1}}}, \isa{x{\isadigit{2}}}, \isa{x{\isadigit{3}}}, without depending on |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
324 |
the details on the system policy for introducing these variants. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
325 |
Recall that within a proof body the system always invents fresh |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
326 |
``skolem constants'', e.g.\ as follows:% |
35001 | 327 |
\end{isamarkuptext}% |
328 |
\isamarkuptrue% |
|
40964 | 329 |
\isacommand{notepad}\isamarkupfalse% |
35001 | 330 |
\isanewline |
40964 | 331 |
\isakeyword{begin}\isanewline |
35001 | 332 |
% |
333 |
\isadelimML |
|
334 |
\ \ % |
|
335 |
\endisadelimML |
|
336 |
% |
|
337 |
\isatagML |
|
40406 | 338 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse% |
339 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
|
340 |
\ \ \ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ % |
|
35001 | 341 |
\isaantiq |
40406 | 342 |
context{}% |
35001 | 343 |
\endisaantiq |
40406 | 344 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
35001 | 345 |
\isanewline |
40406 | 346 |
\ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}x{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ctxt{\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Variable{\isaliteral{2E}{\isachardot}}add{\isaliteral{5F}{\isacharunderscore}}fixes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
347 |
\ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}x{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ctxt{\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Variable{\isaliteral{2E}{\isachardot}}add{\isaliteral{5F}{\isacharunderscore}}fixes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
348 |
\ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}x{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ctxt{\isadigit{2}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Variable{\isaliteral{2E}{\isachardot}}add{\isaliteral{5F}{\isacharunderscore}}fixes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 349 |
\isanewline |
40406 | 350 |
\ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}y{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ y{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
351 |
\ \ \ \ \ \ ctxt{\isadigit{3}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Variable{\isaliteral{2E}{\isachardot}}variant{\isaliteral{5F}{\isacharunderscore}}fixes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}y{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}y{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
352 |
\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline |
|
40964 | 353 |
\isacommand{end}\isamarkupfalse% |
35001 | 354 |
% |
355 |
\endisatagML |
|
356 |
{\isafoldML}% |
|
357 |
% |
|
358 |
\isadelimML |
|
359 |
% |
|
360 |
\endisadelimML |
|
361 |
% |
|
362 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
363 |
In this situation \verb|Variable.add_fixes| and \verb|Variable.variant_fixes| are very similar, but identical name |
35001 | 364 |
proposals given in a row are only accepted by the second version.% |
365 |
\end{isamarkuptext}% |
|
366 |
\isamarkuptrue% |
|
367 |
% |
|
30296 | 368 |
\isamarkupsection{Assumptions \label{sec:assumptions}% |
369 |
} |
|
370 |
\isamarkuptrue% |
|
371 |
% |
|
372 |
\begin{isamarkuptext}% |
|
373 |
An \emph{assumption} is a proposition that it is postulated in the |
|
374 |
current context. Local conclusions may use assumptions as |
|
375 |
additional facts, but this imposes implicit hypotheses that weaken |
|
376 |
the overall statement. |
|
377 |
||
378 |
Assumptions are restricted to fixed non-schematic statements, i.e.\ |
|
379 |
all generality needs to be expressed by explicit quantifiers. |
|
380 |
Nevertheless, the result will be in HHF normal form with outermost |
|
40406 | 381 |
quantifiers stripped. For example, by assuming \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2E}{\isachardot}}\ P\ x} we get \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{3F}{\isacharquery}}x} for schematic \isa{{\isaliteral{3F}{\isacharquery}}x} |
382 |
of fixed type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. Local derivations accumulate more and |
|
383 |
more explicit references to hypotheses: \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B} where \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n} needs to |
|
30296 | 384 |
be covered by the assumptions of the current context. |
385 |
||
40406 | 386 |
\medskip The \isa{add{\isaliteral{5F}{\isacharunderscore}}assms} operation augments the context by |
30296 | 387 |
local assumptions, which are parameterized by an arbitrary \isa{export} rule (see below). |
388 |
||
389 |
The \isa{export} operation moves facts from a (larger) inner |
|
390 |
context into a (smaller) outer context, by discharging the |
|
391 |
difference of the assumptions as specified by the associated export |
|
392 |
rules. Note that the discharged portion is determined by the |
|
35001 | 393 |
difference of contexts, not the facts being exported! There is a |
30296 | 394 |
separate flag to indicate a goal context, where the result is meant |
395 |
to refine an enclosing sub-goal of a structured proof state. |
|
396 |
||
397 |
\medskip The most basic export rule discharges assumptions directly |
|
40406 | 398 |
by means of the \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} introduction rule: |
30296 | 399 |
\[ |
42666 | 400 |
\infer[(\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}} |
30296 | 401 |
\] |
402 |
||
403 |
The variant for goal refinements marks the newly introduced |
|
404 |
premises, which causes the canonical Isar goal refinement scheme to |
|
405 |
enforce unification with local premises within the goal: |
|
406 |
\[ |
|
42666 | 407 |
\infer[(\isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}} |
30296 | 408 |
\] |
409 |
||
410 |
\medskip Alternative versions of assumptions may perform arbitrary |
|
411 |
transformations on export, as long as the corresponding portion of |
|
412 |
hypotheses is removed from the given facts. For example, a local |
|
40406 | 413 |
definition works by fixing \isa{x} and assuming \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}, |
30296 | 414 |
with the following export rule to reverse the effect: |
415 |
\[ |
|
42666 | 416 |
\infer[(\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}expand})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ t}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x}} |
30296 | 417 |
\] |
40406 | 418 |
This works, because the assumption \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} was introduced in |
30296 | 419 |
a context with \isa{x} being fresh, so \isa{x} does not |
40406 | 420 |
occur in \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} here.% |
30296 | 421 |
\end{isamarkuptext}% |
422 |
\isamarkuptrue% |
|
423 |
% |
|
424 |
\isadelimmlref |
|
425 |
% |
|
426 |
\endisadelimmlref |
|
427 |
% |
|
428 |
\isatagmlref |
|
429 |
% |
|
430 |
\begin{isamarkuptext}% |
|
431 |
\begin{mldecls} |
|
432 |
\indexdef{}{ML type}{Assumption.export}\verb|type Assumption.export| \\ |
|
433 |
\indexdef{}{ML}{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\ |
|
434 |
\indexdef{}{ML}{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline% |
|
435 |
\verb| cterm list -> Proof.context -> thm list * Proof.context| \\ |
|
436 |
\indexdef{}{ML}{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline% |
|
437 |
\verb| cterm list -> Proof.context -> thm list * Proof.context| \\ |
|
438 |
\indexdef{}{ML}{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\ |
|
439 |
\end{mldecls} |
|
440 |
||
441 |
\begin{description} |
|
442 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
443 |
\item Type \verb|Assumption.export| represents arbitrary export |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
444 |
rules, which is any function of type \verb|bool -> cterm list|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
445 |
\verb| -> thm -> thm|, where the \verb|bool| indicates goal mode, |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
446 |
and the \verb|cterm list| the collection of assumptions to be |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
447 |
discharged simultaneously. |
30296 | 448 |
|
40406 | 449 |
\item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a primitive assumption \isa{A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A{\isaliteral{27}{\isacharprime}}}, where the |
450 |
conclusion \isa{A{\isaliteral{27}{\isacharprime}}} is in HHF normal form. |
|
30296 | 451 |
|
452 |
\item \verb|Assumption.add_assms|~\isa{r\ As} augments the context |
|
453 |
by assumptions \isa{As} with export rule \isa{r}. The |
|
454 |
resulting facts are hypothetical theorems as produced by the raw |
|
455 |
\verb|Assumption.assume|. |
|
456 |
||
457 |
\item \verb|Assumption.add_assumes|~\isa{As} is a special case of |
|
42666 | 458 |
\verb|Assumption.add_assms| where the export rule performs \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro} or \isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}, depending on goal |
35001 | 459 |
mode. |
30296 | 460 |
|
40406 | 461 |
\item \verb|Assumption.export|~\isa{is{\isaliteral{5F}{\isacharunderscore}}goal\ inner\ outer\ thm} |
30296 | 462 |
exports result \isa{thm} from the the \isa{inner} context |
40406 | 463 |
back into the \isa{outer} one; \isa{is{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ true} means |
30296 | 464 |
this is a goal context. The result is in HHF normal form. Note |
42361 | 465 |
that \verb|Proof_Context.export| combines \verb|Variable.export| |
30296 | 466 |
and \verb|Assumption.export| in the canonical way. |
467 |
||
468 |
\end{description}% |
|
469 |
\end{isamarkuptext}% |
|
470 |
\isamarkuptrue% |
|
471 |
% |
|
472 |
\endisatagmlref |
|
473 |
{\isafoldmlref}% |
|
474 |
% |
|
475 |
\isadelimmlref |
|
476 |
% |
|
477 |
\endisadelimmlref |
|
478 |
% |
|
35001 | 479 |
\isadelimmlex |
480 |
% |
|
481 |
\endisadelimmlex |
|
482 |
% |
|
483 |
\isatagmlex |
|
484 |
% |
|
485 |
\begin{isamarkuptext}% |
|
486 |
The following example demonstrates how rules can be |
|
487 |
derived by building up a context of assumptions first, and exporting |
|
46525 | 488 |
some local fact afterwards. We refer to \isa{Pure} equality |
35001 | 489 |
here for testing purposes.% |
490 |
\end{isamarkuptext}% |
|
491 |
\isamarkuptrue% |
|
492 |
% |
|
493 |
\endisatagmlex |
|
494 |
{\isafoldmlex}% |
|
495 |
% |
|
496 |
\isadelimmlex |
|
497 |
% |
|
498 |
\endisadelimmlex |
|
499 |
% |
|
500 |
\isadelimML |
|
501 |
% |
|
502 |
\endisadelimML |
|
503 |
% |
|
504 |
\isatagML |
|
505 |
\isacommand{ML}\isamarkupfalse% |
|
40406 | 506 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
507 |
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}static\ compile{\isaliteral{2D}{\isacharminus}}time\ context\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ for\ testing\ only{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
508 |
\ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ % |
|
35001 | 509 |
\isaantiq |
40406 | 510 |
context{}% |
35001 | 511 |
\endisaantiq |
40406 | 512 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
35001 | 513 |
\isanewline |
40406 | 514 |
\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}eq{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
515 |
\ \ \ \ ctxt{\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Assumption{\isaliteral{2E}{\isachardot}}add{\isaliteral{5F}{\isacharunderscore}}assumes\ {\isaliteral{5B}{\isacharbrackleft}}% |
|
35001 | 516 |
\isaantiq |
40406 | 517 |
cprop\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ y{\isaliteral{22}{\isachardoublequote}}{}% |
35001 | 518 |
\endisaantiq |
40406 | 519 |
{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
520 |
\ \ val\ eq{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Thm{\isaliteral{2E}{\isachardot}}symmetric\ eq{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
35001 | 521 |
\isanewline |
40406 | 522 |
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}back\ to\ original\ context\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ discharges\ assumption{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
523 |
\ \ val\ r\ {\isaliteral{3D}{\isacharequal}}\ Assumption{\isaliteral{2E}{\isachardot}}export\ false\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ eq{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
524 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
35001 | 525 |
\endisatagML |
526 |
{\isafoldML}% |
|
527 |
% |
|
528 |
\isadelimML |
|
529 |
% |
|
530 |
\endisadelimML |
|
531 |
% |
|
532 |
\begin{isamarkuptext}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
533 |
Note that the variables of the resulting rule are not |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
534 |
generalized. This would have required to fix them properly in the |
42361 | 535 |
context beforehand, and export wrt.\ variables afterwards (cf.\ \verb|Variable.export| or the combined \verb|Proof_Context.export|).% |
35001 | 536 |
\end{isamarkuptext}% |
537 |
\isamarkuptrue% |
|
538 |
% |
|
539 |
\isamarkupsection{Structured goals and results \label{sec:struct-goals}% |
|
30296 | 540 |
} |
541 |
\isamarkuptrue% |
|
542 |
% |
|
543 |
\begin{isamarkuptext}% |
|
544 |
Local results are established by monotonic reasoning from facts |
|
545 |
within a context. This allows common combinations of theorems, |
|
40406 | 546 |
e.g.\ via \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} elimination, resolution rules, or equational |
30296 | 547 |
reasoning, see \secref{sec:thms}. Unaccounted context manipulations |
40406 | 548 |
should be avoided, notably raw \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} introduction or ad-hoc |
30296 | 549 |
references to free variables or assumptions not present in the proof |
550 |
context. |
|
551 |
||
552 |
\medskip The \isa{SUBPROOF} combinator allows to structure a |
|
553 |
tactical proof recursively by decomposing a selected sub-goal: |
|
40406 | 554 |
\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}} is turned into \isa{B{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}} |
555 |
after fixing \isa{x} and assuming \isa{A{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}. This means |
|
30296 | 556 |
the tactic needs to solve the conclusion, but may use the premise as |
557 |
a local fact, for locally fixed variables. |
|
558 |
||
35001 | 559 |
The family of \isa{FOCUS} combinators is similar to \isa{SUBPROOF}, but allows to retain schematic variables and pending |
560 |
subgoals in the resulting goal state. |
|
561 |
||
30296 | 562 |
The \isa{prove} operation provides an interface for structured |
563 |
backwards reasoning under program control, with some explicit sanity |
|
564 |
checks of the result. The goal context can be augmented by |
|
565 |
additional fixed variables (cf.\ \secref{sec:variables}) and |
|
566 |
assumptions (cf.\ \secref{sec:assumptions}), which will be available |
|
567 |
as local facts during the proof and discharged into implications in |
|
568 |
the result. Type and term variables are generalized as usual, |
|
569 |
according to the context. |
|
570 |
||
571 |
The \isa{obtain} operation produces results by eliminating |
|
572 |
existing facts by means of a given tactic. This acts like a dual |
|
573 |
conclusion: the proof demonstrates that the context may be augmented |
|
35001 | 574 |
by parameters and assumptions, without affecting any conclusions |
575 |
that do not mention these parameters. See also |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
576 |
\cite{isabelle-isar-ref} for the user-level \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} and |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
577 |
\hyperlink{command.guess}{\mbox{\isa{\isacommand{guess}}}} elements. Final results, which may not refer to |
30296 | 578 |
the parameters in the conclusion, need to exported explicitly into |
579 |
the original context.% |
|
580 |
\end{isamarkuptext}% |
|
581 |
\isamarkuptrue% |
|
582 |
% |
|
583 |
\isadelimmlref |
|
584 |
% |
|
585 |
\endisadelimmlref |
|
586 |
% |
|
587 |
\isatagmlref |
|
588 |
% |
|
589 |
\begin{isamarkuptext}% |
|
590 |
\begin{mldecls} |
|
46265 | 591 |
\indexdef{}{ML}{SELECT\_GOAL}\verb|SELECT_GOAL: tactic -> int -> tactic| \\ |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
592 |
\indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
593 |
\verb| Proof.context -> int -> tactic| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
594 |
\indexdef{}{ML}{Subgoal.FOCUS}\verb|Subgoal.FOCUS: (Subgoal.focus -> tactic) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
595 |
\verb| Proof.context -> int -> tactic| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
596 |
\indexdef{}{ML}{Subgoal.FOCUS\_PREMS}\verb|Subgoal.FOCUS_PREMS: (Subgoal.focus -> tactic) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
597 |
\verb| Proof.context -> int -> tactic| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
598 |
\indexdef{}{ML}{Subgoal.FOCUS\_PARAMS}\verb|Subgoal.FOCUS_PARAMS: (Subgoal.focus -> tactic) ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
599 |
\verb| Proof.context -> int -> tactic| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
600 |
\indexdef{}{ML}{Subgoal.focus}\verb|Subgoal.focus: Proof.context -> int -> thm -> Subgoal.focus * thm| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
601 |
\indexdef{}{ML}{Subgoal.focus\_prems}\verb|Subgoal.focus_prems: Proof.context -> int -> thm -> Subgoal.focus * thm| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
602 |
\indexdef{}{ML}{Subgoal.focus\_params}\verb|Subgoal.focus_params: Proof.context -> int -> thm -> Subgoal.focus * thm| \\ |
30296 | 603 |
\end{mldecls} |
35001 | 604 |
|
30296 | 605 |
\begin{mldecls} |
606 |
\indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% |
|
607 |
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ |
|
608 |
\indexdef{}{ML}{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline% |
|
609 |
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\ |
|
610 |
\end{mldecls} |
|
611 |
\begin{mldecls} |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
612 |
\indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) -> thm list ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
613 |
\verb| Proof.context -> ((string * cterm) list * thm list) * Proof.context| \\ |
30296 | 614 |
\end{mldecls} |
615 |
||
616 |
\begin{description} |
|
617 |
||
46265 | 618 |
\item \verb|SELECT_GOAL|~\isa{tac\ i} confines a tactic to the |
619 |
specified subgoal \isa{i}. This introduces a nested goal state, |
|
620 |
without decomposing the internal structure of the subgoal yet. |
|
621 |
||
30296 | 622 |
\item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure |
623 |
of the specified sub-goal, producing an extended context and a |
|
624 |
reduced goal, which needs to be solved by the given tactic. All |
|
625 |
schematic parameters of the goal are imported into the context as |
|
626 |
fixed ones, which may not be instantiated in the sub-proof. |
|
627 |
||
35001 | 628 |
\item \verb|Subgoal.FOCUS|, \verb|Subgoal.FOCUS_PREMS|, and \verb|Subgoal.FOCUS_PARAMS| are similar to \verb|SUBPROOF|, but are |
629 |
slightly more flexible: only the specified parts of the subgoal are |
|
630 |
imported into the context, and the body tactic may introduce new |
|
631 |
subgoals and schematic variables. |
|
632 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
633 |
\item \verb|Subgoal.focus|, \verb|Subgoal.focus_prems|, \verb|Subgoal.focus_params| extract the focus information from a goal |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
634 |
state in the same way as the corresponding tacticals above. This is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
635 |
occasionally useful to experiment without writing actual tactics |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
636 |
yet. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
637 |
|
30296 | 638 |
\item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and |
639 |
assumptions \isa{As}, and applies tactic \isa{tac} to solve |
|
640 |
it. The latter may depend on the local assumptions being presented |
|
641 |
as facts. The result is in HHF normal form. |
|
642 |
||
643 |
\item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but |
|
644 |
states several conclusions simultaneously. The goal is encoded by |
|
645 |
means of Pure conjunction; \verb|Goal.conjunction_tac| will turn this |
|
646 |
into a collection of individual subgoals. |
|
647 |
||
648 |
\item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the |
|
649 |
given facts using a tactic, which results in additional fixed |
|
650 |
variables and assumptions in the context. Final results need to be |
|
651 |
exported explicitly. |
|
652 |
||
653 |
\end{description}% |
|
654 |
\end{isamarkuptext}% |
|
655 |
\isamarkuptrue% |
|
656 |
% |
|
657 |
\endisatagmlref |
|
658 |
{\isafoldmlref}% |
|
659 |
% |
|
660 |
\isadelimmlref |
|
661 |
% |
|
662 |
\endisadelimmlref |
|
663 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
664 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
665 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
666 |
\endisadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
667 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
668 |
\isatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
669 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
670 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
671 |
The following minimal example illustrates how to access |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
672 |
the focus information of a structured goal state.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
673 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
674 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
675 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
676 |
\endisatagmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
677 |
{\isafoldmlex}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
678 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
679 |
\isadelimmlex |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
680 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
681 |
\endisadelimmlex |
40964 | 682 |
\isacommand{notepad}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
683 |
\isanewline |
40964 | 684 |
\isakeyword{begin}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
685 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
686 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
687 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
688 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
689 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
690 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
691 |
\isacommand{fix}\isamarkupfalse% |
40406 | 692 |
\ A\ B\ C\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
693 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
694 |
\ \ \isacommand{have}\isamarkupfalse% |
40406 | 695 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
696 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
697 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
698 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
699 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
700 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
701 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
702 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
703 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
704 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
705 |
\ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
706 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
707 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
708 |
\isatagML |
40406 | 709 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
710 |
\isanewline |
40406 | 711 |
\ \ \ \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
712 |
\ \ \ \ \ \ val\ {\isaliteral{7B}{\isacharbraceleft}}goal{\isaliteral{2C}{\isacharcomma}}\ context\ {\isaliteral{3D}{\isacharequal}}\ goal{\isaliteral{5F}{\isacharunderscore}}ctxt{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
713 |
\isaantiq |
40406 | 714 |
Isar{\isaliteral{2E}{\isachardot}}goal{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
715 |
\endisaantiq |
40406 | 716 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
717 |
\ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}focus\ as\ {\isaliteral{7B}{\isacharbraceleft}}params{\isaliteral{2C}{\isacharcomma}}\ asms{\isaliteral{2C}{\isacharcomma}}\ concl{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\ goal{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
718 |
\ \ \ \ \ \ \ \ Subgoal{\isaliteral{2E}{\isachardot}}focus\ goal{\isaliteral{5F}{\isacharunderscore}}ctxt\ {\isadigit{1}}\ goal{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
719 |
\ \ \ \ \ \ val\ {\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}prems\ focus{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
720 |
\ \ \ \ \ \ val\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}params\ focus{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
721 |
\ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
722 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
723 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
724 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
725 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
726 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
727 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
728 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
729 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
730 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
731 |
\ \ \ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
732 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
733 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
734 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
735 |
\isacommand{oops}\isamarkupfalse% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
736 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
737 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
738 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
739 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
740 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
741 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
742 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
743 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
744 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
745 |
\medskip The next example demonstrates forward-elimination in |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
746 |
a local context, using \verb|Obtain.result|.% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
747 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
748 |
\isamarkuptrue% |
40964 | 749 |
\isacommand{notepad}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
750 |
\isanewline |
40964 | 751 |
\isakeyword{begin}\isanewline |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
752 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
753 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
754 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
755 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
756 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
757 |
\isatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
758 |
\isacommand{assume}\isamarkupfalse% |
40406 | 759 |
\ ex{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
760 |
\endisatagproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
761 |
{\isafoldproof}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
762 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
763 |
\isadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
764 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
765 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
766 |
\endisadelimproof |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
767 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
768 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
769 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
770 |
\ \ % |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
771 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
772 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
773 |
\isatagML |
40406 | 774 |
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse% |
775 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
|
776 |
\ \ \ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
777 |
\isaantiq |
40406 | 778 |
context{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
779 |
\endisaantiq |
40406 | 780 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
781 |
\ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}B{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ ctxt{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ctxt{\isadigit{0}}\isanewline |
|
782 |
\ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Obtain{\isaliteral{2E}{\isachardot}}result\ {\isaliteral{28}{\isacharparenleft}}fn\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ etac\ % |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
783 |
\isaantiq |
40406 | 784 |
thm\ exE{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
785 |
\endisaantiq |
40406 | 786 |
\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
787 |
\isaantiq |
40406 | 788 |
thm\ ex{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
789 |
\endisaantiq |
40406 | 790 |
{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
791 |
\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline |
|
792 |
\ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse% |
|
793 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
|
42361 | 794 |
\ \ \ \ singleton\ {\isaliteral{28}{\isacharparenleft}}Proof{\isaliteral{5F}{\isacharunderscore}}Context{\isaliteral{2E}{\isachardot}}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ % |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
795 |
\isaantiq |
40406 | 796 |
thm\ refl{}% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
797 |
\endisaantiq |
40406 | 798 |
{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
799 |
\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline |
|
800 |
\ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse% |
|
801 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
|
42361 | 802 |
\ \ \ \ Proof{\isaliteral{5F}{\isacharunderscore}}Context{\isaliteral{2E}{\isachardot}}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ {\isaliteral{5B}{\isacharbrackleft}}Thm{\isaliteral{2E}{\isachardot}}reflexive\ x{\isaliteral{5D}{\isacharbrackright}}\isanewline |
40406 | 803 |
\ \ \ \ \ \ handle\ ERROR\ msg\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}warning\ msg{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
804 |
\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline |
|
40964 | 805 |
\isacommand{end}\isamarkupfalse% |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
806 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
807 |
\endisatagML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
808 |
{\isafoldML}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
809 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
810 |
\isadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
811 |
\isanewline |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
812 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
813 |
\endisadelimML |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
814 |
% |
30296 | 815 |
\isadelimtheory |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
816 |
\isanewline |
30296 | 817 |
% |
818 |
\endisadelimtheory |
|
819 |
% |
|
820 |
\isatagtheory |
|
821 |
\isacommand{end}\isamarkupfalse% |
|
822 |
% |
|
823 |
\endisatagtheory |
|
824 |
{\isafoldtheory}% |
|
825 |
% |
|
826 |
\isadelimtheory |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
827 |
\isanewline |
30296 | 828 |
% |
829 |
\endisadelimtheory |
|
830 |
\end{isabellebody}% |
|
831 |
%%% Local Variables: |
|
832 |
%%% mode: latex |
|
833 |
%%% TeX-master: "root" |
|
834 |
%%% End: |