src/Provers/induct_method.ML
author wenzelm
Thu Oct 04 15:20:40 2001 +0200 (2001-10-04)
changeset 11670 59f79df42d1f
child 11735 60c0fa10bfc2
permissions -rw-r--r--
proof by cases and induction on types and sets (used to be specific for HOL);
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@11670
     6
Proof by cases and induction on types and sets.
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 vars_of: term -> term list
wenzelm@11670
    22
  val concls_of: thm -> term list
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@11670
    36
  in if m < n then error 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@11670
    40
  in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
wenzelm@11670
    41
wenzelm@11670
    42
wenzelm@11670
    43
(* thms and terms *)
wenzelm@11670
    44
wenzelm@11670
    45
val concls_of = Data.dest_concls o Thm.concl_of;
wenzelm@11670
    46
wenzelm@11670
    47
fun vars_of tm =        (*ordered left-to-right, preferring right!*)
wenzelm@11670
    48
  Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
wenzelm@11670
    49
  |> Library.distinct |> rev;
wenzelm@11670
    50
wenzelm@11670
    51
fun type_name t =
wenzelm@11670
    52
  #1 (Term.dest_Type (Term.type_of t))
wenzelm@11670
    53
    handle TYPE _ => raise TERM ("Type of term argument is too general", [t]);
wenzelm@11670
    54
wenzelm@11670
    55
fun prep_inst align cert f (tm, ts) =
wenzelm@11670
    56
  let
wenzelm@11670
    57
    fun prep_var (x, Some t) =
wenzelm@11670
    58
          let
wenzelm@11670
    59
            val cx = cert x;
wenzelm@11670
    60
            val {T = xT, sign, ...} = Thm.rep_cterm cx;
wenzelm@11670
    61
            val orig_ct = cert t;
wenzelm@11670
    62
            val ct = f orig_ct;
wenzelm@11670
    63
          in
wenzelm@11670
    64
            if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct)
