src/Pure/pure_thy.ML
changeset 15703 727ef1b8b3ee
parent 15696 1da4ce092c0b
child 15715 dfa913c68f9d
     1.1 --- a/src/Pure/pure_thy.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4  signature PURE_THY =
     1.5  sig
     1.6    include BASIC_PURE_THY
     1.7 +  datatype interval = FromTo of int * int | From of int | Single of int
     1.8    val get_thm_closure: theory -> thmref -> thm
     1.9    val get_thms_closure: theory -> thmref -> thm list
    1.10    val single_thm: string -> thm list -> thm
    1.11 @@ -145,20 +146,42 @@
    1.12  
    1.13  (** retrieve theorems **)
    1.14  
    1.15 -type thmref = xstring * int list option;
    1.16 -
    1.17 -(* selections *)
    1.18 -
    1.19  fun the_thms _ (SOME thms) = thms
    1.20    | the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
    1.21  
    1.22  fun single_thm _ [thm] = thm
    1.23    | single_thm name _ = error ("Single theorem expected " ^ quote name);
    1.24  
    1.25 -fun select_thm (s, NONE) xs = xs
    1.26 -  | select_thm (s, SOME is) xs = map
    1.27 -      (fn i => (if i < 1 then raise Subscript else List.nth (xs, i-1)) handle Subscript =>
    1.28 -         error ("Bad subscript " ^ string_of_int i ^ " for " ^ quote s)) is;
    1.29 +
    1.30 +(* selections *)
    1.31 +
    1.32 +datatype interval =
    1.33 +  FromTo of int * int |
    1.34 +  From of int |
    1.35 +  Single of int;
    1.36 +
    1.37 +type thmref = xstring * interval list option;
    1.38 +
    1.39 +local
    1.40 +
    1.41 +fun interval _ (FromTo (i, j)) = i upto j
    1.42 +  | interval n (From i) = i upto n
    1.43 +  | interval _ (Single i) = [i];
    1.44 +
    1.45 +fun select name thms n i =
    1.46 +  if i < 1 orelse i > n then
    1.47 +    error ("Bad subscript " ^ string_of_int i ^ " for " ^
    1.48 +      quote name ^ " (length " ^ string_of_int n ^ ")")
    1.49 +  else List.nth (thms, i - 1);
    1.50 +
    1.51 +in
    1.52 +
    1.53 +fun select_thm (_, NONE) thms = thms
    1.54 +  | select_thm (name, SOME is) thms =
    1.55 +      let val n = length thms
    1.56 +      in map (select name thms n) (List.concat (map (interval n) is)) end;
    1.57 +
    1.58 +end;
    1.59  
    1.60  
    1.61  (* get_thm(s)_closure -- statically scoped versions *)
    1.62 @@ -222,6 +245,7 @@
    1.63    thms_containing thy (consts, []) |> map #2 |> List.concat
    1.64    |> map (fn th => (Thm.name_of_thm th, th))
    1.65  
    1.66 +
    1.67  (* intro/elim theorems *)
    1.68  
    1.69  (* intro: given a goal state, find a suitable intro rule for some subgoal *)