src/Pure/Isar/rule_cases.ML
author wenzelm
Mon Mar 13 13:16:43 2000 +0100 (2000-03-13)
changeset 8427 b19b817522a5
parent 8400 64921d1fef15
child 8497 88d7a4f834ff
permissions -rw-r--r--
tuned;
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
wenzelm@8364
     8
signature RULE_CASES =
wenzelm@8364
     9
sig
wenzelm@8364
    10
  type T (* = (string * typ) list * term list *)
wenzelm@8364
    11
  val name: string list -> thm -> thm
wenzelm@8427
    12
  val case_names: string list -> 'a attribute
wenzelm@8364
    13
  val get: thm -> string list
wenzelm@8364
    14
  val add: thm -> thm * string list
wenzelm@8364
    15
  val none: thm -> thm * string list
wenzelm@8364
    16
  val make: thm -> string list -> (string * T) list
wenzelm@8427
    17
  val rename_params: string list list -> thm -> thm
wenzelm@8364
    18
  val params: string list list -> 'a attribute
wenzelm@8364
    19
end;
wenzelm@8364
    20
wenzelm@8364
    21
structure RuleCases: RULE_CASES =
wenzelm@8364
    22
struct
wenzelm@8364
    23
wenzelm@8364
    24
wenzelm@8364
    25
(* local contexts *)
wenzelm@8364
    26
wenzelm@8364
    27
type T = (string * typ) list * term list;
wenzelm@8364
    28
val casesN = "cases";
wenzelm@8364
    29
wenzelm@8364
    30
wenzelm@8364
    31
(* case names *)
wenzelm@8364
    32
wenzelm@8364
    33
fun name names thm =
wenzelm@8364
    34
  thm
wenzelm@8364
    35
  |> Drule.untag_rule (casesN, [])
wenzelm@8364
    36
  |> Drule.tag_rule (casesN, names);
wenzelm@8364
    37
wenzelm@8427
    38
fun case_names ss = Drule.rule_attribute (K (name ss));
wenzelm@8364
    39
wenzelm@8427
    40
fun get thm = Library.assocs (Thm.tags_of_thm thm) casesN;
wenzelm@8364
    41
fun add thm = (thm, get thm);
wenzelm@8364
    42
fun none thm = (thm, []);
wenzelm@8364
    43
wenzelm@8364
    44
wenzelm@8364
    45
(* prepare cases *)
wenzelm@8364
    46
wenzelm@8364
    47
fun prep_case thm name i =
wenzelm@8364
    48
  let
wenzelm@8364
    49
    val (_, _, Bi, _) = Thm.dest_state (thm, i)
wenzelm@8364
    50
      handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
wenzelm@8364
    51
    val rev_params = rename_wrt_term Bi (Logic.strip_params Bi);
wenzelm@8364
    52
    val rev_frees = map Free rev_params;
wenzelm@8364
    53
    val props = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp Bi);
wenzelm@8364
    54
  in (name, (rev rev_params, props)) end;
wenzelm@8364
    55
wenzelm@8364
    56
fun make thm names =
wenzelm@8364
    57
  #1 (foldr (fn (name, (cases, i)) => (prep_case thm name i :: cases, i - 1))
wenzelm@8364
    58
    (Library.drop (length names - Thm.nprems_of thm, names), ([], Thm.nprems_of thm)));
wenzelm@8364
    59
wenzelm@8364
    60
wenzelm@8427
    61
(* params *)
wenzelm@8364
    62
wenzelm@8364
    63
fun rename_params xss thm =
wenzelm@8364
    64
  #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss));
wenzelm@8364
    65
wenzelm@8364
    66
fun params xss = Drule.rule_attribute (K (rename_params xss));
wenzelm@8364
    67
wenzelm@8364
    68
wenzelm@8364
    69
end;