src/Pure/Isar/rule_cases.ML
author wenzelm
Wed Mar 08 17:48:31 2000 +0100 (2000-03-08)
changeset 8364 0eb9ee70c8f8
child 8400 64921d1fef15
permissions -rw-r--r--
added Isar/rule_cases.ML;
wenzelm@8364
     1
(*  Title:      Pure/Isar/rule_cases.ML
wenzelm@8364
     2
    ID:         $Id$
wenzelm@8364
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8364
     4
wenzelm@8364
     5
Manage local contexts of rules.
wenzelm@8364
     6
wenzelm@8364
     7
TODO:
wenzelm@8364
     8
  - instantiation of cases (including type vars!);
wenzelm@8364
     9
*)
wenzelm@8364
    10
wenzelm@8364
    11
signature RULE_CASES =
wenzelm@8364
    12
sig
wenzelm@8364
    13
  type T (* = (string * typ) list * term list *)
wenzelm@8364
    14
  val name: string list -> thm -> thm
wenzelm@8364
    15
  val get: thm -> string list
wenzelm@8364
    16
  val add: thm -> thm * string list
wenzelm@8364
    17
  val none: thm -> thm * string list
wenzelm@8364
    18
  val make: thm -> string list -> (string * T) list
wenzelm@8364
    19
  val case_names: string list -> 'a attribute
wenzelm@8364
    20
  val params: string list list -> 'a attribute
wenzelm@8364
    21
end;
wenzelm@8364
    22
wenzelm@8364
    23
structure RuleCases: RULE_CASES =
wenzelm@8364
    24
struct
wenzelm@8364
    25
wenzelm@8364
    26
wenzelm@8364
    27
(* local contexts *)
wenzelm@8364
    28
wenzelm@8364
    29
type T = (string * typ) list * term list;
wenzelm@8364
    30
val casesN = "cases";
wenzelm@8364
    31
wenzelm@8364
    32
wenzelm@8364
    33
(* case names *)
wenzelm@8364
    34
wenzelm@8364
    35
fun name names thm =
wenzelm@8364
    36
  thm
wenzelm@8364
    37
  |> Drule.untag_rule (casesN, [])
wenzelm@8364
    38
  |> Drule.tag_rule (casesN, names);
wenzelm@8364
    39
wenzelm@8364
    40
fun get thm =
wenzelm@8364
    41
  (case assoc (Thm.tags_of_thm thm, casesN) of
wenzelm@8364
    42
    None => map Library.string_of_int (1 upto Thm.nprems_of thm)
wenzelm@8364
    43
  | Some names => names);
wenzelm@8364
    44
wenzelm@8364
    45
fun add thm = (thm, get thm);
wenzelm@8364
    46
fun none thm = (thm, []);
wenzelm@8364
    47
wenzelm@8364
    48
wenzelm@8364
    49
(* prepare cases *)
wenzelm@8364
    50
wenzelm@8364
    51
fun prep_case thm name i =
wenzelm@8364
    52
  let
wenzelm@8364
    53
    val (_, _, Bi, _) = Thm.dest_state (thm, i)
wenzelm@8364
    54
      handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
wenzelm@8364
    55
    val rev_params = rename_wrt_term Bi (Logic.strip_params Bi);
wenzelm@8364
    56
    val rev_frees = map Free rev_params;
wenzelm@8364
    57
    val props = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp Bi);
wenzelm@8364
    58
  in (name, (rev rev_params, props)) end;
wenzelm@8364
    59
wenzelm@8364
    60
fun make thm names =
wenzelm@8364
    61
  #1 (foldr (fn (name, (cases, i)) => (prep_case thm name i :: cases, i - 1))
wenzelm@8364
    62
    (Library.drop (length names - Thm.nprems_of thm, names), ([], Thm.nprems_of thm)));
wenzelm@8364
    63
wenzelm@8364
    64
wenzelm@8364
    65
(* attributes *)
wenzelm@8364
    66
wenzelm@8364
    67
fun case_names ss = Drule.rule_attribute (K (name ss));
wenzelm@8364
    68
wenzelm@8364
    69
fun rename_params xss thm =
wenzelm@8364
    70
  #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss));
wenzelm@8364
    71
wenzelm@8364
    72
fun params xss = Drule.rule_attribute (K (rename_params xss));
wenzelm@8364
    73
wenzelm@8364
    74
wenzelm@8364
    75
end;