src/Pure/Isar/rule_cases.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 36354 bbd742107f56
permissions -rw-r--r--
modernized structure Object_Logic;
wenzelm@8364
     1
(*  Title:      Pure/Isar/rule_cases.ML
wenzelm@8364
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8364
     3
wenzelm@18229
     4
Annotations and local contexts of rules.
wenzelm@8364
     5
*)
wenzelm@8364
     6
wenzelm@18188
     7
infix 1 THEN_ALL_NEW_CASES;
wenzelm@18188
     8
wenzelm@18229
     9
signature BASIC_RULE_CASES =
wenzelm@18229
    10
sig
wenzelm@18229
    11
  type cases
wenzelm@18229
    12
  type cases_tactic
wenzelm@18229
    13
  val CASES: cases -> tactic -> cases_tactic
wenzelm@18229
    14
  val NO_CASES: tactic -> cases_tactic
wenzelm@18229
    15
  val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic
wenzelm@18229
    16
  val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
wenzelm@18229
    17
end
wenzelm@18229
    18
wenzelm@8364
    19
signature RULE_CASES =
wenzelm@8364
    20
sig
wenzelm@18229
    21
  include BASIC_RULE_CASES
wenzelm@18608
    22
  datatype T = Case of
wenzelm@18608
    23
   {fixes: (string * typ) list,
wenzelm@18608
    24
    assumes: (string * term list) list,
wenzelm@18608
    25
    binds: (indexname * term option) list,
wenzelm@18608
    26
    cases: (string * T) list}
wenzelm@18608
    27
  val strip_params: term -> (string * typ) list
berghofe@34916
    28
  val make_common: theory * term -> (string * string list) list -> cases
berghofe@34916
    29
  val make_nested: term -> theory * term -> (string * string list) list -> cases
wenzelm@18608
    30
  val apply: term list -> T -> T
