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