src/Provers/induct_method.ML
author wenzelm
Fri Oct 12 12:13:31 2001 +0200 (2001-10-12)
changeset 11735 60c0fa10bfc2
parent 11670 59f79df42d1f
child 11756 8d8a87f350d6
permissions -rw-r--r--
removed vars_of, concls_of;
removed additional rule instantiation argument;
proper enumeration of type rules;
append possibilities of set and type rules (analogous to elim-intro in 'rule');
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@11670
    13
  val conjI: thm
wenzelm@11670
    14
  val atomize: thm list
wenzelm@11670
    15
  val rulify1: thm list
wenzelm@11670
    16
  val rulify2: thm list
wenzelm@11670
    17
end;
wenzelm@11670
    18
wenzelm@11670
    19
signature INDUCT_METHOD =
wenzelm@11670
    20
sig
wenzelm@11670
    21
  val setup: (theory -> theory) list
wenzelm@11670
    22
end;
wenzelm@11670
    23
wenzelm@11670
    24
functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
wenzelm@11670
    25
struct
wenzelm@11670
    26
wenzelm@11670
    27
wenzelm@11670
    28
(** misc utils **)
wenzelm@11670
    29
wenzelm@11670
    30
(* align lists *)
wenzelm@11670
    31
wenzelm@11670
    32
fun align_left msg xs ys =
wenzelm@11670
    33
  let val m = length xs and n = length ys
wenzelm@11735
    34
  in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end;
wenzelm@11670
    35
wenzelm@11670
    36
fun align_right msg xs ys =
wenzelm@11670
    37
  let val m = length xs and n = length ys
wenzelm@11735
    38
  in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
wenzelm@11670
    39
wenzelm@11670
    40
wenzelm@11735
    41
(* prep_inst *)
wenzelm@11670
    42
wenzelm@11735
    43
fun prep_inst align cert tune (tm, ts) =
wenzelm@11670
    44
  let
wenzelm@11670
    45
    fun prep_var (x, Some t) =
wenzelm@11670
    46
          let
wenzelm@11670
    47
            val cx = cert x;
wenzelm@11670
    48
            val {T = xT, sign, ...} = Thm.rep_cterm cx;
wenzelm@11670
    49
            val orig_ct = cert t;
wenzelm@11735
    50
            val ct = tune orig_ct;
wenzelm@11670
    51
          in
wenzelm@11670
    52
            if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct)
wenzelm@11735
    53
            else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
wenzelm@11735
    54
             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
wenzelm@11735
    55
              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
wenzelm@11735
    56
              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
wenzelm@11670
    57
          end
wenzelm@11670
    58
      | prep_var (_, None) = None;
wenzelm@11735
    59
    val xs = InductAttrib.vars_of tm;
wenzelm@11670
    60
  in
wenzelm@11735
    61
    align "Rule has fewer variables than instantiations given" xs ts
wenzelm@11670
    62
    |> mapfilter prep_var
wenzelm@11670
    63
  end;
wenzelm@11670
    64
wenzelm@11670
    65
wenzelm@11735
    66
(* tactics with cases *)
wenzelm@11670
    67
wenzelm@11735
    68
