--- a/src/HOL/Code_Evaluation.thy Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Wed Aug 11 14:31:43 2010 +0200
@@ -64,7 +64,7 @@
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
in
thy
- |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
+ |> Class.instantiation ([tyco], vs, @{sort term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
|> snd
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 11 14:31:43 2010 +0200
@@ -115,7 +115,7 @@
#> snd
in
thy
- |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
+ |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
|> fold_map add_def dtcos
|-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
(fn _ => fn def_thms => tac def_thms) def_thms)
--- a/src/HOL/Tools/Function/size.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML Wed Aug 11 14:31:43 2010 +0200
@@ -145,7 +145,7 @@
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
(map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
- ||> Theory_Target.instantiation
+ ||> Class.instantiation
(map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
||>> fold_map define_overloaded
(def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
--- a/src/HOL/Tools/quickcheck_generators.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Aug 11 14:31:43 2010 +0200
@@ -86,7 +86,7 @@
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
thy
- |> Theory_Target.instantiation ([tyco], vs, @{sort random})
+ |> Class.instantiation ([tyco], vs, @{sort random})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
|> snd
@@ -304,7 +304,7 @@
(HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
in
thy
- |> Theory_Target.instantiation (tycos, vs, @{sort random})
+ |> Class.instantiation (tycos, vs, @{sort random})
|> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
--- a/src/HOL/Tools/typecopy.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML Wed Aug 11 14:31:43 2010 +0200
@@ -116,7 +116,7 @@
thy
|> Code.add_datatype [constr]
|> Code.add_eqn proj_constr
- |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
+ |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition
(NONE, (Attrib.empty_binding, eq)))
--- a/src/HOL/Typerep.thy Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Typerep.thy Wed Aug 11 14:31:43 2010 +0200
@@ -56,7 +56,7 @@
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in
thy
- |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
+ |> Class.instantiation ([tyco], vs, @{sort typerep})
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
|> snd
--- a/src/HOLCF/Tools/pcpodef.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Wed Aug 11 14:31:43 2010 +0200
@@ -203,7 +203,7 @@
val below_eqn = Logic.mk_equals (below_const newT,
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
val lthy3 = thy2
- |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
val ((_, (_, below_ldef)), lthy4) = lthy3
|> Specification.definition (NONE,
((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
--- a/src/HOLCF/Tools/repdef.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML Wed Aug 11 14:31:43 2010 +0200
@@ -112,7 +112,7 @@
(*instantiate class rep*)
val lthy = thy
- |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep});
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort rep});
val ((_, (_, emb_ldef)), lthy) =
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
val ((_, (_, prj_ldef)), lthy) =
--- a/src/Pure/Isar/class_target.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Wed Aug 11 14:31:43 2010 +0200
@@ -47,6 +47,8 @@
val read_multi_arity: theory -> xstring list * xstring list * xstring
-> string list * (string * sort) list * sort
val type_name: string -> string
+ val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
+ val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
(*subclasses*)
val register_subclass: class * class -> morphism option -> Element.witness option
@@ -580,6 +582,35 @@
(Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
end;
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+ case instantiation_param lthy b
+ of SOME c => if mx <> NoSyn then syntax_error c
+ else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
+ ##>> AxClass.define_overloaded b_def (c, rhs))
+ ||> confirm_declaration b
+ | NONE => lthy |>
+ Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun instantiation arities thy =
+ thy
+ |> init_instantiation arities
+ |> Local_Theory.init NONE ""
+ {define = Generic_Target.define instantiation_foundation,
+ notes = Generic_Target.notes
+ (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+ abbrev = Generic_Target.abbrev
+ (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+ declaration = K Generic_Target.theory_declaration,
+ syntax_declaration = K Generic_Target.theory_declaration,
+ pretty = single o pretty_instantiation,
+ reinit = instantiation arities o ProofContext.theory_of,
+ exit = Local_Theory.target_of o conclude_instantiation};
+
+fun instantiation_cmd arities thy =
+ instantiation (read_multi_arity thy arities) thy;
+
(* simplified instantiation interface with no class parameter *)
--- a/src/Pure/Isar/isar_syn.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Aug 11 14:31:43 2010 +0200
@@ -472,7 +472,7 @@
Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
(Parse.multi_arity --| Parse.begin
>> (fn arities => Toplevel.print o
- Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
+ Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
val _ =
Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
--- a/src/Pure/Isar/theory_target.ML Wed Aug 11 14:31:40 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Wed Aug 11 14:31:43 2010 +0200
@@ -10,8 +10,6 @@
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
val init: string option -> theory -> local_theory
val context_cmd: xstring -> theory -> local_theory
- val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
- val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
end;
structure Theory_Target: THEORY_TARGET =
@@ -89,8 +87,6 @@
(* define *)
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-
fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
@@ -103,14 +99,7 @@
#> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
#> pair (lhs, def))
-fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- case Class_Target.instantiation_param lthy b
- of SOME c => if mx <> NoSyn then syntax_error c
- else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
- ##>> AxClass.define_overloaded b_def (c, rhs))
- ||> Class_Target.confirm_declaration b
- | NONE => lthy |>
- Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
if not is_locale then (NoSyn, NoSyn, mx)
@@ -253,24 +242,6 @@
fun context_cmd "-" thy = init NONE thy
| context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
-fun instantiation arities thy =
- thy
- |> Class_Target.init_instantiation arities
- |> Local_Theory.init NONE ""
- {define = Generic_Target.define instantiation_foundation,
- notes = Generic_Target.notes
- (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
- abbrev = Generic_Target.abbrev
- (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
- declaration = K Generic_Target.theory_declaration,
- syntax_declaration = K Generic_Target.theory_declaration,
- pretty = single o Class_Target.pretty_instantiation,
- reinit = instantiation arities o ProofContext.theory_of,
- exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
-
-fun instantiation_cmd arities thy =
- instantiation (Class_Target.read_multi_arity thy arities) thy;
-
end;
end;