src/Provers/induct_method.ML
author wenzelm
Thu, 17 Jan 2002 21:02:18 +0100
changeset 12799 5472afdd3bd3
parent 12305 3c3f98b3d9e7
child 12852 c6a8e310aec5
permissions -rw-r--r--
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm; RuleCases.make interface based on term instead of thm;
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
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     5
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
     6
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
     7
*)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     8
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
     9
signature INDUCT_METHOD_DATA =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    10
sig
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    11
  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
    12
  val cases_default: thm
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
    13
  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
    14
  val conjI: thm
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    15
  val atomize: thm list
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    16
  val rulify1: thm list
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    17
  val rulify2: thm list
12240
0760eda193c4 induct method: localize rews for rule;
wenzelm
parents: 12168
diff changeset
    18
  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
    19
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    20
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    21
signature INDUCT_METHOD =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    22
sig
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    23
  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
    24
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    25
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    26
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
    27
struct
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
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    30
(** misc utils **)
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
(* align lists *)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    33
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    34
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
    35
  let val m = length xs and n = length ys
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    36
  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
    37
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    38
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
    39
  let val m = length xs and n = length ys
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    40
  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
    41
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    42
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    43
(* prep_inst *)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    44
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    45
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
    46
  let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    47
    fun prep_var (x, Some t) =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    48
          let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    49
            val cx = cert x;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    50
            val {T = xT, sign, ...} = Thm.rep_cterm cx;
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
    51
            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
    52
          in
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    53
            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
    54
            else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    55
             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    56
              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    57
              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
    58
          end
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    59
      | prep_var (_, None) = None;
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    60
    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
    61
  in
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    62
    align "Rule has fewer variables than instantiations given" xs ts
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    63
    |> mapfilter prep_var
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    64
  end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    65
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    66
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    67
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    68
(** cases method **)
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
(*
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    71
  rule selection scheme:
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    72
          cases         - classical case split
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    73
    <x:A> cases ...     - set cases
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    74
          cases t       - type cases
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    75
    ...   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
    76
*)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    77
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    78
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    79
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    80
fun resolveq_cases_tac make ruleq i st =
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    81
  ruleq |> Seq.map (fn (rule, (cases, facts)) =>
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    82
    (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
    83
    |> 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
    84
  |> Seq.flat;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
    85
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    86
fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    87
  | find_casesT _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    88
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    89
fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt fact
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    90
  | find_casesS _ _ = [];
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 cases_tac (ctxt, (open_parms, (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
    93
  let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
    94
    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
    95
    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
    96
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    97
    fun inst_rule r =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    98
      if null insts then RuleCases.add r
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
    99
      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   100
        |> (flat o map (prep_inst align_left cert I))
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   101
        |> 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
   102
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   103
    val ruleq =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   104
      (case (facts, insts, opt_rule) of
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   105
        ([], [], None) => Seq.single (RuleCases.add Data.cases_default)
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   106
      | (_, _, None) =>
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   107
          let val rules = find_casesS ctxt facts @ find_casesT ctxt insts in
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   108
            if null rules then error "Unable to figure out cases rule" else ();
12053
7e2e84e503ce Method.trace ctxt;
wenzelm
parents: 11996
diff changeset
   109
            Method.trace ctxt rules;
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   110
            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
   111
          end
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   112
      | (_, _, 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
   113
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   114
    fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   115
      (Method.multi_resolves (take (n, facts)) [th]);
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   116
  in resolveq_cases_tac (RuleCases.make open_parms) (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
   117
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   118
in
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   119
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   120
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   121
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   122
end;
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
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
(** induct method **)
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
(*
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   129
  rule selection scheme:
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   130
    <x:A> induct ...     - set induction
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   131
          induct x       - type induction
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   132
    ...   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
   133
*)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   134
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   135
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   136
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   137
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   138
(* atomize and rulify *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   139
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   140
fun atomize_term sg =
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   141
  ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize;
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   142
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   143
fun rulified_term thm =
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   144
  let val sg = Thm.sign_of_thm thm in
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   145
    Thm.prop_of thm
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   146
    |> MetaSimplifier.rewrite_term sg Data.rulify1
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   147
    |> MetaSimplifier.rewrite_term sg Data.rulify2
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   148
    |> pair sg
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   149
  end;
11756
8d8a87f350d6 use ObjectLogic stuff;
wenzelm
parents: 11735
diff changeset
   150
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   151
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
   152
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   153
val rulify_tac =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   154
  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
   155
  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
   156
  Tactic.norm_hhf_tac;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   157
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   158
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
   159
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   160
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   161
(* imp_intr --- limited to atomic prems *)
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   162
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   163
fun imp_intr i raw_th =
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   164
  let
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   165
    val th = Thm.permute_prems (i - 1) 1 raw_th;
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   166
    val cprems = Drule.cprems_of th;
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   167
    val As = take (length cprems - 1, cprems);
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   168
    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
   169
    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
   170
  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
   171
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   172
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   173
(* join multi-rules *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   174
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   175
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
   176
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   177
fun join_rules [] = []
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   178
  | join_rules [th] = [th]
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   179
  | join_rules (rules as r :: rs) =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   180
      if not (forall (eq_prems r) rs) then []
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   181
      else
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   182
        let
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   183
          val th :: ths = map Drule.freeze_all rules;
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   184
          val cprems = Drule.cprems_of th;
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   185
          val asms = map Thm.assume cprems;
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   186
        in
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   187
          [foldr1 (fn (x, x') => [x, x'] MRS Data.conjI)
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   188
            (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   189
          |> Drule.implies_intr_list cprems
12305
3c3f98b3d9e7 join_rules RuleCases.save;
wenzelm
parents: 12240
diff changeset
   190
          |> Drule.standard'
3c3f98b3d9e7 join_rules RuleCases.save;
wenzelm
parents: 12240
diff changeset
   191
          |> RuleCases.save th]
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   192
        end;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   193
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   194
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   195
(* divinate rule instantiation (cannot handle pending goal parameters) *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   196
11808
c724a9093ebe dest_env: norm_term on rhs;
wenzelm
parents: 11790
diff changeset
   197
fun dest_env sign (env as Envir.Envir {asol, iTs, ...}) =
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   198
  let
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   199
    val pairs = Vartab.dest asol;
11808
c724a9093ebe dest_env: norm_term on rhs;
wenzelm
parents: 11790
diff changeset
   200
    val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2) pairs;
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   201
    val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   202
  in (map (apsnd (Thm.ctyp_of sign)) (Vartab.dest iTs), xs ~~ ts) end;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   203
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   204
fun divinate_inst rule i st =
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   205
  let
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   206
    val {sign, maxidx, ...} = Thm.rep_thm st;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   207
    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
   208
    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
   209
  in
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   210
    if not (null params) then
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   211
      (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
   212
        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
   213
      Seq.single rule)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   214
    else
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   215
      let
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   216
        val rule' = Thm.incr_indexes (maxidx + 1) rule;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   217
        val concl = Logic.strip_assums_concl goal;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   218
      in
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   219
        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
   220
          [(Thm.concl_of rule', concl)])
12162
7c74a52da110 proper handling of mutual rules (esp. for sets);
wenzelm
parents: 12053
diff changeset
   221
        |> 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
   222
      end
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   223
  end handle Subscript => Seq.empty;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   224
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   225
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   226
(* compose tactics with cases *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   227
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   228
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
   229
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   230
fun resolveq_cases_tac' make ruleq i st =
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   231
  ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   232
    |> (Method.insert_tac more_facts THEN' atomize_tac) i
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   233
    |> 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
   234
          st' |> Tactic.rtac rule' i
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   235
          |> Seq.map (rpair (make (rulified_term rule') cases)))
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   236
      |> Seq.flat)
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   237
    |> Seq.flat)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   238
  |> Seq.flat;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   239
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   240
infix 1 THEN_ALL_NEW_CASES;
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   241
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   242
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
   243
  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   244
    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
   245
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   246
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   247
(* find rules *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   248
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   249
fun find_inductT ctxt insts =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   250
  foldr multiply (insts |> mapfilter (fn [] => None | ts => last_elem ts)
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   251
    |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   252
  |> map join_rules |> flat;
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   253
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   254
fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   255
  | find_inductS _ _ = [];
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   256
11790
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   257
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   258
(* main tactic *)
42393a11642d simplified resolveq_cases_tac for cases, separate version for induct;
wenzelm
parents: 11781
diff changeset
   259
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   260
fun induct_tac (ctxt, (open_parms, (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
   261
  let
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   262
    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
   263
    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
   264
12168
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   265
    fun rule_versions r = Seq.cons (r, Seq.filter (not o curry eq_thm r)
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   266
        (Seq.make (fn () => Some (localize r, Seq.empty))))
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   267
      |> Seq.map (rpair (RuleCases.get r));
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   268
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   269
    val inst_rule = apfst (fn r =>
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   270
      if null insts then r
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   271
      else (align_right "Rule has fewer conclusions than arguments given"
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   272
          (Data.dest_concls (Thm.concl_of r)) insts
12799
5472afdd3bd3 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents: 12305
diff changeset
   273
        |> (flat o map (prep_inst align_right cert (atomize_term sg)))
12168
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   274
        |> 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
   275
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   276
    val ruleq =
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   277
      (case opt_rule of
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   278
        None =>
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   279
          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
   280
            conditional (null rules) (fn () => error "Unable to figure out induct rule");
12053
7e2e84e503ce Method.trace ctxt;
wenzelm
parents: 11996
diff changeset
   281
            Method.trace ctxt rules;
12168
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   282
            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
   283
          end
12168
dc93c2e82205 induct: rule_versions produces localized variants;
wenzelm
parents: 12162
diff changeset
   284
      | 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
   285
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   286
    fun prep_rule (th, (cases, n)) =
11996
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   287
      Seq.map (rpair (cases, n - length facts, drop (n, facts)))
b409a8cbe1fb induct: internalize ``missing'' consumes-facts from goal state
wenzelm
parents: 11984
diff changeset
   288
        (Method.multi_resolves (take (n, facts)) [th]);
11984
324f69149895 induct: cases are extracted from rulified rule;
wenzelm
parents: 11808
diff changeset
   289
    val tac = resolveq_cases_tac' (RuleCases.make open_parms) (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
   290
  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
   291
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   292
in
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   293
12162
7c74a52da110 proper handling of mutual rules (esp. for sets);
wenzelm
parents: 12053
diff changeset
   294
val induct_meth = Method.RAW_METHOD_CASES o (HEADGOAL oo induct_tac);
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   295
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   296
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   297
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   298
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   299
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   300
(** concrete syntax **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   301
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   302
val openN = "open";
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   303
val ruleN = "rule";
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   304
val ofN = "of";
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   305
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   306
local
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   307
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   308
fun check k get name =
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   309
  (case get name of Some x => x
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   310
  | None => error ("No rule for " ^ k ^ " " ^ quote name));
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   311
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   312
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   313
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   314
fun rule get_type get_set =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   315
  Scan.depend (fn ctxt =>
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   316
    let val sg = ProofContext.sign_of ctxt in
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   317
      spec InductAttrib.typeN >> (check InductAttrib.typeN (get_type ctxt) o
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   318
        Sign.certify_tyname sg o Sign.intern_tycon sg) ||
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   319
      spec InductAttrib.setN >> (check InductAttrib.setN (get_set ctxt) o
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   320
        Sign.certify_const sg o Sign.intern_const sg)
11670
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   321
    end >> pair ctxt) ||
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   322
  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
   323
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   324
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
   325
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
   326
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   327
val kind_inst =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   328
  (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
   329
    -- Args.colon;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   330
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
   331
val term_dummy = Scan.unless (Scan.lift kind_inst)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   332
  (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   333
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   334
val instss = Args.and_list (Scan.repeat1 term_dummy);
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   335
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   336
in
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   337
11735
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   338
val cases_args = Method.syntax (Args.mode openN -- (instss -- Scan.option cases_rule));
60c0fa10bfc2 removed vars_of, concls_of;
wenzelm
parents: 11670
diff changeset
   339
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
   340
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   341
end;
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   342
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   343
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
(** theory setup **)
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   346
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   347
val setup =
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   348
  [Method.add_methods
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   349
    [(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
   350
     (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
   351
59f79df42d1f proof by cases and induction on types and sets (used to be specific for HOL);
wenzelm
parents:
diff changeset
   352
end;