src/HOL/Tools/induct_method.ML
author wenzelm
Fri, 02 Feb 2001 22:19:52 +0100
changeset 11035 bad7568e76e0
parent 10871 0ff9caa810b1
permissions -rw-r--r--
use hol_rewrite_cterm;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/induct_method.ML
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9230
wenzelm
parents: 9066
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     5
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
     6
Proof by cases and induction on types and sets.
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     7
*)
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     8
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
     9
signature INDUCT_METHOD =
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    10
sig
8431
e5f8ee756a8a export vars_of;
wenzelm
parents: 8400
diff changeset
    11
  val vars_of: term -> term list
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
    12
  val concls_of: thm -> term list
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
    13
  val simp_case_tac: bool -> simpset -> int -> tactic
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    14
  val setup: (theory -> theory) list
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    15
end;
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    16
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    17
structure InductMethod: INDUCT_METHOD =
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    18
struct
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
    19
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    20
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    21
(** theory context references **)
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    22
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    23
val inductive_atomize = thms "inductive_atomize";
10439
be2dc95dfe98 inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents: 10409
diff changeset
    24
val inductive_rulify1 = thms "inductive_rulify1";
be2dc95dfe98 inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents: 10409
diff changeset
    25
val inductive_rulify2 = thms "inductive_rulify2";
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    26
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    27
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    28
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    29
(** misc utils **)
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
    30
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    31
(* align lists *)
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    32
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    33
fun align_left msg xs ys =
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    34
  let val m = length xs and n = length ys
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    35
  in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    36
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    37
fun align_right msg xs ys =
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    38
  let val m = length xs and n = length ys
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    39
  in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    40
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    41
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
    42
(* thms and terms *)
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
    43
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
    44
