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