src/Pure/Isar/locale.ML
changeset 14508 859b11514537
parent 14446 0bc2519e9990
child 14528 1457584110ac
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Apr 02 12:25:48 2004 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Apr 02 14:08:30 2004 +0200
     1.3 @@ -65,6 +65,7 @@
     1.4    val add_thmss: string -> ((string * thm list) * context attribute list) list ->
     1.5      theory * context -> (theory * context) * (string * thm list) list
     1.6    val prune_prems: theory -> thm -> thm
     1.7 +  val instantiate: string -> string -> thm list option -> context -> context
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -96,7 +97,7 @@
    1.12  
    1.13  type locale =
    1.14   {view: cterm list * thm list,
    1.15 -    (* If locale "loc" contains assumptions, either via import or in the
    1.16 +    (* CB: If locale "loc" contains assumptions, either via import or in the
    1.17         locale body, a locale predicate "loc" is defined capturing all the
    1.18         assumptions.  If both import and body contain assumptions, additionally
    1.19         a delta predicate "loc_axioms" is defined that abbreviates the
    1.20 @@ -107,10 +108,11 @@
    1.21         locales with import from the import hierarchy (duplicates removed,
    1.22         cf. [1], normalisation of locale expressions).
    1.23  
    1.24 -       The first part of view in the above definition (also called statement)
    1.25 -       represents this list of assumptions.  The second part (also called
    1.26 -       axioms) contains projections from the predicate "loc" to these
    1.27 -       assumptions.
    1.28 +       The record entry view is either ([], []) or ([statement], axioms)
    1.29 +       where statement is the predicate "loc" applied to the parameters,
    1.30 +       and axioms contains projections from "loc" to the list of assumptions
    1.31 +       generated when entering the locale.
    1.32 +       It appears that an axiom of the form A [A] is never generated.
    1.33       *)
    1.34    import: expr,                                                         (*dynamic import*)
    1.35    elems: ((typ, term, thm list, context attribute) elem * stamp) list,  (*static content*)
    1.36 @@ -229,7 +231,7 @@
    1.37     Remove internal delta predicates (generated by "includes") from the
    1.38     premises of a theorem.
    1.39  
    1.40 -   Assumes no outer quanfifiers and no flex-flex pairs.
    1.41 +   Assumes no outer quantifiers and no flex-flex pairs.
    1.42     May change names of TVars.
    1.43     Performs compress and close_derivation on result, if modified. **)
    1.44  
    1.45 @@ -466,6 +468,9 @@
    1.46  
    1.47  (* parameter types *)
    1.48  
    1.49 +(* CB: frozen_tvars has the following type:
    1.50 +  ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *)
    1.51 +
    1.52  fun frozen_tvars ctxt Ts =
    1.53    let
    1.54      val tvars = rev (foldl Term.add_tvarsT ([], Ts));
    1.55 @@ -492,6 +497,9 @@
    1.56    in map (apsome (Envir.norm_type unifier')) Vs end;
    1.57  
    1.58  fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss));
    1.59 +
    1.60 +(* CB: param_types has the following type:
    1.61 +  ('a * 'b Library.option) list -> ('a * 'b) list *)
    1.62  fun param_types ps = mapfilter (fn (_, None) => None | (x, Some T) => Some (x, T)) ps;
    1.63  
    1.64  
    1.65 @@ -499,6 +507,11 @@
    1.66  
    1.67  local
    1.68  
    1.69 +(* CB: unique_parms has the following type:
    1.70 +     'a ->
    1.71 +     (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->
    1.72 +     (('b * ('c * 'd) list) * 'e) list  *)
    1.73 +
    1.74  fun unique_parms ctxt elemss =
    1.75    let
    1.76      val param_decls =
    1.77 @@ -511,6 +524,12 @@
    1.78      | None => map (apfst (apsnd #1)) elemss)
    1.79    end;
    1.80  
    1.81 +(* CB: unify_parms has the following type:
    1.82 +     ProofContext.context ->
    1.83 +     (string * Term.typ) list ->
    1.84 +     (string * Term.typ Library.option) list list ->
    1.85 +     ((string * Term.sort) * Term.typ) list list *)
    1.86 +
    1.87  fun unify_parms ctxt fixed_parms raw_parmss =
    1.88    let
    1.89      val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
    1.90 @@ -649,13 +668,22 @@
    1.91  
    1.92  in
    1.93  
    1.94 +(* CB: activate_facts prep_facts ((ctxt, axioms), elemss),
    1.95 +   where elemss is a list of pairs consisting of identifiers and context
    1.96 +   elements, extends ctxt by the context elements yielding ctxt' and returns
    1.97 +   ((ctxt', axioms'), (elemss', facts)).
    1.98 +   Assumptions use entries from axioms to set up exporters in ctxt'.  Unused
    1.99 +   axioms are returned as axioms'; elemss' is obtained from elemss (without
   1.100 +   identifier) and the intermediate context with prep_facts.
   1.101 +   If get_facts or get_facts_i is used for prep_facts, these also remove
   1.102 +   the internal/external markers from elemss. *)
   1.103 +
   1.104  fun activate_facts prep_facts arg =
   1.105    apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg);
   1.106  
   1.107  end;
   1.108  
   1.109  
   1.110 -
   1.111  (** prepare context elements **)
   1.112  
   1.113  (* expressions *)
   1.114 @@ -669,7 +697,7 @@
   1.115  
   1.116  local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
   1.117  
   1.118 -(* Map attrib over
   1.119 +(* CB: Map attrib over
   1.120     * A context element: add attrib to attribute lists of assumptions,
   1.121       definitions and facts (on both sides for facts).
   1.122     * Locale expression: no effect. *)
   1.123 @@ -705,6 +733,22 @@
   1.124  
   1.125  datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   1.126  
   1.127 +(* CB: flatten (ids, expr) normalises expr (which is either a locale
   1.128 +   expression or a single context element) wrt.
   1.129 +   to the list ids of already accumulated identifiers.
   1.130 +   It returns (ids', elemss) where ids' is an extension of ids
   1.131 +   with identifiers generated for expr, and elemss is the list of
   1.132 +   context elements generated from expr, decorated with additional
   1.133 +   information (the identifiers?), including parameter names.
   1.134 +   It appears that the identifier name is empty for external elements
   1.135 +   (this is suggested by the implementation of activate_facts). *)
   1.136 +
   1.137 +fun flatten _ (ids, Elem (Fixes fixes)) =
   1.138 +      (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
   1.139 +  | flatten _ (ids, Elem elem) = (ids, [(("", []), Ext elem)])
   1.140 +  | flatten (ctxt, prep_expr) (ids, Expr expr) =
   1.141 +      apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
   1.142 +
   1.143  local
   1.144  
   1.145  local
   1.146 @@ -752,6 +796,9 @@
   1.147  
   1.148  local
   1.149  
   1.150 +(* CB: following code (norm_term, abstract_term, abstract_thm, bind_def)
   1.151 +   used in eval_text for defines elements. *)
   1.152 +
   1.153  val norm_term = Envir.beta_norm oo Term.subst_atomic;
   1.154  
   1.155  fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)
   1.156 @@ -845,12 +892,22 @@
   1.157  
   1.158  fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
   1.159    let
   1.160 +    (* CB: raw_elemss are list of pairs consisting of identifiers and
   1.161 +       context elements, the latter marked as internal or external. *)
   1.162      val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
   1.163 +    (* CB: raw_ctxt is context with additional fixed variables derived from
   1.164 +       the fixes elements in raw_elemss,
   1.165 +       raw_proppss contains assumptions and definitions from the
   1.166 +       (external?) elements in raw_elemss. *)
   1.167      val raw_propps = map flat raw_proppss;
   1.168      val raw_propp = flat raw_propps;
   1.169      val (ctxt, all_propp) =
   1.170        prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
   1.171 +    (* CB: read/cert entire proposition (conclusion and premises from
   1.172 +       the context elements). *)
   1.173      val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt;
   1.174 +    (* CB: it appears that terms declared in the propositions are added
   1.175 +       to the context here. *)
   1.176  
   1.177      val all_propp' = map2 (op ~~)
   1.178        (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
   1.179 @@ -863,9 +920,33 @@
   1.180        (map (ProofContext.default_type raw_ctxt) xs)
   1.181        (map (ProofContext.default_type ctxt) xs);
   1.182      val parms = param_types (xs ~~ typing);
   1.183 +    (* CB: parms are the parameters from raw_elemss, with correct typing. *)
   1.184  
   1.185 +    (* CB: extract information from assumes and defines elements
   1.186 +       (fixes and notes in raw_elemss don't have an effect on text and elemss),
   1.187 +       compute final form of context elements. *)
   1.188      val (text, elemss) = finish_elemss ctxt parms do_close
   1.189        (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);
   1.190 +    (* CB: text has the following structure:
   1.191 +           (((exts, exts'), (ints, ints')), (xs, env, defs))
   1.192 +       where
   1.193 +         exts: external assumptions (terms in external assumes elements)
   1.194 +         exts': dito, normalised wrt. env
   1.195 +         ints: internal assumptions (terms in internal assumes elements)
   1.196 +         ints': dito, normalised wrt. env
   1.197 +         xs: the free variables in exts' and ints' and rhss of definitions,
   1.198 +           this includes parameters except defined parameters
   1.199 +         env: list of term pairs encoding substitutions, where the first term
   1.200 +           is a free variable; substitutions represent defines elements and
   1.201 +           the rhs is normalised wrt. the previous env
   1.202 +         defs: theorems representing the substitutions from defines elements
   1.203 +           (thms are normalised wrt. env).
   1.204 +       elemss is an updated version of raw_elemss:
   1.205 +         - type info added to Fixes
   1.206 +         - axiom and definition statement replaced by corresponding one
   1.207 +           from proppss in Assumes and Defines
   1.208 +         - Facts unchanged
   1.209 +       *)
   1.210    in ((parms, elemss, concl), text) end;
   1.211  
   1.212  in
   1.213 @@ -881,6 +962,7 @@
   1.214  local
   1.215  
   1.216  fun prep_name ctxt (name, atts) =
   1.217 +  (* CB: reject qualified names in locale declarations *)
   1.218    if NameSpace.is_qualified name then
   1.219      raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
   1.220    else (name, atts);
   1.221 @@ -909,15 +991,12 @@
   1.222    let
   1.223      val sign = ProofContext.sign_of context;
   1.224  
   1.225 -    fun flatten (ids, Elem (Fixes fixes)) =
   1.226 -          (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
   1.227 -      | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
   1.228 -      | flatten (ids, Expr expr) =
   1.229 -          apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr));
   1.230 -
   1.231 -    val (import_ids, raw_import_elemss) = flatten ([], Expr import);
   1.232 +    val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import);
   1.233      (* CB: normalise "includes" among elements *)
   1.234 -    val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
   1.235 +    val raw_elemss = flat (#2 ((foldl_map (flatten (context, prep_expr sign))
   1.236 +      (import_ids, elements))));
   1.237 +    (* CB: raw_import_elemss @ raw_elemss is the normalised list of
   1.238 +       context elements obtained from import and elements. *)
   1.239      val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
   1.240        context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
   1.241      val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
   1.242 @@ -938,7 +1017,7 @@
   1.243      val thy = ProofContext.theory_of ctxt;
   1.244      val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
   1.245      val ((view_statement, view_axioms), fixed_params, import) =
   1.246 -(* view_axioms are xxx.axioms of locale xxx *)
   1.247 +(* CB: view_axioms are xxx.axioms of locale xxx *)
   1.248        (case locale of None => (([], []), [], empty)
   1.249        | Some name =>
   1.250            let val {view, params = (ps, _), ...} = the_locale thy name
   1.251 @@ -949,7 +1028,7 @@
   1.252  
   1.253  in
   1.254  
   1.255 -(* CB: arguments are: x->import, y->body (elements?), z->context *)
   1.256 +(* CB: arguments are: x->import, y->body (elements), z->context *)
   1.257  fun read_context x y z = #1 (gen_context true [] [] x y [] z);
   1.258  fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
   1.259  
   1.260 @@ -959,6 +1038,157 @@
   1.261  end;
   1.262  
   1.263  
   1.264 +(** CB: experimental instantiation mechanism **)
   1.265 +
   1.266 +fun instantiate loc_name prfx raw_inst ctxt =
   1.267 +  let
   1.268 +    val thy = ProofContext.theory_of ctxt;
   1.269 +    val sign = Theory.sign_of thy;
   1.270 +    val tsig = Sign.tsig_of sign;
   1.271 +    val cert = cterm_of sign;
   1.272 +
   1.273 +    (** process the locale **)
   1.274 +
   1.275 +    val {view = (_, axioms), params = (ps, _), ...} =
   1.276 +      the_locale thy (intern sign loc_name);
   1.277 +    val fixed_params = param_types ps;
   1.278 +    val (ids, raw_elemss) =
   1.279 +          flatten (ctxt, intern_expr sign) ([], Expr (Locale loc_name));
   1.280 +    val ((parms, all_elemss, concl),
   1.281 +         (spec as (_, (ints, _)), (xs, env, defs))) =
   1.282 +      read_elemss false (* do_close *) ctxt
   1.283 +        fixed_params (* could also put [] here??? *) raw_elemss
   1.284 +        [] (* concl *);
   1.285 +
   1.286 +    (** analyse the instantiation theorem inst **)
   1.287 +
   1.288 +    val inst = case raw_inst of
   1.289 +        None => if null ints
   1.290 +	  then None
   1.291 +	  else error "Locale has assumptions but no chained fact was found"
   1.292 +      | Some [] => if null ints
   1.293 +	  then None
   1.294 +	  else error "Locale has assumptions but no chained fact was found"
   1.295 +      | Some [thm] => if null ints
   1.296 +	  then (warning "Locale has no assumptions: fact ignored"; None)
   1.297 +	  else Some thm
   1.298 +      | Some _ => error "Multiple facts are not allowed";
   1.299 +
   1.300 +    val args = case inst of
   1.301 +            None => []
   1.302 +          | Some thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
   1.303 +              |> Term.strip_comb |> snd;
   1.304 +    val cargs = map cert args;
   1.305 +
   1.306 +    (* process parameters: match their types with those of arguments *)
   1.307 +
   1.308 +    val def_names = map (fn (Free (s, _), _) => s) env;
   1.309 +    val (defined, assumed) = partition
   1.310 +          (fn (s, _) => s mem def_names) fixed_params;
   1.311 +    val cassumed = map (cert o Free) assumed;
   1.312 +    val cdefined = map (cert o Free) defined;
   1.313 +
   1.314 +    val param_types = map snd assumed;
   1.315 +    val v_param_types = map Type.varifyT param_types;
   1.316 +    val arg_types = map Term.fastype_of args;
   1.317 +    val Tenv = foldl (Type.typ_match tsig)
   1.318 +          (Vartab.empty, v_param_types ~~ arg_types)
   1.319 +          handle Library.LIST "~~" => error "Number of parameters does not match number of arguments of chained fact";
   1.320 +    (* get their sorts *)
   1.321 +    val tfrees = foldr Term.add_typ_tfrees (param_types, []);
   1.322 +    val Tenv' = map
   1.323 +          (fn ((a, i), T) => ((a, the (assoc_string (tfrees, a))), T))
   1.324 +          (Vartab.dest Tenv);
   1.325 +
   1.326 +    (* process (internal) elements *)
   1.327 +
   1.328 +    fun inst_type [] T = T
   1.329 +      | inst_type env T =
   1.330 +          Term.map_type_tfree (fn v => if_none (assoc (env, v)) (TFree v)) T;
   1.331 +
   1.332 +    fun inst_term [] t = t
   1.333 +      | inst_term env t = Term.map_term_types (inst_type env) t;
   1.334 +
   1.335 +    (* parameters with argument types *)
   1.336 +
   1.337 +    val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed;
   1.338 +    val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined;
   1.339 +    val cdefining = map (cert o inst_term Tenv' o snd) env;
   1.340 +
   1.341 +    fun inst_thm _ [] th = th
   1.342 +      | inst_thm ctxt Tenv th =
   1.343 +	  let
   1.344 +	    val sign = ProofContext.sign_of ctxt;
   1.345 +	    val cert = Thm.cterm_of sign;
   1.346 +	    val certT = Thm.ctyp_of sign;
   1.347 +	    val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
   1.348 +	    val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []);
   1.349 +	    val Tenv' = filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
   1.350 +	  in
   1.351 +	    if null Tenv' then th
   1.352 +	    else
   1.353 +	      th
   1.354 +	      |> Drule.implies_intr_list (map cert hyps)
   1.355 +	      |> Drule.tvars_intr_list (map (#1 o #1) Tenv')
   1.356 +	      |> (fn (th', al) => th' |>
   1.357 +		Thm.instantiate ((map (fn ((a, _), T) =>
   1.358 +                  (the (assoc (al, a)), certT T)) Tenv'), []))
   1.359 +	      |> (fn th'' => Drule.implies_elim_list th''
   1.360 +		  (map (Thm.assume o cert o inst_term Tenv') hyps))
   1.361 +	  end;
   1.362 +
   1.363 +    fun inst_thm' thm =
   1.364 +      let
   1.365 +        (* not all axs are normally applicable *)
   1.366 +        val hyps = #hyps (rep_thm thm);
   1.367 +        val ass = map (fn ax => (prop_of ax, ax)) axioms;
   1.368 +        val axs' = foldl (fn (axs, hyp) => 
   1.369 +              (case assoc (ass, hyp) of None => axs
   1.370 +                 | Some ax => axs @ [ax])) ([], hyps);
   1.371 +        val thm' = Drule.satisfy_hyps axs' thm;
   1.372 +        (* instantiate types *)
   1.373 +        val thm'' = inst_thm ctxt Tenv' thm';
   1.374 +        (* substitute arguments and discharge hypotheses *)
   1.375 +        val thm''' = case inst of
   1.376 +                None => thm''
   1.377 +              | Some inst_thm => let
   1.378 +		    val hyps = #hyps (rep_thm thm'');
   1.379 +		    val th = thm'' |> implies_intr_hyps
   1.380 +		      |> forall_intr_list (cparams' @ cdefined')
   1.381 +		      |> forall_elim_list (cargs @ cdefining)
   1.382 +		    (* th has premises of the form either inst_thm or x==x *)
   1.383 +		    fun mk hyp = if Logic.is_equals hyp
   1.384 +			  then hyp |> Logic.dest_equals |> snd |> cert
   1.385 +				 |> reflexive
   1.386 +			  else inst_thm
   1.387 +                  in implies_elim_list th (map mk hyps)
   1.388 +                  end;
   1.389 +      in thm''' end;
   1.390 +
   1.391 +    fun inst_elem (ctxt, (Ext _)) = ctxt
   1.392 +      | inst_elem (ctxt, (Int (Notes facts))) =
   1.393 +              (* instantiate fact *)
   1.394 +          let val facts' =
   1.395 +              map (apsnd (map (apfst (map inst_thm')))) facts
   1.396 +              (* rename fact *)
   1.397 +              val facts'' =
   1.398 +              map (apfst (apfst (fn "" => ""
   1.399 +                                  | s => NameSpace.append prfx s)))
   1.400 +                  facts'
   1.401 +          in fst (ProofContext.have_thmss_i facts'' ctxt)
   1.402 +          end
   1.403 +      | inst_elem (ctxt, (Int _)) = ctxt;
   1.404 +
   1.405 +    fun inst_elems (ctxt, (id, elems)) = foldl inst_elem (ctxt, elems);
   1.406 +
   1.407 +    fun inst_elemss ctxt elemss = foldl inst_elems (ctxt, elemss);
   1.408 +
   1.409 +    (* main part *)
   1.410 +
   1.411 +    val ctxt' = ProofContext.qualified true ctxt;
   1.412 +  in ProofContext.restore_qualified ctxt (inst_elemss ctxt' all_elemss)
   1.413 +  end;
   1.414 +
   1.415  
   1.416  (** define locales **)
   1.417  
   1.418 @@ -1019,6 +1249,7 @@
   1.419  
   1.420  fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind)
   1.421    | smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc;
   1.422 +  (* CB: only used in Proof.finish_global. *)
   1.423  
   1.424  end;
   1.425  
   1.426 @@ -1050,6 +1281,8 @@
   1.427  
   1.428  val have_thmss = gen_have_thmss intern ProofContext.get_thms;
   1.429  val have_thmss_i = gen_have_thmss (K I) (K I);
   1.430 +  (* CB: have_thmss(_i) is the base for the Isar commands
   1.431 +     "theorems (in loc)" and "declare (in loc)". *)
   1.432  
   1.433  fun add_thmss loc args (thy, ctxt) =
   1.434    let
   1.435 @@ -1059,6 +1292,7 @@
   1.436      val ((ctxt', _), (_, facts')) =
   1.437        activate_facts (K I) ((ctxt, view_axioms), [(("", []), [Notes args'])]);
   1.438    in ((thy', ctxt'), facts') end;
   1.439 +  (* CB: only used in Proof.finish_global. *)
   1.440  
   1.441  end;
   1.442