wenzelm@18237
    31
  val consume: thm list -> thm list -> ('a * int) * thm ->
wenzelm@18237
    32
    (('a * (int * thm list)) * thm) Seq.seq
wenzelm@18477
    33
  val add_consumes: int -> thm -> thm
wenzelm@24862
    34
  val get_consumes: thm -> int
wenzelm@18728
    35
  val consumes: int -> attribute
wenzelm@18728
    36
  val consumes_default: int -> attribute
berghofe@34986
    37
  val get_constraints: thm -> int
berghofe@34986
    38
  val constraints: int -> attribute
wenzelm@8364
    39
  val name: string list -> thm -> thm
wenzelm@18728
    40
  val case_names: string list -> attribute
wenzelm@18728
    41
  val case_conclusion: string * string list -> attribute
wenzelm@33303
    42
  val is_inner_rule: thm -> bool
wenzelm@33303
    43
  val inner_rule: attribute
wenzelm@12761
    44
  val save: thm -> thm -> thm
wenzelm@18237
    45
  val get: thm -> (string * string list) list * int
wenzelm@8427
    46
  val rename_params: string list list -> thm -> thm
wenzelm@18728
    47
  val params: string list list -> attribute
berghofe@34916
    48
  val internalize_params: thm -> thm
wenzelm@20289
    49
  val mutual_rule: Proof.context -> thm list -> (int list * thm) option
wenzelm@20289
    50
  val strict_mutual_rule: Proof.context -> thm list -> int list * thm
wenzelm@8364
    51
end;
wenzelm@8364
    52
wenzelm@33368
    53
structure Rule_Cases: RULE_CASES =
wenzelm@8364
    54
struct
wenzelm@8364
    55
wenzelm@18608
    56
(** cases **)
wenzelm@18608
    57
wenzelm@18608
    58
datatype T = Case of
wenzelm@18608
    59
 {fixes: (string * typ) list,
wenzelm@18608
    60
  assumes: (string * term list) list,
wenzelm@18608
    61
  binds: (indexname * term option) list,
wenzelm@18608
    62
  cases: (string * T) list};
wenzelm@18608
    63
wenzelm@18608
    64
type cases = (string * T option) list;
wenzelm@18608
    65
wenzelm@18608
    66
val case_conclN = "case";
wenzelm@18608
    67
val case_hypsN = "hyps";
wenzelm@18608
    68
val case_premsN = "prems";
wenzelm@18608
    69
wenzelm@20087
    70
val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
wenzelm@18608
    71
wenzelm@18608
    72
local
wenzelm@18608
    73
wenzelm@18608
    74
fun abs xs t = Term.list_abs (xs, t);
wenzelm@18608
    75
fun app us t = Term.betapplys (t, us);
wenzelm@18608
    76
wenzelm@18608
    77
fun dest_binops cs tm =
wenzelm@18608
    78
  let
wenzelm@18608
    79
    val n = length cs;
wenzelm@18608
    80
    fun dest 0 _ = []
wenzelm@18608
    81
      | dest 1 t = [t]
wenzelm@18608
    82
      | dest k (_ $ t $ u) = t :: dest (k - 1) u
wenzelm@18608
    83
      | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
wenzelm@18608
    84
  in cs ~~ dest n tm end;
wenzelm@18608
    85
wenzelm@18608
    86
fun extract_fixes NONE prop = (strip_params prop, [])
wenzelm@18608
    87
  | extract_fixes (SOME outline) prop =
wenzelm@19012
    88
      chop (length (Logic.strip_params outline)) (strip_params prop);
wenzelm@18608
    89
wenzelm@18608
    90
fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
wenzelm@18608
    91
  | extract_assumes qual (SOME outline) prop =
wenzelm@18608
    92
      let val (hyps, prems) =
wenzelm@19012
    93
        chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
wenzelm@18608
    94
      in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
wenzelm@18608
    95
berghofe@34916
    96
fun extract_case thy (case_outline, raw_prop) name concls =
wenzelm@18608
    97
  let
wenzelm@18608
    98
    val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
wenzelm@18608
    99
    val len = length props;
wenzelm@18608
   100
    val nested = is_some case_outline andalso len > 1;
wenzelm@18608
   101
wenzelm@18608
   102
    fun extract prop =
wenzelm@18608
   103
      let
berghofe@34916
   104
        val (fixes1, fixes2) = extract_fixes case_outline prop;
wenzelm@18608
   105
        val abs_fixes = abs (fixes1 @ fixes2);
wenzelm@18608
   106
        fun abs_fixes1 t =
wenzelm@18608
   107
          if not nested then abs_fixes t
wenzelm@18608
   108
          else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
wenzelm@18608
   109
wenzelm@30364
   110
        val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
wenzelm@19482
   111
          |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
wenzelm@18608
   112
wenzelm@35625
   113
        val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
wenzelm@18608
   114
        val binds =
wenzelm@18608
   115
          (case_conclN, concl) :: dest_binops concls concl
wenzelm@18608
   116
          |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
wenzelm@18608
   117
      in
wenzelm@18608
   118
       ((fixes1, map (apsnd (map abs_fixes1)) assumes1),
wenzelm@18608
   119
        ((fixes2, map (apsnd (map abs_fixes)) assumes2), binds))
wenzelm@18608
   120
      end;
wenzelm@18608
   121
wenzelm@18608
   122
    val cases = map extract props;
wenzelm@18608
   123
wenzelm@18608
   124
    fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
wenzelm@18608
   125
      Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []};
wenzelm@18608
   126
    fun inner_case (_, ((fixes2, assumes2), binds)) =
wenzelm@18608
   127
      Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []};
wenzelm@18608
   128
    fun nested_case ((fixes1, assumes1), _) =
wenzelm@18608
   129
      Case {fixes = fixes1, assumes = assumes1, binds = [],
wenzelm@18608
   130
        cases = map string_of_int (1 upto len) ~~ map inner_case cases};
wenzelm@18608
   131
  in
wenzelm@18608
   132
    if len = 0 then NONE
wenzelm@18608
   133
    else if len = 1 then SOME (common_case (hd cases))
wenzelm@19046
   134
    else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE
wenzelm@18608
   135
    else SOME (nested_case (hd cases))
wenzelm@18608
   136
  end;
wenzelm@18608
   137
berghofe@34916
   138
fun make rule_struct (thy, prop) cases =
wenzelm@18608
   139
  let
wenzelm@18608
   140
    val n = length cases;
wenzelm@21576
   141
    val nprems = Logic.count_prems prop;
wenzelm@18608
   142
    fun add_case (name, concls) (cs, i) =
wenzelm@18608
   143
      ((case try (fn () =>
wenzelm@18608
   144
          (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
wenzelm@18608
   145
        NONE => (name, NONE)
berghofe@34916
   146
      | SOME p => (name, extract_case thy p name concls)) :: cs, i - 1);
haftmann@34058
   147
  in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
wenzelm@18608
   148
wenzelm@18608
   149
in
wenzelm@18608
   150
berghofe@34916
   151
val make_common = make NONE;
berghofe@34916
   152
fun make_nested rule_struct = make (SOME rule_struct);
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@23584
   192
  else Conv.fconv_rule (Conv.prems_conv n (MetaSimplifier.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@22900
   197
    Conv.fconv_rule
wenzelm@23418
   198
      (Conv.concl_conv ~1 (Conjunction.convs
wenzelm@23584
   199
        (Conv.prems_conv ~1 (MetaSimplifier.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
haftmann@33957
   208
    |> Drule.multi_resolve (take m facts)
haftmann@33957
   209
    |> Seq.map (pair (xx, (n - m, 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@33303
   217
  (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
wenzelm@23657
   218
    NONE => NONE
wenzelm@23657
   219
  | SOME s =>
wenzelm@24244
   220
      (case Lexicon.read_nat s of SOME n => SOME n
wenzelm@23657
   221
      | _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th])));
wenzelm@10530
   222
wenzelm@18477
   223
fun get_consumes th = the_default 0 (lookup_consumes th);
wenzelm@18477
   224
skalberg@15531
   225
fun put_consumes NONE th = th
skalberg@15531
   226
  | put_consumes (SOME n) th = th
wenzelm@27865
   227
      |> Thm.untag_rule consumes_tagN
wenzelm@33303
   228
      |> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n));
wenzelm@10530
   229
wenzelm@18477
   230
fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
wenzelm@18477
   231
wenzelm@12761
   232
val save_consumes = put_consumes o lookup_consumes;
wenzelm@12761
   233
wenzelm@33303
   234
fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
wenzelm@21395
   235
wenzelm@16148
   236
fun consumes_default n x =
wenzelm@21395
   237
  if is_some (lookup_consumes (#2 x)) then x else consumes n x;
wenzelm@8364
   238
wenzelm@8364
   239
wenzelm@18229
   240
berghofe@34986
   241
(** equality constraints **)
berghofe@34986
   242
berghofe@34986
   243
val constraints_tagN = "constraints";
berghofe@34986
   244
berghofe@34986
   245
fun lookup_constraints th =
berghofe@34986
   246
  (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
berghofe@34986
   247
    NONE => NONE
berghofe@34986
   248
  | SOME s =>
berghofe@34986
   249
      (case Lexicon.read_nat s of SOME n => SOME n
berghofe@34986
   250
      | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
berghofe@34986
   251
berghofe@34986
   252
fun get_constraints th = the_default 0 (lookup_constraints th);
berghofe@34986
   253
berghofe@34986
   254
fun put_constraints NONE th = th
berghofe@34986
   255
  | put_constraints (SOME n) th = th
berghofe@34986
   256
      |> Thm.untag_rule constraints_tagN
berghofe@34986
   257
      |> Thm.tag_rule (constraints_tagN, string_of_int (if n < 0 then 0 else n));
berghofe@34986
   258
berghofe@34986
   259
val save_constraints = put_constraints o lookup_constraints;
berghofe@34986
   260
berghofe@34986
   261
fun constraints n = Thm.rule_attribute (K (put_constraints (SOME n)));
berghofe@34986
   262
berghofe@34986
   263
berghofe@34986
   264
wenzelm@18229
   265
(** case names **)
wenzelm@18229
   266
wenzelm@23657
   267
val implode_args = space_implode ";";
wenzelm@23657
   268
val explode_args = space_explode ";";
wenzelm@23657
   269
wenzelm@18237
   270
val case_names_tagN = "case_names";
wenzelm@8364
   271
wenzelm@18229
   272
fun add_case_names NONE = I
wenzelm@18229
   273
  | add_case_names (SOME names) =
wenzelm@27865
   274
      Thm.untag_rule case_names_tagN
wenzelm@27865
   275
      #> Thm.tag_rule (case_names_tagN, implode_args names);
wenzelm@8364
   276
wenzelm@23657
   277
fun lookup_case_names th =
wenzelm@23657
   278
  AList.lookup (op =) (Thm.get_tags th) case_names_tagN
wenzelm@23657
   279
  |> Option.map explode_args;
wenzelm@10530
   280
wenzelm@18229
   281
val save_case_names = add_case_names o lookup_case_names;
wenzelm@18229
   282
val name = add_case_names o SOME;
wenzelm@18728
   283
fun case_names ss = Thm.rule_attribute (K (name ss));
wenzelm@8364
   284
wenzelm@10530
   285
wenzelm@18229
   286
wenzelm@18229
   287
(** case conclusions **)
wenzelm@18229
   288
wenzelm@18229
   289
val case_concl_tagN = "case_conclusion";
wenzelm@18229
   290
wenzelm@23657
   291
fun get_case_concl name (a, b) =
wenzelm@23657
   292
  if a = case_concl_tagN then
wenzelm@23657
   293
    (case explode_args b of c :: cs => if c = name then SOME cs else NONE)
wenzelm@23657
   294
  else NONE;
wenzelm@18229
   295
wenzelm@21646
   296
fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>
wenzelm@23657
   297
  filter_out (is_some o get_case_concl name) tags @
wenzelm@23657
   298
    [(case_concl_tagN, implode_args (name :: cs))]);
wenzelm@18229
   299
wenzelm@18229
   300
fun get_case_concls th name =
wenzelm@23657
   301
  these (get_first (get_case_concl name) (Thm.get_tags th));
wenzelm@18229
   302
wenzelm@18229
   303
fun save_case_concls th =
wenzelm@21646
   304
  let val concls = Thm.get_tags th |> map_filter
wenzelm@23657
   305
    (fn (a, b) =>
wenzelm@23657
   306
      if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
wenzelm@23657
   307
      else NONE)
wenzelm@18229
   308
  in fold add_case_concl concls end;
wenzelm@18229
   309
wenzelm@33303
   310
fun case_conclusion concl = Thm.rule_attribute (K (add_case_concl concl));
wenzelm@33303
   311
wenzelm@33303
   312
wenzelm@33303
   313
wenzelm@33303
   314
(** inner rule **)
wenzelm@33303
   315
wenzelm@33303
   316
val inner_rule_tagN = "inner_rule";
wenzelm@33303
   317
wenzelm@33303
   318
fun is_inner_rule th =
wenzelm@33303
   319
  AList.defined (op =) (Thm.get_tags th) inner_rule_tagN;
wenzelm@33303
   320
wenzelm@33303
   321
fun put_inner_rule inner =
wenzelm@33303
   322
  Thm.untag_rule inner_rule_tagN
wenzelm@33303
   323
  #> inner ? Thm.tag_rule (inner_rule_tagN, "");
wenzelm@33303
   324
wenzelm@33303
   325
val save_inner_rule = put_inner_rule o is_inner_rule;
wenzelm@33303
   326
wenzelm@33303
   327
val inner_rule = Thm.rule_attribute (K (put_inner_rule true));
wenzelm@18229
   328
wenzelm@18229
   329
wenzelm@18229
   330
wenzelm@18229
   331
(** case declarations **)
wenzelm@18229
   332
wenzelm@10530
   333
(* access hints *)
wenzelm@10530
   334
wenzelm@33303
   335
fun save th =
wenzelm@33303
   336
  save_consumes th #>
berghofe@34986
   337
  save_constraints th #>
wenzelm@33303
   338
  save_case_names th #>
wenzelm@33303
   339
  save_case_concls th #>
wenzelm@33303
   340
  save_inner_rule th;
wenzelm@12761
   341
wenzelm@18229
   342
fun get th =
wenzelm@12761
   343
  let
wenzelm@18477
   344
    val n = get_consumes th;
wenzelm@18229
   345
    val cases =
wenzelm@18229
   346
      (case lookup_case_names th of
wenzelm@18229
   347
        NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
wenzelm@18229
   348
      | SOME names => map (fn name => (name, get_case_concls th name)) names);
wenzelm@18229
   349
  in (cases, n) end;
wenzelm@10530
   350
wenzelm@8364
   351
wenzelm@8427
   352
(* params *)
wenzelm@8364
   353
wenzelm@18229
   354
fun rename_params xss th =
wenzelm@18229
   355
  th
wenzelm@18229
   356
  |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
wenzelm@18229
   357
  |> save th;
wenzelm@8364
   358
wenzelm@18728
   359
fun params xss = Thm.rule_attribute (K (rename_params xss));
wenzelm@8364
   360
wenzelm@18477
   361
berghofe@34916
   362
(* internalize parameter names *)
berghofe@34916
   363
berghofe@34916
   364
fun internalize_params rule =
berghofe@34916
   365
  let
berghofe@34916
   366
    fun rename prem =
berghofe@34916
   367
      let val xs =
berghofe@34916
   368
        map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
berghofe@34916
   369
      in Logic.list_rename_params (xs, prem) end;
berghofe@34916
   370
    fun rename_prems prop =
berghofe@34916
   371
      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
berghofe@34916
   372
      in Logic.list_implies (map rename As, C) end;
berghofe@34916
   373
  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
berghofe@34916
   374
berghofe@34916
   375
wenzelm@18477
   376
wenzelm@18477
   377
(** mutual_rule **)
wenzelm@18477
   378
wenzelm@18477
   379
local
wenzelm@18477
   380
wenzelm@18477
   381
fun equal_cterms ts us =
wenzelm@35408
   382
  is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us));
wenzelm@18477
   383
wenzelm@19917
   384
fun prep_rule n th =
wenzelm@18477
   385
  let
wenzelm@19917
   386
    val th' = Thm.permute_prems 0 n th;
haftmann@33957
   387
    val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th');
wenzelm@18477
   388
    val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
wenzelm@18477
   389
  in (prems, (n, th'')) end;
wenzelm@18477
   390
wenzelm@18477
   391
in
wenzelm@18477
   392
wenzelm@19917
   393
fun mutual_rule _ [] = NONE
wenzelm@19917
   394
  | mutual_rule _ [th] = SOME ([0], th)
wenzelm@19917
   395
  | mutual_rule ctxt (ths as th :: _) =
wenzelm@18477
   396
      let
wenzelm@31794
   397
        val ((_, ths'), ctxt') = Variable.import true ths ctxt;
wenzelm@19917
   398
        val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
wenzelm@19917
   399
        val (ns, rls) = split_list (map #2 rules);
wenzelm@18477
   400
      in
wenzelm@18477
   401
        if not (forall (equal_cterms prems o #1) rules) then NONE
wenzelm@18477
   402
        else
wenzelm@18477
   403
          SOME (ns,
wenzelm@19917
   404
            rls
wenzelm@23418
   405
            |> Conjunction.intr_balanced
wenzelm@18477
   406
            |> Drule.implies_intr_list prems
wenzelm@19917
   407
            |> singleton (Variable.export ctxt' ctxt)
wenzelm@19917
   408
            |> save th
wenzelm@18477
   409
            |> put_consumes (SOME 0))
wenzelm@18477
   410
      end;
wenzelm@18477
   411
wenzelm@18477
   412
end;
wenzelm@18477
   413
wenzelm@19917
   414
fun strict_mutual_rule ctxt ths =
wenzelm@19917
   415
  (case mutual_rule ctxt ths of
wenzelm@18581
   416
    NONE => error "Failed to join given rules into one mutual rule"
wenzelm@18581
   417
  | SOME res => res);
wenzelm@18581
   418
wenzelm@8364
   419
end;
wenzelm@17113
   420
wenzelm@33368
   421
structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
wenzelm@33303
   422
open Basic_Rule_Cases;