wenzelm@11670
    65
            else error (Pretty.string_of (Pretty.block
wenzelm@11670
    66
              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
wenzelm@11670
    67
                Display.pretty_cterm orig_ct, Pretty.str " ::", Pretty.brk 1,
wenzelm@11670
    68
                Display.pretty_ctyp (#T (Thm.crep_cterm orig_ct))]))
wenzelm@11670
    69
          end
wenzelm@11670
    70
      | prep_var (_, None) = None;
wenzelm@11670
    71
  in
wenzelm@11670
    72
    align "Rule has fewer variables than instantiations given" (vars_of tm) ts
wenzelm@11670
    73
    |> mapfilter prep_var
wenzelm@11670
    74
  end;
wenzelm@11670
    75
wenzelm@11670
    76
wenzelm@11670
    77
(* resolution and cases *)
wenzelm@11670
    78
wenzelm@11670
    79
local
wenzelm@11670
    80
wenzelm@11670
    81
fun gen_resolveq_tac tac rules i st =
wenzelm@11670
    82
  Seq.flat (Seq.map (fn rule => tac rule i st) rules);
wenzelm@11670
    83
wenzelm@11670
    84
in
wenzelm@11670
    85
wenzelm@11670
    86
fun resolveq_cases_tac make tac = gen_resolveq_tac (fn (rule, (cases, facts)) => fn i => fn st =>
wenzelm@11670
    87
  Seq.map (rpair (make rule cases))
wenzelm@11670
    88
    ((Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st));
wenzelm@11670
    89
wenzelm@11670
    90
end;
wenzelm@11670
    91
wenzelm@11670
    92
wenzelm@11670
    93
wenzelm@11670
    94
(** cases method **)
wenzelm@11670
    95
wenzelm@11670
    96
(*
wenzelm@11670
    97
  rule selection:
wenzelm@11670
    98
        cases         - classical case split
wenzelm@11670
    99
        cases t       - datatype exhaustion
wenzelm@11670
   100
  <x:A> cases ...     - set elimination
wenzelm@11670
   101
  ...   cases ... R   - explicit rule
wenzelm@11670
   102
*)
wenzelm@11670
   103
wenzelm@11670
   104
local
wenzelm@11670
   105
wenzelm@11670
   106
fun cases_tac (ctxt, (open_parms, args)) facts =
wenzelm@11670
   107
  let
wenzelm@11670
   108
    val sg = ProofContext.sign_of ctxt;
wenzelm@11670
   109
    val cert = Thm.cterm_of sg;
wenzelm@11670
   110
wenzelm@11670
   111
    fun inst_rule insts thm =
wenzelm@11670
   112
      (align_left "Rule has fewer premises than arguments given" (Thm.prems_of thm) insts
wenzelm@11670
   113
        |> (flat o map (prep_inst align_left cert I))
wenzelm@11670
   114
        |> Drule.cterm_instantiate) thm;
wenzelm@11670
   115
wenzelm@11670
   116
    fun find_cases th =
wenzelm@11670
   117
      NetRules.may_unify (#2 (InductAttrib.get_cases ctxt))
wenzelm@11670
   118
        (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
wenzelm@11670
   119
wenzelm@11670
   120
    val rules =
wenzelm@11670
   121
      (case (fst args, facts) of
wenzelm@11670
   122
        (([], None), []) => [RuleCases.add Data.cases_default]
wenzelm@11670
   123
      | ((insts, None), []) =>
wenzelm@11670
   124
          let
wenzelm@11670
   125
            val name = type_name (hd (flat (map (mapfilter I) insts)))
wenzelm@11670
   126
              handle Library.LIST _ => error "Unable to figure out type cases rule"
wenzelm@11670
   127
          in
wenzelm@11670
   128
            (case InductAttrib.lookup_casesT ctxt name of
wenzelm@11670
   129
              None => error ("No cases rule for type: " ^ quote name)
wenzelm@11670
   130
            | Some thm => [(inst_rule insts thm, RuleCases.get thm)])
wenzelm@11670
   131
          end
wenzelm@11670
   132
      | (([], None), th :: _) => map (RuleCases.add o #2) (find_cases th)
wenzelm@11670
   133
      | ((insts, None), th :: _) =>
wenzelm@11670
   134
          (case find_cases th of        (*may instantiate first rule only!*)
wenzelm@11670
   135
            (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
wenzelm@11670
   136
          | [] => [])
wenzelm@11670
   137
      | (([], Some thm), _) => [RuleCases.add thm]
wenzelm@11670
   138
      | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)])
wenzelm@11670
   139
      |> map (Library.apfst (Attrib.read_inst' (snd args) ctxt));
wenzelm@11670
   140
wenzelm@11670
   141
    fun prep_rule (thm, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
wenzelm@11670
   142
      (Method.multi_resolves (take (n, facts)) [thm]);
wenzelm@11670
   143
  in
wenzelm@11670
   144
    resolveq_cases_tac (RuleCases.make open_parms) (K all_tac)
wenzelm@11670
   145
      (Seq.flat (Seq.map prep_rule (Seq.of_list rules)))
wenzelm@11670
   146
  end;
wenzelm@11670
   147
wenzelm@11670
   148
in
wenzelm@11670
   149
wenzelm@11670
   150
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
wenzelm@11670
   151
wenzelm@11670
   152
end;
wenzelm@11670
   153
wenzelm@11670
   154
wenzelm@11670
   155
wenzelm@11670
   156
(** induct method **)
wenzelm@11670
   157
wenzelm@11670
   158
(*
wenzelm@11670
   159
  rule selection:
wenzelm@11670
   160
        induct x       - datatype induction
wenzelm@11670
   161
  <x:A> induct ...     - set induction
wenzelm@11670
   162
  ...   induct ... R   - explicit rule
wenzelm@11670
   163
*)
wenzelm@11670
   164
wenzelm@11670
   165
local
wenzelm@11670
   166
wenzelm@11670
   167
val atomize_cterm = Thm.cterm_fun AutoBind.drop_judgment o full_rewrite_cterm Data.atomize;
wenzelm@11670
   168
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
wenzelm@11670
   169
val rulify_cterm = full_rewrite_cterm Data.rulify2 o full_rewrite_cterm Data.rulify1;
wenzelm@11670
   170
wenzelm@11670
   171
val rulify_tac =
wenzelm@11670
   172
  Tactic.rewrite_goal_tac Data.rulify1 THEN'
wenzelm@11670
   173
  Tactic.rewrite_goal_tac Data.rulify2 THEN'
wenzelm@11670
   174
  Tactic.norm_hhf_tac;
wenzelm@11670
   175
wenzelm@11670
   176
fun rulify_cases cert =
wenzelm@11670
   177
  let
wenzelm@11670
   178
    val ruly = Thm.term_of o rulify_cterm o cert;
wenzelm@11670
   179
    fun ruly_case {fixes, assumes, binds} =
wenzelm@11670
   180
      {fixes = fixes, assumes = map ruly assumes,
wenzelm@11670
   181
        binds = map (apsnd (apsome (AutoBind.drop_judgment o ruly))) binds};
wenzelm@11670
   182
  in map (apsnd ruly_case) ooo RuleCases.make_raw end;
wenzelm@11670
   183
wenzelm@11670
   184
wenzelm@11670
   185
infix 1 THEN_ALL_NEW_CASES;
wenzelm@11670
   186
wenzelm@11670
   187
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
wenzelm@11670
   188
  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
wenzelm@11670
   189
    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
wenzelm@11670
   190
wenzelm@11670
   191
wenzelm@11670
   192
fun induct_rule ctxt t =
wenzelm@11670
   193
  let val name = type_name t in
wenzelm@11670
   194
    (case InductAttrib.lookup_inductT ctxt name of
wenzelm@11670
   195
      None => error ("No induct rule for type: " ^ quote name)
wenzelm@11670
   196
    | Some thm => (name, thm))
wenzelm@11670
   197
  end;
wenzelm@11670
   198
wenzelm@11670
   199
fun join_rules [(_, thm)] = thm
wenzelm@11670
   200
  | join_rules raw_thms =
wenzelm@11670
   201
      let
wenzelm@11670
   202
        val thms = (map (apsnd Drule.freeze_all) raw_thms);
wenzelm@11670
   203
        fun eq_prems ((_, th1), (_, th2)) =
wenzelm@11670
   204
          Term.aconvs (Thm.prems_of th1, Thm.prems_of th2);
wenzelm@11670
   205
      in
wenzelm@11670
   206
        (case Library.gen_distinct eq_prems thms of
wenzelm@11670
   207
          [(_, thm)] =>
wenzelm@11670
   208
            let
wenzelm@11670
   209
              val cprems = Drule.cprems_of thm;
wenzelm@11670
   210
              val asms = map Thm.assume cprems;
wenzelm@11670
   211
              fun strip (_, th) = Drule.implies_elim_list th asms;
wenzelm@11670
   212
            in
wenzelm@11670
   213
              foldr1 (fn (th, th') => [th, th'] MRS Data.conjI) (map strip thms)
wenzelm@11670
   214
              |> Drule.implies_intr_list cprems
wenzelm@11670
   215
              |> Drule.standard
wenzelm@11670
   216
            end
wenzelm@11670
   217
        | [] => error "No rule given"
wenzelm@11670
   218
        | bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads)))
wenzelm@11670
   219
      end;
wenzelm@11670
   220
wenzelm@11670
   221
wenzelm@11670
   222
fun induct_tac (ctxt, (open_parms, args)) facts =
wenzelm@11670
   223
  let
wenzelm@11670
   224
    val sg = ProofContext.sign_of ctxt;
wenzelm@11670
   225
    val cert = Thm.cterm_of sg;
wenzelm@11670
   226
wenzelm@11670
   227
    fun inst_rule insts thm =
wenzelm@11670
   228
      (align_right "Rule has fewer conclusions than arguments given" (concls_of thm) insts
wenzelm@11670
   229
        |> (flat o map (prep_inst align_right cert atomize_cterm))
wenzelm@11670
   230
        |> Drule.cterm_instantiate) thm;
wenzelm@11670
   231
wenzelm@11670
   232
    fun find_induct th =
wenzelm@11670
   233
      NetRules.may_unify (#2 (InductAttrib.get_induct ctxt))
wenzelm@11670
   234
        (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
wenzelm@11670
   235
wenzelm@11670
   236
    val rules =
wenzelm@11670
   237
      (case (fst args, facts) of
wenzelm@11670
   238
        (([], None), []) => []
wenzelm@11670
   239
      | ((insts, None), []) =>
wenzelm@11670
   240
          let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts
wenzelm@11670
   241
            handle Library.LIST _ => error "Unable to figure out type induction rule"
wenzelm@11670
   242
          in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end
wenzelm@11670
   243
      | (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th)
wenzelm@11670
   244
      | ((insts, None), th :: _) =>
wenzelm@11670
   245
          (case find_induct th of       (*may instantiate first rule only!*)
wenzelm@11670
   246
            (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
wenzelm@11670
   247
          | [] => [])
wenzelm@11670
   248
      | (([], Some thm), _) => [RuleCases.add thm]
wenzelm@11670
   249
      | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)])
wenzelm@11670
   250
      |> map (Library.apfst (Attrib.read_inst' (snd args) ctxt));
wenzelm@11670
   251
wenzelm@11670
   252
    fun prep_rule (thm, (cases, n)) =
wenzelm@11670
   253
      Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [thm]);
wenzelm@11670
   254
    val tac = resolveq_cases_tac (rulify_cases cert open_parms) atomize_tac
wenzelm@11670
   255
      (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
wenzelm@11670
   256
  in tac THEN_ALL_NEW_CASES rulify_tac end;
wenzelm@11670
   257
wenzelm@11670
   258
in
wenzelm@11670
   259
wenzelm@11670
   260
val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac);
wenzelm@11670
   261
wenzelm@11670
   262
end;
wenzelm@11670
   263
wenzelm@11670
   264
wenzelm@11670
   265
wenzelm@11670
   266
(** concrete syntax **)
wenzelm@11670
   267
wenzelm@11670
   268
val openN = "open";
wenzelm@11670
   269
val ruleN = "rule";
wenzelm@11670
   270
val ofN = "of";
wenzelm@11670
   271
wenzelm@11670
   272
local
wenzelm@11670
   273
wenzelm@11670
   274
fun err k get name =
wenzelm@11670
   275
  (case get name of Some x => x
wenzelm@11670
   276
  | None => error ("No rule for " ^ k ^ " " ^ quote name));
wenzelm@11670
   277
wenzelm@11670
   278
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
wenzelm@11670
   279
wenzelm@11670
   280
fun rule get_type get_set =
wenzelm@11670
   281
  Scan.depend (fn ctxt =>
wenzelm@11670
   282
    let val sg = ProofContext.sign_of ctxt in
wenzelm@11670
   283
      spec InductAttrib.typeN >> (err InductAttrib.typeN (get_type ctxt) o Sign.intern_tycon sg) ||
wenzelm@11670
   284
      spec InductAttrib.setN >> (err InductAttrib.setN (get_set ctxt) o Sign.intern_const sg)
wenzelm@11670
   285
    end >> pair ctxt) ||
wenzelm@11670
   286
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
wenzelm@11670
   287
wenzelm@11670
   288
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS;
wenzelm@11670
   289
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
wenzelm@11670
   290
wenzelm@11670
   291
val kind_inst =
wenzelm@11670
   292
  (Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || Args.$$$ ruleN || Args.$$$ ofN)
wenzelm@11670
   293
    -- Args.colon;
wenzelm@11670
   294
val term = Scan.unless (Scan.lift kind_inst) Args.local_term;
wenzelm@11670
   295
val term_dummy = Scan.unless (Scan.lift kind_inst)
wenzelm@11670
   296
  (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
wenzelm@11670
   297
wenzelm@11670
   298
val instss = Args.and_list (Scan.repeat1 term_dummy);
wenzelm@11670
   299
wenzelm@11670
   300
(* FIXME Attrib.insts': better use actual term args *)
wenzelm@11670
   301
val rule_insts =
wenzelm@11670
   302
  Scan.lift (Scan.optional ((Args.$$$ ofN -- Args.colon) |-- Args.!!! Attrib.insts') ([], []));
wenzelm@11670
   303
wenzelm@11670
   304
in
wenzelm@11670
   305
wenzelm@11670
   306
val cases_args =
wenzelm@11670
   307
  Method.syntax (Args.mode openN -- (instss -- Scan.option cases_rule -- rule_insts));
wenzelm@11670
   308
wenzelm@11670
   309
val induct_args =
wenzelm@11670
   310
  Method.syntax (Args.mode openN -- (instss -- Scan.option induct_rule -- rule_insts));
wenzelm@11670
   311
wenzelm@11670
   312
end;
wenzelm@11670
   313
wenzelm@11670
   314
wenzelm@11670
   315
wenzelm@11670
   316
(** theory setup **)
wenzelm@11670
   317
wenzelm@11670
   318
val setup =
wenzelm@11670
   319
  [Method.add_methods
wenzelm@11670
   320
    [(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"),
wenzelm@11670
   321
     (InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")]];
wenzelm@11670
   322
wenzelm@11670
   323
end;