author  wenzelm 
Thu, 26 Jan 2012 15:28:17 +0100  
changeset 46265  b6ab3cdea163 
parent 42666  fee67c099d03 
child 46525  af3df09590f9 
permissions  rwrr 
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 placeholder 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 typeinference. 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 typetheoretic 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 highlevel 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}\verbVariable.add_fixes: \isasep\isanewline% 

171 
\verb string list > Proof.context > string list * Proof.context \\ 

172 
\indexdef{}{ML}{Variable.variant\_fixes}\verbVariable.variant_fixes: \isasep\isanewline% 

173 
\verb string list > Proof.context > string list * Proof.context \\ 

174 
\indexdef{}{ML}{Variable.declare\_term}\verbVariable.declare_term: term > Proof.context > Proof.context \\ 

175 
\indexdef{}{ML}{Variable.declare\_constraints}\verbVariable.declare_constraints: term > Proof.context > Proof.context \\ 

176 
\indexdef{}{ML}{Variable.export}\verbVariable.export: Proof.context > Proof.context > thm list > thm list \\ 

177 
\indexdef{}{ML}{Variable.polymorphic}\verbVariable.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}\verbVariable.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}\verbVariable.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 \verbVariable.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 \verbVariable.variant_fixes is similar to \verbVariable.add_fixes, but always produces fresh variants of the given 

194 
names. 

195 

196 
\item \verbVariable.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 \verbVariable.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 \verbVariable.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 \verbVariable.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 typeinference is to 

213 
fix newly introduced type variables, which is essentially reversed 

214 
with \verbVariable.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 \verbVariable.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 \verbVariable.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 typeinference.% 
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 \verbVariable.add_fixes and \verbVariable.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 nonschematic 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 subgoal 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}\verbtype Assumption.export \\ 

433 
\indexdef{}{ML}{Assumption.assume}\verbAssumption.assume: cterm > thm \\ 

434 
\indexdef{}{ML}{Assumption.add\_assms}\verbAssumption.add_assms: Assumption.export >\isasep\isanewline% 

435 
\verb cterm list > Proof.context > thm list * Proof.context \\ 

436 
\indexdef{}{ML}{Assumption.add\_assumes}\verbAssumption.add_assumes: \isasep\isanewline% 

437 
\verb cterm list > Proof.context > thm list * Proof.context \\ 

438 
\indexdef{}{ML}{Assumption.export}\verbAssumption.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 \verbAssumption.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 \verbbool > cterm list\isasep\isanewline% 
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

445 
\verb > thm > thm, where the \verbbool indicates goal mode, 
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

446 
and the \verbcterm 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 \verbAssumption.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 \verbAssumption.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 
\verbAssumption.assume. 

456 

457 
\item \verbAssumption.add_assumes~\isa{As} is a special case of 

42666  458 
\verbAssumption.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 \verbAssumption.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 \verbProof_Context.export combines \verbVariable.export 
30296  466 
and \verbAssumption.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 

488 
some local fact afterwards. We refer to \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} equality 

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.\ \verbVariable.export or the combined \verbProof_Context.export).% 
35001  536 
\end{isamarkuptext}% 
537 
\isamarkuptrue% 

538 
% 

539 
\isamarkupsection{Structured goals and results \label{sec:structgoals}% 

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 adhoc 
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 subgoal: 

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{isabelleisarref} for the userlevel \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}\verbSELECT_GOAL: tactic > int > tactic \\ 
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

592 
\indexdef{}{ML}{SUBPROOF}\verbSUBPROOF: (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}\verbSubgoal.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}\verbSubgoal.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}\verbSubgoal.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}\verbSubgoal.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}\verbSubgoal.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}\verbSubgoal.focus_params: Proof.context > int > thm > Subgoal.focus * thm \\ 
30296  603 
\end{mldecls} 
35001  604 

30296  605 
\begin{mldecls} 
606 
\indexdef{}{ML}{Goal.prove}\verbGoal.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}\verbGoal.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}\verbObtain.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 \verbSELECT_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 \verbSUBPROOF~\isa{tac\ ctxt\ i} decomposes the structure 
623 
of the specified subgoal, 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 subproof. 

627 

35001  628 
\item \verbSubgoal.FOCUS, \verbSubgoal.FOCUS_PREMS, and \verbSubgoal.FOCUS_PARAMS are similar to \verbSUBPROOF, 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 \verbSubgoal.focus, \verbSubgoal.focus_prems, \verbSubgoal.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 \verbGoal.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 \verbGoal.prove_multi is simular to \verbGoal.prove, but 

644 
states several conclusions simultaneously. The goal is encoded by 

645 
means of Pure conjunction; \verbGoal.conjunction_tac will turn this 

646 
into a collection of individual subgoals. 

647 

648 
\item \verbObtain.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 forwardelimination in 
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

746 
a local context, using \verbObtain.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 
%%% TeXmaster: "root" 

834 
%%% End: 