src/Pure/Isar/rule_cases.ML
author wenzelm
Wed Nov 23 18:52:04 2005 +0100 (2005-11-23)
changeset 18237 2edb6a1f9c14
parent 18229 e5a624483a23
child 18256 8de262a22f23
permissions -rw-r--r--
consume: proper treatment of defs;
simplified case_conclusion;
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@18229
     5
Annotations and local contexts of rules.
wenzelm@8364
     6
*)
wenzelm@8364
     7
wenzelm@18188
     8
infix 1 THEN_ALL_NEW_CASES;
wenzelm@18188
     9
wenzelm@18229
    10
signature BASIC_RULE_CASES =
wenzelm@18229
    11
sig
wenzelm@18229
    12
  type cases
wenzelm@18229
    13
  type cases_tactic
wenzelm@18229
    14
  val CASES: cases -> tactic -> cases_tactic
wenzelm@18229
    15
  val NO_CASES: tactic -> cases_tactic
wenzelm@18229
    16
  val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic
wenzelm@18229
    17
  val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
wenzelm@18229
    18
end
wenzelm@18229
    19
wenzelm@8364
    20
signature RULE_CASES =
wenzelm@8364
    21
sig
wenzelm@18229
    22
  include BASIC_RULE_CASES
wenzelm@18229
    23
  type T
wenzelm@18237
    24
  val consume: thm list -> thm list -> ('a * int) * thm ->
wenzelm@18237
    25
    (('a * (int * thm list)) * thm) Seq.seq
wenzelm@10530
    26
  val consumes: int -> 'a attribute
wenzelm@10530
    27
  val consumes_default: int -> 'a attribute
wenzelm@8364
    28
  val name: string list -> thm -> thm
wenzelm@8427
    29
  val case_names: string list -> 'a attribute
wenzelm@18237
    30
  val case_conclusion: string * string list -> 'a attribute
wenzelm@12761
    31
  val save: thm -> thm -> thm
wenzelm@18237
    32
  val get: thm -> (string * string list) list * int
wenzelm@17861
    33
  val strip_params: term -> (string * typ) list
wenzelm@18237
    34
  val make: bool -> term option -> theory * term -> (string * string list) list -> cases
wenzelm@17361
    35
  val simple: bool -> theory * term -> string -> string * T option
wenzelm@8427
    36
  val rename_params: string list list -> thm -> thm
wenzelm@8364
    37
  val params: string list list -> 'a attribute
wenzelm@8364
    38
end;
wenzelm@8364
    39
wenzelm@8364
    40
structure RuleCases: RULE_CASES =
wenzelm@8364
    41
struct
wenzelm@8364
    42
wenzelm@18229
    43
(** tactics with cases **)
wenzelm@18229
    44
wenzelm@18229
    45
type T =
wenzelm@18229
    46
 {fixes: (string * typ) list,
wenzelm@18229
    47
  assumes: (string * term list) list,
wenzelm@18229
    48
  binds: (indexname * term option) list};
wenzelm@18229
    49
wenzelm@18229
    50
type cases = (string * T option) list;
wenzelm@18229
    51
type cases_tactic = thm -> (cases * thm) Seq.seq;
wenzelm@18229
    52
wenzelm@18229
    53
fun CASES cases tac st = Seq.map (pair cases) (tac st);
wenzelm@18229
    54
fun NO_CASES tac = CASES [] tac;
wenzelm@18229
    55
wenzelm@18229
    56
fun SUBGOAL_CASES tac i st =
wenzelm@18229
    57
  (case try Logic.nth_prem (i, Thm.prop_of st) of
wenzelm@18229
    58
    SOME goal => tac (goal, i) st
wenzelm@18229
    59
  | NONE => Seq.empty);
wenzelm@18229
    60
wenzelm@18229
    61
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
wenzelm@18229
    62
  st |> tac1 i |> Seq.maps (fn (cases, st') =>
wenzelm@18237
    63
    CASES cases (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st)) st');
wenzelm@18229
    64
wenzelm@18229
    65
wenzelm@18229
    66
wenzelm@18229
    67
(** consume facts **)
wenzelm@18229
    68
wenzelm@18237
    69
fun consume defs facts ((x, n), th) =
wenzelm@18237
    70
  let val m = Int.min (length facts, n) in
wenzelm@18237
    71
    th |> K (not (null defs)) ?
wenzelm@18237
    72
      Drule.fconv_rule (Drule.goals_conv (fn i => i <= m) (Tactic.rewrite true defs))
wenzelm@18237
    73
    |> Drule.multi_resolve (Library.take (m, facts))
wenzelm@18237
    74
    |> Seq.map (pair (x, (n - m, Library.drop (m, facts))))
wenzelm@18237
    75
  end;
wenzelm@10811
    76
wenzelm@10811
    77
val consumes_tagN = "consumes";
wenzelm@10811
    78
wenzelm@18229
    79
fun lookup_consumes th =
wenzelm@18229
    80
  let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in
wenzelm@18229
    81
    (case AList.lookup (op =) (Thm.tags_of_thm th) (consumes_tagN) of
skalberg@15531
    82
      NONE => NONE
skalberg@15531
    83
    | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ())
wenzelm@10530
    84
    | _ => err ())
wenzelm@10530
    85
  end;
wenzelm@10530
    86
skalberg@15531
    87
fun put_consumes NONE th = th
skalberg@15531
    88
  | put_consumes (SOME n) th = th
wenzelm@12761
    89
      |> Drule.untag_rule consumes_tagN
wenzelm@12761
    90
      |> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
wenzelm@10530
    91
wenzelm@12761
    92
val save_consumes = put_consumes o lookup_consumes;
wenzelm@12761
    93
skalberg@15531
    94
fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x;
wenzelm@16148
    95
fun consumes_default n x =
wenzelm@16148
    96
  if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
wenzelm@8364
    97
wenzelm@8364
    98
wenzelm@18229
    99
wenzelm@18229
   100
(** case names **)
wenzelm@18229
   101
wenzelm@18237
   102
val case_names_tagN = "case_names";
wenzelm@8364
   103
wenzelm@18229
   104
fun add_case_names NONE = I
wenzelm@18229
   105
  | add_case_names (SOME names) =
wenzelm@18237
   106
      Drule.untag_rule case_names_tagN
wenzelm@18237
   107
      #> Drule.tag_rule (case_names_tagN, names);
wenzelm@8364
   108
wenzelm@18237
   109
fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) case_names_tagN;
wenzelm@10530
   110
wenzelm@18229
   111
val save_case_names = add_case_names o lookup_case_names;
wenzelm@18229
   112
val name = add_case_names o SOME;
wenzelm@8427
   113
fun case_names ss = Drule.rule_attribute (K (name ss));
wenzelm@8364
   114
wenzelm@10530
   115
wenzelm@18229
   116
wenzelm@18229
   117
(** case conclusions **)
wenzelm@18229
   118
wenzelm@18229
   119
val case_concl_tagN = "case_conclusion";
wenzelm@18229
   120
wenzelm@18229
   121
fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name)
wenzelm@18229
   122
  | is_case_concl _ _ = false;
wenzelm@18229
   123
wenzelm@18229
   124
fun add_case_concl (name, cs) = Drule.map_tags (fn tags =>
wenzelm@18229
   125
  filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]);
