--- a/Admin/isatest/settings/at-mac-poly-5.1-para Sat Jan 10 23:56:11 2009 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sun Jan 11 14:22:34 2009 +0100
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 500 --immutable 1500"
+ ML_OPTIONS="--mutable 200 --immutable 1200"
ISABELLE_HOME_USER=~/isabelle-at-mac-poly-e
--- a/src/Pure/Isar/class.ML Sat Jan 10 23:56:11 2009 +0100
+++ b/src/Pure/Isar/class.ML Sun Jan 11 14:22:34 2009 +0100
@@ -7,8 +7,8 @@
signature CLASS =
sig
include CLASS_TARGET
- (*FIXME the split in class_target.ML, theory_target.ML and
- ML is artificial*)
+ (*FIXME the split into class_target.ML, theory_target.ML and
+ class.ML is artificial*)
val class: bstring -> class list -> Element.context_i list
-> theory -> string * local_theory
@@ -45,7 +45,25 @@
|> SOME
end;
-fun calculate_rules thy phi sups base_sort param_map axiom class =
+fun raw_morphism thy class param_map some_axiom =
+ let
+ val ctxt = ProofContext.init thy;
+ val some_wit = case some_axiom
+ of SOME axiom => SOME (Element.prove_witness ctxt
+ (Logic.unvarify (Thm.prop_of axiom))
+ (ALLGOALS (ProofContext.fact_tac [axiom])))
+ | NONE => NONE;
+ val instT = Symtab.empty |> Symtab.update ("'a", TFree ("'a", [class]));
+ val inst = Symtab.make ((map o apsnd) Const param_map);
+ in case some_wit
+ of SOME wit => Element.inst_morphism thy (instT, inst)
+ $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
+ $> Element.satisfy_morphism [wit]
+ | NONE => Element.inst_morphism thy (instT, inst)
+ $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
+ end;
+
+fun calculate_rules thy morph sups base_sort param_map axiom class =
let
fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
(base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
@@ -200,14 +218,13 @@
#-> (fn axiom =>
prove_class_interpretation class inst
(supconsts @ map (pair class o fst o snd) params) (the_list axiom) []
- #-> (fn morphism =>
- `(fn thy => activate_class_morphism thy class inst morphism)
- #-> (fn phi =>
- `(fn thy => calculate_rules thy phi sups base_sort param_map axiom class)
+ #> `(fn thy => raw_morphism thy class param_map axiom)
+ #-> (fn morph =>
+ `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
#-> (fn (assm_intro, of_class) =>
register class sups params base_sort inst
- morphism axiom assm_intro of_class
- #> fold (note_assm_intro class) (the_list assm_intro))))))
+ morph axiom assm_intro of_class
+ #> fold (note_assm_intro class) (the_list assm_intro)))))
|> TheoryTarget.init (SOME class)
|> pair class
end;
--- a/src/Pure/Isar/class_target.ML Sat Jan 10 23:56:11 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Sun Jan 11 14:22:34 2009 +0100
@@ -7,9 +7,8 @@
signature CLASS_TARGET =
sig
(*classes*)
- type raw_morphism = morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list));
val register: class -> class list -> ((string * typ) * (string * typ)) list
- -> sort -> term list -> raw_morphism
+ -> sort -> term list -> morphism
-> thm option -> thm option -> thm -> theory -> theory
val begin: class list -> sort -> Proof.context -> Proof.context
@@ -22,10 +21,8 @@
val intro_classes_tac: thm list -> tactic
val default_intro_tac: Proof.context -> thm list -> tactic
- val activate_class_morphism: theory -> class -> term list
- -> raw_morphism -> morphism
val prove_class_interpretation: class -> term list -> (class * string) list
- -> thm list -> thm list -> theory -> raw_morphism * theory
+ -> thm list -> thm list -> theory -> theory
val prove_subclass_relation: class * class -> thm option -> theory -> theory
val class_prefix: string -> string
@@ -97,19 +94,6 @@
end;
-(** auxiliary **)
-
-val class_prefix = Logic.const_of_class o Sign.base_name;
-
-fun class_name_morphism class =
- Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
-
-type raw_morphism = morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list));
-
-fun activate_class_morphism thy class inst morphism =
- Locale_Layer.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
-
-
(** primitive axclass and instance commands **)
fun axclass_cmd (class, raw_superclasses) raw_specs thy =
@@ -164,8 +148,8 @@
base_sort: sort,
inst: term list
(*canonical interpretation*),
- morphism: Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))
- (*morphism cookie of canonical interpretation*),
+ base_morph: Morphism.morphism
+ (*static part of canonical morphism*),
assm_intro: thm option,
of_class: thm,
axiom: thm option,
@@ -177,21 +161,21 @@
};
fun rep_class_data (ClassData d) = d;
-fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
+fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
(defs, operations)) =
ClassData { consts = consts, base_sort = base_sort, inst = inst,
- morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
+ base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
defs = defs, operations = operations };
-fun map_class_data f (ClassData { consts, base_sort, inst, morphism, assm_intro,
+fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro,
of_class, axiom, defs, operations }) =
- mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
+ mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
(defs, operations)));
fun merge_class_data _ (ClassData { consts = consts,
- base_sort = base_sort, inst = inst, morphism = morphism, assm_intro = assm_intro,
+ base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro,
of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
- ClassData { consts = _, base_sort = _, inst = _, morphism = _, assm_intro = _,
+ ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _,
of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
- mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
+ mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
(Thm.merge_thms (defs1, defs2),
AList.merge (op =) (K true) (operations1, operations2)));
@@ -246,10 +230,19 @@
val { axiom, of_class, ... } = the_class_data thy class
in (axiom, of_class) end;
+val class_prefix = Logic.const_of_class o Sign.base_name;
+
+fun class_binding_morph class =
+ Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
+
fun morphism thy class =
let
- val { inst, morphism, ... } = the_class_data thy class;
- in activate_class_morphism thy class inst morphism end;
+ val { base_morph, defs, ... } = the_class_data thy class;
+ in
+ base_morph
+ $> Morphism.term_morphism (MetaSimplifier.rewrite_term thy defs [])
+ $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule defs)
+ end;
fun print_classes thy =
let
@@ -289,23 +282,23 @@
(* updaters *)
-fun register class superclasses params base_sort inst phi
+fun register class superclasses params base_sort inst morph
axiom assm_intro of_class thy =
let
val operations = map (fn (v_ty as (_, ty), (c, _)) =>
(c, (class, (ty, Free v_ty)))) params;
val add_class = Graph.new_node (class,
mk_class_data (((map o pairself) fst params, base_sort,
- inst, phi, assm_intro, of_class, axiom), ([], operations)))
+ inst, morph, assm_intro, of_class, axiom), ([], operations)))
#> fold (curry Graph.add_edge class) superclasses;
in ClassData.map add_class thy end;
fun register_operation class (c, (t, some_def)) thy =
let
val base_sort = base_sort thy class;
- val prep_typ = map_type_tvar
- (fn (vi as (v, _), sort) => if Name.aT = v
- then TFree (v, base_sort) else TVar (vi, sort));
+ val prep_typ = map_type_tfree
+ (fn (v, sort) => if Name.aT = v
+ then TFree (v, base_sort) else TVar ((v, 0), sort));
val t' = map_types prep_typ t;
val ty' = Term.fastype_of t';
in
@@ -331,9 +324,10 @@
in
thy
|> fold2 add_constraint (map snd consts) no_constraints
- |> Locale_Layer.prove_interpretation tac (class_name_morphism class) (Locale_Layer.Locale class)
+ |> Locale_Layer.prove_interpretation tac (class_binding_morph class) (Locale_Layer.Locale class)
(map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
- ||> fold2 add_constraint (map snd consts) constraints
+ |> snd
+ |> fold2 add_constraint (map snd consts) constraints
end;
fun prove_subclass_relation (sub, sup) some_thm thy =
@@ -444,16 +438,15 @@
let
val prfx = class_prefix class;
val thy' = thy |> Sign.add_path prfx;
- val phi = morphism thy' class;
+ val morph = morphism thy' class;
val inst = the_inst thy' class;
val params = map (apsnd fst o snd) (these_params thy' [class]);
val c' = Sign.full_bname thy' c;
- val dict' = Morphism.term phi dict;
- val dict_def = map_types Logic.unvarifyT dict';
- val ty' = Term.fastype_of dict_def;
+ val dict' = Morphism.term morph dict;
+ val ty' = Term.fastype_of dict';
val ty'' = Type.strip_sorts ty';
- val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
+ val def_eq = Logic.mk_equals (Const (c', ty'), dict');
fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
in
thy'
@@ -462,9 +455,6 @@
|>> Thm.symmetric
||>> get_axiom
|-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
- #> snd
- (*assumption: interpretation cookie does not change
- by adding equations to interpretation*)
#> register_operation class (c', (dict', SOME (Thm.symmetric def')))
#> PureThy.store_thm (c ^ "_raw", def')
#> snd)
@@ -649,9 +639,9 @@
fun prove_instantiation_exit_result f tac x lthy =
let
- val phi = ProofContext.export_morphism lthy
+ val morph = ProofContext.export_morphism lthy
(ProofContext.init (ProofContext.theory_of lthy));
- val y = f phi x;
+ val y = f morph x;
in
lthy
|> prove_instantiation_exit (fn ctxt => tac ctxt y)
--- a/src/Pure/Isar/expression.ML Sat Jan 10 23:56:11 2009 +0100
+++ b/src/Pure/Isar/expression.ML Sun Jan 11 14:22:34 2009 +0100
@@ -12,10 +12,10 @@
type expression = string expr * (Binding.T * string option * mixfix) list;
(* Processing of context statements *)
+ val cert_statement: Element.context_i list -> (term * term list) list list ->
+ Proof.context -> (term * term list) list list * Proof.context;
val read_statement: Element.context list -> (string * string list) list list ->
Proof.context -> (term * term list) list list * Proof.context;
- val cert_statement: Element.context_i list -> (term * term list) list list ->
- Proof.context -> (term * term list) list list * Proof.context;
(* Declaring locales *)
val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
@@ -24,6 +24,9 @@
theory -> string * local_theory;
(* Interpretation *)
+ val cert_goal_expression: expression_i -> Proof.context ->
+ (term list list * (string * morphism) list * morphism) * Proof.context;
+
val sublocale: string -> expression_i -> theory -> Proof.state;
val sublocale_cmd: string -> expression -> theory -> Proof.state;
val interpretation: expression_i -> (Attrib.binding * term) list ->
@@ -740,10 +743,11 @@
map_filter (fn Notes notes => SOME notes | _ => NONE);
val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
+ val axioms = map Element.conclude_witness b_axioms;
val loc_ctxt = thy'
|> Locale.register_locale bname (extraTs, params)
- (asm, rev defs) ([], [])
+ (asm, rev defs) (a_intro, b_intro) axioms ([], [])
(map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev)
|> TheoryTarget.init (SOME name)
|> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
@@ -816,12 +820,54 @@
val ctxt = ProofContext.init thy;
val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt;
-
+
val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+ (*** alternative code -- unclear why it does not work yet ***)
+ fun store_reg ((name, morph), thms) thy =
+ let
+ val thms' = map (Element.morph_witness export') thms;
+ val morph' = morph $> Element.satisfy_morphism thms';
+ in
+ thy
+ |> Locale.add_registration (name, (morph', export))
+ |> pair (name, morph')
+ end;
+
+ fun store_eqns_activate regs [] thy =
+ thy
+ |> fold (fn (name, morph) =>
+ Locale.activate_global_facts (name, morph $> export)) regs
+ | store_eqns_activate regs thms thys =
+ let
+ val thms' = thms |> map (Element.conclude_witness #>
+ Morphism.thm (export' $> export) #>
+ LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+ Drule.abs_def);
+ val eq_morph =
+ Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
+ Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
+ 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')
+ |> 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;
+ (*** alternative code end ***)
+
fun store (Reg (name, morph), thms) (regs, thy) =
let
val thms' = map (Element.morph_witness export') thms;
--- a/src/Pure/Isar/local_defs.ML Sat Jan 10 23:56:11 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Sun Jan 11 14:22:34 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/local_defs.ML
- ID: $Id$
Author: Makarius
Local definitions.
--- a/src/Pure/Isar/locale.ML Sat Jan 10 23:56:11 2009 +0100
+++ b/src/Pure/Isar/locale.ML Sun Jan 11 14:22:34 2009 +0100
@@ -34,6 +34,7 @@
val register_locale: bstring ->
(string * sort) list * (Binding.T * 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.morphism) * stamp) list -> theory -> theory
@@ -45,6 +46,8 @@
(* Specification *)
val defined: theory -> string -> bool
val params_of: theory -> string -> (Binding.T * 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.morphism -> term list
val specification_of: theory -> string -> term option * term list
val declarations_of: theory -> string -> declaration list * declaration list
@@ -118,6 +121,8 @@
(* type and term parameters *)
spec: term option * term list,
(* assumptions (as a single predicate expression) and defines *)
+ intros: thm option * thm option,
+ axioms: thm list,
(** dynamic part **)
decls: (declaration * stamp) list * (declaration * stamp) list,
(* type and term syntax declarations *)
@@ -127,17 +132,18 @@
(* locale dependencies (sublocale relation) *)
};
-fun mk_locale ((parameters, spec), ((decls, notes), dependencies)) =
- Loc {parameters = parameters, spec = spec, decls = decls,
- notes = notes, dependencies = dependencies};
-fun map_locale f (Loc {parameters, spec, decls, notes, dependencies}) =
- mk_locale (f ((parameters, spec), ((decls, notes), dependencies)));
-fun merge_locale (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
- Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
- mk_locale ((parameters, spec),
- (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
- merge (eq_snd op =) (notes, notes')),
- merge (eq_snd op =) (dependencies, dependencies')));
+fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
+ Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
+ decls = decls, notes = notes, dependencies = dependencies};
+fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
+ mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
+fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
+ notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
+ dependencies = dependencies', ...}) = mk_locale
+ ((parameters, spec, intros, axioms),
+ (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
+ merge (eq_snd op =) (notes, notes')),
+ merge (eq_snd op =) (dependencies, dependencies')));
structure LocalesData = TheoryDataFun
(
@@ -159,9 +165,9 @@
of SOME (Loc loc) => loc
| NONE => error ("Unknown locale " ^ quote name);
-fun register_locale bname parameters spec decls notes dependencies thy =
+fun register_locale bname parameters spec intros axioms decls notes dependencies thy =
thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
- mk_locale ((parameters, spec), ((decls, notes), dependencies))) #> snd);
+ mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
fun change_locale name =
LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -175,6 +181,10 @@
fun params_of thy = snd o #parameters o the_locale thy;
+fun intros_of thy = #intros o the_locale thy;
+
+fun axioms_of thy = #axioms o the_locale thy;
+
fun instance_of thy name morph = params_of thy name |>
map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);