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