src/Pure/Isar/rule_cases.ML
author wenzelm
Tue Nov 28 01:11:12 2000 +0100 (2000-11-28 ago)
changeset 10530 df079a585e6d
parent 10407 998778f8d63b
child 10811 98f52cb93d93
permissions -rw-r--r--
added consumes, consumes_default;
added save;
tuned;
wenzelm@8364
     1
(*  Title:      Pure/Isar/rule_cases.ML
wenzelm@8364
     2
    ID:         $Id$
wenzelm@8364
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@8364
     5
wenzelm@8364
     6
Manage local contexts of rules.
wenzelm@8364
     7
*)
wenzelm@8364
     8
wenzelm@8364
     9
signature RULE_CASES =
wenzelm@8364
    10
sig
wenzelm@10530
    11
  val consumes: int -> 'a attribute
wenzelm@10530
    12
  val consumes_default: int -> 'a attribute
wenzelm@8364
    13
  val name: string list -> thm -> thm
wenzelm@8427
    14
  val case_names: string list -> 'a attribute
wenzelm@10530
    15
  val get: thm -> string list * int
wenzelm@10530
    16
  val add: thm -> thm * (string list * int)
wenzelm@10530
    17
  val save: thm -> thm -> thm
wenzelm@10530
    18
  type T (* = (string * typ) list * term list *)
wenzelm@9290
    19
  val make: bool -> thm -> string list -> (string * T) list
wenzelm@8427
    20
  val rename_params: string list list -> thm -> thm
wenzelm@8364
    21
  val params: string list list -> 'a attribute
wenzelm@8364
    22
end;
wenzelm@8364
    23
wenzelm@8364
    24
structure RuleCases: RULE_CASES =
wenzelm@8364
    25
struct
wenzelm@8364
    26
wenzelm@10530
    27
(* number of consumed facts *)
wenzelm@8364
    28
wenzelm@10530
    29
val consumesN = "consumes";
wenzelm@10530
    30
wenzelm@10530
    31
fun lookup_consumes thm = Library.assoc (Thm.tags_of_thm thm, consumesN);
wenzelm@8364
    32
wenzelm@10530
    33
fun get_consumes thm =
wenzelm@10530
    34
  let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in
wenzelm@10530
    35
    (case lookup_consumes thm of
wenzelm@10530
    36
      None => 0
wenzelm@10530
    37
    | Some [s] => (case Syntax.read_nat s of Some n => n | _ => err ())
wenzelm@10530
    38
    | _ => err ())
wenzelm@10530
    39
  end;
wenzelm@10530
    40
wenzelm@10530
    41
fun put_consumes n = Drule.tag_rule (consumesN, [Library.string_of_int n]);
wenzelm@10530
    42
val save_consumes = put_consumes o get_consumes;
wenzelm@10530
    43
wenzelm@10530
    44
fun consumes n x = Drule.rule_attribute (K (put_consumes n)) x;
wenzelm@10530
    45
fun consumes_default n x = if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
wenzelm@8364
    46
wenzelm@8364
    47
wenzelm@8364
    48
(* case names *)
wenzelm@8364
    49
wenzelm@10530
    50
val casesN = "cases";
wenzelm@10530
    51
wenzelm@8364
    52
fun name names thm =
wenzelm@8364
    53
  thm
wenzelm@8497
    54
  |> Drule.untag_rule casesN
wenzelm@8364
    55
  |> Drule.tag_rule (casesN, names);
wenzelm@8364
    56
wenzelm@10530
    57
fun get_case_names thm = Library.assocs (Thm.tags_of_thm thm) casesN;
wenzelm@10530
    58
val save_case_names = name o get_case_names;
wenzelm@10530
    59
wenzelm@8427
    60
fun case_names ss = Drule.rule_attribute (K (name ss));
wenzelm@8364
    61
wenzelm@10530
    62
wenzelm@10530
    63
(* access hints *)
wenzelm@10530
    64
wenzelm@10530
    65
fun get thm = (get_case_names thm, get_consumes thm);
wenzelm@8364
    66
fun add thm = (thm, get thm);
wenzelm@10530
    67
wenzelm@10530
    68
fun save thm = save_case_names thm o save_consumes thm;
wenzelm@8364
    69
wenzelm@8364
    70
wenzelm@8364
    71
(* prepare cases *)
wenzelm@8364
    72
wenzelm@10530
    73
type T = (string * typ) list * term list;
wenzelm@10530
    74
wenzelm@10407
    75
fun prep_case open_parms thm name i =
wenzelm@8364
    76
  let
wenzelm@8364
    77
    val (_, _, Bi, _) = Thm.dest_state (thm, i)
wenzelm@8364
    78
      handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
wenzelm@10407
    79
    val rev_params = map (if open_parms then I else apfst Syntax.internal)
wenzelm@9290
    80
      (rename_wrt_term Bi (Logic.strip_params Bi));
wenzelm@8364
    81
    val rev_frees = map Free rev_params;
wenzelm@8364
    82
    val props = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp Bi);
wenzelm@8364
    83
  in (name, (rev rev_params, props)) end;
wenzelm@8364
    84
wenzelm@10407
    85
fun make open_parms thm names =
wenzelm@10407
    86
  #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms thm name i :: cases, i - 1))
wenzelm@8364
    87
    (Library.drop (length names - Thm.nprems_of thm, names), ([], Thm.nprems_of thm)));
wenzelm@8364
    88
wenzelm@8364
    89
wenzelm@8427
    90
(* params *)
wenzelm@8364
    91
wenzelm@8364
    92
fun rename_params xss thm =
wenzelm@8636
    93
  #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss))
wenzelm@10530
    94
  |> save thm;
wenzelm@8364
    95
wenzelm@8364
    96
fun params xss = Drule.rule_attribute (K (rename_params xss));
wenzelm@8364
    97
wenzelm@8364
    98
wenzelm@8364
    99
end;