--- a/src/Pure/Isar/isar_syn.ML Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Apr 02 14:08:30 2004 +0200
@@ -357,6 +357,12 @@
OuterSyntax.command "using" "augment goal facts" K.prf_decl
(facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
+val instantiateP =
+ OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
+ (P.name --| P.$$$ ":" -- P.xname
+(* (P.xname -- (P.$$$ "[" |-- P.name --| P.$$$ "]") *)
+ >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));
+
(* proof context *)
@@ -756,7 +762,7 @@
default_proofP, immediate_proofP, done_proofP, skip_proofP,
forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
- redoP, undos_proofP, undoP, killP,
+ redoP, undos_proofP, undoP, killP, instantiateP,
(*diagnostic commands*)
pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
print_syntaxP, print_theoremsP, print_localesP, print_localeP,
--- a/src/Pure/Isar/locale.ML Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/locale.ML Fri Apr 02 14:08:30 2004 +0200
@@ -65,6 +65,7 @@
val add_thmss: string -> ((string * thm list) * context attribute list) list ->
theory * context -> (theory * context) * (string * thm list) list
val prune_prems: theory -> thm -> thm
+ val instantiate: string -> string -> thm list option -> context -> context
val setup: (theory -> theory) list
end;
@@ -96,7 +97,7 @@
type locale =
{view: cterm list * thm list,
- (* If locale "loc" contains assumptions, either via import or in the
+ (* CB: If locale "loc" contains assumptions, either via import or in the
locale body, a locale predicate "loc" is defined capturing all the
assumptions. If both import and body contain assumptions, additionally
a delta predicate "loc_axioms" is defined that abbreviates the
@@ -107,10 +108,11 @@
locales with import from the import hierarchy (duplicates removed,
cf. [1], normalisation of locale expressions).
- The first part of view in the above definition (also called statement)
- represents this list of assumptions. The second part (also called
- axioms) contains projections from the predicate "loc" to these
- assumptions.
+ The record entry view is either ([], []) or ([statement], axioms)
+ where statement is the predicate "loc" applied to the parameters,
+ and axioms contains projections from "loc" to the list of assumptions
+ generated when entering the locale.
+ It appears that an axiom of the form A [A] is never generated.
*)
import: expr, (*dynamic import*)
elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*)
@@ -229,7 +231,7 @@
Remove internal delta predicates (generated by "includes") from the
premises of a theorem.
- Assumes no outer quanfifiers and no flex-flex pairs.
+ Assumes no outer quantifiers and no flex-flex pairs.
May change names of TVars.
Performs compress and close_derivation on result, if modified. **)
@@ -466,6 +468,9 @@
(* parameter types *)
+(* CB: frozen_tvars has the following type:
+ ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *)
+
fun frozen_tvars ctxt Ts =
let
val tvars = rev (foldl Term.add_tvarsT ([], Ts));
@@ -492,6 +497,9 @@
in map (apsome (Envir.norm_type unifier')) Vs end;
fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss));
+
+(* CB: param_types has the following type:
+ ('a * 'b Library.option) list -> ('a * 'b) list *)
fun param_types ps = mapfilter (fn (_, None) => None | (x, Some T) => Some (x, T)) ps;
@@ -499,6 +507,11 @@
local
+(* CB: unique_parms has the following type:
+ 'a ->
+ (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->
+ (('b * ('c * 'd) list) * 'e) list *)
+
fun unique_parms ctxt elemss =
let
val param_decls =
@@ -511,6 +524,12 @@
| None => map (apfst (apsnd #1)) elemss)
end;
+(* CB: unify_parms has the following type:
+ ProofContext.context ->
+ (string * Term.typ) list ->
+ (string * Term.typ Library.option) list list ->
+ ((string * Term.sort) * Term.typ) list list *)
+
fun unify_parms ctxt fixed_parms raw_parmss =
let
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
@@ -649,13 +668,22 @@
in
+(* CB: activate_facts prep_facts ((ctxt, axioms), elemss),
+ where elemss is a list of pairs consisting of identifiers and context
+ elements, extends ctxt by the context elements yielding ctxt' and returns
+ ((ctxt', axioms'), (elemss', facts)).
+ Assumptions use entries from axioms to set up exporters in ctxt'. Unused
+ axioms are returned as axioms'; elemss' is obtained from elemss (without
+ identifier) and the intermediate context with prep_facts.
+ If get_facts or get_facts_i is used for prep_facts, these also remove
+ the internal/external markers from elemss. *)
+
fun activate_facts prep_facts arg =
apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg);
end;
-
(** prepare context elements **)
(* expressions *)
@@ -669,7 +697,7 @@
local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
-(* Map attrib over
+(* CB: Map attrib over
* A context element: add attrib to attribute lists of assumptions,
definitions and facts (on both sides for facts).
* Locale expression: no effect. *)
@@ -705,6 +733,22 @@
datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
+(* CB: flatten (ids, 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', elemss) where ids' is an extension of ids
+ with identifiers generated for expr, and elemss is the list of
+ context elements generated from expr, decorated with additional
+ information (the identifiers?), including parameter names.
+ It appears that the identifier name is empty for external elements
+ (this is suggested by the implementation of activate_facts). *)
+
+fun flatten _ (ids, Elem (Fixes fixes)) =
+ (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
+ | flatten _ (ids, Elem elem) = (ids, [(("", []), Ext elem)])
+ | flatten (ctxt, prep_expr) (ids, Expr expr) =
+ apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
+
local
local
@@ -752,6 +796,9 @@
local
+(* CB: following code (norm_term, abstract_term, abstract_thm, bind_def)
+ used in eval_text for defines elements. *)
+
val norm_term = Envir.beta_norm oo Term.subst_atomic;
fun abstract_term eq = (*assumes well-formedness according to ProofContext.cert_def*)
@@ -845,12 +892,22 @@
fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
let
+ (* CB: raw_elemss are list of pairs consisting of identifiers and
+ context elements, the latter marked as internal or external. *)
val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes 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. *)
val raw_propps = map flat raw_proppss;
val raw_propp = flat raw_propps;
val (ctxt, all_propp) =
prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
+ (* CB: read/cert entire proposition (conclusion and premises from
+ the context elements). *)
val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt;
+ (* CB: it appears that terms declared in the propositions are added
+ to the context here. *)
val all_propp' = map2 (op ~~)
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
@@ -863,9 +920,33 @@
(map (ProofContext.default_type raw_ctxt) xs)
(map (ProofContext.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 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
+ - axiom and definition statement replaced by corresponding one
+ from proppss in Assumes and Defines
+ - Facts unchanged
+ *)
in ((parms, elemss, concl), text) end;
in
@@ -881,6 +962,7 @@
local
fun prep_name ctxt (name, atts) =
+ (* CB: reject qualified names in locale declarations *)
if NameSpace.is_qualified name then
raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
else (name, atts);
@@ -909,15 +991,12 @@
let
val sign = ProofContext.sign_of context;
- fun flatten (ids, Elem (Fixes fixes)) =
- (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
- | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
- | flatten (ids, Expr expr) =
- apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr));
-
- val (import_ids, raw_import_elemss) = flatten ([], Expr import);
+ val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import);
(* CB: normalise "includes" among elements *)
- val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
+ val raw_elemss = flat (#2 ((foldl_map (flatten (context, prep_expr sign))
+ (import_ids, elements))));
+ (* CB: raw_import_elemss @ raw_elemss is the normalised list of
+ context elements obtained from import and elements. *)
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
@@ -938,7 +1017,7 @@
val thy = ProofContext.theory_of ctxt;
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
val ((view_statement, view_axioms), fixed_params, import) =
-(* view_axioms are xxx.axioms of locale xxx *)
+(* CB: view_axioms are xxx.axioms of locale xxx *)
(case locale of None => (([], []), [], empty)
| Some name =>
let val {view, params = (ps, _), ...} = the_locale thy name
@@ -949,7 +1028,7 @@
in
-(* CB: arguments are: x->import, y->body (elements?), z->context *)
+(* CB: arguments are: x->import, y->body (elements), z->context *)
fun read_context x y z = #1 (gen_context true [] [] x y [] z);
fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
@@ -959,6 +1038,157 @@
end;
+(** CB: experimental instantiation mechanism **)
+
+fun instantiate loc_name prfx raw_inst ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val sign = Theory.sign_of thy;
+ val tsig = Sign.tsig_of sign;
+ val cert = cterm_of sign;
+
+ (** process the locale **)
+
+ val {view = (_, axioms), params = (ps, _), ...} =
+ the_locale thy (intern sign loc_name);
+ val fixed_params = param_types ps;
+ val (ids, raw_elemss) =
+ flatten (ctxt, intern_expr sign) ([], Expr (Locale loc_name));
+ val ((parms, all_elemss, concl),
+ (spec as (_, (ints, _)), (xs, env, defs))) =
+ read_elemss false (* do_close *) ctxt
+ fixed_params (* could also put [] here??? *) raw_elemss
+ [] (* concl *);
+
+ (** analyse the instantiation theorem inst **)
+
+ val inst = case raw_inst of
+ None => if null ints
+ then None
+ else error "Locale has assumptions but no chained fact was found"
+ | Some [] => if null ints
+ then None
+ else error "Locale has assumptions but no chained fact was found"
+ | Some [thm] => if null ints
+ then (warning "Locale has no assumptions: fact ignored"; None)
+ else Some thm
+ | Some _ => error "Multiple facts are not allowed";
+
+ val args = case inst of
+ None => []
+ | Some thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
+ |> Term.strip_comb |> snd;
+ val cargs = map cert args;
+
+ (* process parameters: match their types with those of arguments *)
+
+ val def_names = map (fn (Free (s, _), _) => s) env;
+ val (defined, assumed) = partition
+ (fn (s, _) => s mem def_names) fixed_params;
+ val cassumed = map (cert o Free) assumed;
+ val cdefined = map (cert o Free) defined;
+
+ val param_types = map snd assumed;
+ val v_param_types = map Type.varifyT param_types;
+ val arg_types = map Term.fastype_of args;
+ val Tenv = foldl (Type.typ_match tsig)
+ (Vartab.empty, v_param_types ~~ arg_types)
+ handle Library.LIST "~~" => error "Number of parameters does not match number of arguments of chained fact";
+ (* get their sorts *)
+ val tfrees = foldr Term.add_typ_tfrees (param_types, []);
+ val Tenv' = map
+ (fn ((a, i), T) => ((a, the (assoc_string (tfrees, a))), T))
+ (Vartab.dest Tenv);
+
+ (* process (internal) elements *)
+
+ fun inst_type [] T = T
+ | inst_type env T =
+ Term.map_type_tfree (fn v => if_none (assoc (env, v)) (TFree v)) T;
+
+ fun inst_term [] t = t
+ | inst_term env t = Term.map_term_types (inst_type env) t;
+
+ (* parameters with argument types *)
+
+ val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed;
+ val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined;
+ val cdefining = map (cert o inst_term Tenv' o snd) env;
+
+ fun inst_thm _ [] th = th
+ | inst_thm ctxt Tenv th =
+ let
+ val sign = ProofContext.sign_of ctxt;
+ val cert = Thm.cterm_of sign;
+ val certT = Thm.ctyp_of sign;
+ val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
+ val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []);
+ val Tenv' = filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
+ in
+ if null Tenv' then th
+ else
+ th
+ |> Drule.implies_intr_list (map cert hyps)
+ |> Drule.tvars_intr_list (map (#1 o #1) Tenv')
+ |> (fn (th', al) => th' |>
+ Thm.instantiate ((map (fn ((a, _), T) =>
+ (the (assoc (al, a)), certT T)) Tenv'), []))
+ |> (fn th'' => Drule.implies_elim_list th''
+ (map (Thm.assume o cert o inst_term Tenv') hyps))
+ end;
+
+ fun inst_thm' thm =
+ let
+ (* not all axs are normally applicable *)
+ val hyps = #hyps (rep_thm thm);
+ val ass = map (fn ax => (prop_of ax, ax)) axioms;
+ val axs' = foldl (fn (axs, hyp) =>
+ (case assoc (ass, hyp) of None => axs
+ | Some ax => axs @ [ax])) ([], hyps);
+ val thm' = Drule.satisfy_hyps axs' thm;
+ (* instantiate types *)
+ val thm'' = inst_thm ctxt Tenv' thm';
+ (* substitute arguments and discharge hypotheses *)
+ val thm''' = case inst of
+ None => thm''
+ | Some inst_thm => let
+ val hyps = #hyps (rep_thm thm'');
+ val th = thm'' |> implies_intr_hyps
+ |> forall_intr_list (cparams' @ cdefined')
+ |> forall_elim_list (cargs @ cdefining)
+ (* th has premises of the form either inst_thm or x==x *)
+ fun mk hyp = if Logic.is_equals hyp
+ then hyp |> Logic.dest_equals |> snd |> cert
+ |> reflexive
+ else inst_thm
+ in implies_elim_list th (map mk hyps)
+ end;
+ in thm''' end;
+
+ fun inst_elem (ctxt, (Ext _)) = ctxt
+ | inst_elem (ctxt, (Int (Notes facts))) =
+ (* instantiate fact *)
+ let val facts' =
+ map (apsnd (map (apfst (map inst_thm')))) facts
+ (* rename fact *)
+ val facts'' =
+ map (apfst (apfst (fn "" => ""
+ | s => NameSpace.append prfx s)))
+ facts'
+ in fst (ProofContext.have_thmss_i facts'' ctxt)
+ end
+ | inst_elem (ctxt, (Int _)) = ctxt;
+
+ fun inst_elems (ctxt, (id, elems)) = foldl inst_elem (ctxt, elems);
+
+ fun inst_elemss ctxt elemss = foldl inst_elems (ctxt, elemss);
+
+ (* main part *)
+
+ val ctxt' = ProofContext.qualified true ctxt;
+ in ProofContext.restore_qualified ctxt (inst_elemss ctxt' all_elemss)
+ end;
+
(** define locales **)
@@ -1019,6 +1249,7 @@
fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind)
| smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc;
+ (* CB: only used in Proof.finish_global. *)
end;
@@ -1050,6 +1281,8 @@
val have_thmss = gen_have_thmss intern ProofContext.get_thms;
val have_thmss_i = gen_have_thmss (K I) (K I);
+ (* CB: have_thmss(_i) is the base for the Isar commands
+ "theorems (in loc)" and "declare (in loc)". *)
fun add_thmss loc args (thy, ctxt) =
let
@@ -1059,6 +1292,7 @@
val ((ctxt', _), (_, facts')) =
activate_facts (K I) ((ctxt, view_axioms), [(("", []), [Notes args'])]);
in ((thy', ctxt'), facts') end;
+ (* CB: only used in Proof.finish_global. *)
end;