23 \isamarkuptrue% |
23 \isamarkuptrue% |
24 % |
24 % |
25 \begin{isamarkuptext}% |
25 \begin{isamarkuptext}% |
26 The logical foundations of Isabelle/Isar are that of the Pure logic, |
26 The logical foundations of Isabelle/Isar are that of the Pure logic, |
27 which has been introduced as a Natural Deduction framework in |
27 which has been introduced as a Natural Deduction framework in |
28 \cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract setting of Pure Type Systems (PTS) |
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) |
29 \cite{Barendregt-Geuvers:2001}, although there are some key |
29 \cite{Barendregt-Geuvers:2001}, although there are some key |
30 differences in the specific treatment of simple types in |
30 differences in the specific treatment of simple types in |
31 Isabelle/Pure. |
31 Isabelle/Pure. |
32 |
32 |
33 Following type-theoretic parlance, the Pure logic consists of three |
33 Following type-theoretic parlance, the Pure logic consists of three |
34 levels of \isa{{\isasymlambda}}-calculus with corresponding arrows, \isa{{\isasymRightarrow}} for syntactic function space (terms depending on terms), \isa{{\isasymAnd}} for universal quantification (proofs depending on terms), and |
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{{\isasymLongrightarrow}} for implication (proofs depending on proofs). |
35 \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for implication (proofs depending on proofs). |
36 |
36 |
37 Derivations are relative to a logical theory, which declares type |
37 Derivations are relative to a logical theory, which declares type |
38 constructors, constants, and axioms. Theory declarations support |
38 constructors, constants, and axioms. Theory declarations support |
39 schematic polymorphism, which is strictly speaking outside the |
39 schematic polymorphism, which is strictly speaking outside the |
40 logic.\footnote{This is the deeper logical reason, why the theory |
40 logic.\footnote{This is the deeper logical reason, why the theory |
41 context \isa{{\isasymTheta}} is separate from the proof context \isa{{\isasymGamma}} |
41 context \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} is separate from the proof context \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} |
42 of the core calculus: type constructors, term constants, and facts |
42 of the core calculus: type constructors, term constants, and facts |
43 (proof constants) may involve arbitrary type schemes, but the type |
43 (proof constants) may involve arbitrary type schemes, but the type |
44 of a locally fixed term parameter is also fixed!}% |
44 of a locally fixed term parameter is also fixed!}% |
45 \end{isamarkuptext}% |
45 \end{isamarkuptext}% |
46 \isamarkuptrue% |
46 \isamarkuptrue% |
52 \begin{isamarkuptext}% |
52 \begin{isamarkuptext}% |
53 The language of types is an uninterpreted order-sorted first-order |
53 The language of types is an uninterpreted order-sorted first-order |
54 algebra; types are qualified by ordered type classes. |
54 algebra; types are qualified by ordered type classes. |
55 |
55 |
56 \medskip A \emph{type class} is an abstract syntactic entity |
56 \medskip A \emph{type class} is an abstract syntactic entity |
57 declared in the theory context. The \emph{subclass relation} \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}} is specified by stating an acyclic |
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 |
58 generating relation; the transitive closure is maintained |
58 generating relation; the transitive closure is maintained |
59 internally. The resulting relation is an ordering: reflexive, |
59 internally. The resulting relation is an ordering: reflexive, |
60 transitive, and antisymmetric. |
60 transitive, and antisymmetric. |
61 |
61 |
62 A \emph{sort} is a list of type classes written as \isa{s\ {\isacharequal}\ {\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, it represents symbolic intersection. Notationally, the |
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 |
63 curly braces are omitted for singleton intersections, i.e.\ any |
63 curly braces are omitted for singleton intersections, i.e.\ any |
64 class \isa{c} may be read as a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering |
64 class \isa{c} may be read as a sort \isa{{\isaliteral{7B}{\isacharbraceleft}}c{\isaliteral{7D}{\isacharbraceright}}}. The ordering |
65 on type classes is extended to sorts according to the meaning of |
65 on type classes is extended to sorts according to the meaning of |
66 intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection \isa{{\isacharbraceleft}{\isacharbraceright}} refers to |
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 |
67 the universal sort, which is the largest element wrt.\ the sort |
67 the universal sort, which is the largest element wrt.\ the sort |
68 order. Thus \isa{{\isacharbraceleft}{\isacharbraceright}} represents the ``full sort'', not the |
68 order. Thus \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} represents the ``full sort'', not the |
69 empty one! The intersection of all (finitely many) classes declared |
69 empty one! The intersection of all (finitely many) classes declared |
70 in the current theory is the least element wrt.\ the sort ordering. |
70 in the current theory is the least element wrt.\ the sort ordering. |
71 |
71 |
72 \medskip A \emph{fixed type variable} is a pair of a basic name |
72 \medskip A \emph{fixed type variable} is a pair of a basic name |
73 (starting with a \isa{{\isacharprime}} character) and a sort constraint, e.g.\ |
73 (starting with a \isa{{\isaliteral{27}{\isacharprime}}} character) and a sort constraint, e.g.\ |
74 \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}. |
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}. |
75 A \emph{schematic type variable} is a pair of an indexname and a |
75 A \emph{schematic type variable} is a pair of an indexname and a |
76 sort constraint, e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually |
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{{\isacharquery}{\isasymalpha}\isactrlisub s}. |
77 printed as \isa{{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s}. |
78 |
78 |
79 Note that \emph{all} syntactic components contribute to the identity |
79 Note that \emph{all} syntactic components contribute to the identity |
80 of type variables: basic name, index, and sort constraint. The core |
80 of type variables: basic name, index, and sort constraint. The core |
81 logic handles type variables with the same name but different sorts |
81 logic handles type variables with the same name but different sorts |
82 as different, although the type-inference layer (which is outside |
82 as different, although the type-inference layer (which is outside |
83 the core) rejects anything like that. |
83 the core) rejects anything like that. |
84 |
84 |
85 A \emph{type constructor} \isa{{\isasymkappa}} is a \isa{k}-ary operator |
85 A \emph{type constructor} \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is a \isa{k}-ary operator |
86 on types declared in the theory. Type constructor application is |
86 on types declared in the theory. Type constructor application is |
87 written postfix as \isa{{\isacharparenleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub k{\isacharparenright}{\isasymkappa}}. For |
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\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ \isa{prop} |
88 \isa{k\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ \isa{prop} |
89 instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses |
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{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}. |
90 are omitted, e.g.\ \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list} instead of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}list}. |
91 Further notation is provided for specific constructors, notably the |
91 Further notation is provided for specific constructors, notably the |
92 right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}. |
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}. |
93 |
93 |
94 The logical category \emph{type} is defined inductively over type |
94 The logical category \emph{type} is defined inductively over type |
95 variables and type constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}{\isasymkappa}}. |
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}}}. |
96 |
96 |
97 A \emph{type abbreviation} is a syntactic definition \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} of an arbitrary type expression \isa{{\isasymtau}} over |
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{\isactrlvec {\isasymalpha}}. Type abbreviations appear as type |
98 variables \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}. Type abbreviations appear as type |
99 constructors in the syntax, but are expanded before entering the |
99 constructors in the syntax, but are expanded before entering the |
100 logical core. |
100 logical core. |
101 |
101 |
102 A \emph{type arity} declares the image behavior of a type |
102 A \emph{type arity} declares the image behavior of a type |
103 constructor wrt.\ the algebra of sorts: \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}{\isasymkappa}} is |
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{{\isasymtau}\isactrlisub i} is |
104 of sort \isa{s} if every argument type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i} is |
105 of sort \isa{s\isactrlisub i}. Arity declarations are implicitly |
105 of sort \isa{s\isaliteral{5C3C5E697375623E}{}\isactrlisub i}. Arity declarations are implicitly |
106 completed, i.e.\ \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}. |
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}. |
107 |
107 |
108 \medskip The sort algebra is always maintained as \emph{coregular}, |
108 \medskip The sort algebra is always maintained as \emph{coregular}, |
109 which means that type arities are consistent with the subclass |
109 which means that type arities are consistent with the subclass |
110 relation: for any type constructor \isa{{\isasymkappa}}, and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, and arities \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} and \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} holds \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} component-wise. |
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. |
111 |
111 |
112 The key property of a coregular order-sorted algebra is that sort |
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 |
113 constraints can be solved in a most general fashion: for each type |
114 constructor \isa{{\isasymkappa}} and sort \isa{s} there is a most general |
114 constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} and sort \isa{s} there is a most general |
115 vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such |
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{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}{\isasymkappa}} is of sort \isa{s}. |
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}. |
117 Consequently, type unification has most general solutions (modulo |
117 Consequently, type unification has most general solutions (modulo |
118 equivalence of sorts), so type-inference produces primary types as |
118 equivalence of sorts), so type-inference produces primary types as |
119 expected \cite{nipkow-prehofer}.% |
119 expected \cite{nipkow-prehofer}.% |
120 \end{isamarkuptext}% |
120 \end{isamarkuptext}% |
121 \isamarkuptrue% |
121 \isamarkuptrue% |
152 \item Type \verb|sort| represents sorts, i.e.\ finite |
152 \item Type \verb|sort| represents sorts, i.e.\ finite |
153 intersections of classes. The empty list \verb|[]: sort| refers to |
153 intersections of classes. The empty list \verb|[]: sort| refers to |
154 the empty class intersection, i.e.\ the ``full sort''. |
154 the empty class intersection, i.e.\ the ``full sort''. |
155 |
155 |
156 \item Type \verb|arity| represents type arities. A triple |
156 \item Type \verb|arity| represents type arities. A triple |
157 \isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}\ {\isacharcolon}\ arity} represents \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} as described above. |
157 \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. |
158 |
158 |
159 \item Type \verb|typ| represents types; this is a datatype with |
159 \item Type \verb|typ| represents types; this is a datatype with |
160 constructors \verb|TFree|, \verb|TVar|, \verb|Type|. |
160 constructors \verb|TFree|, \verb|TVar|, \verb|Type|. |
161 |
161 |
162 \item \verb|Term.map_atyps|~\isa{f\ {\isasymtau}} applies the mapping \isa{f} to all atomic types (\verb|TFree|, \verb|TVar|) occurring in |
162 \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 |
163 \isa{{\isasymtau}}. |
163 \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}. |
164 |
164 |
165 \item \verb|Term.fold_atyps|~\isa{f\ {\isasymtau}} iterates the operation |
165 \item \verb|Term.fold_atyps|~\isa{f\ {\isaliteral{5C3C7461753E}{\isasymtau}}} iterates the operation |
166 \isa{f} over all occurrences of atomic types (\verb|TFree|, \verb|TVar|) in \isa{{\isasymtau}}; the type structure is traversed from left to |
166 \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 |
167 right. |
167 right. |
168 |
168 |
169 \item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}} |
169 \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}}} |
170 tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}. |
170 tests the subsort relation \isa{s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}. |
171 |
171 |
172 \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether type |
172 \item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type |
173 \isa{{\isasymtau}} is of sort \isa{s}. |
173 \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}. |
174 |
174 |
175 \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a new |
175 \item \verb|Sign.add_types|~\isa{{\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 new |
176 type constructors \isa{{\isasymkappa}} with \isa{k} arguments and |
176 type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and |
177 optional mixfix syntax. |
177 optional mixfix syntax. |
178 |
178 |
179 \item \verb|Sign.add_type_abbrev|~\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}}. |
179 \item \verb|Sign.add_type_abbrev|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} 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}}}. |
180 |
180 |
181 \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares a new class \isa{c}, together with class |
181 \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 |
182 relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}. |
182 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}. |
183 |
183 |
184 \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares the class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}. |
184 \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}}}. |
185 |
185 |
186 \item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares |
186 \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 |
187 the arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}. |
187 the arity \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}s}. |
188 |
188 |
189 \end{description}% |
189 \end{description}% |
190 \end{isamarkuptext}% |
190 \end{isamarkuptext}% |
191 \isamarkuptrue% |
191 \isamarkuptrue% |
192 % |
192 % |
280 can be managed as a separate context, that is maintained as a stack |
280 can be managed as a separate context, that is maintained as a stack |
281 of hypothetical binders. The core logic operates on closed terms, |
281 of hypothetical binders. The core logic operates on closed terms, |
282 without any loose variables. |
282 without any loose variables. |
283 |
283 |
284 A \emph{fixed variable} is a pair of a basic name and a type, e.g.\ |
284 A \emph{fixed variable} is a pair of a basic name and a type, e.g.\ |
285 \isa{{\isacharparenleft}x{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed \isa{x\isactrlisub {\isasymtau}} here. A |
285 \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 |
286 \emph{schematic variable} is a pair of an indexname and a type, |
286 \emph{schematic variable} is a pair of an indexname and a type, |
287 e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is likewise printed as \isa{{\isacharquery}x\isactrlisub {\isasymtau}}. |
287 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}}}. |
288 |
288 |
289 \medskip A \emph{constant} is a pair of a basic name and a type, |
289 \medskip A \emph{constant} is a pair of a basic name and a type, |
290 e.g.\ \isa{{\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{c\isactrlisub {\isasymtau}} |
290 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}}} |
291 here. Constants are declared in the context as polymorphic families |
291 here. Constants are declared in the context as polymorphic families |
292 \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that all substitution instances \isa{c\isactrlisub {\isasymtau}} for \isa{{\isasymtau}\ {\isacharequal}\ {\isasymsigma}{\isasymvartheta}} are valid. |
292 \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. |
293 |
293 |
294 The vector of \emph{type arguments} of constant \isa{c\isactrlisub {\isasymtau}} wrt.\ |
294 The vector of \emph{type arguments} of constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} wrt.\ |
295 the declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is defined as the codomain of the |
295 the declaration \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} is defined as the codomain of the |
296 matcher \isa{{\isasymvartheta}\ {\isacharequal}\ {\isacharbraceleft}{\isacharquery}{\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymmapsto}\ {\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isacharquery}{\isasymalpha}\isactrlisub n\ {\isasymmapsto}\ {\isasymtau}\isactrlisub n{\isacharbraceright}} presented in |
296 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 |
297 canonical order \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}}, corresponding to the |
297 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 |
298 left-to-right occurrences of the \isa{{\isasymalpha}\isactrlisub i} in \isa{{\isasymsigma}}. |
298 left-to-right occurrences of the \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i} in \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. |
299 Within a given theory context, there is a one-to-one correspondence |
299 Within a given theory context, there is a one-to-one correspondence |
300 between any constant \isa{c\isactrlisub {\isasymtau}} and the application \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} of its type arguments. For example, with \isa{plus\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}}, the instance \isa{plus\isactrlbsub nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\isactrlesub } corresponds to |
300 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 |
301 \isa{plus{\isacharparenleft}nat{\isacharparenright}}. |
301 \isa{plus{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{29}{\isacharparenright}}}. |
302 |
302 |
303 Constant declarations \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} may contain sort constraints |
303 Constant declarations \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} may contain sort constraints |
304 for type variables in \isa{{\isasymsigma}}. These are observed by |
304 for type variables in \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. These are observed by |
305 type-inference as expected, but \emph{ignored} by the core logic. |
305 type-inference as expected, but \emph{ignored} by the core logic. |
306 This means the primitive logic is able to reason with instances of |
306 This means the primitive logic is able to reason with instances of |
307 polymorphic constants that the user-level type-checker would reject |
307 polymorphic constants that the user-level type-checker would reject |
308 due to violation of type class restrictions. |
308 due to violation of type class restrictions. |
309 |
309 |
310 \medskip An \emph{atomic term} is either a variable or constant. |
310 \medskip An \emph{atomic term} is either a variable or constant. |
311 The logical category \emph{term} is defined inductively over atomic |
311 The logical category \emph{term} is defined inductively over atomic |
312 terms, with abstraction and application as follows: \isa{t\ {\isacharequal}\ b\ {\isacharbar}\ x\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isacharquery}x\isactrlisub {\isasymtau}\ {\isacharbar}\ c\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ t\ {\isacharbar}\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}}. Parsing and printing takes care of |
312 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 |
313 converting between an external representation with named bound |
313 converting between an external representation with named bound |
314 variables. Subsequently, we shall use the latter notation instead |
314 variables. Subsequently, we shall use the latter notation instead |
315 of internal de-Bruijn representation. |
315 of internal de-Bruijn representation. |
316 |
316 |
317 The inductive relation \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} assigns a (unique) type to a |
317 The inductive relation \isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} assigns a (unique) type to a |
318 term according to the structure of atomic terms, abstractions, and |
318 term according to the structure of atomic terms, abstractions, and |
319 applicatins: |
319 applicatins: |
320 \[ |
320 \[ |
321 \infer{\isa{a\isactrlisub {\isasymtau}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}{} |
321 \infer{\isa{a\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}}{} |
322 \qquad |
322 \qquad |
323 \infer{\isa{{\isacharparenleft}{\isasymlambda}x\isactrlsub {\isasymtau}{\isachardot}\ t{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}} |
323 \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}}}} |
324 \qquad |
324 \qquad |
325 \infer{\isa{t\ u\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}} & \isa{u\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}} |
325 \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}}}} |
326 \] |
326 \] |
327 A \emph{well-typed term} is a term that can be typed according to these rules. |
327 A \emph{well-typed term} is a term that can be typed according to these rules. |
328 |
328 |
329 Typing information can be omitted: type-inference is able to |
329 Typing information can be omitted: type-inference is able to |
330 reconstruct the most general type of a raw term, while assigning |
330 reconstruct the most general type of a raw term, while assigning |
331 most general types to all of its variables and constants. |
331 most general types to all of its variables and constants. |
332 Type-inference depends on a context of type constraints for fixed |
332 Type-inference depends on a context of type constraints for fixed |
333 variables, and declarations for polymorphic constants. |
333 variables, and declarations for polymorphic constants. |
334 |
334 |
335 The identity of atomic terms consists both of the name and the type |
335 The identity of atomic terms consists both of the name and the type |
336 component. This means that different variables \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{1}}\isactrlesub } and \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{2}}\isactrlesub } may become the same after |
336 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 |
337 type instantiation. Type-inference rejects variables of the same |
337 type instantiation. Type-inference rejects variables of the same |
338 name, but different types. In contrast, mixed instances of |
338 name, but different types. In contrast, mixed instances of |
339 polymorphic constants occur routinely. |
339 polymorphic constants occur routinely. |
340 |
340 |
341 \medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} |
341 \medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} |
342 is the set of type variables occurring in \isa{t}, but not in |
342 is the set of type variables occurring in \isa{t}, but not in |
343 its type \isa{{\isasymsigma}}. This means that the term implicitly depends |
343 its type \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. This means that the term implicitly depends |
344 on type arguments that are not accounted in the result type, i.e.\ |
344 on type arguments that are not accounted in the result type, i.e.\ |
345 there are different type instances \isa{t{\isasymvartheta}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} and |
345 there are different type instances \isa{t{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} and |
346 \isa{t{\isasymvartheta}{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with the same type. This slightly |
346 \isa{t{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with the same type. This slightly |
347 pathological situation notoriously demands additional care. |
347 pathological situation notoriously demands additional care. |
348 |
348 |
349 \medskip A \emph{term abbreviation} is a syntactic definition \isa{c\isactrlisub {\isasymsigma}\ {\isasymequiv}\ t} of a closed term \isa{t} of type \isa{{\isasymsigma}}, |
349 \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}}}, |
350 without any hidden polymorphism. A term abbreviation looks like a |
350 without any hidden polymorphism. A term abbreviation looks like a |
351 constant in the syntax, but is expanded before entering the logical |
351 constant in the syntax, but is expanded before entering the logical |
352 core. Abbreviations are usually reverted when printing terms, using |
352 core. Abbreviations are usually reverted when printing terms, using |
353 \isa{t\ {\isasymrightarrow}\ c\isactrlisub {\isasymsigma}} as rules for higher-order rewriting. |
353 \isa{t\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} as rules for higher-order rewriting. |
354 |
354 |
355 \medskip Canonical operations on \isa{{\isasymlambda}}-terms include \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion: \isa{{\isasymalpha}}-conversion refers to capture-free |
355 \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 |
356 renaming of bound variables; \isa{{\isasymbeta}}-conversion contracts an |
356 renaming of bound variables; \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion contracts an |
357 abstraction applied to an argument term, substituting the argument |
357 abstraction applied to an argument term, substituting the argument |
358 in the body: \isa{{\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}a} becomes \isa{b{\isacharbrackleft}a{\isacharslash}x{\isacharbrackright}}; \isa{{\isasymeta}}-conversion contracts vacuous application-abstraction: \isa{{\isasymlambda}x{\isachardot}\ f\ x} becomes \isa{f}, provided that the bound variable |
358 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 |
359 does not occur in \isa{f}. |
359 does not occur in \isa{f}. |
360 |
360 |
361 Terms are normally treated modulo \isa{{\isasymalpha}}-conversion, which is |
361 Terms are normally treated modulo \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-conversion, which is |
362 implicit in the de-Bruijn representation. Names for bound variables |
362 implicit in the de-Bruijn representation. Names for bound variables |
363 in abstractions are maintained separately as (meaningless) comments, |
363 in abstractions are maintained separately as (meaningless) comments, |
364 mostly for parsing and printing. Full \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion is |
364 mostly for parsing and printing. Full \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion is |
365 commonplace in various standard operations (\secref{sec:obj-rules}) |
365 commonplace in various standard operations (\secref{sec:obj-rules}) |
366 that are based on higher-order unification and matching.% |
366 that are based on higher-order unification and matching.% |
367 \end{isamarkuptext}% |
367 \end{isamarkuptext}% |
368 \isamarkuptrue% |
368 \isamarkuptrue% |
369 % |
369 % |
511 % |
511 % |
512 \begin{isamarkuptext}% |
512 \begin{isamarkuptext}% |
513 A \emph{proposition} is a well-typed term of type \isa{prop}, a |
513 A \emph{proposition} is a well-typed term of type \isa{prop}, a |
514 \emph{theorem} is a proven proposition (depending on a context of |
514 \emph{theorem} is a proven proposition (depending on a context of |
515 hypotheses and the background theory). Primitive inferences include |
515 hypotheses and the background theory). Primitive inferences include |
516 plain Natural Deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework. There is also a builtin |
516 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 |
517 notion of equality/equivalence \isa{{\isasymequiv}}.% |
517 notion of equality/equivalence \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}.% |
518 \end{isamarkuptext}% |
518 \end{isamarkuptext}% |
519 \isamarkuptrue% |
519 \isamarkuptrue% |
520 % |
520 % |
521 \isamarkupsubsection{Primitive connectives and rules \label{sec:prim-rules}% |
521 \isamarkupsubsection{Primitive connectives and rules \label{sec:prim-rules}% |
522 } |
522 } |
523 \isamarkuptrue% |
523 \isamarkuptrue% |
524 % |
524 % |
525 \begin{isamarkuptext}% |
525 \begin{isamarkuptext}% |
526 The theory \isa{Pure} contains constant declarations for the |
526 The theory \isa{Pure} contains constant declarations for the |
527 primitive connectives \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and \isa{{\isasymequiv}} of |
527 primitive connectives \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}, \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}, and \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} of |
528 the logical framework, see \figref{fig:pure-connectives}. The |
528 the logical framework, see \figref{fig:pure-connectives}. The |
529 derivability judgment \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} is |
529 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 |
530 defined inductively by the primitive inferences given in |
530 defined inductively by the primitive inferences given in |
531 \figref{fig:prim-rules}, with the global restriction that the |
531 \figref{fig:prim-rules}, with the global restriction that the |
532 hypotheses must \emph{not} contain any schematic variables. The |
532 hypotheses must \emph{not} contain any schematic variables. The |
533 builtin equality is conceptually axiomatized as shown in |
533 builtin equality is conceptually axiomatized as shown in |
534 \figref{fig:pure-equality}, although the implementation works |
534 \figref{fig:pure-equality}, although the implementation works |
535 directly with derived inferences. |
535 directly with derived inferences. |
536 |
536 |
537 \begin{figure}[htb] |
537 \begin{figure}[htb] |
538 \begin{center} |
538 \begin{center} |
539 \begin{tabular}{ll} |
539 \begin{tabular}{ll} |
540 \isa{all\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymRightarrow}\ prop{\isacharparenright}\ {\isasymRightarrow}\ prop} & universal quantification (binder \isa{{\isasymAnd}}) \\ |
540 \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}}}) \\ |
541 \isa{{\isasymLongrightarrow}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & implication (right associative infix) \\ |
541 \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & implication (right associative infix) \\ |
542 \isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & equality relation (infix) \\ |
542 \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) \\ |
543 \end{tabular} |
543 \end{tabular} |
544 \caption{Primitive connectives of Pure}\label{fig:pure-connectives} |
544 \caption{Primitive connectives of Pure}\label{fig:pure-connectives} |
545 \end{center} |
545 \end{center} |
546 \end{figure} |
546 \end{figure} |
547 |
547 |
548 \begin{figure}[htb] |
548 \begin{figure}[htb] |
549 \begin{center} |
549 \begin{center} |
550 \[ |
550 \[ |
551 \infer[\isa{{\isacharparenleft}axiom{\isacharparenright}}]{\isa{{\isasymturnstile}\ A}}{\isa{A\ {\isasymin}\ {\isasymTheta}}} |
551 \infer[\isa{{\isaliteral{28}{\isacharparenleft}}axiom{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{\isa{A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C54686574613E}{\isasymTheta}}}} |
552 \qquad |
552 \qquad |
553 \infer[\isa{{\isacharparenleft}assume{\isacharparenright}}]{\isa{A\ {\isasymturnstile}\ A}}{} |
553 \infer[\isa{{\isaliteral{28}{\isacharparenleft}}assume{\isaliteral{29}{\isacharparenright}}}]{\isa{A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{} |
554 \] |
554 \] |
555 \[ |
555 \[ |
556 \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isasymdash}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}} |
556 \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}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}}}} |
557 \qquad |
557 \qquad |
558 \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isasymdash}elim{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}a{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}} |
558 \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}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}}}} |
559 \] |
559 \] |
560 \[ |
560 \[ |
561 \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isasymdash}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}} |
561 \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}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}} |
562 \qquad |
562 \qquad |
563 \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isasymdash}elim{\isacharparenright}}]{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymunion}\ {\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ B}}{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B} & \isa{{\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ A}} |
563 \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}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}} |
564 \] |
564 \] |
565 \caption{Primitive inferences of Pure}\label{fig:prim-rules} |
565 \caption{Primitive inferences of Pure}\label{fig:prim-rules} |
566 \end{center} |
566 \end{center} |
567 \end{figure} |
567 \end{figure} |
568 |
568 |
569 \begin{figure}[htb] |
569 \begin{figure}[htb] |
570 \begin{center} |
570 \begin{center} |
571 \begin{tabular}{ll} |
571 \begin{tabular}{ll} |
572 \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ a\ {\isasymequiv}\ b{\isacharbrackleft}a{\isacharbrackright}} & \isa{{\isasymbeta}}-conversion \\ |
572 \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 \\ |
573 \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity \\ |
573 \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x} & reflexivity \\ |
574 \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ y\ {\isasymLongrightarrow}\ P\ x\ {\isasymLongrightarrow}\ P\ y} & substitution \\ |
574 \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ y} & substitution \\ |
575 \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ f\ x\ {\isasymequiv}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isasymequiv}\ g} & extensionality \\ |
575 \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 \\ |
576 \isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & logical equivalence \\ |
576 \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 \\ |
577 \end{tabular} |
577 \end{tabular} |
578 \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality} |
578 \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality} |
579 \end{center} |
579 \end{center} |
580 \end{figure} |
580 \end{figure} |
581 |
581 |
582 The introduction and elimination rules for \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} are analogous to formation of dependently typed \isa{{\isasymlambda}}-terms representing the underlying proof objects. Proof terms |
582 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 |
583 are irrelevant in the Pure logic, though; they cannot occur within |
583 are irrelevant in the Pure logic, though; they cannot occur within |
584 propositions. The system provides a runtime option to record |
584 propositions. The system provides a runtime option to record |
585 explicit proof terms for primitive inferences. Thus all three |
585 explicit proof terms for primitive inferences. Thus all three |
586 levels of \isa{{\isasymlambda}}-calculus become explicit: \isa{{\isasymRightarrow}} for |
586 levels of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus become explicit: \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} for |
587 terms, and \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} for proofs (cf.\ |
587 terms, and \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for proofs (cf.\ |
588 \cite{Berghofer-Nipkow:2000:TPHOL}). |
588 \cite{Berghofer-Nipkow:2000:TPHOL}). |
589 |
589 |
590 Observe that locally fixed parameters (as in \isa{{\isasymAnd}{\isasymdash}intro}) need not be recorded in the hypotheses, because |
590 Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro}) need not be recorded in the hypotheses, because |
591 the simple syntactic types of Pure are always inhabitable. |
591 the simple syntactic types of Pure are always inhabitable. |
592 ``Assumptions'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} for type-membership are only |
592 ``Assumptions'' \isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} for type-membership are only |
593 present as long as some \isa{x\isactrlisub {\isasymtau}} occurs in the statement |
593 present as long as some \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} occurs in the statement |
594 body.\footnote{This is the key difference to ``\isa{{\isasymlambda}HOL}'' in |
594 body.\footnote{This is the key difference to ``\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}HOL}'' in |
595 the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses |
595 the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses |
596 \isa{x\ {\isacharcolon}\ A} are treated uniformly for propositions and types.} |
596 \isa{x\ {\isaliteral{3A}{\isacharcolon}}\ A} are treated uniformly for propositions and types.} |
597 |
597 |
598 \medskip The axiomatization of a theory is implicitly closed by |
598 \medskip The axiomatization of a theory is implicitly closed by |
599 forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} holds for any substitution instance of an axiom |
599 forming all instances of type and term variables: \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} holds for any substitution instance of an axiom |
600 \isa{{\isasymturnstile}\ A}. By pushing substitutions through derivations |
600 \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}. By pushing substitutions through derivations |
601 inductively, we also get admissible \isa{generalize} and \isa{instantiate} rules as shown in \figref{fig:subst-rules}. |
601 inductively, we also get admissible \isa{generalize} and \isa{instantiate} rules as shown in \figref{fig:subst-rules}. |
602 |
602 |
603 \begin{figure}[htb] |
603 \begin{figure}[htb] |
604 \begin{center} |
604 \begin{center} |
605 \[ |
605 \[ |
606 \infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} & \isa{{\isasymalpha}\ {\isasymnotin}\ {\isasymGamma}}} |
606 \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}}}} |
607 \quad |
607 \quad |
608 \infer[\quad\isa{{\isacharparenleft}generalize{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}} |
608 \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}}}} |
609 \] |
609 \] |
610 \[ |
610 \[ |
611 \infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymtau}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}} |
611 \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}}}} |
612 \quad |
612 \quad |
613 \infer[\quad\isa{{\isacharparenleft}instantiate{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}t{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}} |
613 \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}}}} |
614 \] |
614 \] |
615 \caption{Admissible substitution rules}\label{fig:subst-rules} |
615 \caption{Admissible substitution rules}\label{fig:subst-rules} |
616 \end{center} |
616 \end{center} |
617 \end{figure} |
617 \end{figure} |
618 |
618 |
619 Note that \isa{instantiate} does not require an explicit |
619 Note that \isa{instantiate} does not require an explicit |
620 side-condition, because \isa{{\isasymGamma}} may never contain schematic |
620 side-condition, because \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} may never contain schematic |
621 variables. |
621 variables. |
622 |
622 |
623 In principle, variables could be substituted in hypotheses as well, |
623 In principle, variables could be substituted in hypotheses as well, |
624 but this would disrupt the monotonicity of reasoning: deriving |
624 but this would disrupt the monotonicity of reasoning: deriving |
625 \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymturnstile}\ B{\isasymvartheta}} from \isa{{\isasymGamma}\ {\isasymturnstile}\ B} is |
625 \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} from \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B} is |
626 correct, but \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymsupseteq}\ {\isasymGamma}} does not necessarily hold: |
626 correct, but \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} does not necessarily hold: |
627 the result belongs to a different proof context. |
627 the result belongs to a different proof context. |
628 |
628 |
629 \medskip An \emph{oracle} is a function that produces axioms on the |
629 \medskip An \emph{oracle} is a function that produces axioms on the |
630 fly. Logically, this is an instance of the \isa{axiom} rule |
630 fly. Logically, this is an instance of the \isa{axiom} rule |
631 (\figref{fig:prim-rules}), but there is an operational difference. |
631 (\figref{fig:prim-rules}), but there is an operational difference. |
635 Axiomatizations should be limited to the bare minimum, typically as |
635 Axiomatizations should be limited to the bare minimum, typically as |
636 part of the initial logical basis of an object-logic formalization. |
636 part of the initial logical basis of an object-logic formalization. |
637 Later on, theories are usually developed in a strictly definitional |
637 Later on, theories are usually developed in a strictly definitional |
638 fashion, by stating only certain equalities over new constants. |
638 fashion, by stating only certain equalities over new constants. |
639 |
639 |
640 A \emph{simple definition} consists of a constant declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} together with an axiom \isa{{\isasymturnstile}\ c\ {\isasymequiv}\ t}, where \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is a closed term without any hidden polymorphism. The RHS |
640 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 |
641 may depend on further defined constants, but not \isa{c} itself. |
641 may depend on further defined constants, but not \isa{c} itself. |
642 Definitions of functions may be presented as \isa{c\ \isactrlvec x\ {\isasymequiv}\ t} instead of the puristic \isa{c\ {\isasymequiv}\ {\isasymlambda}\isactrlvec x{\isachardot}\ t}. |
642 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}. |
643 |
643 |
644 An \emph{overloaded definition} consists of a collection of axioms |
644 An \emph{overloaded definition} consists of a collection of axioms |
645 for the same constant, with zero or one equations \isa{c{\isacharparenleft}{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}{\isacharparenright}\ {\isasymequiv}\ t} for each type constructor \isa{{\isasymkappa}} (for |
645 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 |
646 distinct variables \isa{\isactrlvec {\isasymalpha}}). The RHS may mention |
646 distinct variables \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}). The RHS may mention |
647 previously defined constants as above, or arbitrary constants \isa{d{\isacharparenleft}{\isasymalpha}\isactrlisub i{\isacharparenright}} for some \isa{{\isasymalpha}\isactrlisub i} projected from \isa{\isactrlvec {\isasymalpha}}. Thus overloaded definitions essentially work by |
647 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 |
648 primitive recursion over the syntactic structure of a single type |
648 primitive recursion over the syntactic structure of a single type |
649 argument. See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.% |
649 argument. See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.% |
650 \end{isamarkuptext}% |
650 \end{isamarkuptext}% |
651 \isamarkuptrue% |
651 \isamarkuptrue% |
652 % |
652 % |
713 to a result are recorded in any case. |
713 to a result are recorded in any case. |
714 |
714 |
715 \item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim| |
715 \item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim| |
716 correspond to the primitive inferences of \figref{fig:prim-rules}. |
716 correspond to the primitive inferences of \figref{fig:prim-rules}. |
717 |
717 |
718 \item \verb|Thm.generalize|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharcomma}\ \isactrlvec x{\isacharparenright}} |
718 \item \verb|Thm.generalize|~\isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}} |
719 corresponds to the \isa{generalize} rules of |
719 corresponds to the \isa{generalize} rules of |
720 \figref{fig:subst-rules}. Here collections of type and term |
720 \figref{fig:subst-rules}. Here collections of type and term |
721 variables are generalized simultaneously, specified by the given |
721 variables are generalized simultaneously, specified by the given |
722 basic names. |
722 basic names. |
723 |
723 |
724 \item \verb|Thm.instantiate|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}\isactrlisub s{\isacharcomma}\ \isactrlvec x\isactrlisub {\isasymtau}{\isacharparenright}} corresponds to the \isa{instantiate} rules |
724 \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 |
725 of \figref{fig:subst-rules}. Type variables are substituted before |
725 of \figref{fig:subst-rules}. Type variables are substituted before |
726 term variables. Note that the types in \isa{\isactrlvec x\isactrlisub {\isasymtau}} |
726 term variables. Note that the types in \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} |
727 refer to the instantiated versions. |
727 refer to the instantiated versions. |
728 |
728 |
729 \item \verb|Thm.add_axiom|~\isa{{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}\ thy} declares an |
729 \item \verb|Thm.add_axiom|~\isa{{\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}\ thy} declares an |
730 arbitrary proposition as axiom, and retrieves it as a theorem from |
730 arbitrary proposition as axiom, and retrieves it as a theorem from |
731 the resulting theory, cf.\ \isa{axiom} in |
731 the resulting theory, cf.\ \isa{axiom} in |
732 \figref{fig:prim-rules}. Note that the low-level representation in |
732 \figref{fig:prim-rules}. Note that the low-level representation in |
733 the axiom table may differ slightly from the returned theorem. |
733 the axiom table may differ slightly from the returned theorem. |
734 |
734 |
735 \item \verb|Thm.add_oracle|~\isa{{\isacharparenleft}binding{\isacharcomma}\ oracle{\isacharparenright}} produces a named |
735 \item \verb|Thm.add_oracle|~\isa{{\isaliteral{28}{\isacharparenleft}}binding{\isaliteral{2C}{\isacharcomma}}\ oracle{\isaliteral{29}{\isacharparenright}}} produces a named |
736 oracle rule, essentially generating arbitrary axioms on the fly, |
736 oracle rule, essentially generating arbitrary axioms on the fly, |
737 cf.\ \isa{axiom} in \figref{fig:prim-rules}. |
737 cf.\ \isa{axiom} in \figref{fig:prim-rules}. |
738 |
738 |
739 \item \verb|Thm.add_def|~\isa{unchecked\ overloaded\ {\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}} states a definitional axiom for an existing constant |
739 \item \verb|Thm.add_def|~\isa{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 |
740 \isa{c}. Dependencies are recorded via \verb|Theory.add_deps|, |
740 \isa{c}. Dependencies are recorded via \verb|Theory.add_deps|, |
741 unless the \isa{unchecked} option is set. Note that the |
741 unless the \isa{unchecked} option is set. Note that the |
742 low-level representation in the axiom table may differ slightly from |
742 low-level representation in the axiom table may differ slightly from |
743 the returned theorem. |
743 the returned theorem. |
744 |
744 |
745 \item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a named specification |
745 \item \verb|Theory.add_deps|~\isa{name\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} declares dependencies of a named specification |
746 for constant \isa{c\isactrlisub {\isasymtau}}, relative to existing |
746 for constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}, relative to existing |
747 specifications for constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}. |
747 specifications for constants \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}. |
748 |
748 |
749 \end{description}% |
749 \end{description}% |
750 \end{isamarkuptext}% |
750 \end{isamarkuptext}% |
751 \isamarkuptrue% |
751 \isamarkuptrue% |
752 % |
752 % |
787 'lemma' ('(open)')? ((prop +) + 'and') \\ 'by' method method? |
787 'lemma' ('(open)')? ((prop +) + 'and') \\ 'by' method method? |
788 \end{rail} |
788 \end{rail} |
789 |
789 |
790 \begin{description} |
790 \begin{description} |
791 |
791 |
792 \item \isa{{\isacharat}{\isacharbraceleft}ctyp\ {\isasymtau}{\isacharbraceright}} produces a certified type wrt.\ the |
792 \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ctyp\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{7D}{\isacharbraceright}}} produces a certified type wrt.\ the |
793 current background theory --- as abstract value of type \verb|ctyp|. |
793 current background theory --- as abstract value of type \verb|ctyp|. |
794 |
794 |
795 \item \isa{{\isacharat}{\isacharbraceleft}cterm\ t{\isacharbraceright}} and \isa{{\isacharat}{\isacharbraceleft}cprop\ {\isasymphi}{\isacharbraceright}} produce a |
795 \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 |
796 certified term wrt.\ the current background theory --- as abstract |
796 certified term wrt.\ the current background theory --- as abstract |
797 value of type \verb|cterm|. |
797 value of type \verb|cterm|. |
798 |
798 |
799 \item \isa{{\isacharat}{\isacharbraceleft}thm\ a{\isacharbraceright}} produces a singleton fact --- as abstract |
799 \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thm\ a{\isaliteral{7D}{\isacharbraceright}}} produces a singleton fact --- as abstract |
800 value of type \verb|thm|. |
800 value of type \verb|thm|. |
801 |
801 |
802 \item \isa{{\isacharat}{\isacharbraceleft}thms\ a{\isacharbraceright}} produces a general fact --- as abstract |
802 \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thms\ a{\isaliteral{7D}{\isacharbraceright}}} produces a general fact --- as abstract |
803 value of type \verb|thm list|. |
803 value of type \verb|thm list|. |
804 |
804 |
805 \item \isa{{\isacharat}{\isacharbraceleft}lemma\ {\isasymphi}\ by\ meth{\isacharbraceright}} produces a fact that is proven on |
805 \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}lemma\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ by\ meth{\isaliteral{7D}{\isacharbraceright}}} produces a fact that is proven on |
806 the spot according to the minimal proof, which imitates a terminal |
806 the spot according to the minimal proof, which imitates a terminal |
807 Isar proof. The result is an abstract value of type \verb|thm| |
807 Isar proof. The result is an abstract value of type \verb|thm| |
808 or \verb|thm list|, depending on the number of propositions |
808 or \verb|thm list|, depending on the number of propositions |
809 given here. |
809 given here. |
810 |
810 |
811 The internal derivation object lacks a proper theorem name, but it |
811 The internal derivation object lacks a proper theorem name, but it |
812 is formally closed, unless the \isa{{\isacharparenleft}open{\isacharparenright}} option is specified |
812 is formally closed, unless the \isa{{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}} option is specified |
813 (this may impact performance of applications with proof terms). |
813 (this may impact performance of applications with proof terms). |
814 |
814 |
815 Since ML antiquotations are always evaluated at compile-time, there |
815 Since ML antiquotations are always evaluated at compile-time, there |
816 is no run-time overhead even for non-trivial proofs. Nonetheless, |
816 is no run-time overhead even for non-trivial proofs. Nonetheless, |
817 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 |
817 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 |
839 exposed to the user, but appear in internal encodings. |
839 exposed to the user, but appear in internal encodings. |
840 |
840 |
841 \begin{figure}[htb] |
841 \begin{figure}[htb] |
842 \begin{center} |
842 \begin{center} |
843 \begin{tabular}{ll} |
843 \begin{tabular}{ll} |
844 \isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}{\isacharampersand}{\isacharampersand}}) \\ |
844 \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}}}) \\ |
845 \isa{{\isasymturnstile}\ A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\[1ex] |
845 \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] |
846 \isa{prop\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop} & (prefix \isa{{\isacharhash}}, suppressed) \\ |
846 \isa{prop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & (prefix \isa{{\isaliteral{23}{\isacharhash}}}, suppressed) \\ |
847 \isa{{\isacharhash}A\ {\isasymequiv}\ A} \\[1ex] |
847 \isa{{\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A} \\[1ex] |
848 \isa{term\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & (prefix \isa{TERM}) \\ |
848 \isa{term\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & (prefix \isa{TERM}) \\ |
849 \isa{term\ x\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}A{\isachardot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}} \\[1ex] |
849 \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] |
850 \isa{TYPE\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself} & (prefix \isa{TYPE}) \\ |
850 \isa{TYPE\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ itself} & (prefix \isa{TYPE}) \\ |
851 \isa{{\isacharparenleft}unspecified{\isacharparenright}} \\ |
851 \isa{{\isaliteral{28}{\isacharparenleft}}unspecified{\isaliteral{29}{\isacharparenright}}} \\ |
852 \end{tabular} |
852 \end{tabular} |
853 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux} |
853 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux} |
854 \end{center} |
854 \end{center} |
855 \end{figure} |
855 \end{figure} |
856 |
856 |
857 The introduction \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B}, and eliminations |
857 The introduction \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B}, and eliminations |
858 (projections) \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymLongrightarrow}\ B} are |
858 (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 |
859 available as derived rules. Conjunction allows to treat |
859 available as derived rules. Conjunction allows to treat |
860 simultaneous assumptions and conclusions uniformly, e.g.\ consider |
860 simultaneous assumptions and conclusions uniformly, e.g.\ consider |
861 \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ D}. In particular, the goal mechanism |
861 \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 |
862 represents multiple claims as explicit conjunction internally, but |
862 represents multiple claims as explicit conjunction internally, but |
863 this is refined (via backwards introduction) into separate sub-goals |
863 this is refined (via backwards introduction) into separate sub-goals |
864 before the user commences the proof; the final result is projected |
864 before the user commences the proof; the final result is projected |
865 into a list of theorems using eliminations (cf.\ |
865 into a list of theorems using eliminations (cf.\ |
866 \secref{sec:tactical-goals}). |
866 \secref{sec:tactical-goals}). |
867 |
867 |
868 The \isa{prop} marker (\isa{{\isacharhash}}) makes arbitrarily complex |
868 The \isa{prop} marker (\isa{{\isaliteral{23}{\isacharhash}}}) makes arbitrarily complex |
869 propositions appear as atomic, without changing the meaning: \isa{{\isasymGamma}\ {\isasymturnstile}\ A} and \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isacharhash}A} are interchangeable. See |
869 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 |
870 \secref{sec:tactical-goals} for specific operations. |
870 \secref{sec:tactical-goals} for specific operations. |
871 |
871 |
872 The \isa{term} marker turns any well-typed term into a derivable |
872 The \isa{term} marker turns any well-typed term into a derivable |
873 proposition: \isa{{\isasymturnstile}\ TERM\ t} holds unconditionally. Although |
873 proposition: \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ TERM\ t} holds unconditionally. Although |
874 this is logically vacuous, it allows to treat terms and proofs |
874 this is logically vacuous, it allows to treat terms and proofs |
875 uniformly, similar to a type-theoretic framework. |
875 uniformly, similar to a type-theoretic framework. |
876 |
876 |
877 The \isa{TYPE} constructor is the canonical representative of |
877 The \isa{TYPE} constructor is the canonical representative of |
878 the unspecified type \isa{{\isasymalpha}\ itself}; it essentially injects the |
878 the unspecified type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ itself}; it essentially injects the |
879 language of types into that of terms. There is specific notation |
879 language of types into that of terms. There is specific notation |
880 \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} for \isa{TYPE\isactrlbsub {\isasymtau}\ itself\isactrlesub }. |
880 \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} for \isa{TYPE\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isaliteral{5C3C7461753E}{\isasymtau}}\ itself\isaliteral{5C3C5E657375623E}{}\isactrlesub }. |
881 Although being devoid of any particular meaning, the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} accounts for the type \isa{{\isasymtau}} within the term |
881 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 |
882 language. In particular, \isa{TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}} may be used as formal |
882 language. In particular, \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}} may be used as formal |
883 argument in primitive definitions, in order to circumvent hidden |
883 argument in primitive definitions, in order to circumvent hidden |
884 polymorphism (cf.\ \secref{sec:terms}). For example, \isa{c\ TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}\ {\isasymequiv}\ A{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} defines \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself\ {\isasymRightarrow}\ prop} in terms of |
884 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 |
885 a proposition \isa{A} that depends on an additional type |
885 a proposition \isa{A} that depends on an additional type |
886 argument, which is essentially a predicate on types.% |
886 argument, which is essentially a predicate on types.% |
887 \end{isamarkuptext}% |
887 \end{isamarkuptext}% |
888 \isamarkuptrue% |
888 \isamarkuptrue% |
889 % |
889 % |
953 The idea of object-level rules is to model Natural Deduction |
953 The idea of object-level rules is to model Natural Deduction |
954 inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow |
954 inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow |
955 arbitrary nesting similar to \cite{extensions91}. The most basic |
955 arbitrary nesting similar to \cite{extensions91}. The most basic |
956 rule format is that of a \emph{Horn Clause}: |
956 rule format is that of a \emph{Horn Clause}: |
957 \[ |
957 \[ |
958 \infer{\isa{A}}{\isa{A\isactrlsub {\isadigit{1}}} & \isa{{\isasymdots}} & \isa{A\isactrlsub n}} |
958 \infer{\isa{A}}{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} & \isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}} & \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub n}} |
959 \] |
959 \] |
960 where \isa{A{\isacharcomma}\ A\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlsub n} are atomic propositions |
960 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 |
961 of the framework, usually of the form \isa{Trueprop\ B}, where |
961 of the framework, usually of the form \isa{Trueprop\ B}, where |
962 \isa{B} is a (compound) object-level statement. This |
962 \isa{B} is a (compound) object-level statement. This |
963 object-level inference corresponds to an iterated implication in |
963 object-level inference corresponds to an iterated implication in |
964 Pure like this: |
964 Pure like this: |
965 \[ |
965 \[ |
966 \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ A} |
966 \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A} |
967 \] |
967 \] |
968 As an example consider conjunction introduction: \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B}. Any parameters occurring in such rule statements are |
968 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 |
969 conceptionally treated as arbitrary: |
969 conceptionally treated as arbitrary: |
970 \[ |
970 \[ |
971 \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ A\isactrlsub {\isadigit{1}}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymLongrightarrow}\ A\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m} |
971 \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} |
972 \] |
972 \] |
973 |
973 |
974 Nesting of rules means that the positions of \isa{A\isactrlsub i} may |
974 Nesting of rules means that the positions of \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub i} may |
975 again hold compound rules, not just atomic propositions. |
975 again hold compound rules, not just atomic propositions. |
976 Propositions of this format are called \emph{Hereditary Harrop |
976 Propositions of this format are called \emph{Hereditary Harrop |
977 Formulae} in the literature \cite{Miller:1991}. Here we give an |
977 Formulae} in the literature \cite{Miller:1991}. Here we give an |
978 inductive characterization as follows: |
978 inductive characterization as follows: |
979 |
979 |
980 \medskip |
980 \medskip |
981 \begin{tabular}{ll} |
981 \begin{tabular}{ll} |
982 \isa{\isactrlbold x} & set of variables \\ |
982 \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold x} & set of variables \\ |
983 \isa{\isactrlbold A} & set of atomic propositions \\ |
983 \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold A} & set of atomic propositions \\ |
984 \isa{\isactrlbold H\ \ {\isacharequal}\ \ {\isasymAnd}\isactrlbold x\isactrlsup {\isacharasterisk}{\isachardot}\ \isactrlbold H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ \isactrlbold A} & set of Hereditary Harrop Formulas \\ |
984 \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 \\ |
985 \end{tabular} |
985 \end{tabular} |
986 \medskip |
986 \medskip |
987 |
987 |
988 Thus we essentially impose nesting levels on propositions formed |
988 Thus we essentially impose nesting levels on propositions formed |
989 from \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}. At each level there is a prefix |
989 from \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}. At each level there is a prefix |
990 of parameters and compound premises, concluding an atomic |
990 of parameters and compound premises, concluding an atomic |
991 proposition. Typical examples are \isa{{\isasymlongrightarrow}}-introduction \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymlongrightarrow}\ B} or mathematical induction \isa{P\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ P\ n\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n}. Even deeper nesting occurs in well-founded |
991 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 |
992 induction \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharparenleft}{\isasymAnd}y{\isachardot}\ y\ {\isasymprec}\ x\ {\isasymLongrightarrow}\ P\ y{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x}, but this |
992 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 |
993 already marks the limit of rule complexity that is usually seen in |
993 already marks the limit of rule complexity that is usually seen in |
994 practice. |
994 practice. |
995 |
995 |
996 \medskip Regular user-level inferences in Isabelle/Pure always |
996 \medskip Regular user-level inferences in Isabelle/Pure always |
997 maintain the following canonical form of results: |
997 maintain the following canonical form of results: |
998 |
998 |
999 \begin{itemize} |
999 \begin{itemize} |
1000 |
1000 |
1001 \item Normalization by \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}, |
1001 \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}}}, |
1002 which is a theorem of Pure, means that quantifiers are pushed in |
1002 which is a theorem of Pure, means that quantifiers are pushed in |
1003 front of implication at each level of nesting. The normal form is a |
1003 front of implication at each level of nesting. The normal form is a |
1004 Hereditary Harrop Formula. |
1004 Hereditary Harrop Formula. |
1005 |
1005 |
1006 \item The outermost prefix of parameters is represented via |
1006 \item The outermost prefix of parameters is represented via |
1007 schematic variables: instead of \isa{{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ A\ \isactrlvec x} we have \isa{\isactrlvec H\ {\isacharquery}\isactrlvec x\ {\isasymLongrightarrow}\ A\ {\isacharquery}\isactrlvec x}. |
1007 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}. |
1008 Note that this representation looses information about the order of |
1008 Note that this representation looses information about the order of |
1009 parameters, and vacuous quantifiers vanish automatically. |
1009 parameters, and vacuous quantifiers vanish automatically. |
1010 |
1010 |
1011 \end{itemize}% |
1011 \end{itemize}% |
1012 \end{isamarkuptext}% |
1012 \end{isamarkuptext}% |
1048 \begin{isamarkuptext}% |
1048 \begin{isamarkuptext}% |
1049 The rule calculus of Isabelle/Pure provides two main inferences: |
1049 The rule calculus of Isabelle/Pure provides two main inferences: |
1050 \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} (i.e.\ back-chaining of rules) and |
1050 \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} (i.e.\ back-chaining of rules) and |
1051 \hyperlink{inference.assumption}{\mbox{\isa{assumption}}} (i.e.\ closing a branch), both modulo |
1051 \hyperlink{inference.assumption}{\mbox{\isa{assumption}}} (i.e.\ closing a branch), both modulo |
1052 higher-order unification. There are also combined variants, notably |
1052 higher-order unification. There are also combined variants, notably |
1053 \hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isacharunderscore}resolution}}} and \hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isacharunderscore}resolution}}}. |
1053 \hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}resolution}}} and \hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isaliteral{5F}{\isacharunderscore}}resolution}}}. |
1054 |
1054 |
1055 To understand the all-important \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle, |
1055 To understand the all-important \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle, |
1056 we first consider raw \indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}} (modulo |
1056 we first consider raw \indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}} (modulo |
1057 higher-order unification with substitution \isa{{\isasymvartheta}}): |
1057 higher-order unification with substitution \isa{{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}): |
1058 \[ |
1058 \[ |
1059 \infer[(\indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}})]{\isa{\isactrlvec A{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}} |
1059 \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}}}} |
1060 {\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B} & \isa{B{\isacharprime}\ {\isasymLongrightarrow}\ C} & \isa{B{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}}} |
1060 {\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}}}} |
1061 \] |
1061 \] |
1062 Here the conclusion of the first rule is unified with the premise of |
1062 Here the conclusion of the first rule is unified with the premise of |
1063 the second; the resulting rule instance inherits the premises of the |
1063 the second; the resulting rule instance inherits the premises of the |
1064 first and conclusion of the second. Note that \isa{C} can again |
1064 first and conclusion of the second. Note that \isa{C} can again |
1065 consist of iterated implications. We can also permute the premises |
1065 consist of iterated implications. We can also permute the premises |
1066 of the second rule back-and-forth in order to compose with \isa{B{\isacharprime}} in any position (subsequently we shall always refer to |
1066 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 |
1067 position 1 w.l.o.g.). |
1067 position 1 w.l.o.g.). |
1068 |
1068 |
1069 In \hyperlink{inference.composition}{\mbox{\isa{composition}}} the internal structure of the common |
1069 In \hyperlink{inference.composition}{\mbox{\isa{composition}}} the internal structure of the common |
1070 part \isa{B} and \isa{B{\isacharprime}} is not taken into account. For |
1070 part \isa{B} and \isa{B{\isaliteral{27}{\isacharprime}}} is not taken into account. For |
1071 proper \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} we require \isa{B} to be atomic, |
1071 proper \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} we require \isa{B} to be atomic, |
1072 and explicitly observe the structure \isa{{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x} of the premise of the second rule. The |
1072 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 |
1073 idea is to adapt the first rule by ``lifting'' it into this context, |
1073 idea is to adapt the first rule by ``lifting'' it into this context, |
1074 by means of iterated application of the following inferences: |
1074 by means of iterated application of the following inferences: |
1075 \[ |
1075 \[ |
1076 \infer[(\indexdef{}{inference}{imp\_lift}\hypertarget{inference.imp-lift}{\hyperlink{inference.imp-lift}{\mbox{\isa{imp{\isacharunderscore}lift}}}})]{\isa{{\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ \isactrlvec A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ B{\isacharparenright}}}{\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B}} |
1076 \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}} |
1077 \] |
1077 \] |
1078 \[ |
1078 \[ |
1079 \infer[(\indexdef{}{inference}{all\_lift}\hypertarget{inference.all-lift}{\hyperlink{inference.all-lift}{\mbox{\isa{all{\isacharunderscore}lift}}}})]{\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec A\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}}}{\isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a}} |
1079 \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}} |
1080 \] |
1080 \] |
1081 By combining raw composition with lifting, we get full \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} as follows: |
1081 By combining raw composition with lifting, we get full \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} as follows: |
1082 \[ |
1082 \[ |
1083 \infer[(\indexdef{}{inference}{resolution}\hypertarget{inference.resolution}{\hyperlink{inference.resolution}{\mbox{\isa{resolution}}}})] |
1083 \infer[(\indexdef{}{inference}{resolution}\hypertarget{inference.resolution}{\hyperlink{inference.resolution}{\mbox{\isa{resolution}}}})] |
1084 {\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ \isactrlvec A\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}} |
1084 {\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}}}} |
1085 {\begin{tabular}{l} |
1085 {\begin{tabular}{l} |
1086 \isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a} \\ |
1086 \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a} \\ |
1087 \isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} \\ |
1087 \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} \\ |
1088 \isa{{\isacharparenleft}{\isasymlambda}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}} \\ |
1088 \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}}} \\ |
1089 \end{tabular}} |
1089 \end{tabular}} |
1090 \] |
1090 \] |
1091 |
1091 |
1092 Continued resolution of rules allows to back-chain a problem towards |
1092 Continued resolution of rules allows to back-chain a problem towards |
1093 more and sub-problems. Branches are closed either by resolving with |
1093 more and sub-problems. Branches are closed either by resolving with |
1094 a rule of 0 premises, or by producing a ``short-circuit'' within a |
1094 a rule of 0 premises, or by producing a ``short-circuit'' within a |
1095 solved situation (again modulo unification): |
1095 solved situation (again modulo unification): |
1096 \[ |
1096 \[ |
1097 \infer[(\indexdef{}{inference}{assumption}\hypertarget{inference.assumption}{\hyperlink{inference.assumption}{\mbox{\isa{assumption}}}})]{\isa{C{\isasymvartheta}}} |
1097 \infer[(\indexdef{}{inference}{assumption}\hypertarget{inference.assumption}{\hyperlink{inference.assumption}{\mbox{\isa{assumption}}}})]{\isa{C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}} |
1098 {\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ A\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} & \isa{A{\isasymvartheta}\ {\isacharequal}\ H\isactrlsub i{\isasymvartheta}}~~\text{(for some~\isa{i})}} |
1098 {\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})}} |
1099 \] |
1099 \] |
1100 |
1100 |
1101 FIXME \indexdef{}{inference}{elim\_resolution}\hypertarget{inference.elim-resolution}{\hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isacharunderscore}resolution}}}}, \indexdef{}{inference}{dest\_resolution}\hypertarget{inference.dest-resolution}{\hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isacharunderscore}resolution}}}}% |
1101 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}}}}% |
1102 \end{isamarkuptext}% |
1102 \end{isamarkuptext}% |
1103 \isamarkuptrue% |
1103 \isamarkuptrue% |
1104 % |
1104 % |
1105 \isadelimmlref |
1105 \isadelimmlref |
1106 % |
1106 % |