src/Provers/induct_method.ML
author nipkow
Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago)
changeset 13157 4a4599f78f18
parent 13105 3d1e7a199bdc
child 13197 0567f4fd1415
permissions -rw-r--r--
allowed more general split rules to cope with div/mod 2
wenzelm@11670
     1
(*  Title:      Provers/induct_method.ML
wenzelm@11670
     2
    ID:         $Id$
wenzelm@11670
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@11670
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@11670
     5
wenzelm@11735
     6
Proof by cases and induction on sets and types.
wenzelm@11670
     7
*)
wenzelm@11670
     8
wenzelm@11670
     9
signature INDUCT_METHOD_DATA =
wenzelm@11670
    10
sig
wenzelm@11670
    11
  val dest_concls: term -> term list
wenzelm@11670
    12
  val cases_default: thm
wenzelm@11996
    13
  val local_impI: thm
wenzelm@11670
    14
  val conjI: thm
wenzelm@11670
    15
  val atomize: thm list
wenzelm@11670
    16
  val rulify1: thm list
wenzelm@11670
    17
  val rulify2: thm list
wenzelm@12240
    18
  val localize: thm list
wenzelm@11670
    19
end;
wenzelm@11670
    20
wenzelm@11670
    21
signature INDUCT_METHOD =
wenzelm@11670
    22
sig
wenzelm@11670
    23
  val setup: (theory -> theory) list
wenzelm@11670
    24
end;
wenzelm@11670
    25
wenzelm@11670
    26
functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
wenzelm@11670
    27
struct
wenzelm@11670
    28
wenzelm@11670
    29
wenzelm@11670
    30
(** misc utils **)
wenzelm@11670
    31
wenzelm@11670
    32
(* align lists *)
wenzelm@11670
    33
wenzelm@11670
    34
fun align_left msg xs ys =
wenzelm@11670
    35
  let val m = length xs and n = length ys
wenzelm@11735
    36
  in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end;
wenzelm@11670
    37
wenzelm@11670
    38
fun align_right msg xs ys =
wenzelm@11670
    39
  let val m = length xs and n = length ys
wenzelm@11735
    40
  in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
wenzelm@11670
    41
wenzelm@11670
    42
wenzelm@11735
    43
(* prep_inst *)
wenzelm@11670
    44
wenzelm@11735
    45
fun prep_inst align cert tune (tm, ts) =
wenzelm@11670
    46
  let
wenzelm@11670
    47
    fun prep_var (x, Some t) =
wenzelm@11670
    48
          let
wenzelm@11670
    49
            val cx = cert x;
wenzelm@11670
    50
            val {T = xT, sign, ...} = Thm.rep_cterm cx;
wenzelm@12799
    51
            val ct = cert (tune t);
wenzelm@11670
    52
          in
wenzelm@11670
    53
            if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct)
wenzelm@11735
    54
            else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
wenzelm@11735
    55
             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
wenzelm@11735
    56
              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
wenzelm@11735
    57
              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
wenzelm@11670
    58
          end
wenzelm@11670
    59
      | prep_var (_, None) = None;
wenzelm@11735
    60
    val xs = InductAttrib.vars_of tm;
wenzelm@11670
    61
  in
wenzelm@11735
    62
    align "Rule has fewer variables than instantiations given" xs ts
wenzelm@11670
    63
    |> mapfilter prep_var
wenzelm@11670
    64
  end;
wenzelm@11670
    65
wenzelm@11670
    66
wenzelm@11670
    67
wenzelm@11670
    68
(** cases method **)
wenzelm@11670
    69
wenzelm@11670
    70
(*
wenzelm@11735
    71
  rule selection scheme:
wenzelm@11735
    72
          cases         - classical case split
wenzelm@11735
    73
    <x:A> cases ...     - set cases
wenzelm@11735
    74
          cases t       - type cases
wenzelm@11735
    75
    ...   cases ... R   - explicit rule
wenzelm@11670
    76
*)
wenzelm@11670
    77
wenzelm@11670
    78
local
wenzelm@11670
    79
