src/Pure/Isar/rule_cases.ML
author wenzelm
Wed, 08 Mar 2000 17:48:31 +0100
changeset 8364 0eb9ee70c8f8
child 8400 64921d1fef15
permissions -rw-r--r--
added Isar/rule_cases.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/rule_cases.ML
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     4
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     5
Manage local contexts of rules.
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     6
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     7
TODO:
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     8
  - instantiation of cases (including type vars!);
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     9
*)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    10
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    11
signature RULE_CASES =
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    12
sig
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    13
  type T (* = (string * typ) list * term list *)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    14
  val name: string list -> thm -> thm
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    15
  val get: thm -> string list
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    16
  val add: thm -> thm * string list
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    17
  val none: thm -> thm * string list
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    18
  val make: thm -> string list -> (string * T) list
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    19
  val case_names: string list -> 'a attribute
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    20
  val params: string list list -> 'a attribute
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    21
end;
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    22
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    23
structure RuleCases: RULE_CASES =
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    24
struct
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    25
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    26
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    27
(* local contexts *)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    28
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    29
type T = (string * typ) list * term list;
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    30
val casesN = "cases";
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    31
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    32
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    33
(* case names *)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    34
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    35
fun name names thm =
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    36
  thm
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    37
  |> Drule.untag_rule (casesN, [])
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    38
  |> Drule.tag_rule (casesN, names);
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    39
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    40
fun get thm =
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    41
  (case assoc (Thm.tags_of_thm thm, casesN) of
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    42
    None => map Library.string_of_int (1 upto Thm.nprems_of thm)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    43
  | Some names => names);
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    44
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    45
fun add thm = (thm, get thm);
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    46
fun none thm = (thm, []);
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    47
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    48
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    49
(* prepare cases *)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    50
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    51
fun prep_case thm name i =
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    52
  let
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    53
    val (_, _, Bi, _) = Thm.dest_state (thm, i)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    54
      handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    55
    val rev_params = rename_wrt_term Bi (Logic.strip_params Bi);
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    56
    val rev_frees = map Free rev_params;
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    57
    val props = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp Bi);
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    58
  in (name, (rev rev_params, props)) end;
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    59
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    60
fun make thm names =
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    61
  #1 (foldr (fn (name, (cases, i)) => (prep_case thm name i :: cases, i - 1))
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    62
    (Library.drop (length names - Thm.nprems_of thm, names), ([], Thm.nprems_of thm)));
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    63
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    64
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    65
(* attributes *)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    66
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    67
fun case_names ss = Drule.rule_attribute (K (name ss));
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    68
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    69
fun rename_params xss thm =
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    70
  #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss));
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    71
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    72
fun params xss = Drule.rule_attribute (K (rename_params xss));
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    73
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    74
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    75
end;