src/Provers/induct_method.ML
author haftmann
Tue, 04 Oct 2005 10:58:46 +0200
changeset 17749 4fb42f4d61df
parent 16391 65c8070844ea
child 17961 6ebd59acf58a
permissions -rw-r--r--
removed removed IntFloor
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     1
(*  Title:      Provers/induct_method.ML
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     4
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
     5
Proof by cases and induction on sets and types.
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     6
*)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     7
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     8
signature INDUCT_METHOD_DATA =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     9
sig
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    10
  val dest_concls: term -> term list
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    11
  val cases_default: thm
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
    12
  val local_impI: thm
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    13
  val conjI: thm
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    14
  val atomize: thm list
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    15
  val rulify1: thm list
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    16
  val rulify2: thm list
12240
0760eda193c4 induct method: localize rews for rule;
wenzelm
parents: 12168
diff changeset
    17
  val localize: thm list
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    18
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    19
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    20
signature INDUCT_METHOD =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    21
sig
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
    22
  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
    23
    thm list -> int -> RuleCases.tactic
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
    24
  val induct_tac: Proof.context -> bool -> term option list list ->
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
    25
    thm option -> thm list -> int -> RuleCases.tactic
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    26
  val setup: (theory -> theory) list
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    27
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    28
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    29
functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    30
struct
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    31
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    32
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    33
(** misc utils **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    34
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    35
(* align lists *)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    36
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    37
fun align_left msg xs ys =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    38
  let val m = length xs and n = length ys
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    39
  in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    40
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    41
fun align_right msg xs ys =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    42
  let val m = length xs and n = length ys
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    43
  in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    44
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    45
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    46
(* prep_inst *)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    47
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    48
fun prep_inst align cert tune (tm, ts) =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    49
  let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
    50
    fun prep_var (x, SOME t) =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    51
          let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    52
            val cx = cert x;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    53
            val {T = xT, sign, ...} = Thm.rep_cterm cx;
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
    54
            val ct = cert (tune t);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    55
          in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
    56
            if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    57
            else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    58
             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    59
              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    60
              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    61
          end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
    62
      | prep_var (_, NONE) = NONE;
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    63
    val xs = InductAttrib.vars_of tm;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    64
  in
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    65
    align "Rule has fewer variables than instantiations given" xs ts
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    66
    |> List.mapPartial prep_var
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    67
  end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    68
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    69
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    70
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    71
(** cases method **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    72
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    73
(*
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    74
  rule selection scheme:
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    75
          cases         - classical case split
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    76
    <x:A> cases ...     - set cases
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    77
          cases t       - type cases
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    78
    ...   cases ... R   - explicit rule
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    79
*)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    80
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    81
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    82
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    83
fun resolveq_cases_tac make ruleq i st =
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    84
  ruleq |> Seq.map (fn (rule, (cases, facts)) =>
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    85
    (Method.insert_tac facts THEN' Tactic.rtac rule) i st
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
    86
    |> Seq.map (rpair (make (Thm.sign_of_thm rule, Thm.prop_of rule) cases)))
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    87
  |> Seq.flat;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    88
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
    89
fun find_casesT ctxt ((SOME t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    90
  | find_casesT _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    91
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    92
fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt fact
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    93
  | find_casesS _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    94
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
    95
in
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
    96
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
    97
fun cases_tac ctxt is_open insts opt_rule facts =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    98
  let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    99
    val sg = ProofContext.sign_of ctxt;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   100
    val cert = Thm.cterm_of sg;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   101
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   102
    fun inst_rule r =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   103
      if null insts then RuleCases.add r
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   104
      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   105
        |> (List.concat o map (prep_inst align_left cert I))
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   106
        |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   107
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   108
    val ruleq =
12852
c6a8e310aec5 cases: really append cases_default;
wenzelm
parents: 12799
diff changeset
   109
      (case opt_rule of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   110
        NONE =>
12852
c6a8e310aec5 cases: really append cases_default;
wenzelm
parents: 12799
diff changeset
   111
          let val rules = find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default] in
12053
7e2e84e503ce Method.trace ctxt;
wenzelm
parents: 11996
diff changeset
   112
            Method.trace ctxt rules;
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   113
            Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   114
          end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   115
      | SOME r => Seq.single (inst_rule r));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   116
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   117
    fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (Library.drop (n, facts))) o rpair cases)
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   118
      (Method.multi_resolves (Library.take (n, facts)) [th]);
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   119
  in resolveq_cases_tac (RuleCases.make is_open NONE) (Seq.flat (Seq.map prep_rule ruleq)) end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   120
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   121
val cases_meth = Method.METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   122
  (fn (ctxt, (is_open, (insts, opt_rule))) => cases_tac ctxt is_open insts opt_rule));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   123
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   124
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   125
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   126
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   127
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   128
(** induct method **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   129
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   130
(*
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   131
  rule selection scheme:
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   132
    <x:A> induct ...     - set induction
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   133
          induct x       - type induction
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   134
    ...   induct ... R   - explicit rule
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   135
*)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   136
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   137
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   138
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   139
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   140
(* atomize and rulify *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   141
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   142
fun atomize_term sg =
13197
0567f4fd1415 Changed interface of MetaSimplifier.rewrite_term.
berghofe
parents: 13105
diff changeset
   143
  ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize [];
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   144
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   145
fun rulified_term thm =
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   146
  let val sg = Thm.sign_of_thm thm in
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   147
    Thm.prop_of thm
13197
0567f4fd1415 Changed interface of MetaSimplifier.rewrite_term.
berghofe
parents: 13105
diff changeset
   148
    |> MetaSimplifier.rewrite_term sg Data.rulify1 []
0567f4fd1415 Changed interface of MetaSimplifier.rewrite_term.
berghofe
parents: 13105
diff changeset
   149
    |> MetaSimplifier.rewrite_term sg Data.rulify2 []
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   150
    |> pair sg
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   151
  end;
11756
8d8a87f350d6 use ObjectLogic stuff;
wenzelm
parents: 11735
diff changeset
   152
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   153
val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   154
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   155
val rulify_tac =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   156
  Tactic.rewrite_goal_tac Data.rulify1 THEN'
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   157
  Tactic.rewrite_goal_tac Data.rulify2 THEN'
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   158
  Tactic.norm_hhf_tac;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   159
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   160
val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize;
12162
7c74a52da110 proper handling of mutual rules (esp. for sets);
wenzelm
parents: 12053
diff changeset
   161
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   162
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   163
(* imp_intr --- limited to atomic prems *)
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   164
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   165
fun imp_intr i raw_th =
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   166
  let
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   167
    val th = Thm.permute_prems (i - 1) 1 raw_th;
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   168
    val cprems = Drule.cprems_of th;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   169
    val As = Library.take (length cprems - 1, cprems);
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   170
    val C = Thm.cterm_of (Thm.sign_of_thm th) (Var (("C", #maxidx (Thm.rep_thm th) + 1), propT));
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   171
    val dummy_st = Drule.mk_triv_goal (Drule.list_implies (As, C));
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   172
  in th COMP Thm.lift_rule (dummy_st, 1) Data.local_impI end;
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   173
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   174
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   175
(* join multi-rules *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   176
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   177
val eq_prems = curry (Term.aconvs o pairself Thm.prems_of);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   178
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   179
fun join_rules [] = []
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   180
  | join_rules [th] = [th]
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   181
  | join_rules (rules as r :: rs) =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   182
      if not (forall (eq_prems r) rs) then []
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   183
      else
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   184
        let
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   185
          val th :: ths = map Drule.freeze_all rules;
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   186
          val cprems = Drule.cprems_of th;
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   187
          val asms = map Thm.assume cprems;
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   188
        in
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   189
          [foldr1 (fn (x, x') => [x, x'] MRS Data.conjI)
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   190
            (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   191
          |> Drule.implies_intr_list cprems
12305
3c3f98b3d9e7 join_rules RuleCases.save;
wenzelm
parents: 12240
diff changeset
   192
          |> Drule.standard'
13425
119ae829ad9b support for split assumptions in cases (hyps vs. prems);
wenzelm
parents: 13197
diff changeset
   193
          |> RuleCases.save r]
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   194
        end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   195
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   196
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   197
(* divinate rule instantiation (cannot handle pending goal parameters) *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   198
15794
5de27a5fc5ed Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15708
diff changeset
   199
fun dest_env sign (env as Envir.Envir {iTs, ...}) =
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   200
  let
15794
5de27a5fc5ed Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15708
diff changeset
   201
    val pairs = Envir.alist_of env;
5de27a5fc5ed Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15708
diff changeset
   202
    val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2 o #2) pairs;
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   203
    val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
15794
5de27a5fc5ed Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15708
diff changeset
   204
    val cert = Thm.ctyp_of sign;
5de27a5fc5ed Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15708
diff changeset
   205
  in (map (fn (ixn, (S, T)) => (cert (TVar (ixn, S)), cert T)) (Vartab.dest iTs), xs ~~ ts) end;
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   206
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   207
fun divinate_inst rule i st =
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   208
  let
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   209
    val {sign, maxidx, ...} = Thm.rep_thm st;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   210
    val goal = List.nth (Thm.prems_of st, i - 1);  (*exception Subscript*)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   211
    val params = rev (rename_wrt_term goal (Logic.strip_params goal));  (*as they are printed :-*)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   212
  in
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   213
    if not (null params) then
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   214
      (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   215
        commas (map (Sign.string_of_term sign o Syntax.mark_boundT) params));
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   216
      Seq.single rule)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   217
    else
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   218
      let
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   219
        val rule' = Thm.incr_indexes (maxidx + 1) rule;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   220
        val concl = Logic.strip_assums_concl goal;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   221
      in
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   222
        Unify.smash_unifiers (sign, Envir.empty (#maxidx (Thm.rep_thm rule')),
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   223
          [(Thm.concl_of rule', concl)])
12162
7c74a52da110 proper handling of mutual rules (esp. for sets);
wenzelm
parents: 12053
diff changeset
   224
        |> Seq.map (fn env => Drule.instantiate (dest_env sign env) rule')
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   225
      end
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   226
  end handle Subscript => Seq.empty;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   227
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   228
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   229
(* compose tactics with cases *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   230
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   231
fun internalize k th = if k > 0 then internalize (k - 1) (imp_intr k th) else th;
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   232
13597
a8230e035e96 fixes !!-bound vars in induction statement automatically
nipkow
parents: 13425
diff changeset
   233
fun resolveq_cases_tac' make is_open ruleq i st =
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   234
  ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   235
    |> (Method.insert_tac more_facts THEN' atomize_tac) i
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   236
    |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   237
          st' |> Tactic.rtac rule' i
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   238
          |> Seq.map (rpair (make is_open (SOME (Thm.prop_of rule')) (rulified_term rule') cases)))
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   239
      |> Seq.flat)
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   240
    |> Seq.flat)
14404
4952c5a92e04 Transitive_Closure: added consumes and case_names attributes
nipkow
parents: 13597
diff changeset
   241
  |> Seq.flat;
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   242
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   243
infix 1 THEN_ALL_NEW_CASES;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   244
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   245
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   246
  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   247
    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   248
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   249
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   250
(* find rules *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   251
15235
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   252
(* rename all outermost !!-bound vars of type T in all premises of thm to x,
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   253
   possibly indexed to avoid clashes *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   254
fun rename [[SOME(Free(x,Type(T,_)))]] thm =
15235
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   255
  let
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   256
    fun index i [] = []
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   257
      | index i (y::ys) = if x=y then x^string_of_int i :: index (i+1) ys
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   258
                          else y :: index i ys;
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   259
    fun rename_params [] = []
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   260
      | rename_params ((y,Type(U,_))::ys) =
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   261
          (if U=T then x else y)::rename_params ys
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   262
      | rename_params ((y,_)::ys) = y::rename_params ys;
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   263
    fun rename_asm (A:term):term = 
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   264
      let val xs = rename_params (Logic.strip_params A)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   265
          val xs' = case List.filter (equal x) xs of
15235
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   266
                      [] => xs | [_] => xs | _ => index 1 xs
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   267
      in Logic.list_rename_params (xs',A) end;
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   268
    fun rename_prop (p:term) =
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   269
      let val (As,C) = Logic.strip_horn p
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   270
      in Logic.list_implies(map rename_asm As, C) end;
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   271
    val cp' = cterm_fun rename_prop (cprop_of thm);
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   272
    val thm' = equal_elim (reflexive cp') thm
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   273
  in Thm.put_name_tags (Thm.get_name_tags thm) thm' end
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   274
  | rename _ thm = thm;
614a804d7116 Induction now preserves the name of the induction variable.
nipkow
parents: 14981
diff changeset
   275
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   276
fun find_inductT ctxt insts =
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   277
  foldr multiply [[]] (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   278
    |> map (InductAttrib.find_inductT ctxt o fastype_of))
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   279
  |> map join_rules |> List.concat |> map (rename insts);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   280
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   281
fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   282
  | find_inductS _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   283
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   284
in
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   285
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   286
(* main tactic *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   287
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   288
fun induct_tac ctxt is_open insts opt_rule facts =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   289
  let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   290
    val sg = ProofContext.sign_of ctxt;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   291
    val cert = Thm.cterm_of sg;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   292
13105
3d1e7a199bdc use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents: 12852
diff changeset
   293
    fun rule_versions r = Seq.cons (r, Seq.filter (not o curry Thm.eq_thm r)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   294
        (Seq.make (fn () => SOME (localize r, Seq.empty))))
12168
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   295
      |> Seq.map (rpair (RuleCases.get r));
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   296
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   297
    val inst_rule = apfst (fn r =>
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   298
      if null insts then r
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   299
      else (align_right "Rule has fewer conclusions than arguments given"
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   300
          (Data.dest_concls (Thm.concl_of r)) insts
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   301
        |> (List.concat o map (prep_inst align_right cert (atomize_term sg)))
12168
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   302
        |> Drule.cterm_instantiate) r);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   303
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   304
    val ruleq =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   305
      (case opt_rule of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   306
        NONE =>
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   307
          let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
12168
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   308
            conditional (null rules) (fn () => error "Unable to figure out induct rule");
12053
7e2e84e503ce Method.trace ctxt;
wenzelm
parents: 11996
diff changeset
   309
            Method.trace ctxt rules;
12168
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   310
            rules |> Seq.THEN (Seq.of_list, Seq.THEN (rule_versions, Seq.try inst_rule))
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   311
          end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   312
      | SOME r => r |> Seq.THEN (rule_versions, Seq.single o inst_rule));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   313
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   314
    fun prep_rule (th, (cases, n)) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   315
      Seq.map (rpair (cases, n - length facts, Library.drop (n, facts)))
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   316
        (Method.multi_resolves (Library.take (n, facts)) [th]);
13597
a8230e035e96 fixes !!-bound vars in induction statement automatically
nipkow
parents: 13425
diff changeset
   317
    val tac = resolveq_cases_tac' RuleCases.make is_open (Seq.flat (Seq.map prep_rule ruleq));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   318
  in tac THEN_ALL_NEW_CASES rulify_tac end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   319
16391
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   320
val induct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo
65c8070844ea export cases_tac, induct_tac;
wenzelm
parents: 15794
diff changeset
   321
  (fn (ctxt, (is_open, (insts, opt_rule))) => induct_tac ctxt is_open insts opt_rule));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   322
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   323
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   324
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   325
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   326
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   327
(** concrete syntax **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   328
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   329
val openN = "open";
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   330
val ruleN = "rule";
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   331
val ofN = "of";
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   332
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   333
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   334
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   335
fun named_rule k arg get =
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   336
  Scan.lift (Args.$$$ k -- Args.colon) |-- arg :-- (fn name => Scan.peek (fn ctxt =>
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   337
    (case get ctxt name of SOME x => Scan.succeed x
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   338
    | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))) >> #2;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   339
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   340
fun rule get_type get_set =
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   341
  named_rule InductAttrib.typeN Args.local_tyname get_type ||
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   342
  named_rule InductAttrib.setN Args.local_const get_set ||
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   343
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   344
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   345
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   346
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   347
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   348
val kind_inst =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   349
  (Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || Args.$$$ ruleN || Args.$$$ ofN)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   350
    -- Args.colon;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   351
val term = Scan.unless (Scan.lift kind_inst) Args.local_term;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   352
val term_dummy = Scan.unless (Scan.lift kind_inst)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15235
diff changeset
   353
  (Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   354
13425
119ae829ad9b support for split assumptions in cases (hyps vs. prems);
wenzelm
parents: 13197
diff changeset
   355
val instss = Args.and_list (Scan.repeat term_dummy);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   356
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   357
in
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   358
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   359
val cases_args = Method.syntax (Args.mode openN -- (instss -- Scan.option cases_rule));
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   360
val induct_args = Method.syntax (Args.mode openN -- (instss -- Scan.option induct_rule));
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   361
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   362
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   363
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   364
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   365
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   366
(** theory setup **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   367
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   368
val setup =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   369
  [Method.add_methods
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   370
    [(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"),
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   371
     (InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")]];
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   372
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   373
end;
15708
ef7b74e52f11 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
   374