--- a/NEWS Fri Mar 12 20:04:48 2010 +0100
+++ b/NEWS Sat Mar 13 15:11:59 2010 +0100
@@ -83,6 +83,12 @@
*** HOL ***
+* Command 'typedef' now works within a local theory context -- without
+introducing dependencies on parameters or assumptions, which is not
+possible in Isabelle/Pure/HOL. Note that the logical environment may
+contain multiple interpretations of local typedefs (with different
+non-emptiness proofs), even in a global theory context.
+
* Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
Min, Max from theory Finite_Set. INCOMPATIBILITY.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Mar 12 20:04:48 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 13 15:11:59 2010 +0100
@@ -4,17 +4,14 @@
chapter {* Isabelle/HOL \label{ch:hol} *}
-section {* Primitive types \label{sec:hol-typedef} *}
+section {* Typedef axiomatization \label{sec:hol-typedef} *}
text {*
\begin{matharray}{rcl}
- @{command_def (HOL) "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "typedef"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+ @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
\end{matharray}
\begin{rail}
- 'typedecl' typespec mixfix?
- ;
'typedef' altname? abstype '=' repset
;
@@ -28,23 +25,25 @@
\begin{description}
- \item @{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} is similar
- to the original @{command "typedecl"} of Isabelle/Pure (see
- \secref{sec:types-pure}), but also declares type arity @{text "t ::
- (type, \<dots>, type) type"}, making @{text t} an actual HOL type
- constructor. %FIXME check, update
+ \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
+ axiomatizes a Gordon/HOL-style type definition in the background
+ theory of the current context, depending on a non-emptiness result
+ of the set @{text A} (which needs to be proven interactively).
+
+ The raw type may not depend on parameters or assumptions of the
+ context --- this is logically impossible in Isabelle/HOL --- but the
+ non-emptiness property can be local, potentially resulting in
+ multiple interpretations in target contexts. Thus the established
+ bijection between the representing set @{text A} and the new type
+ @{text t} may semantically depend on local assumptions.
- \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} sets up
- a goal stating non-emptiness of the set @{text A}. After finishing
- the proof, the theory will be augmented by a Gordon/HOL-style type
- definition, which establishes a bijection between the representing
- set @{text A} and the new type @{text t}.
-
- Technically, @{command (HOL) "typedef"} defines both a type @{text
- t} and a set (term constant) of the same name (an alternative base
- name may be given in parentheses). The injection from type to set
- is called @{text Rep_t}, its inverse @{text Abs_t} (this may be
- changed via an explicit @{keyword (HOL) "morphisms"} declaration).
+ By default, @{command (HOL) "typedef"} defines both a type @{text t}
+ and a set (term constant) of the same name, unless an alternative
+ base name is given in parentheses, or the ``@{text "(open)"}''
+ declaration is used to suppress a separate constant definition
+ altogether. The injection from type to set is called @{text Rep_t},
+ its inverse @{text Abs_t} --- this may be changed via an explicit
+ @{keyword (HOL) "morphisms"} declaration.
Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
Abs_t_inverse} provide the most basic characterization as a
@@ -57,19 +56,11 @@
on surjectivity; these are already declared as set or type rules for
the generic @{method cases} and @{method induct} methods.
- An alternative name may be specified in parentheses; the default is
- to use @{text t} as indicated before. The ``@{text "(open)"}''
- declaration suppresses a separate constant definition for the
- representing set.
+ An alternative name for the set definition (and other derived
+ entities) may be specified in parentheses; the default is to use
+ @{text t} as indicated before.
\end{description}
-
- Note that raw type declarations are rarely used in practice; the
- main application is with experimental (or even axiomatic!) theory
- fragments. Instead of primitive HOL type definitions, user-level
- theories usually refer to higher-level packages such as @{command
- (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL)
- "datatype"} (see \secref{sec:hol-datatype}).
*}
@@ -906,7 +897,7 @@
*}
-section {* Invoking automated reasoning tools -- The Sledgehammer *}
+section {* Invoking automated reasoning tools --- The Sledgehammer *}
text {*
Isabelle/HOL includes a generic \emph{ATP manager} that allows
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Mar 12 20:04:48 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 13 15:11:59 2010 +0100
@@ -22,19 +22,16 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Primitive types \label{sec:hol-typedef}%
+\isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\end{matharray}
\begin{rail}
- 'typedecl' typespec mixfix?
- ;
'typedef' altname? abstype '=' repset
;
@@ -48,21 +45,25 @@
\begin{description}
- \item \hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} is similar
- to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of Isabelle/Pure (see
- \secref{sec:types-pure}), but also declares type arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an actual HOL type
- constructor. %FIXME check, update
+ \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}}
+ axiomatizes a Gordon/HOL-style type definition in the background
+ theory of the current context, depending on a non-emptiness result
+ of the set \isa{A} (which needs to be proven interactively).
+
+ The raw type may not depend on parameters or assumptions of the
+ context --- this is logically impossible in Isabelle/HOL --- but the
+ non-emptiness property can be local, potentially resulting in
+ multiple interpretations in target contexts. Thus the established
+ bijection between the representing set \isa{A} and the new type
+ \isa{t} may semantically depend on local assumptions.
- \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}} sets up
- a goal stating non-emptiness of the set \isa{A}. After finishing
- the proof, the theory will be augmented by a Gordon/HOL-style type
- definition, which establishes a bijection between the representing
- set \isa{A} and the new type \isa{t}.
-
- Technically, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base
- name may be given in parentheses). The injection from type to set
- is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be
- changed via an explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration).
+ By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
+ and a set (term constant) of the same name, unless an alternative
+ base name is given in parentheses, or the ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
+ declaration is used to suppress a separate constant definition
+ altogether. The injection from type to set is called \isa{Rep{\isacharunderscore}t},
+ its inverse \isa{Abs{\isacharunderscore}t} --- this may be changed via an explicit
+ \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
Theorems \isa{Rep{\isacharunderscore}t}, \isa{Rep{\isacharunderscore}t{\isacharunderscore}inverse}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inverse} provide the most basic characterization as a
corresponding injection/surjection pair (in both directions). Rules
@@ -74,17 +75,11 @@
on surjectivity; these are already declared as set or type rules for
the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
- An alternative name may be specified in parentheses; the default is
- to use \isa{t} as indicated before. The ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
- declaration suppresses a separate constant definition for the
- representing set.
+ An alternative name for the set definition (and other derived
+ entities) may be specified in parentheses; the default is to use
+ \isa{t} as indicated before.
- \end{description}
-
- Note that raw type declarations are rarely used in practice; the
- main application is with experimental (or even axiomatic!) theory
- fragments. Instead of primitive HOL type definitions, user-level
- theories usually refer to higher-level packages such as \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}} (see \secref{sec:hol-record}) or \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} (see \secref{sec:hol-datatype}).%
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -920,7 +915,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
+\isamarkupsection{Invoking automated reasoning tools --- The Sledgehammer%
}
\isamarkuptrue%
%
--- a/src/HOL/Import/proof_kernel.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML Sat Mar 13 15:11:59 2010 +0100
@@ -2094,7 +2094,7 @@
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
val ((_, typedef_info), thy') =
- Typedef.add_typedef false (SOME (Binding.name thmname))
+ Typedef.add_typedef_global false (SOME (Binding.name thmname))
(Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy
val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
@@ -2182,7 +2182,7 @@
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
val ((_, typedef_info), thy') =
- Typedef.add_typedef false NONE (Binding.name tycname,tnames,tsyn) c
+ Typedef.add_typedef_global false NONE (Binding.name tycname,tnames,tsyn) c
(SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
val fulltyname = Sign.intern_type thy' tycname
--- a/src/HOL/Import/replay.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Import/replay.ML Sat Mar 13 15:11:59 2010 +0100
@@ -343,7 +343,7 @@
| delta (Hol_theorem (thyname, thmname, th)) thy =
add_hol4_theorem thyname thmname ([], th_of thy th) thy
| delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy =
- snd (Typedef.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
+ snd (Typedef.add_typedef_global false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
(Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
| delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
add_hol4_type_mapping thyname tycname true fulltyname thy
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Mar 13 15:11:59 2010 +0100
@@ -615,7 +615,7 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
- Typedef.add_typedef false (SOME (Binding.name name'))
+ Typedef.add_typedef_global false (SOME (Binding.name name'))
(Binding.name name, map fst tvs, mx)
(Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sat Mar 13 15:11:59 2010 +0100
@@ -190,7 +190,7 @@
val (typedefs, thy3) = thy2 |>
Sign.parent_path |>
fold_map (fn ((((name, mx), tvs), c), name') =>
- Typedef.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
+ Typedef.add_typedef_global false (SOME (Binding.name name')) (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 13 15:11:59 2010 +0100
@@ -560,14 +560,15 @@
set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
|> Logic.varify,
set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
- else case Typedef.get_info thy s of
- SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
- Rep_inverse, ...} =>
+ else case Typedef.get_info_global thy s of
+ (* FIXME handle multiple typedef interpretations (!??) *)
+ [{abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
+ Rep_inverse, ...}] =>
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
Rep_inverse = SOME Rep_inverse}
- | NONE => NONE
+ | _ => NONE
(* theory -> string -> bool *)
val is_typedef = is_some oo typedef_info
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Sat Mar 13 15:11:59 2010 +0100
@@ -75,7 +75,7 @@
EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
in
Local_Theory.theory_result
- (Typedef.add_typedef false NONE
+ (Typedef.add_typedef_global false NONE
(qty_name, vs, mx)
(typedef_term rel rty lthy)
NONE typedef_tac) lthy
--- a/src/HOL/Tools/record.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Tools/record.ML Sat Mar 13 15:11:59 2010 +0100
@@ -104,8 +104,8 @@
let
fun get_thms thy name =
let
- val {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
- Abs_inverse = abs_inverse, ...} = Typedef.the_info thy name;
+ val [{Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
+ Abs_inverse = abs_inverse, ...}] = Typedef.get_info_global thy name;
val rewrite_rule =
MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
in
--- a/src/HOL/Tools/refute.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Tools/refute.ML Sat Mar 13 15:11:59 2010 +0100
@@ -614,7 +614,7 @@
(let
(* Term.term -> Term.typ option *)
fun type_of_type_definition (Const (s', T')) =
- if s'="Typedef.type_definition" then
+ if s'= @{const_name type_definition} then
SOME T'
else
NONE
--- a/src/HOL/Tools/typecopy.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Tools/typecopy.ML Sat Mar 13 15:11:59 2010 +0100
@@ -80,7 +80,7 @@
end
in
thy
- |> Typedef.add_typedef false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
+ |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
(HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
|-> (fn (tyco, info) => add_info tyco info)
end;
@@ -91,8 +91,9 @@
fun add_default_code tyco thy =
let
val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
- typ = ty_rep, ... } = get_info thy tyco;
- val SOME { Rep_inject = proj_inject, ... } = Typedef.get_info thy tyco;
+ typ = ty_rep, ... } = get_info thy tyco;
+ (* FIXME handle multiple typedef interpretations (!??) *)
+ val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
val constr = (c, Logic.unvarifyT (Sign.the_const_type thy c));
val ty = Type (tyco, map TFree vs);
val proj = Const (proj, ty --> ty_rep);
--- a/src/HOL/Tools/typedef.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Sat Mar 13 15:11:59 2010 +0100
@@ -2,7 +2,7 @@
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Gordon/HOL-style type definitions: create a new syntactic type
-represented by a non-empty subset.
+represented by a non-empty set.
*)
signature TYPEDEF =
@@ -12,16 +12,19 @@
type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm}
+ val transform_info: morphism -> info -> info
+ val get_info: Proof.context -> string -> info list
+ val get_info_global: theory -> string -> info list
+ val interpretation: (string -> theory -> theory) -> theory -> theory
+ val setup: theory -> theory
val add_typedef: bool -> binding option -> binding * string list * mixfix ->
+ term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
+ val add_typedef_global: bool -> binding option -> binding * string list * mixfix ->
term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
val typedef: (bool * binding) * (binding * string list * mixfix) * term *
- (binding * binding) option -> theory -> Proof.state
+ (binding * binding) option -> local_theory -> Proof.state
val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string *
- (binding * binding) option -> theory -> Proof.state
- val get_info: theory -> string -> info option
- val the_info: theory -> string -> info
- val interpretation: (string -> theory -> theory) -> theory -> theory
- val setup: theory -> theory
+ (binding * binding) option -> local_theory -> Proof.state
end;
structure Typedef: TYPEDEF =
@@ -32,207 +35,261 @@
(* theory data *)
type info =
- {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
- type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
+ {(*global part*)
+ rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
+ (*local part*)
+ inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm};
-structure TypedefData = Theory_Data
+fun transform_info phi (info: info) =
+ let
+ val thm = Morphism.thm phi;
+ val {rep_type, abs_type, Rep_name, Abs_name, inhabited, type_definition,
+ set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
+ Rep_cases, Abs_cases, Rep_induct, Abs_induct} = info;
+ in
+ {rep_type = rep_type, abs_type = abs_type, Rep_name = Rep_name, Abs_name = Abs_name,
+ inhabited = thm inhabited, type_definition = thm type_definition,
+ set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
+ Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
+ Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
+ Abs_induct = thm Abs_induct}
+ end;
+
+structure Data = Generic_Data
(
- type T = info Symtab.table;
+ type T = info list Symtab.table;
val empty = Symtab.empty;
val extend = I;
- fun merge data = Symtab.merge (K true) data;
+ fun merge data = Symtab.merge_list (K true) data;
);
-val get_info = Symtab.lookup o TypedefData.get;
+val get_info = Symtab.lookup_list o Data.get o Context.Proof;
+val get_info_global = Symtab.lookup_list o Data.get o Context.Theory;
+
+fun put_info name info = Data.map (Symtab.cons_list (name, info));
+
+
+(* global interpretation *)
+
+structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
+val interpretation = Typedef_Interpretation.interpretation;
+
+val setup = Typedef_Interpretation.init;
+
+
+(* primitive typedef axiomatization -- for fresh typedecl *)
+
+fun mk_inhabited A =
+ let val T = HOLogic.dest_setT (Term.fastype_of A)
+ in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end;
+
+fun mk_typedef newT oldT RepC AbsC A =
+ let
+ val typedefC =
+ Const (@{const_name type_definition},
+ (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
+ in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
-fun the_info thy name =
- (case get_info thy name of
- SOME info => info
- | NONE => error ("Unknown typedef " ^ quote name));
+fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A thy =
+ let
+ (* errors *)
+
+ fun show_names pairs = commas_quote (map fst pairs);
+
+ val lhs_tfrees = Term.add_tfreesT newT [];
+ val rhs_tfrees = Term.add_tfreesT oldT [];
+ val _ =
+ (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => ()
+ | extras => error ("Extra type variables in representing set: " ^ show_names extras));
+
+ val _ =
+ (case Term.add_frees A [] of [] => []
+ | xs => error ("Illegal variables in representing set: " ^ show_names xs));
-fun put_info name info = TypedefData.map (Symtab.update (name, info));
+
+ (* axiomatization *)
+
+ val ((RepC, AbsC), consts_thy) = thy
+ |> Sign.declare_const ((Rep_name, newT --> oldT), NoSyn)
+ ||>> Sign.declare_const ((Abs_name, oldT --> newT), NoSyn);
+
+ val typedef_deps = Term.add_consts A [];
+
+ val (axiom, axiom_thy) = consts_thy
+ |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
+ ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
+ ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
+
+ in ((RepC, AbsC, axiom), axiom_thy) end;
(* prepare_typedef *)
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
-val interpretation = Typedef_Interpretation.interpretation;
-
-fun prepare_typedef prep_term def name (tname, vs, mx) raw_set opt_morphs thy =
+fun prepare_typedef prep_term def_set name (tname, vs, mx) raw_set opt_morphs lthy =
let
- val _ = Theory.requires thy "Typedef" "typedefs";
- val ctxt = ProofContext.init thy;
-
- val full = Sign.full_name thy;
- val full_name = full name;
+ val full_name = Local_Theory.full_name lthy name;
val bname = Binding.name_of name;
- (*rhs*)
- val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
+
+ (* rhs *)
+
+ val set = prep_term (lthy |> fold declare_type_name vs) raw_set;
val setT = Term.fastype_of set;
+ val oldT = HOLogic.dest_setT setT handle TYPE _ =>
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT));
+
+ val goal = mk_inhabited set;
+ val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
+
+
+ (* lhs *)
+
+ val (newT, typedecl_lthy) = lthy
+ |> Typedecl.typedecl_wrt [set] (tname, vs, mx)
+ ||> Variable.declare_term set;
+
+ val Type (full_tname, type_args) = newT;
+ val lhs_tfrees = map Term.dest_TFree type_args;
+
+
+ (* set definition *)
+
+ (* FIXME let Local_Theory.define handle hidden polymorphism (!??!) *)
+
val rhs_tfrees = Term.add_tfrees set [];
val rhs_tfreesT = Term.add_tfreesT setT [];
- val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
- (*lhs*)
- val defS = Sign.defaultS thy;
- val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
- val args_setT = lhs_tfrees
+ val set_argsT = lhs_tfrees
|> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
|> map TFree;
+ val set_args = map Logic.mk_type set_argsT;
- val full_tname = full tname;
- val newT = Type (full_tname, map TFree lhs_tfrees);
+ val ((set', set_def), set_lthy) =
+ if def_set then
+ typedecl_lthy
+ |> Local_Theory.define
+ ((name, NoSyn), ((Thm.def_binding name, []), fold_rev lambda set_args set))
+ |>> (fn (s, (_, set_def)) => (Term.list_comb (s, set_args), SOME set_def))
+ else ((set, NONE), typedecl_lthy);
+
+
+ (* axiomatization *)
val (Rep_name, Abs_name) =
(case opt_morphs of
NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
| SOME morphs => morphs);
- val setT' = map Term.itselfT args_setT ---> setT;
- val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
- val RepC = Const (full Rep_name, newT --> oldT);
- val AbsC = Const (full Abs_name, oldT --> newT);
- (*inhabitance*)
- fun mk_inhabited A =
- HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
- val set' = if def then setC else set;
- val goal' = mk_inhabited set';
- val goal = mk_inhabited set;
- val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
-
- (*axiomatization*)
val typedef_name = Binding.prefix_name "type_definition_" name;
- val typedefC =
- Const (@{const_name type_definition},
- (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
- val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
- val typedef_deps = Term.add_consts set' [];
- (*set definition*)
- fun add_def theory =
- if def then
- theory
- |> Sign.add_consts_i [(name, setT', NoSyn)]
- |> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
- |-> (fn [th] => pair (SOME th))
- else (NONE, theory);
- fun contract_def NONE th = th
- | contract_def (SOME def_eq) th =
- let
- val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
- val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
- in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
+ val ((RepC, AbsC, typedef), typedef_lthy) =
+ let
+ val thy = ProofContext.theory_of set_lthy;
+ val cert = Thm.cterm_of thy;
+ val (defs, A) =
+ Local_Defs.export_cterm set_lthy (ProofContext.init thy) (cert set') ||> Thm.term_of;
- fun typedef_result inhabited =
- Typedecl.typedecl_global (tname, vs, mx)
- #> snd
- #> Sign.add_consts_i
- [(Rep_name, newT --> oldT, NoSyn),
- (Abs_name, oldT --> newT, NoSyn)]
- #> add_def
- #-> (fn set_def =>
- PureThy.add_axioms [((typedef_name, typedef_prop),
- [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
- ##>> pair set_def)
- ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
- ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
- #-> (fn ([type_definition], set_def) => fn thy1 =>
- let
- fun make th = Drule.export_without_context (th OF [type_definition]);
- val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
- Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
- thy1
- |> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thms
- [((Rep_name, make @{thm type_definition.Rep}), []),
- ((Binding.suffix_name "_inverse" Rep_name, make @{thm type_definition.Rep_inverse}), []),
- ((Binding.suffix_name "_inverse" Abs_name, make @{thm type_definition.Abs_inverse}), []),
- ((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
- ((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
- ((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
- [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
- ((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
- [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
- ((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
- [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
- ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
- [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
- ||> Sign.restore_naming thy1;
- val info = {rep_type = oldT, abs_type = newT,
- Rep_name = full Rep_name, Abs_name = full Abs_name,
- inhabited = inhabited, type_definition = type_definition, set_def = set_def,
- Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
- Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
- Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
- in
- thy2
- |> put_info full_tname info
- |> Typedef_Interpretation.data full_tname
- |> pair (full_tname, info)
- end);
+ val ((RepC, AbsC, axiom), axiom_lthy) = set_lthy |>
+ Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
+
+ val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy);
+ val typedef =
+ Local_Defs.contract axiom_lthy defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
+ in ((RepC, AbsC, typedef), axiom_lthy) end;
+
+ val alias_lthy = typedef_lthy
+ |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
+ |> Local_Theory.const_alias Abs_name (#1 (Term.dest_Const AbsC));
- (* errors *)
-
- fun show_names pairs = commas_quote (map fst pairs);
+ (* result *)
- val illegal_vars =
- if null (Term.add_vars set []) andalso null (Term.add_tvars set []) then []
- else ["Illegal schematic variable(s) on rhs"];
-
- val dup_lhs_tfrees =
- (case duplicates (op =) lhs_tfrees of [] => []
- | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
+ fun note_qualify ((b, atts), th) =
+ Local_Theory.note ((Binding.qualify false bname b, map (Attrib.internal o K) atts), [th])
+ #>> (fn (_, [th']) => th');
- val extra_rhs_tfrees =
- (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => []
- | extras => ["Extra type variables on rhs: " ^ show_names extras]);
-
- val illegal_frees =
- (case Term.add_frees set [] of [] => []
- | xs => ["Illegal variables on rhs: " ^ show_names xs]);
+ fun typedef_result inhabited lthy1 =
+ let
+ val cert = Thm.cterm_of (ProofContext.theory_of lthy1);
+ val inhabited' =
+ Local_Defs.contract lthy1 (the_list set_def) (cert (mk_inhabited set')) inhabited;
+ val typedef' = inhabited' RS typedef;
+ fun make th = Goal.norm_result (typedef' RS th);
+ val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
+ Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
+ |> Local_Theory.note ((typedef_name, []), [typedef'])
+ ||>> note_qualify ((Rep_name, []), make @{thm type_definition.Rep})
+ ||>> note_qualify ((Binding.suffix_name "_inverse" Rep_name, []),
+ make @{thm type_definition.Rep_inverse})
+ ||>> note_qualify ((Binding.suffix_name "_inverse" Abs_name, []),
+ make @{thm type_definition.Abs_inverse})
+ ||>> note_qualify ((Binding.suffix_name "_inject" Rep_name, []),
+ make @{thm type_definition.Rep_inject})
+ ||>> note_qualify ((Binding.suffix_name "_inject" Abs_name, []),
+ make @{thm type_definition.Abs_inject})
+ ||>> note_qualify ((Binding.suffix_name "_cases" Rep_name,
+ [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
+ make @{thm type_definition.Rep_cases})
+ ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name,
+ [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
+ make @{thm type_definition.Abs_cases})
+ ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name,
+ [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
+ make @{thm type_definition.Rep_induct})
+ ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name,
+ [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]),
+ make @{thm type_definition.Abs_induct});
- val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
- val _ = if null errs then () else error (cat_lines errs);
+ val info = {rep_type = oldT, abs_type = newT,
+ Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC),
+ inhabited = inhabited, type_definition = type_definition, set_def = set_def,
+ Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
+ Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
+ Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
+ in
+ lthy2
+ |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
+ |> Local_Theory.theory (Typedef_Interpretation.data full_tname)
+ |> pair (full_tname, info)
+ end;
- (*test theory errors now!*)
- val test_thy = Theory.copy thy;
- val _ = typedef_result (Skip_Proof.make_thm test_thy goal) test_thy;
-
- in (set, goal, goal_pat, typedef_result) end
+ in ((goal, goal_pat, typedef_result), alias_lthy) end
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
(* add_typedef: tactic interface *)
-fun add_typedef def opt_name typ set opt_morphs tac thy =
+fun add_typedef def opt_name typ set opt_morphs tac lthy =
let
val name = the_default (#1 typ) opt_name;
- val (set, goal, _, typedef_result) =
- prepare_typedef Syntax.check_term def name typ set opt_morphs thy;
- val inhabited = Goal.prove_global thy [] [] goal (K tac)
- handle ERROR msg => cat_error msg
- ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
- in typedef_result inhabited thy end;
+ val ((goal, _, typedef_result), lthy') =
+ prepare_typedef Syntax.check_term def name typ set opt_morphs lthy;
+ val inhabited =
+ Goal.prove lthy' [] [] goal (K tac)
+ |> Goal.norm_result |> Thm.close_derivation;
+ in typedef_result inhabited lthy' end;
+
+fun add_typedef_global def opt_name typ set opt_morphs tac =
+ Theory_Target.init NONE
+ #> add_typedef def opt_name typ set opt_morphs tac
+ #> Local_Theory.exit_result_global (apsnd o transform_info);
(* typedef: proof interface *)
local
-fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy =
+fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) lthy =
let
- val (_, goal, goal_pat, typedef_result) =
- prepare_typedef prep_term def name typ set opt_morphs thy;
- fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
- in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end;
+ val ((goal, goal_pat, typedef_result), lthy') =
+ prepare_typedef prep_term def name typ set opt_morphs lthy;
+ fun after_qed [[th]] = snd o typedef_result th;
+ in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end;
in
@@ -250,7 +307,7 @@
val _ = OuterKeyword.keyword "morphisms";
val _ =
- OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
+ OuterSyntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
OuterKeyword.thy_goal
(Scan.optional (P.$$$ "(" |--
((P.$$$ "open" >> K false) -- Scan.option P.binding ||
@@ -258,11 +315,9 @@
(P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
>> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) =>
- Toplevel.print o Toplevel.theory_to_proof
- (typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs))));
+ typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs)));
end;
-val setup = Typedef_Interpretation.init;
+end;
-end;
--- a/src/HOL/Tools/typedef_codegen.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOL/Tools/typedef_codegen.ML Sat Mar 13 15:11:59 2010 +0100
@@ -24,9 +24,10 @@
val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
fun lookup f T =
- (case Typedef.get_info thy (get_name T) of
- NONE => ""
- | SOME info => f info);
+ (* FIXME handle multiple typedef interpretations (!??) *)
+ (case Typedef.get_info_global thy (get_name T) of
+ [info] => f info
+ | _ => "");
in
(case strip_comb t of
(Const (s, Type ("fun", [T, U])), ts) =>
@@ -45,58 +46,61 @@
| mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
- (case Typedef.get_info thy s of
- NONE => NONE
- | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} =>
- if is_some (Codegen.get_assoc_type thy tname) then NONE else
- let
- val module' = Codegen.if_library
- (Codegen.thyname_of_type thy tname) module;
- val node_id = tname ^ " (type)";
- val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
- (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
- Ts ||>>
- Codegen.mk_const_id module' Abs_name ||>>
- Codegen.mk_const_id module' Rep_name ||>>
- Codegen.mk_type_id module' s;
- val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
- in SOME (tyexpr, case try (Codegen.get_node gr') node_id of
- NONE =>
- let
- val (p :: ps, gr'') = fold_map
- (Codegen.invoke_tycodegen thy defs node_id module' false)
- (oldT :: Us) (Codegen.add_edge (node_id, dep)
- (Codegen.new_node (node_id, (NONE, "", "")) gr'));
- val s =
- Codegen.string_of (Pretty.block [Codegen.str "datatype ",
- mk_tyexpr ps (snd ty_id),
- Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
- Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
- Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
- Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
- Codegen.str "x) = x;"]) ^ "\n\n" ^
- (if "term_of" mem !Codegen.mode then
- Codegen.string_of (Pretty.block [Codegen.str "fun ",
- Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
- Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
- Codegen.str "x) =", Pretty.brk 1,
- Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
- Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
- Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
- Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
- Codegen.str "x;"]) ^ "\n\n"
- else "") ^
- (if "test" mem !Codegen.mode then
- Codegen.string_of (Pretty.block [Codegen.str "fun ",
- Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
- Codegen.str "i =", Pretty.brk 1,
- Pretty.block [Codegen.str (Abs_id ^ " ("),
- Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
- Codegen.str "i);"]]) ^ "\n\n"
- else "")
- in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
- | SOME _ => Codegen.add_edge (node_id, dep) gr')
- end)
+ (case Typedef.get_info_global thy s of
+ (* FIXME handle multiple typedef interpretations (!??) *)
+ [{abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}] =>
+ if is_some (Codegen.get_assoc_type thy tname) then NONE
+ else
+ let
+ val module' = Codegen.if_library
+ (Codegen.thyname_of_type thy tname) module;
+ val node_id = tname ^ " (type)";
+ val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
+ (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
+ Ts ||>>
+ Codegen.mk_const_id module' Abs_name ||>>
+ Codegen.mk_const_id module' Rep_name ||>>
+ Codegen.mk_type_id module' s;
+ val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
+ in
+ SOME (tyexpr, case try (Codegen.get_node gr') node_id of
+ NONE =>
+ let
+ val (p :: ps, gr'') = fold_map
+ (Codegen.invoke_tycodegen thy defs node_id module' false)
+ (oldT :: Us) (Codegen.add_edge (node_id, dep)
+ (Codegen.new_node (node_id, (NONE, "", "")) gr'));
+ val s =
+ Codegen.string_of (Pretty.block [Codegen.str "datatype ",
+ mk_tyexpr ps (snd ty_id),
+ Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
+ Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
+ Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
+ Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
+ Codegen.str "x) = x;"]) ^ "\n\n" ^
+ (if "term_of" mem !Codegen.mode then
+ Codegen.string_of (Pretty.block [Codegen.str "fun ",
+ Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
+ Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
+ Codegen.str "x) =", Pretty.brk 1,
+ Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
+ Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
+ Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
+ Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
+ Codegen.str "x;"]) ^ "\n\n"
+ else "") ^
+ (if "test" mem !Codegen.mode then
+ Codegen.string_of (Pretty.block [Codegen.str "fun ",
+ Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
+ Codegen.str "i =", Pretty.brk 1,
+ Pretty.block [Codegen.str (Abs_id ^ " ("),
+ Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
+ Codegen.str "i);"]]) ^ "\n\n"
+ else "")
+ in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
+ | SOME _ => Codegen.add_edge (node_id, dep) gr')
+ end
+ | _ => NONE)
| typedef_tycodegen thy defs dep module brack _ gr = NONE;
val setup =
--- a/src/HOLCF/Tools/pcpodef.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Sat Mar 13 15:11:59 2010 +0100
@@ -181,7 +181,7 @@
let
val name = the_default (#1 typ) opt_name;
val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy
- |> Typedef.add_typedef def opt_name typ set opt_morphs tac;
+ |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
val oldT = #rep_type info;
val newT = #abs_type info;
val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
--- a/src/Pure/Isar/local_defs.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/Pure/Isar/local_defs.ML Sat Mar 13 15:11:59 2010 +0100
@@ -20,6 +20,7 @@
val export_cterm: Proof.context -> Proof.context -> cterm -> thm list * cterm
val trans_terms: Proof.context -> thm list -> thm
val trans_props: Proof.context -> thm list -> thm
+ val contract: Proof.context -> thm list -> cterm -> thm -> thm
val print_rules: Proof.context -> unit
val defn_add: attribute
val defn_del: attribute
@@ -179,6 +180,8 @@
end;
+fun contract ctxt defs ct th =
+ trans_props ctxt [th, Thm.symmetric (MetaSimplifier.rewrite true defs ct)];
(** defived definitions **)
--- a/src/Pure/Isar/local_theory.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/Pure/Isar/local_theory.ML Sat Mar 13 15:11:59 2010 +0100
@@ -44,6 +44,9 @@
val declaration: bool -> declaration -> local_theory -> local_theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
+ val class_alias: binding -> class -> local_theory -> local_theory
+ val type_alias: binding -> string -> local_theory -> local_theory
+ val const_alias: binding -> string -> local_theory -> local_theory
val init: serial option -> string -> operations -> Proof.context -> local_theory
val restore: local_theory -> local_theory
val reinit: local_theory -> local_theory
@@ -199,6 +202,9 @@
val notes = notes_kind "";
fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
+
+(* notation *)
+
fun type_notation add mode raw_args lthy =
let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
in type_syntax false (ProofContext.target_type_notation add mode args) lthy end;
@@ -208,6 +214,19 @@
in term_syntax false (ProofContext.target_notation add mode args) lthy end;
+(* name space aliases *)
+
+fun alias syntax_declaration global_alias local_alias b name =
+ syntax_declaration false (fn phi =>
+ let val b' = Morphism.binding phi b
+ in Context.mapping (global_alias b' name) (local_alias b' name) end)
+ #> local_alias b name;
+
+val class_alias = alias type_syntax Sign.class_alias ProofContext.class_alias;
+val type_alias = alias type_syntax Sign.type_alias ProofContext.type_alias;
+val const_alias = alias term_syntax Sign.const_alias ProofContext.const_alias;
+
+
(* init *)
fun init group theory_prefix operations target =
--- a/src/Pure/Isar/theory_target.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML Sat Mar 13 15:11:59 2010 +0100
@@ -122,7 +122,6 @@
(*export assumes/defines*)
val th = Goal.norm_result raw_th;
val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
- val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
val nprems = Thm.nprems_of th' - Thm.nprems_of th;
@@ -152,7 +151,7 @@
val result'' =
(case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
NONE => raise THM ("Failed to re-import result", 0, [result'])
- | SOME res => Local_Defs.trans_props ctxt [res, Thm.symmetric concl_conv])
+ | SOME res => Local_Defs.contract ctxt defs (Thm.cprop_of th) res)
|> Goal.norm_result
|> PureThy.name_thm false false name;
--- a/src/Pure/Isar/typedecl.ML Fri Mar 12 20:04:48 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML Sat Mar 13 15:11:59 2010 +0100
@@ -6,6 +6,8 @@
signature TYPEDECL =
sig
+ val typedecl_wrt: term list -> binding * string list * mixfix ->
+ local_theory -> typ * local_theory
val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory
val typedecl_global: binding * string list * mixfix -> theory -> typ * theory
end;
@@ -13,21 +15,24 @@
structure Typedecl: TYPEDECL =
struct
-fun typedecl (b, vs, mx) lthy =
+fun typedecl_wrt terms (b, vs, mx) lthy =
let
fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
val _ = has_duplicates (op =) vs andalso err "Duplicate parameters";
val name = Local_Theory.full_name lthy b;
val n = length vs;
- val args = map (fn a => TFree (a, ProofContext.default_sort lthy (a, ~1))) vs;
+
+ val args_ctxt = lthy |> fold Variable.declare_constraints terms;
+ val args = map (fn a => TFree (a, ProofContext.default_sort args_ctxt (a, ~1))) vs;
val T = Type (name, args);
val bad_args =
#2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
|> filter_out Term.is_TVar;
val _ = not (null bad_args) andalso
- err ("Locally fixed type arguments " ^ commas_quote (map (Syntax.string_of_typ lthy) bad_args));
+ err ("Locally fixed type arguments " ^
+ commas_quote (map (Syntax.string_of_typ args_ctxt) bad_args));
val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy);
in
@@ -37,16 +42,14 @@
(case base_sort of
NONE => I
| SOME S => AxClass.axiomatize_arity (name, replicate n S, S)))
- |> Local_Theory.checkpoint
|> Local_Theory.type_notation true Syntax.mode_default [(T, mx)]
- |> Local_Theory.type_syntax false (fn phi =>
- let val b' = Morphism.binding phi b
- in Context.mapping (Sign.type_alias b' name) (ProofContext.type_alias b' name) end)
- |> ProofContext.type_alias b name
+ |> Local_Theory.type_alias b name
|> Variable.declare_typ T
|> pair T
end;
+val typedecl = typedecl_wrt [];
+
fun typedecl_global decl =
Theory_Target.init NONE
#> typedecl decl