doc-src/IsarImplementation/Thy/document/Proof.tex
author wenzelm
Thu, 26 Jan 2012 15:28:17 +0100
changeset 46265 b6ab3cdea163
parent 42666 fee67c099d03
child 46525 af3df09590f9
permissions -rw-r--r--
added SELECT_GOAL;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     1
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{Proof}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     4
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     5
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     6
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     7
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     8
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     9
\isatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    10
\isacommand{theory}\isamarkupfalse%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    11
\ Proof\isanewline
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    12
\isakeyword{imports}\ Base\isanewline
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    13
\isakeyword{begin}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    14
\endisatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    15
{\isafoldtheory}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    16
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    17
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    18
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    19
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    20
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    21
\isamarkupchapter{Structured proofs%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    22
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    23
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    24
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    25
\isamarkupsection{Variables \label{sec:variables}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    26
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    27
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    28
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    29
\begin{isamarkuptext}%
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    30
Any variable that is not explicitly bound by \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-abstraction
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    31
  is considered as ``free''.  Logically, free variables act like
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    33
  holds \emph{for all} values of \isa{x}.  Free variables for
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    35
  that \isa{x} does not occur elsewhere in the context.
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    37
  quantifier, \isa{x} is essentially ``arbitrary, but fixed'',
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    38
  while from outside it appears as a place-holder for instantiation
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    39
  (thanks to \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} elimination).
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    40
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    41
  The Pure logic represents the idea of variables being either inside
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    42
  or outside the current scope by providing separate syntactic
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    43
  categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    44
  \emph{schematic variables} (e.g.\ \isa{{\isaliteral{3F}{\isacharquery}}x}).  Incidently, a
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
    46
  explicit quantifier.  The same principle works for type variables:
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
    48
  without demanding a truly polymorphic framework.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    49
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    50
  \medskip Additional care is required to treat type variables in a
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    51
  way that facilitates type-inference.  In principle, term variables
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    52
  depend on type variables, which means that type variables would have
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    53
  to be declared first.  For example, a raw type-theoretic framework
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    54
  would demand the context to be constructed in stages as follows:
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    56
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    57
  We allow a slightly less formalistic mode of operation: term
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    58
  variables \isa{x} are fixed without specifying a type yet
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    59
  (essentially \emph{all} potential occurrences of some instance
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    60
  \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} are fixed); the first occurrence of \isa{x}
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    61
  within a specific term assigns its most general type, which is then
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    62
  maintained consistently in the context.  The above example becomes
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    64
  \isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}} is an implicit consequence of the occurrence of
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    65
  \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C616C7068613E}{\isasymalpha}}} in the subsequent proposition.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    66
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    67
  This twist of dependencies is also accommodated by the reverse
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    68
  operation of exporting results from a context: a type variable
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    69
  \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} is considered fixed as long as it occurs in some fixed
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
    75
\isacommand{notepad}\isamarkupfalse%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
    76
\isanewline
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
    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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
    99