wenzelm@18229
   126
wenzelm@18229
   127
fun get_case_concls th name =
wenzelm@18237
   128
  (case find_first (is_case_concl name) (Thm.tags_of_thm th) of
wenzelm@18237
   129
    SOME (_, _ :: cs) => cs
wenzelm@18237
   130
  | _ => []);
wenzelm@18229
   131
wenzelm@18229
   132
fun save_case_concls th =
wenzelm@18229
   133
  let val concls = Thm.tags_of_thm th |> List.mapPartial
wenzelm@18237
   134
    (fn (a, b :: cs) =>
wenzelm@18237
   135
      if a = case_concl_tagN then SOME (b, cs) else NONE
wenzelm@18229
   136
    | _ => NONE)
wenzelm@18229
   137
  in fold add_case_concl concls end;
wenzelm@18229
   138
wenzelm@18237
   139
fun case_conclusion concl = Drule.rule_attribute (fn _ => add_case_concl concl);
wenzelm@18229
   140
wenzelm@18229
   141
wenzelm@18229
   142
wenzelm@18229
   143
(** case declarations **)
wenzelm@18229
   144
wenzelm@10530
   145
(* access hints *)
wenzelm@10530
   146
wenzelm@18229
   147
fun save th = save_consumes th #> save_case_names th #> save_case_concls th;
wenzelm@12761
   148
wenzelm@18229
   149
fun get th =
wenzelm@12761
   150
  let
wenzelm@18229
   151
    val n = the_default 0 (lookup_consumes th);
wenzelm@18229
   152
    val cases =
wenzelm@18229
   153
      (case lookup_case_names th of
wenzelm@18229
   154
        NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
wenzelm@18229
   155
      | SOME names => map (fn name => (name, get_case_concls th name)) names);