wenzelm@11790
    80
fun resolveq_cases_tac make ruleq i st =
wenzelm@11790
    81
  ruleq |> Seq.map (fn (rule, (cases, facts)) =>
wenzelm@11790
    82
    (Method.insert_tac facts THEN' Tactic.rtac rule) i st
wenzelm@12799
    83
    |> Seq.map (rpair (make (Thm.sign_of_thm rule, Thm.prop_of rule) cases)))
wenzelm@11790
    84
  |> Seq.flat;
wenzelm@11790
    85
wenzelm@11735
    86
fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
wenzelm@11735
    87
  | find_casesT _ _ = [];
wenzelm@11735
    88
wenzelm@11735
    89
fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt fact
wenzelm@11735
    90
  | find_casesS _ _ = [];
wenzelm@11735
    91
wenzelm@11735
    92
fun cases_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
wenzelm@11670
    93
  let
wenzelm@11670
    94
    val sg = ProofContext.sign_of ctxt;
wenzelm@11670
    95
    val cert = Thm.cterm_of sg;
wenzelm@11670
    96
wenzelm@11735
    97
    fun inst_rule r =
wenzelm@11735
    98
      if null insts then RuleCases.add r
wenzelm@11735
    99
      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
wenzelm@11670
   100
        |> (flat o map (prep_inst align_left cert I))
wenzelm@11735
   101
        |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
wenzelm@11670
   102
wenzelm@11735
   103
    val ruleq =
wenzelm@12852
   104
      (case opt_rule of
wenzelm@12852
   105
        None =>
wenzelm@12852
   106
          let val rules = find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default] in
wenzelm@12053
   107
            Method.trace ctxt rules;
wenzelm@11735
   108
            Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
wenzelm@11670
   109
          end
wenzelm@12852
   110
      | Some r => Seq.single (inst_rule r));
wenzelm@11670
   111
wenzelm@11735
   112
    fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
wenzelm@11735
   113
      (Method.multi_resolves (take (n, facts)) [th]);
wenzelm@11790
   114
  in resolveq_cases_tac (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq)) end;
wenzelm@11670
   115
wenzelm@11670
   116
in
wenzelm@11670
   117
wenzelm@12852
   118
val cases_meth = Method.METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo cases_tac);
wenzelm@11670
   119
wenzelm@11670
   120
end;
wenzelm@11670
   121
wenzelm@11670
   122
wenzelm@11670
   123
wenzelm@11670
   124
(** induct method **)
wenzelm@11670
   125
wenzelm@11670
   126
(*
wenzelm@11735
   127
  rule selection scheme:
wenzelm@11735
   128
    <x:A> induct ...     - set induction
wenzelm@11735
   129
          induct x       - type induction
wenzelm@11735
   130
    ...   induct ... R   - explicit rule
wenzelm@11670
   131
*)
wenzelm@11670
   132
wenzelm@11670
   133
local
wenzelm@11670
   134
wenzelm@11790
   135
wenzelm@11790
   136
(* atomize and rulify *)
wenzelm@11790
   137
wenzelm@12799
   138
fun atomize_term sg =
wenzelm@12799
   139
  ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize;
wenzelm@12799
   140
wenzelm@12799
   141
fun rulified_term thm =
wenzelm@12799
   142
  let val sg = Thm.sign_of_thm thm in
wenzelm@12799
   143
    Thm.prop_of thm
wenzelm@12799
   144
    |> MetaSimplifier.rewrite_term sg Data.rulify1
wenzelm@12799
   145
    |> MetaSimplifier.rewrite_term sg Data.rulify2
wenzelm@12799
   146
    |> pair sg
wenzelm@12799
   147
  end;
wenzelm@11756
   148
wenzelm@11670
   149
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
wenzelm@11670
   150
wenzelm@11670
   151
val rulify_tac =
wenzelm@11670
   152
  Tactic.rewrite_goal_tac Data.rulify1 THEN'
wenzelm@11670
   153
  Tactic.rewrite_goal_tac Data.rulify2 THEN'
