src/Tools/induct_tacs.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46849 36f392239b6a
child 48992 0518bf89c777
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28308
d4396a28fb29 fixed headers
haftmann
parents: 27882
diff changeset
     1
(*  Title:      Tools/induct_tacs.ML
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
     3
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
     4
Unstructured induction and cases analysis.
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
     5
*)
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
     6
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
     7
signature INDUCT_TACS =
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
     8
sig
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
     9
  val case_tac: Proof.context -> string -> int -> tactic
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    10
  val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    11
  val induct_tac: Proof.context -> string option list list -> int -> tactic
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    12
  val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    13
  val setup: theory -> theory
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    14
end
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    15
45133
2214ba5bdfff modernized structure Induct_Tacs;
wenzelm
parents: 42361
diff changeset
    16
structure Induct_Tacs: INDUCT_TACS =
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    17
struct
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    18
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    19
(* case analysis *)
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    20
46836
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    21
fun check_type ctxt (t, pos) =
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    22
  let
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    23
    val u = singleton (Variable.polymorphic ctxt) t;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    24
    val U = Term.fastype_of u;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    25
    val _ = Term.is_TVar U andalso
46836
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    26
      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.str_of pos);
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    27
  in (u, U) end;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    28
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
    29
fun gen_case_tac ctxt0 s opt_rule i st =
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    30
  let
32863
5e8cef567042 eliminated dead code;
wenzelm
parents: 30541
diff changeset
    31
    val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    32
    val rule =
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    33
      (case opt_rule of
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    34
        SOME rule => rule
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    35
      | NONE =>
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    36
          (case Induct.find_casesT ctxt
46836
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    37
              (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s,
46849
36f392239b6a tuned signature;
wenzelm
parents: 46836
diff changeset
    38
                Syntax.read_token_pos s))) of
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    39
            rule :: _ => rule
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    40
          | [] => @{thm case_split}));
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    41
    val _ = Method.trace ctxt [rule];
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    42
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    43
    val xi =
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    44
      (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    45
        Var (xi, _) :: _ => xi
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    46
      | _ => raise THM ("Malformed cases rule", 0, [rule]));
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    47
  in res_inst_tac ctxt [(xi, s)] rule i st end
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    48
  handle THM _ => Seq.empty;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    49
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
    50
fun case_tac ctxt s = gen_case_tac ctxt s NONE;
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
    51
fun case_rule_tac ctxt s rule = gen_case_tac ctxt s (SOME rule);
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    52
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    53
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    54
(* induction *)
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    55
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    56
local
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    57
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    58
fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    59
  | prep_var _ = NONE;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    60
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    61
fun prep_inst (concl, xs) =
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    62
  let val vs = Induct.vars_of concl
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
    63
  in map_filter prep_var (drop (length vs - length xs) vs ~~ xs) end;
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    64
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    65
in
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    66
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
    67
fun gen_induct_tac ctxt0 varss opt_rules i st =
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    68
  let
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    69
    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    70
    val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    71
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    72
    fun induct_var name =
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    73
      let
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    74
        val t = Syntax.read_term ctxt name;
46849
36f392239b6a tuned signature;
wenzelm
parents: 46836
diff changeset
    75
        val pos = Syntax.read_token_pos name;
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    76
        val (x, _) = Term.dest_Free t handle TERM _ =>
46836
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    77
          error ("Induction argument not a variable: " ^
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    78
            Syntax.string_of_term ctxt t ^ Position.str_of pos);
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    79
        val eq_x = fn Free (y, _) => x = y | _ => false;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    80
        val _ =
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    81
          if Term.exists_subterm eq_x concl then ()
46836
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    82
          else
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    83
            error ("No such variable in subgoal: " ^
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    84
              Syntax.string_of_term ctxt t ^ Position.str_of pos);
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    85
        val _ =
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    86
          if (exists o Term.exists_subterm) eq_x prems then
46836
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    87
            warning ("Induction variable occurs also among premises: " ^
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    88
              Syntax.string_of_term ctxt t ^ Position.str_of pos)
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    89
          else ();
46836
58490158cd74 more precise warning/error positions;
wenzelm
parents: 45133
diff changeset
    90
      in #1 (check_type ctxt (t, pos)) end;
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    91
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    92
    val argss = map (map (Option.map induct_var)) varss;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    93
    val rule =
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    94
      (case opt_rules of
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32863
diff changeset
    95
        SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    96
      | NONE =>
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32863
diff changeset
    97
          (case map_filter (Rule_Cases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    98
            (_, rule) :: _ => rule
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
    99
          | [] => raise THM ("No induction rules", 0, [])));
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   100
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 33957
diff changeset
   101
    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   102
    val _ = Method.trace ctxt [rule'];
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   103
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   104
    val concls = Logic.dest_conjunctions (Thm.concl_of rule);
40722
441260986b63 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents: 36960
diff changeset
   105
    val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   106
      error "Induction rule has different numbers of variables";
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   107
  in res_inst_tac ctxt insts rule' i st end
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   108
  handle THM _ => Seq.empty;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   109
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   110
end;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   111
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   112
fun induct_tac ctxt args = gen_induct_tac ctxt args NONE;
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   113
fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt args (SOME rules);
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   114
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   115
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   116
(* method syntax *)
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   117
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   118
local
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   119
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   120
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   121
val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   122
val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   123
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   124
val varss =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 35625
diff changeset
   125
  Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   126
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   127
in
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   128
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   129
val setup =
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   130
  Method.setup @{binding case_tac}
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   131
    (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   132
      (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   133
    "unstructured case analysis on types" #>
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   134
  Method.setup @{binding induct_tac}
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   135
    (Args.goal_spec -- varss -- opt_rules >>
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   136
      (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
9f168bdc468a simplified method setup;
wenzelm
parents: 30161
diff changeset
   137
    "unstructured induction on types";
27326
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   138
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   139
end;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   140
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   141
end;
d3beec370964 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
wenzelm
parents:
diff changeset
   142