src/Pure/Isar/rule_cases.ML
author wenzelm
Sat Jan 07 12:26:33 2006 +0100 (2006-01-07)
changeset 18608 9cdcc2a5c8b3
parent 18581 6538fdcc98dc
child 18728 6790126ab5f6
permissions -rw-r--r--
support nested cases;
added apply_case;
replaced make/simple by make_common/nested/simple;
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@18608
    23
  datatype T = Case of
wenzelm@18608
    24
   {fixes: (string * typ) list,
wenzelm@18608
    25
    assumes: (string * term list) list,
wenzelm@18608
    26
    binds: (indexname * term option) list,
wenzelm@18608
    27
    cases: (string * T) list}
wenzelm@18608
    28
  val strip_params: term -> (string * typ) list
wenzelm@18608
    29
  val make_common: bool -> theory * term -> (string * string list) list -> cases
wenzelm@18608
    30
  val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases
wenzelm@18608
    31
  val make_simple: bool -> theory * term -> string -> cases
wenzelm@18608
    32
  val apply: term list -> T -> T
wenzelm@18237
    33
  val consume: thm list -> thm list -> ('a * int) * thm ->
wenzelm@18237
    34
    (('a * (int * thm list)) * thm) Seq.seq
wenzelm@18477
    35
  val add_consumes: int -> thm -> thm
wenzelm@10530
    36
  val consumes: int -> 'a attribute
wenzelm@10530
    37
  val consumes_default: int -> 'a attribute
wenzelm@8364
    38
  val name: string list -> thm -> thm
wenzelm@8427
    39
  val case_names: string list -> 'a attribute
wenzelm@18237
    40
  val case_conclusion: string * string list -> 'a attribute
wenzelm@12761
    41
  val save: thm -> thm -> thm
wenzelm@18237
    42
  val get: thm -> (string * string list) list * int
wenzelm@8427
    43
  val rename_params: string list list -> thm -> thm
wenzelm@8364
    44
  val params: string list list -> 'a attribute
wenzelm@18477
    45
  val mutual_rule: thm list -> (int list * thm) option
wenzelm@18581
    46
  val strict_mutual_rule: thm list -> int list * thm
wenzelm@8364
    47
end;
wenzelm@8364
    48
wenzelm@8364
    49
structure RuleCases: RULE_CASES =
wenzelm@8364
    50
struct
wenzelm@8364
    51
wenzelm@18608
    52
(** cases **)
wenzelm@18608
    53
wenzelm@18608
    54
datatype T = Case of
wenzelm@18608
    55
 {fixes: (string * typ) list,
wenzelm@18608
    56
  assumes: (string * term list) list,
wenzelm@18608
    57
  binds: (indexname * term option) list,
wenzelm@18608
    58
  cases: (string * T) list};
wenzelm@18608
    59
wenzelm@18608
    60
type cases = (string * T option) list;
wenzelm@18608
    61
wenzelm@18608
    62
val case_conclN = "case";
wenzelm@18608
    63
val case_hypsN = "hyps";
wenzelm@18608
    64
val case_premsN = "prems";
wenzelm@18608
    65
wenzelm@18608
    66
val strip_params = map (apfst (perhaps (try Syntax.dest_skolem))) o Logic.strip_params;
wenzelm@18608
    67
wenzelm@18608
    68
local
wenzelm@18608
    69
wenzelm@18608
    70
fun abs xs t = Term.list_abs (xs, t);
wenzelm@18608
    71
fun app us t = Term.betapplys (t, us);
wenzelm@18608
    72
wenzelm@18608
    73
fun dest_binops cs tm =
wenzelm@18608
    74
  let
wenzelm@18608
    75
    val n = length cs;
wenzelm@18608
    76
    fun dest 0 _ = []
wenzelm@18608
    77
      | dest 1 t = [t]
wenzelm@18608
    78
      | dest k (_ $ t $ u) = t :: dest (k - 1) u
wenzelm@18608
    79
      | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
wenzelm@18608
    80
  in cs ~~ dest n tm end;
wenzelm@18608
    81
wenzelm@18608
    82
fun extract_fixes NONE prop = (strip_params prop, [])
wenzelm@18608
    83
  | extract_fixes (SOME outline) prop =
wenzelm@18608
    84
      splitAt (length (Logic.strip_params outline), strip_params prop);
wenzelm@18608
    85
wenzelm@18608
    86
fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
wenzelm@18608
    87
  | extract_assumes qual (SOME outline) prop =
wenzelm@18608
    88
      let val (hyps, prems) =
wenzelm@18608
    89
        splitAt (length (Logic.strip_assums_hyp outline), Logic.strip_assums_hyp prop)
wenzelm@18608
    90
      in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
wenzelm@18608
    91
wenzelm@18608
    92
fun extract_case is_open thy (case_outline, raw_prop) name concls =
wenzelm@18608
    93
  let
wenzelm@18608
    94
    val rename = if is_open then I else (apfst Syntax.internal);
wenzelm@18608
    95
wenzelm@18608
    96
    val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
wenzelm@18608
    97
    val len = length props;
wenzelm@18608
    98
    val nested = is_some case_outline andalso len > 1;
wenzelm@18608
    99
wenzelm@18608
   100
    fun extract prop =
wenzelm@18608
   101
      let
wenzelm@18608
   102
        val (fixes1, fixes2) = extract_fixes case_outline prop
wenzelm@18608
   103
          |> apfst (map rename);
wenzelm@18608
   104
        val abs_fixes = abs (fixes1 @ fixes2);
wenzelm@18608
   105
        fun abs_fixes1 t =
wenzelm@18608
   106
          if not nested then abs_fixes t
wenzelm@18608
   107
          else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
wenzelm@18608
   108
wenzelm@18608
   109
        val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop
wenzelm@18608
   110
          |> pairself (map (apsnd (List.concat o map Logic.dest_conjunctions)));
wenzelm@18608
   111
wenzelm@18608
   112
        val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
wenzelm@18608
   113
        val binds =
wenzelm@18608
   114
          (case_conclN, concl) :: dest_binops concls concl
wenzelm@18608
   115
          |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
wenzelm@18608
   116
      in
wenzelm@18608
   117
       ((fixes1, map (apsnd (map abs_fixes1)) assumes1),
wenzelm@18608
   118
        ((fixes2, map (apsnd (map abs_fixes)) assumes2), binds))
wenzelm@18608
   119
      end;
wenzelm@18608
   120
wenzelm@18608
   121
    val cases = map extract props;
wenzelm@18608
   122
wenzelm@18608
   123
    fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
wenzelm@18608
   124
      Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []};
wenzelm@18608
   125
    fun inner_case (_, ((fixes2, assumes2), binds)) =
wenzelm@18608
   126
      Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []};
wenzelm@18608
   127
    fun nested_case ((fixes1, assumes1), _) =
wenzelm@18608
   128
      Case {fixes = fixes1, assumes = assumes1, binds = [],
wenzelm@18608
   129
        cases = map string_of_int (1 upto len) ~~ map inner_case cases};
wenzelm@18608
   130
  in
wenzelm@18608
   131
    if len = 0 then NONE
wenzelm@18608
   132
    else if len = 1 then SOME (common_case (hd cases))
wenzelm@18608
   133
    else if is_none case_outline orelse length (gen_distinct (op =) (map fst cases)) > 1 then NONE
wenzelm@18608
   134
    else SOME (nested_case (hd cases))
wenzelm@18608
   135
  end;
wenzelm@18608
   136
wenzelm@18608
   137
fun make is_open rule_struct (thy, prop) cases =
wenzelm@18608
   138
  let
wenzelm@18608
   139
    val n = length cases;
wenzelm@18608
   140
    val nprems = Logic.count_prems (prop, 0);
wenzelm@18608
   141
    fun add_case (name, concls) (cs, i) =
wenzelm@18608
   142
      ((case try (fn () =>
wenzelm@18608
   143
          (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
wenzelm@18608
   144
        NONE => (name, NONE)
wenzelm@18608
   145
      | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
wenzelm@18608
   146
  in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end;
wenzelm@18608
   147
wenzelm@18608
   148
in
wenzelm@18608
   149
wenzelm@18608
   150
fun make_common is_open = make is_open NONE;
wenzelm@18608
   151
fun make_nested is_open rule_struct = make is_open (SOME rule_struct);
wenzelm@18608
   152
fun make_simple is_open (thy, prop) name = [(name, extract_case is_open thy (NONE, prop) "" [])];
wenzelm@18608
   153
wenzelm@18608
   154
fun apply args =
wenzelm@18608
   155
  let
wenzelm@18608
   156
    fun appl (Case {fixes, assumes, binds, cases}) =
wenzelm@18608
   157
      let
wenzelm@18608
   158
        val assumes' = map (apsnd (map (app args))) assumes;
wenzelm@18608
   159
        val binds' = map (apsnd (Option.map (app args))) binds;
wenzelm@18608
   160
        val cases' = map (apsnd appl) cases;
wenzelm@18608
   161
      in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end;
wenzelm@18608
   162
  in appl end;
wenzelm@18608
   163
wenzelm@18608
   164
end;
wenzelm@18608
   165
wenzelm@18608
   166
wenzelm@18608
   167
wenzelm@18229
   168
(** tactics with cases **)
wenzelm@18229
   169
wenzelm@18229
   170
type cases_tactic = thm -> (cases * thm) Seq.seq;
wenzelm@18229
   171
wenzelm@18229
   172
fun CASES cases tac st = Seq.map (pair cases) (tac st);
wenzelm@18229
   173
fun NO_CASES tac = CASES [] tac;
wenzelm@18229
   174
wenzelm@18229
   175
fun SUBGOAL_CASES tac i st =
wenzelm@18229
   176
  (case try Logic.nth_prem (i, Thm.prop_of st) of
wenzelm@18229
   177
    SOME goal => tac (goal, i) st
wenzelm@18229
   178
  | NONE => Seq.empty);
wenzelm@18229
   179
wenzelm@18229
   180
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
wenzelm@18229
   181
  st |> tac1 i |> Seq.maps (fn (cases, st') =>
wenzelm@18237
   182
    CASES cases (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st)) st');
wenzelm@18229
   183
wenzelm@18229
   184
wenzelm@18229
   185
wenzelm@18229
   186
(** consume facts **)
wenzelm@18229
   187
wenzelm@18477
   188
local
wenzelm@18477
   189
wenzelm@18477
   190
fun unfold_prems n defs th =
wenzelm@18477
   191
  if null defs then th
wenzelm@18477
   192
  else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs)) th;
wenzelm@18477
   193
wenzelm@18477
   194
fun unfold_prems_concls defs th =
wenzelm@18477
   195
  if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
wenzelm@18477
   196
  else
wenzelm@18477
   197
    Drule.fconv_rule
wenzelm@18477
   198
      (Drule.concl_conv ~1 (Drule.conjunction_conv ~1
wenzelm@18477
   199
        (K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
wenzelm@18477
   200
wenzelm@18477
   201
in
wenzelm@18477
   202
wenzelm@18477
   203
fun consume defs facts ((xx, n), th) =
wenzelm@18237
   204
  let val m = Int.min (length facts, n) in
wenzelm@18477
   205
    th
wenzelm@18477
   206
    |> unfold_prems n defs
wenzelm@18477
   207
    |> unfold_prems_concls defs
wenzelm@18237
   208
    |> Drule.multi_resolve (Library.take (m, facts))
wenzelm@18477
   209
    |> Seq.map (pair (xx, (n - m, Library.drop (m, facts))))
wenzelm@18237
   210
  end;
wenzelm@10811
   211
wenzelm@18477
   212
end;
wenzelm@18477
   213
wenzelm@10811
   214
val consumes_tagN = "consumes";
wenzelm@10811
   215
wenzelm@18229
   216
fun lookup_consumes th =
wenzelm@18229
   217
  let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in
wenzelm@18229
   218
    (case AList.lookup (op =) (Thm.tags_of_thm th) (consumes_tagN) of
skalberg@15531
   219
      NONE => NONE
skalberg@15531
   220
    | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ())
wenzelm@10530
   221
    | _ => err ())
wenzelm@10530
   222
  end;
wenzelm@10530
   223
wenzelm@18477
   224
fun get_consumes th = the_default 0 (lookup_consumes th);
wenzelm@18477
   225
skalberg@15531
   226
fun put_consumes NONE th = th
skalberg@15531
   227
  | put_consumes (SOME n) th = th
wenzelm@12761
   228
      |> Drule.untag_rule consumes_tagN
wenzelm@12761
   229
      |> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
wenzelm@10530
   230
wenzelm@18477
   231
fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
wenzelm@18477
   232
wenzelm@12761
   233
val save_consumes = put_consumes o lookup_consumes;
wenzelm@12761
   234
skalberg@15531
   235
fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x;
wenzelm@16148
   236
fun consumes_default n x =
wenzelm@16148
   237
  if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
wenzelm@8364
   238
wenzelm@8364
   239
wenzelm@18229
   240
wenzelm@18229
   241
(** case names **)
wenzelm@18229
   242
wenzelm@18237
   243
val case_names_tagN = "case_names";
wenzelm@8364
   244
wenzelm@18229
   245
fun add_case_names NONE = I
wenzelm@18229
   246
  | add_case_names (SOME names) =
wenzelm@18237
   247
      Drule.untag_rule case_names_tagN
wenzelm@18237
   248
      #> Drule.tag_rule (case_names_tagN, names);
wenzelm@8364
   249
wenzelm@18237
   250
fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) case_names_tagN;
wenzelm@10530
   251
wenzelm@18229
   252
val save_case_names = add_case_names o lookup_case_names;
wenzelm@18229
   253
val name = add_case_names o SOME;
wenzelm@8427
   254
fun case_names ss = Drule.rule_attribute (K (name ss));
wenzelm@8364
   255
wenzelm@10530
   256
wenzelm@18229
   257
wenzelm@18229
   258
(** case conclusions **)
wenzelm@18229
   259
wenzelm@18229
   260
val case_concl_tagN = "case_conclusion";
wenzelm@18229
   261
wenzelm@18229
   262
fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name)
wenzelm@18229
   263
  | is_case_concl _ _ = false;
wenzelm@18229
   264
wenzelm@18229
   265
fun add_case_concl (name, cs) = Drule.map_tags (fn tags =>
wenzelm@18229
   266
  filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]);
wenzelm@18229
   267
wenzelm@18229
   268
fun get_case_concls th name =
wenzelm@18237
   269
  (case find_first (is_case_concl name) (Thm.tags_of_thm th) of
wenzelm@18237
   270
    SOME (_, _ :: cs) => cs
wenzelm@18237
   271
  | _ => []);
wenzelm@18229
   272
wenzelm@18229
   273
fun save_case_concls th =
wenzelm@18229
   274
  let val concls = Thm.tags_of_thm th |> List.mapPartial
wenzelm@18237
   275
    (fn (a, b :: cs) =>
wenzelm@18237
   276
      if a = case_concl_tagN then SOME (b, cs) else NONE
wenzelm@18229
   277
    | _ => NONE)
wenzelm@18229
   278
  in fold add_case_concl concls end;
wenzelm@18229
   279
wenzelm@18237
   280
fun case_conclusion concl = Drule.rule_attribute (fn _ => add_case_concl concl);
wenzelm@18229
   281
wenzelm@18229
   282
wenzelm@18229
   283
wenzelm@18229
   284
(** case declarations **)
wenzelm@18229
   285
wenzelm@10530
   286
(* access hints *)
wenzelm@10530
   287
wenzelm@18229
   288
fun save th = save_consumes th #> save_case_names th #> save_case_concls th;
wenzelm@12761
   289
wenzelm@18229
   290
fun get th =
wenzelm@12761
   291
  let
wenzelm@18477
   292
    val n = get_consumes th;
wenzelm@18229
   293
    val cases =
wenzelm@18229
   294
      (case lookup_case_names th of
wenzelm@18229
   295
        NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
wenzelm@18229
   296
      | SOME names => map (fn name => (name, get_case_concls th name)) names);
wenzelm@18229
   297
  in (cases, n) end;
wenzelm@10530
   298
wenzelm@8364
   299
wenzelm@8427
   300
(* params *)
wenzelm@8364
   301
wenzelm@18229
   302
fun rename_params xss th =
wenzelm@18229
   303
  th
wenzelm@18229
   304
  |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
wenzelm@18229
   305
  |> save th;
wenzelm@8364
   306
wenzelm@8364
   307
fun params xss = Drule.rule_attribute (K (rename_params xss));
wenzelm@8364
   308
wenzelm@18477
   309
wenzelm@18477
   310
wenzelm@18477
   311
(** mutual_rule **)
wenzelm@18477
   312
wenzelm@18477
   313
local
wenzelm@18477
   314
wenzelm@18477
   315
fun equal_cterms ts us =
wenzelm@18477
   316
  list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us) = EQUAL;
wenzelm@18477
   317
wenzelm@18477
   318
fun prep_rule th =
wenzelm@18477
   319
  let
wenzelm@18477
   320
    val n = get_consumes th;
wenzelm@18477
   321
    val th' = Drule.freeze_all (Thm.permute_prems 0 n th);
wenzelm@18477
   322
    val prems = Library.take (Thm.nprems_of th' - n, Drule.cprems_of th');
wenzelm@18477
   323
    val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
wenzelm@18477
   324
  in (prems, (n, th'')) end;
wenzelm@18477
   325
wenzelm@18477
   326
in
wenzelm@18477
   327
wenzelm@18477
   328
fun mutual_rule [] = NONE
wenzelm@18477
   329
  | mutual_rule [th] = SOME ([0], th)
wenzelm@18477
   330
  | mutual_rule raw_rules =
wenzelm@18477
   331
      let
wenzelm@18477
   332
        val rules as (prems, _) :: _ = map prep_rule raw_rules;
wenzelm@18477
   333
        val (ns, ths) = split_list (map #2 rules);
wenzelm@18477
   334
      in
wenzelm@18477
   335
        if not (forall (equal_cterms prems o #1) rules) then NONE
wenzelm@18477
   336
        else
wenzelm@18477
   337
          SOME (ns,
wenzelm@18477
   338
            ths
wenzelm@18477
   339
            |> foldr1 (uncurry Drule.conj_intr)
wenzelm@18477
   340
            |> Drule.implies_intr_list prems
wenzelm@18477
   341
            |> Drule.standard'
wenzelm@18477
   342
            |> save (hd raw_rules)
wenzelm@18477
   343
            |> put_consumes (SOME 0))
wenzelm@18477
   344
      end;
wenzelm@18477
   345
wenzelm@18477
   346
end;
wenzelm@18477
   347
wenzelm@18581
   348
fun strict_mutual_rule ths =
wenzelm@18581
   349
  (case mutual_rule ths of
wenzelm@18581
   350
    NONE => error "Failed to join given rules into one mutual rule"
wenzelm@18581
   351
  | SOME res => res);
wenzelm@18581
   352
wenzelm@8364
   353
end;
wenzelm@17113
   354
wenzelm@18229
   355
structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;
wenzelm@18229
   356
open BasicRuleCases;