# HG changeset patch
# User berghofe
# Date 1106585778 -3600
# Node ID 956d6acacf8937f83aed14cfad6224e5d837130a
# Parent  735dd4260500c8afcc81ed0f8b759fca9cb38d0c
Specific theorems in a named list of theorems can now be referred to
via indices (type thmref).

diff -r 735dd4260500 -r 956d6acacf89 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -133,8 +133,12 @@
 
 (* theorems *)
 
+val thm_sel = Args.parens (Scan.pass () (Args.enum1 "," (Scan.lift
+  (   Args.nat --| Args.$$$ "-" -- Args.nat >> op upto
+   || Args.nat >> single)) >> flat));
+
 fun gen_thm get attrib app =
-  Scan.depend (fn st => Args.name -- Args.opt_attribs >>
+  Scan.depend (fn st => Args.name -- Scan.option thm_sel -- Args.opt_attribs >>
     (fn (name, srcs) => app ((st, get st name), map (attrib st) srcs)));
 
 val global_thm = gen_thm PureThy.get_thm global_attribute Thm.apply_attributes;
diff -r 735dd4260500 -r 956d6acacf89 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -57,14 +57,14 @@
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
   val print_thms_containing: int option * string list
     -> Toplevel.transition -> Toplevel.transition
-  val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
+  val thm_deps: (thmref * Args.src list) list -> Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_lthms: Toplevel.transition -> Toplevel.transition
   val print_cases: Toplevel.transition -> Toplevel.transition
   val print_intros: Toplevel.transition -> Toplevel.transition
-  val print_thms: string list * (string * Args.src list) list
+  val print_thms: string list * (thmref * Args.src list) list
     -> Toplevel.transition -> Toplevel.transition
-  val print_prfs: bool -> string list * (string * Args.src list) list option
+  val print_prfs: bool -> string list * (thmref * Args.src list) list option
     -> Toplevel.transition -> Toplevel.transition
   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
diff -r 735dd4260500 -r 956d6acacf89 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -13,35 +13,35 @@
   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
   val add_defs: bool * ((bstring * string) * Args.src list) list -> theory -> theory
   val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
-  val theorems: string -> ((bstring * Args.src list) * (xstring * Args.src list) list) list
+  val theorems: string -> ((bstring * Args.src list) * (thmref * Args.src list) list) list
     -> theory -> theory * (string * thm list) list
   val theorems_i: string ->
     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
     -> theory -> theory * (string * thm list) list
   val locale_theorems: string -> xstring ->
-    ((bstring * Args.src list) * (xstring * Args.src list) list) list
+    ((bstring * Args.src list) * (thmref * Args.src list) list) list
     -> theory -> theory * (bstring * thm list) list
   val locale_theorems_i: string -> string ->
     ((bstring * Proof.context attribute list)
       * (thm list * Proof.context attribute list) list) list
     -> theory -> theory * (string * thm list) list
   val smart_theorems: string -> xstring option ->
-    ((bstring * Args.src list) * (xstring * Args.src list) list) list
+    ((bstring * Args.src list) * (thmref * Args.src list) list) list
     -> theory -> theory * (string * thm list) list
-  val declare_theorems: xstring option -> (xstring * Args.src list) list -> theory -> theory
-  val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list
+  val declare_theorems: xstring option -> (thmref * Args.src list) list -> theory -> theory
+  val apply_theorems: (thmref * Args.src list) list -> theory -> theory * thm list
   val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
-  val have_facts: ((string * Args.src list) * (string * Args.src list) list) list
+  val have_facts: ((string * Args.src list) * (thmref * Args.src list) list) list
     -> ProofHistory.T -> ProofHistory.T
   val have_facts_i: ((string * Proof.context attribute list) *
     (thm * Proof.context attribute list) list) list -> ProofHistory.T -> ProofHistory.T
-  val from_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+  val from_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
   val from_facts_i: (thm * Proof.context attribute list) list list
     -> ProofHistory.T -> ProofHistory.T
-  val with_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+  val with_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
   val with_facts_i: (thm * Proof.context attribute list) list list
     -> ProofHistory.T -> ProofHistory.T
-  val using_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+  val using_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
   val using_facts_i: (thm * Proof.context attribute list) list list
     -> ProofHistory.T -> ProofHistory.T
   val chain: ProofHistory.T -> ProofHistory.T
@@ -130,10 +130,10 @@
   val done_proof: Toplevel.transition -> Toplevel.transition
   val skip_proof: Toplevel.transition -> Toplevel.transition
   val forget_proof: Toplevel.transition -> Toplevel.transition
-  val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
-  val also: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
+  val get_thmss: (thmref * Args.src list) list -> Proof.state -> thm list
+  val also: (thmref * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
   val also_i: thm list option -> Toplevel.transition -> Toplevel.transition
-  val finally: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
+  val finally: (thmref * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
   val finally_i: thm list option -> Toplevel.transition -> Toplevel.transition
   val moreover: Toplevel.transition -> Toplevel.transition
   val ultimately: Toplevel.transition -> Toplevel.transition
diff -r 735dd4260500 -r 956d6acacf89 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -71,7 +71,7 @@
     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
   val note_thmss: string -> xstring ->
-    ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
+    ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
     theory -> theory * (bstring * thm list) list
   val note_thmss_i: string -> string ->
     ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
@@ -106,7 +106,7 @@
 datatype 'a elem_expr =
   Elem of 'a | Expr of expr;
 
-type 'att element = (string, string, string, 'att) elem;
+type 'att element = (string, string, thmref, 'att) elem;
 type 'att element_i = (typ, term, thm list, 'att) elem;
 
 type locale =
