src/Pure/Isar/rule_cases.ML
author wenzelm
Thu Jan 11 19:38:37 2001 +0100 (2001-01-11 ago)
changeset 10872 87bb4462c434
parent 10830 d19f9f4c35ee
child 10886 f6b16554720d
permissions -rw-r--r--
make_raw: do not AutoBind.drop_judgment;
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@10811
    18
  type T
wenzelm@9290
    19
  val make: bool -> thm -> string list -> (string * T) list
wenzelm@10872
    20
  val make_raw: bool -> thm -> string list -> (string * T) list
wenzelm@8427
    21
  val rename_params: string list list -> thm -> thm
wenzelm@8364
    22
  val params: string list list -> 'a attribute
wenzelm@8364
    23
end;
wenzelm@8364
    24
wenzelm@8364
    25
structure RuleCases: RULE_CASES =
wenzelm@8364
    26
struct
wenzelm@8364
    27
wenzelm@10811
    28
(* names *)
wenzelm@10811
    29
wenzelm@10811
    30
val consumes_tagN = "consumes";
wenzelm@10811
    31
val cases_tagN = "cases";
wenzelm@10811
    32
val case_conclN = "case";
wenzelm@10811
    33
wenzelm@10811
    34
wenzelm@10530
    35
(* number of consumed facts *)
wenzelm@8364
    36
wenzelm@10811
    37
fun lookup_consumes thm = Library.assoc (Thm.tags_of_thm thm, consumes_tagN);
wenzelm@8364
    38
wenzelm@10530
    39
fun get_consumes thm =
wenzelm@10530
    40
  let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in
wenzelm@10530
    41
    (case lookup_consumes thm of
wenzelm@10530
    42
      None => 0
wenzelm@10530
    43
    | Some [s] => (case Syntax.read_nat s of Some n => n | _ => err ())
wenzelm@10530
    44
    | _ => err ())
wenzelm@10530
    45
  end;
wenzelm@10530
    46
wenzelm@10811
    47
fun put_consumes n = Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
wenzelm@10530
    48
val save_consumes = put_consumes o get_consumes;
wenzelm@10530
    49
wenzelm@10530
    50
fun consumes n x = Drule.rule_attribute (K (put_consumes n)) x;
wenzelm@10530
    51
fun consumes_default n x = if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
wenzelm@8364
    52
wenzelm@8364
    53
wenzelm@8364
    54
(* case names *)
wenzelm@8364
    55
wenzelm@8364
    56
fun name names thm =
wenzelm@8364
    57
  thm
wenzelm@10811
    58
  |> Drule.untag_rule cases_tagN
wenzelm@10811
    59
  |> Drule.tag_rule (cases_tagN, names);
wenzelm@8364
    60
wenzelm@10811
    61
fun get_case_names thm = Library.assocs (Thm.tags_of_thm thm) cases_tagN;
wenzelm@10530
    62
val save_case_names = name o get_case_names;
wenzelm@10530
    63
wenzelm@8427
    64
fun case_names ss = Drule.rule_attribute (K (name ss));
wenzelm@8364
    65
wenzelm@10530
    66
wenzelm@10530
    67
(* access hints *)
wenzelm@10530
    68
wenzelm@10530
    69
fun get thm = (get_case_names thm, get_consumes thm);
wenzelm@8364
    70
fun add thm = (thm, get thm);
wenzelm@10530
    71
wenzelm@10530
    72
fun save thm = save_case_names thm o save_consumes thm;
wenzelm@8364
    73
wenzelm@8364
    74
wenzelm@8364
    75
(* prepare cases *)
wenzelm@8364
    76
wenzelm@10811
    77
type T = {fixes: (string * typ) list, assumes: term list, binds: (indexname * term option) list};
wenzelm@10530
    78
wenzelm@10872
    79
local
wenzelm@10872
    80
wenzelm@10872
    81
fun prep_case raw open_parms thm name i =
wenzelm@8364
    82
  let
wenzelm@8364
    83
    val (_, _, Bi, _) = Thm.dest_state (thm, i)
wenzelm@8364
    84
      handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
wenzelm@10830
    85
    val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi);
wenzelm@10811
    86
    val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
wenzelm@10872
    87
    val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
wenzelm@10872
    88
    val bind = ((case_conclN, 0), Some (if raw then concl else AutoBind.drop_judgment concl));
wenzelm@10872
    89
  in (name, {fixes = xs, assumes = asms, binds = [bind]}) end;
wenzelm@8364
    90
wenzelm@10872
    91
fun gen_make raw open_parms raw_thm names =
wenzelm@10811
    92
  let val thm = Tactic.norm_hhf raw_thm in
wenzelm@10872
    93
    #1 (foldr (fn (name, (cases, i)) => (prep_case raw open_parms thm name i :: cases, i - 1))
wenzelm@10811
    94
      (Library.drop (length names - Thm.nprems_of thm, names), ([], Thm.nprems_of thm)))
wenzelm@10811
    95
  end;
wenzelm@8364
    96
wenzelm@10872
    97
in
wenzelm@10872
    98
wenzelm@10872
    99
val make = gen_make false;
wenzelm@10872
   100
val make_raw = gen_make true;
wenzelm@10872
   101
wenzelm@10872
   102
end;
wenzelm@10872
   103
wenzelm@8364
   104
wenzelm@8427
   105
(* params *)
wenzelm@8364
   106
wenzelm@8364
   107
fun rename_params xss thm =
wenzelm@8636
   108
  #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss))
wenzelm@10530
   109
  |> save thm;
wenzelm@8364
   110
wenzelm@8364
   111
fun params xss = Drule.rule_attribute (K (rename_params xss));
wenzelm@8364
   112
wenzelm@8364
   113
wenzelm@8364
   114
end;