src/Pure/Isar/rule_cases.ML
author wenzelm
Tue Jan 15 00:13:20 2002 +0100 (2002-01-15)
changeset 12761 b0c39f9837af
parent 12166 5fc22b8c03e9
child 12809 787ecc2ac737
permissions -rw-r--r--
save: be slightly more about absent tags;
get/add: missing case_names default to numbers 1, 2, 3, ...;
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@12761
    15
  val save: thm -> thm -> thm
wenzelm@10530
    16
  val get: thm -> string list * int
wenzelm@10530
    17
  val add: thm -> thm * (string list * int)
wenzelm@10811
    18
  type T
wenzelm@12166
    19
  val empty: T
wenzelm@9290
    20
  val make: 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@12761
    37
fun lookup_consumes thm =
wenzelm@10530
    38
  let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in
wenzelm@12761
    39
    (case Library.assoc (Thm.tags_of_thm thm, consumes_tagN) of
wenzelm@12761
    40
      None => None
wenzelm@12761
    41
    | Some [s] => (case Syntax.read_nat s of Some n => Some n | _ => err ())
wenzelm@10530
    42
    | _ => err ())
wenzelm@10530
    43
  end;
wenzelm@10530
    44
wenzelm@12761
    45
fun put_consumes None th = th
wenzelm@12761
    46
  | put_consumes (Some n) th = th
wenzelm@12761
    47
      |> Drule.untag_rule consumes_tagN
wenzelm@12761
    48
      |> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
wenzelm@10530
    49
wenzelm@12761
    50
val save_consumes = put_consumes o lookup_consumes;
wenzelm@12761
    51
wenzelm@12761
    52
fun consumes n x = Drule.rule_attribute (K (put_consumes (Some n))) x;
wenzelm@10530
    53
fun consumes_default n x = if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
wenzelm@8364
    54
wenzelm@8364
    55
wenzelm@8364
    56
(* case names *)
wenzelm@8364
    57
wenzelm@12761
    58
fun put_case_names None thm = thm
wenzelm@12761
    59
  | put_case_names (Some names) thm =
wenzelm@12761
    60
      thm
wenzelm@12761
    61
      |> Drule.untag_rule cases_tagN
wenzelm@12761
    62
      |> Drule.tag_rule (cases_tagN, names);
wenzelm@8364
    63
wenzelm@12761
    64
fun lookup_case_names thm = Library.assoc (Thm.tags_of_thm thm, cases_tagN);
wenzelm@10530
    65
wenzelm@12761
    66
val save_case_names = put_case_names o lookup_case_names;
wenzelm@12761
    67
val name = put_case_names o Some;
wenzelm@8427
    68
fun case_names ss = Drule.rule_attribute (K (name ss));
wenzelm@8364
    69
wenzelm@10530
    70
wenzelm@10530
    71
(* access hints *)
wenzelm@10530
    72
wenzelm@12761
    73
fun save thm = save_case_names thm o save_consumes thm;
wenzelm@12761
    74
wenzelm@12761
    75
fun get thm =
wenzelm@12761
    76
  let
wenzelm@12761
    77
    val n = if_none (lookup_consumes thm) 0;
wenzelm@12761
    78
    val ss =
wenzelm@12761
    79
      (case lookup_case_names thm of
wenzelm@12761
    80
        None => map Library.string_of_int (1 upto (Thm.nprems_of thm - n))
wenzelm@12761
    81
      | Some ss => ss);
wenzelm@12761
    82
  in (ss, n) end;
wenzelm@12761
    83
wenzelm@8364
    84
fun add thm = (thm, get thm);
wenzelm@10530
    85
wenzelm@8364
    86
wenzelm@8364
    87
(* prepare cases *)
wenzelm@8364
    88
wenzelm@10811
    89
type T = {fixes: (string * typ) list, assumes: term list, binds: (indexname * term option) list};
wenzelm@10530
    90
wenzelm@12166
    91
val empty = {fixes = [], assumes = [], binds = []};
wenzelm@12166
    92
wenzelm@11983
    93
fun prep_case open_parms thm name i =
wenzelm@8364
    94
  let
wenzelm@8364
    95
    val (_, _, Bi, _) = Thm.dest_state (thm, i)
wenzelm@8364
    96
      handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
wenzelm@10830
    97
    val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi);
wenzelm@10811
    98
    val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
wenzelm@10872
    99
    val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
wenzelm@11983
   100
    val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment (Thm.sign_of_thm thm) concl));
wenzelm@10872
   101
  in (name, {fixes = xs, assumes = asms, binds = [bind]}) end;
wenzelm@8364
   102
wenzelm@11983
   103
fun make open_parms raw_thm names =
wenzelm@10811
   104
  let val thm = Tactic.norm_hhf raw_thm in
wenzelm@11983
   105
    #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms thm name i :: cases, i - 1))
wenzelm@11983
   106
      (Library.drop (length names - Thm.nprems_of thm, names), ([], length names)))
wenzelm@10811
   107
  end;
wenzelm@8364
   108
wenzelm@8364
   109
wenzelm@8427
   110
(* params *)
wenzelm@8364
   111
oheimb@11002
   112
fun rename_params xss thm = foldln Thm.rename_params_rule xss thm
wenzelm@10530
   113
  |> save thm;
wenzelm@8364
   114
wenzelm@8364
   115
fun params xss = Drule.rule_attribute (K (rename_params xss));
wenzelm@8364
   116
wenzelm@8364
   117
end;