# HG changeset patch # User wenzelm # Date 1158074614 -7200 # Node ID d7ad1217c24a8c58aacc1de16e76fac9b1291769 # Parent 9125f0d9544946950644e333b9c315eea2a82fd6 more on terms; diff -r 9125f0d95449 -r d7ad1217c24a doc-src/IsarImplementation/Thy/document/logic.tex --- a/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 12 17:12:51 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 12 17:23:34 2006 +0200 @@ -103,7 +103,7 @@ \medskip The sort algebra is always maintained as \emph{coregular}, which means that type arities are consistent with the subclass - relation: for each type constructor \isa{{\isasymkappa}} and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds componentwise. + relation: for each type constructor \isa{{\isasymkappa}} and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds component-wise. The key property of a coregular order-sorted algebra is that sort constraints may be always solved in a most general fashion: for each @@ -128,6 +128,7 @@ \indexmltype{sort}\verb|type sort| \\ \indexmltype{arity}\verb|type arity| \\ \indexmltype{typ}\verb|type typ| \\ + \indexml{map-atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\ \indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\ \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\ \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\ @@ -153,8 +154,11 @@ \item \verb|typ| represents types; this is a datatype with constructors \verb|TFree|, \verb|TVar|, \verb|Type|. - \item \verb|fold_atyps|~\isa{f\ {\isasymtau}} iterates function \isa{f} - over all occurrences of atoms (\verb|TFree| or \verb|TVar|) of \isa{{\isasymtau}}; the type structure is traversed from left to right. + \item \verb|map_atyps|~\isa{f\ {\isasymtau}} applies mapping \isa{f} to + all atomic types (\verb|TFree|, \verb|TVar|) occurring in \isa{{\isasymtau}}. + + \item \verb|fold_atyps|~\isa{f\ {\isasymtau}} iterates operation \isa{f} + over all occurrences of atoms (\verb|TFree|, \verb|TVar|) in \isa{{\isasymtau}}; the type structure is traversed from left to right. \item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}} tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}. @@ -197,18 +201,18 @@ \glossary{Term}{FIXME} The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus - with de-Bruijn indices for bound variables, and named free variables - and constants. Terms with loose bound variables are usually - considered malformed. The types of variables and constants is - stored explicitly at each occurrence in the term. + with de-Bruijn indices for bound variables + \cite{debruijn72,paulson-ml2}, and named free variables and + constants. Terms with loose bound variables are usually considered + malformed. The types of variables and constants is stored + explicitly at each occurrence in the term. \medskip A \emph{bound variable} is a natural number \isa{b}, which refers to the next binder that is \isa{b} steps upwards from the occurrence of \isa{b} (counting from zero). Bindings may be introduced as abstractions within the term, or as a separate context (an inside-out list). This associates each bound variable - with a type, and a name that is maintained as a comment for parsing - and printing. A \emph{loose variables} is a bound variable that is + with a type. A \emph{loose variables} is a bound variable that is outside the current scope of local binders or the context. For example, the de-Bruijn term \isa{{\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{0}}} corresponds to \isa{{\isasymlambda}x\isactrlisub {\isasymtau}{\isachardot}\ {\isasymlambda}y\isactrlisub {\isasymtau}{\isachardot}\ x\ {\isacharplus}\ y} in a named @@ -281,7 +285,20 @@ looks like a constant at the surface, but is fully expanded before entering the logical core. Abbreviations are usually reverted when printing terms, using rules \isa{t\ {\isasymrightarrow}\ c\isactrlisub {\isasymsigma}} has a - higher-order term rewrite system.% + higher-order term rewrite system. + + \medskip Canonical operations on \isa{{\isasymlambda}}-terms include \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion. \isa{{\isasymalpha}}-conversion refers to capture-free + renaming of bound variables; \isa{{\isasymbeta}}-conversion contracts an + abstraction applied to some argument term, substituting the argument + 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 + \isa{{\isadigit{0}}} does not occur in \isa{f}. + + Terms are almost always treated module \isa{{\isasymalpha}}-conversion, which + is implicit in the de-Bruijn representation. The names in + abstractions of bound variables are maintained only as a comment for + parsing and printing. Full \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-equivalence is usually + taken for granted higher rules (\secref{sec:rules}), anything + depending on higher-order unification or rewriting.% \end{isamarkuptext}% \isamarkuptrue% % @@ -294,15 +311,68 @@ \begin{isamarkuptext}% \begin{mldecls} \indexmltype{term}\verb|type term| \\ + \indexml{op aconv}\verb|op aconv: term * term -> bool| \\ + \indexml{map-term-types}\verb|map_term_types: (typ -> typ) -> term -> term| \\ %FIXME rename map_types + \indexml{fold-types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\ \indexml{map-aterms}\verb|map_aterms: (term -> term) -> term -> term| \\ \indexml{fold-aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\ \indexml{fastype-of}\verb|fastype_of: term -> typ| \\ - \indexml{fold-types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\ + \indexml{lambda}\verb|lambda: term -> term -> term| \\ + \indexml{betapply}\verb|betapply: term * term -> term| \\ + \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (bstring * typ * mixfix) list -> theory -> theory| \\ + \indexml{Sign.add-abbrevs}\verb|Sign.add_abbrevs: string * bool ->|\isasep\isanewline% +\verb| ((bstring * mixfix) * term) list -> theory -> theory| \\ + \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\ + \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\ \end{mldecls} \begin{description} - \item \verb|term| FIXME + \item \verb|term| represents de-Bruijn terms with comments in + abstractions for bound variable names. This is a datatype with + constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|op $|. + + \item \isa{t}~\verb|aconv|~\isa{u} checks \isa{{\isasymalpha}}-equivalence of two terms. This is the basic equality relation + on type \verb|term|; raw datatype equality should only be used + for operations related to parsing or printing! + + \item \verb|map_term_types|~\isa{f\ t} applies mapping \isa{f} + to all types occurring in \isa{t}. + + \item \verb|fold_types|~\isa{f\ t} iterates operation \isa{f} + over all occurrences of types in \isa{t}; the term structure is + traversed from left to right. + + \item \verb|map_aterms|~\isa{f\ t} applies mapping \isa{f} to + all atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) + occurring in \isa{t}. + + \item \verb|fold_aterms|~\isa{f\ t} iterates operation \isa{f} + over all occurrences of atomic terms in (\verb|Bound|, \verb|Free|, + \verb|Var|, \verb|Const|) \isa{t}; the term structure is traversed + from left to right. + + \item \verb|fastype_of|~\isa{t} recomputes the type of a + well-formed term, while omitting any sanity checks. This operation + is relatively slow. + + \item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the original (atomic) term \isa{a} are replaced by bound variables. + + \item \verb|betapply|~\isa{t\ u} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion \isa{t} is an + abstraction. + + \item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a + new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax. + + \item \verb|Sign.add_abbrevs|~\isa{print{\isacharunderscore}mode\ {\isacharbrackleft}{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} + declares a new term abbreviation \isa{c\ {\isasymequiv}\ t} with optional + mixfix syntax. + + \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} produces the + type arguments of the instance \isa{c\isactrlisub {\isasymtau}} wrt.\ its + declaration in the theory. + + \item \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}} produces the full instance \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} wrt.\ its declaration in the theory. \end{description}% \end{isamarkuptext}% @@ -333,7 +403,7 @@ rarely spelled out explicitly. Theorems are usually normalized according to the \seeglossary{HHF} format. FIXME} - \glossary{Fact}{Sometimes used interchangably for + \glossary{Fact}{Sometimes used interchangeably for \seeglossary{theorem}. Strictly speaking, a list of theorems, essentially an extra-logical conjunction. Facts emerge either as local assumptions, or as results of local goal statements --- both @@ -501,7 +571,7 @@ important to maintain this invariant in add-on applications! There are two main principles of rule composition: \isa{resolution} (i.e.\ backchaining of rules) and \isa{by{\isacharminus}assumption} (i.e.\ closing a branch); both principles are - combined in the variants of \isa{elim{\isacharminus}resosultion} and \isa{dest{\isacharminus}resolution}. Raw \isa{composition} is occasionally + combined in the variants of \isa{elim{\isacharminus}resolution} and \isa{dest{\isacharminus}resolution}. Raw \isa{composition} is occasionally useful as well, also it is strictly speaking outside of the proper rule calculus. diff -r 9125f0d95449 -r d7ad1217c24a doc-src/IsarImplementation/Thy/logic.thy --- a/doc-src/IsarImplementation/Thy/logic.thy Tue Sep 12 17:12:51 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/logic.thy Tue Sep 12 17:23:34 2006 +0200 @@ -102,7 +102,7 @@ "c\<^isub>1 \ c\<^isub>2"}, any arity @{text "\ :: (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\ :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \ - \<^vec>s\<^isub>2"} holds componentwise. + \<^vec>s\<^isub>2"} holds component-wise. The key property of a coregular order-sorted algebra is that sort constraints may be always solved in a most general fashion: for each @@ -122,6 +122,7 @@ @{index_ML_type sort} \\ @{index_ML_type arity} \\ @{index_ML_type typ} \\ + @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\ @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\ @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\ @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\ @@ -148,8 +149,11 @@ \item @{ML_type typ} represents types; this is a datatype with constructors @{ML TFree}, @{ML TVar}, @{ML Type}. - \item @{ML fold_atyps}~@{text "f \"} iterates function @{text "f"} - over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text + \item @{ML map_atyps}~@{text "f \"} applies mapping @{text "f"} to + all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text "\"}. + + \item @{ML fold_atyps}~@{text "f \"} iterates operation @{text "f"} + over all occurrences of atoms (@{ML TFree}, @{ML TVar}) in @{text "\"}; the type structure is traversed from left to right. \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"} @@ -188,18 +192,18 @@ \glossary{Term}{FIXME} The language of terms is that of simply-typed @{text "\"}-calculus - with de-Bruijn indices for bound variables, and named free variables - and constants. Terms with loose bound variables are usually - considered malformed. The types of variables and constants is - stored explicitly at each occurrence in the term. + with de-Bruijn indices for bound variables + \cite{debruijn72,paulson-ml2}, and named free variables and + constants. Terms with loose bound variables are usually considered + malformed. The types of variables and constants is stored + explicitly at each occurrence in the term. \medskip A \emph{bound variable} is a natural number @{text "b"}, which refers to the next binder that is @{text "b"} steps upwards from the occurrence of @{text "b"} (counting from zero). Bindings may be introduced as abstractions within the term, or as a separate context (an inside-out list). This associates each bound variable - with a type, and a name that is maintained as a comment for parsing - and printing. A \emph{loose variables} is a bound variable that is + with a type. A \emph{loose variables} is a bound variable that is outside the current scope of local binders or the context. For example, the de-Bruijn term @{text "\\<^isub>\. \\<^isub>\. 1 + 0"} corresponds to @{text "\x\<^isub>\. \y\<^isub>\. x + y"} in a named @@ -284,20 +288,96 @@ entering the logical core. Abbreviations are usually reverted when printing terms, using rules @{text "t \ c\<^isub>\"} has a higher-order term rewrite system. + + \medskip Canonical operations on @{text "\"}-terms include @{text + "\\\"}-conversion. @{text "\"}-conversion refers to capture-free + renaming of bound variables; @{text "\"}-conversion contracts an + abstraction applied to some argument term, substituting the argument + in the body: @{text "(\x. b)a"} becomes @{text "b[a/x]"}; @{text + "\"}-conversion contracts vacuous application-abstraction: @{text + "\x. f x"} becomes @{text "f"}, provided that the bound variable + @{text "0"} does not occur in @{text "f"}. + + Terms are almost always treated module @{text "\"}-conversion, which + is implicit in the de-Bruijn representation. The names in + abstractions of bound variables are maintained only as a comment for + parsing and printing. Full @{text "\\\"}-equivalence is usually + taken for granted higher rules (\secref{sec:rules}), anything + depending on higher-order unification or rewriting. *} text %mlref {* \begin{mldecls} @{index_ML_type term} \\ + @{index_ML "op aconv": "term * term -> bool"} \\ + @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\ %FIXME rename map_types + @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\ @{index_ML map_aterms: "(term -> term) -> term -> term"} \\ @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\ @{index_ML fastype_of: "term -> typ"} \\ - @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\ + @{index_ML lambda: "term -> term -> term"} \\ + @{index_ML betapply: "term * term -> term"} \\ + @{index_ML Sign.add_consts_i: "(bstring * typ * mixfix) list -> theory -> theory"} \\ + @{index_ML Sign.add_abbrevs: "string * bool -> + ((bstring * mixfix) * term) list -> theory -> theory"} \\ + @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\ + @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ \end{mldecls} \begin{description} - \item @{ML_type term} FIXME + \item @{ML_type term} represents de-Bruijn terms with comments in + abstractions for bound variable names. This is a datatype with + constructors @{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}, @{ML + Abs}, @{ML "op $"}. + + \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text + "\"}-equivalence of two terms. This is the basic equality relation + on type @{ML_type term}; raw datatype equality should only be used + for operations related to parsing or printing! + + \item @{ML map_term_types}~@{text "f t"} applies mapping @{text "f"} + to all types occurring in @{text "t"}. + + \item @{ML fold_types}~@{text "f t"} iterates operation @{text "f"} + over all occurrences of types in @{text "t"}; the term structure is + traversed from left to right. + + \item @{ML map_aterms}~@{text "f t"} applies mapping @{text "f"} to + all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}) + occurring in @{text "t"}. + + \item @{ML fold_aterms}~@{text "f t"} iterates operation @{text "f"} + over all occurrences of atomic terms in (@{ML Bound}, @{ML Free}, + @{ML Var}, @{ML Const}) @{text "t"}; the term structure is traversed + from left to right. + + \item @{ML fastype_of}~@{text "t"} recomputes the type of a + well-formed term, while omitting any sanity checks. This operation + is relatively slow. + + \item @{ML lambda}~@{text "a b"} produces an abstraction @{text + "\a. b"}, where occurrences of the original (atomic) term @{text + "a"} are replaced by bound variables. + + \item @{ML betapply}~@{text "t u"} produces an application @{text "t + u"}, with topmost @{text "\"}-conversion @{text "t"} is an + abstraction. + + \item @{ML Sign.add_consts_i}~@{text "[(c, \, mx), \]"} declares a + new constant @{text "c :: \"} with optional mixfix syntax. + + \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \]"} + declares a new term abbreviation @{text "c \ t"} with optional + mixfix syntax. + + \item @{ML Sign.const_typargs}~@{text "thy (c, \)"} produces the + type arguments of the instance @{text "c\<^isub>\"} wrt.\ its + declaration in the theory. + + \item @{ML Sign.const_instance}~@{text "thy (c, [\\<^isub>1, \, + \\<^isub>n])"} produces the full instance @{text "c(\\<^isub>1, \, + \\<^isub>n)"} wrt.\ its declaration in the theory. \end{description} *} @@ -319,7 +399,7 @@ rarely spelled out explicitly. Theorems are usually normalized according to the \seeglossary{HHF} format. FIXME} - \glossary{Fact}{Sometimes used interchangably for + \glossary{Fact}{Sometimes used interchangeably for \seeglossary{theorem}. Strictly speaking, a list of theorems, essentially an extra-logical conjunction. Facts emerge either as local assumptions, or as results of local goal statements --- both @@ -495,7 +575,7 @@ There are two main principles of rule composition: @{text "resolution"} (i.e.\ backchaining of rules) and @{text "by-assumption"} (i.e.\ closing a branch); both principles are - combined in the variants of @{text "elim-resosultion"} and @{text + combined in the variants of @{text "elim-resolution"} and @{text "dest-resolution"}. Raw @{text "composition"} is occasionally useful as well, also it is strictly speaking outside of the proper rule calculus.