wenzelm@18229
   156
  in (cases, n) end;
wenzelm@10530
   157
wenzelm@8364
   158
wenzelm@18229
   159
(* extract cases *)
wenzelm@8364
   160
wenzelm@18229
   161
val case_conclN = "case";
wenzelm@18229
   162
val case_hypsN = "hyps";
wenzelm@18229
   163
val case_premsN = "prems";
wenzelm@13425
   164
wenzelm@18188
   165
val strip_params = map (apfst Syntax.deskolem) o Logic.strip_params;
wenzelm@17167
   166
wenzelm@18237
   167
fun dest_binops cs tm =
wenzelm@18237
   168
  let
wenzelm@18237
   169
    val n = length cs;
wenzelm@18237
   170
    fun dest 0 _ = []
wenzelm@18237
   171
      | dest 1 t = [t]
wenzelm@18237
   172
      | dest k (_ $ t $ u) = t :: dest (k - 1) u
wenzelm@18237
   173
      | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
wenzelm@18237
   174
  in cs ~~ dest n tm end;
wenzelm@18237
   175
wenzelm@18229
   176
fun extract_case is_open thy (split, raw_prop) name concls =
wenzelm@8364
   177
  let
wenzelm@17361
   178
    val prop = Drule.norm_hhf thy raw_prop;
wenzelm@16148
   179
wenzelm@17861
   180
    val xs = strip_params prop;
wenzelm@16148
   181
    val rename = if is_open then I else map (apfst Syntax.internal);
wenzelm@18229
   182
    val fixes =
wenzelm@16148
   183
      (case split of
wenzelm@16148
   184
        NONE => rename xs
wenzelm@16148
   185
      | SOME t =>
wenzelm@16148
   186
          let val (us, vs) = splitAt (length (Logic.strip_params t), xs)
wenzelm@16148
   187
          in rename us @ vs end);
wenzelm@18229
   188
    fun abs_fixes t = Term.list_abs (fixes, t);
wenzelm@16148
   189
wenzelm@18229
   190
    val asms = map abs_fixes (Logic.strip_assums_hyp prop);
wenzelm@18229
   191
    val assumes =
wenzelm@16148
   192
      (case split of
wenzelm@16148
   193
        NONE => [("", asms)]
skalberg@15531
   194
      | SOME t =>
wenzelm@16148
   195
          let val (hyps, prems) = splitAt (length (Logic.strip_assums_hyp t), asms)
wenzelm@16148
   196
          in [(case_hypsN, hyps), (case_premsN, prems)] end);
wenzelm@16148
   197
wenzelm@18229
   198
    val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
wenzelm@18237
   199
    val binds = (case_conclN, concl) :: dest_binops concls concl
wenzelm@18237
   200
      |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
wenzelm@18229
   201
  in {fixes = fixes, assumes = assumes, binds = binds} end;
wenzelm@8364
   202
wenzelm@18229
   203
fun make is_open split (thy, prop) cases =
wenzelm@16148
   204
  let
wenzelm@18229
   205
    val n = length cases;
wenzelm@16148
   206
    val nprems = Logic.count_prems (prop, 0);
wenzelm@18229
   207
    fun add_case (name, concls) (cs, i) =
wenzelm@16148
   208
      ((case try (fn () =>
wenzelm@16148
   209
          (Option.map (curry Logic.nth_prem i) split, Logic.nth_prem (i, prop))) () of
wenzelm@16148
   210
        NONE => (name, NONE)
wenzelm@18229
   211
      | SOME sp => (name, SOME (extract_case is_open thy sp name concls))) :: cs, i - 1);
wenzelm@18229
   212
  in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end;
wenzelm@8364
   213
wenzelm@18229
   214
fun simple is_open (thy, prop) name =
wenzelm@18229
   215
  (name, SOME (extract_case is_open thy (NONE, prop) name []));
wenzelm@17361
   216
wenzelm@8364
   217
wenzelm@8427
   218
(* params *)
wenzelm@8364
   219
wenzelm@18229
   220
fun rename_params xss th =
wenzelm@18229
   221
  th
wenzelm@18229
   222
  |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
wenzelm@18229
   223
  |> save th;
wenzelm@8364
   224
wenzelm@8364
   225
fun params xss = Drule.rule_attribute (K (rename_params xss));
wenzelm@8364
   226
wenzelm@8364
   227
end;
wenzelm@17113
   228
wenzelm@18229
   229
structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;
wenzelm@18229
   230
open BasicRuleCases;