src/Pure/Isar/rule_cases.ML
author skalberg
Sun Feb 13 17:15:14 2005 +0100 (2005-02-13)
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
permissions -rw-r--r--
Deleted Library.option type.
wenzelm@8364
     1
(*  Title:      Pure/Isar/rule_cases.ML
wenzelm@8364
     2
    ID:         $Id$
wenzelm@8364
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8364
     4
wenzelm@8364
     5
Manage local contexts of rules.
wenzelm@8364
     6
*)
wenzelm@8364
     7
wenzelm@8364
     8
signature RULE_CASES =
wenzelm@8364
     9
sig
wenzelm@10530
    10
  val consumes: int -> 'a attribute
wenzelm@10530
    11
  val consumes_default: int -> 'a attribute
wenzelm@8364
    12
  val name: string list -> thm -> thm
wenzelm@8427
    13
  val case_names: string list -> 'a attribute
wenzelm@12761
    14
  val save: thm -> thm -> thm
wenzelm@10530
    15
  val get: thm -> string list * int
wenzelm@10530
    16
  val add: thm -> thm * (string list * int)
wenzelm@10811
    17
  type T
wenzelm@12166
    18
  val empty: T
nipkow@14404
    19
  val make: bool -> term option -> Sign.sg * term -> 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@12761
    36
fun lookup_consumes thm =
wenzelm@10530
    37
  let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in
wenzelm@12761
    38
    (case Library.assoc (Thm.tags_of_thm thm, consumes_tagN) of
skalberg@15531
    39
      NONE => NONE
skalberg@15531
    40
    | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ())
wenzelm@10530
    41
    | _ => err ())
wenzelm@10530
    42
  end;
wenzelm@10530
    43
skalberg@15531
    44
fun put_consumes NONE th = th
skalberg@15531
    45
  | put_consumes (SOME n) th = th
wenzelm@12761
    46
      |> Drule.untag_rule consumes_tagN
wenzelm@12761
    47
      |> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
wenzelm@10530
    48
wenzelm@12761
    49
val save_consumes = put_consumes o lookup_consumes;
wenzelm@12761
    50
skalberg@15531
    51
fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x;
wenzelm@10530
    52
fun consumes_default n x = if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
wenzelm@8364
    53
wenzelm@8364
    54
wenzelm@8364
    55
(* case names *)
wenzelm@8364
    56
skalberg@15531
    57
fun put_case_names NONE thm = thm
skalberg@15531
    58
  | put_case_names (SOME names) thm =
wenzelm@12761
    59
      thm
wenzelm@12761
    60
      |> Drule.untag_rule cases_tagN
wenzelm@12761
    61
      |> Drule.tag_rule (cases_tagN, names);
wenzelm@8364
    62
wenzelm@12761
    63
fun lookup_case_names thm = Library.assoc (Thm.tags_of_thm thm, cases_tagN);
wenzelm@10530
    64
wenzelm@12761
    65
val save_case_names = put_case_names o lookup_case_names;
skalberg@15531
    66
val name = put_case_names o SOME;
wenzelm@8427
    67
fun case_names ss = Drule.rule_attribute (K (name ss));
wenzelm@8364
    68
wenzelm@10530
    69
wenzelm@10530
    70
(* access hints *)
wenzelm@10530
    71
wenzelm@12761
    72
fun save thm = save_case_names thm o save_consumes thm;
wenzelm@12761
    73
wenzelm@12761
    74
fun get thm =
wenzelm@12761
    75
  let
wenzelm@12761
    76
    val n = if_none (lookup_consumes thm) 0;
wenzelm@12761
    77
    val ss =
wenzelm@12761
    78
      (case lookup_case_names thm of
skalberg@15531
    79
        NONE => map Library.string_of_int (1 upto (Thm.nprems_of thm - n))
skalberg@15531
    80
      | SOME ss => ss);
wenzelm@12761
    81
  in (ss, n) end;
wenzelm@12761
    82
wenzelm@8364
    83
fun add thm = (thm, get thm);
wenzelm@10530
    84
wenzelm@8364
    85
wenzelm@8364
    86
(* prepare cases *)
wenzelm@8364
    87
wenzelm@13425
    88
type T =
wenzelm@13425
    89
 {fixes: (string * typ) list,
wenzelm@13425
    90
  assumes: (string * term list) list,
wenzelm@13425
    91
  binds: (indexname * term option) list};
wenzelm@13425
    92
wenzelm@13425
    93
val hypsN = "hyps";
wenzelm@13425
    94
val premsN = "prems";
wenzelm@10530
    95
wenzelm@12166
    96
val empty = {fixes = [], assumes = [], binds = []};
wenzelm@12166
    97
nipkow@13596
    98
fun nth_subgoal(i,prop) =
berghofe@13668
    99
  hd (#1 (Logic.strip_prems (i, [], prop)));
nipkow@13596
   100
  
nipkow@14404
   101
fun prep_case is_open split sg prop name i =
wenzelm@8364
   102
  let
nipkow@14404
   103
    val Bi = Drule.norm_hhf sg (nth_subgoal(i,prop));
nipkow@13596
   104
    val all_xs = Logic.strip_params Bi
skalberg@15531
   105
    val n = (case split of NONE => length all_xs
skalberg@15531
   106
             | SOME t => length (Logic.strip_params(nth_subgoal(i,t))))
nipkow@13629
   107
    val (ind_xs, goal_xs) = splitAt(n,all_xs)
nipkow@14404
   108
    val rename = if is_open then I else apfst Syntax.internal
nipkow@13596
   109
    val xs = map rename ind_xs @ goal_xs
wenzelm@10811
   110
    val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
wenzelm@13425
   111
    val named_asms =
skalberg@15531
   112
      (case split of NONE => [("", asms)]
skalberg@15531
   113
      | SOME t =>
nipkow@13596
   114
          let val h = length (Logic.strip_assums_hyp(nth_subgoal(i,t)))
nipkow@13629
   115
              val (ps,qs) = splitAt(h, asms)
nipkow@13629
   116
          in [(hypsN, ps), (premsN, qs)] end);
wenzelm@10872
   117
    val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
skalberg@15531
   118
    val bind = ((case_conclN, 0), SOME (ObjectLogic.drop_judgment sg concl));
wenzelm@13425
   119
  in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end;
wenzelm@8364
   120
nipkow@14404
   121
fun make is_open split (sg, prop) names =
berghofe@13668
   122
  let val nprems = Logic.count_prems (prop, 0) in
nipkow@14404
   123
    foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
wenzelm@13425
   124
      (Library.drop (length names - nprems, names), ([], length names)) |> #1
wenzelm@10811
   125
  end;
wenzelm@8364
   126
wenzelm@8364
   127
wenzelm@8427
   128
(* params *)
wenzelm@8364
   129
oheimb@11002
   130
fun rename_params xss thm = foldln Thm.rename_params_rule xss thm
wenzelm@10530
   131
  |> save thm;
wenzelm@8364
   132
wenzelm@8364
   133
fun params xss = Drule.rule_attribute (K (rename_params xss));
wenzelm@8364
   134
wenzelm@8364
   135
end;