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