wenzelm@11670
   154
  Tactic.norm_hhf_tac;
wenzelm@11670
   155
wenzelm@12799
   156
val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize;
wenzelm@12162
   157
wenzelm@11670
   158
wenzelm@11996
   159
(* imp_intr --- limited to atomic prems *)
wenzelm@11996
   160
wenzelm@11996
   161
fun imp_intr i raw_th =
wenzelm@11996
   162
  let
wenzelm@11996
   163
    val th = Thm.permute_prems (i - 1) 1 raw_th;
wenzelm@11996
   164
    val cprems = Drule.cprems_of th;
wenzelm@11996
   165
    val As = take (length cprems - 1, cprems);
wenzelm@11996
   166
    val C = Thm.cterm_of (Thm.sign_of_thm th) (Var (("C", #maxidx (Thm.rep_thm th) + 1), propT));
wenzelm@11996
   167
    val dummy_st = Drule.mk_triv_goal (Drule.list_implies (As, C));
wenzelm@11996
   168
  in th COMP Thm.lift_rule (dummy_st, 1) Data.local_impI end;
wenzelm@11996
   169
wenzelm@11996
   170
wenzelm@11790
   171
(* join multi-rules *)
wenzelm@11790
   172
wenzelm@11735
   173
val eq_prems = curry (Term.aconvs o pairself Thm.prems_of);
wenzelm@11670
   174
wenzelm@11735
   175
fun join_rules [] = []
wenzelm@11735
   176
  | join_rules [th] = [th]
wenzelm@11735
   177
  | join_rules (rules as r :: rs) =
wenzelm@11735
   178
      if not (forall (eq_prems r) rs) then []
wenzelm@11735
   179
      else
wenzelm@11735
   180
        let
wenzelm@11735
   181
          val th :: ths = map Drule.freeze_all rules;
wenzelm@11735
   182
          val cprems = Drule.cprems_of th;
wenzelm@11735
   183
          val asms = map Thm.assume cprems;
wenzelm@11735
   184
        in
wenzelm@11735
   185
          [foldr1 (fn (x, x') => [x, x'] MRS Data.conjI)
wenzelm@11735
   186
            (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
wenzelm@11735
   187
          |> Drule.implies_intr_list cprems
wenzelm@12305
   188
          |> Drule.standard'
wenzelm@12305
   189
          |> RuleCases.save th]
wenzelm@11735
   190
        end;
wenzelm@11670
   191
wenzelm@11790
   192
wenzelm@11790
   193
(* divinate rule instantiation (cannot handle pending goal parameters) *)
wenzelm@11790
   194
wenzelm@11808
   195
fun dest_env sign (env as Envir.Envir {asol, iTs, ...}) =
wenzelm@11790
   196
  let
wenzelm@11790
   197
    val pairs = Vartab.dest asol;
wenzelm@11808
   198
    val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2) pairs;
wenzelm@11790
   199
    val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
wenzelm@11790
   200
  in (map (apsnd (Thm.ctyp_of sign)) (Vartab.dest iTs), xs ~~ ts) end;
wenzelm@11790
   201
wenzelm@11790
   202
fun divinate_inst rule i st =
wenzelm@11790
   203
  let
wenzelm@11790
   204
    val {sign, maxidx, ...} = Thm.rep_thm st;
wenzelm@11790
   205
    val goal = List.nth (Thm.prems_of st, i - 1);  (*exception Subscript*)
wenzelm@11790
   206
    val params = rev (rename_wrt_term goal (Logic.strip_params goal));  (*as they are printed :-*)
wenzelm@11790
   207
  in
wenzelm@11790
   208
    if not (null params) then
wenzelm@11790
   209
      (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
wenzelm@11790
   210
        commas (map (Sign.string_of_term sign o Syntax.mark_boundT) params));
wenzelm@11790
   211
      Seq.single rule)
wenzelm@11790
   212
    else
wenzelm@11790
   213
      let
wenzelm@11790
   214
        val rule' = Thm.incr_indexes (maxidx + 1) rule;
wenzelm@11790
   215
        val concl = Logic.strip_assums_concl goal;
wenzelm@11790
   216
      in
wenzelm@11790
   217
        Unify.smash_unifiers (sign, Envir.empty (#maxidx (Thm.rep_thm rule')),
wenzelm@11790
   218
          [(Thm.concl_of rule', concl)])
wenzelm@12162
   219
        |> Seq.map (fn env => Drule.instantiate (dest_env sign env) rule')
wenzelm@11790
   220
      end
wenzelm@11790
   221
  end handle Subscript => Seq.empty;
wenzelm@11790
   222
wenzelm@11790
   223
wenzelm@11790
   224
(* compose tactics with cases *)
wenzelm@11790
   225
wenzelm@11996
   226
fun internalize k th = if k > 0 then internalize (k - 1) (imp_intr k th) else th;
wenzelm@11996
   227
wenzelm@11790
   228
fun resolveq_cases_tac' make ruleq i st =
wenzelm@11996
   229
  ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
wenzelm@11996
   230
    |> (Method.insert_tac more_facts THEN' atomize_tac) i
wenzelm@11996
   231
    |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
wenzelm@12799
   232
          st' |> Tactic.rtac rule' i
wenzelm@12799
   233
          |> Seq.map (rpair (make (rulified_term rule') cases)))
wenzelm@12799
   234
      |> Seq.flat)
wenzelm@11790
   235
    |> Seq.flat)
wenzelm@11790
   236
  |> Seq.flat;
wenzelm@11790
   237
wenzelm@11790
   238
infix 1 THEN_ALL_NEW_CASES;
wenzelm@11790
   239
wenzelm@11790
   240
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
wenzelm@11790
   241
  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
wenzelm@11790
   242
    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
wenzelm@11790
   243
wenzelm@11790
   244
wenzelm@11790
   245
(* find rules *)
wenzelm@11790
   246
wenzelm@11735
   247
fun find_inductT ctxt insts =
wenzelm@11735
   248
  foldr multiply (insts |> mapfilter (fn [] => None | ts => last_elem ts)
wenzelm@11735
   249
    |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
wenzelm@11735
   250
  |> map join_rules |> flat;
wenzelm@11670
   251
wenzelm@11735
   252
fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
wenzelm@11735
   253
  | find_inductS _ _ = [];
wenzelm@11735
   254
wenzelm@11790
   255
wenzelm@11790
   256
(* main tactic *)
wenzelm@11790
   257
wenzelm@11735
   258
fun induct_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
wenzelm@11670
   259
  let
wenzelm@11670
   260
    val sg = ProofContext.sign_of ctxt;
wenzelm@11670
   261
    val cert = Thm.cterm_of sg;
wenzelm@11670
   262
wenzelm@13105
   263
    fun rule_versions r = Seq.cons (r, Seq.filter (not o curry Thm.eq_thm r)
wenzelm@12168
   264
        (Seq.make (fn () => Some (localize r, Seq.empty))))
wenzelm@12168
   265
      |> Seq.map (rpair (RuleCases.get r));
wenzelm@12168
   266
wenzelm@12168
   267
    val inst_rule = apfst (fn r =>
wenzelm@12168
   268
      if null insts then r
wenzelm@11735
   269
      else (align_right "Rule has fewer conclusions than arguments given"
wenzelm@11735
   270
          (Data.dest_concls (Thm.concl_of r)) insts
wenzelm@12799
   271
        |> (flat o map (prep_inst align_right cert (atomize_term sg)))
wenzelm@12168
   272
        |> Drule.cterm_instantiate) r);
wenzelm@11670
   273
wenzelm@11735
   274
    val ruleq =
wenzelm@11735
   275
      (case opt_rule of
wenzelm@11735
   276
        None =>
wenzelm@11735
   277
          let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
wenzelm@12168
   278
            conditional (null rules) (fn () => error "Unable to figure out induct rule");
wenzelm@12053
   279
            Method.trace ctxt rules;
wenzelm@12168
   280
            rules |> Seq.THEN (Seq.of_list, Seq.THEN (rule_versions, Seq.try inst_rule))
wenzelm@11735
   281
          end
wenzelm@12168
   282
      | Some r => r |> Seq.THEN (rule_versions, Seq.single o inst_rule));
wenzelm@11670
   283
wenzelm@11735
   284
    fun prep_rule (th, (cases, n)) =
wenzelm@11996
   285
      Seq.map (rpair (cases, n - length facts, drop (n, facts)))
wenzelm@11996
   286
        (Method.multi_resolves (take (n, facts)) [th]);
wenzelm@11984
   287
    val tac = resolveq_cases_tac' (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq));
wenzelm@11670
   288
  in tac THEN_ALL_NEW_CASES rulify_tac end;
wenzelm@11670
   289
wenzelm@11670
   290
in
wenzelm@11670
   291
wenzelm@12852
   292
val induct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo induct_tac);
wenzelm@11670
   293
wenzelm@11670
   294
end;
wenzelm@11670
   295
wenzelm@11670
   296
wenzelm@11670
   297
wenzelm@11670
   298
(** concrete syntax **)
wenzelm@11670
   299
wenzelm@11670
   300
val openN = "open";
wenzelm@11670
   301
val ruleN = "rule";
wenzelm@11670
   302
val ofN = "of";
wenzelm@11670
   303
wenzelm@11670
   304
local
wenzelm@11670
   305
wenzelm@11735
   306
fun check k get name =
wenzelm@11670
   307
  (case get name of Some x => x
wenzelm@11670
   308
  | None => error ("No rule for " ^ k ^ " " ^ quote name));
wenzelm@11670
   309
wenzelm@11670
   310
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
wenzelm@11670
   311
wenzelm@11670
   312
fun rule get_type get_set =
wenzelm@11670
   313
  Scan.depend (fn ctxt =>
wenzelm@11670
   314
    let val sg = ProofContext.sign_of ctxt in
wenzelm@11735
   315
      spec InductAttrib.typeN >> (check InductAttrib.typeN (get_type ctxt) o
wenzelm@11735
   316
        Sign.certify_tyname sg o Sign.intern_tycon sg) ||
wenzelm@11735
   317
      spec InductAttrib.setN >> (check InductAttrib.setN (get_set ctxt) o
wenzelm@11735
   318
        Sign.certify_const sg o Sign.intern_const sg)
wenzelm@11670
   319
    end >> pair ctxt) ||
wenzelm@11670
   320
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
wenzelm@11670
   321
wenzelm@11670
   322
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS;
wenzelm@11670
   323
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
wenzelm@11670
   324
wenzelm@11670
   325
val kind_inst =
wenzelm@11670
   326
  (Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || Args.$$$ ruleN || Args.$$$ ofN)
wenzelm@11670
   327
    -- Args.colon;
wenzelm@11670
   328
val term = Scan.unless (Scan.lift kind_inst) Args.local_term;
wenzelm@11670
   329
val term_dummy = Scan.unless (Scan.lift kind_inst)
wenzelm@11670
   330
  (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
wenzelm@11670
   331
wenzelm@11670
   332
val instss = Args.and_list (Scan.repeat1 term_dummy);
wenzelm@11670
   333
wenzelm@11670
   334
in
wenzelm@11670
   335
wenzelm@11735
   336
val cases_args = Method.syntax (Args.mode openN -- (instss -- Scan.option cases_rule));
wenzelm@11735
   337
val induct_args = Method.syntax (Args.mode openN -- (instss -- Scan.option induct_rule));
wenzelm@11670
   338
wenzelm@11670
   339
end;
wenzelm@11670
   340
wenzelm@11670
   341
wenzelm@11670
   342
wenzelm@11670
   343
(** theory setup **)
wenzelm@11670
   344
wenzelm@11670
   345
val setup =
wenzelm@11670
   346
  [Method.add_methods
wenzelm@11670
   347
    [(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"),
wenzelm@11670
   348
     (InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")]];
wenzelm@11670
   349
wenzelm@11670
   350
end;