# HG changeset patch # User haftmann # Date 1232553105 -3600 # Node ID 88ba5e5ac6d84c35e67493f39cca8e16f0bc5235 # Parent bb0f395db245581e0e24c8bfd6122e63fbe31347# Parent 1f930609dcd096713fe7b364506dd9d25aba2f07 merged diff -r bb0f395db245 -r 88ba5e5ac6d8 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 21 16:51:45 2009 +0100 @@ -317,7 +317,7 @@ a theory by constant declararion and primitive definitions: \smallskip\begin{mldecls} - @{ML "Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix + @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory"} \\ @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"} \end{mldecls} diff -r bb0f395db245 -r 88ba5e5ac6d8 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Jan 20 19:09:19 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 21 16:51:45 2009 +0100 @@ -366,7 +366,7 @@ a theory by constant declararion and primitive definitions: \smallskip\begin{mldecls} - \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline% + \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline% \verb| -> theory -> term * theory| \\ \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory| \end{mldecls} diff -r bb0f395db245 -r 88ba5e5ac6d8 doc-src/IsarImplementation/Thy/document/logic.tex --- a/doc-src/IsarImplementation/Thy/document/logic.tex Tue Jan 20 19:09:19 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex Wed Jan 21 16:51:45 2009 +0100 @@ -325,9 +325,9 @@ \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\ \indexml{lambda}\verb|lambda: term -> term -> term| \\ \indexml{betapply}\verb|betapply: term * term -> term| \\ - \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix ->|\isasep\isanewline% + \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline% \verb| theory -> term * theory| \\ - \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Binding.T * term ->|\isasep\isanewline% + \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline% \verb| theory -> (term * term) * 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| \\ diff -r bb0f395db245 -r 88ba5e5ac6d8 doc-src/IsarImplementation/Thy/document/prelim.tex --- a/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Jan 20 19:09:19 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Wed Jan 21 16:51:45 2009 +0100 @@ -816,13 +816,13 @@ \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\ \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\ \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\ - \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> Binding.T -> string| \\ + \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\ \end{mldecls} \begin{mldecls} \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\ \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\ \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\ - \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T| \\ + \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\ \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\ \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\ \end{mldecls} diff -r bb0f395db245 -r 88ba5e5ac6d8 doc-src/IsarImplementation/Thy/logic.thy --- a/doc-src/IsarImplementation/Thy/logic.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/logic.thy Wed Jan 21 16:51:45 2009 +0100 @@ -323,9 +323,9 @@ @{index_ML fastype_of: "term -> typ"} \\ @{index_ML lambda: "term -> term -> term"} \\ @{index_ML betapply: "term * term -> term"} \\ - @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix -> + @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix -> theory -> term * theory"} \\ - @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * term -> + @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term -> theory -> (term * term) * theory"} \\ @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\ @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ diff -r bb0f395db245 -r 88ba5e5ac6d8 doc-src/IsarImplementation/Thy/prelim.thy --- a/doc-src/IsarImplementation/Thy/prelim.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/prelim.thy Wed Jan 21 16:51:45 2009 +0100 @@ -707,13 +707,13 @@ @{index_ML_type NameSpace.naming} \\ @{index_ML NameSpace.default_naming: NameSpace.naming} \\ @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\ - @{index_ML NameSpace.full_name: "NameSpace.naming -> Binding.T -> string"} \\ + @{index_ML NameSpace.full_name: "NameSpace.naming -> binding -> string"} \\ \end{mldecls} \begin{mldecls} @{index_ML_type NameSpace.T} \\ @{index_ML NameSpace.empty: NameSpace.T} \\ @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\ - @{index_ML NameSpace.declare: "NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T"} \\ + @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T"} \\ @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\ @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\ \end{mldecls} diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/ATP_Linkup.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ATP_Linkup.thy - ID: $Id$ Author: Lawrence C Paulson Author: Jia Meng, NICTA Author: Fabian Immler, TUM diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Code_Eval.thy --- a/src/HOL/Code_Eval.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Code_Eval.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Code_Eval.thy - ID: $Id$ Author: Florian Haftmann, TU Muenchen *) @@ -24,7 +23,7 @@ code_datatype Const App class term_of = typerep + - fixes term_of :: "'a \ term" + fixes term_of :: "'a::{} \ term" lemma term_of_anything: "term_of x \ t" by (rule eq_reflection) (cases "term_of x", cases t, simp) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Datatype.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Datatype.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Stefan Berghofer and Markus Wenzel, TU Muenchen diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Finite_Set.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Finite_Set.thy - ID: $Id$ Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel with contributions by Jeremy Avigad *) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/FunDef.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/FunDef.thy - ID: $Id$ Author: Alexander Krauss, TU Muenchen *) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Lattices.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Lattices.thy - ID: $Id$ Author: Tobias Nipkow *) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Nominal/nominal_induct.ML Wed Jan 21 16:51:45 2009 +0100 @@ -6,7 +6,7 @@ structure NominalInduct: sig - val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list -> + val nominal_induct_tac: Proof.context -> (binding option * term) option list list -> (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> RuleCases.cases_tactic val nominal_induct_method: Method.src -> Proof.context -> Method.method diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Wed Jan 21 16:51:45 2009 +0100 @@ -9,8 +9,8 @@ signature NOMINAL_PRIMREC = sig val add_primrec: term list option -> term option -> - (Binding.T * typ option * mixfix) list -> - (Binding.T * typ option * mixfix) list -> + (binding * typ option * mixfix) list -> + (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> local_theory -> Proof.state end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Orderings.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Orderings.thy - ID: $Id$ Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson *) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Jan 21 16:51:45 2009 +0100 @@ -390,7 +390,7 @@ (wfrec $ map_types poly_tvars R) $ functional val def_term = mk_const_def thy (x, Ty, wfrec_R_M) - val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy + val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy in (thy', def) end; end; @@ -549,7 +549,7 @@ val ([def0], theory) = thy |> PureThy.add_defs false - [Thm.no_attributes (fid ^ "_def", defn)] + [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)] val def = Thm.freezeT def0; val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def) else () diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Jan 21 16:51:45 2009 +0100 @@ -238,7 +238,7 @@ (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => - ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T, + (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) @@ -262,7 +262,7 @@ in thy2 |> Sign.add_path (space_implode "_" new_type_names) - |> PureThy.add_thmss [(("recs", rec_thms), [])] + |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [])] ||> Sign.parent_path ||> Theory.checkpoint |-> (fn thms => pair (reccomb_names, Library.flat thms)) @@ -316,7 +316,7 @@ fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))); val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T'); val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn); - val def = ((Sign.base_name name) ^ "_def", + val def = (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (list_comb (Const (name, caseT), fns1), list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @ fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) ))); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/datatype_aux.ML Wed Jan 21 16:51:45 2009 +0100 @@ -76,7 +76,7 @@ fun store_thmss_atts label tnames attss thmss = fold_map (fn ((tname, atts), thms) => Sign.add_path tname - #> PureThy.add_thmss [((label, thms), atts)] + #> PureThy.add_thmss [((Binding.name label, thms), atts)] #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss) ##> Theory.checkpoint; @@ -85,7 +85,7 @@ fun store_thms_atts label tnames attss thmss = fold_map (fn ((tname, atts), thms) => Sign.add_path tname - #> PureThy.add_thms [((label, thms), atts)] + #> PureThy.add_thms [((Binding.name label, thms), atts)] #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss) ##> Theory.checkpoint; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/datatype_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -196,13 +196,13 @@ fun add_rules simps case_thms rec_thms inject distinct weak_case_congs cong_att = - PureThy.add_thmss [(("simps", simps), []), - (("", flat case_thms @ + PureThy.add_thmss [((Binding.name "simps", simps), []), + ((Binding.empty, flat case_thms @ flat distinct @ rec_thms), [Simplifier.simp_add]), - (("", rec_thms), [Code.add_default_eqn_attribute]), - (("", flat inject), [iff_add]), - (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]), - (("", weak_case_congs), [cong_att])] + ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]), + ((Binding.empty, flat inject), [iff_add]), + ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]), + ((Binding.empty, weak_case_congs), [cong_att])] #> snd; @@ -213,15 +213,15 @@ val inducts = ProjectRule.projections (ProofContext.init thy) induction; fun named_rules (name, {index, exhaustion, ...}: datatype_info) = - [(("", nth inducts index), [Induct.induct_type name]), - (("", exhaustion), [Induct.cases_type name])]; + [((Binding.empty, nth inducts index), [Induct.induct_type name]), + ((Binding.empty, exhaustion), [Induct.cases_type name])]; fun unnamed_rule i = - (("", nth inducts i), [Thm.kind_internal, Induct.induct_type ""]); + ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]); in thy |> PureThy.add_thms (maps named_rules infos @ map unnamed_rule (length infos upto length inducts - 1)) |> snd - |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd + |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd end; @@ -451,7 +451,7 @@ |> store_thmss "inject" new_type_names inject ||>> store_thmss "distinct" new_type_names distinct ||> Sign.add_path (space_implode "_" new_type_names) - ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])]; + ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])]; val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms) ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~ diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Wed Jan 21 16:51:45 2009 +0100 @@ -130,7 +130,7 @@ val vs = map (fn i => List.nth (pnames, i)) is; val (thm', thy') = thy |> Sign.absolute_path - |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm) + |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm) ||> Sign.restore_naming thy; val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []); @@ -196,7 +196,7 @@ val exh_name = Thm.get_name exhaustion; val (thm', thy') = thy |> Sign.absolute_path - |> PureThy.store_thm (exh_name ^ "_P_correctness", thm) + |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm) ||> Sign.restore_naming thy; val P = Var (("P", 0), rT' --> HOLogic.boolT); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Jan 21 16:51:45 2009 +0100 @@ -242,7 +242,7 @@ val ([def_thm], thy') = thy |> Sign.add_consts_i [(cname', constrT, mx)] - |> (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)]; + |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end; @@ -343,7 +343,7 @@ val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds); val fTs = map fastype_of fs; - val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", + val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Sign.base_name iso_name ^ "_def"), Logic.mk_equals (Const (iso_name, T --> Univ_elT), list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos); val (def_thms, thy') = @@ -631,7 +631,7 @@ val ([dt_induct'], thy7) = thy6 |> Sign.add_path big_name - |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] + |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||> Sign.parent_path ||> Theory.checkpoint; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -9,14 +9,14 @@ signature FUNDEF_PACKAGE = sig - val add_fundef : (Binding.T * string option * mixfix) list + val add_fundef : (binding * string option * mixfix) list -> (Attrib.binding * string) list -> FundefCommon.fundef_config -> bool list -> local_theory -> Proof.state - val add_fundef_i: (Binding.T * typ option * mixfix) list + val add_fundef_i: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> FundefCommon.fundef_config -> bool list diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/function_package/size.ML Wed Jan 21 16:51:45 2009 +0100 @@ -144,7 +144,7 @@ (size_names ~~ recTs1)) |> PureThy.add_defs false (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs))) - (def_names ~~ (size_fns ~~ rec_combs1))) + (map Binding.name def_names ~~ (size_fns ~~ rec_combs1))) ||> TheoryTarget.instantiation (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size]) ||>> fold_map define_overloaded @@ -208,7 +208,7 @@ prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3; val ([size_thms], thy'') = PureThy.add_thmss - [(("size", size_eqns), + [((Binding.name "size", size_eqns), [Simplifier.simp_add, Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy' diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/inductive_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -38,17 +38,17 @@ thm list list * local_theory type inductive_flags val add_inductive_i: - inductive_flags -> ((Binding.T * typ) * mixfix) list -> + inductive_flags -> ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> inductive_result * local_theory val add_inductive: bool -> bool -> - (Binding.T * string option * mixfix) list -> - (Binding.T * string option * mixfix) list -> + (binding * string option * mixfix) list -> + (binding * string option * mixfix) list -> (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list -> bool -> local_theory -> inductive_result * local_theory val add_inductive_global: string -> inductive_flags -> - ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> + ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> thm list -> theory -> inductive_result * theory val arities_of: thm -> (string * int) list val params_of: thm -> term list @@ -63,16 +63,16 @@ sig include BASIC_INDUCTIVE_PACKAGE type add_ind_def - val declare_rules: string -> Binding.T -> bool -> bool -> string list -> - thm list -> Binding.T list -> Attrib.src list list -> (thm * string list) list -> + val declare_rules: string -> binding -> bool -> bool -> string list -> + thm list -> binding list -> Attrib.src list list -> (thm * string list) list -> thm -> local_theory -> thm list * thm list * thm * local_theory val add_ind_def: add_ind_def val gen_add_inductive_i: add_ind_def -> inductive_flags -> - ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> + ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> inductive_result * local_theory val gen_add_inductive: add_ind_def -> bool -> bool -> - (Binding.T * string option * mixfix) list -> - (Binding.T * string option * mixfix) list -> + (binding * string option * mixfix) list -> + (binding * string option * mixfix) list -> (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list -> bool -> local_theory -> inductive_result * local_theory val gen_ind_decl: add_ind_def -> bool -> @@ -720,13 +720,13 @@ in (intrs', elims', induct', ctxt3) end; type inductive_flags = - {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T, + {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding, coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool} type add_ind_def = inductive_flags -> term list -> (Attrib.binding * term) list -> thm list -> - term list -> (Binding.T * mixfix) list -> + term list -> (binding * mixfix) list -> local_theory -> inductive_result * local_theory fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Jan 21 16:51:45 2009 +0100 @@ -391,14 +391,14 @@ REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac, DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); - val (thm', thy') = PureThy.store_thm (space_implode "_" - (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy; + val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_" + (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy; val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) (DatatypeAux.split_conj_thm thm'); val ([thms'], thy'') = PureThy.add_thmss - [((space_implode "_" + [((Binding.name (space_implode "_" (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @ - ["correctness"]), thms), [])] thy'; + ["correctness"])), thms), [])] thy'; val realizers = inducts ~~ thms' ~~ rlzs ~~ rs; in Extraction.add_realizers_i @@ -451,8 +451,8 @@ rewrite_goals_tac rews, REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN' DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); - val (thm', thy') = PureThy.store_thm (space_implode "_" - (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy + val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_" + (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy in Extraction.add_realizers_i [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy' diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/inductive_set_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -12,13 +12,13 @@ val pred_set_conv_att: attribute val add_inductive_i: InductivePackage.inductive_flags -> - ((Binding.T * typ) * mixfix) list -> + ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> InductivePackage.inductive_result * local_theory val add_inductive: bool -> bool -> - (Binding.T * string option * mixfix) list -> - (Binding.T * string option * mixfix) list -> + (binding * string option * mixfix) list -> + (binding * string option * mixfix) list -> (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list -> bool -> local_theory -> InductivePackage.inductive_result * local_theory val codegen_preproc: theory -> thm list -> thm list diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/old_primrec_package.ML --- a/src/HOL/Tools/old_primrec_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/old_primrec_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -305,11 +305,11 @@ end; fun thy_note ((name, atts), thms) = - PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms)); + PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms)); fun thy_def false ((name, atts), t) = - PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)) + PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm)) | thy_def true ((name, atts), t) = - PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)); + PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm)); in diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/primrec_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -7,12 +7,12 @@ signature PRIMREC_PACKAGE = sig - val add_primrec: (Binding.T * typ option * mixfix) list -> + val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> local_theory -> thm list * local_theory - val add_primrec_global: (Binding.T * typ option * mixfix) list -> + val add_primrec_global: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> thm list * theory val add_primrec_overloaded: (string * (string * typ) * bool) list -> - (Binding.T * typ option * mixfix) list -> + (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> thm list * theory end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/recdef_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/recdef_package.ML - ID: $Id$ Author: Markus Wenzel, TU Muenchen Wrapper module for Konrad Slind's TFL package. @@ -16,10 +15,10 @@ val cong_del: attribute val wf_add: attribute val wf_del: attribute - val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list -> + val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list -> Attrib.src option -> theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} - val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list -> + val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list -> theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list -> theory -> theory * {induct_rules: thm} @@ -214,8 +213,8 @@ thy |> Sign.add_path bname |> PureThy.add_thmss - ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) - ||>> PureThy.add_thms [(("induct", induct), [])]; + (((Binding.name "simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) + ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]; val result = {simps = simps', rules = rules', induct = induct', tcs = tcs}; val thy = thy @@ -243,7 +242,7 @@ val ([induct_rules'], thy3) = thy2 |> Sign.add_path bname - |> PureThy.add_thms [(("induct_rules", induct_rules), [])] + |> PureThy.add_thms [((Binding.name "induct_rules", induct_rules), [])] ||> Sign.parent_path; in (thy3, {induct_rules = induct_rules'}) end; @@ -299,7 +298,7 @@ val recdef_decl = Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true -- - P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop) + P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/record_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -1534,8 +1534,10 @@ |> extension_typedef name repT (alphas@[zeta]) ||> Sign.add_consts_i (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls)) - ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs)) - ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs) + ||>> PureThy.add_defs false + (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs)) + ||>> PureThy.add_defs false + (map (Thm.no_attributes o apfst Binding.name) upd_specs) |-> (fn args as ((_, dest_defs), upd_defs) => fold Code.add_default_eqn dest_defs #> fold Code.add_default_eqn upd_defs @@ -1693,14 +1695,14 @@ [dest_convs',upd_convs']), thm_thy) = defs_thy - |> (PureThy.add_thms o map Thm.no_attributes) + |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) [("ext_inject", inject), ("ext_induct", induct), ("ext_cases", cases), ("ext_surjective", surjective), ("ext_split", split_meta)] - ||>> (PureThy.add_thmss o map Thm.no_attributes) - [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)] + ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name)) + [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)] in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs') end; @@ -1938,9 +1940,9 @@ (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn])) |> (Sign.add_consts_i o map Syntax.no_syn) (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) - |> ((PureThy.add_defs false o map Thm.no_attributes) sel_specs) - ||>> ((PureThy.add_defs false o map Thm.no_attributes) upd_specs) - ||>> ((PureThy.add_defs false o map Thm.no_attributes) + |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs) + ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs) + ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) [make_spec, fields_spec, extend_spec, truncate_spec]) |-> (fn defs as ((sel_defs, upd_defs), derived_defs) => fold Code.add_default_eqn sel_defs @@ -2164,17 +2166,17 @@ val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'], [surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) = defs_thy - |> (PureThy.add_thmss o map Thm.no_attributes) + |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name)) [("select_convs", sel_convs_standard), ("update_convs", upd_convs), ("select_defs", sel_defs), ("update_defs", upd_defs), ("splits", [split_meta_standard,split_object,split_ex]), ("defs", derived_defs)] - ||>> (PureThy.add_thms o map Thm.no_attributes) + ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) [("surjective", surjective), ("equality", equality)] - ||>> PureThy.add_thms + ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name) [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)), (("induct", induct), induct_type_global name), (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)), @@ -2186,8 +2188,8 @@ val final_thy = thms_thy |> (snd oo PureThy.add_thmss) - [(("simps", sel_upd_simps), [Simplifier.simp_add]), - (("iffs",iffs), [iff_add])] + [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]), + ((Binding.name "iffs", iffs), [iff_add])] |> put_record name (make_record_info args parent fields extension induct_scheme') |> put_sel_upd (names @ [full_moreN]) sel_upd_simps |> add_record_equalities extension_id equality' diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/res_axioms.ML Wed Jan 21 16:51:45 2009 +0100 @@ -84,7 +84,7 @@ val (c, thy') = Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy val cdef = cname ^ "_def" - val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy' + val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy' val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef) in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx = diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/specification_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -28,7 +28,7 @@ else thname val def_eq = Logic.mk_equals (Const(cname_full,ctype), HOLogic.choice_const ctype $ P) - val (thms, thy') = PureThy.add_defs covld [((cdefname,def_eq),[])] thy + val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy val thm' = [thm,hd thms] MRS @{thm exE_some} in mk_definitional cos (thy',thm') @@ -39,7 +39,7 @@ let fun process [] (thy,tm) = let - val (thms, thy') = PureThy.add_axioms [((axname,HOLogic.mk_Trueprop tm),[])] thy + val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy in (thy',hd thms) end @@ -184,7 +184,7 @@ if name = "" then arg |> Library.swap else (writeln (" " ^ name ^ ": " ^ (Display.string_of_thm thm)); - PureThy.store_thm (name, thm) thy) + PureThy.store_thm (Binding.name name, thm) thy) in args |> apsnd (remove_alls frees) |> apsnd undo_imps diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Tools/typedef_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -112,7 +112,8 @@ if def then theory |> Sign.add_consts_i [(name, setT', NoSyn)] - |> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))] + |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name) + (PrimitiveDefs.mk_defpair (setC, set)))] |-> (fn [th] => pair (SOME th)) else (NONE, theory); fun contract_def NONE th = th @@ -130,7 +131,7 @@ (Abs_name, oldT --> newT, NoSyn)] #> add_def #-> (fn set_def => - PureThy.add_axioms [((typedef_name, typedef_prop), + PureThy.add_axioms [((Binding.name 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 @@ -143,7 +144,7 @@ thy1 |> Sign.add_path name |> PureThy.add_thms - ([((Rep_name, make @{thm type_definition.Rep}), []), + ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []), ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []), ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []), ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []), diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Typerep.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ -(* Title: HOL/Library/RType.thy - ID: $Id$ +(* Title: HOL/Typerep.thy Author: Florian Haftmann, TU Muenchen *) @@ -15,9 +14,7 @@ fixes typerep :: "'a\{} itself \ typerep" begin -definition - typerep_of :: "'a \ typerep" -where +definition typerep_of :: "'a \ typerep" where [simp]: "typerep_of x = typerep TYPE('a)" end diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/Wellfounded.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ -(* ID: $Id$ - Author: Tobias Nipkow +(* Author: Tobias Nipkow Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Konrad Slind, Alexander Krauss Copyright 1992-2008 University of Cambridge and TU Muenchen diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOL/ex/Quickcheck.thy --- a/src/HOL/ex/Quickcheck.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOL/ex/Quickcheck.thy Wed Jan 21 16:51:45 2009 +0100 @@ -200,7 +200,7 @@ in lthy |> LocalTheory.theory (Code.del_eqns c - #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal]) + #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal]) #-> Code.add_eqn) end; in diff -r bb0f395db245 -r 88ba5e5ac6d8 src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/HOLCF/Tools/fixrec_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -9,9 +9,9 @@ val legacy_infer_term: theory -> term -> term val legacy_infer_prop: theory -> term -> term val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory - val add_fixrec_i: bool -> ((Binding.T * attribute list) * term) list list -> theory -> theory + val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory val add_fixpat: Attrib.binding * string list -> theory -> theory - val add_fixpat_i: (Binding.T * attribute list) * term list -> theory -> theory + val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory end; structure FixrecPackage: FIXREC_PACKAGE = diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/General/binding.ML Wed Jan 21 16:51:45 2009 +0100 @@ -6,6 +6,7 @@ signature BASIC_BINDING = sig + type binding val long_names: bool ref val short_names: bool ref val unique_names: bool ref @@ -92,6 +93,8 @@ else space_implode "." (map mk_prefix prefix) ^ ":" ^ name end; +type binding = T; + end; structure Basic_Binding : BASIC_BINDING = Binding; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/General/name_space.ML Wed Jan 21 16:51:45 2009 +0100 @@ -3,9 +3,10 @@ Generic name spaces with declared and hidden entries. Unknown names are considered global; no support for absolute addressing. +Cf. Pure/General/binding.ML *) -type bstring = string; (*names to be bound*) +type bstring = string; (*simple names to be bound -- legacy*) type xstring = string; (*external names*) signature NAME_SPACE = @@ -31,8 +32,8 @@ val merge: T * T -> T type naming val default_naming: naming - val declare: naming -> Binding.T -> T -> string * T - val full_name: naming -> Binding.T -> string + val declare: naming -> binding -> T -> string * T + val full_name: naming -> binding -> string val external_names: naming -> string -> string list val path_of: naming -> string val add_path: string -> naming -> naming @@ -41,7 +42,7 @@ val sticky_prefix: string -> naming -> naming type 'a table = T * 'a Symtab.table val empty_table: 'a table - val bind: naming -> Binding.T * 'a + val bind: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*) val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table val join_tables: (string -> 'a * 'a -> 'a) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/IsaMakefile Wed Jan 21 16:51:45 2009 +0100 @@ -41,7 +41,7 @@ Isar/expression.ML Isar/find_theorems.ML Isar/isar.ML \ Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML \ Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \ - Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/old_locale.ML \ + Isar/locale.ML Isar/method.ML Isar/net_rules.ML \ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \ Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \ Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \ @@ -75,7 +75,7 @@ Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \ Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \ Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML \ - Thy/thy_syntax.ML Tools/ROOT.ML Tools/invoke.ML \ + Thy/thy_syntax.ML Tools/ROOT.ML \ Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \ assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \ consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \ diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/ROOT.ML Wed Jan 21 16:51:45 2009 +0100 @@ -53,7 +53,6 @@ (*local theories and targets*) use "local_theory.ML"; use "overloading.ML"; -use "old_locale.ML"; use "locale.ML"; use "class_target.ML"; use "theory_target.ML"; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/args.ML Wed Jan 21 16:51:45 2009 +0100 @@ -35,7 +35,7 @@ val name_source: T list -> string * T list val name_source_position: T list -> (SymbolPos.text * Position.T) * T list val name: T list -> string * T list - val binding: T list -> Binding.T * T list + val binding: T list -> binding * T list val alt_name: T list -> string * T list val symbol: T list -> string * T list val liberal_name: T list -> string * T list @@ -66,8 +66,8 @@ val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list val attribs: (string -> string) -> T list -> src list * T list val opt_attribs: (string -> string) -> T list -> src list * T list - val thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list - val opt_thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list + val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list + val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) -> src -> Proof.context -> 'a * Proof.context diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/attrib.ML Wed Jan 21 16:51:45 2009 +0100 @@ -7,7 +7,7 @@ signature ATTRIB = sig type src = Args.src - type binding = Binding.T * src list + type binding = binding * src list val empty_binding: binding val print_attributes: theory -> unit val intern: theory -> xstring -> string @@ -54,7 +54,7 @@ type src = Args.src; -type binding = Binding.T * src list; +type binding = binding * src list; val empty_binding: binding = (Binding.empty, []); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/calculation.ML Wed Jan 21 16:51:45 2009 +0100 @@ -98,8 +98,8 @@ ("sym", sym_att, "declaration of symmetry rule"), ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #> PureThy.add_thms - [(("", transitive_thm), [trans_add]), - (("", symmetric_thm), [sym_add])] #> snd)); + [((Binding.empty, transitive_thm), [trans_add]), + ((Binding.empty, symmetric_thm), [sym_add])] #> snd)); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/class.ML Wed Jan 21 16:51:45 2009 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/Isar/ML Author: Florian Haftmann, TU Muenchen -Type classes derived from primitive axclasses and locales - interfaces +Type classes derived from primitive axclasses and locales - interfaces. *) signature CLASS = @@ -34,7 +34,7 @@ (* instantiation of canonical interpretation *) (*FIXME inst_morph should be calculated manually and not instantiate constraint*) - val aT = TFree ("'a", base_sort); + val aT = TFree (Name.aT, base_sort); val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt |> Expression.cert_goal_expression ([(class, (("", false), Expression.Named ((map o apsnd) Const param_map)))], []); @@ -89,7 +89,88 @@ in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end; -fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems = +fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt => + let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end)); + +fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) => + if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort) + else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi) + (*FIXME does not occur*) + | T as TFree (v, sort) => + if v = Name.aT then T + else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")); + +val singleton_fixate = (map o map_atyps) (fn TVar (vi, sort) + => TFree (Name.aT, sort) | T => T); + +fun add_tfrees_of_element (Element.Fixes fxs) = fold (fn (_, SOME T, _) => Term.add_tfreesT T + | _ => I) fxs + | add_tfrees_of_element (Element.Constrains cnstrs) = fold (Term.add_tfreesT o snd) cnstrs + | add_tfrees_of_element (Element.Assumes assms) = fold (fold (fn (t, ts) => + Term.add_tfrees t #> fold Term.add_tfrees ts) o snd) assms + | add_tfrees_of_element _ = I; + +fun fork_syn (Element.Fixes xs) = + fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs + #>> Element.Fixes + | fork_syn x = pair x; + +fun prep_class_spec prep_class prep_decl thy raw_supclasses raw_elems = + let + (* prepare import *) + val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); + val (sups, others_basesort) = map (prep_class thy) raw_supclasses + |> Sign.minimize_sort thy + |> List.partition (is_class thy); + + val supparams = (map o apsnd) (snd o snd) (these_params thy sups); + val supparam_names = map fst supparams; + val _ = if has_duplicates (op =) supparam_names + then error ("Duplicate parameter(s) in superclasses: " + ^ (commas o map quote o duplicates (op =)) supparam_names) + else (); + val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional []))) + sups, []); + val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort; + + (* infer types and base sort *) + val base_constraints = (map o apsnd) + (map_type_tfree (K (TVar ((Name.aT, 0), given_basesort))) o fst o snd) + (these_operations thy sups); + val ((_, _, inferred_elems), _) = ProofContext.init thy + |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints + |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort)) + |> add_typ_check ~2 "singleton_fixate" singleton_fixate + |> prep_decl supexpr raw_elems; + (*FIXME propagation of given base sort into class spec broken*) + (*FIXME check for *all* side conditions here, extra check function for elements, + less side-condition checks in check phase*) + val base_sort = if null inferred_elems then given_basesort else + case fold add_tfrees_of_element inferred_elems [] + of [] => error "No type variable in class specification" + | [(_, sort)] => sort + | _ => error "Multiple type variables in class specification" + val sup_sort = inter_sort base_sort sups + + (* process elements as class specification *) + val begin_ctxt = begin sups base_sort + #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps) + (K (TFree (Name.aT, base_sort))) supparams) + (*FIXME should constraints be issued in begin?*) + val ((_, _, syntax_elems), _) = ProofContext.init thy + |> begin_ctxt + |> Expression.cert_declaration supexpr inferred_elems; + val (elems, global_syntax) = fold_map fork_syn syntax_elems []; + val constrain = Element.Constrains ((map o apsnd o map_atyps) + (K (TFree (Name.aT, base_sort))) supparams); + (*FIXME 2009 perhaps better: control type variable by explicit + parameter instantiation of import expression*) + in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end; + +val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration; +val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration; + +(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems = let (*FIXME 2009 simplify*) val supclasses = map (prep_class thy) raw_supclasses; @@ -126,7 +207,7 @@ in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end; val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration; -val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration; +val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*) fun add_consts bname class base_sort sups supparams global_syntax thy = let @@ -235,19 +316,13 @@ #> ProofContext.theory_of #> TheoryTarget.init (SOME sub); in do_proof after_qed some_prop goal_ctxt end; -fun user_proof after_qed NONE = - Proof.theorem_i NONE (K (after_qed NONE)) [[]] - #> Element.refine_witness #> Seq.hd - | user_proof after_qed (SOME prop) = - Proof.theorem_i NONE (after_qed o SOME o Element.make_witness prop - o Thm.close_derivation o the_single o the_single) - [[(Element.mark_witness prop, [])]] - #> Element.refine_witness #> Seq.hd; +fun user_proof after_qed some_prop = + Element.witness_proof (after_qed o try the_single o the_single) + [the_list some_prop]; -fun tactic_proof tac after_qed NONE ctxt = - after_qed NONE ctxt - | tactic_proof tac after_qed (SOME prop) ctxt = - after_qed (SOME (Element.prove_witness ctxt prop tac)) ctxt; +fun tactic_proof tac after_qed some_prop ctxt = + after_qed (Option.map + (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt; in diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Wed Jan 21 16:51:45 2009 +0100 @@ -18,6 +18,7 @@ val rules: theory -> class -> thm option * thm val these_params: theory -> sort -> (string * (class * (string * typ))) list val these_defs: theory -> sort -> thm list + val these_operations: theory -> sort -> (string * (class * (typ * term))) list val print_classes: theory -> unit val begin: class list -> sort -> Proof.context -> Proof.context @@ -253,7 +254,6 @@ in fold amend (heritage thy [class]) thy end; fun register_operation class (c, (t, some_def)) thy = - (*FIXME 2009 does this still also work for abbrevs?*) let val base_sort = base_sort thy class; val prep_typ = map_type_tfree @@ -297,11 +297,14 @@ (* class context syntax *) -fun synchronize_class_syntax sups base_sort ctxt = +fun these_unchecks thy = + map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy; + +fun synchronize_class_syntax sort base_sort ctxt = let val thy = ProofContext.theory_of ctxt; val algebra = Sign.classes_of thy; - val operations = these_operations thy sups; + val operations = these_operations thy sort; fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); val primary_constraints = (map o apsnd) (subst_class_typ base_sort o fst o snd) operations; @@ -322,7 +325,7 @@ | NONE => NONE) | NONE => NONE) fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c); - val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations; + val unchecks = these_unchecks thy sort; in ctxt |> fold declare_const primary_constraints @@ -337,11 +340,11 @@ val base_sort = base_sort thy class; in synchronize_class_syntax [class] base_sort ctxt end; -fun begin sups base_sort ctxt = +fun begin sort base_sort ctxt = ctxt |> Variable.declare_term (Logic.mk_type (TFree (Name.aT, base_sort))) - |> synchronize_class_syntax sups base_sort + |> synchronize_class_syntax sort base_sort |> Overloading.add_improvable_syntax; fun init class thy = @@ -356,52 +359,42 @@ fun declare class pos ((c, mx), dict) thy = let - val prfx = class_prefix class; - val thy' = thy |> Sign.add_path prfx; - (*FIXME 2009 use proper name morphism*) - val morph = morphism thy' class; - val params = map (apsnd fst o snd) (these_params thy' [class]); - - val c' = Sign.full_bname thy' c; + val morph = morphism thy class; + val b = Morphism.binding morph (Binding.name c); + val b_def = Morphism.binding morph (Binding.name (c ^ "_dict")); + val c' = Sign.full_name thy b; val dict' = Morphism.term morph dict; val ty' = Term.fastype_of dict'; - val ty'' = Type.strip_sorts ty'; - (*FIXME 2009 the tinkering with theorems here is a mess*) - val def_eq = Logic.mk_equals (Const (c', ty'), dict'); - fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy); + val def_eq = Logic.mk_equals (Const (c', ty'), dict') + |> map_types Type.strip_sorts; in - thy' - |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd - |> Thm.add_def false false (c, def_eq) (*FIXME 2009 name of theorem*) - (*FIXME 2009 add_def should accept binding*) - |>> Thm.symmetric - ||>> get_axiom - |-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def'))) - #> PureThy.store_thm (c ^ "_raw", def') (*FIXME 2009 name of theorem*) - (*FIXME 2009 store_thm etc. should accept binding*) - #> snd) - |> Sign.restore_naming thy + thy + |> Sign.declare_const pos ((b, Type.strip_sorts ty'), mx) + |> snd + |> Thm.add_def false false (b_def, def_eq) + |>> Thm.varifyT + |-> (fn def_thm => PureThy.store_thm (b_def, def_thm) + #> snd + #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) |> Sign.add_const_constraint (c', SOME ty') end; fun abbrev class prmode pos ((c, mx), rhs) thy = let - val prfx = class_prefix class; - val thy' = thy |> Sign.add_path prfx; - - val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) - (these_operations thy [class]); - val c' = Sign.full_bname thy' c; + val morph = morphism thy class; + val unchecks = these_unchecks thy [class]; + val b = Morphism.binding morph (Binding.name c); + val c' = Sign.full_name thy b; val rhs' = Pattern.rewrite_term thy unchecks [] rhs; - val rhs'' = map_types Logic.varifyT rhs'; val ty' = Term.fastype_of rhs'; + val rhs'' = map_types ((*Type.strip_sorts o *)Logic.varifyT) rhs'; in - thy' - |> Sign.add_abbrev (#1 prmode) pos (Binding.name c, map_types Type.strip_sorts rhs'') |> snd + thy + |> Sign.add_abbrev (#1 prmode) pos (b, rhs'') + |> snd |> Sign.add_const_constraint (c', SOME ty') |> Sign.notation true prmode [(Const (c', ty'), mx)] |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE)) - |> Sign.restore_naming thy end; @@ -610,8 +603,7 @@ end; fun default_intro_tac ctxt [] = - intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE - Locale.intro_locales_tac true ctxt [] + intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] | default_intro_tac _ _ = no_tac; fun default_tac rules ctxt facts = diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/constdefs.ML Wed Jan 21 16:51:45 2009 +0100 @@ -8,12 +8,12 @@ signature CONSTDEFS = sig - val add_constdefs: (Binding.T * string option) list * - ((Binding.T * string option * mixfix) option * + val add_constdefs: (binding * string option) list * + ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory - val add_constdefs_i: (Binding.T * typ option) list * - ((Binding.T * typ option * mixfix) option * - ((Binding.T * attribute list) * term)) list -> theory -> theory + val add_constdefs_i: (binding * typ option) list * + ((binding * typ option * mixfix) option * + ((binding * attribute list) * term)) list -> theory -> theory end; structure Constdefs: CONSTDEFS = @@ -52,7 +52,7 @@ val thy' = thy |> Sign.add_consts_i [(c, T, mx)] - |> PureThy.add_defs false [((name, def), atts)] + |> PureThy.add_defs false [((Binding.name name, def), atts)] |-> (fn [thm] => Code.add_default_eqn thm); in ((c, T), thy') end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/context_rules.ML Wed Jan 21 16:51:45 2009 +0100 @@ -199,7 +199,7 @@ val dest_query = rule_add elim_queryK Tactic.make_elim; val _ = Context.>> (Context.map_theory - (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])])); + (snd o PureThy.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])])); (* concrete syntax *) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/element.ML Wed Jan 21 16:51:45 2009 +0100 @@ -9,11 +9,11 @@ sig datatype ('typ, 'term) stmt = Shows of (Attrib.binding * ('term * 'term list) list) list | - Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list + Obtains of (binding * ((binding * 'typ option) list * 'term list)) list type statement = (string, string) stmt type statement_i = (typ, term) stmt datatype ('typ, 'term, 'fact) ctxt = - Fixes of (Binding.T * 'typ option * mixfix) list | + Fixes of (binding * 'typ option * mixfix) list | Constrains of (string * 'typ) list | Assumes of (Attrib.binding * ('term * 'term list) list) list | Defines of (Attrib.binding * ('term * 'term list)) list | @@ -23,12 +23,12 @@ val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) -> (Attrib.binding * ('fact * Attrib.src list) list) list -> (Attrib.binding * ('c * Attrib.src list) list) list - val map_ctxt': {binding: Binding.T -> Binding.T, - var: Binding.T * mixfix -> Binding.T * mixfix, + val map_ctxt': {binding: binding -> binding, + var: binding * mixfix -> binding * mixfix, typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt - val map_ctxt: {binding: Binding.T -> Binding.T, - var: Binding.T * mixfix -> Binding.T * mixfix, + val map_ctxt: {binding: binding -> binding, + var: binding * mixfix -> binding * mixfix, typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt val map_ctxt_attrib: (Attrib.src -> Attrib.src) -> @@ -41,25 +41,21 @@ val pretty_ctxt: Proof.context -> context_i -> Pretty.T list val pretty_statement: Proof.context -> string -> thm -> Pretty.T type witness - val map_witness: (term * thm -> term * thm) -> witness -> witness + val prove_witness: Proof.context -> term -> tactic -> witness + val witness_proof: (witness list list -> Proof.context -> Proof.context) -> + term list list -> Proof.context -> Proof.state + val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) -> + term list list -> term list -> Proof.context -> Proof.state + val witness_local_proof: (witness list list -> Proof.state -> Proof.state) -> + string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state val morph_witness: morphism -> witness -> witness - val witness_prop: witness -> term - val witness_hyps: witness -> term list - val assume_witness: theory -> term -> witness - val prove_witness: Proof.context -> term -> tactic -> witness - val close_witness: witness -> witness val conclude_witness: witness -> thm - val mark_witness: term -> term - val make_witness: term -> thm -> witness - val dest_witness: witness -> term * thm - val transfer_witness: theory -> witness -> witness - val refine_witness: Proof.state -> Proof.state Seq.seq val pretty_witness: Proof.context -> witness -> Pretty.T val rename: (string * (string * mixfix option)) list -> string -> string val rename_var_name: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix val rename_var: (string * (string * mixfix option)) list -> - Binding.T * mixfix -> Binding.T * mixfix + binding * mixfix -> binding * mixfix val rename_term: (string * (string * mixfix option)) list -> term -> term val rename_thm: (string * (string * mixfix option)) list -> thm -> thm val rename_morphism: (string * (string * mixfix option)) list -> morphism @@ -93,7 +89,7 @@ datatype ('typ, 'term) stmt = Shows of (Attrib.binding * ('term * 'term list) list) list | - Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list; + Obtains of (binding * ((binding * 'typ option) list * 'term list)) list; type statement = (string, string) stmt; type statement_i = (typ, term) stmt; @@ -102,7 +98,7 @@ (* context *) datatype ('typ, 'term, 'fact) ctxt = - Fixes of (Binding.T * 'typ option * mixfix) list | + Fixes of (binding * 'typ option * mixfix) list | Constrains of (string * 'typ) list | Assumes of (Attrib.binding * ('term * 'term list) list) list | Defines of (Attrib.binding * ('term * 'term list)) list | @@ -300,24 +296,51 @@ datatype witness = Witness of term * thm; +val mark_witness = Logic.protect; +fun witness_prop (Witness (t, _)) = t; +fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th); fun map_witness f (Witness witn) = Witness (f witn); fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th)); -fun witness_prop (Witness (t, _)) = t; -fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th); - -fun assume_witness thy t = - Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t))); - fun prove_witness ctxt t tac = - Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (Logic.protect t) (fn _ => + Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ => Tactic.rtac Drule.protectI 1 THEN tac))); -val close_witness = map_witness (fn (t, th) => (t, Thm.close_derivation th)); +local + +val refine_witness = + Proof.refine (Method.Basic (K (Method.RAW_METHOD + (K (ALLGOALS + (CONJUNCTS (ALLGOALS + (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); -fun conclude_witness (Witness (_, th)) = - Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th)); +fun gen_witness_proof proof after_qed wit_propss eq_props = + let + val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss + @ [map (rpair []) eq_props]; + fun after_qed' thmss = + let + val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss); + in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; + in proof after_qed' propss #> refine_witness #> Seq.hd end; + +in + +fun witness_proof after_qed wit_propss = + gen_witness_proof (Proof.theorem_i NONE) (fn wits => fn _ => after_qed wits) + wit_propss []; + +val witness_proof_eqs = gen_witness_proof (Proof.theorem_i NONE); + +fun witness_local_proof after_qed cmd wit_propss goal_ctxt int = + gen_witness_proof (fn after_qed' => fn propss => + Proof.map_context (K goal_ctxt) + #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i + cmd NONE after_qed' (map (pair (Binding.empty, [])) propss)) + (fn wits => fn _ => after_qed wits) wit_propss []; + +end; (*local*) fun compose_witness (Witness (_, th)) r = let @@ -330,18 +353,8 @@ (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th')) end; -val mark_witness = Logic.protect; - -fun make_witness t th = Witness (t, th); -fun dest_witness (Witness w) = w; - -fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th); - -val refine_witness = - Proof.refine (Method.Basic (K (Method.RAW_METHOD - (K (ALLGOALS - (CONJUNCTS (ALLGOALS - (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); +fun conclude_witness (Witness (_, th)) = + Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th)); fun pretty_witness ctxt witn = let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/expression.ML Wed Jan 21 16:51:45 2009 +0100 @@ -9,8 +9,8 @@ (* Locale expressions *) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list type 'term expr = (string * ((string * bool) * 'term map)) list - type expression_i = term expr * (Binding.T * typ option * mixfix) list - type expression = string expr * (Binding.T * string option * mixfix) list + type expression_i = term expr * (binding * typ option * mixfix) list + type expression = string expr * (binding * string option * mixfix) list (* Processing of context statements *) val cert_statement: Element.context_i list -> (term * term list) list list -> @@ -20,14 +20,14 @@ (* Declaring locales *) val cert_declaration: expression_i -> Element.context_i list -> Proof.context -> - ((Binding.T * typ option * mixfix) list * (string * morphism) list + ((binding * typ option * mixfix) list * (string * morphism) list * Element.context_i list) * ((string * typ) list * Proof.context) val cert_read_declaration: expression_i -> Element.context list -> Proof.context -> - ((Binding.T * typ option * mixfix) list * (string * morphism) list + ((binding * typ option * mixfix) list * (string * morphism) list * Element.context_i list) * ((string * typ) list * Proof.context) (*FIXME*) val read_declaration: expression -> Element.context list -> Proof.context -> - ((Binding.T * typ option * mixfix) list * (string * morphism) list + ((binding * typ option * mixfix) list * (string * morphism) list * Element.context_i list) * ((string * typ) list * Proof.context) val add_locale: bstring -> bstring -> expression_i -> Element.context_i list -> theory -> string * local_theory @@ -64,8 +64,8 @@ type 'term expr = (string * ((string * bool) * 'term map)) list; -type expression = string expr * (Binding.T * string option * mixfix) list; -type expression_i = term expr * (Binding.T * typ option * mixfix) list; +type expression = string expr * (binding * string option * mixfix) list; +type expression_i = term expr * (binding * typ option * mixfix) list; (** Internalise locale names in expr **) @@ -640,7 +640,7 @@ |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd |> PureThy.add_defs false - [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])]; + [((Binding.name (Thm.def_name bname), Logic.mk_equals (head, body)), [Thm.kind_internal])]; val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; val cert = Thm.cterm_of defs_thy; @@ -786,41 +786,23 @@ (*** Interpretation ***) -(** Witnesses and goals **) - -fun prep_propp propss = propss |> map (map (rpair [] o Element.mark_witness)); - -val prep_result = map2 (fn props => fn thms => - map2 Element.make_witness props (map Thm.close_derivation thms)); - - (** Interpretation between locales: declaring sublocale relationships **) local -fun gen_sublocale prep_expr intern - raw_target expression thy = +fun gen_sublocale prep_expr intern raw_target expression thy = let val target = intern thy raw_target; val target_ctxt = Locale.init target thy; val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt; - fun store_dep (name, morph) thms = - Locale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export); - - fun after_qed results = - ProofContext.theory ( - (* store dependencies *) - fold2 store_dep deps (prep_result propss results) #> - (* propagate registrations *) - (fn thy => fold_rev Locale.activate_global_facts + fun after_qed witss = ProofContext.theory ( + fold2 (fn (name, morph) => fn wits => Locale.add_dependency target + (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #> + (fn thy => fold_rev Locale.activate_global_facts (Locale.get_registrations thy) thy)); - in - goal_ctxt |> - Proof.theorem_i NONE after_qed (prep_propp propss) |> - Element.refine_witness |> Seq.hd - end; + in Element.witness_proof after_qed propss goal_ctxt end; in @@ -845,10 +827,10 @@ val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; - fun store_reg ((name, morph), thms) thy = + fun store_reg ((name, morph), wits) thy = let - val thms' = map (Element.morph_witness export') thms; - val morph' = morph $> Element.satisfy_morphism thms'; + val wits' = map (Element.morph_witness export') wits; + val morph' = morph $> Element.satisfy_morphism wits'; in thy |> Locale.add_registration (name, (morph', export)) @@ -859,35 +841,26 @@ thy |> fold (fn (name, morph) => Locale.activate_global_facts (name, morph $> export)) regs - | store_eqns_activate regs thms thy = + | store_eqns_activate regs eqs thy = let - val thms' = thms |> map (Element.conclude_witness #> - Morphism.thm (export' $> export) #> + val eqs' = eqs |> map (Morphism.thm (export' $> export) #> LocalDefs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def); - val eq_morph = Element.eq_morphism thy thms'; + val eq_morph = Element.eq_morphism thy eqs'; val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns; in thy |> fold (fn (name, morph) => Locale.amend_registration eq_morph (name, morph) #> Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs - |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn th => [([th], [])]) thms') + |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs') |> snd end; - fun after_qed results = - let - val (wits_reg, wits_eq) = split_last (prep_result (propss @ [eqns]) results); - in ProofContext.theory (fold_map store_reg (regs ~~ wits_reg) - #-> (fn regs => store_eqns_activate regs wits_eq)) - end; + fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits) + #-> (fn regs => store_eqns_activate regs eqs)); - in - goal_ctxt |> - Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |> - Element.refine_witness |> Seq.hd - end; + in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end; in @@ -910,20 +883,16 @@ val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt; - fun store_reg ((name, morph), thms) = + fun store_reg (name, morph) thms = let val morph' = morph $> Element.satisfy_morphism thms $> export; - in - Locale.activate_local_facts (name, morph') - end; + in Locale.activate_local_facts (name, morph') end; - fun after_qed results = - Proof.map_context (fold store_reg (regs ~~ prep_result propss results)); + fun after_qed wits = + Proof.map_context (fold2 store_reg regs wits); in - state |> Proof.map_context (K goal_ctxt) |> - Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i - "interpret" NONE after_qed (map (pair (Binding.empty, [])) (prep_propp propss)) |> - Element.refine_witness |> Seq.hd + state + |> Element.witness_local_proof after_qed "interpret" propss goal_ctxt int end; in diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Wed Jan 21 16:51:45 2009 +0100 @@ -13,8 +13,8 @@ val typed_print_translation: bool * (string * Position.T) -> theory -> theory val print_ast_translation: bool * (string * Position.T) -> theory -> theory val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory - val add_axioms: ((Binding.T * string) * Attrib.src list) list -> theory -> theory - val add_defs: (bool * bool) * ((Binding.T * string) * Attrib.src list) list -> theory -> theory + val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory + val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory val declaration: string * Position.T -> local_theory -> local_theory val simproc_setup: string -> string list -> string * Position.T -> string list -> local_theory -> local_theory @@ -53,7 +53,6 @@ val print_theorems: Toplevel.transition -> Toplevel.transition val print_locales: Toplevel.transition -> Toplevel.transition val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition - val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition val print_attributes: Toplevel.transition -> Toplevel.transition val print_simpset: Toplevel.transition -> Toplevel.transition val print_rules: Toplevel.transition -> Toplevel.transition @@ -359,12 +358,6 @@ Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) show_facts name); -fun print_registrations show_wits name = Toplevel.unknown_context o - Toplevel.keep (Toplevel.node_case - (Context.cases (Old_Locale.print_registrations show_wits name o ProofContext.init) - (Old_Locale.print_registrations show_wits name)) - (Old_Locale.print_registrations show_wits name o Proof.context_of)); - val print_attributes = Toplevel.unknown_theory o Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Jan 21 16:51:45 2009 +0100 @@ -418,45 +418,6 @@ >> (fn expr => Toplevel.print o Toplevel.proof' (fn int => Expression.interpret_cmd expr int))); -local - -val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty; - -in - -val locale_val = - SpecParse.locale_expr -- - Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || - Scan.repeat1 SpecParse.context_element >> pair Old_Locale.empty; - -val _ = - OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl - (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Old_Locale.empty, []) -- P.opt_begin - >> (fn ((name, (expr, elems)), begin) => - (begin ? Toplevel.print) o Toplevel.begin_local_theory begin - (Old_Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin))); - -val _ = - OuterSyntax.command "class_interpretation" - "prove and register interpretation of locale expression in theory or locale" K.thy_goal - (P.xname --| (P.$$$ "\\" || P.$$$ "<") -- P.!!! SpecParse.locale_expr - >> (Toplevel.print oo (Toplevel.theory_to_proof o Old_Locale.interpretation_in_locale I)) || - opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts - >> (fn ((name, expr), insts) => Toplevel.print o - Toplevel.theory_to_proof - (Old_Locale.interpretation_cmd (Binding.base_name name) expr insts))); - -val _ = - OuterSyntax.command "class_interpret" - "prove and register interpretation of locale expression in proof context" - (K.tag_proof K.prf_goal) - (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts - >> (fn ((name, expr), insts) => Toplevel.print o - Toplevel.proof' - (fn int => Old_Locale.interpret_cmd (Binding.base_name name) expr insts int))); - -end; - (* classes *) @@ -857,12 +818,6 @@ (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale)); val _ = - OuterSyntax.improper_command "print_interps" - "print interpretations of named locale" K.diag - (Scan.optional (P.$$$ "!" >> K true) false -- P.xname - >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations)); - -val _ = OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/local_defs.ML Wed Jan 21 16:51:45 2009 +0100 @@ -11,10 +11,10 @@ val mk_def: Proof.context -> (string * term) list -> term list val expand: cterm list -> thm -> thm val def_export: Assumption.export - val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list -> + val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list -> Proof.context -> (term * (string * thm)) list * Proof.context - val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context - val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context -> + val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context + val fixed_abbrev: (binding * mixfix) * term -> Proof.context -> (term * term) * Proof.context val export: Proof.context -> Proof.context -> thm -> thm list * thm val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/local_theory.ML Wed Jan 21 16:51:45 2009 +0100 @@ -18,16 +18,16 @@ val raw_theory: (theory -> theory) -> local_theory -> local_theory val checkpoint: local_theory -> local_theory val full_naming: local_theory -> NameSpace.naming - val full_name: local_theory -> Binding.T -> string + val full_name: local_theory -> binding -> string val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val theory: (theory -> theory) -> local_theory -> local_theory val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory val target: (Proof.context -> Proof.context) -> local_theory -> local_theory val affirm: local_theory -> local_theory val pretty: local_theory -> Pretty.T list - val abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory -> + val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory - val define: string -> (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory -> + val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> @@ -55,10 +55,10 @@ type operations = {pretty: local_theory -> Pretty.T list, - abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory -> + abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory, define: string -> - (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory -> + (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory, notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/locale.ML Wed Jan 21 16:51:45 2009 +0100 @@ -29,23 +29,18 @@ signature LOCALE = sig - type locale - + (* Locale specification *) val register_locale: bstring -> - (string * sort) list * (Binding.T * typ option * mixfix) list -> + (string * sort) list * (binding * typ option * mixfix) list -> term option * term list -> thm option * thm option -> thm list -> (declaration * stamp) list * (declaration * stamp) list -> ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list -> ((string * morphism) * stamp) list -> theory -> theory - - (* Locale name space *) val intern: theory -> xstring -> string val extern: theory -> string -> xstring - - (* Specification *) val defined: theory -> string -> bool - val params_of: theory -> string -> (Binding.T * typ option * mixfix) list + val params_of: theory -> string -> (binding * typ option * mixfix) list val intros_of: theory -> string -> thm option * thm option val axioms_of: theory -> string -> thm list val instance_of: theory -> string -> morphism -> term list @@ -112,13 +107,25 @@ datatype ctxt = datatype Element.ctxt; +fun global_note_qualified kind facts thy = (*FIXME*) + thy + |> Sign.qualified_names + |> PureThy.note_thmss kind facts + ||> Sign.restore_naming thy; + +fun local_note_qualified kind facts ctxt = (*FIXME*) + ctxt + |> ProofContext.qualified_names + |> ProofContext.note_thmss_i kind facts + ||> ProofContext.restore_naming ctxt; + (*** Theory data ***) datatype locale = Loc of { (** static part **) - parameters: (string * sort) list * (Binding.T * typ option * mixfix) list, + parameters: (string * sort) list * (binding * typ option * mixfix) list, (* type and term parameters *) spec: term option * term list, (* assumptions (as a single predicate expression) and defines *) @@ -330,7 +337,7 @@ fun init_global_elem (Notes (kind, facts)) thy = let val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts - in Old_Locale.global_note_qualified kind facts' thy |> snd end + in global_note_qualified kind facts' thy |> snd end fun init_local_elem (Fixes fixes) ctxt = ctxt |> ProofContext.add_fixes_i fixes |> snd @@ -352,7 +359,7 @@ | init_local_elem (Notes (kind, facts)) ctxt = let val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts - in Old_Locale.local_note_qualified kind facts' ctxt |> snd end + in local_note_qualified kind facts' ctxt |> snd end fun cons_elem false (Notes notes) elems = elems | cons_elem _ elem elems = elem :: elems @@ -445,7 +452,7 @@ let val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |> Attrib.map_facts (Attrib.attribute_i thy) - in Old_Locale.global_note_qualified kind args'' #> snd end) + in global_note_qualified kind args'' #> snd end) (get_registrations thy |> filter (fn (name, _) => name = loc)) thy)) in ctxt'' end; @@ -496,12 +503,10 @@ val _ = Context.>> (Context.map_theory (Method.add_methods [("intro_locales", - Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt ORELSE' - Old_Locale.intro_locales_tac false ctxt)), + Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)), "back-chain introduction rules of locales without unfolding predicates"), ("unfold_locales", - Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE' - Old_Locale.intro_locales_tac true ctxt)), + Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)), "back-chain all introduction rules of locales")])); end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/obtain.ML Wed Jan 21 16:51:45 2009 +0100 @@ -39,16 +39,16 @@ signature OBTAIN = sig val thatN: string - val obtain: string -> (Binding.T * string option * mixfix) list -> + val obtain: string -> (binding * string option * mixfix) list -> (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state - val obtain_i: string -> (Binding.T * typ option * mixfix) list -> - ((Binding.T * attribute list) * (term * term list) list) list -> + val obtain_i: string -> (binding * typ option * mixfix) list -> + ((binding * attribute list) * (term * term list) list) list -> bool -> Proof.state -> Proof.state val result: (Proof.context -> tactic) -> thm list -> Proof.context -> (cterm list * thm list) * Proof.context - val guess: (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state - val guess_i: (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state + val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state + val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state end; structure Obtain: OBTAIN = diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/old_locale.ML --- a/src/Pure/Isar/old_locale.ML Tue Jan 20 19:09:19 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2485 +0,0 @@ -(* Title: Pure/Isar/locale.ML - Author: Clemens Ballarin, TU Muenchen - Author: Markus Wenzel, LMU/TU Muenchen - -Locales -- Isar proof contexts as meta-level predicates, with local -syntax and implicit structures. - -Draws basic ideas from Florian Kammueller's original version of -locales, but uses the richer infrastructure of Isar instead of the raw -meta-logic. Furthermore, structured import of contexts (with merge -and rename operations) are provided, as well as type-inference of the -signature parts, and predicate definitions of the specification text. - -Interpretation enables the reuse of theorems of locales in other -contexts, namely those defined by theories, structured proofs and -locales themselves. - -See also: - -[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar. - In Stefano Berardi et al., Types for Proofs and Programs: International - Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004. -[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing - Dependencies between Locales. Technical Report TUM-I0607, Technische - Universitaet Muenchen, 2006. -[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and - Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108, - pages 31-43, 2006. -*) - -(* TODO: -- beta-eta normalisation of interpretation parameters -- dangling type frees in locales -- test subsumption of interpretations when merging theories -*) - -signature OLD_LOCALE = -sig - datatype expr = - Locale of string | - Rename of expr * (string * mixfix option) option list | - Merge of expr list - val empty: expr - - val intern: theory -> xstring -> string - val intern_expr: theory -> expr -> expr - val extern: theory -> string -> xstring - val init: string -> theory -> Proof.context - - (* The specification of a locale *) - val parameters_of: theory -> string -> ((string * typ) * mixfix) list - val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list - val local_asms_of: theory -> string -> (Attrib.binding * term list) list - val global_asms_of: theory -> string -> (Attrib.binding * term list) list - - (* Theorems *) - val intros: theory -> string -> thm list * thm list - val dests: theory -> string -> thm list - (* Not part of the official interface. DO NOT USE *) - val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list - - (* Not part of the official interface. DO NOT USE *) - val declarations_of: theory -> string -> declaration list * declaration list; - - (* Processing of locale statements *) - val read_context_statement: string option -> Element.context list -> - (string * string list) list list -> Proof.context -> - string option * Proof.context * Proof.context * (term * term list) list list - val read_context_statement_cmd: xstring option -> Element.context list -> - (string * string list) list list -> Proof.context -> - string option * Proof.context * Proof.context * (term * term list) list list - val cert_context_statement: string option -> Element.context_i list -> - (term * term list) list list -> Proof.context -> - string option * Proof.context * Proof.context * (term * term list) list list - val read_expr: expr -> Element.context list -> Proof.context -> - Element.context_i list * Proof.context - val cert_expr: expr -> Element.context_i list -> Proof.context -> - Element.context_i list * Proof.context - - (* Diagnostic functions *) - val print_locales: theory -> unit - val print_locale: theory -> bool -> expr -> Element.context list -> unit - val print_registrations: bool -> string -> Proof.context -> unit - - val add_locale: string -> bstring -> expr -> Element.context_i list -> theory - -> string * Proof.context - val add_locale_cmd: bstring -> expr -> Element.context list -> theory - -> string * Proof.context - - (* Tactics *) - val intro_locales_tac: bool -> Proof.context -> thm list -> tactic - - (* Storing results *) - val global_note_qualified: string -> - ((Binding.T * attribute list) * (thm list * attribute list) list) list -> - theory -> (string * thm list) list * theory - val local_note_qualified: string -> - ((Binding.T * attribute list) * (thm list * attribute list) list) list -> - Proof.context -> (string * thm list) list * Proof.context - 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 - - (* Interpretation *) - val get_interpret_morph: theory -> (Binding.T -> Binding.T) -> string * string -> - (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> - string -> term list -> Morphism.morphism - val interpretation: (Proof.context -> Proof.context) -> - (Binding.T -> Binding.T) -> expr -> - term option list * (Attrib.binding * term) list -> - theory -> - (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state - val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list -> - theory -> Proof.state - val interpretation_in_locale: (Proof.context -> Proof.context) -> - xstring * expr -> theory -> Proof.state - val interpret: (Proof.state -> Proof.state) -> - (Binding.T -> Binding.T) -> expr -> - term option list * (Attrib.binding * term) list -> - bool -> Proof.state -> - (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state - val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list -> - bool -> Proof.state -> Proof.state -end; - -structure Old_Locale: OLD_LOCALE = -struct - -(* legacy operations *) - -fun merge_lists _ xs [] = xs - | merge_lists _ [] ys = ys - | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys; - -fun merge_alists eq xs = merge_lists (eq_fst eq) xs; - - -(* auxiliary: noting name bindings with qualified base names *) - -fun global_note_qualified kind facts thy = - thy - |> Sign.qualified_names - |> PureThy.note_thmss kind facts - ||> Sign.restore_naming thy; - -fun local_note_qualified kind facts ctxt = - ctxt - |> ProofContext.qualified_names - |> ProofContext.note_thmss_i kind facts - ||> ProofContext.restore_naming ctxt; - - -(** locale elements and expressions **) - -datatype ctxt = datatype Element.ctxt; - -datatype expr = - Locale of string | - Rename of expr * (string * mixfix option) option list | - Merge of expr list; - -val empty = Merge []; - -datatype 'a element = - Elem of 'a | Expr of expr; - -fun map_elem f (Elem e) = Elem (f e) - | map_elem _ (Expr e) = Expr e; - -type decl = declaration * stamp; - -type locale = - {axiom: Element.witness list, - (* For locales that define predicates this is [A [A]], where A is the locale - specification. Otherwise []. - Only required to generate the right witnesses for locales with predicates. *) - elems: (Element.context_i * stamp) list, - (* Static content, neither Fixes nor Constrains elements *) - params: ((string * typ) * mixfix) list, (*all term params*) - decls: decl list * decl list, (*type/term_syntax declarations*) - regs: ((string * string list) * Element.witness list) list, - (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *) - intros: thm list * thm list, - (* Introduction rules: of delta predicate and locale predicate. *) - dests: thm list} - (* Destruction rules: projections from locale predicate to predicates of fragments. *) - -(* CB: an internal (Int) locale element was either imported or included, - an external (Ext) element appears directly in the locale text. *) - -datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b; - - - -(** substitutions on Vars -- clone from element.ML **) - -(* instantiate types *) - -fun var_instT_type env = - if Vartab.is_empty env then I - else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x)); - -fun var_instT_term env = - if Vartab.is_empty env then I - else Term.map_types (var_instT_type env); - -fun var_inst_term (envT, env) = - if Vartab.is_empty env then var_instT_term envT - else - let - val instT = var_instT_type envT; - fun inst (Const (x, T)) = Const (x, instT T) - | inst (Free (x, T)) = Free(x, instT T) - | inst (Var (xi, T)) = - (case Vartab.lookup env xi of - NONE => Var (xi, instT T) - | SOME t => t) - | inst (b as Bound _) = b - | inst (Abs (x, T, t)) = Abs (x, instT T, inst t) - | inst (t $ u) = inst t $ inst u; - in Envir.beta_norm o inst end; - - -(** management of registrations in theories and proof contexts **) - -type registration = - {prfx: (Binding.T -> Binding.T) * (string * string), - (* first component: interpretation name morphism; - second component: parameter prefix *) - exp: Morphism.morphism, - (* maps content to its originating context *) - imp: (typ Vartab.table * typ list) * (term Vartab.table * term list), - (* inverse of exp *) - wits: Element.witness list, - (* witnesses of the registration *) - eqns: thm Termtab.table, - (* theorems (equations) interpreting derived concepts and indexed by lhs *) - morph: unit - (* interpreting morphism *) - } - -structure Registrations : - sig - type T - val empty: T - val join: T * T -> T - val dest: theory -> T -> - (term list * - (((Binding.T -> Binding.T) * (string * string)) * - (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * - Element.witness list * - thm Termtab.table)) list - val test: theory -> T * term list -> bool - val lookup: theory -> - T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> - (((Binding.T -> Binding.T) * (string * string)) * Element.witness list * thm Termtab.table) option - val insert: theory -> term list -> ((Binding.T -> Binding.T) * (string * string)) -> - (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> - T -> - T * (term list * (((Binding.T -> Binding.T) * (string * string)) * Element.witness list)) list - val add_witness: term list -> Element.witness -> T -> T - val add_equation: term list -> thm -> T -> T -(* - val update_morph: term list -> Morphism.morphism -> T -> T - val get_morph: theory -> T -> - term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) -> - Morphism.morphism -*) - end = -struct - (* A registration is indexed by parameter instantiation. - NB: index is exported whereas content is internalised. *) - type T = registration Termtab.table; - - fun mk_reg prfx exp imp wits eqns morph = - {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph}; - - fun map_reg f reg = - let - val {prfx, exp, imp, wits, eqns, morph} = reg; - val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph); - in mk_reg prfx' exp' imp' wits' eqns' morph' end; - - val empty = Termtab.empty; - - (* term list represented as single term, for simultaneous matching *) - fun termify ts = - Term.list_comb (Const ("", map fastype_of ts ---> propT), ts); - fun untermify t = - let fun ut (Const _) ts = ts - | ut (s $ t) ts = ut s (t::ts) - in ut t [] end; - - (* joining of registrations: - - prefix and morphisms of right theory; - - witnesses are equal, no attempt to subsumption testing; - - union of equalities, if conflicting (i.e. two eqns with equal lhs) - eqn of right theory takes precedence *) - fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) => - mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2); - - fun dest_transfer thy regs = - Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) => - (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m)))); - - fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |> - map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns))); - - (* registrations that subsume t *) - fun subsumers thy t regs = - filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs); - - (* test if registration that subsumes the query is present *) - fun test thy (regs, ts) = - not (null (subsumers thy (termify ts) regs)); - - (* look up registration, pick one that subsumes the query *) - fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) = - let - val t = termify ts; - val subs = subsumers thy t regs; - in - (case subs of - [] => NONE - | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) => - let - val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); - val tinst' = domT' |> map (fn (T as TFree (x, _)) => - (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst - |> var_instT_type impT)) |> Symtab.make; - val inst' = dom' |> map (fn (t as Free (x, _)) => - (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst) - |> var_inst_term (impT, imp))) |> Symtab.make; - val inst'_morph = Element.inst_morphism thy (tinst', inst'); - in SOME (prfx, - map (Element.morph_witness inst'_morph) wits, - Termtab.map (Morphism.thm inst'_morph) eqns) - end) - end; - - (* add registration if not subsumed by ones already present, - additionally returns registrations that are strictly subsumed *) - fun insert thy ts prfx (exp, imp) regs = - let - val t = termify ts; - val subs = subsumers thy t regs ; - in (case subs of - [] => let - val sups = - filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); - val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits))) - in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end - | _ => (regs, [])) - end; - - fun gen_add f ts regs = - let - val t = termify ts; - in - Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs - end; - - (* add witness theorem to registration, - only if instantiation is exact, otherwise exception Option raised *) - fun add_witness ts wit regs = - gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m)) - ts regs; - - (* add equation to registration, replaces previous equation with same lhs; - only if instantiation is exact, otherwise exception Option raised; - exception TERM raised if not a meta equality *) - fun add_equation ts thm regs = - gen_add (fn (x, e, i, thms, eqns, m) => - (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m)) - ts regs; - -end; - - -(** theory data : locales **) - -structure LocalesData = TheoryDataFun -( - type T = NameSpace.T * locale Symtab.table; - (* 1st entry: locale namespace, - 2nd entry: locales of the theory *) - - val empty = NameSpace.empty_table; - val copy = I; - val extend = I; - - fun join_locales _ - ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale, - {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) = - {axiom = axiom, - elems = merge_lists (eq_snd (op =)) elems elems', - params = params, - decls = - (Library.merge (eq_snd (op =)) (decls1, decls1'), - Library.merge (eq_snd (op =)) (decls2, decls2')), - regs = merge_alists (op =) regs regs', - intros = intros, - dests = dests}; - fun merge _ = NameSpace.join_tables join_locales; -); - - - -(** context data : registrations **) - -structure RegistrationsData = GenericDataFun -( - type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*) - val empty = Symtab.empty; - val extend = I; - fun merge _ = Symtab.join (K Registrations.join); -); - - -(** access locales **) - -val intern = NameSpace.intern o #1 o LocalesData.get; -val extern = NameSpace.extern o #1 o LocalesData.get; - -fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name; - -fun the_locale thy name = case get_locale thy name - of SOME loc => loc - | NONE => error ("Unknown locale " ^ quote name); - -fun register_locale bname loc thy = - thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) - (Binding.name bname, loc) #> snd); - -fun change_locale name f thy = - let - val {axiom, elems, params, decls, regs, intros, dests} = - the_locale thy name; - val (axiom', elems', params', decls', regs', intros', dests') = - f (axiom, elems, params, decls, regs, intros, dests); - in - thy - |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom', - elems = elems', params = params', - decls = decls', regs = regs', intros = intros', dests = dests'})) - end; - -fun print_locales thy = - let val (space, locs) = LocalesData.get thy in - Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) - |> Pretty.writeln - end; - - -(* access registrations *) - -(* retrieve registration from theory or context *) - -fun get_registrations ctxt name = - case Symtab.lookup (RegistrationsData.get ctxt) name of - NONE => [] - | SOME reg => Registrations.dest (Context.theory_of ctxt) reg; - -fun get_global_registrations thy = get_registrations (Context.Theory thy); -fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt); - - -fun get_registration ctxt imprt (name, ps) = - case Symtab.lookup (RegistrationsData.get ctxt) name of - NONE => NONE - | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt)); - -fun get_global_registration thy = get_registration (Context.Theory thy); -fun get_local_registration ctxt = get_registration (Context.Proof ctxt); - - -fun test_registration ctxt (name, ps) = - case Symtab.lookup (RegistrationsData.get ctxt) name of - NONE => false - | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps); - -fun test_global_registration thy = test_registration (Context.Theory thy); -fun test_local_registration ctxt = test_registration (Context.Proof ctxt); - - -(* add registration to theory or context, ignored if subsumed *) - -fun put_registration (name, ps) prfx morphs ctxt = - RegistrationsData.map (fn regs => - let - val thy = Context.theory_of ctxt; - val reg = the_default Registrations.empty (Symtab.lookup regs name); - val (reg', sups) = Registrations.insert thy ps prfx morphs reg; - val _ = if not (null sups) then warning - ("Subsumed interpretation(s) of locale " ^ - quote (extern thy name) ^ - "\nwith the following prefix(es):" ^ - commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups)) - else (); - in Symtab.update (name, reg') regs end) ctxt; - -fun put_global_registration id prfx morphs = - Context.theory_map (put_registration id prfx morphs); -fun put_local_registration id prfx morphs = - Context.proof_map (put_registration id prfx morphs); - -fun put_registration_in_locale name id = - change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) => - (axiom, elems, params, decls, regs @ [(id, [])], intros, dests)); - - -(* add witness theorem to registration, ignored if registration not present *) - -fun add_witness (name, ps) thm = - RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm)); - -fun add_global_witness id thm = Context.theory_map (add_witness id thm); -fun add_local_witness id thm = Context.proof_map (add_witness id thm); - - -fun add_witness_in_locale name id thm = - change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) => - let - fun add (id', thms) = - if id = id' then (id', thm :: thms) else (id', thms); - in (axiom, elems, params, decls, map add regs, intros, dests) end); - - -(* add equation to registration, ignored if registration not present *) - -fun add_equation (name, ps) thm = - RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm)); - -fun add_global_equation id thm = Context.theory_map (add_equation id thm); -fun add_local_equation id thm = Context.proof_map (add_equation id thm); - -(* -(* update morphism of registration, ignored if registration not present *) - -fun update_morph (name, ps) morph = - RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph)); - -fun update_global_morph id morph = Context.theory_map (update_morph id morph); -fun update_local_morph id morph = Context.proof_map (update_morph id morph); -*) - - -(* printing of registrations *) - -fun print_registrations show_wits loc ctxt = - let - val thy = ProofContext.theory_of ctxt; - val prt_term = Pretty.quote o Syntax.pretty_term ctxt; - fun prt_term' t = if !show_types - then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", - Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] - else prt_term t; - val prt_thm = prt_term o prop_of; - fun prt_inst ts = - Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts)); - fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx] - | prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx]; - fun prt_eqns [] = Pretty.str "no equations." - | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 :: - Pretty.breaks (map prt_thm eqns)); - fun prt_core ts eqns = - [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)]; - fun prt_witns [] = Pretty.str "no witnesses." - | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 :: - Pretty.breaks (map (Element.pretty_witness ctxt) witns)) - fun prt_reg (ts, (_, _, witns, eqns)) = - if show_wits - then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]) - else Pretty.block (prt_core ts eqns) - - val loc_int = intern thy loc; - val regs = RegistrationsData.get (Context.Proof ctxt); - val loc_regs = Symtab.lookup regs loc_int; - in - (case loc_regs of - NONE => Pretty.str ("no interpretations") - | SOME r => let - val r' = Registrations.dest thy r; - val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r'; - in Pretty.big_list ("interpretations:") (map prt_reg r'') end) - |> Pretty.writeln - end; - - -(* diagnostics *) - -fun err_in_locale ctxt msg ids = - let - val thy = ProofContext.theory_of ctxt; - fun prt_id (name, parms) = - [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))]; - val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); - val err_msg = - if forall (fn (s, _) => s = "") ids then msg - else msg ^ "\n" ^ Pretty.string_of (Pretty.block - (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); - in error err_msg end; - -fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); - - -fun pretty_ren NONE = Pretty.str "_" - | pretty_ren (SOME (x, NONE)) = Pretty.str x - | pretty_ren (SOME (x, SOME syn)) = - Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn]; - -fun pretty_expr thy (Locale name) = Pretty.str (extern thy name) - | pretty_expr thy (Rename (expr, xs)) = - Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)] - | pretty_expr thy (Merge es) = - Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block; - -fun err_in_expr _ msg (Merge []) = error msg - | err_in_expr ctxt msg expr = - error (msg ^ "\n" ^ Pretty.string_of (Pretty.block - [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1, - pretty_expr (ProofContext.theory_of ctxt) expr])); - - -(** structured contexts: rename + merge + implicit type instantiation **) - -(* parameter types *) - -fun frozen_tvars ctxt Ts = - #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt) - |> map (fn ((xi, S), T) => (xi, (S, T))); - -fun unify_frozen ctxt maxidx Ts Us = - let - fun paramify NONE i = (NONE, i) - | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i); - - val (Ts', maxidx') = fold_map paramify Ts maxidx; - val (Us', maxidx'') = fold_map paramify Us maxidx'; - val thy = ProofContext.theory_of ctxt; - - fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env - handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) - | unify _ env = env; - val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx''); - val Vs = map (Option.map (Envir.norm_type unifier)) Us'; - val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier; - in map (Option.map (Envir.norm_type unifier')) Vs end; - -fun params_of elemss = - distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss); - -fun params_of' elemss = - distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss); - -fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params); - - -(* CB: param_types has the following type: - ('a * 'b option) list -> ('a * 'b) list *) -fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; - - -fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss - handle Symtab.DUP x => err_in_locale ctxt - ("Conflicting syntax for parameter: " ^ quote x) (map fst ids); - - -(* Distinction of assumed vs. derived identifiers. - The former may have axioms relating assumptions of the context to - assumptions of the specification fragment (for locales with - predicates). The latter have witnesses relating assumptions of the - specification fragment to assumptions of other (assumed) specification - fragments. *) - -datatype 'a mode = Assumed of 'a | Derived of 'a; - -fun map_mode f (Assumed x) = Assumed (f x) - | map_mode f (Derived x) = Derived (f x); - - -(* flatten expressions *) - -local - -fun unify_parms ctxt fixed_parms raw_parmss = - let - val thy = ProofContext.theory_of ctxt; - val maxidx = length raw_parmss; - val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss; - - fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S)); - fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); - val parms = fixed_parms @ maps varify_parms idx_parmss; - - fun unify T U envir = Sign.typ_unify thy (U, T) envir - handle Type.TUNIFY => - let - val T' = Envir.norm_type (fst envir) T; - val U' = Envir.norm_type (fst envir) U; - val prt = Syntax.string_of_typ ctxt; - in - raise TYPE ("unify_parms: failed to unify types " ^ - prt U' ^ " and " ^ prt T', [U', T'], []) - end; - fun unify_list (T :: Us) = fold (unify T) Us - | unify_list [] = I; - val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms))) - (Vartab.empty, maxidx); - - val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms); - val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier; - - fun inst_parms (i, ps) = - List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps) - |> map_filter (fn (a, S) => - let val T = Envir.norm_type unifier' (TVar ((a, i), S)) - in if T = TFree (a, S) then NONE else SOME (a, T) end) - |> Symtab.make; - in map inst_parms idx_parmss end; - -in - -fun unify_elemss _ _ [] = [] - | unify_elemss _ [] [elems] = [elems] - | unify_elemss ctxt fixed_parms elemss = - let - val thy = ProofContext.theory_of ctxt; - val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss) - |> map (Element.instT_morphism thy); - fun inst ((((name, ps), mode), elems), phi) = - (((name, map (apsnd (Option.map (Morphism.typ phi))) ps), - map_mode (map (Element.morph_witness phi)) mode), - map (Element.morph_ctxt phi) elems); - in map inst (elemss ~~ phis) end; - - -fun renaming xs parms = zip_options parms xs - handle Library.UnequalLengths => - error ("Too many arguments in renaming: " ^ - commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs)); - - -(* params_of_expr: - Compute parameters (with types and syntax) of locale expression. -*) - -fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) = - let - val thy = ProofContext.theory_of ctxt; - - fun merge_tenvs fixed tenv1 tenv2 = - let - val [env1, env2] = unify_parms ctxt fixed - [tenv1 |> Symtab.dest |> map (apsnd SOME), - tenv2 |> Symtab.dest |> map (apsnd SOME)] - in - Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1, - Symtab.map (Element.instT_type env2) tenv2) - end; - - fun merge_syn expr syn1 syn2 = - Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2) - handle Symtab.DUP x => err_in_expr ctxt - ("Conflicting syntax for parameter: " ^ quote x) expr; - - fun params_of (expr as Locale name) = - let - val {params, ...} = the_locale thy name; - in (map (fst o fst) params, params |> map fst |> Symtab.make, - params |> map (apfst fst) |> Symtab.make) end - | params_of (expr as Rename (e, xs)) = - let - val (parms', types', syn') = params_of e; - val ren = renaming xs parms'; - (* renaming may reduce number of parameters *) - val new_parms = map (Element.rename ren) parms' |> distinct (op =); - val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren); - val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty - handle Symtab.DUP x => - err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr; - val syn_types = map (apsnd (fn mx => - SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0))))) - (Symtab.dest new_syn); - val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren)); - val (env :: _) = unify_parms ctxt [] - ((ren_types |> map (apsnd SOME)) :: map single syn_types); - val new_types = fold (Symtab.insert (op =)) - (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty; - in (new_parms, new_types, new_syn) end - | params_of (Merge es) = - fold (fn e => fn (parms, types, syn) => - let - val (parms', types', syn') = params_of e - in - (merge_lists (op =) parms parms', merge_tenvs [] types types', - merge_syn e syn syn') - end) - es ([], Symtab.empty, Symtab.empty) - - val (parms, types, syn) = params_of expr; - in - (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types, - merge_syn expr prev_syn syn) - end; - -fun make_params_ids params = [(("", params), ([], Assumed []))]; -fun make_raw_params_elemss (params, tenv, syn) = - [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []), - Int [Fixes (map (fn p => - (Binding.name p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])]; - - -(* flatten_expr: - Extend list of identifiers by those new in locale expression expr. - Compute corresponding list of lists of locale elements (one entry per - identifier). - - Identifiers represent locale fragments and are in an extended form: - ((name, ps), (ax_ps, axs)) - (name, ps) is the locale name with all its parameters. - (ax_ps, axs) is the locale axioms with its parameters; - axs are always taken from the top level of the locale hierarchy, - hence axioms may contain additional parameters from later fragments: - ps subset of ax_ps. axs is either singleton or empty. - - Elements are enriched by identifier-like information: - (((name, ax_ps), axs), elems) - The parameters in ax_ps are the axiom parameters, but enriched by type - info: now each entry is a pair of string and typ option. Axioms are - type-instantiated. - -*) - -fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = - let - val thy = ProofContext.theory_of ctxt; - - fun rename_parms top ren ((name, ps), (parms, mode)) = - ((name, map (Element.rename ren) ps), - if top - then (map (Element.rename ren) parms, - map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode) - else (parms, mode)); - - (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *) - - fun add_with_regs ((name, pTs), mode) (wits, ids, visited) = - if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs) - then (wits, ids, visited) - else - let - val {params, regs, ...} = the_locale thy name; - val pTs' = map #1 params; - val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs; - (* dummy syntax, since required by rename *) - val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs'); - val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs'']; - (* propagate parameter types, to keep them consistent *) - val regs' = map (fn ((name, ps), wits) => - ((name, map (Element.rename ren) ps), - map (Element.transfer_witness thy) wits)) regs; - val new_regs = regs'; - val new_ids = map fst new_regs; - val new_idTs = - map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids; - - val new_wits = new_regs |> map (#2 #> map - (Element.morph_witness - (Element.instT_morphism thy env $> - Element.rename_morphism ren $> - Element.satisfy_morphism wits) - #> Element.close_witness)); - val new_ids' = map (fn (id, wits) => - (id, ([], Derived wits))) (new_ids ~~ new_wits); - val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) => - ((n, pTs), mode)) (new_idTs ~~ new_ids'); - val new_id = ((name, map #1 pTs), ([], mode)); - val (wits', ids', visited') = fold add_with_regs new_idTs' - (wits @ flat new_wits, ids, visited @ [new_id]); - in - (wits', ids' @ [new_id], visited') - end; - - (* distribute top-level axioms over assumed ids *) - - fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms = - let - val {elems, ...} = the_locale thy name; - val ts = maps - (fn (Assumes asms, _) => maps (map #1 o #2) asms - | _ => []) - elems; - val (axs1, axs2) = chop (length ts) axioms; - in (((name, parms), (all_ps, Assumed axs1)), axs2) end - | axiomify all_ps (id, (_, Derived ths)) axioms = - ((id, (all_ps, Derived ths)), axioms); - - (* identifiers of an expression *) - - fun identify top (Locale name) = - (* CB: ids_ax is a list of tuples of the form ((name, ps), axs), - where name is a locale name, ps a list of parameter names and axs - a list of axioms relating to the identifier, axs is empty unless - identify at top level (top = true); - parms is accumulated list of parameters *) - let - val {axiom, params, ...} = the_locale thy name; - val ps = map (#1 o #1) params; - val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []); - val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids''; - in (ids_ax, ps) end - | identify top (Rename (e, xs)) = - let - val (ids', parms') = identify top e; - val ren = renaming xs parms' - handle ERROR msg => err_in_locale' ctxt msg ids'; - - val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids'); - val parms'' = distinct (op =) (maps (#2 o #1) ids''); - in (ids'', parms'') end - | identify top (Merge es) = - fold (fn e => fn (ids, parms) => - let - val (ids', parms') = identify top e - in - (merge_alists (op =) ids ids', merge_lists (op =) parms parms') - end) - es ([], []); - - fun inst_wit all_params (t, th) = let - val {hyps, prop, ...} = Thm.rep_thm th; - val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []); - val [env] = unify_parms ctxt all_params [ps]; - val t' = Element.instT_term env t; - val th' = Element.instT_thm thy env th; - in (t', th') end; - - fun eval all_params tenv syn ((name, params), (locale_params, mode)) = - let - val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name; - val elems = map fst elems_stamped; - val ps = map fst ps_mx; - fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt); - val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params; - val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode; - val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params; - val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps]; - val (lprfx, pprfx) = param_prefix name params; - val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx - #> Binding.add_prefix false lprfx; - val elem_morphism = - Element.rename_morphism ren $> - Morphism.binding_morphism add_prefices $> - Element.instT_morphism thy env; - val elems' = map (Element.morph_ctxt elem_morphism) elems; - in (((name, map (apsnd SOME) locale_params'), mode'), elems') end; - - (* parameters, their types and syntax *) - val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty); - val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params'; - (* compute identifiers and syntax, merge with previous ones *) - val (ids, _) = identify true expr; - val idents = subtract (eq_fst (op =)) prev_idents ids; - val syntax = merge_syntax ctxt ids (syn, prev_syntax); - (* type-instantiate elements *) - val final_elemss = map (eval all_params tenv syntax) idents; - in ((prev_idents @ idents, syntax), final_elemss) end; - -end; - - -(* activate elements *) - -local - -fun axioms_export axs _ As = - (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t); - - -(* NB: derived ids contain only facts at this stage *) - -fun activate_elem _ _ (Fixes fixes) (ctxt, mode) = - ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode)) - | activate_elem _ _ (Constrains _) (ctxt, mode) = - ([], (ctxt, mode)) - | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) = - let - val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; - val ts = maps (map #1 o #2) asms'; - val (ps, qs) = chop (length ts) axs; - val (_, ctxt') = - ctxt |> fold Variable.auto_fixes ts - |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms'; - in ([], (ctxt', Assumed qs)) end - | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) = - ([], (ctxt, Derived ths)) - | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) = - let - val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; - val asms = defs' |> map (fn ((name, atts), (t, ps)) => - let val ((c, _), t') = LocalDefs.cert_def ctxt t - in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end); - val (_, ctxt') = - ctxt |> fold (Variable.auto_fixes o #1) asms - |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); - in ([], (ctxt', Assumed axs)) end - | activate_elem _ _ (Defines defs) (ctxt, Derived ths) = - ([], (ctxt, Derived ths)) - | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) = - let - val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; - val (res, ctxt') = ctxt |> local_note_qualified kind facts'; - in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end; - -fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt = - let - val thy = ProofContext.theory_of ctxt; - val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = "")) - elems (ProofContext.qualified_names ctxt, mode) - handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]; - val ctxt'' = if name = "" then ctxt' - else let - val ps' = map (fn (n, SOME T) => Free (n, T)) ps; - in if test_local_registration ctxt' (name, ps') then ctxt' - else let - val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, "")) - (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt' - in case mode of - Assumed axs => - fold (add_local_witness (name, ps') o - Element.assume_witness thy o Element.witness_prop) axs ctxt'' - | Derived ths => - fold (add_local_witness (name, ps')) ths ctxt'' - end - end - in (ProofContext.restore_naming ctxt ctxt'', res) end; - -fun activate_elemss ax_in_ctxt prep_facts = - fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt => - let - val elems = map (prep_facts ctxt) raw_elems; - val (ctxt', res) = apsnd flat - (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt); - val elems' = elems |> map (Element.map_ctxt_attrib Args.closure); - in (((((name, ps), mode), elems'), res), ctxt') end); - -in - -(* CB: activate_facts prep_facts elemss ctxt, - where elemss is a list of pairs consisting of identifiers and - context elements, extends ctxt by the context elements yielding - ctxt' and returns ((elemss', facts), ctxt'). - Identifiers in the argument are of the form ((name, ps), axs) and - assumptions use the axioms in the identifiers to set up exporters - in ctxt'. elemss' does not contain identifiers and is obtained - from elemss and the intermediate context with prep_facts. - If read_facts or cert_facts is used for prep_facts, these also remove - the internal/external markers from elemss. *) - -fun activate_facts ax_in_ctxt prep_facts args = - activate_elemss ax_in_ctxt prep_facts args - #>> (apsnd flat o split_list); - -end; - - - -(** prepare locale elements **) - -(* expressions *) - -fun intern_expr thy (Locale xname) = Locale (intern thy xname) - | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) - | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs); - - -(* propositions and bindings *) - -(* flatten (ctxt, prep_expr) ((ids, syn), expr) - normalises expr (which is either a locale - expression or a single context element) wrt. - to the list ids of already accumulated identifiers. - It returns ((ids', syn'), elemss) where ids' is an extension of ids - with identifiers generated for expr, and elemss is the list of - context elements generated from expr. - syn and syn' are symtabs mapping parameter names to their syntax. syn' - is an extension of syn. - For details, see flatten_expr. - - Additionally, for a locale expression, the elems are grouped into a single - Int; individual context elements are marked Ext. In this case, the - identifier-like information of the element is as follows: - - for Fixes: (("", ps), []) where the ps have type info NONE - - for other elements: (("", []), []). - The implementation of activate_facts relies on identifier names being - empty strings for external elements. -*) - -fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let - val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))] - in - ((ids', - merge_syntax ctxt ids' - (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes)) - handle Symtab.DUP x => err_in_locale ctxt - ("Conflicting syntax for parameter: " ^ quote x) - (map #1 ids')), - [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))]) - end - | flatten _ ((ids, syn), Elem elem) = - ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)]) - | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) = - apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr)); - -local - -local - -fun declare_int_elem (Fixes fixes) ctxt = - ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) => - (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd) - | declare_int_elem _ ctxt = ([], ctxt); - -fun declare_ext_elem prep_vars (Fixes fixes) ctxt = - let val (vars, _) = prep_vars fixes ctxt - in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end - | declare_ext_elem prep_vars (Constrains csts) ctxt = - let val (_, ctxt') = prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) ctxt - in ([], ctxt') end - | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt) - | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt) - | declare_ext_elem _ (Notes _) ctxt = ([], ctxt); - -fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems - of Int es => fold_map declare_int_elem es ctxt - | Ext e => declare_ext_elem prep_vars e ctxt |>> single) - handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]) - | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt); - -in - -fun declare_elemss prep_vars fixed_params raw_elemss ctxt = - let - (* CB: fix of type bug of goal in target with context elements. - Parameters new in context elements must receive types that are - distinct from types of parameters in target (fixed_params). *) - val ctxt_with_fixed = - fold Variable.declare_term (map Free fixed_params) ctxt; - val int_elemss = - raw_elemss - |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE) - |> unify_elemss ctxt_with_fixed fixed_params; - val (raw_elemss', _) = - fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x)) - raw_elemss int_elemss; - in fold_map (declare_elems prep_vars) raw_elemss' ctxt end; - -end; - -local - -val norm_term = Envir.beta_norm oo Term.subst_atomic; - -fun abstract_thm thy eq = - Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def; - -fun bind_def ctxt (name, ps) eq (xs, env, ths) = - let - val ((y, T), b) = LocalDefs.abs_def eq; - val b' = norm_term env b; - val th = abstract_thm (ProofContext.theory_of ctxt) eq; - fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; - in - exists (fn (x, _) => x = y) xs andalso - err "Attempt to define previously specified variable"; - exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso - err "Attempt to redefine variable"; - (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) - end; - - -(* CB: for finish_elems (Int and Ext), - extracts specification, only of assumed elements *) - -fun eval_text _ _ _ (Fixes _) text = text - | eval_text _ _ _ (Constrains _) text = text - | eval_text _ (_, Assumed _) is_ext (Assumes asms) - (((exts, exts'), (ints, ints')), (xs, env, defs)) = - let - val ts = maps (map #1 o #2) asms; - val ts' = map (norm_term env) ts; - val spec' = - if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) - else ((exts, exts'), (ints @ ts, ints' @ ts')); - in (spec', (fold Term.add_frees ts' xs, env, defs)) end - | eval_text _ (_, Derived _) _ (Assumes _) text = text - | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) = - (spec, fold (bind_def ctxt id o #1 o #2) defs binds) - | eval_text _ (_, Derived _) _ (Defines _) text = text - | eval_text _ _ _ (Notes _) text = text; - - -(* for finish_elems (Int), - remove redundant elements of derived identifiers, - turn assumptions and definitions into facts, - satisfy hypotheses of facts *) - -fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes) - | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts) - | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms) - | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs) - - | finish_derived _ _ (Derived _) (Fixes _) = NONE - | finish_derived _ _ (Derived _) (Constrains _) = NONE - | finish_derived sign satisfy (Derived _) (Assumes asms) = asms - |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) - |> pair Thm.assumptionK |> Notes - |> Element.morph_ctxt satisfy |> SOME - | finish_derived sign satisfy (Derived _) (Defines defs) = defs - |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) - |> pair Thm.definitionK |> Notes - |> Element.morph_ctxt satisfy |> SOME - - | finish_derived _ satisfy _ (Notes facts) = Notes facts - |> Element.morph_ctxt satisfy |> SOME; - -(* CB: for finish_elems (Ext) *) - -fun closeup _ false elem = elem - | closeup ctxt true elem = - let - fun close_frees t = - let - val rev_frees = - Term.fold_aterms (fn Free (x, T) => - if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t []; - in Term.list_all_free (rev rev_frees, t) end; - - fun no_binds [] = [] - | no_binds _ = error "Illegal term bindings in locale element"; - in - (case elem of - Assumes asms => Assumes (asms |> map (fn (a, propps) => - (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) - | Defines defs => Defines (defs |> map (fn (a, (t, ps)) => - (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) - | e => e) - end; - - -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) => - let val x = Binding.base_name b - in (b, AList.lookup (op =) parms x, mx) end) fixes) - | finish_ext_elem parms _ (Constrains _, _) = Constrains [] - | finish_ext_elem _ close (Assumes asms, propp) = - close (Assumes (map #1 asms ~~ propp)) - | finish_ext_elem _ close (Defines defs, propp) = - close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp)) - | finish_ext_elem _ _ (Notes facts, _) = Notes facts; - - -(* CB: finish_parms introduces type info from parms to identifiers *) -(* CB: only needed for types that have been NONE so far??? - If so, which are these??? *) - -fun finish_parms parms (((name, ps), mode), elems) = - (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems); - -fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) = - let - val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)]; - val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths; - val text' = fold (eval_text ctxt id' false) es text; - val es' = map_filter - (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es; - in ((text', wits'), (id', map Int es')) end - | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) = - let - val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); - val text' = eval_text ctxt id true e' text; - in ((text', wits), (id, [Ext e'])) end - -in - -(* CB: only called by prep_elemss *) - -fun finish_elemss ctxt parms do_close = - foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); - -end; - - -(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *) - -fun defs_ord (defs1, defs2) = - list_ord (fn ((_, (d1, _)), (_, (d2, _))) => - TermOrd.fast_term_ord (d1, d2)) (defs1, defs2); -structure Defstab = - TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord); - -fun rem_dup_defs es ds = - fold_map (fn e as (Defines defs) => (fn ds => - if Defstab.defined ds defs - then (Defines [], ds) - else (e, Defstab.update (defs, ()) ds)) - | e => (fn ds => (e, ds))) es ds; -fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds) - | rem_dup_elemss (Ext e) ds = (Ext e, ds); -fun rem_dup_defines raw_elemss = - fold_map (fn (id as (_, (Assumed _)), es) => (fn ds => - apfst (pair id) (rem_dup_elemss es ds)) - | (id as (_, (Derived _)), es) => (fn ds => - ((id, es), ds))) raw_elemss Defstab.empty |> #1; - -(* CB: type inference and consistency checks for locales. - - Works by building a context (through declare_elemss), extracting the - required information and adjusting the context elements (finish_elemss). - Can also universally close free vars in assms and defs. This is only - needed for Ext elements and controlled by parameter do_close. - - Only elements of assumed identifiers are considered. -*) - -fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl = - let - (* CB: contexts computed in the course of this function are discarded. - They are used for type inference and consistency checks only. *) - (* CB: fixed_params are the parameters (with types) of the target locale, - empty list if there is no target. *) - (* CB: raw_elemss are list of pairs consisting of identifiers and - context elements, the latter marked as internal or external. *) - val raw_elemss = rem_dup_defines raw_elemss; - val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context; - (* CB: raw_ctxt is context with additional fixed variables derived from - the fixes elements in raw_elemss, - raw_proppss contains assumptions and definitions from the - external elements in raw_elemss. *) - fun prep_prop raw_propp (raw_ctxt, raw_concl) = - let - (* CB: add type information from fixed_params to context (declare_term) *) - (* CB: process patterns (conclusion and external elements only) *) - val (ctxt, all_propp) = - prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); - (* CB: add type information from conclusion and external elements to context *) - val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt; - (* CB: resolve schematic variables (patterns) in conclusion and external elements. *) - val all_propp' = map2 (curry (op ~~)) - (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); - val (concl, propp) = chop (length raw_concl) all_propp'; - in (propp, (ctxt, concl)) end - - val (proppss, (ctxt, concl)) = - (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl); - - (* CB: obtain all parameters from identifier part of raw_elemss *) - val xs = map #1 (params_of' raw_elemss); - val typing = unify_frozen ctxt 0 - (map (Variable.default_type raw_ctxt) xs) - (map (Variable.default_type ctxt) xs); - val parms = param_types (xs ~~ typing); - (* CB: parms are the parameters from raw_elemss, with correct typing. *) - - (* CB: extract information from assumes and defines elements - (fixes, constrains and notes in raw_elemss don't have an effect on - text and elemss), compute final form of context elements. *) - val ((text, _), elemss) = finish_elemss ctxt parms do_close - ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss); - (* CB: text has the following structure: - (((exts, exts'), (ints, ints')), (xs, env, defs)) - where - exts: external assumptions (terms in external assumes elements) - exts': dito, normalised wrt. env - ints: internal assumptions (terms in internal assumes elements) - ints': dito, normalised wrt. env - xs: the free variables in exts' and ints' and rhss of definitions, - this includes parameters except defined parameters - env: list of term pairs encoding substitutions, where the first term - is a free variable; substitutions represent defines elements and - the rhs is normalised wrt. the previous env - defs: theorems representing the substitutions from defines elements - (thms are normalised wrt. env). - elemss is an updated version of raw_elemss: - - type info added to Fixes and modified in Constrains - - axiom and definition statement replaced by corresponding one - from proppss in Assumes and Defines - - Facts unchanged - *) - in ((parms, elemss, concl), text) end; - -in - -fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x; -fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x; - -end; - - -(* facts and attributes *) - -local - -fun check_name name = - if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) - else name; - -fun prep_facts _ _ _ ctxt (Int elem) = elem - |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt))) - | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt - {var = I, typ = I, term = I, - binding = Binding.map_base prep_name, - fact = get ctxt, - attrib = Args.assignable o intern (ProofContext.theory_of ctxt)}; - -in - -fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x; -fun cert_facts x = prep_facts I (K I) (K I) x; - -end; - - -(* Get the specification of a locale *) - -(*The global specification is made from the parameters and global - assumptions, the local specification from the parameters and the - local assumptions.*) - -local - -fun gen_asms_of get thy name = - let - val ctxt = ProofContext.init thy; - val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name)); - val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss []; - in - elemss |> get - |> maps (fn (_, es) => map (fn Int e => e) es) - |> maps (fn Assumes asms => asms | _ => []) - |> map (apsnd (map fst)) - end; - -in - -fun parameters_of thy = #params o the_locale thy; - -fun intros thy = #intros o the_locale thy; - (*returns introduction rule for delta predicate and locale predicate - as a pair of singleton lists*) - -fun dests thy = #dests o the_locale thy; - -fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts - | _ => NONE) o #elems o the_locale thy; - -fun parameters_of_expr thy expr = - let - val ctxt = ProofContext.init thy; - val pts = params_of_expr ctxt [] (intern_expr thy expr) - ([], Symtab.empty, Symtab.empty); - val raw_params_elemss = make_raw_params_elemss pts; - val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy) - (([], Symtab.empty), Expr expr); - val ((parms, _, _), _) = - read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) []; - in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end; - -fun local_asms_of thy name = - gen_asms_of (single o Library.last_elem) thy name; - -fun global_asms_of thy name = - gen_asms_of I thy name; - -end; - - -(* full context statements: imports + elements + conclusion *) - -local - -fun prep_context_statement prep_expr prep_elemss prep_facts - do_close fixed_params imports elements raw_concl context = - let - val thy = ProofContext.theory_of context; - - val (import_params, import_tenv, import_syn) = - params_of_expr context fixed_params (prep_expr thy imports) - ([], Symtab.empty, Symtab.empty); - val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements; - val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params) - (map (prep_expr thy) includes) (import_params, import_tenv, import_syn); - - val ((import_ids, _), raw_import_elemss) = - flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports); - (* CB: normalise "includes" among elements *) - val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy)) - ((import_ids, incl_syn), elements); - - val raw_elemss = flat raw_elemsss; - (* CB: raw_import_elemss @ raw_elemss is the normalised list of - context elements obtained from import and elements. *) - (* Now additional elements for parameters are inserted. *) - val import_params_ids = make_params_ids import_params; - val incl_params_ids = - make_params_ids (incl_params \\ import_params); - val raw_import_params_elemss = - make_raw_params_elemss (import_params, incl_tenv, incl_syn); - val raw_incl_params_elemss = - make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn); - val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close - context fixed_params - (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl; - - (* replace extended ids (for axioms) by ids *) - val (import_ids', incl_ids) = chop (length import_ids) ids; - val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids; - val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) => - (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems)) - (all_ids ~~ all_elemss); - (* CB: all_elemss and parms contain the correct parameter types *) - - val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss'; - val ((import_elemss, _), import_ctxt) = - activate_facts false prep_facts ps context; - - val ((elemss, _), ctxt) = - activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt); - in - ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), - (parms, spec, defs)), concl) - end; - -fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt = - let - val thy = ProofContext.theory_of ctxt; - val locale = Option.map (prep_locale thy) raw_locale; - val (fixed_params, imports) = - (case locale of - NONE => ([], empty) - | SOME name => - let val {params = ps, ...} = the_locale thy name - in (map fst ps, Locale name) end); - val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') = - prep_ctxt false fixed_params imports (map Elem elems) concl ctxt; - in (locale, locale_ctxt, elems_ctxt, concl') end; - -fun prep_expr prep imports body ctxt = - let - val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt; - val all_elems = maps snd (import_elemss @ elemss); - in (all_elems, ctxt') end; - -in - -val read_ctxt = prep_context_statement intern_expr read_elemss read_facts; -val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts; - -fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt); -fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt); - -val read_expr = prep_expr read_context; -val cert_expr = prep_expr cert_context; - -fun read_context_statement loc = prep_statement (K I) read_ctxt loc; -fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc; -fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc; - -end; - - -(* init *) - -fun init loc = - ProofContext.init - #> #2 o cert_context_statement (SOME loc) [] []; - - -(* print locale *) - -fun print_locale thy show_facts imports body = - let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in - Pretty.big_list "locale elements:" (all_elems - |> (if show_facts then I else filter (fn Notes _ => false | _ => true)) - |> map (Element.pretty_ctxt ctxt) |> filter_out null - |> map Pretty.chunks) - |> Pretty.writeln - end; - - - -(** store results **) - -(* join equations of an id with already accumulated ones *) - -fun join_eqns get_reg id eqns = - let - val eqns' = case get_reg id - of NONE => eqns - | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns') - (* prefer equations from eqns' *) - in ((id, eqns'), eqns') end; - - -(* collect witnesses and equations up to a particular target for a - registration; requires parameters and flattened list of identifiers - instead of recomputing it from the target *) - -fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let - - val thy = ProofContext.theory_of ctxt; - - val ts = map (var_inst_term (impT, imp)) ext_ts; - val (parms, parmTs) = split_list parms; - val parmvTs = map Logic.varifyT parmTs; - val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty; - val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T)) - |> Symtab.make; - val inst = Symtab.make (parms ~~ ts); - - (* instantiate parameter names in ids *) - val ext_inst = Symtab.make (parms ~~ ext_ts); - fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps; - val inst_ids = map (apfst (apsnd ext_inst_names)) ids; - val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids; - val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids; - val eqns = - fold_map (join_eqns (get_local_registration ctxt imprt)) - (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd; - in ((tinst, inst), wits, eqns) end; - - -(* compute and apply morphism *) - -fun name_morph phi_name (lprfx, pprfx) b = - b - |> (if not (Binding.is_empty b) andalso pprfx <> "" - then Binding.add_prefix false pprfx else I) - |> (if not (Binding.is_empty b) - then Binding.add_prefix false lprfx else I) - |> phi_name; - -fun inst_morph thy phi_name param_prfx insts prems eqns export = - let - (* standardise export morphism *) - val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; - val exp_term = TermSubst.zero_var_indexes o Morphism.term export; - (* FIXME sync with exp_fact *) - val exp_typ = Logic.type_map exp_term; - val export' = - Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; - in - Morphism.binding_morphism (name_morph phi_name param_prfx) $> - Element.inst_morphism thy insts $> - Element.satisfy_morphism prems $> - Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> - Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $> - export' - end; - -fun activate_note thy phi_name param_prfx attrib insts prems eqns exp = - (Element.facts_map o Element.morph_ctxt) - (inst_morph thy phi_name param_prfx insts prems eqns exp) - #> Attrib.map_facts attrib; - - -(* public interface to interpretation morphism *) - -fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts = - let - val parms = the_locale thy target |> #params |> map fst; - val ids = flatten (ProofContext.init thy, intern_expr thy) - (([], Symtab.empty), Expr (Locale target)) |> fst |> fst; - val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; - in - inst_morph thy phi_name param_prfx insts prems eqns exp - end; - -(* store instantiations of args for all registered interpretations - of the theory *) - -fun note_thmss_registrations target (kind, args) thy = - let - val parms = the_locale thy target |> #params |> map fst; - val ids = flatten (ProofContext.init thy, intern_expr thy) - (([], Symtab.empty), Expr (Locale target)) |> fst |> fst; - - val regs = get_global_registrations thy target; - (* add args to thy for all registrations *) - - fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy = - let - val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; - val args' = args - |> activate_note thy phi_name param_prfx - (Attrib.attribute_i thy) insts prems eqns exp; - in - thy - |> global_note_qualified kind args' - |> snd - end; - in fold activate regs thy end; - - -(* locale results *) - -fun add_thmss loc kind args ctxt = - let - val (([(_, [Notes args'])], _), ctxt') = - activate_facts true cert_facts - [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt; - val ctxt'' = ctxt' |> ProofContext.theory - (change_locale loc - (fn (axiom, elems, params, decls, regs, intros, dests) => - (axiom, elems @ [(Notes args', stamp ())], - params, decls, regs, intros, dests)) - #> note_thmss_registrations loc args'); - in ctxt'' end; - - -(* declarations *) - -local - -fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi)); - -fun add_decls add loc decl = - ProofContext.theory (change_locale loc - (fn (axiom, elems, params, decls, regs, intros, dests) => - (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #> - add_thmss loc Thm.internalK - [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([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); - -fun declarations_of thy loc = - the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst); - -end; - - - -(** define locales **) - -(* predicate text *) -(* CB: generate locale predicates and delta predicates *) - -local - -(* introN: name of theorems for introduction rules of locale and - delta predicates; - axiomsN: name of theorem set with destruct rules for locale predicates, - also name suffix of delta predicates. *) - -val introN = "intro"; -val axiomsN = "axioms"; - -fun atomize_spec thy ts = - let - val t = Logic.mk_conjunction_balanced ts; - val body = ObjectLogic.atomize_term thy t; - val bodyT = Term.fastype_of body; - in - if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) - else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t)) - end; - -fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => - if length args = n then - Syntax.const "_aprop" $ - Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) - else raise Match); - -(* CB: define one predicate including its intro rule and axioms - - bname: predicate name - - parms: locale parameters - - defs: thms representing substitutions from defines elements - - ts: terms representing locale assumptions (not normalised wrt. defs) - - norm_ts: terms representing locale assumptions (normalised wrt. defs) - - thy: the theory -*) - -fun def_pred bname parms defs ts norm_ts thy = - let - val name = Sign.full_bname thy bname; - - val (body, bodyT, body_eq) = atomize_spec thy norm_ts; - val env = Term.add_free_names body []; - val xs = filter (member (op =) env o #1) parms; - val Ts = map #2 xs; - val extraTs = - (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts []) - |> Library.sort_wrt #1 |> map TFree; - val predT = map Term.itselfT extraTs ---> Ts ---> bodyT; - - val args = map Logic.mk_type extraTs @ map Free xs; - val head = Term.list_comb (Const (name, predT), args); - val statement = ObjectLogic.ensure_propT thy head; - - val ([pred_def], defs_thy) = - thy - |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) - |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd - |> PureThy.add_defs false - [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])]; - val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; - - val cert = Thm.cterm_of defs_thy; - - val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => - MetaSimplifier.rewrite_goals_tac [pred_def] THEN - Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN - Tactic.compose_tac (false, - Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); - - val conjuncts = - (Drule.equal_elim_rule2 OF [body_eq, - MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))]) - |> Conjunction.elim_balanced (length ts); - val axioms = ts ~~ conjuncts |> map (fn (t, ax) => - Element.prove_witness defs_ctxt t - (MetaSimplifier.rewrite_goals_tac defs THEN - Tactic.compose_tac (false, ax, 0) 1)); - in ((statement, intro, axioms), defs_thy) end; - -fun assumes_to_notes (Assumes asms) axms = - fold_map (fn (a, spec) => fn axs => - let val (ps, qs) = chop (length spec) axs - in ((a, [(ps, [])]), qs) end) asms axms - |> apfst (curry Notes Thm.assumptionK) - | assumes_to_notes e axms = (e, axms); - -(* CB: the following two change only "new" elems, these have identifier ("", _). *) - -(* turn Assumes into Notes elements *) - -fun change_assumes_elemss axioms elemss = - let - val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms); - fun change (id as ("", _), es) = - fold_map assumes_to_notes (map satisfy es) - #-> (fn es' => pair (id, es')) - | change e = pair e; - in - fst (fold_map change elemss (map Element.conclude_witness axioms)) - end; - -(* adjust hyps of Notes elements *) - -fun change_elemss_hyps axioms elemss = - let - val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms); - fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es) - | change e = e; - in map change elemss end; - -in - -(* CB: main predicate definition function *) - -fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy = - let - val ((elemss', more_ts), a_elem, a_intro, thy'') = - if null exts then ((elemss, []), [], [], thy) - else - let - val aname = if null ints then pname else pname ^ "_" ^ axiomsN; - val ((statement, intro, axioms), thy') = - thy - |> def_pred aname parms defs exts exts'; - val elemss' = change_assumes_elemss axioms elemss; - val a_elem = [(("", []), - [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])]; - val (_, thy'') = - thy' - |> Sign.add_path aname - |> Sign.no_base_names - |> PureThy.note_thmss Thm.internalK [((Binding.name introN, []), [([intro], [])])] - ||> Sign.restore_naming thy'; - in ((elemss', [statement]), a_elem, [intro], thy'') end; - val (predicate, stmt', elemss'', b_intro, thy'''') = - if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'') - else - let - val ((statement, intro, axioms), thy''') = - thy'' - |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts); - val cstatement = Thm.cterm_of thy''' statement; - val elemss'' = change_elemss_hyps axioms elemss'; - val b_elem = [(("", []), - [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])]; - val (_, thy'''') = - thy''' - |> Sign.add_path pname - |> Sign.no_base_names - |> PureThy.note_thmss Thm.internalK - [((Binding.name introN, []), [([intro], [])]), - ((Binding.name axiomsN, []), - [(map (Drule.standard o Element.conclude_witness) axioms, [])])] - ||> Sign.restore_naming thy'''; - in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end; - in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end; - -end; - - -(* add_locale(_i) *) - -local - -(* turn Defines into Notes elements, accumulate definition terms *) - -fun defines_to_notes is_ext thy (Defines defs) defns = - let - val defs' = map (fn (_, (def, _)) => (Attrib.empty_binding, (def, []))) defs - val notes = map (fn (a, (def, _)) => - (a, [([assume (cterm_of thy def)], [])])) defs - in - (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs']) - end - | defines_to_notes _ _ e defns = (SOME e, defns); - -fun change_defines_elemss thy elemss defns = - let - fun change (id as (n, _), es) defns = - let - val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns - in ((id, map_filter I es'), defns') end - in fold_map change elemss defns end; - -fun gen_add_locale prep_ctxt prep_expr - predicate_name bname raw_imports raw_body thy = - (* predicate_name: "" - locale with predicate named as locale - "name" - locale with predicate named "name" *) - let - val thy_ctxt = ProofContext.init thy; - val name = Sign.full_bname thy bname; - val _ = is_some (get_locale thy name) andalso - error ("Duplicate definition of locale " ^ quote name); - - val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), - text as (parms, ((_, exts'), _), defs)) = - prep_ctxt raw_imports raw_body thy_ctxt; - val elemss = import_elemss @ body_elemss |> - map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE); - - val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\ - List.foldr OldTerm.add_typ_tfrees [] (map snd parms); - val _ = if null extraTs then () - else warning ("Additional type variable(s) in locale specification " ^ quote bname); - - val predicate_name' = case predicate_name of "" => bname | _ => predicate_name; - val (elemss', defns) = change_defines_elemss thy elemss []; - val elemss'' = elemss' @ [(("", []), defns)]; - val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') = - define_preds predicate_name' text elemss'' thy; - val regs = pred_axioms - |> fold_map (fn (id, elems) => fn wts => let - val ts = flat (map_filter (fn (Assumes asms) => - SOME (maps (map #1 o #2) asms) | _ => NONE) elems); - val (wts1, wts2) = chop (length ts) wts; - in ((apsnd (map fst) id, wts1), wts2) end) elemss''' - |> fst - |> map_filter (fn (("", _), _) => NONE | e => SOME e); - fun axiomify axioms elemss = - (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let - val ts = flat (map_filter (fn (Assumes asms) => - SOME (maps (map #1 o #2) asms) | _ => NONE) elems); - val (axs1, axs2) = chop (length ts) axs; - in (axs2, ((id, Assumed axs1), elems)) end) - |> snd; - val ((_, facts), ctxt) = activate_facts true (K I) - (axiomify pred_axioms elemss''') (ProofContext.init thy'); - val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt; - val export = Thm.close_derivation o Goal.norm_result o - singleton (ProofContext.export view_ctxt thy_ctxt); - val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); - val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss'''); - val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems'; - val axs' = map (Element.assume_witness thy') stmt'; - val loc_ctxt = thy' - |> Sign.add_path bname - |> Sign.no_base_names - |> PureThy.note_thmss Thm.assumptionK facts' |> snd - |> Sign.restore_naming thy' - |> register_locale bname {axiom = axs', - elems = map (fn e => (e, stamp ())) elems'', - params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), - decls = ([], []), - regs = regs, - intros = intros, - dests = map Element.conclude_witness pred_axioms} - |> init name; - in (name, loc_ctxt) end; - -in - -val add_locale = gen_add_locale cert_context (K I); -val add_locale_cmd = gen_add_locale read_context intern_expr ""; - -end; - -val _ = Context.>> (Context.map_theory - (add_locale "" "var" empty [Fixes [(Binding.name (Name.internal "x"), NONE, NoSyn)]] #> - snd #> ProofContext.theory_of #> - add_locale "" "struct" empty [Fixes [(Binding.name (Name.internal "S"), NONE, Structure)]] #> - snd #> ProofContext.theory_of)); - - - - -(** Normalisation of locale statements --- - discharges goals implied by interpretations **) - -local - -fun locale_assm_intros thy = - Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros)) - (#2 (LocalesData.get thy)) []; -fun locale_base_intros thy = - Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros)) - (#2 (LocalesData.get thy)) []; - -fun all_witnesses ctxt = - let - val thy = ProofContext.theory_of ctxt; - fun get registrations = Symtab.fold (fn (_, regs) => fn thms => - (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) => - map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms) - registrations []; - in get (RegistrationsData.get (Context.Proof ctxt)) end; - -in - -fun intro_locales_tac eager ctxt facts st = - let - val wits = all_witnesses ctxt; - val thy = ProofContext.theory_of ctxt; - val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []); - in - Method.intros_tac (wits @ intros) facts st - end; - -end; - - -(** Interpretation commands **) - -local - -(* extract proof obligations (assms and defs) from elements *) - -fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems) - | extract_asms_elems ((id, Derived _), _) = (id, []); - - -(* activate instantiated facts in theory or context *) - -fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn - phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt = - let - val ctxt = mk_ctxt thy_ctxt; - fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt); - fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt); - - val (all_propss, eq_props) = chop (length all_elemss) propss; - val (all_thmss, eq_thms) = chop (length all_elemss) thmss; - - (* Filter out fragments already registered. *) - - val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) => - test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss)))); - val (new_pss, ys) = split_list xs; - val (new_propss, new_thmss) = split_list ys; - - val thy_ctxt' = thy_ctxt - (* add registrations *) - |> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp)) - new_elemss new_pss - (* add witnesses of Assumed elements (only those generate proof obligations) *) - |> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss - (* add equations *) - |> fold2 (fn (id, _) => fold (add_eqn id)) eq_props - ((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o - Element.conclude_witness) eq_thms); - - val prems = flat (map_filter - (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id) - | ((_, Derived _), _) => NONE) all_elemss); - - val thy_ctxt'' = thy_ctxt' - (* add witnesses of Derived elements *) - |> fold (fn (id, thms) => fold - (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms) - (map_filter (fn ((_, Assumed _), _) => NONE - | ((id, Derived thms), _) => SOME (id, thms)) new_elemss) - - fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt = - let - val ctxt = mk_ctxt thy_ctxt; - val thy = ProofContext.theory_of ctxt; - val facts' = facts - |> activate_note thy phi_name param_prfx - (attrib thy_ctxt) insts prems eqns exp; - in - thy_ctxt - |> note kind facts' - |> snd - end - | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt; - - fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt = - let - val ctxt = mk_ctxt thy_ctxt; - val thy = ProofContext.theory_of ctxt; - val {params, elems, ...} = the_locale thy loc; - val parms = map fst params; - val param_prfx = param_prefix loc ps; - val ids = flatten (ProofContext.init thy, intern_expr thy) - (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst; - val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts; - in - thy_ctxt - |> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems - end; - - in - thy_ctxt'' - (* add equations as lemmas to context *) - |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK) - ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])])) - (unflat eq_thms eq_attns) eq_thms - (* add interpreted facts *) - |> fold2 activate_elems new_elemss new_pss - end; - -fun global_activate_facts_elemss x = gen_activate_facts_elemss - ProofContext.init - global_note_qualified - Attrib.attribute_i - put_global_registration - add_global_witness - add_global_equation - x; - -fun local_activate_facts_elemss x = gen_activate_facts_elemss - I - local_note_qualified - (Attrib.attribute_i o ProofContext.theory_of) - put_local_registration - add_local_witness - add_local_equation - x; - -fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) = - let - (* parameters *) - val (parm_names, parm_types) = parms |> split_list - ||> map (TypeInfer.paramify_vars o Logic.varifyT); - val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar); - val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst; - - (* parameter instantiations *) - val d = length parms - length insts; - val insts = - if d < 0 then error "More arguments than parameters in instantiation." - else insts @ replicate d NONE; - val (given_ps, given_insts) = - ((parm_names ~~ parm_types) ~~ insts) |> map_filter - (fn (_, NONE) => NONE - | ((n, T), SOME inst) => SOME ((n, T), inst)) - |> split_list; - val (given_parm_names, given_parm_types) = given_ps |> split_list; - - (* parse insts / eqns *) - val given_insts' = map (parse_term ctxt) given_insts; - val eqns' = map (parse_prop ctxt) eqns; - - (* type inference and contexts *) - val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns'; - val res = Syntax.check_terms ctxt arg; - val ctxt' = ctxt |> fold Variable.auto_fixes res; - - (* instantiation *) - val (type_parms'', res') = chop (length type_parms) res; - val (given_insts'', eqns'') = chop (length given_insts) res'; - val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); - val inst = Symtab.make (given_parm_names ~~ given_insts''); - - (* export from eigencontext *) - val export = Variable.export_morphism ctxt' ctxt; - - (* import, its inverse *) - val domT = fold Term.add_tfrees res [] |> map TFree; - val importT = domT |> map (fn x => (Morphism.typ export x, x)) - |> map_filter (fn (TFree _, _) => NONE (* fixed point of export *) - | (TVar y, x) => SOME (fst y, x) - | _ => error "internal: illegal export in interpretation") - |> Vartab.make; - val dom = fold Term.add_frees res [] |> map Free; - val imprt = dom |> map (fn x => (Morphism.term export x, x)) - |> map_filter (fn (Free _, _) => NONE (* fixed point of export *) - | (Var y, x) => SOME (fst y, x) - | _ => error "internal: illegal export in interpretation") - |> Vartab.make; - in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end; - -val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop; -val check_instantiations = prep_instantiations (K I) (K I); - -fun gen_prep_registration mk_ctxt test_reg activate - prep_attr prep_expr prep_insts - thy_ctxt phi_name raw_expr raw_insts = - let - val ctxt = mk_ctxt thy_ctxt; - val thy = ProofContext.theory_of ctxt; - val ctxt' = ProofContext.init thy; - fun prep_attn attn = (apsnd o map) - (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn; - - val expr = prep_expr thy raw_expr; - - val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty); - val params_ids = make_params_ids (#1 pts); - val raw_params_elemss = make_raw_params_elemss pts; - val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr); - val ((parms, all_elemss, _), (_, (_, defs, _))) = - read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) []; - - (** compute instantiation **) - - (* consistency check: equations need to be stored in a particular locale, - therefore if equations are present locale expression must be a name *) - - val _ = case (expr, snd raw_insts) of - (Locale _, _) => () | (_, []) => () - | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name."; - - (* read or certify instantiation *) - val (raw_insts', raw_eqns) = raw_insts; - val (raw_eq_attns, raw_eqns') = split_list raw_eqns; - val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns'); - val eq_attns = map prep_attn raw_eq_attns; - - (* defined params without given instantiation *) - val not_given = filter_out (Symtab.defined inst1 o fst) parms; - fun add_def (p, pT) inst = - let - val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of - NONE => error ("Instance missing for parameter " ^ quote p) - | SOME (Free (_, T), t) => (t, T); - val d = Element.inst_term (instT, inst) t; - in Symtab.update_new (p, d) inst end; - val inst2 = fold add_def not_given inst1; - val inst_morphism = Element.inst_morphism thy (instT, inst2); - (* Note: insts contain no vars. *) - - (** compute proof obligations **) - - (* restore "small" ids *) - val ids' = map (fn ((n, ps), (_, mode)) => - ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) - ids; - val (_, all_elemss') = chop (length raw_params_elemss) all_elemss - (* instantiate ids and elements *) - val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) => - ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps), - map (fn Int e => Element.morph_ctxt inst_morphism e) elems) - |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode))); - - (* equations *) - val eqn_elems = if null eqns then [] - else [(Library.last_elem inst_elemss |> fst |> fst, eqns)]; - - val propss = map extract_asms_elems inst_elemss @ eqn_elems; - - in - (propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs) - end; - -fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init - test_global_registration - global_activate_facts_elemss mk_ctxt; - -fun gen_prep_local_registration mk_ctxt = gen_prep_registration I - test_local_registration - local_activate_facts_elemss mk_ctxt; - -val prep_global_registration = gen_prep_global_registration - (K I) (K I) check_instantiations; -val prep_global_registration_cmd = gen_prep_global_registration - Attrib.intern_src intern_expr read_instantiations; - -val prep_local_registration = gen_prep_local_registration - (K I) (K I) check_instantiations; -val prep_local_registration_cmd = gen_prep_local_registration - Attrib.intern_src intern_expr read_instantiations; - -fun prep_registration_in_locale target expr thy = - (* target already in internal form *) - let - val ctxt = ProofContext.init thy; - val ((raw_target_ids, target_syn), _) = flatten (ctxt, I) - (([], Symtab.empty), Expr (Locale target)); - val fixed = the_locale thy target |> #params |> map #1; - val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy) - ((raw_target_ids, target_syn), Expr expr); - val (target_ids, ids) = chop (length raw_target_ids) all_ids; - val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss []; - - (** compute proof obligations **) - - (* restore "small" ids, with mode *) - val ids' = map (apsnd snd) ids; - (* remove Int markers *) - val elemss' = map (fn (_, es) => - map (fn Int e => e) es) elemss - (* extract assumptions and defs *) - val ids_elemss = ids' ~~ elemss'; - val propss = map extract_asms_elems ids_elemss; - - (** activation function: - - add registrations to the target locale - - add induced registrations for all global registrations of - the target, unless already present - - add facts of induced registrations to theory **) - - fun activate thmss thy = - let - val satisfy = Element.satisfy_thm (flat thmss); - val ids_elemss_thmss = ids_elemss ~~ thmss; - val regs = get_global_registrations thy target; - - fun activate_id (((id, Assumed _), _), thms) thy = - thy |> put_registration_in_locale target id - |> fold (add_witness_in_locale target id) thms - | activate_id _ thy = thy; - - fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy = - let - val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts; - val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts)); - val disch = Element.satisfy_thm wits; - val new_elemss = filter (fn (((name, ps), _), _) => - not (test_global_registration thy (name, inst_parms ps))) (ids_elemss); - fun activate_assumed_id (((_, Derived _), _), _) thy = thy - | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let - val ps' = inst_parms ps; - in - if test_global_registration thy (name, ps') - then thy - else thy - |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp) - |> fold (fn witn => fn thy => add_global_witness (name, ps') - (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms - end; - - fun activate_derived_id ((_, Assumed _), _) thy = thy - | activate_derived_id (((name, ps), Derived ths), _) thy = let - val ps' = inst_parms ps; - in - if test_global_registration thy (name, ps') - then thy - else thy - |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp) - |> fold (fn witn => fn thy => add_global_witness (name, ps') - (witn |> Element.map_witness (fn (t, th) => (* FIXME *) - (Element.inst_term insts t, - disch (Element.inst_thm thy insts (satisfy th))))) thy) ths - end; - - fun activate_elem (loc, ps) (Notes (kind, facts)) thy = - let - val att_morphism = - Morphism.binding_morphism (name_morph phi_name param_prfx) $> - Morphism.thm_morphism satisfy $> - Element.inst_morphism thy insts $> - Morphism.thm_morphism disch; - val facts' = facts - |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism) - |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy) - |> (map o apfst o apfst) (name_morph phi_name param_prfx); - in - thy - |> global_note_qualified kind facts' - |> snd - end - | activate_elem _ _ thy = thy; - - fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy; - - in thy |> fold activate_assumed_id ids_elemss_thmss - |> fold activate_derived_id ids_elemss - |> fold activate_elems new_elemss end; - in - thy |> fold activate_id ids_elemss_thmss - |> fold activate_reg regs - end; - - in (propss, activate) end; - -fun prep_propp propss = propss |> map (fn (_, props) => - map (rpair [] o Element.mark_witness) props); - -fun prep_result propps thmss = - ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss); - -fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy = - let - val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts; - fun after_qed' results = - ProofContext.theory (activate (prep_result propss results)) - #> after_qed; - in - thy - |> ProofContext.init - |> Proof.theorem_i NONE after_qed' (prep_propp propss) - |> Element.refine_witness - |> Seq.hd - |> pair morphs - end; - -fun gen_interpret prep_registration after_qed name_morph expr insts int state = - let - val _ = Proof.assert_forward_or_chain state; - val ctxt = Proof.context_of state; - val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts; - fun after_qed' results = - Proof.map_context (K (ctxt |> activate (prep_result propss results))) - #> Proof.put_facts NONE - #> after_qed; - in - state - |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i - "interpret" NONE after_qed' (map (pair (Binding.empty, [])) (prep_propp propss)) - |> Element.refine_witness |> Seq.hd - |> pair morphs - end; - -fun standard_name_morph interp_prfx b = - if Binding.is_empty b then b - else Binding.map_prefix (fn ((lprfx, _) :: pprfx) => - fold (Binding.add_prefix false o fst) pprfx - #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx - #> Binding.add_prefix false lprfx - ) b; - -in - -val interpretation = gen_interpretation prep_global_registration; -fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd - I (standard_name_morph interp_prfx); - -fun interpretation_in_locale after_qed (raw_target, expr) thy = - let - val target = intern thy raw_target; - val (propss, activate) = prep_registration_in_locale target expr thy; - val raw_propp = prep_propp propss; - - val (_, _, goal_ctxt, propp) = thy - |> ProofContext.init - |> cert_context_statement (SOME target) [] raw_propp; - - fun after_qed' results = - ProofContext.theory (activate (prep_result propss results)) - #> after_qed; - in - goal_ctxt - |> Proof.theorem_i NONE after_qed' propp - |> Element.refine_witness |> Seq.hd - end; - -val interpret = gen_interpret prep_local_registration; -fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd - I (standard_name_morph interp_prfx); - -end; - -end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/outer_parse.ML Wed Jan 21 16:51:45 2009 +0100 @@ -61,12 +61,12 @@ val list: 'a parser -> 'a list parser val list1: 'a parser -> 'a list parser val name: bstring parser - val binding: Binding.T parser + val binding: binding parser val xname: xstring parser val text: string parser val path: Path.T parser val parname: string parser - val parbinding: Binding.T parser + val parbinding: binding parser val sort: string parser val arity: (string * string list * string) parser val multi_arity: (string list * string list * string) parser @@ -81,11 +81,11 @@ val opt_mixfix': mixfix parser val where_: string parser val const: (string * string * mixfix) parser - val params: (Binding.T * string option) list parser - val simple_fixes: (Binding.T * string option) list parser - val fixes: (Binding.T * string option * mixfix) list parser - val for_fixes: (Binding.T * string option * mixfix) list parser - val for_simple_fixes: (Binding.T * string option) list parser + val params: (binding * string option) list parser + val simple_fixes: (binding * string option) list parser + val fixes: (binding * string option * mixfix) list parser + val for_fixes: (binding * string option * mixfix) list parser + val for_simple_fixes: (binding * string option) list parser val ML_source: (SymbolPos.text * Position.T) parser val doc_source: (SymbolPos.text * Position.T) parser val term_group: string parser diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/overloading.ML Wed Jan 21 16:51:45 2009 +0100 @@ -134,8 +134,8 @@ fun declare c_ty = pair (Const c_ty); -fun define checked name (c, t) = - Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t)); +fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name, + Logic.mk_equals (Const (c, Term.fastype_of t), t)); (* target *) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/proof.ML Wed Jan 21 16:51:45 2009 +0100 @@ -43,27 +43,27 @@ val match_bind_i: (term list * term) list -> state -> state val let_bind: (string list * string) list -> state -> state val let_bind_i: (term list * term) list -> state -> state - val fix: (Binding.T * string option * mixfix) list -> state -> state - val fix_i: (Binding.T * typ option * mixfix) list -> state -> state + val fix: (binding * string option * mixfix) list -> state -> state + val fix_i: (binding * typ option * mixfix) list -> state -> state val assm: Assumption.export -> (Attrib.binding * (string * string list) list) list -> state -> state val assm_i: Assumption.export -> - ((Binding.T * attribute list) * (term * term list) list) list -> state -> state + ((binding * attribute list) * (term * term list) list) list -> state -> state val assume: (Attrib.binding * (string * string list) list) list -> state -> state - val assume_i: ((Binding.T * attribute list) * (term * term list) list) list -> + val assume_i: ((binding * attribute list) * (term * term list) list) list -> state -> state val presume: (Attrib.binding * (string * string list) list) list -> state -> state - val presume_i: ((Binding.T * attribute list) * (term * term list) list) list -> + val presume_i: ((binding * attribute list) * (term * term list) list) list -> state -> state - val def: (Attrib.binding * ((Binding.T * mixfix) * (string * string list))) list -> + val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state - val def_i: ((Binding.T * attribute list) * - ((Binding.T * mixfix) * (term * term list))) list -> state -> state + val def_i: ((binding * attribute list) * + ((binding * mixfix) * (term * term list))) list -> state -> state val chain: state -> state val chain_facts: thm list -> state -> state val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state - val note_thmss_i: ((Binding.T * attribute list) * + val note_thmss_i: ((binding * attribute list) * (thm list * attribute list) list) list -> state -> state val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state val from_thmss_i: ((thm list * attribute list) list) list -> state -> state @@ -87,7 +87,7 @@ (theory -> 'a -> attribute) -> (context * 'b list -> context * (term list list * (context -> context))) -> string -> Method.text option -> (thm list list -> state -> state) -> - ((Binding.T * 'a list) * 'b) list -> state -> state + ((binding * 'a list) * 'b) list -> state -> state val local_qed: Method.text option * bool -> state -> state val theorem: Method.text option -> (thm list list -> context -> context) -> (string * string list) list list -> context -> state @@ -107,11 +107,11 @@ val have: Method.text option -> (thm list list -> state -> state) -> (Attrib.binding * (string * string list) list) list -> bool -> state -> state val have_i: Method.text option -> (thm list list -> state -> state) -> - ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state + ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state val show: Method.text option -> (thm list list -> state -> state) -> (Attrib.binding * (string * string list) list) list -> bool -> state -> state val show_i: Method.text option -> (thm list list -> state -> state) -> - ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state + ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state val schematic_goal: state -> bool val is_relevant: state -> bool val local_future_proof: (state -> ('a * state) Future.future) -> diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Jan 21 16:51:45 2009 +0100 @@ -23,7 +23,7 @@ val abbrev_mode: Proof.context -> bool val set_stmt: bool -> Proof.context -> Proof.context val naming_of: Proof.context -> NameSpace.naming - val full_name: Proof.context -> Binding.T -> string + val full_name: Proof.context -> binding -> string val full_bname: Proof.context -> bstring -> string val consts_of: Proof.context -> Consts.T val const_syntax_name: Proof.context -> string -> string @@ -105,27 +105,27 @@ val restore_naming: Proof.context -> Proof.context -> Proof.context val reset_naming: Proof.context -> Proof.context val note_thmss: string -> - ((Binding.T * attribute list) * (Facts.ref * attribute list) list) list -> + ((binding * attribute list) * (Facts.ref * attribute list) list) list -> Proof.context -> (string * thm list) list * Proof.context val note_thmss_i: string -> - ((Binding.T * attribute list) * (thm list * attribute list) list) list -> + ((binding * attribute list) * (thm list * attribute list) list) list -> Proof.context -> (string * thm list) list * Proof.context val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context - val read_vars: (Binding.T * string option * mixfix) list -> Proof.context -> - (Binding.T * typ option * mixfix) list * Proof.context - val cert_vars: (Binding.T * typ option * mixfix) list -> Proof.context -> - (Binding.T * typ option * mixfix) list * Proof.context - val add_fixes: (Binding.T * string option * mixfix) list -> + val read_vars: (binding * string option * mixfix) list -> Proof.context -> + (binding * typ option * mixfix) list * Proof.context + val cert_vars: (binding * typ option * mixfix) list -> Proof.context -> + (binding * typ option * mixfix) list * Proof.context + val add_fixes: (binding * string option * mixfix) list -> Proof.context -> string list * Proof.context - val add_fixes_i: (Binding.T * typ option * mixfix) list -> + val add_fixes_i: (binding * typ option * mixfix) list -> Proof.context -> string list * Proof.context val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a) val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context val add_assms: Assumption.export -> - ((Binding.T * attribute list) * (string * string list) list) list -> + ((binding * attribute list) * (string * string list) list) list -> Proof.context -> (string * thm list) list * Proof.context val add_assms_i: Assumption.export -> - ((Binding.T * attribute list) * (term * term list) list) list -> + ((binding * attribute list) * (term * term list) list) list -> Proof.context -> (string * thm list) list * Proof.context val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context @@ -135,7 +135,7 @@ Context.generic -> Context.generic val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> Properties.T -> - Binding.T * term -> Proof.context -> (term * term) * Proof.context + binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context val verbose: bool ref val setmp_verbose: ('a -> 'b) -> 'a -> 'b diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/spec_parse.ML --- a/src/Pure/Isar/spec_parse.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/spec_parse.ML Wed Jan 21 16:51:45 2009 +0100 @@ -15,24 +15,23 @@ val opt_thm_name: string -> Attrib.binding parser val spec: (Attrib.binding * string list) parser val named_spec: (Attrib.binding * string list) parser - val spec_name: ((Binding.T * string) * Attrib.src list) parser - val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser + val spec_name: ((binding * string) * Attrib.src list) parser + val spec_opt_name: ((binding * string) * Attrib.src list) parser val xthm: (Facts.ref * Attrib.src list) parser val xthms1: (Facts.ref * Attrib.src list) list parser val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser val locale_mixfix: mixfix parser - val locale_fixes: (Binding.T * string option * mixfix) list parser + val locale_fixes: (binding * string option * mixfix) list parser val locale_insts: (string option list * (Attrib.binding * string) list) parser val class_expr: string list parser - val locale_expr: Old_Locale.expr parser - val locale_expression: Expression.expression parser + val locale_expression: Expression.expression parser val locale_keyword: string parser val context_element: Element.context parser val statement: (Attrib.binding * (string * string list) list) list parser val general_statement: (Element.context list * Element.statement) parser val statement_keyword: string parser val specification: - (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser + (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser end; structure SpecParse: SPEC_PARSE = @@ -115,13 +114,6 @@ val class_expr = plus1_unless locale_keyword P.xname; -val locale_expr = - let - fun expr2 x = (P.xname >> Old_Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x - and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Old_Locale.Rename || expr2) x - and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Old_Locale.Merge es)) x; - in expr0 end; - val locale_expression = let fun expr2 x = P.xname x; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/specification.ML Wed Jan 21 16:51:45 2009 +0100 @@ -9,33 +9,33 @@ signature SPECIFICATION = sig val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit - val check_specification: (Binding.T * typ option * mixfix) list -> + val check_specification: (binding * typ option * mixfix) list -> (Attrib.binding * term list) list list -> Proof.context -> - (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context - val read_specification: (Binding.T * string option * mixfix) list -> + (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context + val read_specification: (binding * string option * mixfix) list -> (Attrib.binding * string list) list list -> Proof.context -> - (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context - val check_free_specification: (Binding.T * typ option * mixfix) list -> + (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context + val check_free_specification: (binding * typ option * mixfix) list -> (Attrib.binding * term list) list -> Proof.context -> - (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context - val read_free_specification: (Binding.T * string option * mixfix) list -> + (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context + val read_free_specification: (binding * string option * mixfix) list -> (Attrib.binding * string list) list -> Proof.context -> - (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context - val axiomatization: (Binding.T * typ option * mixfix) list -> + (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context + val axiomatization: (binding * typ option * mixfix) list -> (Attrib.binding * term list) list -> theory -> (term list * (string * thm list) list) * theory - val axiomatization_cmd: (Binding.T * string option * mixfix) list -> + val axiomatization_cmd: (binding * string option * mixfix) list -> (Attrib.binding * string list) list -> theory -> (term list * (string * thm list) list) * theory val definition: - (Binding.T * typ option * mixfix) option * (Attrib.binding * term) -> + (binding * typ option * mixfix) option * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val definition_cmd: - (Binding.T * string option * mixfix) option * (Attrib.binding * string) -> + (binding * string option * mixfix) option * (Attrib.binding * string) -> local_theory -> (term * (string * thm)) * local_theory - val abbreviation: Syntax.mode -> (Binding.T * typ option * mixfix) option * term -> + val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term -> local_theory -> local_theory - val abbreviation_cmd: Syntax.mode -> (Binding.T * string option * mixfix) option * string -> + val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string -> local_theory -> local_theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory @@ -149,7 +149,8 @@ (*axioms*) val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) => - fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props)) + fold_map Thm.add_axiom + ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props))) #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs; val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Isar/theory_target.ML Wed Jan 21 16:51:45 2009 +0100 @@ -6,7 +6,7 @@ signature THEORY_TARGET = sig - val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool, + val peek: local_theory -> {target: string, is_locale: bool, is_class: bool, instantiation: string list * (string * sort) list * sort, overloading: (string * (string * typ) * bool) list} val init: string option -> theory -> local_theory @@ -21,34 +21,17 @@ structure TheoryTarget: THEORY_TARGET = struct -(* new locales *) - -fun locale_extern new_locale x = - if new_locale then Locale.extern x else Old_Locale.extern x; -fun locale_add_type_syntax new_locale x = - if new_locale then Locale.add_type_syntax x else Old_Locale.add_type_syntax x; -fun locale_add_term_syntax new_locale x = - if new_locale then Locale.add_term_syntax x else Old_Locale.add_term_syntax x; -fun locale_add_declaration new_locale x = - if new_locale then Locale.add_declaration x else Old_Locale.add_declaration x; -fun locale_add_thmss new_locale x = - if new_locale then Locale.add_thmss x else Old_Locale.add_thmss x; -fun locale_init new_locale x = - if new_locale then Locale.init x else Old_Locale.init x; -fun locale_intern new_locale x = - if new_locale then Locale.intern x else Old_Locale.intern x; - (* context data *) -datatype target = Target of {target: string, new_locale: bool, is_locale: bool, +datatype target = Target of {target: string, is_locale: bool, is_class: bool, instantiation: string list * (string * sort) list * sort, overloading: (string * (string * typ) * bool) list}; -fun make_target target new_locale is_locale is_class instantiation overloading = - Target {target = target, new_locale = new_locale, is_locale = is_locale, +fun make_target target is_locale is_class instantiation overloading = + Target {target = target, is_locale = is_locale, is_class = is_class, instantiation = instantiation, overloading = overloading}; -val global_target = make_target "" false false false ([], [], []) []; +val global_target = make_target "" false false ([], [], []) []; structure Data = ProofDataFun ( @@ -64,7 +47,7 @@ fun pretty_thy ctxt target is_locale is_class = let val thy = ProofContext.theory_of ctxt; - val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target; + val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target; val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) @@ -89,7 +72,7 @@ (* target declarations *) -fun target_decl add (Target {target, new_locale, ...}) d lthy = +fun target_decl add (Target {target, ...}) d lthy = let val d' = Morphism.transform (LocalTheory.target_morphism lthy) d; val d0 = Morphism.form d'; @@ -100,12 +83,12 @@ |> LocalTheory.target (Context.proof_map d0) else lthy - |> LocalTheory.target (add new_locale target d') + |> LocalTheory.target (add target d') end; -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 type_syntax = target_decl Locale.add_type_syntax; +val term_syntax = target_decl Locale.add_term_syntax; +val declaration = target_decl Locale.add_declaration; fun class_target (Target {target, ...}) f = LocalTheory.raw_theory f #> @@ -166,7 +149,7 @@ |> ProofContext.note_thmss_i kind facts ||> ProofContext.restore_naming ctxt; -fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy = +fun notes (Target {target, is_locale, ...}) kind facts lthy = let val thy = ProofContext.theory_of lthy; val facts' = facts @@ -185,7 +168,7 @@ #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd #> Sign.restore_naming thy) |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd) - |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts) + |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts) |> note_local kind local_facts end; @@ -313,7 +296,7 @@ (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs)) | NONE => if is_none (Class_Target.instantiation_param lthy c) - then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq)) + then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq)) else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs))); val (global_def, lthy3) = lthy2 |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs')); @@ -335,13 +318,13 @@ fun init_target _ NONE = global_target | init_target thy (SOME target) = make_target target (Locale.defined thy (Locale.intern thy target)) - true (Class_Target.is_class thy target) ([], [], []) []; + (Class_Target.is_class thy target) ([], [], []) []; -fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) = +fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) = if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation else if not (null overloading) then Overloading.init overloading else if not is_locale then ProofContext.init - else if not is_class then locale_init new_locale target + else if not is_class then Locale.init target else Class_Target.init target; fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = @@ -375,7 +358,7 @@ val ctxt = ProofContext.init thy; val ops = raw_ops |> map (fn (name, const, checked) => (name, Term.dest_Const (prep_const ctxt const), checked)); - in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end; + in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end; in @@ -383,10 +366,9 @@ fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt; fun context "-" thy = init NONE thy - | context target thy = init (SOME (locale_intern - (Locale.defined thy (Locale.intern thy target)) thy target)) thy; + | context target thy = init (SOME (Locale.intern thy target)) thy; -fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []); +fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []); fun instantiation_cmd raw_arities thy = instantiation (read_multi_arity thy raw_arities) thy; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/ML/ml_context.ML Wed Jan 21 16:51:45 2009 +0100 @@ -126,7 +126,8 @@ fun ml_store sel (name, ths) = let - val ths' = Context.>>> (Context.map_theory_result (PureThy.store_thms (name, ths))); + val ths' = Context.>>> (Context.map_theory_result + (PureThy.store_thms (Binding.name name, ths))); val _ = if name = "" then () else if not (ML_Syntax.is_identifier name) then diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Wed Jan 21 16:51:45 2009 +0100 @@ -733,11 +733,11 @@ val (def_thms, thy') = if t = nullt then ([], thy) else thy |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] - |> PureThy.add_defs false [((extr_name s vs ^ "_def", + |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"), Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])] in thy' - |> PureThy.store_thm (corr_name s vs, + |> PureThy.store_thm (Binding.name (corr_name s vs), Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop)) (Thm.forall_elim_var 0) (forall_intr_frees (ProofChecker.thm_of_proof thy' diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Tools/ROOT.ML Wed Jan 21 16:51:45 2009 +0100 @@ -9,8 +9,5 @@ (*basic XML support*) use "xml_syntax.ML"; -(*derived theory and proof elements*) -use "invoke.ML"; - (*quickcheck needed here because of pg preferences*) use "../../Tools/quickcheck.ML" diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Tools/invoke.ML --- a/src/Pure/Tools/invoke.ML Tue Jan 20 19:09:19 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,127 +0,0 @@ -(* Title: Pure/Tools/invoke.ML - Author: Makarius - -Schematic invocation of locale expression in proof context. -*) - -signature INVOKE = -sig - val invoke: string * Attrib.src list -> Old_Locale.expr -> string option list -> - (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state - val invoke_i: string * attribute list -> Old_Locale.expr -> term option list -> - (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state -end; - -structure Invoke: INVOKE = -struct - - -(* invoke *) - -local - -fun gen_invoke prep_att prep_expr parse_term add_fixes - (prfx, raw_atts) raw_expr raw_insts fixes int state = - let - val thy = Proof.theory_of state; - val _ = Proof.assert_forward_or_chain state; - val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; - - val more_atts = map (prep_att thy) raw_atts; - val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy); - - val prems = maps Element.prems_of elems; - val params = maps Element.params_of elems; - val types = rev (fold Term.add_tfrees prems (fold (Term.add_tfreesT o #2) params [])); - - val prems' = map Logic.varify prems; - val params' = map (Logic.varify o Free) params; - val types' = map (Logic.varifyT o TFree) types; - - val state' = state - |> Proof.enter_forward - |> Proof.begin_block - |> Proof.map_context (snd o add_fixes fixes); - val ctxt' = Proof.context_of state'; - - val raw_insts' = zip_options params' raw_insts - handle Library.UnequalLengths => error "Too many instantiations"; - - fun prep_inst (t, u) = - TypeInfer.constrain (TypeInfer.paramify_vars (Term.fastype_of t)) (parse_term ctxt' u); - val insts = map #1 raw_insts' ~~ - Variable.polymorphic ctxt' (Syntax.check_terms ctxt' (map prep_inst raw_insts')); - val inst_rules = - replicate (length types') Drule.termI @ - map (fn t => - (case AList.lookup (op =) insts t of - SOME u => Drule.mk_term (Thm.cterm_of thy u) - | NONE => Drule.termI)) params'; - - val propp = - [((Binding.empty, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'), - ((Binding.empty, []), map (rpair [] o Logic.mk_term) params'), - ((Binding.empty, []), map (rpair [] o Element.mark_witness) prems')]; - fun after_qed results = - Proof.end_block #> - Proof.map_context (fn ctxt => - let - val ([res_types, res_params, res_prems], ctxt'') = - fold_burrow (apfst snd oo Variable.import_thms false) results ctxt'; - - val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types; - val params'' = map (Thm.term_of o Drule.dest_term) res_params; - val inst = Element.morph_ctxt (Element.inst_morphism thy - (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params''))); - val elems' = map inst elems; - val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems; - val notes = - maps (Element.facts_of thy) elems' - |> Element.satisfy_facts prems'' - |> Element.generalize_facts ctxt'' ctxt - |> Attrib.map_facts (Attrib.attribute_i thy) - |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs)); - in - ctxt - |> ProofContext.sticky_prefix prfx - |> ProofContext.qualified_names - |> (snd o ProofContext.note_thmss_i "" notes) - |> ProofContext.restore_naming ctxt - end) #> - Proof.put_facts NONE; - in - state' - |> Proof.chain_facts chain_facts - |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i - "invoke" NONE after_qed propp - |> Element.refine_witness - |> Seq.hd - |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))), - Position.none)) - |> Seq.hd - end; - -in - -fun invoke x = - gen_invoke Attrib.attribute Old_Locale.read_expr Syntax.parse_term ProofContext.add_fixes x; -fun invoke_i x = gen_invoke (K I) Old_Locale.cert_expr (K I) ProofContext.add_fixes_i x; - -end; - - -(* concrete syntax *) - -local structure P = OuterParse and K = OuterKeyword in - -val _ = - OuterSyntax.command "invoke" - "schematic invocation of locale expression in proof context" - (K.tag_proof K.prf_goal) - (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes - >> (fn ((((name, atts), expr), (insts, _)), fixes) => - Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes))); - -end; - -end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/Tools/named_thms.ML --- a/src/Pure/Tools/named_thms.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/Tools/named_thms.ML Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/Tools/named_thms.ML - ID: $Id$ Author: Makarius Named collections of theorems in canonical order. @@ -36,6 +35,6 @@ val setup = Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #> - PureThy.add_thms_dynamic (name, Data.get); + PureThy.add_thms_dynamic (Binding.name name, Data.get); end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/assumption.ML --- a/src/Pure/assumption.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/assumption.ML Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/assumption.ML - ID: $Id$ Author: Makarius Local assumptions, parameterized by export rules. @@ -79,7 +78,7 @@ (* named prems -- legacy feature *) val _ = Context.>> - (Context.map_theory (PureThy.add_thms_dynamic ("prems", + (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems", fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt))); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/axclass.ML Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/axclass.ML - ID: $Id$ Author: Markus Wenzel, TU Muenchen Type classes defined as predicates, associated with a record of @@ -9,7 +8,7 @@ signature AX_CLASS = sig val define_class: bstring * class list -> string list -> - ((Binding.T * attribute list) * term list) list -> theory -> class * theory + ((binding * attribute list) * term list) list -> theory -> class * theory val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory val prove_classrel: class * class -> tactic -> theory -> theory @@ -329,7 +328,8 @@ quote (Syntax.string_of_classrel ctxt [c1, c2])); in thy - |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])] + |> PureThy.add_thms [((Binding.name + (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])] |-> (fn [th'] => add_classrel th') end; @@ -345,7 +345,7 @@ quote (Syntax.string_of_arity ctxt arity)); in thy - |> PureThy.add_thms (map (rpair []) (names ~~ ths)) + |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths)) |-> fold add_arity end; @@ -372,10 +372,10 @@ |> Sign.no_base_names |> Sign.declare_const [] ((Binding.name c', T'), NoSyn) |-> (fn const' as Const (c'', _) => Thm.add_def false true - (Thm.def_name c', Logic.mk_equals (Const (c, T'), const')) + (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const')) #>> Thm.varifyT #-> (fn thm => add_inst_param (c, tyco) (c'', thm) - #> PureThy.add_thm ((c', thm), [Thm.kind_internal]) + #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal]) #> snd #> Sign.restore_naming thy #> pair (Const (c, T)))) @@ -391,7 +391,7 @@ (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name; in thy - |> Thm.add_def false false (name', prop) + |> Thm.add_def false false (Binding.name name', prop) |>> (fn thm => Drule.transitive_thm OF [eq, thm]) end; @@ -469,7 +469,7 @@ val ([def], def_thy) = thy |> Sign.primitive_class (bclass, super) - |> PureThy.add_defs false [((Thm.def_name bconst, class_eq), [])]; + |> PureThy.add_defs false [((Binding.name (Thm.def_name bconst), class_eq), [])]; val (raw_intro, (raw_classrel, raw_axioms)) = split_defined (length conjs) def ||> chop (length super); @@ -515,7 +515,11 @@ val args = prep thy raw_args; val specs = mk args; val names = name args; - in thy |> PureThy.add_axioms (map (rpair []) (names ~~ specs)) |-> fold add end; + in + thy + |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs)) + |-> fold add + end; fun ax_classrel prep = axiomatize (map o prep) (map Logic.mk_classrel) diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/consts.ML --- a/src/Pure/consts.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/consts.ML Wed Jan 21 16:51:45 2009 +0100 @@ -30,10 +30,10 @@ val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) val typargs: T -> string * typ -> typ list val instance: T -> string * typ list -> typ - val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T + val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T val constrain: string * typ option -> T -> T val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T -> - Binding.T * term -> T -> (term * term) * T + binding * term -> T -> (term * term) * T val revert_abbrev: string -> string -> T -> T val hide: bool -> string -> T -> T val empty: T diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/drule.ML Wed Jan 21 16:51:45 2009 +0100 @@ -460,10 +460,10 @@ val read_prop = certify o SimpleSyntax.read_prop; fun store_thm name th = - Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th))); + Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th))); fun store_thm_open name th = - Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th))); + Context.>>> (Context.map_theory_result (PureThy.store_thm_open (Binding.name name, th))); fun store_standard_thm name th = store_thm name (standard th); fun store_standard_thm_open name thm = store_thm_open name (standard' thm); diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/facts.ML --- a/src/Pure/facts.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/facts.ML Wed Jan 21 16:51:45 2009 +0100 @@ -30,9 +30,9 @@ val props: T -> thm list val could_unify: T -> term -> thm list val merge: T * T -> T - val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T - val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T - val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T + val add_global: NameSpace.naming -> binding * thm list -> T -> string * T + val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T + val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T val del: string -> T -> T val hide: bool -> string -> T -> T end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/more_thm.ML Wed Jan 21 16:51:45 2009 +0100 @@ -38,8 +38,8 @@ val forall_elim_vars: int -> thm -> thm val unvarify: thm -> thm val close_derivation: thm -> thm - val add_axiom: bstring * term -> theory -> thm * theory - val add_def: bool -> bool -> bstring * term -> theory -> thm * theory + val add_axiom: binding * term -> theory -> thm * theory + val add_def: bool -> bool -> binding * term -> theory -> thm * theory val rule_attribute: (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val theory_attributes: attribute list -> theory * thm -> theory * thm @@ -276,14 +276,15 @@ (** specification primitives **) -fun add_axiom (name, prop) thy = +fun add_axiom (b, prop) thy = let - val name' = if name = "" then "axiom_" ^ serial_string () else name; - val thy' = thy |> Theory.add_axioms_i [(name', prop)]; - val axm = unvarify (Thm.axiom thy' (Sign.full_bname thy' name')); + val b' = if Binding.is_empty b + then Binding.name ("axiom_" ^ serial_string ()) else b; + val thy' = thy |> Theory.add_axioms_i [(b', prop)]; + val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b')); in (axm, thy') end; -fun add_def unchecked overloaded (name, prop) thy = +fun add_def unchecked overloaded (b, prop) thy = let val tfrees = rev (map TFree (Term.add_tfrees prop [])); val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees)); @@ -291,8 +292,8 @@ val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees); val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop; - val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy; - val axm' = Thm.axiom thy' (Sign.full_bname thy' name); + val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy; + val axm' = Thm.axiom thy' (Sign.full_name thy' b); val thm = unvarify (Thm.instantiate (recover_sorts, []) axm'); in (thm, thy') end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/morphism.ML --- a/src/Pure/morphism.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/morphism.ML Wed Jan 21 16:51:45 2009 +0100 @@ -16,21 +16,21 @@ signature MORPHISM = sig include BASIC_MORPHISM - val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix - val binding: morphism -> Binding.T -> Binding.T + val var: morphism -> binding * mixfix -> binding * mixfix + val binding: morphism -> binding -> binding val typ: morphism -> typ -> typ val term: morphism -> term -> term val fact: morphism -> thm list -> thm list val thm: morphism -> thm -> thm val cterm: morphism -> cterm -> cterm val morphism: - {binding: Binding.T -> Binding.T, - var: Binding.T * mixfix -> Binding.T * mixfix, + {binding: binding -> binding, + var: binding * mixfix -> binding * mixfix, typ: typ -> typ, term: term -> term, fact: thm list -> thm list} -> morphism - val binding_morphism: (Binding.T -> Binding.T) -> morphism - val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism + val binding_morphism: (binding -> binding) -> morphism + val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism val typ_morphism: (typ -> typ) -> morphism val term_morphism: (term -> term) -> morphism val fact_morphism: (thm list -> thm list) -> morphism @@ -45,8 +45,8 @@ struct datatype morphism = Morphism of - {binding: Binding.T -> Binding.T, - var: Binding.T * mixfix -> Binding.T * mixfix, + {binding: binding -> binding, + var: binding * mixfix -> binding * mixfix, typ: typ -> typ, term: term -> term, fact: thm list -> thm list}; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/primitive_defs.ML Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/primitive_defs.ML - ID: $Id$ Author: Makarius Primitive definition forms. diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/pure_thy.ML Wed Jan 21 16:51:45 2009 +0100 @@ -24,27 +24,27 @@ val name_thm: bool -> bool -> Position.T -> string -> thm -> thm val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list - val store_thms: bstring * thm list -> theory -> thm list * theory - val store_thm: bstring * thm -> theory -> thm * theory - val store_thm_open: bstring * thm -> theory -> thm * theory - val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory - val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory - val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory - val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory - val note_thmss: string -> ((Binding.T * attribute list) * + val store_thms: binding * thm list -> theory -> thm list * theory + val store_thm: binding * thm -> theory -> thm * theory + val store_thm_open: binding * thm -> theory -> thm * theory + val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory + val add_thm: (binding * thm) * attribute list -> theory -> thm * theory + val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory + val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory + val note_thmss: string -> ((binding * attribute list) * (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory - val note_thmss_grouped: string -> string -> ((Binding.T * attribute list) * + val note_thmss_grouped: string -> string -> ((binding * attribute list) * (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory - val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory + val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory - val add_defs: bool -> ((bstring * term) * attribute list) list -> + val add_defs: bool -> ((binding * term) * attribute list) list -> theory -> thm list * theory - val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list -> + val add_defs_unchecked: bool -> ((binding * term) * attribute list) list -> + theory -> thm list * theory + val add_defs_cmd: bool -> ((bstring * string) * attribute list) list -> theory -> thm list * theory val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list -> theory -> thm list * theory - val add_defs_cmd: bool -> ((bstring * string) * attribute list) list -> - theory -> thm list * theory val old_appl_syntax: theory -> bool val old_appl_syntax_setup: theory -> theory end; @@ -163,21 +163,21 @@ (* store_thm(s) *) -fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none) - (name_thms false true Position.none) I (Binding.name bname, thms); +fun store_thms (b, thms) = enter_thms (name_thms true true Position.none) + (name_thms false true Position.none) I (b, thms); -fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single; +fun store_thm (b, th) = store_thms (b, [th]) #>> the_single; -fun store_thm_open (bname, th) = +fun store_thm_open (b, th) = enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I - (Binding.name bname, [th]) #>> the_single; + (b, [th]) #>> the_single; (* add_thms(s) *) -fun add_thms_atts pre_name ((bname, thms), atts) = +fun add_thms_atts pre_name ((b, thms), atts) = enter_thms pre_name (name_thms false true Position.none) - (foldl_map (Thm.theory_attributes atts)) (Binding.name bname, thms); + (foldl_map (Thm.theory_attributes atts)) (b, thms); fun gen_add_thmss pre_name = fold_map (add_thms_atts pre_name); @@ -192,9 +192,9 @@ (* add_thms_dynamic *) -fun add_thms_dynamic (bname, f) thy = thy +fun add_thms_dynamic (b, f) thy = thy |> (FactsData.map o apfst) - (Facts.add_dynamic (Sign.naming_of thy) (Binding.name bname, f) #> snd); + (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd); (* note_thmss *) @@ -224,21 +224,21 @@ (* store axioms as theorems *) local - fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_bname thy name); + fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b); fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs; - fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy => + fun add_axm prep_b add = fold_map (fn ((b, ax), atts) => fn thy => let - val named_ax = [(name, ax)]; + val named_ax = [(b, ax)]; val thy' = add named_ax thy; - val thm = hd (get_axs thy' named_ax); - in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end); + val thm = hd (get_axs thy' ((map o apfst) prep_b named_ax)); + in apfst hd (gen_add_thms (K I) [((prep_b b, thm), atts)] thy') end); in - val add_defs = add_axm o Theory.add_defs_i false; - val add_defs_unchecked = add_axm o Theory.add_defs_i true; - val add_axioms = add_axm Theory.add_axioms_i; - val add_defs_cmd = add_axm o Theory.add_defs false; - val add_defs_unchecked_cmd = add_axm o Theory.add_defs true; - val add_axioms_cmd = add_axm Theory.add_axioms; + val add_defs = add_axm I o Theory.add_defs_i false; + val add_defs_unchecked = add_axm I o Theory.add_defs_i true; + val add_axioms = add_axm I Theory.add_axioms_i; + val add_defs_cmd = add_axm Binding.name o Theory.add_defs false; + val add_defs_unchecked_cmd = add_axm Binding.name o Theory.add_defs true; + val add_axioms_cmd = add_axm Binding.name Theory.add_axioms; end; @@ -378,16 +378,16 @@ ("sort_constraint", typ "'a itself => prop", NoSyn), ("conjunction", typ "prop => prop => prop", NoSyn)] #> (add_defs false o map Thm.no_attributes) - [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"), - ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), - ("sort_constraint_def", + [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"), + (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), + (Binding.name "sort_constraint_def", prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\ \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"), - ("conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd + (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd #> Sign.hide_const false "Pure.term" #> Sign.hide_const false "Pure.sort_constraint" #> Sign.hide_const false "Pure.conjunction" - #> add_thmss [(("nothing", []), [])] #> snd - #> Theory.add_axioms_i Proofterm.equality_axms)); + #> add_thmss [((Binding.name "nothing", []), [])] #> snd + #> Theory.add_axioms_i ((map o apfst) Binding.name Proofterm.equality_axms))); end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/sign.ML --- a/src/Pure/sign.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/sign.ML Wed Jan 21 16:51:45 2009 +0100 @@ -14,7 +14,7 @@ tsig: Type.tsig, consts: Consts.T} val naming_of: theory -> NameSpace.naming - val full_name: theory -> Binding.T -> string + val full_name: theory -> binding -> string val base_name: string -> bstring val full_bname: theory -> bstring -> string val full_bname_path: theory -> string -> bstring -> string @@ -91,10 +91,10 @@ val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory - val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory + val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory val add_consts: (bstring * string * mixfix) list -> theory -> theory val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory - val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory + val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory val revert_abbrev: string -> string -> theory -> theory val add_const_constraint: string * typ option -> theory -> theory val primitive_class: string * class list -> theory -> theory diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Pure/theory.ML --- a/src/Pure/theory.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Pure/theory.ML Wed Jan 21 16:51:45 2009 +0100 @@ -29,14 +29,14 @@ val at_end: (theory -> theory option) -> theory -> theory val begin_theory: string -> theory list -> theory val end_theory: theory -> theory + val add_axioms_i: (binding * term) list -> theory -> theory val add_axioms: (bstring * string) list -> theory -> theory - val add_axioms_i: (bstring * term) list -> theory -> theory val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory + val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory - val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory + val add_finals_i: bool -> term list -> theory -> theory val add_finals: bool -> string list -> theory -> theory - val add_finals_i: bool -> term list -> theory -> theory - val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory + val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory end structure Theory: THEORY = @@ -157,19 +157,19 @@ fun err_in_axm msg name = cat_error msg ("The error(s) above occurred in axiom " ^ quote name); -fun cert_axm thy (name, raw_tm) = +fun cert_axm thy (b, raw_tm) = let val (t, T, _) = Sign.certify_prop thy raw_tm handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; in Term.no_dummy_patterns t handle TERM (msg, _) => error msg; - (name, Sign.no_vars (Syntax.pp_global thy) t) + (b, Sign.no_vars (Syntax.pp_global thy) t) end; -fun read_axm thy (name, str) = - cert_axm thy (name, Syntax.read_prop_global thy str) - handle ERROR msg => err_in_axm msg name; +fun read_axm thy (bname, str) = + cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str) + handle ERROR msg => err_in_axm msg bname; (* add_axioms(_i) *) @@ -178,15 +178,15 @@ fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms => let - val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms; + val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms; val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms handle Symtab.DUP dup => err_dup_axm dup; in axioms' end); in +val add_axioms_i = gen_add_axioms cert_axm; val add_axioms = gen_add_axioms read_axm; -val add_axioms_i = gen_add_axioms cert_axm; end; @@ -250,16 +250,16 @@ (* check_def *) -fun check_def thy unchecked overloaded (bname, tm) defs = +fun check_def thy unchecked overloaded (b, tm) defs = let val ctxt = ProofContext.init thy; - val name = Sign.full_bname thy bname; + val name = Sign.full_name thy b; val (lhs_const, rhs) = Sign.cert_def ctxt tm; val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs []; val _ = check_overloading thy overloaded lhs_const; in defs |> dependencies thy unchecked true name lhs_const rhs_consts end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block - [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"), + [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)])); @@ -298,8 +298,8 @@ in +val add_finals_i = gen_add_finals (K I); val add_finals = gen_add_finals Syntax.read_term_global; -val add_finals_i = gen_add_finals (K I); end; diff -r bb0f395db245 -r 88ba5e5ac6d8 src/Tools/induct.ML --- a/src/Tools/induct.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/Tools/induct.ML Wed Jan 21 16:51:45 2009 +0100 @@ -50,7 +50,7 @@ val setN: string (*proof methods*) val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic - val add_defs: (Binding.T option * term) option list -> Proof.context -> + val add_defs: (binding option * term) option list -> Proof.context -> (term option list * thm list) * Proof.context val atomize_term: theory -> term -> term val atomize_tac: int -> tactic @@ -62,7 +62,7 @@ val cases_tac: Proof.context -> term option list list -> thm option -> thm list -> int -> cases_tactic val get_inductT: Proof.context -> term option list list -> thm list list - val induct_tac: Proof.context -> (Binding.T option * term) option list list -> + val induct_tac: Proof.context -> (binding option * term) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> cases_tactic val coinduct_tac: Proof.context -> term option list -> term option list -> thm option -> diff -r bb0f395db245 -r 88ba5e5ac6d8 src/ZF/Inductive_ZF.thy --- a/src/ZF/Inductive_ZF.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/ZF/Inductive_ZF.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,4 @@ (* Title: ZF/Inductive_ZF.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge diff -r bb0f395db245 -r 88ba5e5ac6d8 src/ZF/Main_ZF.thy --- a/src/ZF/Main_ZF.thy Tue Jan 20 19:09:19 2009 +0100 +++ b/src/ZF/Main_ZF.thy Wed Jan 21 16:51:45 2009 +0100 @@ -1,5 +1,3 @@ -(*$Id$*) - header{*Theory Main: Everything Except AC*} theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin diff -r bb0f395db245 -r 88ba5e5ac6d8 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/ZF/Tools/datatype_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -247,7 +247,7 @@ if need_recursor then thy |> Sign.add_consts_i [(recursor_base_name, recursor_typ, NoSyn)] - |> (snd o PureThy.add_defs false [Thm.no_attributes recursor_def]) + |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def]) else thy; val (con_defs, thy0) = thy_path @@ -255,7 +255,7 @@ ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)) |> PureThy.add_defs false - (map Thm.no_attributes + (map (Thm.no_attributes o apfst Binding.name) (case_def :: List.concat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) @@ -383,13 +383,13 @@ (*Updating theory components: simprules and datatype info*) (thy1 |> Sign.add_path big_rec_base_name |> PureThy.add_thmss - [(("simps", simps), [Simplifier.simp_add]), - (("", intrs), [Classical.safe_intro NONE]), - (("con_defs", con_defs), []), - (("case_eqns", case_eqns), []), - (("recursor_eqns", recursor_eqns), []), - (("free_iffs", free_iffs), []), - (("free_elims", free_SEs), [])] |> snd + [((Binding.name "simps", simps), [Simplifier.simp_add]), + ((Binding.empty , intrs), [Classical.safe_intro NONE]), + ((Binding.name "con_defs", con_defs), []), + ((Binding.name "case_eqns", case_eqns), []), + ((Binding.name "recursor_eqns", recursor_eqns), []), + ((Binding.name "free_iffs", free_iffs), []), + ((Binding.name "free_elims", free_SEs), [])] |> snd |> DatatypesData.map (Symtab.update (big_rec_name, dt_info)) |> ConstructorsData.map (fold Symtab.update con_pairs) |> Sign.parent_path, diff -r bb0f395db245 -r 88ba5e5ac6d8 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Wed Jan 21 16:51:45 2009 +0100 @@ -158,7 +158,7 @@ in thy |> Sign.add_path (Sign.base_name big_rec_name) - |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd + |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy)) |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy)) |> Sign.parent_path diff -r bb0f395db245 -r 88ba5e5ac6d8 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/ZF/Tools/inductive_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -27,10 +27,10 @@ (*Insert definitions for the recursive sets, which must *already* be declared as constants in parent theory!*) val add_inductive_i: bool -> term list * term -> - ((Binding.T * term) * attribute list) list -> + ((binding * term) * attribute list) list -> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result val add_inductive: string list * string -> - ((Binding.T * string) * Attrib.src list) list -> + ((binding * string) * Attrib.src list) list -> (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result @@ -173,7 +173,7 @@ val (_, thy1) = thy |> Sign.add_path big_rec_base_name - |> PureThy.add_defs false (map Thm.no_attributes axpairs); + |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs); val ctxt1 = ProofContext.init thy1; @@ -510,9 +510,9 @@ val ([induct', mutual_induct'], thy') = thy - |> PureThy.add_thms [((co_prefix ^ "induct", induct), + |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), induct), [case_names, Induct.induct_pred big_rec_name]), - (("mutual_induct", mutual_induct), [case_names])]; + ((Binding.name "mutual_induct", mutual_induct), [case_names])]; in ((thy', induct'), mutual_induct') end; (*of induction_rules*) @@ -522,7 +522,7 @@ if not coind then induction_rules raw_induct thy1 else (thy1 - |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])] + |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])] |> apfst hd |> Library.swap, TrueI) and defs = big_rec_def :: part_rec_defs @@ -531,15 +531,15 @@ thy2 |> IndCases.declare big_rec_name make_cases |> PureThy.add_thms - [(("bnd_mono", bnd_mono), []), - (("dom_subset", dom_subset), []), - (("cases", elim), [case_names, Induct.cases_pred big_rec_name])] + [((Binding.name "bnd_mono", bnd_mono), []), + ((Binding.name "dom_subset", dom_subset), []), + ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])] ||>> (PureThy.add_thmss o map Thm.no_attributes) - [("defs", defs), - ("intros", intrs)]; + [(Binding.name "defs", defs), + (Binding.name "intros", intrs)]; val (intrs'', thy4) = thy3 - |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs) + |> PureThy.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs) ||> Sign.parent_path; in (thy4, diff -r bb0f395db245 -r 88ba5e5ac6d8 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Tue Jan 20 19:09:19 2009 +0100 +++ b/src/ZF/Tools/primrec_package.ML Wed Jan 21 16:51:45 2009 +0100 @@ -8,8 +8,8 @@ signature PRIMREC_PACKAGE = sig - val add_primrec: ((Binding.T * string) * Attrib.src list) list -> theory -> theory * thm list - val add_primrec_i: ((Binding.T * term) * attribute list) list -> theory -> theory * thm list + val add_primrec: ((binding * string) * Attrib.src list) list -> theory -> theory * thm list + val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list end; structure PrimrecPackage : PRIMREC_PACKAGE = @@ -169,7 +169,7 @@ val ([def_thm], thy1) = thy |> Sign.add_path (Sign.base_name fname) - |> (PureThy.add_defs false o map Thm.no_attributes) [def]; + |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)]; val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) val eqn_thms = @@ -179,10 +179,10 @@ val (eqn_thms', thy2) = thy1 - |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts); + |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); val (_, thy3) = thy2 - |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])] + |> PureThy.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])] ||> Sign.parent_path; in (thy3, eqn_thms') end;