Experimental command for instantiation of locales in proof contexts:
authorballarin
Fri Apr 02 14:08:30 2004 +0200 (2004-04-02)
changeset 14508859b11514537
parent 14507 0af3da3beae8
child 14509 9d8978a2ae56
Experimental command for instantiation of locales in proof contexts:
instantiate <label>: <loc>
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/FOL/IsaMakefile
src/FOL/ex/LocaleInst.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/NEWS	Fri Apr 02 12:25:48 2004 +0200
     1.2 +++ b/NEWS	Fri Apr 02 14:08:30 2004 +0200
     1.3 @@ -52,7 +52,8 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 -* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
     1.8 +* Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
     1.9 +  cut_tac, subgoal_tac and thin_tac:
    1.10    - Now understand static (Isar) contexts.  As a consequence, users of Isar
    1.11      locales are no longer forced to write Isar proof scripts.
    1.12      For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
    1.13 @@ -79,6 +80,14 @@
    1.14      specification and "includes" elements in goal statement.
    1.15    - Rule sets <locale>.intro and <locale>.axioms no longer declared as
    1.16      [intro?] and [elim?] (respectively) by default.
    1.17 +  - Experimental command for instantiation of locales in proof contexts:
    1.18 +        instantiate <label>: <loc>
    1.19 +    Instantiates locale <loc> and adds all its theorems to the current context
    1.20 +    taking into account their attributes, and qualifying their names with
    1.21 +    <label>.  If the locale has assumptions, a chained fact of the form
    1.22 +    "<loc> t1 ... tn" is expected from which instantiations of the parameters
    1.23 +    are derived.
    1.24 +    A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
    1.25  
    1.26  * HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.27    (Isar) contexts.
     2.1 --- a/etc/isar-keywords-ZF.el	Fri Apr 02 12:25:48 2004 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Fri Apr 02 14:08:30 2004 +0200
     2.3 @@ -55,6 +55,7 @@
     2.4      "exit"
     2.5      "extract"
     2.6      "extract_type"
     2.7 +    "finalconsts"
     2.8      "finally"
     2.9      "fix"
    2.10      "from"
    2.11 @@ -69,6 +70,7 @@
    2.12      "inductive_cases"
    2.13      "init_toplevel"
    2.14      "instance"
    2.15 +    "instantiate"
    2.16      "judgment"
    2.17      "kill"
    2.18      "kill_thy"
    2.19 @@ -308,6 +310,7 @@
    2.20      "defs"
    2.21      "extract"
    2.22      "extract_type"
    2.23 +    "finalconsts"
    2.24      "generate_code"
    2.25      "global"
    2.26      "hide"
    2.27 @@ -393,6 +396,7 @@
    2.28  
    2.29  (defconst isar-keywords-proof-decl
    2.30    '("also"
    2.31 +    "instantiate"
    2.32      "let"
    2.33      "moreover"
    2.34      "note"
     3.1 --- a/etc/isar-keywords.el	Fri Apr 02 12:25:48 2004 +0200
     3.2 +++ b/etc/isar-keywords.el	Fri Apr 02 14:08:30 2004 +0200
     3.3 @@ -73,6 +73,7 @@
     3.4      "inductive_cases"
     3.5      "init_toplevel"
     3.6      "instance"
     3.7 +    "instantiate"
     3.8      "judgment"
     3.9      "kill"
    3.10      "kill_thy"
    3.11 @@ -429,6 +430,7 @@
    3.12  
    3.13  (defconst isar-keywords-proof-decl
    3.14    '("also"
    3.15 +    "instantiate"
    3.16      "let"
    3.17      "moreover"
    3.18      "note"
     4.1 --- a/src/FOL/IsaMakefile	Fri Apr 02 12:25:48 2004 +0200
     4.2 +++ b/src/FOL/IsaMakefile	Fri Apr 02 14:08:30 2004 +0200
     4.3 @@ -44,6 +44,7 @@
     4.4  
     4.5  $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
     4.6    ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy	\
     4.7 +  ex/LocaleInst.thy \
     4.8    ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy	\
     4.9    ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
    4.10    ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/FOL/ex/LocaleInst.thy	Fri Apr 02 14:08:30 2004 +0200
     5.3 @@ -0,0 +1,114 @@
     5.4 +(*  Title:      FOL/ex/LocaleInst.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Clemens Ballarin
     5.7 +    Copyright (c) 2004 by Clemens Ballarin
     5.8 +
     5.9 +Test of locale instantiation mechanism, also provides a few examples.
    5.10 +*)
    5.11 +
    5.12 +header {* Test of Locale instantiation *}
    5.13 +
    5.14 +theory LocaleInst = FOL:
    5.15 +
    5.16 +ML {* set show_hyps *}
    5.17 +
    5.18 +section {* Locale without assumptions *}
    5.19 +
    5.20 +locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
    5.21 +
    5.22 +lemma "[| A; B |] ==> A & B"
    5.23 +proof -
    5.24 +  instantiate my: L1   txt {* No chained fact required. *}
    5.25 +  assume B and A  txt {* order reversed *}
    5.26 +  then show "A & B" ..
    5.27 +  txt {* Applies @{thm my.rev_conjI}. *}
    5.28 +qed
    5.29 +
    5.30 +section {* Simple locale with assumptions *}
    5.31 +
    5.32 +typedecl i
    5.33 +arities  i :: "term"
    5.34 +
    5.35 +consts bin :: "[i, i] => i" (infixl "#" 60)
    5.36 +
    5.37 +axioms i_assoc: "(x # y) # z = x # (y # z)"
    5.38 +  i_comm: "x # y = y # x"
    5.39 +
    5.40 +locale L2 =
    5.41 +  fixes OP (infixl "+" 60)
    5.42 +  assumes assoc: "(x + y) + z = x + (y + z)"
    5.43 +    and comm: "x + y = y + x"
    5.44 +
    5.45 +lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
    5.46 +proof -
    5.47 +  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
    5.48 +  also have "... = (y + x) + z" by (simp add: comm)
    5.49 +  also have "... = y + (x + z)" by (simp add: assoc)
    5.50 +  finally show ?thesis .
    5.51 +qed
    5.52 +
    5.53 +lemmas (in L2) AC = comm assoc lcomm
    5.54 +
    5.55 +lemma "(x::i) # y # z # w = y # x # w # z"
    5.56 +proof -
    5.57 +  have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm])
    5.58 +  then instantiate my: L2
    5.59 +    txt {* Chained fact required to discharge assumptions of @{text L2}
    5.60 +      and instantiate parameters. *}
    5.61 +  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
    5.62 +qed
    5.63 +
    5.64 +section {* Nested locale with assumptions *}
    5.65 +
    5.66 +locale L3 =
    5.67 +  fixes OP (infixl "+" 60)
    5.68 +  assumes assoc: "(x + y) + z = x + (y + z)"
    5.69 +
    5.70 +locale L4 = L3 +
    5.71 +  assumes comm: "x + y = y + x"
    5.72 +
    5.73 +lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
    5.74 +proof -
    5.75 +  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
    5.76 +  also have "... = (y + x) + z" by (simp add: comm)
    5.77 +  also have "... = y + (x + z)" by (simp add: assoc)
    5.78 +  finally show ?thesis .
    5.79 +qed
    5.80 +
    5.81 +lemmas (in L4) AC = comm assoc lcomm
    5.82 +
    5.83 +text {* Conceptually difficult locale:
    5.84 +   2nd context fragment contains facts with differing metahyps. *}
    5.85 +
    5.86 +lemma L4_intro:
    5.87 +  fixes OP (infixl "+" 60)
    5.88 +  assumes assoc: "!!x y z. (x + y) + z = x + (y + z)"
    5.89 +    and comm: "!!x y. x + y = y + x"
    5.90 +  shows "L4 (op+)"
    5.91 +    by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm)
    5.92 +
    5.93 +lemma "(x::i) # y # z # w = y # x # w # z"
    5.94 +proof -
    5.95 +  have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm])
    5.96 +  then instantiate my: L4
    5.97 +  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
    5.98 +qed
    5.99 +
   5.100 +section {* Locale with definition *}
   5.101 +
   5.102 +text {* This example is admittedly not very creative :-) *}
   5.103 +
   5.104 +locale L5 = L4 + var A +
   5.105 +  defines A_def: "A == True"
   5.106 +
   5.107 +lemma (in L5) lem: A
   5.108 +  by (unfold A_def) rule
   5.109 +
   5.110 +lemma "L5(op #) ==> True"
   5.111 +proof -
   5.112 +  assume "L5(op #)"
   5.113 +  then instantiate my: L5
   5.114 +  show ?thesis by (rule lem)  (* lem instantiated to True *)
   5.115 +qed
   5.116 +
   5.117 +end
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 02 12:25:48 2004 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 02 14:08:30 2004 +0200
     6.3 @@ -357,6 +357,12 @@
     6.4    OuterSyntax.command "using" "augment goal facts" K.prf_decl
     6.5      (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
     6.6  
     6.7 +val instantiateP =
     6.8 +  OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
     6.9 +    (P.name --| P.$$$ ":" -- P.xname
    6.10 +(*    (P.xname -- (P.$$$ "[" |-- P.name --| P.$$$ "]") *)
    6.11 +      >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));
    6.12 +
    6.13  
    6.14  (* proof context *)
    6.15  
    6.16 @@ -756,7 +762,7 @@
    6.17    default_proofP, immediate_proofP, done_proofP, skip_proofP,
    6.18    forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
    6.19    finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
    6.20 -  redoP, undos_proofP, undoP, killP,
    6.21 +  redoP, undos_proofP, undoP, killP, instantiateP,
    6.22    (*diagnostic commands*)
    6.23    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    6.24    print_syntaxP, print_theoremsP, print_localesP, print_localeP,
     7.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Apr 02 12:25:48 2004 +0200
     7.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 02 14:08:30 2004 +0200
     7.3 @@ -48,6 +48,7 @@
     7.4    val using_facts_i: (thm * Proof.context attribute list) list list
     7.5      -> ProofHistory.T -> ProofHistory.T
     7.6    val chain: ProofHistory.T -> ProofHistory.T
     7.7 +  val instantiate_locale: string * string -> ProofHistory.T -> ProofHistory.T
     7.8    val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
     7.9    val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
    7.10    val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
    7.11 @@ -290,6 +291,10 @@
    7.12  
    7.13  val chain = ProofHistory.apply Proof.chain;
    7.14  
    7.15 +(* locale instantiation *)
    7.16 +
    7.17 +fun instantiate_locale (prfx, loc) =
    7.18 +  ProofHistory.apply (Proof.instantiate_locale (loc, prfx));
    7.19  
    7.20  (* context *)
    7.21  
     8.1 --- a/src/Pure/Isar/locale.ML	Fri Apr 02 12:25:48 2004 +0200
     8.2 +++ b/src/Pure/Isar/locale.ML	Fri Apr 02 14:08:30 2004 +0200
     8.3 @@ -65,6 +65,7 @@
     8.4    val add_thmss: string -> ((string * thm list) * context attribute list) list ->
     8.5      theory * context -> (theory * context) * (string * thm list) list
     8.6    val prune_prems: theory -> thm -> thm
     8.7 +  val instantiate: string -> string -> thm list option -> context -> context
     8.8    val setup: (theory -> theory) list
     8.9  end;
    8.10  
    8.11 @@ -96,7 +97,7 @@
    8.12  
    8.13  type locale =
    8.14   {view: cterm list * thm list,
    8.15 -    (* If locale "loc" contains assumptions, either via import or in the
    8.16 +    (* CB: If locale "loc" contains assumptions, either via import or in the
    8.17         locale body, a locale predicate "loc" is defined capturing all the
    8.18         assumptions.  If both import and body contain assumptions, additionally
    8.19         a delta predicate "loc_axioms" is defined that abbreviates the
    8.20 @@ -107,10 +108,11 @@
    8.21         locales with import from the import hierarchy (duplicates removed,
    8.22         cf. [1], normalisation of locale expressions).
    8.23  
    8.24 -       The first part of view in the above definition (also called statement)
    8.25 -       represents this list of assumptions.  The second part (also called
    8.26 -       axioms) contains projections from the predicate "loc" to these
    8.27 -       assumptions.
    8.28 +       The record entry view is either ([], []) or ([statement], axioms)
    8.29 +       where statement is the predicate "loc" applied to the parameters,
    8.30 +       and axioms contains projections from "loc" to the list of assumptions
    8.31 +       generated when entering the locale.
    8.32 +       It appears that an axiom of the form A [A] is never generated.
    8.33       *)
    8.34    import: expr,                                                         (*dynamic import*)
    8.35    elems: ((typ, term, thm list, context attribute) elem * stamp) list,  (*static content*)
    8.36 @@ -229,7 +231,7 @@
    8.37     Remove internal delta predicates (generated by "includes") from the
    8.38     premises of a theorem.
    8.39  
    8.40 -   Assumes no outer quanfifiers and no flex-flex pairs.
    8.41 +   Assumes no outer quantifiers and no flex-flex pairs.
    8.42     May change names of TVars.
    8.43     Performs compress and close_derivation on result, if modified. **)
    8.44  
    8.45 @@ -466,6 +468,9 @@
    8.46  
    8.47  (* parameter types *)
    8.48  
    8.49 +(* CB: frozen_tvars has the following type:
    8.50 +  ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *)
    8.51 +
    8.52  fun frozen_tvars ctxt Ts =
    8.53    let
    8.54      val tvars = rev (foldl Term.add_tvarsT ([], Ts));
    8.55 @@ -492,6 +497,9 @@
    8.56    in map (apsome (Envir.norm_type unifier')) Vs end;
    8.57  
    8.58  fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss));
    8.59 +
    8.60 +(* CB: param_types has the following type:
    8.61 +  ('a * 'b Library.option) list -> ('a * 'b) list *)
    8.62  fun param_types ps = mapfilter (fn (_, None) => None | (x, Some T) => Some (x, T)) ps;
    8.63  
    8.64  
    8.65 @@ -499,6 +507,11 @@
    8.66  
    8.67  local
    8.68  
    8.69 +(* CB: unique_parms has the following type:
    8.70 +     'a ->
    8.71 +     (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->
    8.72 +     (('b * ('c * 'd) list) * 'e) list  *)
    8.73 +
    8.74  fun unique_parms ctxt elemss =
    8.75    let
    8.76      val param_decls =
    8.77 @@ -511,6 +524,12 @@
    8.78      | None => map (apfst (apsnd #1)) elemss)
    8.79    end;
    8.80  
    8.81 +(* CB: unify_parms has the following type:
    8.82 +     ProofContext.context ->
    8.83 +     (string * Term.typ) list ->
    8.84 +     (string * Term.typ Library.option) list list ->
    8.85 +     ((string * Term.sort) * Term.typ) list list *)
    8.86 +
    8.87  fun unify_parms ctxt fixed_parms raw_parmss =
    8.88    let
    8.89      val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
    8.90 @@ -649,13 +668,22 @@
    8.91  
    8.92  in
    8.93  
    8.94 +(* CB: activate_facts prep_facts ((ctxt, axioms), elemss),
    8.95 +   where elemss is a list of pairs consisting of identifiers and context
    8.96 +   elements, extends ctxt by the context elements yielding ctxt' and returns
    8.97 +   ((ctxt', axioms'), (elemss', facts)).
    8.98 +   Assumptions use entries from axioms to set up exporters in ctxt'.  Unused
    8.99 +   axioms are returned as axioms'; elemss' is obtained from elemss (without
   8.100 +   identifier) and the intermediate context with prep_facts.
   8.101 +   If get_facts or get_facts_i is used for prep_facts, these also remove
   8.102 +   the internal/external markers from elemss. *)
   8.103 +
   8.104  fun activate_facts prep_facts arg =
   8.105    apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg);
   8.106  
   8.107  end;
   8.108  
   8.109  
   8.110 -
   8.111  (** prepare context elements **)
   8.112  
   8.113  (* expressions *)
   8.114 @@ -669,7 +697,7 @@
   8.115  
   8.116  local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
   8.117  
   8.118 -(* Map attrib over
   8.119 +(* CB: Map attrib over
   8.120     * A context element: add attrib to attribute lists of assumptions,
   8.121       definitions and facts (on both sides for facts).
   8.122     * Locale expression: no effect. *)
   8.123 @@ -705,6 +733,22 @@
   8.124  
   8.125  datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   8.126  
   8.127 +(* CB: flatten (ids, expr) normalises expr (which is either a locale
   8.128 +   expression or a single context element) wrt.
   8.129 +   to the list ids of already accumulated identifiers.
   8.130 +   It returns (ids', elemss) where ids' is an extension of ids
   8.131 +   with identifiers generated for expr, and elemss is the list of
   8.132 +   context elements generated from expr, decorated with additional
   8.133 +   information (the identifiers?), including parameter names.
   8.134 +   It appears that the identifier name is empty for external elements
   8.135 +   (this is suggested by the implementation of activate_facts). *)
   8.136 +
   8.137 +fun flatten _ (ids, Elem (Fixes fixes)) =
   8.138 +      (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
   8.139 +  | flatten _ (ids, Elem elem) = (ids, [(("", []), Ext elem)])
   8.140 +  | flatten (ctxt, prep_expr) (ids, Expr expr) =
   8.141 +      apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
   8.142 +
   8.143  local
   8.144  
   8.145  local
   8.146 @@ -752,6 +796,9 @@
   8.147  
   8.148  local
   8.149  
   8.150 +(* CB: following code (norm_term, abstract_term, abstract_thm, bind_def)
   8.151 +   used in eval_text for defines elements. *)
   8.152 +
   8.153  val norm_term = Envir.beta_norm oo Term.subst_atomic;
   8.154  
   8.155  fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)
   8.156 @@ -845,12 +892,22 @@
   8.157  
   8.158  fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
   8.159    let
   8.160 +    (* CB: raw_elemss are list of pairs consisting of identifiers and
   8.161 +       context elements, the latter marked as internal or external. *)
   8.162      val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
   8.163 +    (* CB: raw_ctxt is context with additional fixed variables derived from
   8.164 +       the fixes elements in raw_elemss,
   8.165 +       raw_proppss contains assumptions and definitions from the
   8.166 +       (external?) elements in raw_elemss. *)
   8.167      val raw_propps = map flat raw_proppss;
   8.168      val raw_propp = flat raw_propps;
   8.169      val (ctxt, all_propp) =
   8.170        prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
   8.171 +    (* CB: read/cert entire proposition (conclusion and premises from
   8.172 +       the context elements). *)
   8.173      val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt;
   8.174 +    (* CB: it appears that terms declared in the propositions are added
   8.175 +       to the context here. *)
   8.176  
   8.177      val all_propp' = map2 (op ~~)
   8.178        (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
   8.179 @@ -863,9 +920,33 @@
   8.180        (map (ProofContext.default_type raw_ctxt) xs)
   8.181        (map (ProofContext.default_type ctxt) xs);
   8.182      val parms = param_types (xs ~~ typing);
   8.183 +    (* CB: parms are the parameters from raw_elemss, with correct typing. *)
   8.184  
   8.185 +    (* CB: extract information from assumes and defines elements
   8.186 +       (fixes and notes in raw_elemss don't have an effect on text and elemss),
   8.187 +       compute final form of context elements. *)
   8.188      val (text, elemss) = finish_elemss ctxt parms do_close
   8.189        (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);
   8.190 +    (* CB: text has the following structure:
   8.191 +           (((exts, exts'), (ints, ints')), (xs, env, defs))
   8.192 +       where
   8.193 +         exts: external assumptions (terms in external assumes elements)
   8.194 +         exts': dito, normalised wrt. env
   8.195 +         ints: internal assumptions (terms in internal assumes elements)
   8.196 +         ints': dito, normalised wrt. env
   8.197 +         xs: the free variables in exts' and ints' and rhss of definitions,
   8.198 +           this includes parameters except defined parameters
   8.199 +         env: list of term pairs encoding substitutions, where the first term
   8.200 +           is a free variable; substitutions represent defines elements and
   8.201 +           the rhs is normalised wrt. the previous env
   8.202 +         defs: theorems representing the substitutions from defines elements
   8.203 +           (thms are normalised wrt. env).
   8.204 +       elemss is an updated version of raw_elemss:
   8.205 +         - type info added to Fixes
   8.206 +         - axiom and definition statement replaced by corresponding one
   8.207 +           from proppss in Assumes and Defines
   8.208 +         - Facts unchanged
   8.209 +       *)
   8.210    in ((parms, elemss, concl), text) end;
   8.211  
   8.212  in
   8.213 @@ -881,6 +962,7 @@
   8.214  local
   8.215  
   8.216  fun prep_name ctxt (name, atts) =
   8.217 +  (* CB: reject qualified names in locale declarations *)
   8.218    if NameSpace.is_qualified name then
   8.219      raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
   8.220    else (name, atts);
   8.221 @@ -909,15 +991,12 @@
   8.222    let
   8.223      val sign = ProofContext.sign_of context;
   8.224  
   8.225 -    fun flatten (ids, Elem (Fixes fixes)) =
   8.226 -          (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
   8.227 -      | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
   8.228 -      | flatten (ids, Expr expr) =
   8.229 -          apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr));
   8.230 -
   8.231 -    val (import_ids, raw_import_elemss) = flatten ([], Expr import);
   8.232 +    val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import);
   8.233      (* CB: normalise "includes" among elements *)
   8.234 -    val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
   8.235 +    val raw_elemss = flat (#2 ((foldl_map (flatten (context, prep_expr sign))
   8.236 +      (import_ids, elements))));
   8.237 +    (* CB: raw_import_elemss @ raw_elemss is the normalised list of
   8.238 +       context elements obtained from import and elements. *)
   8.239      val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
   8.240        context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
   8.241      val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
   8.242 @@ -938,7 +1017,7 @@
   8.243      val thy = ProofContext.theory_of ctxt;
   8.244      val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
   8.245      val ((view_statement, view_axioms), fixed_params, import) =
   8.246 -(* view_axioms are xxx.axioms of locale xxx *)
   8.247 +(* CB: view_axioms are xxx.axioms of locale xxx *)
   8.248        (case locale of None => (([], []), [], empty)
   8.249        | Some name =>
   8.250            let val {view, params = (ps, _), ...} = the_locale thy name
   8.251 @@ -949,7 +1028,7 @@
   8.252  
   8.253  in
   8.254  
   8.255 -(* CB: arguments are: x->import, y->body (elements?), z->context *)
   8.256 +(* CB: arguments are: x->import, y->body (elements), z->context *)
   8.257  fun read_context x y z = #1 (gen_context true [] [] x y [] z);
   8.258  fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
   8.259  
   8.260 @@ -959,6 +1038,157 @@
   8.261  end;
   8.262  
   8.263  
   8.264 +(** CB: experimental instantiation mechanism **)
   8.265 +
   8.266 +fun instantiate loc_name prfx raw_inst ctxt =
   8.267 +  let
   8.268 +    val thy = ProofContext.theory_of ctxt;
   8.269 +    val sign = Theory.sign_of thy;
   8.270 +    val tsig = Sign.tsig_of sign;
   8.271 +    val cert = cterm_of sign;
   8.272 +
   8.273 +    (** process the locale **)
   8.274 +
   8.275 +    val {view = (_, axioms), params = (ps, _), ...} =
   8.276 +      the_locale thy (intern sign loc_name);
   8.277 +    val fixed_params = param_types ps;
   8.278 +    val (ids, raw_elemss) =
   8.279 +          flatten (ctxt, intern_expr sign) ([], Expr (Locale loc_name));
   8.280 +    val ((parms, all_elemss, concl),
   8.281 +         (spec as (_, (ints, _)), (xs, env, defs))) =
   8.282 +      read_elemss false (* do_close *) ctxt
   8.283 +        fixed_params (* could also put [] here??? *) raw_elemss
   8.284 +        [] (* concl *);
   8.285 +
   8.286 +    (** analyse the instantiation theorem inst **)
   8.287 +
   8.288 +    val inst = case raw_inst of
   8.289 +        None => if null ints
   8.290 +	  then None
   8.291 +	  else error "Locale has assumptions but no chained fact was found"
   8.292 +      | Some [] => if null ints
   8.293 +	  then None
   8.294 +	  else error "Locale has assumptions but no chained fact was found"
   8.295 +      | Some [thm] => if null ints
   8.296 +	  then (warning "Locale has no assumptions: fact ignored"; None)
   8.297 +	  else Some thm
   8.298 +      | Some _ => error "Multiple facts are not allowed";
   8.299 +
   8.300 +    val args = case inst of
   8.301 +            None => []
   8.302 +          | Some thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
   8.303 +              |> Term.strip_comb |> snd;
   8.304 +    val cargs = map cert args;
   8.305 +
   8.306 +    (* process parameters: match their types with those of arguments *)
   8.307 +
   8.308 +    val def_names = map (fn (Free (s, _), _) => s) env;
   8.309 +    val (defined, assumed) = partition
   8.310 +          (fn (s, _) => s mem def_names) fixed_params;
   8.311 +    val cassumed = map (cert o Free) assumed;
   8.312 +    val cdefined = map (cert o Free) defined;
   8.313 +
   8.314 +    val param_types = map snd assumed;
   8.315 +    val v_param_types = map Type.varifyT param_types;
   8.316 +    val arg_types = map Term.fastype_of args;
   8.317 +    val Tenv = foldl (Type.typ_match tsig)
   8.318 +          (Vartab.empty, v_param_types ~~ arg_types)
   8.319 +          handle Library.LIST "~~" => error "Number of parameters does not match number of arguments of chained fact";
   8.320 +    (* get their sorts *)
   8.321 +    val tfrees = foldr Term.add_typ_tfrees (param_types, []);
   8.322 +    val Tenv' = map
   8.323 +          (fn ((a, i), T) => ((a, the (assoc_string (tfrees, a))), T))
   8.324 +          (Vartab.dest Tenv);
   8.325 +
   8.326 +    (* process (internal) elements *)
   8.327 +
   8.328 +    fun inst_type [] T = T
   8.329 +      | inst_type env T =
   8.330 +          Term.map_type_tfree (fn v => if_none (assoc (env, v)) (TFree v)) T;
   8.331 +
   8.332 +    fun inst_term [] t = t
   8.333 +      | inst_term env t = Term.map_term_types (inst_type env) t;
   8.334 +
   8.335 +    (* parameters with argument types *)
   8.336 +
   8.337 +    val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed;
   8.338 +    val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined;
   8.339 +    val cdefining = map (cert o inst_term Tenv' o snd) env;
   8.340 +
   8.341 +    fun inst_thm _ [] th = th
   8.342 +      | inst_thm ctxt Tenv th =
   8.343 +	  let
   8.344 +	    val sign = ProofContext.sign_of ctxt;
   8.345 +	    val cert = Thm.cterm_of sign;
   8.346 +	    val certT = Thm.ctyp_of sign;
   8.347 +	    val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
   8.348 +	    val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []);
   8.349 +	    val Tenv' = filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
   8.350 +	  in
   8.351 +	    if null Tenv' then th
   8.352 +	    else
   8.353 +	      th
   8.354 +	      |> Drule.implies_intr_list (map cert hyps)
   8.355 +	      |> Drule.tvars_intr_list (map (#1 o #1) Tenv')
   8.356 +	      |> (fn (th', al) => th' |>
   8.357 +		Thm.instantiate ((map (fn ((a, _), T) =>
   8.358 +                  (the (assoc (al, a)), certT T)) Tenv'), []))
   8.359 +	      |> (fn th'' => Drule.implies_elim_list th''
   8.360 +		  (map (Thm.assume o cert o inst_term Tenv') hyps))
   8.361 +	  end;
   8.362 +
   8.363 +    fun inst_thm' thm =
   8.364 +      let
   8.365 +        (* not all axs are normally applicable *)
   8.366 +        val hyps = #hyps (rep_thm thm);
   8.367 +        val ass = map (fn ax => (prop_of ax, ax)) axioms;
   8.368 +        val axs' = foldl (fn (axs, hyp) => 
   8.369 +              (case assoc (ass, hyp) of None => axs
   8.370 +                 | Some ax => axs @ [ax])) ([], hyps);
   8.371 +        val thm' = Drule.satisfy_hyps axs' thm;
   8.372 +        (* instantiate types *)
   8.373 +        val thm'' = inst_thm ctxt Tenv' thm';
   8.374 +        (* substitute arguments and discharge hypotheses *)
   8.375 +        val thm''' = case inst of
   8.376 +                None => thm''
   8.377 +              | Some inst_thm => let
   8.378 +		    val hyps = #hyps (rep_thm thm'');
   8.379 +		    val th = thm'' |> implies_intr_hyps
   8.380 +		      |> forall_intr_list (cparams' @ cdefined')
   8.381 +		      |> forall_elim_list (cargs @ cdefining)
   8.382 +		    (* th has premises of the form either inst_thm or x==x *)
   8.383 +		    fun mk hyp = if Logic.is_equals hyp
   8.384 +			  then hyp |> Logic.dest_equals |> snd |> cert
   8.385 +				 |> reflexive
   8.386 +			  else inst_thm
   8.387 +                  in implies_elim_list th (map mk hyps)
   8.388 +                  end;
   8.389 +      in thm''' end;
   8.390 +
   8.391 +    fun inst_elem (ctxt, (Ext _)) = ctxt
   8.392 +      | inst_elem (ctxt, (Int (Notes facts))) =
   8.393 +              (* instantiate fact *)
   8.394 +          let val facts' =
   8.395 +              map (apsnd (map (apfst (map inst_thm')))) facts
   8.396 +              (* rename fact *)
   8.397 +              val facts'' =
   8.398 +              map (apfst (apfst (fn "" => ""
   8.399 +                                  | s => NameSpace.append prfx s)))
   8.400 +                  facts'
   8.401 +          in fst (ProofContext.have_thmss_i facts'' ctxt)
   8.402 +          end
   8.403 +      | inst_elem (ctxt, (Int _)) = ctxt;
   8.404 +
   8.405 +    fun inst_elems (ctxt, (id, elems)) = foldl inst_elem (ctxt, elems);
   8.406 +
   8.407 +    fun inst_elemss ctxt elemss = foldl inst_elems (ctxt, elemss);
   8.408 +
   8.409 +    (* main part *)
   8.410 +
   8.411 +    val ctxt' = ProofContext.qualified true ctxt;
   8.412 +  in ProofContext.restore_qualified ctxt (inst_elemss ctxt' all_elemss)
   8.413 +  end;
   8.414 +
   8.415  
   8.416  (** define locales **)
   8.417  
   8.418 @@ -1019,6 +1249,7 @@
   8.419  
   8.420  fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind)
   8.421    | smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc;
   8.422 +  (* CB: only used in Proof.finish_global. *)
   8.423  
   8.424  end;
   8.425  
   8.426 @@ -1050,6 +1281,8 @@
   8.427  
   8.428  val have_thmss = gen_have_thmss intern ProofContext.get_thms;
   8.429  val have_thmss_i = gen_have_thmss (K I) (K I);
   8.430 +  (* CB: have_thmss(_i) is the base for the Isar commands
   8.431 +     "theorems (in loc)" and "declare (in loc)". *)
   8.432  
   8.433  fun add_thmss loc args (thy, ctxt) =
   8.434    let
   8.435 @@ -1059,6 +1292,7 @@
   8.436      val ((ctxt', _), (_, facts')) =
   8.437        activate_facts (K I) ((ctxt, view_axioms), [(("", []), [Notes args'])]);
   8.438    in ((thy', ctxt'), facts') end;
   8.439 +  (* CB: only used in Proof.finish_global. *)
   8.440  
   8.441  end;
   8.442  
     9.1 --- a/src/Pure/Isar/method.ML	Fri Apr 02 12:25:48 2004 +0200
     9.2 +++ b/src/Pure/Isar/method.ML	Fri Apr 02 14:08:30 2004 +0200
     9.3 @@ -368,7 +368,8 @@
     9.4  	val params = Logic.strip_params Bi
     9.5  			     (* params of subgoal i as string typ pairs *)
     9.6  	val params = rev(Term.rename_wrt_term Bi params)
     9.7 -						 (* as they are printed *)
     9.8 +			   (* as they are printed: bound variables with *)
     9.9 +                           (* the same name are renamed during printing *)
    9.10          fun types' (a, ~1) = (case assoc (params, a) of
    9.11                  None => types (a, ~1)
    9.12                | some => some)
    10.1 --- a/src/Pure/Isar/outer_parse.ML	Fri Apr 02 12:25:48 2004 +0200
    10.2 +++ b/src/Pure/Isar/outer_parse.ML	Fri Apr 02 14:08:30 2004 +0200
    10.3 @@ -174,7 +174,8 @@
    10.4  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    10.5  
    10.6  val uname = underscore >> K None || name >> Some;
    10.7 -
    10.8 +  (* CB: underscore yields None, any other name Some with that string.
    10.9 +     Used, for example, in the renaming of locale parameters.  *)
   10.10  
   10.11  (* sorts and arities *)
   10.12  
    11.1 --- a/src/Pure/Isar/proof.ML	Fri Apr 02 12:25:48 2004 +0200
    11.2 +++ b/src/Pure/Isar/proof.ML	Fri Apr 02 14:08:30 2004 +0200
    11.3 @@ -65,6 +65,7 @@
    11.4      (thm list * context attribute list) list) list -> state -> state
    11.5    val using_thmss: ((xstring * context attribute list) list) list -> state -> state
    11.6    val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
    11.7 +  val instantiate_locale: string * string -> state -> state
    11.8    val fix: (string list * string option) list -> state -> state
    11.9    val fix_i: (string list * typ option) list -> state -> state
   11.10    val assm: ProofContext.exporter
   11.11 @@ -510,6 +511,7 @@
   11.12  
   11.13  
   11.14  (* have_thmss *)
   11.15 +(* CB: this implements "note" of the Isar/VM *)
   11.16  
   11.17  local
   11.18  
   11.19 @@ -565,6 +567,19 @@
   11.20  end;
   11.21  
   11.22  
   11.23 +(* locale instantiation *)
   11.24 +
   11.25 +fun instantiate_locale (loc_name, prfx) state = let
   11.26 +    val ctxt = context_of state;
   11.27 +    val facts = if is_chain state then get_facts state else None;
   11.28 +  in
   11.29 +    state
   11.30 +    |> assert_forward_or_chain
   11.31 +    |> enter_forward
   11.32 +    |> reset_facts
   11.33 +    |> map_context (Locale.instantiate loc_name prfx facts)
   11.34 +  end;
   11.35 +
   11.36  (* fix *)
   11.37  
   11.38  fun gen_fix f xs state =
    12.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 02 12:25:48 2004 +0200
    12.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Apr 02 14:08:30 2004 +0200
    12.3 @@ -160,9 +160,17 @@
    12.4        ((cterm list * exporter) list *                         (*assumes: A ==> _*)
    12.5          (string * thm list) list) *
    12.6        (string * string) list,                                 (*fixes: !!x. _*)
    12.7 +    (* CB: asms is of the form ((asms, prems), fixed) *)
    12.8      binds: (term * typ) option Vartab.table,                  (*term bindings*)
    12.9      thms: bool * NameSpace.T * thm list option Symtab.table
   12.10        * FactIndex.T,                                          (*local thms*)
   12.11 +    (* CB: thms is of the form (q, n, t, i) where
   12.12 +       q: indicates whether theorems with qualified names may be stored;
   12.13 +          this is initially forbidden (false); flag may be changed with
   12.14 +          qualified and restore_qualified;
   12.15 +       n: theorem namespace;
   12.16 +       t: table of theorems;
   12.17 +       i: index for theorem lookup (find theorem command) *) 
   12.18      cases: (string * RuleCases.T) list,                       (*local contexts*)
   12.19      defs:
   12.20        typ Vartab.table *                                      (*type constraints*)
   12.21 @@ -1215,6 +1223,8 @@
   12.22  
   12.23  end;
   12.24  
   12.25 +(* CB: fix free variables occuring in ts, unless already fixed. *)
   12.26 +
   12.27  fun fix_frees ts ctxt =
   12.28    let
   12.29      val frees = foldl Term.add_frees ([], ts);