src/Pure/Isar/locale.ML
changeset 29441 28d7d7572b81
parent 29392 aa3a30b625d1
child 29502 2cbc80397a17
     1.1 --- a/src/Pure/Isar/locale.ML	Sun Jan 11 14:18:16 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Sun Jan 11 14:18:17 2009 +0100
     1.3 @@ -34,6 +34,7 @@
     1.4    val register_locale: bstring ->
     1.5      (string * sort) list * (Binding.T * typ option * mixfix) list ->
     1.6      term option * term list ->
     1.7 +    thm option * thm option -> thm list ->
     1.8      (declaration * stamp) list * (declaration * stamp) list ->
     1.9      ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
    1.10      ((string * Morphism.morphism) * stamp) list -> theory -> theory
    1.11 @@ -45,6 +46,8 @@
    1.12    (* Specification *)
    1.13    val defined: theory -> string -> bool
    1.14    val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
    1.15 +  val intros_of: theory -> string -> thm option * thm option
    1.16 +  val axioms_of: theory -> string -> thm list
    1.17    val instance_of: theory -> string -> Morphism.morphism -> term list
    1.18    val specification_of: theory -> string -> term option * term list
    1.19    val declarations_of: theory -> string -> declaration list * declaration list
    1.20 @@ -118,6 +121,8 @@
    1.21      (* type and term parameters *)
    1.22    spec: term option * term list,
    1.23      (* assumptions (as a single predicate expression) and defines *)
    1.24 +  intros: thm option * thm option,
    1.25 +  axioms: thm list,
    1.26    (** dynamic part **)
    1.27    decls: (declaration * stamp) list * (declaration * stamp) list,
    1.28      (* type and term syntax declarations *)
    1.29 @@ -127,17 +132,18 @@
    1.30      (* locale dependencies (sublocale relation) *)
    1.31  };
    1.32  
    1.33 -fun mk_locale ((parameters, spec), ((decls, notes), dependencies)) =
    1.34 -  Loc {parameters = parameters, spec = spec, decls = decls,
    1.35 -    notes = notes, dependencies = dependencies};
    1.36 -fun map_locale f (Loc {parameters, spec, decls, notes, dependencies}) =
    1.37 -  mk_locale (f ((parameters, spec), ((decls, notes), dependencies)));
    1.38 -fun merge_locale (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
    1.39 -  Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
    1.40 -    mk_locale ((parameters, spec),
    1.41 -      (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
    1.42 -        merge (eq_snd op =) (notes, notes')),
    1.43 -          merge (eq_snd op =) (dependencies, dependencies')));
    1.44 +fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
    1.45 +  Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
    1.46 +    decls = decls, notes = notes, dependencies = dependencies};
    1.47 +fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
    1.48 +  mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
    1.49 +fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
    1.50 +  notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
    1.51 +    dependencies = dependencies', ...}) = mk_locale
    1.52 +      ((parameters, spec, intros, axioms),
    1.53 +        (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
    1.54 +          merge (eq_snd op =) (notes, notes')),
    1.55 +            merge (eq_snd op =) (dependencies, dependencies')));
    1.56  
    1.57  structure LocalesData = TheoryDataFun
    1.58  (
    1.59 @@ -159,9 +165,9 @@
    1.60   of SOME (Loc loc) => loc
    1.61    | NONE => error ("Unknown locale " ^ quote name);
    1.62  
    1.63 -fun register_locale bname parameters spec decls notes dependencies thy =
    1.64 +fun register_locale bname parameters spec intros axioms decls notes dependencies thy =
    1.65    thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
    1.66 -    mk_locale ((parameters, spec), ((decls, notes), dependencies))) #> snd);
    1.67 +    mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
    1.68  
    1.69  fun change_locale name =
    1.70    LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
    1.71 @@ -175,6 +181,10 @@
    1.72  
    1.73  fun params_of thy = snd o #parameters o the_locale thy;
    1.74  
    1.75 +fun intros_of thy = #intros o the_locale thy;
    1.76 +
    1.77 +fun axioms_of thy = #axioms o the_locale thy;
    1.78 +
    1.79  fun instance_of thy name morph = params_of thy name |>
    1.80    map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
    1.81