HOLCF: discontinued special version of 'constdefs';
authorwenzelm
Thu Apr 29 06:01:20 2004 +0200 (2004-04-29)
changeset 14682a5072752114c
parent 14681 16fcef3a3174
child 14683 2757b50f8f48
HOLCF: discontinued special version of 'constdefs';
NEWS
doc-src/IsarRef/logics.tex
src/HOLCF/cont_consts.ML
     1.1 --- a/NEWS	Wed Apr 28 10:45:35 2004 +0200
     1.2 +++ b/NEWS	Thu Apr 29 06:01:20 2004 +0200
     1.3 @@ -12,13 +12,21 @@
     1.4  records), see also isar-ref manual.  Potential INCOMPATIBILITY: need
     1.5  to observe strictly sequential dependencies of definitions within a
     1.6  single 'constdefs' section -- some existing specifications may have to
     1.7 -be reordered.
     1.8 +be reordered; moreover, the declared name needs to be an identifier.
     1.9 +In the worst case may have to fall back on plain 'consts' + 'defs'.
    1.10  
    1.11  * Pure: 'advanced' translation functions (parse_translation etc.) may
    1.12  depend on the signature of the theory context being presently used for
    1.13  parsing/printing, see also isar-ref manual.
    1.14  
    1.15  
    1.16 +*** HOLCF ***
    1.17 +
    1.18 +* HOLCF: discontinued special version of 'constdefs' (which used to
    1.19 +support continuous functions) in favor of the general Pure one with
    1.20 +full type-inference.
    1.21 +
    1.22 +
    1.23  
    1.24  New in Isabelle2004 (April 2004)
    1.25  --------------------------------
     2.1 --- a/doc-src/IsarRef/logics.tex	Wed Apr 28 10:45:35 2004 +0200
     2.2 +++ b/doc-src/IsarRef/logics.tex	Thu Apr 29 06:01:20 2004 +0200
     2.3 @@ -735,29 +735,22 @@
     2.4  
     2.5  \subsection{Mixfix syntax for continuous operations}
     2.6  
     2.7 -\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
     2.8 +\indexisarcmdof{HOLCF}{consts}
     2.9  
    2.10  \begin{matharray}{rcl}
    2.11    \isarcmd{consts} & : & \isartrans{theory}{theory} \\
    2.12 -  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
    2.13  \end{matharray}
    2.14  
    2.15 -\begin{rail}
    2.16 -  'constdefs' (name '::' type mixfix? prop +)
    2.17 -  ;
    2.18 -\end{rail}
    2.19 -
    2.20  HOLCF provides a separate type for continuous functions $\alpha \to
    2.21  \beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix
    2.22  syntax normally refers directly to the pure meta-level function type $\alpha
    2.23  \To \beta$, with application $f\,x$.
    2.24  
    2.25 -The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ resemble those of Pure
    2.26 -Isabelle (cf.\ \S\ref{sec:consts}), although automated type-inference is not
    2.27 -supported here.  Internally, declarations involving continuous function types
    2.28 -are treated specifically, transforming the syntax template accordingly and
    2.29 -generating syntax translation rules for the abstract and concrete
    2.30 -representation of application.  Note that mixing continuous and meta-level
    2.31 +The HOLCF variant of $\CONSTS$ modifies that of Pure Isabelle (cf.\ 
    2.32 +\S\ref{sec:consts}) such that declarations involving continuous function types
    2.33 +are treated specifically.  Any given syntax template is transformed
    2.34 +internally, generating translation rules for the abstract and concrete
    2.35 +representation of continuous application.  Note that mixing of HOLCF and Pure
    2.36  application is \emph{not} supported!
    2.37  
    2.38  \subsection{Recursive domains}
     3.1 --- a/src/HOLCF/cont_consts.ML	Wed Apr 28 10:45:35 2004 +0200
     3.2 +++ b/src/HOLCF/cont_consts.ML	Thu Apr 29 06:01:20 2004 +0200
     3.3 @@ -3,16 +3,14 @@
     3.4      Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
     3.5      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.6  
     3.7 -HOLCF version of consts/constdefs: handle continuous function types in
     3.8 -mixfix syntax.
     3.9 +HOLCF version of consts: handle continuous function types in mixfix
    3.10 +syntax.
    3.11  *)
    3.12  
    3.13  signature CONT_CONSTS =
    3.14  sig
    3.15    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    3.16    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    3.17 -  val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
    3.18 -  val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
    3.19  end;
    3.20  
    3.21  structure ContConsts: CONT_CONSTS =
    3.22 @@ -104,18 +102,6 @@
    3.23  val add_consts_i = gen_add_consts Thm.ctyp_of;
    3.24  
    3.25  
    3.26 -(* add_constdefs(_i) *)
    3.27 -
    3.28 -fun gen_add_constdefs consts defs args thy =
    3.29 -  thy
    3.30 -  |> consts (map fst args)
    3.31 -  |> defs (false, map (fn ((c, _, mx), s) =>
    3.32 -    ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
    3.33 -
    3.34 -fun add_constdefs args = gen_add_constdefs add_consts IsarThy.add_defs args;
    3.35 -fun add_constdefs_i args = gen_add_constdefs add_consts_i IsarThy.add_defs_i args;
    3.36 -
    3.37 -
    3.38  (* outer syntax *)
    3.39  
    3.40  local structure P = OuterParse and K = OuterSyntax.Keyword in
    3.41 @@ -124,12 +110,7 @@
    3.42    OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
    3.43      (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
    3.44  
    3.45 -val constdefsP =
    3.46 -  OuterSyntax.command "constdefs" "declare and define constants (HOLCF)" K.thy_decl
    3.47 -    (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o add_constdefs));
    3.48 -
    3.49 -
    3.50 -val _ = OuterSyntax.add_parsers [constsP, constdefsP];
    3.51 +val _ = OuterSyntax.add_parsers [constsP];
    3.52  
    3.53  end;
    3.54