src/Pure/Isar/rule_cases.ML
author wenzelm
Wed Dec 05 03:18:03 2001 +0100 (2001-12-05 ago)
changeset 12385 389d11fb62c8
parent 12166 5fc22b8c03e9
child 12761 b0c39f9837af
permissions -rw-r--r--
removed unused functionality (weight etc.);
     1 (*  Title:      Pure/Isar/rule_cases.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Manage local contexts of rules.
     7 *)
     8 
     9 signature RULE_CASES =
    10 sig
    11   val consumes: int -> 'a attribute
    12   val consumes_default: int -> 'a attribute
    13   val name: string list -> thm -> thm
    14   val case_names: string list -> 'a attribute
    15   val get: thm -> string list * int
    16   val add: thm -> thm * (string list * int)
    17   val save: thm -> thm -> thm
    18   type T
    19   val empty: T
    20   val make: bool -> thm -> string list -> (string * T) list
    21   val rename_params: string list list -> thm -> thm
    22   val params: string list list -> 'a attribute
    23 end;
    24 
    25 structure RuleCases: RULE_CASES =
    26 struct
    27 
    28 (* names *)
    29 
    30 val consumes_tagN = "consumes";
    31 val cases_tagN = "cases";
    32 val case_conclN = "case";
    33 
    34 
    35 (* number of consumed facts *)
    36 
    37 fun lookup_consumes thm = Library.assoc (Thm.tags_of_thm thm, consumes_tagN);
    38 
    39 fun get_consumes thm =
    40   let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in
    41     (case lookup_consumes thm of
    42       None => 0
    43     | Some [s] => (case Syntax.read_nat s of Some n => n | _ => err ())
    44     | _ => err ())
    45   end;
    46 
    47 fun put_consumes n =
    48   Drule.tag_rule (consumes_tagN, [Library.string_of_int n]) o Drule.untag_rule consumes_tagN;
    49 val save_consumes = put_consumes o get_consumes;
    50 
    51 fun consumes n x = Drule.rule_attribute (K (put_consumes n)) x;
    52 fun consumes_default n x = if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
    53 
    54 
    55 (* case names *)
    56 
    57 fun name names thm =
    58   thm
    59   |> Drule.untag_rule cases_tagN
    60   |> Drule.tag_rule (cases_tagN, names);
    61 
    62 fun get_case_names thm = Library.assocs (Thm.tags_of_thm thm) cases_tagN;
    63 val save_case_names = name o get_case_names;
    64 
    65 fun case_names ss = Drule.rule_attribute (K (name ss));
    66 
    67 
    68 (* access hints *)
    69 
    70 fun get thm = (get_case_names thm, get_consumes thm);
    71 fun add thm = (thm, get thm);
    72 
    73 fun save thm = save_case_names thm o save_consumes thm;
    74 
    75 
    76 (* prepare cases *)
    77 
    78 type T = {fixes: (string * typ) list, assumes: term list, binds: (indexname * term option) list};
    79 
    80 val empty = {fixes = [], assumes = [], binds = []};
    81 
    82 fun prep_case open_parms thm name i =
    83   let
    84     val (_, _, Bi, _) = Thm.dest_state (thm, i)
    85       handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
    86     val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi);
    87     val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
    88     val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
    89     val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment (Thm.sign_of_thm thm) concl));
    90   in (name, {fixes = xs, assumes = asms, binds = [bind]}) end;
    91 
    92 fun make open_parms raw_thm names =
    93   let val thm = Tactic.norm_hhf raw_thm in
    94     #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms thm name i :: cases, i - 1))
    95       (Library.drop (length names - Thm.nprems_of thm, names), ([], length names)))
    96   end;
    97 
    98 
    99 (* params *)
   100 
   101 fun rename_params xss thm = foldln Thm.rename_params_rule xss thm
   102   |> save thm;
   103 
   104 fun params xss = Drule.rule_attribute (K (rename_params xss));
   105 
   106 
   107 end;