fun imp_concl_of t = imp_concl_of (#2 (HOLogic.dest_imp t)) handle TERM _ => t;
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
    45
val concls_of = map imp_concl_of o HOLogic.dest_conj o HOLogic.dest_Trueprop o Thm.concl_of;
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
    46
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
    47
fun vars_of tm =        (*ordered left-to-right, preferring right!*)
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    48
  Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
    49
  |> Library.distinct |> rev;
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
    50
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    51
fun type_name t =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
    52
  #1 (Term.dest_Type (Term.type_of t))
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    53
    handle TYPE _ => raise TERM ("Type of term argument is too general", [t]);
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    54
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    55
fun prep_inst align cert f (tm, ts) =
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    56
  let
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    57
    fun prep_var (x, Some t) =
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    58
          let
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    59
            val cx = cert x;
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    60
            val {T = xT, sign, ...} = Thm.rep_cterm cx;
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    61
            val orig_ct = cert t;
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    62
            val ct = f orig_ct;
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    63
          in
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    64
            if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct)
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    65
            else error (Pretty.string_of (Pretty.block
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    66
              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    67
                Display.pretty_cterm orig_ct, Pretty.str " ::", Pretty.brk 1,
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    68
                Display.pretty_ctyp (#T (Thm.crep_cterm orig_ct))]))
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    69
          end
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    70
      | prep_var (_, None) = None;
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    71
  in
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    72
    align "Rule has fewer variables than instantiations given" (vars_of tm) ts
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    73
    |> mapfilter prep_var
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
    74
  end;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
    75
10728
13cb6d29f7ff export rewrite_cterm;
wenzelm
parents: 10542
diff changeset
    76
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
    77
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    78
(* simplifying cases rules *)
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    79
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    80
local
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    81
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    82
(*delete needless equality assumptions*)
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
    83
val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    84
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    85
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    86
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    87
in
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    88
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
    89
fun simp_case_tac solved ss i =
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
    90
  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
    91
  THEN_MAYBE (if solved then no_tac else all_tac);
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    92
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    93
end;
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    94
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
    95
10542
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
    96
(* resolution and cases *)
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
    97
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
    98
local
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
    99
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   100
fun gen_resolveq_tac tac rules i st =
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   101
  Seq.flat (Seq.map (fn rule => tac rule i st) rules);
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   102
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   103
in
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   104
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   105
fun resolveq_cases_tac make tac = gen_resolveq_tac (fn (rule, (cases, facts)) => fn i => fn st =>
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   106
  Seq.map (rpair (make rule cases))
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   107
    ((Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st));
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   108
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   109
end;
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   110
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   111
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   112
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   113
(** cases method **)
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   114
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   115
(*
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   116
  rule selection:
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   117
        cases         - classical case split
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   118
        cases t       - datatype exhaustion
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   119
  <x:A> cases ...     - set elimination
8451
614f18139d47 tuned comments;
wenzelm
parents: 8431
diff changeset
   120
  ...   cases ... R   - explicit rule
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   121
*)
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   122
9066
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8815
diff changeset
   123
val case_split = RuleCases.name ["True", "False"] case_split_thm;
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8815
diff changeset
   124
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   125
local
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   126
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   127
fun simplified_cases ctxt cases thm =
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   128
  let
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   129
    val nprems = Thm.nprems_of thm;
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   130
    val opt_cases =
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   131
      Library.replicate (nprems - Int.min (nprems, length cases)) None @
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   132
      map Some (Library.take (nprems, cases));
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   133
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   134
    val tac = simp_case_tac true (Simplifier.get_local_simpset ctxt);
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   135
    fun simp ((i, c), (th, cs)) =
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   136
      (case try (Tactic.rule_by_tactic (tac i)) th of
9313
b5a29408dc39 fixed simplified_cases;
wenzelm
parents: 9299
diff changeset
   137
        None => (th, c :: cs)
b5a29408dc39 fixed simplified_cases;
wenzelm
parents: 9299
diff changeset
   138
      | Some th' => (th', None :: cs));
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   139
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   140
    val (thm', opt_cases') = foldr simp (1 upto Thm.nprems_of thm ~~ opt_cases, (thm, []));
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   141
  in (thm', mapfilter I opt_cases') end;
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   142
9624
de254f375477 changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents: 9597
diff changeset
   143
fun cases_tac (ctxt, ((simplified, open_parms), args)) facts =
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   144
  let
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   145
    val sg = ProofContext.sign_of ctxt;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   146
    val cert = Thm.cterm_of sg;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   147
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   148
    fun inst_rule insts thm =
9914
67e9b7239548 case args: align_right;
wenzelm
parents: 9893
diff changeset
   149
      (align_left "Rule has fewer premises than arguments given" (Thm.prems_of thm) insts
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   150
        |> (flat o map (prep_inst align_left cert I))
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   151
        |> Drule.cterm_instantiate) thm;
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   152
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   153
    fun find_cases th =
10271
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   154
      NetRules.may_unify (#2 (InductAttrib.get_cases ctxt))
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   155
        (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   156
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   157
    val rules =
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   158
      (case (fst args, facts) of
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   159
        (([], None), []) => [RuleCases.add case_split]
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   160
      | ((insts, None), []) =>
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   161
          let
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   162
            val name = type_name (hd (flat (map (mapfilter I) insts)))
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   163
              handle Library.LIST _ => error "Unable to figure out type cases rule"
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   164
          in
10271
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   165
            (case InductAttrib.lookup_casesT ctxt name of
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   166
              None => error ("No cases rule for type: " ^ quote name)
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   167
            | Some thm => [(inst_rule insts thm, RuleCases.get thm)])
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   168
          end
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   169
      | (([], None), th :: _) => map (RuleCases.add o #2) (find_cases th)
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   170
      | ((insts, None), th :: _) =>
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   171
          (case find_cases th of        (*may instantiate first rule only!*)
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   172
            (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   173
          | [] => [])
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   174
      | (([], Some thm), _) => [RuleCases.add thm]
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   175
      | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)])
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   176
      |> map (Library.apfst (Attrib.read_inst' (snd args) ctxt));
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   177
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   178
    val cond_simp = if simplified then simplified_cases ctxt else rpair;
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   179
10527
7934b0fa8dcc consume facts;
wenzelm
parents: 10455
diff changeset
   180
    fun prep_rule (thm, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o cond_simp cases)
7934b0fa8dcc consume facts;
wenzelm
parents: 10455
diff changeset
   181
      (Method.multi_resolves (take (n, facts)) [thm]);
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   182
  in
10542
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   183
    resolveq_cases_tac (RuleCases.make open_parms) (K all_tac)
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   184
      (Seq.flat (Seq.map prep_rule (Seq.of_list rules)))
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   185
  end;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   186
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   187
in
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   188
8671
6ce91a80f616 HEADGOAL;
wenzelm
parents: 8540
diff changeset
   189
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   190
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   191
end;
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   192
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   193
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   194
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   195
(** induct method **)
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   196
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   197
(*
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   198
  rule selection:
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   199
        induct x       - datatype induction
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   200
  <x:A> induct ...     - set induction
8451
614f18139d47 tuned comments;
wenzelm
parents: 8431
diff changeset
   201
  ...   induct ... R   - explicit rule
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   202
*)
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   203
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   204
local
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   205
11035
bad7568e76e0 use hol_rewrite_cterm;
wenzelm
parents: 10871
diff changeset
   206
val atomize_cterm = Thm.cterm_fun AutoBind.drop_judgment o hol_rewrite_cterm inductive_atomize;
10439
be2dc95dfe98 inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents: 10409
diff changeset
   207
val atomize_tac = Tactic.rewrite_goal_tac inductive_atomize;
11035
bad7568e76e0 use hol_rewrite_cterm;
wenzelm
parents: 10871
diff changeset
   208
val rulify_cterm = hol_rewrite_cterm inductive_rulify2 o hol_rewrite_cterm inductive_rulify1;
10439
be2dc95dfe98 inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents: 10409
diff changeset
   209
be2dc95dfe98 inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents: 10409
diff changeset
   210
val rulify_tac =
be2dc95dfe98 inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents: 10409
diff changeset
   211
  Tactic.rewrite_goal_tac inductive_rulify1 THEN'
be2dc95dfe98 inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents: 10409
diff changeset
   212
  Tactic.rewrite_goal_tac inductive_rulify2 THEN'
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   213
  Tactic.norm_hhf_tac;
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   214
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   215
fun rulify_cases cert =
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   216
  let
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   217
    val ruly = Thm.term_of o rulify_cterm o cert;
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   218
    fun ruly_case {fixes, assumes, binds} =
10814
2ccc84b8f5a0 case binds: AutoBind.drop_judgment;
wenzelm
parents: 10803
diff changeset
   219
      {fixes = fixes, assumes = map ruly assumes,
2ccc84b8f5a0 case binds: AutoBind.drop_judgment;
wenzelm
parents: 10803
diff changeset
   220
        binds = map (apsnd (apsome (AutoBind.drop_judgment o ruly))) binds};
10871
0ff9caa810b1 induct cases: RuleCases.make_raw;
wenzelm
parents: 10814
diff changeset
   221
  in map (apsnd ruly_case) ooo RuleCases.make_raw end;
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   222
10455
acfdc430f4cd removed warning for "stripped" option;
wenzelm
parents: 10439
diff changeset
   223
val weak_strip_tac = REPEAT o Tactic.match_tac [impI, allI, ballI];
acfdc430f4cd removed warning for "stripped" option;
wenzelm
parents: 10439
diff changeset
   224
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   225
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   226
infix 1 THEN_ALL_NEW_CASES;
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   227
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   228
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   229
  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
8540
3a45bc1ff175 tuned degenerate cases / induct;
wenzelm
parents: 8451
diff changeset
   230
    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   231
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   232
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   233
fun induct_rule ctxt t =
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   234
  let val name = type_name t in
10271
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   235
    (case InductAttrib.lookup_inductT ctxt name of
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   236
      None => error ("No induct rule for type: " ^ quote name)
8332
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   237
    | Some thm => (name, thm))
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   238
  end;
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   239
8332
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   240
fun join_rules [(_, thm)] = thm
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   241
  | join_rules raw_thms =
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   242
      let
8332
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   243
        val thms = (map (apsnd Drule.freeze_all) raw_thms);
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   244
        fun eq_prems ((_, th1), (_, th2)) =
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   245
          Term.aconvs (Thm.prems_of th1, Thm.prems_of th2);
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   246
      in
8332
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   247
        (case Library.gen_distinct eq_prems thms of
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   248
          [(_, thm)] =>
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   249
            let
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   250
              val cprems = Drule.cprems_of thm;
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   251
              val asms = map Thm.assume cprems;
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   252
              fun strip (_, th) = Drule.implies_elim_list th asms;
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   253
            in
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   254
              foldr1 (fn (th, th') => [th, th'] MRS conjI) (map strip thms)
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   255
              |> Drule.implies_intr_list cprems
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   256
              |> Drule.standard
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   257
            end
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   258
        | [] => error "No rule given"
88fe0f1a480f join_rules: compatibility check;
wenzelm
parents: 8330
diff changeset
   259
        | bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads)))
8330
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   260
      end;
c411706dc503 join induct rules;
wenzelm
parents: 8315
diff changeset
   261
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   262
9624
de254f375477 changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents: 9597
diff changeset
   263
fun induct_tac (ctxt, ((stripped, open_parms), args)) facts =
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   264
  let
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   265
    val sg = ProofContext.sign_of ctxt;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   266
    val cert = Thm.cterm_of sg;
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   267
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   268
    fun inst_rule insts thm =
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   269
      (align_right "Rule has fewer conclusions than arguments given" (concls_of thm) insts
10409
10a1b95ce642 method 'induct' now handles non-atomic goals;
wenzelm
parents: 10271
diff changeset
   270
        |> (flat o map (prep_inst align_right cert atomize_cterm))
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   271
        |> Drule.cterm_instantiate) thm;
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   272
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   273
    fun find_induct th =
10271
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   274
      NetRules.may_unify (#2 (InductAttrib.get_induct ctxt))
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   275
        (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   276
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   277
    val rules =
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   278
      (case (fst args, facts) of
8540
3a45bc1ff175 tuned degenerate cases / induct;
wenzelm
parents: 8451
diff changeset
   279
        (([], None), []) => []
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   280
      | ((insts, None), []) =>
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   281
          let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   282
            handle Library.LIST _ => error "Unable to figure out type induction rule"
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   283
          in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   284
      | (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th)
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   285
      | ((insts, None), th :: _) =>
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   286
          (case find_induct th of       (*may instantiate first rule only!*)
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   287
            (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   288
          | [] => [])
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   289
      | (([], Some thm), _) => [RuleCases.add thm]
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   290
      | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)])
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   291
      |> map (Library.apfst (Attrib.read_inst' (snd args) ctxt));
8376
f5628700ab9a added dest_global/local_rules;
wenzelm
parents: 8344
diff changeset
   292
10527
7934b0fa8dcc consume facts;
wenzelm
parents: 10455
diff changeset
   293
    fun prep_rule (thm, (cases, n)) =
7934b0fa8dcc consume facts;
wenzelm
parents: 10455
diff changeset
   294
      Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [thm]);
10542
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   295
    val tac = resolveq_cases_tac (rulify_cases cert open_parms) atomize_tac
9624
de254f375477 changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents: 9597
diff changeset
   296
      (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   297
  in
10542
92cd56dfc17e resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents: 10527
diff changeset
   298
    tac THEN_ALL_NEW_CASES (rulify_tac THEN' (if stripped then weak_strip_tac else K all_tac))
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   299
  end;
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   300
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   301
in
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   302
8671
6ce91a80f616 HEADGOAL;
wenzelm
parents: 8540
diff changeset
   303
val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac);
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   304
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   305
end;
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   306
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   307
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   308
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   309
(** concrete syntax **)
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   310
8337
5b6430edf06d added con_elim_s(olved_)tac;
wenzelm
parents: 8332
diff changeset
   311
val simplifiedN = "simplified";
8344
4417e588d9f7 induct: "stripped" option;
wenzelm
parents: 8337
diff changeset
   312
val strippedN = "stripped";
9624
de254f375477 changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents: 9597
diff changeset
   313
val openN = "open";
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   314
val ruleN = "rule";
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   315
val ofN = "of";
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   316
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   317
local
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   318
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   319
fun err k get name =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   320
  (case get name of Some x => x
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   321
  | None => error ("No rule for " ^ k ^ " " ^ quote name));
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   322
10271
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   323
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   324
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   325
fun rule get_type get_set =
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   326
  Scan.depend (fn ctxt =>
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   327
    let val sg = ProofContext.sign_of ctxt in
10271
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   328
      spec InductAttrib.typeN >> (err InductAttrib.typeN (get_type ctxt) o Sign.intern_tycon sg) ||
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   329
      spec InductAttrib.setN >> (err InductAttrib.setN (get_set ctxt) o Sign.intern_const sg)
8308
45e11d3ccbe4 cases/induct attributes;
wenzelm
parents: 8295
diff changeset
   330
    end >> pair ctxt) ||
8815
187547eae4c5 use Args.colon / Args.parens;
wenzelm
parents: 8695
diff changeset
   331
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   332
10271
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   333
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS;
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   334
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   335
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   336
val kind_inst =
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   337
  (Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || Args.$$$ ruleN || Args.$$$ ofN)
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   338
    -- Args.colon;
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   339
val term = Scan.unless (Scan.lift kind_inst) Args.local_term;
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   340
val term_dummy = Scan.unless (Scan.lift kind_inst)
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   341
  (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
6446
583add9799c3 may specify induction predicates as well;
wenzelm
parents: 6442
diff changeset
   342
9597
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   343
val instss = Args.and_list (Scan.repeat1 term_dummy);
938a99cc55f7 cases: support multiple insts;
wenzelm
parents: 9313
diff changeset
   344
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   345
(* FIXME Attrib.insts': better use actual term args *)
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   346
val rule_insts =
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   347
  Scan.lift (Scan.optional ((Args.$$$ ofN -- Args.colon) |-- Args.!!! Attrib.insts') ([], []));
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   348
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   349
in
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   350
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   351
val cases_args = Method.syntax
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   352
  (Args.mode simplifiedN -- Args.mode openN -- (instss -- Scan.option cases_rule -- rule_insts));
9299
c5cda71de65d added simp_case_tac;
wenzelm
parents: 9230
diff changeset
   353
8695
850e84526745 export concl_of;
wenzelm
parents: 8688
diff changeset
   354
val induct_args = Method.syntax
10803
bdc3aa1c193b 'of:' params spec;
wenzelm
parents: 10728
diff changeset
   355
  (Args.mode strippedN -- Args.mode openN -- (instss -- Scan.option induct_rule -- rule_insts));
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   356
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   357
end;
6446
583add9799c3 may specify induction predicates as well;
wenzelm
parents: 6442
diff changeset
   358
583add9799c3 may specify induction predicates as well;
wenzelm
parents: 6442
diff changeset
   359
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   360
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   361
(** theory setup **)
6446
583add9799c3 may specify induction predicates as well;
wenzelm
parents: 6442
diff changeset
   362
8278
5928c72b7057 induct: tuned syntax;
wenzelm
parents: 8154
diff changeset
   363
val setup =
10271
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   364
  [Method.add_methods
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   365
    [(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"),
45b996639c45 split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents: 10013
diff changeset
   366
     (InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")],
9066
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8815
diff changeset
   367
   (#1 o PureThy.add_thms [(("case_split", case_split), [])])];
6442
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   368
6a95ceaa977e Proof by induction on types / set / functions.
wenzelm
parents:
diff changeset
   369
end;