Further work on interpretation commands. New command `interpret' for
authorballarin
Thu Mar 24 17:03:37 2005 +0100 (2005-03-24 ago)
changeset 15624484178635bd8
parent 15623 8b40f741597c
child 15625 43f1669cbae3
Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/FOL/ex/LocaleTest.thy
src/Pure/General/name_space.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
     1.1 --- a/etc/isar-keywords-ZF.el	Thu Mar 24 16:36:40 2005 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Thu Mar 24 17:03:37 2005 +0100
     1.3 @@ -74,6 +74,7 @@
     1.4      "init_toplevel"
     1.5      "instance"
     1.6      "instantiate"
     1.7 +    "interpret"
     1.8      "interpretation"
     1.9      "judgment"
    1.10      "kill"
    1.11 @@ -389,6 +390,7 @@
    1.12  (defconst isar-keywords-proof-goal
    1.13    '("have"
    1.14      "hence"
    1.15 +    "interpret"
    1.16      "show"
    1.17      "thus"))
    1.18  
     2.1 --- a/etc/isar-keywords.el	Thu Mar 24 16:36:40 2005 +0100
     2.2 +++ b/etc/isar-keywords.el	Thu Mar 24 17:03:37 2005 +0100
     2.3 @@ -77,6 +77,7 @@
     2.4      "init_toplevel"
     2.5      "instance"
     2.6      "instantiate"
     2.7 +    "interpret"
     2.8      "interpretation"
     2.9      "judgment"
    2.10      "kill"
    2.11 @@ -423,6 +424,7 @@
    2.12  (defconst isar-keywords-proof-goal
    2.13    '("have"
    2.14      "hence"
    2.15 +    "interpret"
    2.16      "show"
    2.17      "thus"))
    2.18  
     3.1 --- a/src/FOL/ex/LocaleTest.thy	Thu Mar 24 16:36:40 2005 +0100
     3.2 +++ b/src/FOL/ex/LocaleTest.thy	Thu Mar 24 17:03:37 2005 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4  print_interps L
     3.5  print_interps M
     3.6  
     3.7 -interpretation test [simp]: L .
     3.8 +interpretation test [simp]: L print_interps M .
     3.9  
    3.10  interpretation L .
    3.11  
    3.12 @@ -52,8 +52,19 @@
    3.13  
    3.14  print_interps A
    3.15  
    3.16 -(*
    3.17 -thm asm_A a.asm_A p1.a.asm_A
    3.18 +(* possible accesses
    3.19 +thm p1.a.asm_A thm LocaleTest.p1.a.asm_A
    3.20 +thm LocaleTest.asm_A thm p1.asm_A
    3.21 +*)
    3.22 +
    3.23 +(* without prefix *)
    3.24 +
    3.25 +interpretation C ["W::'b" "Z::'b"] by (auto intro: A.intro C_axioms.intro)
    3.26 +
    3.27 +print_interps A
    3.28 +
    3.29 +(* possible accesses
    3.30 +thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A
    3.31  *)
    3.32  
    3.33  interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute)
    3.34 @@ -64,7 +75,7 @@
    3.35  thm p2.a.asm_A
    3.36  *)
    3.37  
    3.38 -interpretation p3: D [X Y] by (auto intro: A.intro)
    3.39 +interpretation p3: D [X Y] .
    3.40  
    3.41  (* duplicate: not registered *)
    3.42  (*
    3.43 @@ -87,4 +98,18 @@
    3.44  interpretation A [Z] apply - apply (auto intro: A.intro) done
    3.45  *)
    3.46  
    3.47 +theorem True
    3.48 +proof -
    3.49 +  fix alpha::i and beta::i and gamma::i
    3.50 +  assume "A(alpha)"
    3.51 +  then interpret p5: A [alpha] .
    3.52 +  print_interps A
    3.53 +  interpret p6: C [alpha beta] by (auto intro: C_axioms.intro)
    3.54 +  print_interps A   (* p6 not added! *)
    3.55 +  print_interps C
    3.56 +qed rule
    3.57 +
    3.58 +(* lemma "bla.bla": True by rule *)
    3.59 +
    3.60 +
    3.61  end
     4.1 --- a/src/Pure/General/name_space.ML	Thu Mar 24 16:36:40 2005 +0100
     4.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 24 17:03:37 2005 +0100
     4.3 @@ -24,6 +24,7 @@
     4.4    type T
     4.5    val empty: T
     4.6    val extend: T * string list -> T
     4.7 +  val extend': (string -> string list) -> T * string list -> T
     4.8    val merge: T * T -> T
     4.9    val hide: bool -> T * string list -> T
    4.10    val intern: T -> string -> string
    4.11 @@ -97,12 +98,15 @@
    4.12  
    4.13  (* extend *)            (*later entries preferred*)
    4.14  
    4.15 -fun extend_aux (name, tab) =
    4.16 +fun gen_extend_aux acc (name, tab) =
    4.17    if is_hidden name then
    4.18      error ("Attempt to declare hidden name " ^ quote name)
    4.19 -  else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name);
    4.20 +  else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, acc name);
    4.21  
    4.22 -fun extend (NameSpace tab, names) = NameSpace (foldr extend_aux tab names);
    4.23 +fun extend' acc (NameSpace tab, names) =
    4.24 +  NameSpace (foldr (gen_extend_aux acc) tab names);
    4.25 +fun extend (NameSpace tab, names) =
    4.26 +  NameSpace (foldr (gen_extend_aux accesses) tab names);
    4.27  
    4.28  
    4.29  (* merge *)             (*1st preferred over 2nd*)
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 24 16:36:40 2005 +0100
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 24 17:03:37 2005 +0100
     5.3 @@ -222,10 +222,9 @@
     5.4      Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body)
     5.5    end);
     5.6  
     5.7 -fun print_registrations name = Toplevel.unknown_theory o
     5.8 -  Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in
     5.9 -    Locale.print_global_registrations thy name
    5.10 -  end);
    5.11 +fun print_registrations name = Toplevel.unknown_context o
    5.12 +  Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations name)
    5.13 +    (Locale.print_local_registrations name o Proof.context_of));
    5.14  
    5.15  val print_attributes = Toplevel.unknown_theory o
    5.16    Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 24 16:36:40 2005 +0100
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 24 17:03:37 2005 +0100
     6.3 @@ -317,11 +317,17 @@
     6.4  
     6.5  val interpretationP =
     6.6    OuterSyntax.command "interpretation"
     6.7 -  "prove and register interpretation of locale expression" K.thy_goal
     6.8 +  "prove and register interpretation of locale expression in theory" K.thy_goal
     6.9    ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
    6.10       >> IsarThy.register_globally)
    6.11     >> (Toplevel.print oo Toplevel.theory_to_proof));
    6.12  
    6.13 +val interpretP =
    6.14 +  OuterSyntax.command "interpret"
    6.15 +    "prove and register interpretation of locale expression in context"
    6.16 +    K.prf_goal
    6.17 +    (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val >>
    6.18 +      ((Toplevel.print oo Toplevel.proof) o IsarThy.register_locally));
    6.19  
    6.20  (** proof commands **)
    6.21  
    6.22 @@ -800,7 +806,7 @@
    6.23    default_proofP, immediate_proofP, done_proofP, skip_proofP,
    6.24    forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
    6.25    finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
    6.26 -  redoP, undos_proofP, undoP, killP, interpretationP, instantiateP,
    6.27 +  redoP, undos_proofP, undoP, killP, interpretationP, interpretP, instantiateP,
    6.28    (*diagnostic commands*)
    6.29    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    6.30    print_syntaxP, print_theoremsP, print_localesP, print_localeP,
     7.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Mar 24 16:36:40 2005 +0100
     7.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 24 17:03:37 2005 +0100
     7.3 @@ -157,6 +157,9 @@
     7.4    val register_globally:
     7.5      ((string * Args.src list) * Locale.expr) * string option list ->
     7.6      bool -> theory -> ProofHistory.T
     7.7 +  val register_locally:
     7.8 +    ((string * Args.src list) * Locale.expr) * string option list ->
     7.9 +    ProofHistory.T -> ProofHistory.T
    7.10  
    7.11  end;
    7.12  
    7.13 @@ -625,16 +628,16 @@
    7.14  val context = init_context (ThyInfo.quiet_update_thy true);
    7.15  
    7.16  
    7.17 -(* global registration of locale interpretation *)
    7.18 +(* registration of locale interpretation *)
    7.19  
    7.20 -fun register_globally (((prfx, atts), expr), insts) b (* bool *) thy =
    7.21 +fun register_globally (((prfx, atts), expr), insts) b thy =
    7.22    let
    7.23 -    val (thy', propss, activate) = Locale.prep_registration
    7.24 +    val (thy', propss, activate) = Locale.prep_global_registration
    7.25            (prfx, map (Attrib.global_attribute thy) atts) expr insts thy;
    7.26      fun witness id (thy, thm) = let
    7.27          val thm' = Drule.freeze_all thm;
    7.28        in
    7.29 -        (Locale.global_add_witness id thm' thy, thm')
    7.30 +        (Locale.add_global_witness id thm' thy, thm')
    7.31        end;
    7.32    in
    7.33      multi_theorem_i Drule.internalK activate ("", []) [] 
    7.34 @@ -642,5 +645,18 @@
    7.35          map (fn prop => (prop, ([], []))) props)) propss) b thy'
    7.36    end;
    7.37  
    7.38 +fun register_locally (((prfx, atts), expr), insts) =
    7.39 +  ProofHistory.apply (fn state =>
    7.40 +    let
    7.41 +      val ctxt = Proof.context_of state;
    7.42 +      val (ctxt', propss, activate) = Locale.prep_local_registration
    7.43 +            (prfx, map (Attrib.local_attribute' ctxt) atts) expr insts ctxt;
    7.44 +      fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm);
    7.45 +    in state
    7.46 +      |> Proof.map_context (fn _ => ctxt')
    7.47 +      |> Proof.interpret_i activate Seq.single true
    7.48 +           (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
    7.49 +             map (fn prop => (prop, ([], []))) props)) propss)
    7.50 +    end);
    7.51  
    7.52  end;
     8.1 --- a/src/Pure/Isar/locale.ML	Thu Mar 24 16:36:40 2005 +0100
     8.2 +++ b/src/Pure/Isar/locale.ML	Thu Mar 24 17:03:37 2005 +0100
     8.3 @@ -68,7 +68,8 @@
     8.4    (* Diagnostic functions *)
     8.5    val print_locales: theory -> unit
     8.6    val print_locale: theory -> expr -> multi_attribute element list -> unit
     8.7 -  val print_global_registrations: theory -> string -> unit
     8.8 +  val print_global_registrations: string -> theory -> unit
     8.9 +  val print_local_registrations: string -> context -> unit
    8.10  
    8.11    val add_locale: bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
    8.12    val add_locale_i: bool -> bstring -> expr -> multi_attribute element_i list
    8.13 @@ -85,14 +86,21 @@
    8.14    val add_thmss: string -> ((string * thm list) * multi_attribute list) list ->
    8.15      theory * context -> (theory * context) * (string * thm list) list
    8.16  
    8.17 +  (* Locale interpretation *)
    8.18    val instantiate: string -> string * context attribute list
    8.19      -> thm list option -> context -> context
    8.20 -  val prep_registration:
    8.21 +  val prep_global_registration:
    8.22      string * theory attribute list -> expr -> string option list -> theory ->
    8.23      theory * ((string * term list) * term list) list * (theory -> theory)
    8.24 -  val global_add_witness:
    8.25 +  val prep_local_registration:
    8.26 +    string * context attribute list -> expr -> string option list -> context ->
    8.27 +    context * ((string * term list) * term list) list * (context -> context)
    8.28 +  val add_global_witness:
    8.29      string * term list -> thm -> theory -> theory
    8.30 +  val add_local_witness:
    8.31 +    string * term list -> thm -> context -> context
    8.32  
    8.33 +  (* Theory setup for locales *)
    8.34    val setup: (theory -> theory) list
    8.35  end;
    8.36  
    8.37 @@ -138,7 +146,7 @@
    8.38         (cf. [1], normalisation of locale expressions.)
    8.39      *)
    8.40    import: expr,                                       (*dynamic import*)
    8.41 -  elems: (multi_attribute element_i * stamp) list,  (*static content*)
    8.42 +  elems: (multi_attribute element_i * stamp) list,    (*static content*)
    8.43    params: (string * typ option) list * string list}   (*all/local params*)
    8.44  
    8.45  
    8.46 @@ -147,7 +155,7 @@
    8.47  structure Termlisttab = TableFun(type key = term list
    8.48    val ord = Library.list_ord Term.term_ord);
    8.49  
    8.50 -structure LocalesArgs =
    8.51 +structure GlobalLocalesArgs =
    8.52  struct
    8.53    val name = "Isar/locales";
    8.54    type T = NameSpace.T * locale Symtab.table *
    8.55 @@ -180,24 +188,41 @@
    8.56      |> Pretty.writeln;
    8.57  end;
    8.58  
    8.59 -structure LocalesData = TheoryDataFun(LocalesArgs);
    8.60 -val print_locales = LocalesData.print;
    8.61 +structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs);
    8.62 +
    8.63 +(** context data **)
    8.64  
    8.65 -val intern = NameSpace.intern o #1 o LocalesData.get_sg;
    8.66 -val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg;
    8.67 +structure LocalLocalesArgs =
    8.68 +struct
    8.69 +  val name = "Isar/locales";
    8.70 +  type T = ((string * context attribute list) * thm list) Termlisttab.table
    8.71 +           Symtab.table;
    8.72 +    (* registrations: theorems instantiating locale assumptions,
    8.73 +         with prefix and attributes, indexed by locale name and parameter
    8.74 +         instantiation *)
    8.75 +  fun init _ = Symtab.empty;
    8.76 +  fun print _ _ = ();
    8.77 +end;
    8.78 +
    8.79 +structure LocalLocalesData = ProofDataFun(LocalLocalesArgs);
    8.80  
    8.81  
    8.82  (* access locales *)
    8.83  
    8.84 +val print_locales = GlobalLocalesData.print;
    8.85 +
    8.86 +val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg;
    8.87 +val cond_extern = NameSpace.cond_extern o #1 o GlobalLocalesData.get_sg;
    8.88 +
    8.89  fun declare_locale name =
    8.90 -  LocalesData.map (fn (space, locs, regs) =>
    8.91 +  GlobalLocalesData.map (fn (space, locs, regs) =>
    8.92      (NameSpace.extend (space, [name]), locs, regs));
    8.93  
    8.94  fun put_locale name loc =
    8.95 -  LocalesData.map (fn (space, locs, regs) =>
    8.96 +  GlobalLocalesData.map (fn (space, locs, regs) =>
    8.97      (space, Symtab.update ((name, loc), locs), regs));
    8.98  
    8.99 -fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name);
   8.100 +fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name);
   8.101  
   8.102  fun the_locale thy name =
   8.103    (case get_locale thy name of
   8.104 @@ -207,34 +232,73 @@
   8.105  
   8.106  (* access registrations *)
   8.107  
   8.108 -(* add registration to theory, ignored if already present *)
   8.109 +(* retrieve registration from theory or context *)
   8.110 +
   8.111 +fun gen_get_registration get thy_ctxt (name, ps) =
   8.112 +  case Symtab.lookup (get thy_ctxt, name) of
   8.113 +      NONE => NONE
   8.114 +    | SOME tab => Termlisttab.lookup (tab, ps);
   8.115 +
   8.116 +val get_global_registration =
   8.117 +     gen_get_registration (#3 o GlobalLocalesData.get);
   8.118 +val get_local_registration =
   8.119 +     gen_get_registration LocalLocalesData.get;
   8.120  
   8.121 -fun global_put_registration (name, ps) attn =
   8.122 -  LocalesData.map (fn (space, locs, regs) =>
   8.123 -    (space, locs, let
   8.124 +val test_global_registration = isSome oo get_global_registration;
   8.125 +val test_local_registration = isSome oo get_local_registration;
   8.126 +fun smart_test_registration ctxt id =
   8.127 +  let
   8.128 +    val thy = ProofContext.theory_of ctxt;
   8.129 +  in
   8.130 +    test_global_registration thy id orelse test_local_registration ctxt id
   8.131 +  end;
   8.132 +
   8.133 +
   8.134 +(* add registration to theory or context, ignored if already present *)
   8.135 +
   8.136 +fun gen_put_registration map (name, ps) attn =
   8.137 +  map (fn regs =>
   8.138 +      let
   8.139          val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty);
   8.140        in
   8.141          Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)),
   8.142            regs)
   8.143 -      end handle Termlisttab.DUP _ => regs));
   8.144 +      end handle Termlisttab.DUP _ => regs);
   8.145 +
   8.146 +val put_global_registration =
   8.147 +     gen_put_registration (fn f =>
   8.148 +       GlobalLocalesData.map (fn (space, locs, regs) =>
   8.149 +         (space, locs, f regs)));
   8.150 +val put_local_registration = gen_put_registration LocalLocalesData.map;
   8.151  
   8.152 -(* add witness theorem to registration in theory,
   8.153 +fun smart_put_registration id attn ctxt =
   8.154 +  (* ignore registration if already present in theory *)
   8.155 +     let
   8.156 +       val thy = ProofContext.theory_of ctxt;
   8.157 +     in case get_global_registration thy id of
   8.158 +          NONE => put_local_registration id attn ctxt
   8.159 +        | SOME _ => ctxt
   8.160 +     end;
   8.161 +
   8.162 +
   8.163 +(* add witness theorem to registration in theory or context,
   8.164     ignored if registration not present *)
   8.165  
   8.166 -fun global_add_witness (name, ps) thm =
   8.167 -  LocalesData.map (fn (space, locs, regs) =>
   8.168 -    (space, locs, let
   8.169 +fun gen_add_witness map (name, ps) thm =
   8.170 +  map (fn regs =>
   8.171 +      let
   8.172          val tab = valOf (Symtab.lookup (regs, name));
   8.173          val (x, thms) = valOf (Termlisttab.lookup (tab, ps));
   8.174        in
   8.175          Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)),
   8.176            regs)
   8.177 -      end handle Option => regs))
   8.178 +      end handle Option => regs);
   8.179  
   8.180 -fun global_get_registration thy (name, ps) =
   8.181 -  case Symtab.lookup (#3 (LocalesData.get thy), name) of
   8.182 -      NONE => NONE
   8.183 -    | SOME tab => Termlisttab.lookup (tab, ps);
   8.184 +val add_global_witness =
   8.185 +     gen_add_witness (fn f =>
   8.186 +       GlobalLocalesData.map (fn (space, locs, regs) =>
   8.187 +         (space, locs, f regs)));
   8.188 +val add_local_witness = gen_add_witness LocalLocalesData.map;
   8.189  
   8.190  
   8.191  (* import hierarchy
   8.192 @@ -255,28 +319,36 @@
   8.193    end;
   8.194  
   8.195  
   8.196 -(* registrations *)
   8.197 +(* printing of registrations *)
   8.198  
   8.199 -fun print_global_registrations thy loc =
   8.200 +fun gen_print_registrations get_regs get_sign msg loc thy_ctxt =
   8.201    let
   8.202 -    val sg = Theory.sign_of thy;
   8.203 +    val sg = get_sign thy_ctxt;
   8.204      val loc_int = intern sg loc;
   8.205 -    val (_, _, regs) = LocalesData.get thy;
   8.206 +    val regs = get_regs thy_ctxt;
   8.207      val prt_term = Pretty.quote o Sign.pretty_term sg;
   8.208 -    fun prt_inst (ts, ((prfx, _), thms)) = let
   8.209 -in
   8.210 +    fun prt_inst (ts, ((prfx, _), thms)) =
   8.211        Pretty.block [Pretty.str prfx, Pretty.str ":", Pretty.brk 1,
   8.212 -        Pretty.list "(" ")" (map prt_term ts)]
   8.213 -end;
   8.214 +        Pretty.list "(" ")" (map prt_term ts)];
   8.215      val loc_regs = Symtab.lookup (regs, loc_int);
   8.216    in
   8.217      (case loc_regs of
   8.218 -        NONE => Pretty.str "No interpretations."
   8.219 -      | SOME r => Pretty.big_list "interpretations:"
   8.220 +        NONE => Pretty.str ("No interpretations in " ^ msg ^ ".")
   8.221 +      | SOME r => Pretty.big_list ("Interpretations in " ^ msg ^ ":")
   8.222            (map prt_inst (Termlisttab.dest r)))
   8.223      |> Pretty.writeln
   8.224    end;
   8.225  
   8.226 +val print_global_registrations =
   8.227 +     gen_print_registrations (#3 o GlobalLocalesData.get)
   8.228 +       Theory.sign_of "theory";
   8.229 +val print_local_registrations' =
   8.230 +     gen_print_registrations LocalLocalesData.get
   8.231 +       ProofContext.sign_of "context";
   8.232 +fun print_local_registrations loc ctxt =
   8.233 +  (print_global_registrations loc (ProofContext.theory_of ctxt);
   8.234 +   print_local_registrations' loc ctxt);
   8.235 +
   8.236  
   8.237  (* diagnostics *)
   8.238  
   8.239 @@ -1747,53 +1819,83 @@
   8.240  fun extract_asms_elemss elemss =
   8.241        map extract_asms_elems elemss;
   8.242  
   8.243 -(* add registration, without theorems, to theory *)
   8.244 -
   8.245 -fun prep_reg_global attn (thy, (id, _)) =
   8.246 -      global_put_registration id attn thy;
   8.247 -
   8.248 -(* activate instantiated facts in theory *)
   8.249 +(* activate instantiated facts in theory or context *)
   8.250  
   8.251 -fun activate_facts_elem _ _ (thy, Fixes _) = thy
   8.252 -  | activate_facts_elem _ _ (thy, Assumes _) = thy
   8.253 -  | activate_facts_elem _ _ (thy, Defines _) = thy
   8.254 -  | activate_facts_elem disch (prfx, atts) (thy, Notes facts) =
   8.255 +fun activate_facts_elem _ _ _ _ (thy_ctxt, Fixes _) = thy_ctxt
   8.256 +  | activate_facts_elem _ _ _ _ (thy_ctxt, Assumes _) = thy_ctxt
   8.257 +  | activate_facts_elem _ _ _ _ (thy_ctxt, Defines _) = thy_ctxt
   8.258 +  | activate_facts_elem note_thmss which
   8.259 +        disch (prfx, atts) (thy_ctxt, Notes facts) =
   8.260        let
   8.261 -        (* extract theory attributes *)
   8.262 -        val (Notes facts) = map_attrib_element_i fst (Notes facts);
   8.263 +        (* extract theory or context attributes *)
   8.264 +        val (Notes facts) = map_attrib_element_i which (Notes facts);
   8.265          (* add attributs from registration *)
   8.266          val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
   8.267          (* discharge hyps and varify *)
   8.268 -        val facts'' = map (apsnd (map (apfst (map (Drule.standard o disch))))) facts';
   8.269 +        val facts'' = map (apsnd (map (apfst (map disch)))) facts';
   8.270 +        (* prefix names *)
   8.271 +        val facts''' = map (apfst (apfst (fn name =>
   8.272 +          if prfx = "" orelse name = "" then name
   8.273 +          else NameSpace.pack [prfx, name]))) facts'';
   8.274        in
   8.275 -        fst (note_thmss_qualified' "" prfx facts'' thy)
   8.276 +        fst (note_thmss prfx facts''' thy_ctxt)
   8.277        end;
   8.278  
   8.279 -fun activate_facts_elems disch (thy, (id, elems)) =
   8.280 +fun activate_facts_elems get_reg note_thmss which
   8.281 +        disch (thy_ctxt, (id, elems)) =
   8.282        let
   8.283 -        val ((prfx, atts2), _) = valOf (global_get_registration thy id)
   8.284 +        val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id)
   8.285            handle Option => error ("(internal) unknown registration of " ^
   8.286              quote (fst id) ^ " while activating facts.");
   8.287        in
   8.288 -        Library.foldl (activate_facts_elem disch (prfx, atts2)) (thy, elems)
   8.289 +        Library.foldl (activate_facts_elem note_thmss which
   8.290 +          disch (prfx, atts2)) (thy_ctxt, elems)
   8.291        end;
   8.292  
   8.293 -fun activate_facts_elemss all_elemss new_elemss thy =
   8.294 +fun gen_activate_facts_elemss get_reg note_thmss which standard
   8.295 +        all_elemss new_elemss thy_ctxt =
   8.296        let
   8.297          val prems = List.concat (List.mapPartial (fn (id, _) =>
   8.298 -              Option.map snd (global_get_registration thy id)
   8.299 +              Option.map snd (get_reg thy_ctxt id)
   8.300                  handle Option => error ("(internal) unknown registration of " ^
   8.301                    quote (fst id) ^ " while activating facts.")) all_elemss);
   8.302 -      in Library.foldl (activate_facts_elems (Drule.satisfy_hyps prems))
   8.303 -        (thy, new_elemss) end;
   8.304 -
   8.305 -in
   8.306 +      in Library.foldl (activate_facts_elems get_reg note_thmss which
   8.307 +        (standard o Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end;
   8.308  
   8.309 -fun prep_registration attn expr insts thy =
   8.310 +fun loc_accesses prfx name =
   8.311 +  (* full qualified name is T.p.r.n where
   8.312 +       T: theory name, p: interpretation prefix, r: renaming prefix, n: name
   8.313 +  *)
   8.314 +     if prfx = "" then
   8.315 +       case NameSpace.unpack name of
   8.316 +	   [] => [""]
   8.317 +	 | [T, n] => map NameSpace.pack [[T, n], [n]]
   8.318 +	 | [T, r, n] => map NameSpace.pack [[T, r, n], (*[T, n],*) [r, n], [n]]
   8.319 +	 | _ => error ("Locale accesses: illegal name " ^ quote name)
   8.320 +     else case NameSpace.unpack name of
   8.321 +           [] => [""]
   8.322 +         | [T, p, n] => map NameSpace.pack [[T, p, n], [p, n]]
   8.323 +         | [T, p, r, n] => map NameSpace.pack
   8.324 +             [[T, p, r, n], [T, p, n], [p, r, n], [p, n]]
   8.325 +         | _ => error ("Locale accesses: illegal name " ^ quote name);
   8.326 +
   8.327 +val global_activate_facts_elemss = gen_activate_facts_elemss
   8.328 +      get_global_registration
   8.329 +      (fn prfx => PureThy.note_thmss_qualified_i (loc_accesses prfx)
   8.330 +        (Drule.kind ""))
   8.331 +      fst Drule.standard;
   8.332 +val local_activate_facts_elemss = gen_activate_facts_elemss
   8.333 +      get_local_registration (fn prfx => fn _ => fn ctxt => (ctxt, ctxt)) snd I;
   8.334 +(*
   8.335 +val local_activate_facts_elemss = gen_activate_facts_elemss
   8.336 +      get_local_registration (fn prfx => ProofContext.note_thmss_i) snd I;
   8.337 +*)
   8.338 +
   8.339 +fun gen_prep_registration mk_ctxt read_terms test_reg put_reg activate
   8.340 +    attn expr insts thy_ctxt =
   8.341    let
   8.342 -    val ctxt = ProofContext.init thy;
   8.343 -    val sign = Theory.sign_of thy;
   8.344 -    val tsig = Sign.tsig_of sign;
   8.345 +    val ctxt = mk_ctxt thy_ctxt;
   8.346 +    val sign = ProofContext.sign_of ctxt;
   8.347  
   8.348      val (ids, raw_elemss) =
   8.349            flatten (ctxt, intern_expr sign) ([], Expr expr);
   8.350 @@ -1819,8 +1921,7 @@
   8.351      val tvars = foldr Term.add_typ_tvars [] pvTs;
   8.352      val used = foldr Term.add_typ_varnames [] pvTs;
   8.353      fun sorts (a, i) = assoc (tvars, (a, i));
   8.354 -    val (vs, vinst) = Sign.read_def_terms (sign, K NONE, sorts) used true
   8.355 -         given_insts;
   8.356 +    val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
   8.357      (* replace new types (which are TFrees) by ones with new names *)
   8.358      val new_Tnames = foldr Term.add_term_tfree_names [] vs;
   8.359      val new_Tnames' = Term.invent_names used "'a" (length new_Tnames);
   8.360 @@ -1858,9 +1959,9 @@
   8.361              map (fn Int e => e) elems)) 
   8.362            (ids' ~~ all_elemss);
   8.363  
   8.364 -    (* remove fragments already registered with theory *)
   8.365 +    (* remove fragments already registered with theory or context *)
   8.366      val new_inst_elemss = List.filter (fn (id, _) =>
   8.367 -          is_none (global_get_registration thy id)) inst_elemss;
   8.368 +          not (test_reg thy_ctxt id)) inst_elemss;
   8.369  
   8.370      val propss = extract_asms_elemss new_inst_elemss;
   8.371  
   8.372 @@ -1868,9 +1969,27 @@
   8.373      (** add registrations to theory,
   8.374          without theorems, these are added after the proof **)
   8.375  
   8.376 -    val thy' = Library.foldl (prep_reg_global attn) (thy, new_inst_elemss);
   8.377 +    val thy_ctxt' = Library.foldl (fn (thy_ctxt, (id, _)) =>
   8.378 +          put_reg id attn thy_ctxt) (thy_ctxt, new_inst_elemss);
   8.379 +
   8.380 +  in (thy_ctxt', propss, activate inst_elemss new_inst_elemss) end;
   8.381 +
   8.382 +in
   8.383  
   8.384 -  in (thy', propss, activate_facts_elemss inst_elemss new_inst_elemss) end;
   8.385 +val prep_global_registration = gen_prep_registration
   8.386 +     ProofContext.init
   8.387 +     (fn thy => fn sorts => fn used =>
   8.388 +       Sign.read_def_terms (Theory.sign_of thy, K NONE, sorts) used true)
   8.389 +     test_global_registration
   8.390 +     put_global_registration
   8.391 +     global_activate_facts_elemss;
   8.392 +
   8.393 +val prep_local_registration = gen_prep_registration
   8.394 +     I
   8.395 +     (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE))
   8.396 +     smart_test_registration
   8.397 +     put_local_registration
   8.398 +     local_activate_facts_elemss;
   8.399  
   8.400  end;  (* local *)
   8.401  
   8.402 @@ -1879,7 +1998,7 @@
   8.403  (** locale theory setup **)
   8.404  
   8.405  val setup =
   8.406 - [LocalesData.init,
   8.407 + [GlobalLocalesData.init, LocalLocalesData.init,
   8.408    add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, SOME Syntax.NoSyn)]],
   8.409    add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]];
   8.410  
     9.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 24 16:36:40 2005 +0100
     9.2 +++ b/src/Pure/Isar/proof.ML	Thu Mar 24 17:03:37 2005 +0100
     9.3 @@ -115,6 +115,12 @@
     9.4    val have_i: (state -> state Seq.seq) -> bool
     9.5      -> ((string * context attribute list) * (term * (term list * term list)) list) list
     9.6      -> state -> state
     9.7 +  val interpret: (context -> context) -> (state -> state Seq.seq) -> bool
     9.8 +    -> ((string * context attribute list) * (string * (string list * string list)) list) list
     9.9 +    -> state -> state
    9.10 +  val interpret_i: (context -> context) -> (state -> state Seq.seq) -> bool
    9.11 +    -> ((string * context attribute list) * (term * (term list * term list)) list) list
    9.12 +    -> state -> state
    9.13    val at_bottom: state -> bool
    9.14    val local_qed: (state -> state Seq.seq)
    9.15      -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit)
    9.16 @@ -143,11 +149,12 @@
    9.17  
    9.18  (* type goal *)
    9.19  
    9.20 -(* CB: three kinds of Isar goals are distinguished:
    9.21 +(* CB: four kinds of Isar goals are distinguished:
    9.22     - Theorem: global goal in a theory, corresponds to Isar commands theorem,
    9.23       lemma and corollary,
    9.24     - Have: local goal in a proof, Isar command have
    9.25     - Show: local goal in a proof, Isar command show
    9.26 +   - Interpret: local goal in a proof, Isar command interpret
    9.27  *)
    9.28  
    9.29  datatype kind =
    9.30 @@ -156,10 +163,14 @@
    9.31      locale_spec: (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option,
    9.32      view: cterm list * cterm list, (* target view and includes view *)
    9.33      thy_mod: theory -> theory} |   (* used in finish_global to modify final
    9.34 -      theory, normally set to I;
    9.35 -      used by registration command to activate registrations *)
    9.36 +                                      theory, normally set to I; used by
    9.37 +                                      registration command to activate
    9.38 +                                      registrations *)
    9.39    Show of context attribute list list |
    9.40 -  Have of context attribute list list;
    9.41 +  Have of context attribute list list |
    9.42 +  Interpret of {attss: context attribute list list,
    9.43 +    ctxt_mod: context -> context}; (* used in finish_local to modify final
    9.44 +                                      context *)
    9.45  
    9.46  (* CB: this function prints the goal kind (Isar command), name and target in
    9.47     the proof state *)
    9.48 @@ -170,7 +181,8 @@
    9.49          locale_spec = SOME (name, _), ...}) =
    9.50        s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
    9.51    | kind_name _ (Show _) = "show"
    9.52 -  | kind_name _ (Have _) = "have";
    9.53 +  | kind_name _ (Have _) = "have"
    9.54 +  | kind_name _ (Interpret _) = "interpret";
    9.55  
    9.56  type goal =
    9.57   (kind *             (*result kind*)
    9.58 @@ -824,7 +836,10 @@
    9.59  val show_i = local_goal' ProofContext.bind_propp_i Show;
    9.60  val have = local_goal ProofContext.bind_propp Have;
    9.61  val have_i = local_goal ProofContext.bind_propp_i Have;
    9.62 -
    9.63 +fun interpret ctxt_mod = local_goal ProofContext.bind_propp
    9.64 +  (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod});
    9.65 +fun interpret_i ctxt_mod = local_goal ProofContext.bind_propp_i
    9.66 +  (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod});
    9.67  
    9.68  
    9.69  (** conclusions **)
    9.70 @@ -872,19 +887,28 @@
    9.71        results |> map (ProofContext.export false goal_ctxt outer_ctxt)
    9.72        |> Seq.commute |> Seq.map (Library.unflat tss);
    9.73  
    9.74 -    val (attss, opt_solve) =
    9.75 +    val (attss, opt_solve, ctxt_mod) =
    9.76        (case kind of
    9.77          Show attss => (attss,
    9.78 -          export_goals goal_ctxt (if pr then print_rule else (K (K ()))) results)
    9.79 -      | Have attss => (attss, Seq.single)
    9.80 +          export_goals goal_ctxt (if pr then print_rule else (K (K ())))
    9.81 +            results, I)
    9.82 +      | Have attss => (attss, Seq.single, I)
    9.83 +      | Interpret {attss, ctxt_mod} => (attss, Seq.single, ctxt_mod)
    9.84        | _ => err_malformed "finish_local" state);
    9.85    in
    9.86      conditional pr (fn () => print_result goal_ctxt
    9.87        (kind_name (sign_of state) kind, names ~~ Library.unflat tss results));
    9.88      outer_state
    9.89      |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts)
    9.90 +(* original version
    9.91      |> (fn st => Seq.map (fn res =>
    9.92 -      note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
    9.93 +      note_thmss_i ((names ~~ attss) ~~
    9.94 +          map (single o Thm.no_attributes) res) st) resultq)
    9.95 +*)
    9.96 +    |> (fn st => Seq.map (fn res =>
    9.97 +      st |> note_thmss_i ((names ~~ attss) ~~
    9.98 +              map (single o Thm.no_attributes) res)
    9.99 +         |> map_context ctxt_mod) resultq)
   9.100      |> (Seq.flat o Seq.map opt_solve)
   9.101      |> (Seq.flat o Seq.map after_qed)
   9.102    end;
    10.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 24 16:36:40 2005 +0100
    10.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 24 17:03:37 2005 +0100
    10.3 @@ -199,8 +199,8 @@
    10.4        sort Vartab.table *                                     (*default sorts*)
    10.5        string list *                                           (*used type variables*)
    10.6        term list Symtab.table,
    10.7 -      delta: Object.T Symtab.table (* difference between local and global claset and simpset*),
    10.8 -      delta_count: int ref (* number of local anonymous thms *)
    10.9 +    delta: Object.T Symtab.table (* difference between local and global claset and simpset*),
   10.10 +    delta_count: int ref (* number of local anonymous thms *)
   10.11  };                                (*type variable occurrences*)
   10.12  
   10.13  exception CONTEXT of string * context;
    11.1 --- a/src/Pure/pure_thy.ML	Thu Mar 24 16:36:40 2005 +0100
    11.2 +++ b/src/Pure/pure_thy.ML	Thu Mar 24 17:03:37 2005 +0100
    11.3 @@ -45,10 +45,24 @@
    11.4    val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
    11.5    val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
    11.6      -> theory * thm list list
    11.7 -  val note_thmss: theory attribute -> ((bstring * theory attribute list) *
    11.8 -    (thmref * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
    11.9 -  val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
   11.10 -    (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
   11.11 +  val note_thmss:
   11.12 +    theory attribute -> ((bstring * theory attribute list) *
   11.13 +    (thmref * theory attribute list) list) list -> theory ->
   11.14 +    theory * (bstring * thm list) list
   11.15 +  val note_thmss_i:
   11.16 +    theory attribute -> ((bstring * theory attribute list) *
   11.17 +    (thm list * theory attribute list) list) list -> theory ->
   11.18 +    theory * (bstring * thm list) list
   11.19 +  val note_thmss_qualified:
   11.20 +    (string -> string list) ->
   11.21 +    theory attribute -> ((bstring * theory attribute list) *
   11.22 +    (thmref * theory attribute list) list) list -> theory ->
   11.23 +    theory * (bstring * thm list) list
   11.24 +  val note_thmss_qualified_i:
   11.25 +    (string -> string list) ->
   11.26 +    theory attribute -> ((bstring * theory attribute list) *
   11.27 +    (thm list * theory attribute list) list) list -> theory ->
   11.28 +    theory * (bstring * thm list) list
   11.29    val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
   11.30    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
   11.31    val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory
   11.32 @@ -309,15 +323,15 @@
   11.33  fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
   11.34  fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
   11.35  
   11.36 -fun enter_thms _ _ _ app_att thy ("", thms) = app_att (thy, thms)
   11.37 -  | enter_thms sg pre_name post_name app_att thy (bname, thms) =
   11.38 +fun gen_enter_thms _ _ _ _ _ app_att thy ("", thms) = app_att (thy, thms)
   11.39 +  | gen_enter_thms full acc sg pre_name post_name app_att thy (bname, thms) =
   11.40        let
   11.41 -        val name = Sign.full_name sg bname;
   11.42 +        val name = full sg bname;
   11.43          val (thy', thms') = app_att (thy, pre_name name thms);
   11.44          val named_thms = post_name name thms';
   11.45  
   11.46          val r as ref {space, thms_tab, index} = get_theorems_sg sg;
   11.47 -        val space' = NameSpace.extend (space, [name]);
   11.48 +        val space' = NameSpace.extend' acc (space, [name]);
   11.49          val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
   11.50          val index' = FactIndex.add (K false) (index, (name, named_thms));
   11.51        in
   11.52 @@ -330,6 +344,7 @@
   11.53          (thy', named_thms)
   11.54        end;
   11.55  
   11.56 +fun enter_thms sg = gen_enter_thms Sign.full_name NameSpace.accesses sg;
   11.57  
   11.58  (* add_thms(s) *)
   11.59  
   11.60 @@ -351,21 +366,31 @@
   11.61  
   11.62  local
   11.63  
   11.64 -fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
   11.65 +fun gen_note_thss enter get kind_att (thy, ((bname, more_atts), ths_atts)) =
   11.66    let
   11.67      fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
   11.68 -    val (thy', thms) = enter_thms (Theory.sign_of thy)
   11.69 +    val (thy', thms) = enter (Theory.sign_of thy)
   11.70        name_thmss (name_thms false) (apsnd List.concat o foldl_map app) thy
   11.71        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
   11.72    in (thy', (bname, thms)) end;
   11.73  
   11.74 -fun gen_note_thmss get kind_att args thy =
   11.75 -  foldl_map (gen_note_thss get kind_att) (thy, args);
   11.76 +fun gen_note_thmss enter get kind_att args thy =
   11.77 +  foldl_map (gen_note_thss enter get kind_att) (thy, args);
   11.78  
   11.79  in
   11.80  
   11.81 -val note_thmss = gen_note_thmss get_thms;
   11.82 -val note_thmss_i = gen_note_thmss (K I);
   11.83 +(* if path is set, only permit unqualified names *)
   11.84 +
   11.85 +val note_thmss = gen_note_thmss enter_thms get_thms;
   11.86 +val note_thmss_i = gen_note_thmss enter_thms (K I);
   11.87 +
   11.88 +(* always permit qualified names,
   11.89 +   clients may specify non-standard access policy *)
   11.90 +
   11.91 +fun note_thmss_qualified acc =
   11.92 +  gen_note_thmss (gen_enter_thms Sign.full_name' acc) get_thms;
   11.93 +fun note_thmss_qualified_i acc =
   11.94 +  gen_note_thmss (gen_enter_thms Sign.full_name' acc) (K I);
   11.95  
   11.96  end;
   11.97  
    12.1 --- a/src/Pure/sign.ML	Thu Mar 24 16:36:40 2005 +0100
    12.2 +++ b/src/Pure/sign.ML	Thu Mar 24 17:03:37 2005 +0100
    12.3 @@ -54,6 +54,7 @@
    12.4    val typeK: string
    12.5    val constK: string
    12.6    val full_name: sg -> bstring -> string
    12.7 +  val full_name': sg -> bstring -> string
    12.8    val full_name_path: sg -> string -> bstring -> string
    12.9    val base_name: string -> bstring
   12.10    val intern: sg -> string -> xstring -> string
   12.11 @@ -491,7 +492,7 @@
   12.12  fun add_names x = change_space NameSpace.extend x;
   12.13  fun hide_names b x = change_space (NameSpace.hide b) x;
   12.14  
   12.15 -(*make full names*)
   12.16 +(*make full names, standard version*)
   12.17  fun full _ "" = error "Attempt to declare empty name \"\""
   12.18    | full NONE bname = bname
   12.19    | full (SOME path) bname =
   12.20 @@ -503,6 +504,18 @@
   12.21            else warning ("Declared non-identifier " ^ quote name); name
   12.22          end;
   12.23  
   12.24 +(*make full names, variant permitting qualified names*)
   12.25 +fun full' _ "" = error "Attempt to declare empty name \"\""
   12.26 +  | full' NONE bname = bname
   12.27 +  | full' (SOME path) bname =
   12.28 +      let
   12.29 +        val bnames = NameSpace.unpack bname;
   12.30 +        val name = NameSpace.pack (path @ bnames)
   12.31 +      in
   12.32 +        if forall Syntax.is_identifier bnames then ()
   12.33 +        else warning ("Declared non-identifier " ^ quote name); name
   12.34 +      end;
   12.35 +
   12.36  (*base name*)
   12.37  val base_name = NameSpace.base;
   12.38  
   12.39 @@ -566,6 +579,7 @@
   12.40    val intern_tycons = intrn_tycons o spaces_of;
   12.41  
   12.42    val full_name = full o #path o rep_sg;
   12.43 +  val full_name' = full' o #path o rep_sg;
   12.44  
   12.45    fun full_name_path sg elems =
   12.46      full (SOME (getOpt (#path (rep_sg sg), []) @ NameSpace.unpack elems));