author | wenzelm |
Wed, 25 Jan 2012 21:14:00 +0100 | |
changeset 46262 | 912b42e64fde |
parent 46256 | bc874d2ee55a |
child 46497 | 89ccf66aa73d |
permissions | -rw-r--r-- |
30296 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Logic}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Logic\isanewline |
|
12 |
\isakeyword{imports}\ Base\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Primitive logic \label{ch:logic}% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\begin{isamarkuptext}% |
|
26 |
The logical foundations of Isabelle/Isar are that of the Pure logic, |
|
27 |
which has been introduced as a Natural Deduction framework in |
|
40406 | 28 |
\cite{paulson700}. This is essentially the same logic as ``\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}HOL}'' in the more abstract setting of Pure Type Systems (PTS) |
30296 | 29 |
\cite{Barendregt-Geuvers:2001}, although there are some key |
30 |
differences in the specific treatment of simple types in |
|
31 |
Isabelle/Pure. |
|
32 |
||
33 |
Following type-theoretic parlance, the Pure logic consists of three |
|
40406 | 34 |
levels of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus with corresponding arrows, \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} for syntactic function space (terms depending on terms), \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} for universal quantification (proofs depending on terms), and |
35 |
\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for implication (proofs depending on proofs). |
|
30296 | 36 |
|
37 |
Derivations are relative to a logical theory, which declares type |
|
38 |
constructors, constants, and axioms. Theory declarations support |
|
39 |
schematic polymorphism, which is strictly speaking outside the |
|
40 |
logic.\footnote{This is the deeper logical reason, why the theory |
|
40406 | 41 |
context \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} is separate from the proof context \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} |
35001 | 42 |
of the core calculus: type constructors, term constants, and facts |
43 |
(proof constants) may involve arbitrary type schemes, but the type |
|
44 |
of a locally fixed term parameter is also fixed!}% |
|
30296 | 45 |
\end{isamarkuptext}% |
46 |
\isamarkuptrue% |
|
47 |
% |
|
48 |
\isamarkupsection{Types \label{sec:types}% |
|
49 |
} |
|
50 |
\isamarkuptrue% |
|
51 |
% |
|
52 |
\begin{isamarkuptext}% |
|
53 |
The language of types is an uninterpreted order-sorted first-order |
|
54 |
algebra; types are qualified by ordered type classes. |
|
55 |
||
56 |
\medskip A \emph{type class} is an abstract syntactic entity |
|
40406 | 57 |
declared in the theory context. The \emph{subclass relation} \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} is specified by stating an acyclic |
30296 | 58 |
generating relation; the transitive closure is maintained |
59 |
internally. The resulting relation is an ordering: reflexive, |
|
60 |
transitive, and antisymmetric. |
|
61 |
||
40406 | 62 |
A \emph{sort} is a list of type classes written as \isa{s\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{7D}{\isacharbraceright}}}, it represents symbolic intersection. Notationally, the |
35001 | 63 |
curly braces are omitted for singleton intersections, i.e.\ any |
40406 | 64 |
class \isa{c} may be read as a sort \isa{{\isaliteral{7B}{\isacharbraceleft}}c{\isaliteral{7D}{\isacharbraceright}}}. The ordering |
35001 | 65 |
on type classes is extended to sorts according to the meaning of |
40406 | 66 |
intersections: \isa{{\isaliteral{7B}{\isacharbraceleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ {\isaliteral{7B}{\isacharbraceleft}}d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ d\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}} iff \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}j{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ d\isaliteral{5C3C5E697375623E}{}\isactrlisub j}. The empty intersection \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} refers to |
35001 | 67 |
the universal sort, which is the largest element wrt.\ the sort |
40406 | 68 |
order. Thus \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} represents the ``full sort'', not the |
35001 | 69 |
empty one! The intersection of all (finitely many) classes declared |
70 |
in the current theory is the least element wrt.\ the sort ordering. |
|
30296 | 71 |
|
72 |
\medskip A \emph{fixed type variable} is a pair of a basic name |
|
40406 | 73 |
(starting with a \isa{{\isaliteral{27}{\isacharprime}}} character) and a sort constraint, e.g.\ |
74 |
\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} which is usually printed as \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s}. |
|
30296 | 75 |
A \emph{schematic type variable} is a pair of an indexname and a |
40406 | 76 |
sort constraint, e.g.\ \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} which is usually |
77 |
printed as \isa{{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s}. |
|
30296 | 78 |
|
79 |
Note that \emph{all} syntactic components contribute to the identity |
|
35001 | 80 |
of type variables: basic name, index, and sort constraint. The core |
81 |
logic handles type variables with the same name but different sorts |
|
82 |
as different, although the type-inference layer (which is outside |
|
83 |
the core) rejects anything like that. |
|
30296 | 84 |
|
40406 | 85 |
A \emph{type constructor} \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is a \isa{k}-ary operator |
30296 | 86 |
on types declared in the theory. Type constructor application is |
40406 | 87 |
written postfix as \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}. For |
88 |
\isa{k\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ \isa{prop} |
|
89 |
instead of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}prop}. For \isa{k\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}} the parentheses |
|
90 |
are omitted, e.g.\ \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list} instead of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}list}. |
|
30296 | 91 |
Further notation is provided for specific constructors, notably the |
40406 | 92 |
right-associative infix \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}} instead of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{29}{\isacharparenright}}fun}. |
30296 | 93 |
|
35001 | 94 |
The logical category \emph{type} is defined inductively over type |
40406 | 95 |
variables and type constructors as follows: \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}. |
30296 | 96 |
|
40406 | 97 |
A \emph{type abbreviation} is a syntactic definition \isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} of an arbitrary type expression \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} over |
98 |
variables \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. Type abbreviations appear as type |
|
30296 | 99 |
constructors in the syntax, but are expanded before entering the |
100 |
logical core. |
|
101 |
||
102 |
A \emph{type arity} declares the image behavior of a type |
|
40406 | 103 |
constructor wrt.\ the algebra of sorts: \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}s} means that \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is |
104 |
of sort \isa{s} if every argument type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i} is |
|
105 |
of sort \isa{s\isaliteral{5C3C5E697375623E}{}\isactrlisub i}. Arity declarations are implicitly |
|
106 |
completed, i.e.\ \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c} entails \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c{\isaliteral{27}{\isacharprime}}} for any \isa{c{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ c}. |
|
30296 | 107 |
|
108 |
\medskip The sort algebra is always maintained as \emph{coregular}, |
|
109 |
which means that type arities are consistent with the subclass |
|
40406 | 110 |
relation: for any type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}, and classes \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}, and arities \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}} and \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} holds \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} component-wise. |
30296 | 111 |
|
112 |
The key property of a coregular order-sorted algebra is that sort |
|
113 |
constraints can be solved in a most general fashion: for each type |
|
40406 | 114 |
constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} and sort \isa{s} there is a most general |
115 |
vector of argument sorts \isa{{\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}} such |
|
116 |
that a type scheme \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub s\isaliteral{5C3C5E697375623E}{}\isactrlisub k\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is of sort \isa{s}. |
|
30296 | 117 |
Consequently, type unification has most general solutions (modulo |
118 |
equivalence of sorts), so type-inference produces primary types as |
|
119 |
expected \cite{nipkow-prehofer}.% |
|
120 |
\end{isamarkuptext}% |
|
121 |
\isamarkuptrue% |
|
122 |
% |
|
123 |
\isadelimmlref |
|
124 |
% |
|
125 |
\endisadelimmlref |
|
126 |
% |
|
127 |
\isatagmlref |
|
128 |
% |
|
129 |
\begin{isamarkuptext}% |
|
130 |
\begin{mldecls} |
|
35001 | 131 |
\indexdef{}{ML type}{class}\verb|type class = string| \\ |
132 |
\indexdef{}{ML type}{sort}\verb|type sort = class list| \\ |
|
133 |
\indexdef{}{ML type}{arity}\verb|type arity = string * sort list * sort| \\ |
|
30296 | 134 |
\indexdef{}{ML type}{typ}\verb|type typ| \\ |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
135 |
\indexdef{}{ML}{Term.map\_atyps}\verb|Term.map_atyps: (typ -> typ) -> typ -> typ| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
136 |
\indexdef{}{ML}{Term.fold\_atyps}\verb|Term.fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\ |
30296 | 137 |
\end{mldecls} |
138 |
\begin{mldecls} |
|
139 |
\indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\ |
|
140 |
\indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\ |
|
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
141 |
\indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: Proof.context ->|\isasep\isanewline% |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
142 |
\verb| (binding * int * mixfix) list -> theory -> theory| \\ |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
143 |
\indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: Proof.context ->|\isasep\isanewline% |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
144 |
\verb| binding * string list * typ -> theory -> theory| \\ |
30355 | 145 |
\indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\ |
30296 | 146 |
\indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\ |
147 |
\indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\ |
|
148 |
\end{mldecls} |
|
149 |
||
150 |
\begin{description} |
|
151 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
152 |
\item Type \verb|class| represents type classes. |
30296 | 153 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
154 |
\item Type \verb|sort| represents sorts, i.e.\ finite |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
155 |
intersections of classes. The empty list \verb|[]: sort| refers to |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
156 |
the empty class intersection, i.e.\ the ``full sort''. |
30296 | 157 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
158 |
\item Type \verb|arity| represents type arities. A triple |
40406 | 159 |
\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}\ arity} represents \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}s} as described above. |
30296 | 160 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
161 |
\item Type \verb|typ| represents types; this is a datatype with |
30296 | 162 |
constructors \verb|TFree|, \verb|TVar|, \verb|Type|. |
163 |
||
40406 | 164 |
\item \verb|Term.map_atyps|~\isa{f\ {\isaliteral{5C3C7461753E}{\isasymtau}}} applies the mapping \isa{f} to all atomic types (\verb|TFree|, \verb|TVar|) occurring in |
165 |
\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}. |
|
30296 | 166 |
|
40406 | 167 |
\item \verb|Term.fold_atyps|~\isa{f\ {\isaliteral{5C3C7461753E}{\isasymtau}}} iterates the operation |
168 |
\isa{f} over all occurrences of atomic types (\verb|TFree|, \verb|TVar|) in \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}; the type structure is traversed from left to |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
169 |
right. |
30296 | 170 |
|
40406 | 171 |
\item \verb|Sign.subsort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} |
172 |
tests the subsort relation \isa{s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}. |
|
30296 | 173 |
|
40406 | 174 |
\item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type |
175 |
\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}. |
|
30296 | 176 |
|
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
177 |
\item \verb|Sign.add_types|~\isa{ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}} declares a |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
178 |
new type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and |
30296 | 179 |
optional mixfix syntax. |
180 |
||
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
181 |
\item \verb|Sign.add_type_abbrev|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
182 |
defines a new type abbreviation \isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}. |
30296 | 183 |
|
40406 | 184 |
\item \verb|Sign.primitive_class|~\isa{{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}} declares a new class \isa{c}, together with class |
185 |
relations \isa{c\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub i}, for \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ n}. |
|
30296 | 186 |
|
40406 | 187 |
\item \verb|Sign.primitive_classrel|~\isa{{\isaliteral{28}{\isacharparenleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} declares the class relation \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}. |
30296 | 188 |
|
40406 | 189 |
\item \verb|Sign.primitive_arity|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} declares |
190 |
the arity \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}s}. |
|
30296 | 191 |
|
192 |
\end{description}% |
|
193 |
\end{isamarkuptext}% |
|
194 |
\isamarkuptrue% |
|
195 |
% |
|
196 |
\endisatagmlref |
|
197 |
{\isafoldmlref}% |
|
198 |
% |
|
199 |
\isadelimmlref |
|
200 |
% |
|
201 |
\endisadelimmlref |
|
202 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
203 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
204 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
205 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
206 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
207 |
\isatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
208 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
209 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
210 |
\begin{matharray}{rcl} |
40406 | 211 |
\indexdef{}{ML antiquotation}{class}\hypertarget{ML antiquotation.class}{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
212 |
\indexdef{}{ML antiquotation}{sort}\hypertarget{ML antiquotation.sort}{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
213 |
\indexdef{}{ML antiquotation}{type\_name}\hypertarget{ML antiquotation.type-name}{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
214 |
\indexdef{}{ML antiquotation}{type\_abbrev}\hypertarget{ML antiquotation.type-abbrev}{\hyperlink{ML antiquotation.type-abbrev}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}abbrev}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
215 |
\indexdef{}{ML antiquotation}{nonterminal}\hypertarget{ML antiquotation.nonterminal}{\hyperlink{ML antiquotation.nonterminal}{\mbox{\isa{nonterminal}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
216 |
\indexdef{}{ML antiquotation}{typ}\hypertarget{ML antiquotation.typ}{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
217 |
\end{matharray} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
218 |
|
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
219 |
\begin{railoutput} |
42662 | 220 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
221 |
\rail@term{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
222 |
\rail@nont{\isa{nameref}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
223 |
\rail@end |
42662 | 224 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
225 |
\rail@term{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
226 |
\rail@nont{\isa{sort}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
227 |
\rail@end |
42662 | 228 |
\rail@begin{3}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
229 |
\rail@bar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
230 |
\rail@term{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
231 |
\rail@nextbar{1} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
232 |
\rail@term{\hyperlink{ML antiquotation.type-abbrev}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}abbrev}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
233 |
\rail@nextbar{2} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
234 |
\rail@term{\hyperlink{ML antiquotation.nonterminal}{\mbox{\isa{nonterminal}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
235 |
\rail@endbar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
236 |
\rail@nont{\isa{nameref}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
237 |
\rail@end |
42662 | 238 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
239 |
\rail@term{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
240 |
\rail@nont{\isa{type}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
241 |
\rail@end |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
242 |
\end{railoutput} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
243 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
244 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
245 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
246 |
|
40406 | 247 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}class\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized class \isa{c} --- as \verb|string| literal. |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
248 |
|
40406 | 249 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}sort\ s{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized sort \isa{s} |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
250 |
--- as \verb|string list| literal. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
251 |
|
40406 | 252 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}type{\isaliteral{5F}{\isacharunderscore}}name\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized type |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
253 |
constructor \isa{c} --- as \verb|string| literal. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
254 |
|
40406 | 255 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}type{\isaliteral{5F}{\isacharunderscore}}abbrev\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized type |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
256 |
abbreviation \isa{c} --- as \verb|string| literal. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
257 |
|
40406 | 258 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}nonterminal\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized syntactic |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
259 |
type~/ grammar nonterminal \isa{c} --- as \verb|string| |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
260 |
literal. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
261 |
|
40406 | 262 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}typ\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
263 |
--- as constructor term for datatype \verb|typ|. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
264 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
265 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
266 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
267 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
268 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
269 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
270 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
271 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
272 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
273 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
274 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
275 |
% |
30296 | 276 |
\isamarkupsection{Terms \label{sec:terms}% |
277 |
} |
|
278 |
\isamarkuptrue% |
|
279 |
% |
|
280 |
\begin{isamarkuptext}% |
|
40406 | 281 |
The language of terms is that of simply-typed \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus |
30296 | 282 |
with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72} |
283 |
or \cite{paulson-ml2}), with the types being determined by the |
|
284 |
corresponding binders. In contrast, free variables and constants |
|
35001 | 285 |
have an explicit name and type in each occurrence. |
30296 | 286 |
|
287 |
\medskip A \emph{bound variable} is a natural number \isa{b}, |
|
288 |
which accounts for the number of intermediate binders between the |
|
289 |
variable occurrence in the body and its binding position. For |
|
40406 | 290 |
example, the de-Bruijn term \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub bool\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub bool\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2E}{\isachardot}}\ {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isadigit{0}}} would |
291 |
correspond to \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E627375623E}{}\isactrlbsub bool\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}y\isaliteral{5C3C5E627375623E}{}\isactrlbsub bool\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y} in a named |
|
30296 | 292 |
representation. Note that a bound variable may be represented by |
293 |
different de-Bruijn indices at different occurrences, depending on |
|
294 |
the nesting of abstractions. |
|
295 |
||
296 |
A \emph{loose variable} is a bound variable that is outside the |
|
297 |
scope of local binders. The types (and names) for loose variables |
|
298 |
can be managed as a separate context, that is maintained as a stack |
|
299 |
of hypothetical binders. The core logic operates on closed terms, |
|
300 |
without any loose variables. |
|
301 |
||
302 |
A \emph{fixed variable} is a pair of a basic name and a type, e.g.\ |
|
40406 | 303 |
\isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} which is usually printed \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} here. A |
30296 | 304 |
\emph{schematic variable} is a pair of an indexname and a type, |
40406 | 305 |
e.g.\ \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} which is likewise printed as \isa{{\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}. |
30296 | 306 |
|
307 |
\medskip A \emph{constant} is a pair of a basic name and a type, |
|
40406 | 308 |
e.g.\ \isa{{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} which is usually printed as \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} |
35001 | 309 |
here. Constants are declared in the context as polymorphic families |
40406 | 310 |
\isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}, meaning that all substitution instances \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} for \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} are valid. |
30296 | 311 |
|
40406 | 312 |
The vector of \emph{type arguments} of constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} wrt.\ |
313 |
the declaration \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} is defined as the codomain of the |
|
314 |
matcher \isa{{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}} presented in |
|
315 |
canonical order \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}}, corresponding to the |
|
316 |
left-to-right occurrences of the \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i} in \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. |
|
35001 | 317 |
Within a given theory context, there is a one-to-one correspondence |
40406 | 318 |
between any constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} and the application \isa{c{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} of its type arguments. For example, with \isa{plus\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, the instance \isa{plus\isaliteral{5C3C5E627375623E}{}\isactrlbsub nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\isaliteral{5C3C5E657375623E}{}\isactrlesub } corresponds to |
319 |
\isa{plus{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{29}{\isacharparenright}}}. |
|
30296 | 320 |
|
40406 | 321 |
Constant declarations \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} may contain sort constraints |
322 |
for type variables in \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. These are observed by |
|
30296 | 323 |
type-inference as expected, but \emph{ignored} by the core logic. |
324 |
This means the primitive logic is able to reason with instances of |
|
325 |
polymorphic constants that the user-level type-checker would reject |
|
326 |
due to violation of type class restrictions. |
|
327 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
328 |
\medskip An \emph{atomic term} is either a variable or constant. |
35001 | 329 |
The logical category \emph{term} is defined inductively over atomic |
40406 | 330 |
terms, with abstraction and application as follows: \isa{t\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{7C}{\isacharbar}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{7C}{\isacharbar}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{7C}{\isacharbar}}\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}. Parsing and printing takes care of |
35001 | 331 |
converting between an external representation with named bound |
332 |
variables. Subsequently, we shall use the latter notation instead |
|
333 |
of internal de-Bruijn representation. |
|
30296 | 334 |
|
40406 | 335 |
The inductive relation \isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} assigns a (unique) type to a |
30296 | 336 |
term according to the structure of atomic terms, abstractions, and |
337 |
applicatins: |
|
338 |
\[ |
|
40406 | 339 |
\infer{\isa{a\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}}{} |
30296 | 340 |
\qquad |
40406 | 341 |
\infer{\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}}{\isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}} |
30296 | 342 |
\qquad |
40406 | 343 |
\infer{\isa{t\ u\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}}{\isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} & \isa{u\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}} |
30296 | 344 |
\] |
345 |
A \emph{well-typed term} is a term that can be typed according to these rules. |
|
346 |
||
347 |
Typing information can be omitted: type-inference is able to |
|
348 |
reconstruct the most general type of a raw term, while assigning |
|
349 |
most general types to all of its variables and constants. |
|
350 |
Type-inference depends on a context of type constraints for fixed |
|
351 |
variables, and declarations for polymorphic constants. |
|
352 |
||
353 |
The identity of atomic terms consists both of the name and the type |
|
40406 | 354 |
component. This means that different variables \isa{x\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isaliteral{5C3C5E657375623E}{}\isactrlesub } and \isa{x\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\isaliteral{5C3C5E657375623E}{}\isactrlesub } may become the same after |
35001 | 355 |
type instantiation. Type-inference rejects variables of the same |
356 |
name, but different types. In contrast, mixed instances of |
|
357 |
polymorphic constants occur routinely. |
|
30296 | 358 |
|
40406 | 359 |
\medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} |
30296 | 360 |
is the set of type variables occurring in \isa{t}, but not in |
40406 | 361 |
its type \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. This means that the term implicitly depends |
35001 | 362 |
on type arguments that are not accounted in the result type, i.e.\ |
40406 | 363 |
there are different type instances \isa{t{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} and |
364 |
\isa{t{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with the same type. This slightly |
|
30296 | 365 |
pathological situation notoriously demands additional care. |
366 |
||
40406 | 367 |
\medskip A \emph{term abbreviation} is a syntactic definition \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} of a closed term \isa{t} of type \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}, |
30296 | 368 |
without any hidden polymorphism. A term abbreviation looks like a |
369 |
constant in the syntax, but is expanded before entering the logical |
|
370 |
core. Abbreviations are usually reverted when printing terms, using |
|
40406 | 371 |
\isa{t\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} as rules for higher-order rewriting. |
30296 | 372 |
|
40406 | 373 |
\medskip Canonical operations on \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms include \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion: \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-conversion refers to capture-free |
374 |
renaming of bound variables; \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion contracts an |
|
30296 | 375 |
abstraction applied to an argument term, substituting the argument |
40406 | 376 |
in the body: \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}a} becomes \isa{b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2F}{\isacharslash}}x{\isaliteral{5D}{\isacharbrackright}}}; \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion contracts vacuous application-abstraction: \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ f\ x} becomes \isa{f}, provided that the bound variable |
30296 | 377 |
does not occur in \isa{f}. |
378 |
||
40406 | 379 |
Terms are normally treated modulo \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-conversion, which is |
30296 | 380 |
implicit in the de-Bruijn representation. Names for bound variables |
381 |
in abstractions are maintained separately as (meaningless) comments, |
|
40406 | 382 |
mostly for parsing and printing. Full \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion is |
30296 | 383 |
commonplace in various standard operations (\secref{sec:obj-rules}) |
384 |
that are based on higher-order unification and matching.% |
|
385 |
\end{isamarkuptext}% |
|
386 |
\isamarkuptrue% |
|
387 |
% |
|
388 |
\isadelimmlref |
|
389 |
% |
|
390 |
\endisadelimmlref |
|
391 |
% |
|
392 |
\isatagmlref |
|
393 |
% |
|
394 |
\begin{isamarkuptext}% |
|
395 |
\begin{mldecls} |
|
396 |
\indexdef{}{ML type}{term}\verb|type term| \\ |
|
46262 | 397 |
\indexdef{}{ML infix}{aconv}\verb|infix aconv: term * term -> bool| \\ |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
398 |
\indexdef{}{ML}{Term.map\_types}\verb|Term.map_types: (typ -> typ) -> term -> term| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
399 |
\indexdef{}{ML}{Term.fold\_types}\verb|Term.fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
400 |
\indexdef{}{ML}{Term.map\_aterms}\verb|Term.map_aterms: (term -> term) -> term -> term| \\ |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
401 |
\indexdef{}{ML}{Term.fold\_aterms}\verb|Term.fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\ |
30296 | 402 |
\end{mldecls} |
403 |
\begin{mldecls} |
|
404 |
\indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\ |
|
405 |
\indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\ |
|
406 |
\indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\ |
|
42934 | 407 |
\indexdef{}{ML}{incr\_boundvars}\verb|incr_boundvars: int -> term -> term| \\ |
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
408 |
\indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Proof.context ->|\isasep\isanewline% |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
409 |
\verb| (binding * typ) * mixfix -> theory -> term * theory| \\ |
33174 | 410 |
\indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline% |
30296 | 411 |
\verb| theory -> (term * term) * theory| \\ |
412 |
\indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\ |
|
413 |
\indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\ |
|
414 |
\end{mldecls} |
|
415 |
||
416 |
\begin{description} |
|
417 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
418 |
\item Type \verb|term| represents de-Bruijn terms, with comments |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
419 |
in abstractions, and explicitly named free variables and constants; |
46262 | 420 |
this is a datatype with constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|$|. |
30296 | 421 |
|
40406 | 422 |
\item \isa{t}~\verb|aconv|~\isa{u} checks \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-equivalence of two terms. This is the basic equality relation |
30296 | 423 |
on type \verb|term|; raw datatype equality should only be used |
424 |
for operations related to parsing or printing! |
|
425 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
426 |
\item \verb|Term.map_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}. |
30296 | 427 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
428 |
\item \verb|Term.fold_types|~\isa{f\ t} iterates the operation |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
429 |
\isa{f} over all occurrences of types in \isa{t}; the term |
30296 | 430 |
structure is traversed from left to right. |
431 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
432 |
\item \verb|Term.map_aterms|~\isa{f\ t} applies the mapping \isa{f} to all atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) occurring in \isa{t}. |
30296 | 433 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
434 |
\item \verb|Term.fold_aterms|~\isa{f\ t} iterates the operation |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
435 |
\isa{f} over all occurrences of atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) in \isa{t}; the term structure is |
30296 | 436 |
traversed from left to right. |
437 |
||
438 |
\item \verb|fastype_of|~\isa{t} determines the type of a |
|
439 |
well-typed term. This operation is relatively slow, despite the |
|
440 |
omission of any sanity checks. |
|
441 |
||
40406 | 442 |
\item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}a{\isaliteral{2E}{\isachardot}}\ b}, where occurrences of the atomic term \isa{a} in the |
30296 | 443 |
body \isa{b} are replaced by bound variables. |
444 |
||
40406 | 445 |
\item \verb|betapply|~\isa{{\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ u{\isaliteral{29}{\isacharparenright}}} produces an application \isa{t\ u}, with topmost \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion if \isa{t} is an |
30296 | 446 |
abstraction. |
447 |
||
42934 | 448 |
\item \verb|incr_boundvars|~\isa{j} increments a term's dangling |
449 |
bound variables by the offset \isa{j}. This is required when |
|
450 |
moving a subterm into a context where it is enclosed by a different |
|
451 |
number of abstractions. Bound variables with a matching abstraction |
|
452 |
are unaffected. |
|
453 |
||
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
454 |
\item \verb|Sign.declare_const|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} declares |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
455 |
a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix syntax. |
30296 | 456 |
|
40406 | 457 |
\item \verb|Sign.add_abbrev|~\isa{print{\isaliteral{5F}{\isacharunderscore}}mode\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}} |
458 |
introduces a new term abbreviation \isa{c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}. |
|
30296 | 459 |
|
40406 | 460 |
\item \verb|Sign.const_typargs|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} and \verb|Sign.const_instance|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}} |
30296 | 461 |
convert between two representations of polymorphic constants: full |
462 |
type instance vs.\ compact type arguments form. |
|
463 |
||
464 |
\end{description}% |
|
465 |
\end{isamarkuptext}% |
|
466 |
\isamarkuptrue% |
|
467 |
% |
|
468 |
\endisatagmlref |
|
469 |
{\isafoldmlref}% |
|
470 |
% |
|
471 |
\isadelimmlref |
|
472 |
% |
|
473 |
\endisadelimmlref |
|
474 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
475 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
476 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
477 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
478 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
479 |
\isatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
480 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
481 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
482 |
\begin{matharray}{rcl} |
40406 | 483 |
\indexdef{}{ML antiquotation}{const\_name}\hypertarget{ML antiquotation.const-name}{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
484 |
\indexdef{}{ML antiquotation}{const\_abbrev}\hypertarget{ML antiquotation.const-abbrev}{\hyperlink{ML antiquotation.const-abbrev}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}abbrev}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
485 |
\indexdef{}{ML antiquotation}{const}\hypertarget{ML antiquotation.const}{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
486 |
\indexdef{}{ML antiquotation}{term}\hypertarget{ML antiquotation.term}{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
487 |
\indexdef{}{ML antiquotation}{prop}\hypertarget{ML antiquotation.prop}{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
488 |
\end{matharray} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
489 |
|
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
490 |
\begin{railoutput} |
42662 | 491 |
\rail@begin{2}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
492 |
\rail@bar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
493 |
\rail@term{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
494 |
\rail@nextbar{1} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
495 |
\rail@term{\hyperlink{ML antiquotation.const-abbrev}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}abbrev}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
496 |
\rail@endbar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
497 |
\rail@nont{\isa{nameref}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
498 |
\rail@end |
42662 | 499 |
\rail@begin{3}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
500 |
\rail@term{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
501 |
\rail@bar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
502 |
\rail@nextbar{1} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
503 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
504 |
\rail@plus |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
505 |
\rail@nont{\isa{type}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
506 |
\rail@nextplus{2} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
507 |
\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
508 |
\rail@endplus |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
509 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
510 |
\rail@endbar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
511 |
\rail@end |
42662 | 512 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
513 |
\rail@term{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
514 |
\rail@nont{\isa{term}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
515 |
\rail@end |
42662 | 516 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
517 |
\rail@term{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
518 |
\rail@nont{\isa{prop}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
519 |
\rail@end |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
520 |
\end{railoutput} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
521 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
522 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
523 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
524 |
|
40406 | 525 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const{\isaliteral{5F}{\isacharunderscore}}name\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized logical |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
526 |
constant name \isa{c} --- as \verb|string| literal. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
527 |
|
40406 | 528 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const{\isaliteral{5F}{\isacharunderscore}}abbrev\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
529 |
abbreviated constant name \isa{c} --- as \verb|string| |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
530 |
literal. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
531 |
|
40406 | 532 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const\ c{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
533 |
constant \isa{c} with precise type instantiation in the sense of |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
534 |
\verb|Sign.const_instance| --- as \verb|Const| constructor term for |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
535 |
datatype \verb|term|. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
536 |
|
40406 | 537 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term\ t{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized term \isa{t} |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
538 |
--- as constructor term for datatype \verb|term|. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
539 |
|
40406 | 540 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}prop\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized proposition |
541 |
\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} --- as constructor term for datatype \verb|term|. |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
542 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
543 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
544 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
545 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
546 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
547 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
548 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
549 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
550 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
551 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
552 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
553 |
% |
30296 | 554 |
\isamarkupsection{Theorems \label{sec:thms}% |
555 |
} |
|
556 |
\isamarkuptrue% |
|
557 |
% |
|
558 |
\begin{isamarkuptext}% |
|
559 |
A \emph{proposition} is a well-typed term of type \isa{prop}, a |
|
560 |
\emph{theorem} is a proven proposition (depending on a context of |
|
561 |
hypotheses and the background theory). Primitive inferences include |
|
40406 | 562 |
plain Natural Deduction rules for the primary connectives \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} of the framework. There is also a builtin |
563 |
notion of equality/equivalence \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}.% |
|
30296 | 564 |
\end{isamarkuptext}% |
565 |
\isamarkuptrue% |
|
566 |
% |
|
567 |
\isamarkupsubsection{Primitive connectives and rules \label{sec:prim-rules}% |
|
568 |
} |
|
569 |
\isamarkuptrue% |
|
570 |
% |
|
571 |
\begin{isamarkuptext}% |
|
572 |
The theory \isa{Pure} contains constant declarations for the |
|
40406 | 573 |
primitive connectives \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}, \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}, and \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} of |
30296 | 574 |
the logical framework, see \figref{fig:pure-connectives}. The |
40406 | 575 |
derivability judgment \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} is |
30296 | 576 |
defined inductively by the primitive inferences given in |
577 |
\figref{fig:prim-rules}, with the global restriction that the |
|
578 |
hypotheses must \emph{not} contain any schematic variables. The |
|
579 |
builtin equality is conceptually axiomatized as shown in |
|
580 |
\figref{fig:pure-equality}, although the implementation works |
|
581 |
directly with derived inferences. |
|
582 |
||
583 |
\begin{figure}[htb] |
|
584 |
\begin{center} |
|
585 |
\begin{tabular}{ll} |
|
40406 | 586 |
\isa{all\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & universal quantification (binder \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}) \\ |
587 |
\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & implication (right associative infix) \\ |
|
588 |
\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & equality relation (infix) \\ |
|
30296 | 589 |
\end{tabular} |
590 |
\caption{Primitive connectives of Pure}\label{fig:pure-connectives} |
|
591 |
\end{center} |
|
592 |
\end{figure} |
|
593 |
||
594 |
\begin{figure}[htb] |
|
595 |
\begin{center} |
|
596 |
\[ |
|
40406 | 597 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}axiom{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{\isa{A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C54686574613E}{\isasymTheta}}}} |
30296 | 598 |
\qquad |
40406 | 599 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}assume{\isaliteral{29}{\isacharparenright}}}]{\isa{A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{} |
30296 | 600 |
\] |
601 |
\[ |
|
42666 | 602 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} |
30296 | 603 |
\qquad |
42666 | 604 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}} |
30296 | 605 |
\] |
606 |
\[ |
|
42666 | 607 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\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 | 608 |
\qquad |
42666 | 609 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}} |
30296 | 610 |
\] |
611 |
\caption{Primitive inferences of Pure}\label{fig:prim-rules} |
|
612 |
\end{center} |
|
613 |
\end{figure} |
|
614 |
||
615 |
\begin{figure}[htb] |
|
616 |
\begin{center} |
|
617 |
\begin{tabular}{ll} |
|
40406 | 618 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion \\ |
619 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x} & reflexivity \\ |
|
620 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ y} & substitution \\ |
|
621 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g} & extensionality \\ |
|
622 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ B} & logical equivalence \\ |
|
30296 | 623 |
\end{tabular} |
624 |
\caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality} |
|
625 |
\end{center} |
|
626 |
\end{figure} |
|
627 |
||
40406 | 628 |
The introduction and elimination rules for \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} are analogous to formation of dependently typed \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms representing the underlying proof objects. Proof terms |
30296 | 629 |
are irrelevant in the Pure logic, though; they cannot occur within |
630 |
propositions. The system provides a runtime option to record |
|
631 |
explicit proof terms for primitive inferences. Thus all three |
|
40406 | 632 |
levels of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus become explicit: \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} for |
633 |
terms, and \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for proofs (cf.\ |
|
30296 | 634 |
\cite{Berghofer-Nipkow:2000:TPHOL}). |
635 |
||
42666 | 636 |
Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}) need not be recorded in the hypotheses, because |
35001 | 637 |
the simple syntactic types of Pure are always inhabitable. |
40406 | 638 |
``Assumptions'' \isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} for type-membership are only |
639 |
present as long as some \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} occurs in the statement |
|
640 |
body.\footnote{This is the key difference to ``\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}HOL}'' in |
|
35001 | 641 |
the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses |
40406 | 642 |
\isa{x\ {\isaliteral{3A}{\isacharcolon}}\ A} are treated uniformly for propositions and types.} |
30296 | 643 |
|
644 |
\medskip The axiomatization of a theory is implicitly closed by |
|
40406 | 645 |
forming all instances of type and term variables: \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} holds for any substitution instance of an axiom |
646 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}. By pushing substitutions through derivations |
|
35001 | 647 |
inductively, we also get admissible \isa{generalize} and \isa{instantiate} rules as shown in \figref{fig:subst-rules}. |
30296 | 648 |
|
649 |
\begin{figure}[htb] |
|
650 |
\begin{center} |
|
651 |
\[ |
|
40406 | 652 |
\infer{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} |
30296 | 653 |
\quad |
40406 | 654 |
\infer[\quad\isa{{\isaliteral{28}{\isacharparenleft}}generalize{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} |
30296 | 655 |
\] |
656 |
\[ |
|
40406 | 657 |
\infer{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}}} |
30296 | 658 |
\quad |
40406 | 659 |
\infer[\quad\isa{{\isaliteral{28}{\isacharparenleft}}instantiate{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}}} |
30296 | 660 |
\] |
661 |
\caption{Admissible substitution rules}\label{fig:subst-rules} |
|
662 |
\end{center} |
|
663 |
\end{figure} |
|
664 |
||
665 |
Note that \isa{instantiate} does not require an explicit |
|
40406 | 666 |
side-condition, because \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} may never contain schematic |
30296 | 667 |
variables. |
668 |
||
669 |
In principle, variables could be substituted in hypotheses as well, |
|
670 |
but this would disrupt the monotonicity of reasoning: deriving |
|
40406 | 671 |
\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} from \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B} is |
672 |
correct, but \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} does not necessarily hold: |
|
30296 | 673 |
the result belongs to a different proof context. |
674 |
||
675 |
\medskip An \emph{oracle} is a function that produces axioms on the |
|
676 |
fly. Logically, this is an instance of the \isa{axiom} rule |
|
677 |
(\figref{fig:prim-rules}), but there is an operational difference. |
|
678 |
The system always records oracle invocations within derivations of |
|
679 |
theorems by a unique tag. |
|
680 |
||
681 |
Axiomatizations should be limited to the bare minimum, typically as |
|
682 |
part of the initial logical basis of an object-logic formalization. |
|
683 |
Later on, theories are usually developed in a strictly definitional |
|
684 |
fashion, by stating only certain equalities over new constants. |
|
685 |
||
40406 | 686 |
A \emph{simple definition} consists of a constant declaration \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} together with an axiom \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}, where \isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} is a closed term without any hidden polymorphism. The RHS |
30296 | 687 |
may depend on further defined constants, but not \isa{c} itself. |
40406 | 688 |
Definitions of functions may be presented as \isa{c\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} instead of the puristic \isa{c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ t}. |
30296 | 689 |
|
690 |
An \emph{overloaded definition} consists of a collection of axioms |
|
40406 | 691 |
for the same constant, with zero or one equations \isa{c{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} for each type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} (for |
692 |
distinct variables \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}). The RHS may mention |
|
693 |
previously defined constants as above, or arbitrary constants \isa{d{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{29}{\isacharparenright}}} for some \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i} projected from \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. Thus overloaded definitions essentially work by |
|
30296 | 694 |
primitive recursion over the syntactic structure of a single type |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
695 |
argument. See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.% |
30296 | 696 |
\end{isamarkuptext}% |
697 |
\isamarkuptrue% |
|
698 |
% |
|
699 |
\isadelimmlref |
|
700 |
% |
|
701 |
\endisadelimmlref |
|
702 |
% |
|
703 |
\isatagmlref |
|
704 |
% |
|
705 |
\begin{isamarkuptext}% |
|
706 |
\begin{mldecls} |
|
46253 | 707 |
\indexdef{}{ML}{Logic.all}\verb|Logic.all: term -> term -> term| \\ |
708 |
\indexdef{}{ML}{Logic.mk\_implies}\verb|Logic.mk_implies: term * term -> term| \\ |
|
709 |
\end{mldecls} |
|
710 |
\begin{mldecls} |
|
30296 | 711 |
\indexdef{}{ML type}{ctyp}\verb|type ctyp| \\ |
712 |
\indexdef{}{ML type}{cterm}\verb|type cterm| \\ |
|
713 |
\indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\ |
|
714 |
\indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\ |
|
46253 | 715 |
\indexdef{}{ML}{Thm.capply}\verb|Thm.capply: cterm -> cterm -> cterm| \\ |
716 |
\indexdef{}{ML}{Thm.cabs}\verb|Thm.cabs: cterm -> cterm -> cterm| \\ |
|
717 |
\indexdef{}{ML}{Thm.all}\verb|Thm.all: cterm -> cterm -> cterm| \\ |
|
718 |
\indexdef{}{ML}{Drule.mk\_implies}\verb|Drule.mk_implies: cterm * cterm -> cterm| \\ |
|
30296 | 719 |
\end{mldecls} |
720 |
\begin{mldecls} |
|
721 |
\indexdef{}{ML type}{thm}\verb|type thm| \\ |
|
32836 | 722 |
\indexdef{}{ML}{proofs}\verb|proofs: int Unsynchronized.ref| \\ |
42933 | 723 |
\indexdef{}{ML}{Thm.transfer}\verb|Thm.transfer: theory -> thm -> thm| \\ |
30296 | 724 |
\indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\ |
725 |
\indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\ |
|
726 |
\indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\ |
|
727 |
\indexdef{}{ML}{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\ |
|
728 |
\indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\ |
|
729 |
\indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\ |
|
730 |
\indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\ |
|
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
731 |
\indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: Proof.context ->|\isasep\isanewline% |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
732 |
\verb| binding * term -> theory -> (string * thm) * theory| \\ |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
733 |
\indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: binding * ('a -> cterm) -> theory ->|\isasep\isanewline% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
734 |
\verb| (string * ('a -> thm)) * theory| \\ |
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
735 |
\indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: Proof.context -> bool -> bool ->|\isasep\isanewline% |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
736 |
\verb| binding * term -> theory -> (string * thm) * theory| \\ |
30296 | 737 |
\end{mldecls} |
738 |
\begin{mldecls} |
|
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
739 |
\indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: Proof.context -> string ->|\isasep\isanewline% |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
740 |
\verb| string * typ -> (string * typ) list -> theory -> theory| \\ |
30296 | 741 |
\end{mldecls} |
742 |
||
743 |
\begin{description} |
|
744 |
||
46253 | 745 |
\item \verb|Logic.all|~\isa{a\ B} produces a Pure quantification |
746 |
\isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}a{\isaliteral{2E}{\isachardot}}\ B}, where occurrences of the atomic term \isa{a} in |
|
747 |
the body proposition \isa{B} are replaced by bound variables. |
|
748 |
(See also \verb|lambda| on terms.) |
|
749 |
||
750 |
\item \verb|Logic.mk_implies|~\isa{{\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{29}{\isacharparenright}}} produces a Pure |
|
751 |
implication \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}. |
|
752 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
753 |
\item Types \verb|ctyp| and \verb|cterm| represent certified |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
754 |
types and terms, respectively. These are abstract datatypes that |
30296 | 755 |
guarantee that its values have passed the full well-formedness (and |
756 |
well-typedness) checks, relative to the declarations of type |
|
46253 | 757 |
constructors, constants etc.\ in the background theory. The |
758 |
abstract types \verb|ctyp| and \verb|cterm| are part of the |
|
759 |
same inference kernel that is mainly responsible for \verb|thm|. |
|
760 |
Thus syntactic operations on \verb|ctyp| and \verb|cterm| |
|
761 |
are located in the \verb|Thm| module, even though theorems are |
|
762 |
not yet involved at that stage. |
|
30296 | 763 |
|
40406 | 764 |
\item \verb|Thm.ctyp_of|~\isa{thy\ {\isaliteral{5C3C7461753E}{\isasymtau}}} and \verb|Thm.cterm_of|~\isa{thy\ t} explicitly checks types and terms, |
30296 | 765 |
respectively. This also involves some basic normalizations, such |
766 |
expansion of type and term abbreviations from the theory context. |
|
46253 | 767 |
Full re-certification is relatively slow and should be avoided in |
768 |
tight reasoning loops. |
|
30296 | 769 |
|
46253 | 770 |
\item \verb|Thm.capply|, \verb|Thm.cabs|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions) |
771 |
incrementally. This is equivalent to \verb|Thm.cterm_of| after |
|
46262 | 772 |
unchecked \verb|$|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in |
46253 | 773 |
performance when large existing entities are composed by a few extra |
774 |
constructions on top. There are separate operations to decompose |
|
775 |
certified terms and theorems to produce certified terms again. |
|
30296 | 776 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
777 |
\item Type \verb|thm| represents proven propositions. This is |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
778 |
an abstract datatype that guarantees that its values have been |
30296 | 779 |
constructed by basic principles of the \verb|Thm| module. |
780 |
Every \verb|thm| value contains a sliding back-reference to the |
|
781 |
enclosing theory, cf.\ \secref{sec:context-theory}. |
|
782 |
||
35001 | 783 |
\item \verb|proofs| specifies the detail of proof recording within |
30296 | 784 |
\verb|thm| values: \verb|0| records only the names of oracles, |
785 |
\verb|1| records oracle names and propositions, \verb|2| additionally |
|
786 |
records full proof terms. Officially named theorems that contribute |
|
35001 | 787 |
to a result are recorded in any case. |
30296 | 788 |
|
42933 | 789 |
\item \verb|Thm.transfer|~\isa{thy\ thm} transfers the given |
790 |
theorem to a \emph{larger} theory, see also \secref{sec:context}. |
|
791 |
This formal adjustment of the background context has no logical |
|
792 |
significance, but is occasionally required for formal reasons, e.g.\ |
|
793 |
when theorems that are imported from more basic theories are used in |
|
794 |
the current situation. |
|
795 |
||
30296 | 796 |
\item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim| |
797 |
correspond to the primitive inferences of \figref{fig:prim-rules}. |
|
798 |
||
40406 | 799 |
\item \verb|Thm.generalize|~\isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}} |
30296 | 800 |
corresponds to the \isa{generalize} rules of |
801 |
\figref{fig:subst-rules}. Here collections of type and term |
|
802 |
variables are generalized simultaneously, specified by the given |
|
803 |
basic names. |
|
804 |
||
40406 | 805 |
\item \verb|Thm.instantiate|~\isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} corresponds to the \isa{instantiate} rules |
30296 | 806 |
of \figref{fig:subst-rules}. Type variables are substituted before |
40406 | 807 |
term variables. Note that the types in \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} |
30296 | 808 |
refer to the instantiated versions. |
809 |
||
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
810 |
\item \verb|Thm.add_axiom|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}} declares an |
35927 | 811 |
arbitrary proposition as axiom, and retrieves it as a theorem from |
812 |
the resulting theory, cf.\ \isa{axiom} in |
|
813 |
\figref{fig:prim-rules}. Note that the low-level representation in |
|
814 |
the axiom table may differ slightly from the returned theorem. |
|
30296 | 815 |
|
40406 | 816 |
\item \verb|Thm.add_oracle|~\isa{{\isaliteral{28}{\isacharparenleft}}binding{\isaliteral{2C}{\isacharcomma}}\ oracle{\isaliteral{29}{\isacharparenright}}} produces a named |
30296 | 817 |
oracle rule, essentially generating arbitrary axioms on the fly, |
818 |
cf.\ \isa{axiom} in \figref{fig:prim-rules}. |
|
819 |
||
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
820 |
\item \verb|Thm.add_def|~\isa{ctxt\ unchecked\ overloaded\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ c\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}} states a definitional axiom for an existing constant |
35927 | 821 |
\isa{c}. Dependencies are recorded via \verb|Theory.add_deps|, |
822 |
unless the \isa{unchecked} option is set. Note that the |
|
823 |
low-level representation in the axiom table may differ slightly from |
|
824 |
the returned theorem. |
|
30296 | 825 |
|
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
826 |
\item \verb|Theory.add_deps|~\isa{ctxt\ name\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} |
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40406
diff
changeset
|
827 |
declares dependencies of a named specification for constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}, relative to existing specifications for constants \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. |
30296 | 828 |
|
829 |
\end{description}% |
|
830 |
\end{isamarkuptext}% |
|
831 |
\isamarkuptrue% |
|
832 |
% |
|
833 |
\endisatagmlref |
|
834 |
{\isafoldmlref}% |
|
835 |
% |
|
836 |
\isadelimmlref |
|
837 |
% |
|
838 |
\endisadelimmlref |
|
839 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
840 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
841 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
842 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
843 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
844 |
\isatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
845 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
846 |
\begin{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
847 |
\begin{matharray}{rcl} |
40406 | 848 |
\indexdef{}{ML antiquotation}{ctyp}\hypertarget{ML antiquotation.ctyp}{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
849 |
\indexdef{}{ML antiquotation}{cterm}\hypertarget{ML antiquotation.cterm}{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
850 |
\indexdef{}{ML antiquotation}{cprop}\hypertarget{ML antiquotation.cprop}{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
851 |
\indexdef{}{ML antiquotation}{thm}\hypertarget{ML antiquotation.thm}{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
852 |
\indexdef{}{ML antiquotation}{thms}\hypertarget{ML antiquotation.thms}{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
853 |
\indexdef{}{ML antiquotation}{lemma}\hypertarget{ML antiquotation.lemma}{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
854 |
\end{matharray} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
855 |
|
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
856 |
\begin{railoutput} |
42662 | 857 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
858 |
\rail@term{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
859 |
\rail@nont{\isa{typ}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
860 |
\rail@end |
42662 | 861 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
862 |
\rail@term{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
863 |
\rail@nont{\isa{term}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
864 |
\rail@end |
42662 | 865 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
866 |
\rail@term{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
867 |
\rail@nont{\isa{prop}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
868 |
\rail@end |
42662 | 869 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
870 |
\rail@term{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
871 |
\rail@nont{\isa{thmref}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
872 |
\rail@end |
42662 | 873 |
\rail@begin{1}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
874 |
\rail@term{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
875 |
\rail@nont{\isa{thmrefs}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
876 |
\rail@end |
42662 | 877 |
\rail@begin{6}{} |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
878 |
\rail@term{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
879 |
\rail@bar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
880 |
\rail@nextbar{1} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
881 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
42517
b68e1c27709a
simplified keyword markup (without formal checking);
wenzelm
parents:
42510
diff
changeset
|
882 |
\rail@term{\isa{\isakeyword{open}}}[] |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
883 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
884 |
\rail@endbar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
885 |
\rail@plus |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
886 |
\rail@plus |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
887 |
\rail@nont{\isa{prop}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
888 |
\rail@nextplus{1} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
889 |
\rail@endplus |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
890 |
\rail@nextplus{2} |
42517
b68e1c27709a
simplified keyword markup (without formal checking);
wenzelm
parents:
42510
diff
changeset
|
891 |
\rail@cterm{\isa{\isakeyword{and}}}[] |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
892 |
\rail@endplus |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
893 |
\rail@cr{4} |
42517
b68e1c27709a
simplified keyword markup (without formal checking);
wenzelm
parents:
42510
diff
changeset
|
894 |
\rail@term{\isa{\isakeyword{by}}}[] |
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
895 |
\rail@nont{\isa{method}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
896 |
\rail@bar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
897 |
\rail@nextbar{5} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
898 |
\rail@nont{\isa{method}}[] |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
899 |
\rail@endbar |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
900 |
\rail@end |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
901 |
\end{railoutput} |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset
|
902 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
903 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
904 |
\begin{description} |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
905 |
|
40406 | 906 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ctyp\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{7D}{\isacharbraceright}}} produces a certified type wrt.\ the |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
907 |
current background theory --- as abstract value of type \verb|ctyp|. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
908 |
|
40406 | 909 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}cterm\ t{\isaliteral{7D}{\isacharbraceright}}} and \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}cprop\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{7D}{\isacharbraceright}}} produce a |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
910 |
certified term wrt.\ the current background theory --- as abstract |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
911 |
value of type \verb|cterm|. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
912 |
|
40406 | 913 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thm\ a{\isaliteral{7D}{\isacharbraceright}}} produces a singleton fact --- as abstract |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
914 |
value of type \verb|thm|. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
915 |
|
40406 | 916 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thms\ a{\isaliteral{7D}{\isacharbraceright}}} produces a general fact --- as abstract |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
917 |
value of type \verb|thm list|. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
918 |
|
40406 | 919 |
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}lemma\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ by\ meth{\isaliteral{7D}{\isacharbraceright}}} produces a fact that is proven on |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
920 |
the spot according to the minimal proof, which imitates a terminal |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
921 |
Isar proof. The result is an abstract value of type \verb|thm| |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
922 |
or \verb|thm list|, depending on the number of propositions |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
923 |
given here. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
924 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
925 |
The internal derivation object lacks a proper theorem name, but it |
40406 | 926 |
is formally closed, unless the \isa{{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}} option is specified |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
927 |
(this may impact performance of applications with proof terms). |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
928 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
929 |
Since ML antiquotations are always evaluated at compile-time, there |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
930 |
is no run-time overhead even for non-trivial proofs. Nonetheless, |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
931 |
the justification is syntactically limited to a single \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} step. More complex Isar proofs should be done in regular |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
932 |
theory source, before compiling the corresponding ML text that uses |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
933 |
the result. |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
934 |
|
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
935 |
\end{description}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
936 |
\end{isamarkuptext}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
937 |
\isamarkuptrue% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
938 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
939 |
\endisatagmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
940 |
{\isafoldmlantiq}% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
941 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
942 |
\isadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
943 |
% |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
944 |
\endisadelimmlantiq |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
945 |
% |
46254 | 946 |
\isamarkupsubsection{Auxiliary connectives \label{sec:logic-aux}% |
30296 | 947 |
} |
948 |
\isamarkuptrue% |
|
949 |
% |
|
950 |
\begin{isamarkuptext}% |
|
46254 | 951 |
Theory \isa{Pure} provides a few auxiliary connectives |
952 |
that are defined on top of the primitive ones, see |
|
953 |
\figref{fig:pure-aux}. These special constants are useful in |
|
954 |
certain internal encodings, and are normally not directly exposed to |
|
955 |
the user. |
|
30296 | 956 |
|
957 |
\begin{figure}[htb] |
|
958 |
\begin{center} |
|
959 |
\begin{tabular}{ll} |
|
40406 | 960 |
\isa{conjunction\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & (infix \isa{{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}}) \\ |
961 |
\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}C{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}} \\[1ex] |
|
962 |
\isa{prop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & (prefix \isa{{\isaliteral{23}{\isacharhash}}}, suppressed) \\ |
|
963 |
\isa{{\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A} \\[1ex] |
|
964 |
\isa{term\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & (prefix \isa{TERM}) \\ |
|
965 |
\isa{term\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}A{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{29}{\isacharparenright}}} \\[1ex] |
|
966 |
\isa{TYPE\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ itself} & (prefix \isa{TYPE}) \\ |
|
967 |
\isa{{\isaliteral{28}{\isacharparenleft}}unspecified{\isaliteral{29}{\isacharparenright}}} \\ |
|
30296 | 968 |
\end{tabular} |
969 |
\caption{Definitions of auxiliary connectives}\label{fig:pure-aux} |
|
970 |
\end{center} |
|
971 |
\end{figure} |
|
972 |
||
40406 | 973 |
The introduction \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B}, and eliminations |
974 |
(projections) \isa{A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A} and \isa{A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} are |
|
35001 | 975 |
available as derived rules. Conjunction allows to treat |
976 |
simultaneous assumptions and conclusions uniformly, e.g.\ consider |
|
40406 | 977 |
\isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ D}. In particular, the goal mechanism |
35001 | 978 |
represents multiple claims as explicit conjunction internally, but |
979 |
this is refined (via backwards introduction) into separate sub-goals |
|
980 |
before the user commences the proof; the final result is projected |
|
981 |
into a list of theorems using eliminations (cf.\ |
|
30296 | 982 |
\secref{sec:tactical-goals}). |
983 |
||
40406 | 984 |
The \isa{prop} marker (\isa{{\isaliteral{23}{\isacharhash}}}) makes arbitrarily complex |
985 |
propositions appear as atomic, without changing the meaning: \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A} and \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A} are interchangeable. See |
|
30296 | 986 |
\secref{sec:tactical-goals} for specific operations. |
987 |
||
988 |
The \isa{term} marker turns any well-typed term into a derivable |
|
40406 | 989 |
proposition: \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ TERM\ t} holds unconditionally. Although |
30296 | 990 |
this is logically vacuous, it allows to treat terms and proofs |
991 |
uniformly, similar to a type-theoretic framework. |
|
992 |
||
993 |
The \isa{TYPE} constructor is the canonical representative of |
|
40406 | 994 |
the unspecified type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ itself}; it essentially injects the |
30296 | 995 |
language of types into that of terms. There is specific notation |
40406 | 996 |
\isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} for \isa{TYPE\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isaliteral{5C3C7461753E}{\isasymtau}}\ itself\isaliteral{5C3C5E657375623E}{}\isactrlesub }. |
997 |
Although being devoid of any particular meaning, the term \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} accounts for the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} within the term |
|
998 |
language. In particular, \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}} may be used as formal |
|
30296 | 999 |
argument in primitive definitions, in order to circumvent hidden |
40406 | 1000 |
polymorphism (cf.\ \secref{sec:terms}). For example, \isa{c\ TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}} defines \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ itself\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} in terms of |
30296 | 1001 |
a proposition \isa{A} that depends on an additional type |
1002 |
argument, which is essentially a predicate on types.% |
|
1003 |
\end{isamarkuptext}% |
|
1004 |
\isamarkuptrue% |
|
1005 |
% |
|
1006 |
\isadelimmlref |
|
1007 |
% |
|
1008 |
\endisadelimmlref |
|
1009 |
% |
|
1010 |
\isatagmlref |
|
1011 |
% |
|
1012 |
\begin{isamarkuptext}% |
|
1013 |
\begin{mldecls} |
|
1014 |
\indexdef{}{ML}{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\ |
|
1015 |
\indexdef{}{ML}{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\ |
|
1016 |
\indexdef{}{ML}{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\ |
|
1017 |
\indexdef{}{ML}{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\ |
|
1018 |
\indexdef{}{ML}{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\ |
|
1019 |
\indexdef{}{ML}{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\ |
|
1020 |
\end{mldecls} |
|
1021 |
||
1022 |
\begin{description} |
|
1023 |
||
40406 | 1024 |
\item \verb|Conjunction.intr| derives \isa{A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B} from \isa{A} and \isa{B}. |
30296 | 1025 |
|
1026 |
\item \verb|Conjunction.elim| derives \isa{A} and \isa{B} |
|
40406 | 1027 |
from \isa{A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B}. |
30296 | 1028 |
|
1029 |
\item \verb|Drule.mk_term| derives \isa{TERM\ t}. |
|
1030 |
||
1031 |
\item \verb|Drule.dest_term| recovers term \isa{t} from \isa{TERM\ t}. |
|
1032 |
||
40406 | 1033 |
\item \verb|Logic.mk_type|~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} produces the term \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}}. |
30296 | 1034 |
|
40406 | 1035 |
\item \verb|Logic.dest_type|~\isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} recovers the type |
1036 |
\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}. |
|
30296 | 1037 |
|
1038 |
\end{description}% |
|
1039 |
\end{isamarkuptext}% |
|
1040 |
\isamarkuptrue% |
|
1041 |
% |
|
1042 |
\endisatagmlref |
|
1043 |
{\isafoldmlref}% |
|
1044 |
% |
|
1045 |
\isadelimmlref |
|
1046 |
% |
|
1047 |
\endisadelimmlref |
|
1048 |
% |
|
1049 |
\isamarkupsection{Object-level rules \label{sec:obj-rules}% |
|
1050 |
} |
|
1051 |
\isamarkuptrue% |
|
1052 |
% |
|
1053 |
\begin{isamarkuptext}% |
|
1054 |
The primitive inferences covered so far mostly serve foundational |
|
1055 |
purposes. User-level reasoning usually works via object-level rules |
|
1056 |
that are represented as theorems of Pure. Composition of rules |
|
1057 |
involves \emph{backchaining}, \emph{higher-order unification} modulo |
|
40406 | 1058 |
\isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms, and so-called |
1059 |
\emph{lifting} of rules into a context of \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} connectives. Thus the full power of higher-order Natural |
|
30296 | 1060 |
Deduction in Isabelle/Pure becomes readily available.% |
1061 |
\end{isamarkuptext}% |
|
1062 |
\isamarkuptrue% |
|
1063 |
% |
|
1064 |
\isamarkupsubsection{Hereditary Harrop Formulae% |
|
1065 |
} |
|
1066 |
\isamarkuptrue% |
|
1067 |
% |
|
1068 |
\begin{isamarkuptext}% |
|
1069 |
The idea of object-level rules is to model Natural Deduction |
|
1070 |
inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow |
|
1071 |
arbitrary nesting similar to \cite{extensions91}. The most basic |
|
1072 |
rule format is that of a \emph{Horn Clause}: |
|
1073 |
\[ |
|
40406 | 1074 |
\infer{\isa{A}}{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} & \isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}} & \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub n}} |
30296 | 1075 |
\] |
40406 | 1076 |
where \isa{A{\isaliteral{2C}{\isacharcomma}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n} are atomic propositions |
30296 | 1077 |
of the framework, usually of the form \isa{Trueprop\ B}, where |
1078 |
\isa{B} is a (compound) object-level statement. This |
|
1079 |
object-level inference corresponds to an iterated implication in |
|
1080 |
Pure like this: |
|
1081 |
\[ |
|
40406 | 1082 |
\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A} |
30296 | 1083 |
\] |
40406 | 1084 |
As an example consider conjunction introduction: \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B}. Any parameters occurring in such rule statements are |
30296 | 1085 |
conceptionally treated as arbitrary: |
1086 |
\[ |
|
40406 | 1087 |
\isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m} |
30296 | 1088 |
\] |
1089 |
||
40406 | 1090 |
Nesting of rules means that the positions of \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub i} may |
30296 | 1091 |
again hold compound rules, not just atomic propositions. |
1092 |
Propositions of this format are called \emph{Hereditary Harrop |
|
1093 |
Formulae} in the literature \cite{Miller:1991}. Here we give an |
|
1094 |
inductive characterization as follows: |
|
1095 |
||
1096 |
\medskip |
|
1097 |
\begin{tabular}{ll} |
|
40406 | 1098 |
\isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold x} & set of variables \\ |
1099 |
\isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold A} & set of atomic propositions \\ |
|
1100 |
\isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold H\ \ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold x\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E626F6C643E}{}\isactrlbold H\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E626F6C643E}{}\isactrlbold A} & set of Hereditary Harrop Formulas \\ |
|
30296 | 1101 |
\end{tabular} |
1102 |
\medskip |
|
1103 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
1104 |
Thus we essentially impose nesting levels on propositions formed |
40406 | 1105 |
from \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}. At each level there is a prefix |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
36345
diff
changeset
|
1106 |
of parameters and compound premises, concluding an atomic |
40406 | 1107 |
proposition. Typical examples are \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}-introduction \isa{{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B} or mathematical induction \isa{P\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ P\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n}. Even deeper nesting occurs in well-founded |
1108 |
induction \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}y{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{5C3C707265633E}{\isasymprec}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x}, but this |
|
35001 | 1109 |
already marks the limit of rule complexity that is usually seen in |
1110 |
practice. |
|
30296 | 1111 |
|
1112 |
\medskip Regular user-level inferences in Isabelle/Pure always |
|
1113 |
maintain the following canonical form of results: |
|
1114 |
||
1115 |
\begin{itemize} |
|
1116 |
||
40406 | 1117 |
\item Normalization by \isa{{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{29}{\isacharparenright}}}, |
30296 | 1118 |
which is a theorem of Pure, means that quantifiers are pushed in |
1119 |
front of implication at each level of nesting. The normal form is a |
|
1120 |
Hereditary Harrop Formula. |
|
1121 |
||
1122 |
\item The outermost prefix of parameters is represented via |
|
40406 | 1123 |
schematic variables: instead of \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x} we have \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec H\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x}. |
30296 | 1124 |
Note that this representation looses information about the order of |
1125 |
parameters, and vacuous quantifiers vanish automatically. |
|
1126 |
||
1127 |
\end{itemize}% |
|
1128 |
\end{isamarkuptext}% |
|
1129 |
\isamarkuptrue% |
|
1130 |
% |
|
1131 |
\isadelimmlref |
|
1132 |
% |
|
1133 |
\endisadelimmlref |
|
1134 |
% |
|
1135 |
\isatagmlref |
|
1136 |
% |
|
1137 |
\begin{isamarkuptext}% |
|
1138 |
\begin{mldecls} |
|
30552
58db56278478
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
wenzelm
parents:
30355
diff
changeset
|
1139 |
\indexdef{}{ML}{Simplifier.norm\_hhf}\verb|Simplifier.norm_hhf: thm -> thm| \\ |
30296 | 1140 |
\end{mldecls} |
1141 |
||
1142 |
\begin{description} |
|
1143 |
||
30552
58db56278478
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
wenzelm
parents:
30355
diff
changeset
|
1144 |
\item \verb|Simplifier.norm_hhf|~\isa{thm} normalizes the given |
30296 | 1145 |
theorem according to the canonical form specified above. This is |
1146 |
occasionally helpful to repair some low-level tools that do not |
|
1147 |
handle Hereditary Harrop Formulae properly. |
|
1148 |
||
1149 |
\end{description}% |
|
1150 |
\end{isamarkuptext}% |
|
1151 |
\isamarkuptrue% |
|
1152 |
% |
|
1153 |
\endisatagmlref |
|
1154 |
{\isafoldmlref}% |
|
1155 |
% |
|
1156 |
\isadelimmlref |
|
1157 |
% |
|
1158 |
\endisadelimmlref |
|
1159 |
% |
|
1160 |
\isamarkupsubsection{Rule composition% |
|
1161 |
} |
|
1162 |
\isamarkuptrue% |
|
1163 |
% |
|
1164 |
\begin{isamarkuptext}% |
|
1165 |
The rule calculus of Isabelle/Pure provides two main inferences: |
|
1166 |
\hyperlink{inference.resolution}{\mbox{\isa{resolution}}} (i.e.\ back-chaining of rules) and |
|
1167 |
\hyperlink{inference.assumption}{\mbox{\isa{assumption}}} (i.e.\ closing a branch), both modulo |
|
1168 |
higher-order unification. There are also combined variants, notably |
|
40406 | 1169 |
\hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}resolution}}} and \hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isaliteral{5F}{\isacharunderscore}}resolution}}}. |
30296 | 1170 |
|
1171 |
To understand the all-important \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle, |
|
1172 |
we first consider raw \indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}} (modulo |
|
40406 | 1173 |
higher-order unification with substitution \isa{{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}): |
30296 | 1174 |
\[ |
40406 | 1175 |
\infer[(\indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}})]{\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}} |
1176 |
{\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{B{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C} & \isa{B{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}} |
|
30296 | 1177 |
\] |
1178 |
Here the conclusion of the first rule is unified with the premise of |
|
1179 |
the second; the resulting rule instance inherits the premises of the |
|
1180 |
first and conclusion of the second. Note that \isa{C} can again |
|
1181 |
consist of iterated implications. We can also permute the premises |
|
40406 | 1182 |
of the second rule back-and-forth in order to compose with \isa{B{\isaliteral{27}{\isacharprime}}} in any position (subsequently we shall always refer to |
30296 | 1183 |
position 1 w.l.o.g.). |
1184 |
||
1185 |
In \hyperlink{inference.composition}{\mbox{\isa{composition}}} the internal structure of the common |
|
40406 | 1186 |
part \isa{B} and \isa{B{\isaliteral{27}{\isacharprime}}} is not taken into account. For |
30296 | 1187 |
proper \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} we require \isa{B} to be atomic, |
40406 | 1188 |
and explicitly observe the structure \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{27}{\isacharprime}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x} of the premise of the second rule. The |
30296 | 1189 |
idea is to adapt the first rule by ``lifting'' it into this context, |
1190 |
by means of iterated application of the following inferences: |
|
1191 |
\[ |
|
40406 | 1192 |
\infer[(\indexdef{}{inference}{imp\_lift}\hypertarget{inference.imp-lift}{\hyperlink{inference.imp-lift}{\mbox{\isa{imp{\isaliteral{5F}{\isacharunderscore}}lift}}}})]{\isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}}}{\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}} |
30296 | 1193 |
\] |
1194 |
\[ |
|
40406 | 1195 |
\infer[(\indexdef{}{inference}{all\_lift}\hypertarget{inference.all-lift}{\hyperlink{inference.all-lift}{\mbox{\isa{all{\isaliteral{5F}{\isacharunderscore}}lift}}}})]{\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ B\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}}{\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a}} |
30296 | 1196 |
\] |
1197 |
By combining raw composition with lifting, we get full \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} as follows: |
|
1198 |
\[ |
|
1199 |
\infer[(\indexdef{}{inference}{resolution}\hypertarget{inference.resolution}{\hyperlink{inference.resolution}{\mbox{\isa{resolution}}}})] |
|
40406 | 1200 |
{\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}} |
30296 | 1201 |
{\begin{tabular}{l} |
40406 | 1202 |
\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a} \\ |
1203 |
\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{27}{\isacharprime}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C} \\ |
|
1204 |
\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ B\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} \\ |
|
30296 | 1205 |
\end{tabular}} |
1206 |
\] |
|
1207 |
||
1208 |
Continued resolution of rules allows to back-chain a problem towards |
|
1209 |
more and sub-problems. Branches are closed either by resolving with |
|
1210 |
a rule of 0 premises, or by producing a ``short-circuit'' within a |
|
1211 |
solved situation (again modulo unification): |
|
1212 |
\[ |
|
40406 | 1213 |
\infer[(\indexdef{}{inference}{assumption}\hypertarget{inference.assumption}{\hyperlink{inference.assumption}{\mbox{\isa{assumption}}}})]{\isa{C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}} |
1214 |
{\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C} & \isa{A{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3D}{\isacharequal}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}~~\text{(for some~\isa{i})}} |
|
30296 | 1215 |
\] |
1216 |
||
40406 | 1217 |
FIXME \indexdef{}{inference}{elim\_resolution}\hypertarget{inference.elim-resolution}{\hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}resolution}}}}, \indexdef{}{inference}{dest\_resolution}\hypertarget{inference.dest-resolution}{\hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isaliteral{5F}{\isacharunderscore}}resolution}}}}% |
30296 | 1218 |
\end{isamarkuptext}% |
1219 |
\isamarkuptrue% |
|
1220 |
% |
|
1221 |
\isadelimmlref |
|
1222 |
% |
|
1223 |
\endisadelimmlref |
|
1224 |
% |
|
1225 |
\isatagmlref |
|
1226 |
% |
|
1227 |
\begin{isamarkuptext}% |
|
1228 |
\begin{mldecls} |
|
46262 | 1229 |
\indexdef{}{ML infix}{RSN}\verb|infix RSN: thm * (int * thm) -> thm| \\ |
1230 |
\indexdef{}{ML infix}{RS}\verb|infix RS: thm * thm -> thm| \\ |
|
46256 | 1231 |
|
46262 | 1232 |
\indexdef{}{ML infix}{RLN}\verb|infix RLN: thm list * (int * thm list) -> thm list| \\ |
1233 |
\indexdef{}{ML infix}{RL}\verb|infix RL: thm list * thm list -> thm list| \\ |
|
46256 | 1234 |
|
46262 | 1235 |
\indexdef{}{ML infix}{MRS}\verb|infix MRS: thm list * thm -> thm| \\ |
1236 |
\indexdef{}{ML infix}{OF}\verb|infix OF: thm * thm list -> thm| \\ |
|
30296 | 1237 |
\end{mldecls} |
1238 |
||
1239 |
\begin{description} |
|
1240 |
||
46256 | 1241 |
\item \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RSN\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} resolves the conclusion of |
1242 |
\isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} with the \isa{i}-th premise of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}, |
|
1243 |
according to the \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle explained above. |
|
1244 |
Unless there is precisely one resolvent it raises exception \verb|THM|. |
|
1245 |
||
1246 |
This corresponds to the rule attribute \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} in Isar |
|
1247 |
source language. |
|
1248 |
||
1249 |
\item \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RS\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} abbreviates \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RS\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. |
|
30296 | 1250 |
|
46256 | 1251 |
\item \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RLN\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} joins lists of rules. For |
1252 |
every \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} in \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} in |
|
1253 |
\isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}, it resolves the conclusion of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} with |
|
1254 |
the \isa{i}-th premise of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}, accumulating multiple |
|
1255 |
results in one big list. Note that such strict enumerations of |
|
1256 |
higher-order unifications can be inefficient compared to the lazy |
|
1257 |
variant seen in elementary tactics like \verb|resolve_tac|. |
|
1258 |
||
1259 |
\item \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RL\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} abbreviates \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RLN\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. |
|
1260 |
||
1261 |
\item \isa{{\isaliteral{5B}{\isacharbrackleft}}rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}\ MRS\ rule} resolves \isa{rule\isaliteral{5C3C5E697375623E}{}\isactrlisub i} |
|
1262 |
against premise \isa{i} of \isa{rule}, for \isa{i\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}}. By working from right to left, newly emerging premises are |
|
1263 |
concatenated in the result, without interfering. |
|
1264 |
||
1265 |
\item \isa{rule\ OF\ rules} abbreviates \isa{rules\ MRS\ rule}. |
|
1266 |
||
1267 |
This corresponds to the rule attribute \hyperlink{attribute.OF}{\mbox{\isa{OF}}} in Isar |
|
1268 |
source language. |
|
30296 | 1269 |
|
1270 |
\end{description}% |
|
1271 |
\end{isamarkuptext}% |
|
1272 |
\isamarkuptrue% |
|
1273 |
% |
|
1274 |
\endisatagmlref |
|
1275 |
{\isafoldmlref}% |
|
1276 |
% |
|
1277 |
\isadelimmlref |
|
1278 |
% |
|
1279 |
\endisadelimmlref |
|
1280 |
% |
|
1281 |
\isadelimtheory |
|
1282 |
% |
|
1283 |
\endisadelimtheory |
|
1284 |
% |
|
1285 |
\isatagtheory |
|
1286 |
\isacommand{end}\isamarkupfalse% |
|
1287 |
% |
|
1288 |
\endisatagtheory |
|
1289 |
{\isafoldtheory}% |
|
1290 |
% |
|
1291 |
\isadelimtheory |
|
1292 |
% |
|
1293 |
\endisadelimtheory |
|
1294 |
\isanewline |
|
1295 |
\end{isabellebody}% |
|
1296 |
%%% Local Variables: |
|
1297 |
%%% mode: latex |
|
1298 |
%%% TeX-master: "root" |
|
1299 |
%%% End: |