fun resolveq_cases_tac make tac ruleq i st =
wenzelm@11735
    69
  ruleq |> Seq.map (fn (rule, (cases, facts)) =>
wenzelm@11735
    70
    (Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st
wenzelm@11735
    71
    |> Seq.map (rpair (make rule cases)))
wenzelm@11735
    72
  |> Seq.flat;
wenzelm@11670
    73
wenzelm@11735
    74
wenzelm@11735
    75
infix 1 THEN_ALL_NEW_CASES;
wenzelm@11670
    76
wenzelm@11735
    77
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
wenzelm@11735
    78
  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
wenzelm@11735
    79
    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
wenzelm@11670
    80
wenzelm@11670
    81
wenzelm@11670
    82
wenzelm@11670
    83
(** cases method **)
wenzelm@11670
    84
wenzelm@11670
    85
(*
wenzelm@11735
    86
  rule selection scheme:
wenzelm@11735
    87
          cases         - classical case split
wenzelm@11735
    88
    <x:A> cases ...     - set cases
wenzelm@11735
    89
          cases t       - type cases
wenzelm@11735
    90
    ...   cases ... R   - explicit rule
wenzelm@11670
    91
*)
wenzelm@11670
    92
wenzelm@11670
    93
local
wenzelm@11670
    94
wenzelm@11735
    95
fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
wenzelm@11735
    96
  | find_casesT _ _ = [];
wenzelm@11735
    97
wenzelm@11735
    98
fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt fact
wenzelm@11735
    99
  | find_casesS _ _ = [];
wenzelm@11735
   100
wenzelm@11735
   101
fun cases_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
wenzelm@11670
   102
  let
wenzelm@11670
   103
    val sg = ProofContext.sign_of ctxt;
wenzelm@11670
   104
    val cert = Thm.cterm_of sg;
wenzelm@11670
   105
wenzelm@11735
   106
    fun inst_rule r =
wenzelm@11735
   107
      if null insts then RuleCases.add r
wenzelm@11735
   108
      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
wenzelm@11670
   109
        |> (flat o map (prep_inst align_left cert I))
wenzelm@11735
   110
        |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
wenzelm@11670
   111
wenzelm@11735
   112
    val ruleq =
wenzelm@11735
   113
      (case (facts, insts, opt_rule) of
wenzelm@11735
   114
        ([], [], None) => Seq.single (RuleCases.add Data.cases_default)
wenzelm@11735
   115
      | (_, _, None) =>
wenzelm@11735
   116
          let val rules = find_casesS ctxt facts @ find_casesT ctxt insts in
wenzelm@11735
   117
            if null rules then error "Unable to figure out cases rule" else ();
wenzelm@11735
   118
            Method.trace rules;
wenzelm@11735
   119
            Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
wenzelm@11670
   120
          end
wenzelm@11735
   121
      | (_, _, Some r) => Seq.single (inst_rule r));
wenzelm@11670
   122
wenzelm@11735
   123
    fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
wenzelm@11735
   124
      (Method.multi_resolves (take (n, facts)) [th]);
wenzelm@11670
   125
  in
wenzelm@11670
   126
    resolveq_cases_tac (RuleCases.make open_parms) (K all_tac)
wenzelm@11735
   127
      (Seq.flat (Seq.map prep_rule ruleq))
wenzelm@11670
   128
  end;
wenzelm@11670
   129
wenzelm@11670
   130
in
wenzelm@11670
   131
wenzelm@11670
   132
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
wenzelm@11670
   133
wenzelm@11670
   134
end;
wenzelm@11670
   135
wenzelm@11670
   136
wenzelm@11670
   137
wenzelm@11670
   138
(** induct method **)
wenzelm@11670
   139
wenzelm@11670
   140
(*
wenzelm@11735
   141
  rule selection scheme:
wenzelm@11735
   142
    <x:A> induct ...     - set induction
wenzelm@11735
   143
          induct x       - type induction
wenzelm@11735
   144
    ...   induct ... R   - explicit rule
wenzelm@11670
   145
*)
wenzelm@11670
   146
wenzelm@11670
   147
local
wenzelm@11670
   148
wenzelm@11670
   149
val atomize_cterm = Thm.cterm_fun AutoBind.drop_judgment o full_rewrite_cterm Data.atomize;
wenzelm@11670
   150
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
wenzelm@11670
   151
val rulify_cterm = full_rewrite_cterm Data.rulify2 o full_rewrite_cterm Data.rulify1;
wenzelm@11670
   152
wenzelm@11670
   153
val rulify_tac =
wenzelm@11670
   154
  Tactic.rewrite_goal_tac Data.rulify1 THEN'
wenzelm@11670
   155
  Tactic.rewrite_goal_tac Data.rulify2 THEN'
wenzelm@11670
   156
  Tactic.norm_hhf_tac;
wenzelm@11670
   157
wenzelm@11670
   158
fun rulify_cases cert =
wenzelm@11670
   159
  let
wenzelm@11670
   160
    val ruly = Thm.term_of o rulify_cterm o cert;
wenzelm@11670
   161
    fun ruly_case {fixes, assumes, binds} =
wenzelm@11670
   162
      {fixes = fixes, assumes = map ruly assumes,
wenzelm@11670
   163
        binds = map (apsnd (apsome (AutoBind.drop_judgment o ruly))) binds};
wenzelm@11670
   164
  in map (apsnd ruly_case) ooo RuleCases.make_raw end;
wenzelm@11670
   165
wenzelm@11670
   166
wenzelm@11735
   167
val eq_prems = curry (Term.aconvs o pairself Thm.prems_of);
wenzelm@11670
   168
wenzelm@11735
   169
fun join_rules [] = []
wenzelm@11735
   170
  | join_rules [th] = [th]
wenzelm@11735
   171
  | join_rules (rules as r :: rs) =
wenzelm@11735
   172
      if not (forall (eq_prems r) rs) then []
wenzelm@11735
   173
      else
wenzelm@11735
   174
        let
wenzelm@11735
   175
          val th :: ths = map Drule.freeze_all rules;
wenzelm@11735
   176
          val cprems = Drule.cprems_of th;
wenzelm@11735
   177
          val asms = map Thm.assume cprems;
wenzelm@11735
   178
        in
wenzelm@11735
   179
          [foldr1 (fn (x, x') => [x, x'] MRS Data.conjI)
wenzelm@11735
   180
            (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
wenzelm@11735
   181
          |> Drule.implies_intr_list cprems
wenzelm@11735
   182
          |> Drule.standard']
wenzelm@11735
   183
        end;
wenzelm@11670
   184
wenzelm@11735
   185
fun find_inductT ctxt insts =
wenzelm@11735
   186
  foldr multiply (insts |> mapfilter (fn [] => None | ts => last_elem ts)
wenzelm@11735
   187
    |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
wenzelm@11735
   188
  |> map join_rules |> flat;
wenzelm@11670
   189
wenzelm@11735
   190
fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
wenzelm@11735
   191
  | find_inductS _ _ = [];
wenzelm@11735
   192
wenzelm@11735
   193
fun induct_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
wenzelm@11670
   194
  let
wenzelm@11670
   195
    val sg = ProofContext.sign_of ctxt;
wenzelm@11670
   196
    val cert = Thm.cterm_of sg;
wenzelm@11670
   197
wenzelm@11735
   198
    fun inst_rule r =
wenzelm@11735
   199
      if null insts then RuleCases.add r
wenzelm@11735
   200
      else (align_right "Rule has fewer conclusions than arguments given"
wenzelm@11735
   201
          (Data.dest_concls (Thm.concl_of r)) insts
wenzelm@11670
   202
        |> (flat o map (prep_inst align_right cert atomize_cterm))
wenzelm@11735
   203
        |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
wenzelm@11670
   204
wenzelm@11735
   205
    val ruleq =
wenzelm@11735
   206
      (case opt_rule of
wenzelm@11735
   207
        None =>
wenzelm@11735
   208
          let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
wenzelm@11735
   209
            if null rules then error "Unable to figure out induct rule" else ();
wenzelm@11735
   210
            Method.trace rules;
wenzelm@11735
   211
            Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
wenzelm@11735
   212
          end
wenzelm@11735
   213
      | Some r => Seq.single (inst_rule r));
wenzelm@11670
   214
wenzelm@11735
   215
    (* FIXME divinate rule_inst *)
wenzelm@11735
   216
wenzelm@11735
   217
    fun prep_rule (th, (cases, n)) =
wenzelm@11735
   218
      Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [th]);
wenzelm@11670
   219
    val tac = resolveq_cases_tac (rulify_cases cert open_parms) atomize_tac
wenzelm@11735
   220
      (Seq.flat (Seq.map prep_rule ruleq));
wenzelm@11670
   221
  in tac THEN_ALL_NEW_CASES rulify_tac end;
wenzelm@11670
   222
wenzelm@11670
   223
in
wenzelm@11670
   224
wenzelm@11670
   225
val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac);
wenzelm@11670
   226
wenzelm@11670
   227
end;
wenzelm@11670
   228
wenzelm@11670
   229
wenzelm@11670
   230
wenzelm@11670
   231
(** concrete syntax **)
wenzelm@11670
   232
wenzelm@11670
   233
val openN = "open";
wenzelm@11670
   234
val ruleN = "rule";
wenzelm@11670
   235
val ofN = "of";
wenzelm@11670
   236
wenzelm@11670
   237
local
wenzelm@11670
   238
wenzelm@11735
   239
fun check k get name =
wenzelm@11670
   240
  (case get name of Some x => x
wenzelm@11670
   241
  | None => error ("No rule for " ^ k ^ " " ^ quote name));
wenzelm@11670
   242
wenzelm@11670
   243
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
wenzelm@11670
   244
wenzelm@11670
   245
fun rule get_type get_set =
wenzelm@11670
   246
  Scan.depend (fn ctxt =>
wenzelm@11670
   247
    let val sg = ProofContext.sign_of ctxt in
wenzelm@11735
   248
      spec InductAttrib.typeN >> (check InductAttrib.typeN (get_type ctxt) o
wenzelm@11735
   249
        Sign.certify_tyname sg o Sign.intern_tycon sg) ||
wenzelm@11735
   250
      spec InductAttrib.setN >> (check InductAttrib.setN (get_set ctxt) o
wenzelm@11735
   251
        Sign.certify_const sg o Sign.intern_const sg)
wenzelm@11670
   252
    end >> pair ctxt) ||
wenzelm@11670
   253
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
wenzelm@11670
   254
wenzelm@11670
   255
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS;
wenzelm@11670
   256
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
wenzelm@11670
   257
wenzelm@11670
   258
val kind_inst =
wenzelm@11670
   259
  (Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || Args.$$$ ruleN || Args.$$$ ofN)
wenzelm@11670
   260
    -- Args.colon;
wenzelm@11670
   261
val term = Scan.unless (Scan.lift kind_inst) Args.local_term;
wenzelm@11670
   262
val term_dummy = Scan.unless (Scan.lift kind_inst)
wenzelm@11670
   263
  (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
wenzelm@11670
   264
wenzelm@11670
   265
val instss = Args.and_list (Scan.repeat1 term_dummy);
wenzelm@11670
   266
wenzelm@11670
   267
in
wenzelm@11670
   268
wenzelm@11735
   269
val cases_args = Method.syntax (Args.mode openN -- (instss -- Scan.option cases_rule));
wenzelm@11735
   270
val induct_args = Method.syntax (Args.mode openN -- (instss -- Scan.option induct_rule));
wenzelm@11670
   271
wenzelm@11670
   272
end;
wenzelm@11670
   273
wenzelm@11670
   274
wenzelm@11670
   275
wenzelm@11670
   276
(** theory setup **)
wenzelm@11670
   277
wenzelm@11670
   278
val setup =
wenzelm@11670
   279
  [Method.add_methods
wenzelm@11670
   280
    [(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"),
wenzelm@11670
   281
     (InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")]];
wenzelm@11670
   282
wenzelm@11670
   283
end;