diff -r 735dd4260500 -r 956d6acacf89 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/method.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -487,8 +487,8 @@
 fun tactic txt ctxt = METHOD (fn facts =>
   (Context.use_mltext
     ("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \
-     \let val thm = PureIsar.ProofContext.get_thm_closure ctxt\n\
-     \  and thms = PureIsar.ProofContext.get_thms_closure ctxt in\n"
+     \let val thm = PureIsar.ProofContext.get_thm_closure ctxt o rpair None\n\
+     \  and thms = PureIsar.ProofContext.get_thms_closure ctxt o rpair None in\n"
      ^ txt ^
      "\nend in PureIsar.Method.set_tactic tactic end")
     false None;
diff -r 735dd4260500 -r 956d6acacf89 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -67,8 +67,8 @@
   val opt_thm_name: string -> token list -> (bstring * Args.src list) * token list
   val spec_name: token list -> ((bstring * string) * Args.src list) * token list
   val spec_opt_name: token list -> ((bstring * string) * Args.src list) * token list
-  val xthm: token list -> (xstring * Args.src list) * token list
-  val xthms1: token list -> (xstring * Args.src list) list * token list
+  val xthm: token list -> (thmref * Args.src list) * token list
+  val xthms1: token list -> (thmref * Args.src list) list * token list
   val locale_target: token list -> xstring option * token list
   val locale_expr: token list -> Locale.expr * token list
   val locale_keyword: token list -> string * token list
@@ -149,6 +149,7 @@
 val semicolon = $$$ ";";
 
 val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
+val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
 
 val nat = number >> (#1 o Library.read_int o Symbol.explode);
 
@@ -295,7 +296,11 @@
 val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
 val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
 
-val xthm = xname -- opt_attribs;
+val thm_sel = $$$ "(" |-- list1
+  (   nat --| minus -- nat >> op upto
+   || nat >> single) --| $$$ ")" >> flat;
+
+val xthm = xname -- Scan.option thm_sel -- opt_attribs;
 val xthms1 = Scan.repeat1 xthm;
 
 
diff -r 735dd4260500 -r 956d6acacf89 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -58,14 +58,14 @@
   val let_bind_i: (term list * term) list -> state -> state
   val simple_note_thms: string -> thm list -> state -> state
   val note_thmss: ((bstring * context attribute list) *
-    (xstring * context attribute list) list) list -> state -> state
+    (thmref * context attribute list) list) list -> state -> state
   val note_thmss_i: ((bstring * context attribute list) *
     (thm list * context attribute list) list) list -> state -> state
   val with_thmss: ((bstring * context attribute list) *
-    (xstring * context attribute list) list) list -> state -> state
+    (thmref * context attribute list) list) list -> state -> state
   val with_thmss_i: ((bstring * context attribute list) *
     (thm list * context attribute list) list) list -> state -> state
-  val using_thmss: ((xstring * context attribute list) list) list -> state -> state
+  val using_thmss: ((thmref * context attribute list) list) list -> state -> state
   val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
   val instantiate_locale: string * (string * context attribute list) -> state
     -> state
diff -r 735dd4260500 -r 956d6acacf89 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -90,10 +90,10 @@
     -> context * (term list list * (context -> context))
   val bind_propp_schematic_i: context * (term * (term list * term list)) list list
     -> context * (term list list * (context -> context))
-  val get_thm: context -> string -> thm
-  val get_thm_closure: context -> string -> thm
-  val get_thms: context -> string -> thm list
-  val get_thms_closure: context -> string -> thm list
+  val get_thm: context -> thmref -> thm
+  val get_thm_closure: context -> thmref -> thm
+  val get_thms: context -> thmref -> thm list
+  val get_thms_closure: context -> thmref -> thm list
   val cond_extern: context -> string -> xstring
   val qualified: bool -> context -> context
   val restore_qualified: context -> context -> context
@@ -103,7 +103,7 @@
   val put_thmss: (string * thm list) list -> context -> context
   val reset_thms: string -> context -> context
   val note_thmss:
-    ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
+    ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
       context -> context * (bstring * thm list) list
   val note_thmss_i:
     ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
@@ -988,10 +988,11 @@
     val sg_ref = Sign.self_ref (Theory.sign_of thy);
     val get_from_thy = f thy;
   in
-    fn xname =>
+    fn xnamei as (xname, _) =>
       (case Symtab.lookup (tab, NameSpace.intern space xname) of
-        Some (Some ths) => map (Thm.transfer_sg (Sign.deref sg_ref)) ths
-      | _ => get_from_thy xname) |> g xname
+        Some (Some ths) => map (Thm.transfer_sg (Sign.deref sg_ref))
+          (PureThy.select_thm xnamei ths)
+      | _ => get_from_thy xnamei) |> g xname
   end;
 
 val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm;