\ {\isaliteral{28}{\isacharparenleft}}rule\ reflexive{\isaliteral{29}{\isacharparenright}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   139
  frontier between fixed and schematic variables.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   140
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   141
  The \isa{add{\isaliteral{5F}{\isacharunderscore}}fixes} operation explictly declares fixed
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   142
  variables; the \isa{declare{\isaliteral{5F}{\isacharunderscore}}term} operation absorbs a term into
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   143
  a context by fixing new type variables and adding syntactic
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   144
  constraints.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   145
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   146
  The \isa{export} operation is able to perform the main work of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   147
  generalizing term and type variables as sketched above, assuming
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   148
  that fixing variables and terms have been declared properly.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   149
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   150
  There \isa{import} operation makes a generalized fact a genuine
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   151
  part of the context, by inventing fixed variables for the schematic
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   152
  ones.  The effect can be reversed by using \isa{export} later,
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   153
  potentially with an extended context; the result is equivalent to
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   154
  the original modulo renaming of schematic variables.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   155
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   156
  The \isa{focus} operation provides a variant of \isa{import}
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   159
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   160
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   161
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   162
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   163
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   164
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   165
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   166
\isatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   167
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   168
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   169
\begin{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   170
  \indexdef{}{ML}{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   171
\verb|  string list -> Proof.context -> string list * Proof.context| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   172
  \indexdef{}{ML}{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   173
\verb|  string list -> Proof.context -> string list * Proof.context| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   174
  \indexdef{}{ML}{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   175
  \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   176
  \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   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
aa48c2b8f8e0 updated Variable.import;
wenzelm
parents: 32201
diff changeset
   179
\verb|  (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\
42509
9d107a52b634 updated Variable.focus;
wenzelm
parents: 42361
diff changeset
   180
  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: term -> Proof.context ->|\isasep\isanewline%
9d107a52b634 updated Variable.focus;
wenzelm
parents: 42361
diff changeset
   181
\verb|  ((string * (string * typ)) list * term) * Proof.context| \\
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   182
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   183
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   184
  \begin{description}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   185
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   186
  \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   187
  variables \isa{xs}, returning the resulting internal names.  By
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   188
  default, the internal representation coincides with the external
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   189
  one, which also means that the given variables must not be fixed
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   190
  already.  There is a different policy within a local proof body: the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   191
  given names are just hints for newly invented Skolem variables.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   192
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   193
  \item \verb|Variable.variant_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   194
  names.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   195
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   196
  \item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   197
  \isa{t} to belong to the context.  This automatically fixes new
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   198
  type variables, but not term variables.  Syntactic constraints for
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   199
  type and term variables are declared uniformly, though.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   200
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   201
  \item \verb|Variable.declare_constraints|~\isa{t\ ctxt} declares
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   202
  syntactic constraints from term \isa{t}, without making it part
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   203
  of the context yet.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   204
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   205
  \item \verb|Variable.export|~\isa{inner\ outer\ thms} generalizes
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   206
  fixed type and term variables in \isa{thms} according to the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   207
  difference of the \isa{inner} and \isa{outer} context,
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   208
  following the principles sketched above.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   209
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   210
  \item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   211
  variables in \isa{ts} as far as possible, even those occurring
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   212
  in fixed term variables.  The default policy of type-inference is to
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   213
  fix newly introduced type variables, which is essentially reversed
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   214
  with \verb|Variable.polymorphic|: here the given terms are detached
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   215
  from the context as far as possible.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   218
  type and term variables for the schematic ones occurring in \isa{thms}.  The \isa{open} flag indicates whether the fixed names
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   219
  should be accessible to the user, otherwise newly introduced names
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   220
  are marked as ``internal'' (\secref{sec:names}).
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   221
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   222
  \item \verb|Variable.focus|~\isa{B} decomposes the outermost \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} prefix of proposition \isa{B}.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   223
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   224
  \end{description}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   225
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   226
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   227
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   228
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   229
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   230
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   231
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   232
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   233
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   234
%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   235
\isadelimmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   236
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   237
\endisadelimmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   238
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   239
\isatagmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   240
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   244
\end{isamarkuptext}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   245
\isamarkuptrue%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   246
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   247
\endisatagmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   248
{\isafoldmlex}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   249
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   250
\isadelimmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   251
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   252
\endisadelimmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   253
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   254
\isadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   255
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   256
\endisadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   257
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   258
\isatagML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   259
\isacommand{ML}\isamarkupfalse%
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   260
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   262
\ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ %
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   263
\isaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   264
context{}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   265
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   266
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   267
\isanewline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   270
\isanewline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   274
\isanewline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   275
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}term\ u\ enforces\ specific\ type\ assignment{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   277
\isanewline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   281
{\isaliteral{2A7D}{\isacharverbatimclose}}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   282
\endisatagML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   283
{\isafoldML}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   284
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   285
\isadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   286
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   287
\endisadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   288
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   289
\begin{isamarkuptext}%
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 39885
diff changeset
   290
In the above example, the starting context is derived from the
916cb4a28ffd misc tuning;
wenzelm
parents: 39885
diff changeset
   291
  toplevel theory, which means that fixed variables are internalized
40153
wenzelm
parents: 40126
diff changeset
   292
  literally: \isa{x} is mapped again to \isa{x}, and
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 39885
diff changeset
   293
  attempting to fix it again in the subsequent context is an error.
916cb4a28ffd misc tuning;
wenzelm
parents: 39885
diff changeset
   294
  Alternatively, fixed parameters can be renamed explicitly as
916cb4a28ffd misc tuning;
wenzelm
parents: 39885
diff changeset
   295
  follows:%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   296
\end{isamarkuptext}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   297
\isamarkuptrue%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   298
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   299
\isadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   300
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   301
\endisadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   302
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   303
\isatagML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   304
\isacommand{ML}\isamarkupfalse%
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   305
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   306
\ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ %
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   307
\isaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   308
context{}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   309
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   310
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   313
{\isaliteral{2A7D}{\isacharverbatimclose}}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   314
\endisatagML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   315
{\isafoldML}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   316
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   317
\isadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   318
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   319
\endisadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   320
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   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
wenzelm
parents: 40126
diff changeset
   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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   327
\end{isamarkuptext}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   328
\isamarkuptrue%
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   329
\isacommand{notepad}\isamarkupfalse%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   330
\isanewline
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   331
\isakeyword{begin}\isanewline
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   332
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   333
\isadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   334
\ \ %
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   335
\endisadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   336
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   337
\isatagML
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   338
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse%
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   339
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   340
\ \ \ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ %
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   341
\isaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   342
context{}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   343
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   344
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   345
\isanewline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   349
\isanewline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   352
\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   353
\isacommand{end}\isamarkupfalse%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   354
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   355
\endisatagML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   356
{\isafoldML}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   357
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   358
\isadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   359
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   360
\endisadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   361
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   364
  proposals given in a row are only accepted by the second version.%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   365
\end{isamarkuptext}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   366
\isamarkuptrue%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   367
%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   368
\isamarkupsection{Assumptions \label{sec:assumptions}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   369
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   370
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   371
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   372
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   373
An \emph{assumption} is a proposition that it is postulated in the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   374
  current context.  Local conclusions may use assumptions as
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   375
  additional facts, but this imposes implicit hypotheses that weaken
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   376
  the overall statement.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   377
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   378
  Assumptions are restricted to fixed non-schematic statements, i.e.\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   379
  all generality needs to be expressed by explicit quantifiers.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   380
  Nevertheless, the result will be in HHF normal form with outermost
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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}
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   382
  of fixed type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}.  Local derivations accumulate more and
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   384
  be covered by the assumptions of the current context.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   385
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   386
  \medskip The \isa{add{\isaliteral{5F}{\isacharunderscore}}assms} operation augments the context by
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   387
  local assumptions, which are parameterized by an arbitrary \isa{export} rule (see below).
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   388
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   389
  The \isa{export} operation moves facts from a (larger) inner
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   390
  context into a (smaller) outer context, by discharging the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   391
  difference of the assumptions as specified by the associated export
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   392
  rules.  Note that the discharged portion is determined by the
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   393
  difference of contexts, not the facts being exported!  There is a
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   394
  separate flag to indicate a goal context, where the result is meant
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   395
  to refine an enclosing sub-goal of a structured proof state.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   396
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   397
  \medskip The most basic export rule discharges assumptions directly
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   398
  by means of the \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} introduction rule:
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   399
  \[
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42509
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   401
  \]
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   402
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   403
  The variant for goal refinements marks the newly introduced
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   404
  premises, which causes the canonical Isar goal refinement scheme to
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   405
  enforce unification with local premises within the goal:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   406
  \[
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42509
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   408
  \]
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   409
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   410
  \medskip Alternative versions of assumptions may perform arbitrary
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   411
  transformations on export, as long as the corresponding portion of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   412
  hypotheses is removed from the given facts.  For example, a local
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   413
  definition works by fixing \isa{x} and assuming \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t},
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   414
  with the following export rule to reverse the effect:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   415
  \[
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42509
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   417
  \]
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   418
  This works, because the assumption \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} was introduced in
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   419
  a context with \isa{x} being fresh, so \isa{x} does not
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   420
  occur in \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} here.%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   421
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   422
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   423
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   424
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   425
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   426
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   427
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   428
\isatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   429
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   430
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   431
\begin{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   432
  \indexdef{}{ML type}{Assumption.export}\verb|type Assumption.export| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   433
  \indexdef{}{ML}{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   434
  \indexdef{}{ML}{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   435
\verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   436
  \indexdef{}{ML}{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   437
\verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   438
  \indexdef{}{ML}{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   439
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   440
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   441
  \begin{description}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   448
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   450
  conclusion \isa{A{\isaliteral{27}{\isacharprime}}} is in HHF normal form.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   451
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   452
  \item \verb|Assumption.add_assms|~\isa{r\ As} augments the context
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   453
  by assumptions \isa{As} with export rule \isa{r}.  The
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   454
  resulting facts are hypothetical theorems as produced by the raw
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   455
  \verb|Assumption.assume|.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   456
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   457
  \item \verb|Assumption.add_assumes|~\isa{As} is a special case of
42666
fee67c099d03 use existing \<hyphen>;
wenzelm
parents: 42509
diff changeset
   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
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   459
  mode.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   460
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   461
  \item \verb|Assumption.export|~\isa{is{\isaliteral{5F}{\isacharunderscore}}goal\ inner\ outer\ thm}
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   462
  exports result \isa{thm} from the the \isa{inner} context
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   463
  back into the \isa{outer} one; \isa{is{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ true} means
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   464
  this is a goal context.  The result is in HHF normal form.  Note
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40964
diff changeset
   465
  that \verb|Proof_Context.export| combines \verb|Variable.export|
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   466
  and \verb|Assumption.export| in the canonical way.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   467
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   468
  \end{description}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   469
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   470
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   471
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   472
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   473
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   474
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   475
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   476
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   477
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   478
%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   479
\isadelimmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   480
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   481
\endisadelimmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   482
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   483
\isatagmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   484
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   485
\begin{isamarkuptext}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   486
The following example demonstrates how rules can be
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   487
  derived by building up a context of assumptions first, and exporting
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   488
  some local fact afterwards.  We refer to \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} equality
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   489
  here for testing purposes.%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   490
\end{isamarkuptext}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   491
\isamarkuptrue%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   492
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   493
\endisatagmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   494
{\isafoldmlex}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   495
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   496
\isadelimmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   497
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   498
\endisadelimmlex
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   499
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   500
\isadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   501
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   502
\endisadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   503
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   504
\isatagML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   505
\isacommand{ML}\isamarkupfalse%
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   506
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   508
\ \ val\ ctxt{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ %
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   509
\isaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   510
context{}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   511
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   512
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   513
\isanewline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   515
\ \ \ \ ctxt{\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ Assumption{\isaliteral{2E}{\isachardot}}add{\isaliteral{5F}{\isacharunderscore}}assumes\ {\isaliteral{5B}{\isacharbrackleft}}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   516
\isaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   517
cprop\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ y{\isaliteral{22}{\isachardoublequote}}{}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   518
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   519
{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   520
\ \ val\ eq{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Thm{\isaliteral{2E}{\isachardot}}symmetric\ eq{\isaliteral{3B}{\isacharsemicolon}}\isanewline
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   521
\isanewline
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   524
{\isaliteral{2A7D}{\isacharverbatimclose}}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   525
\endisatagML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   526
{\isafoldML}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   527
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   528
\isadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   529
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   530
\endisadelimML
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   531
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   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
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40964
diff changeset
   535
  context beforehand, and export wrt.\ variables afterwards (cf.\ \verb|Variable.export| or the combined \verb|Proof_Context.export|).%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   536
\end{isamarkuptext}%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   537
\isamarkuptrue%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   538
%
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   539
\isamarkupsection{Structured goals and results \label{sec:struct-goals}%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   540
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   541
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   542
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   543
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   544
Local results are established by monotonic reasoning from facts
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   545
  within a context.  This allows common combinations of theorems,
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   546
  e.g.\ via \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} elimination, resolution rules, or equational
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   547
  reasoning, see \secref{sec:thms}.  Unaccounted context manipulations
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   548
  should be avoided, notably raw \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} introduction or ad-hoc
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   549
  references to free variables or assumptions not present in the proof
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   550
  context.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   551
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   552
  \medskip The \isa{SUBPROOF} combinator allows to structure a
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   553
  tactical proof recursively by decomposing a selected sub-goal:
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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}}}
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   555
  after fixing \isa{x} and assuming \isa{A{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}.  This means
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   556
  the tactic needs to solve the conclusion, but may use the premise as
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   557
  a local fact, for locally fixed variables.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   558
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   559
  The family of \isa{FOCUS} combinators is similar to \isa{SUBPROOF}, but allows to retain schematic variables and pending
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   560
  subgoals in the resulting goal state.
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   561
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   562
  The \isa{prove} operation provides an interface for structured
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   563
  backwards reasoning under program control, with some explicit sanity
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   564
  checks of the result.  The goal context can be augmented by
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   565
  additional fixed variables (cf.\ \secref{sec:variables}) and
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   566
  assumptions (cf.\ \secref{sec:assumptions}), which will be available
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   567
  as local facts during the proof and discharged into implications in
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   568
  the result.  Type and term variables are generalized as usual,
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   569
  according to the context.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   570
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   571
  The \isa{obtain} operation produces results by eliminating
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   572
  existing facts by means of a given tactic.  This acts like a dual
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   573
  conclusion: the proof demonstrates that the context may be augmented
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   574
  by parameters and assumptions, without affecting any conclusions
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   578
  the parameters in the conclusion, need to exported explicitly into
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   579
  the original context.%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   580
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   581
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   582
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   583
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   584
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   585
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   586
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   587
\isatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   588
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   589
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   590
\begin{mldecls}
46265
b6ab3cdea163 added SELECT_GOAL;
wenzelm
parents: 42666
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   603
  \end{mldecls}
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   604
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   605
  \begin{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   606
  \indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   607
\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   608
  \indexdef{}{ML}{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   609
\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   610
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   614
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   615
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   616
  \begin{description}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   617
46265
b6ab3cdea163 added SELECT_GOAL;
wenzelm
parents: 42666
diff changeset
   618
  \item \verb|SELECT_GOAL|~\isa{tac\ i} confines a tactic to the
b6ab3cdea163 added SELECT_GOAL;
wenzelm
parents: 42666
diff changeset
   619
  specified subgoal \isa{i}.  This introduces a nested goal state,
b6ab3cdea163 added SELECT_GOAL;
wenzelm
parents: 42666
diff changeset
   620
  without decomposing the internal structure of the subgoal yet.
b6ab3cdea163 added SELECT_GOAL;
wenzelm
parents: 42666
diff changeset
   621
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   622
  \item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   623
  of the specified sub-goal, producing an extended context and a
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   624
  reduced goal, which needs to be solved by the given tactic.  All
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   625
  schematic parameters of the goal are imported into the context as
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   626
  fixed ones, which may not be instantiated in the sub-proof.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   627
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   628
  \item \verb|Subgoal.FOCUS|, \verb|Subgoal.FOCUS_PREMS|, and \verb|Subgoal.FOCUS_PARAMS| are similar to \verb|SUBPROOF|, but are
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   629
  slightly more flexible: only the specified parts of the subgoal are
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   630
  imported into the context, and the body tactic may introduce new
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   631
  subgoals and schematic variables.
31f8d9eaceff updated generated files;
wenzelm
parents: 32302
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   639
  assumptions \isa{As}, and applies tactic \isa{tac} to solve
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   640
  it.  The latter may depend on the local assumptions being presented
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   641
  as facts.  The result is in HHF normal form.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   642
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   643
  \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   644
  states several conclusions simultaneously.  The goal is encoded by
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   645
  means of Pure conjunction; \verb|Goal.conjunction_tac| will turn this
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   646
  into a collection of individual subgoals.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   647
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   648
  \item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   649
  given facts using a tactic, which results in additional fixed
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   650
  variables and assumptions in the context.  Final results need to be
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   651
  exported explicitly.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   652
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   653
  \end{description}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   654
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   655
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   656
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   657
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   658
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   659
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   660
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   661
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   662
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   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
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   682
\isacommand{notepad}\isamarkupfalse%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   683
\isanewline
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   711
\ \ \ \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   714
Isar{\isaliteral{2E}{\isachardot}}goal{}%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   715
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   716
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   718
\ \ \ \ \ \ \ \ Subgoal{\isaliteral{2E}{\isachardot}}focus\ goal{\isaliteral{5F}{\isacharunderscore}}ctxt\ {\isadigit{1}}\ goal{\isaliteral{3B}{\isacharsemicolon}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   749
\isacommand{notepad}\isamarkupfalse%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   750
\isanewline
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   774
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse%
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   775
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   778
context{}%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   779
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   780
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   784
thm\ exE{}%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   785
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   788
thm\ ex{}%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   789
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   790
{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   791
\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   792
\ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse%
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   793
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40964
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   796
thm\ refl{}%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   797
\endisaantiq
40406
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   798
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   799
\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   800
\ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse%
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   801
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40964
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   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
313a24b66a8d updated generated files;
wenzelm
parents: 40153
diff changeset
   804
\ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40406
diff changeset
   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
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   815
\isadelimtheory
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   816
\isanewline
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   817
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   818
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   819
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   820
\isatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   821
\isacommand{end}\isamarkupfalse%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   822
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   823
\endisatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   824
{\isafoldtheory}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   825
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   826
\isadelimtheory
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   827
\isanewline
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   828
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   829
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   830
\end{isabellebody}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   831
%%% Local Variables:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   832
%%% mode: latex
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   833
%%% TeX-master: "root"
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   834
%%% End: