--- a/src/HOL/Tools/TFL/post.ML Mon Mar 15 17:34:03 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML Mon Mar 15 22:22:28 2010 +0100
@@ -203,7 +203,7 @@
*---------------------------------------------------------------------------*)
fun define_i strict thy cs ss congs wfs fid R eqs =
let val {functional,pats} = Prim.mk_functional thy eqs
- val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional
+ val (thy, def) = Prim.wfrec_definition0 thy fid R functional
val (lhs, _) = Logic.dest_equals (prop_of def)
val {induct, rules, tcs} =
simplify_defn strict thy cs ss congs wfs fid pats def
@@ -228,8 +228,7 @@
#1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));
fun defer_i thy congs fid eqs =
- let val {rules,R,theory,full_pats_TCs,SV,...} =
- Prim.lazyR_def thy (Long_Name.base_name fid) congs eqs
+ let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
val dummy = writeln "Proving induction theorem ...";
val induction = Prim.mk_induction theory
--- a/src/HOL/Tools/TFL/tfl.ML Mon Mar 15 17:34:03 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Mon Mar 15 22:22:28 2010 +0100
@@ -360,9 +360,9 @@
(*For Isabelle, the lhs of a definition must be a constant.*)
-fun legacy_const_def sign (c, Ty, rhs) =
+fun const_def sign (c, Ty, rhs) =
singleton (Syntax.check_terms (ProofContext.init sign))
- (Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
+ (Const("==",dummyT) $ Const(c,Ty) $ rhs);
(*Make all TVars available for instantiation by adding a ? to the front*)
fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
@@ -376,17 +376,13 @@
val (wfrec,_) = S.strip_comb rhs
in
fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
- let val def_name = if x<>fid then
- raise TFL_ERR "wfrec_definition0"
- ("Expected a definition of " ^
- quote fid ^ " but found one of " ^
- quote x)
- else x ^ "_def"
+ let val def_name = Long_Name.base_name fid ^ "_def"
val wfrec_R_M = map_types poly_tvars
(wfrec $ map_types poly_tvars R)
$ functional
- val def_term = legacy_const_def thy (x, Ty, wfrec_R_M)
- val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
+ val def_term = const_def thy (fid, Ty, wfrec_R_M)
+ val ([def], thy') =
+ PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
in (thy', def) end;
end;
@@ -540,7 +536,7 @@
val {lhs,rhs} = S.dest_eq proto_def'
val (c,args) = S.strip_comb lhs
val (name,Ty) = dest_atom c
- val defn = legacy_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
+ val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs))
val ([def0], theory) =
thy
|> PureThy.add_defs false
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 15 17:34:03 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Mar 15 22:22:28 2010 +0100
@@ -50,9 +50,29 @@
(* ----- general proof facilities ------------------------------------------- *)
+local
+
+fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
+ | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
+ | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
+
+fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
+ | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
+ | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
+ | map_term _ _ _ (t as Bound _) = t
+ | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
+ | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
+
+in
+
+fun intern_term thy =
+ map_term (Sign.intern_class thy) (Sign.intern_type thy) (Sign.intern_const thy);
+
+end;
+
fun legacy_infer_term thy t =
let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
- in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end;
+ in singleton (Syntax.check_terms ctxt) (intern_term thy t) end;
fun pg'' thy defs t tacs =
let
@@ -451,7 +471,7 @@
local
fun legacy_infer_term thy t =
- singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
+ singleton (Syntax.check_terms (ProofContext.init thy)) (intern_term thy t);
fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
fun infer_props thy = map (apsnd (legacy_infer_prop thy));
fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
--- a/src/Pure/Isar/expression.ML Mon Mar 15 17:34:03 2010 +0100
+++ b/src/Pure/Isar/expression.ML Mon Mar 15 22:22:28 2010 +0100
@@ -772,7 +772,7 @@
val loc_ctxt = thy'
|> Locale.register_locale binding (extraTs, params)
- (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
+ (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
|> Theory_Target.init (SOME name)
|> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
--- a/src/Pure/Isar/local_theory.ML Mon Mar 15 17:34:03 2010 +0100
+++ b/src/Pure/Isar/local_theory.ML Mon Mar 15 22:22:28 2010 +0100
@@ -39,9 +39,8 @@
local_theory -> (string * thm list) list * local_theory
val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
local_theory -> (string * thm list) list * local_theory
- val type_syntax: bool -> declaration -> local_theory -> local_theory
- val term_syntax: bool -> declaration -> local_theory -> local_theory
val declaration: bool -> declaration -> local_theory -> local_theory
+ val syntax_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
@@ -72,9 +71,8 @@
notes: string ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
local_theory -> (string * thm list) list * local_theory,
- type_syntax: bool -> declaration -> local_theory -> local_theory,
- term_syntax: bool -> declaration -> local_theory -> local_theory,
declaration: bool -> declaration -> local_theory -> local_theory,
+ syntax_declaration: bool -> declaration -> local_theory -> local_theory,
reinit: local_theory -> local_theory,
exit: local_theory -> Proof.context};
@@ -195,9 +193,8 @@
val abbrev = apsnd checkpoint ooo operation2 #abbrev;
val define = apsnd checkpoint oo operation1 #define;
val notes_kind = apsnd checkpoint ooo operation2 #notes;
-val type_syntax = checkpoint ooo operation2 #type_syntax;
-val term_syntax = checkpoint ooo operation2 #term_syntax;
val declaration = checkpoint ooo operation2 #declaration;
+val syntax_declaration = checkpoint ooo operation2 #syntax_declaration;
val notes = notes_kind "";
fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
@@ -207,24 +204,24 @@
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;
+ in syntax_declaration false (ProofContext.target_type_notation add mode args) lthy end;
fun notation add mode raw_args lthy =
let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
- in term_syntax false (ProofContext.target_notation add mode args) lthy end;
+ in syntax_declaration false (ProofContext.target_notation add mode args) lthy end;
(* name space aliases *)
-fun alias syntax_declaration global_alias local_alias b name =
+fun alias 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;
+val class_alias = alias Sign.class_alias ProofContext.class_alias;
+val type_alias = alias Sign.type_alias ProofContext.type_alias;
+val const_alias = alias Sign.const_alias ProofContext.const_alias;
(* init *)
--- a/src/Pure/Isar/locale.ML Mon Mar 15 17:34:03 2010 +0100
+++ b/src/Pure/Isar/locale.ML Mon Mar 15 22:22:28 2010 +0100
@@ -33,7 +33,7 @@
(string * sort) list * ((string * typ) * mixfix) list ->
term option * term list ->
thm option * thm option -> thm list ->
- declaration list * declaration list ->
+ declaration list ->
(string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
(string * morphism) list -> theory -> theory
val intern: theory -> xstring -> string
@@ -44,14 +44,12 @@
val axioms_of: theory -> string -> thm list
val instance_of: theory -> string -> morphism -> term list
val specification_of: theory -> string -> term option * term list
- val declarations_of: theory -> string -> declaration list * declaration list
(* Storing results *)
val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
Proof.context -> Proof.context
- val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
- val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
val add_declaration: string -> declaration -> Proof.context -> Proof.context
+ val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
(* Activation *)
val activate_declarations: string * morphism -> Proof.context -> Proof.context
@@ -97,26 +95,27 @@
intros: thm option * thm option,
axioms: thm list,
(** dynamic part **)
- decls: (declaration * stamp) list * (declaration * stamp) list,
- (* type and term syntax declarations *)
+ syntax_decls: (declaration * stamp) list,
+ (* syntax declarations *)
notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
(* theorem declarations *)
dependencies: ((string * morphism) * stamp) list
(* locale dependencies (sublocale relation) *)
};
-fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
+fun mk_locale ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)) =
Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
- decls = decls, notes = notes, dependencies = dependencies};
+ syntax_decls = syntax_decls, notes = notes, dependencies = dependencies};
+
+fun map_locale f (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies}) =
+ mk_locale (f ((parameters, spec, intros, axioms), ((syntax_decls, notes), dependencies)));
-fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
- mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
-
-fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
- notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
- dependencies = dependencies', ...}) = mk_locale
+fun merge_locale
+ (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies},
+ Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', ...}) =
+ mk_locale
((parameters, spec, intros, axioms),
- (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
+ ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
merge (eq_snd op =) (notes, notes')),
merge (eq_snd op =) (dependencies, dependencies')));
@@ -139,11 +138,11 @@
SOME (Loc loc) => loc
| NONE => error ("Unknown locale " ^ quote name));
-fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
+fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
(binding,
mk_locale ((parameters, spec, intros, axioms),
- ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
+ ((map (fn decl => (decl, stamp ())) syntax_decls, map (fn n => (n, stamp ())) notes),
map (fn d => (d, stamp ())) dependencies))) #> snd);
fun change_locale name =
@@ -167,9 +166,6 @@
fun specification_of thy = #spec o the_locale thy;
-fun declarations_of thy name = the_locale thy name |>
- #decls |> pairself (map fst);
-
fun dependencies_of thy name = the_locale thy name |>
#dependencies |> map fst;
@@ -257,14 +253,13 @@
(* Declarations, facts and entire locale content *)
-fun activate_decls (name, morph) context =
+fun activate_syntax_decls (name, morph) context =
let
val thy = Context.theory_of context;
- val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
+ val {syntax_decls, ...} = the_locale thy name;
in
context
- |> fold_rev (fn (decl, _) => decl morph) typ_decls
- |> fold_rev (fn (decl, _) => decl morph) term_decls
+ |> fold_rev (fn (decl, _) => decl morph) syntax_decls
end;
fun activate_notes activ_elem transfer thy (name, morph) input =
@@ -300,7 +295,10 @@
fun activate_declarations dep = Context.proof_map (fn context =>
let
val thy = Context.theory_of context;
- in roundup thy activate_decls Morphism.identity dep (get_idents context, context) |-> put_idents end);
+ in
+ roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
+ |-> put_idents
+ end);
fun activate_facts dep context =
let
@@ -512,23 +510,15 @@
(* Declarations *)
-local
-
-fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
-
-fun add_decls add loc decl =
- ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
+fun add_declaration loc decl =
add_thmss loc ""
- [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
+ [((Binding.conceal Binding.empty,
+ [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
[([Drule.dummy_thm], [])])];
-in
-
-val add_type_syntax = add_decls (apfst o cons);
-val add_term_syntax = add_decls (apsnd o cons);
-val add_declaration = add_decls (K I);
-
-end;
+fun add_syntax_declaration loc decl =
+ ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, stamp ())))
+ #> add_declaration loc decl;
(*** Reasoning about locales ***)
--- a/src/Pure/Isar/theory_target.ML Mon Mar 15 17:34:03 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML Mon Mar 15 22:22:28 2010 +0100
@@ -99,9 +99,8 @@
in
-val type_syntax = target_decl Locale.add_type_syntax;
-val term_syntax = target_decl Locale.add_term_syntax;
val declaration = target_decl Locale.add_declaration;
+val syntax_declaration = target_decl Locale.add_syntax_declaration;
end;
@@ -229,7 +228,7 @@
Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
#-> (fn (lhs, _) =>
let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
- term_syntax ta false (locale_const ta prmode ((b, mx2), lhs')) #>
+ syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
end)
else
@@ -277,7 +276,7 @@
val t = Term.list_comb (const, params);
in
lthy'
- |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
+ |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
|> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
|> Local_Defs.add_def ((b, NoSyn), t)
end;
@@ -354,9 +353,8 @@
abbrev = abbrev ta,
define = define ta,
notes = notes ta,
- type_syntax = type_syntax ta,
- term_syntax = term_syntax ta,
declaration = declaration ta,
+ syntax_declaration = syntax_declaration ta,
reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
exit = Local_Theory.target_of o
(if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
--- a/src/Pure/sign.ML Mon Mar 15 17:34:03 2010 +0100
+++ b/src/Pure/sign.ML Mon Mar 15 22:22:28 2010 +0100
@@ -56,7 +56,6 @@
val extern_type: theory -> string -> xstring
val intern_const: theory -> xstring -> string
val extern_const: theory -> string -> xstring
- val intern_term: theory -> term -> term
val arity_number: theory -> string -> int
val arity_sorts: theory -> string -> sort -> sort list
val certify_class: theory -> class -> class
@@ -143,7 +142,7 @@
fun make_sign (naming, syn, tsig, consts) =
Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
-structure SignData = Theory_Data_PP
+structure Data = Theory_Data_PP
(
type T = sign;
fun extend (Sign {syn, tsig, consts, ...}) =
@@ -164,9 +163,9 @@
in make_sign (naming, syn, tsig, consts) end;
);
-fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
+fun rep_sg thy = Data.get thy |> (fn Sign args => args);
-fun map_sign f = SignData.map (fn Sign {naming, syn, tsig, consts} =>
+fun map_sign f = Data.map (fn Sign {naming, syn, tsig, consts} =>
make_sign (f (naming, syn, tsig, consts)));
fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts));
@@ -247,25 +246,6 @@
val intern_const = Name_Space.intern o const_space;
val extern_const = Name_Space.extern o const_space;
-local
-
-fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
- | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
- | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
-
-fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
- | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
- | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
- | map_term _ _ _ (t as Bound _) = t
- | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
- | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
-
-in
-
-fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
-
-end;
-
(** certify entities **) (*exception TYPE*)