@@ -1449,7 +1450,7 @@
 fun lthms_containing (ctxt as Context {thms = (_, _, _, index), ...}) idx =
   let
     fun valid (name, ths) =
-      (case try (transform_error (fn () => get_thms ctxt name)) () of
+      (case try (transform_error (fn () => get_thms ctxt (name, None))) () of
         None => false
       | Some ths' => Library.equal_lists Thm.eq_thm (ths, ths'));
   in gen_distinct eq_fst (filter valid (FactIndex.find idx index)) end;
diff -r 735dd4260500 -r 956d6acacf89 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Jan 24 16:25:36 2005 +0100
+++ b/src/Pure/pure_thy.ML	Mon Jan 24 17:56:18 2005 +0100
@@ -7,11 +7,12 @@
 
 signature BASIC_PURE_THY =
 sig
+  type thmref
   val print_theorems: theory -> unit
   val print_theory: theory -> unit
-  val get_thm: theory -> xstring -> thm
-  val get_thms: theory -> xstring -> thm list
-  val get_thmss: theory -> xstring list -> thm list
+  val get_thm: theory -> thmref -> thm
+  val get_thms: theory -> thmref -> thm list
+  val get_thmss: theory -> thmref list -> thm list
   val thms_of: theory -> (string * thm) list
   structure ProtoPure:
     sig
@@ -23,9 +24,10 @@
 signature PURE_THY =
 sig
   include BASIC_PURE_THY
-  val get_thm_closure: theory -> xstring -> thm
-  val get_thms_closure: theory -> xstring -> thm list
+  val get_thm_closure: theory -> thmref -> thm
+  val get_thms_closure: theory -> thmref -> thm list
   val single_thm: string -> thm list -> thm
+  val select_thm: thmref -> thm list -> thm list
   val cond_extern_thm_sg: Sign.sg -> string -> xstring
   val thms_containing: theory -> string list * string list -> (string * thm list) list
   val thms_containing_consts: theory -> string list -> (string * thm) list
@@ -44,7 +46,7 @@
   val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
     -> theory * thm list list
   val note_thmss: theory attribute -> ((bstring * theory attribute list) *
-    (xstring * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
+    (thmref * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
   val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
     (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
   val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
@@ -129,6 +131,8 @@
 
 (** retrieve theorems **)
 
+type thmref = xstring * int list option;
+
 (* selections *)
 
 fun the_thms _ (Some thms) = thms
@@ -137,6 +141,11 @@
 fun single_thm _ [thm] = thm
   | single_thm name _ = error ("Single theorem expected " ^ quote name);
 
+fun select_thm (s, None) xs = xs
+  | select_thm (s, Some is) xs = map
+      (fn i => nth_elem (i, xs) handle LIST _ =>
+         error ("Bad subscript " ^ string_of_int i ^ " for " ^ quote s)) is;
+
 
 (* get_thm(s)_closure -- statically scoped versions *)
 
@@ -154,21 +163,23 @@
 
 fun get_thms_closure thy =
   let val closures = map lookup_thms (thy :: Theory.ancestors_of thy)
-  in fn name => the_thms name (get_first (fn f => f name) closures) end;
+  in fn namei as (name, _) => select_thm namei
+    (the_thms name (get_first (fn f => f name) closures))
+  end;
 
 fun get_thm_closure thy =
   let val get = get_thms_closure thy
-  in fn name => single_thm name (get name) end;
+  in fn namei as (name, _) => single_thm name (get namei) end;
 
 
 (* get_thm etc. *)
 
-fun get_thms theory name =
+fun get_thms theory (namei as (name, _)) =
   get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
-  |> the_thms name |> map (Thm.transfer theory);
+  |> the_thms name |> select_thm namei |> map (Thm.transfer theory);
 
 fun get_thmss thy names = flat (map (get_thms thy) names);
-fun get_thm thy name = single_thm name (get_thms thy name);
+fun get_thm thy (namei as (name, _)) = single_thm name (get_thms thy namei);
 
 
 (* thms_of *)
@@ -184,7 +195,7 @@
 fun thms_containing thy idx =
   let
     fun valid (name, ths) =
-      (case try (transform_error (get_thms thy)) name of
+      (case try (transform_error (get_thms thy)) (name, None) of
         None => false
       | Some ths' => Library.equal_lists Thm.eq_thm (ths, ths'));
   in