src/HOL/Tools/induct_method.ML
author wenzelm
Sat Jul 01 19:55:22 2000 +0200 (2000-07-01)
changeset 9230 17ae63f82ad8
parent 9066 b1e874e38dab
child 9299 c5cda71de65d
permissions -rw-r--r--
GPLed;
wenzelm@6442
     1
(*  Title:      HOL/Tools/induct_method.ML
wenzelm@6442
     2
    ID:         $Id$
wenzelm@6442
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9230
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6442
     5
wenzelm@8376
     6
Proof by cases and induction on types and sets.
wenzelm@6442
     7
*)
wenzelm@6442
     8
wenzelm@6442
     9
signature INDUCT_METHOD =
wenzelm@6442
    10
sig
wenzelm@8376
    11
  val dest_global_rules: theory ->
wenzelm@8376
    12
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
wenzelm@8376
    13
      type_induct: (string * thm) list, set_induct: (string * thm) list}
wenzelm@8308
    14
  val print_global_rules: theory -> unit
wenzelm@8376
    15
  val dest_local_rules: Proof.context ->
wenzelm@8376
    16
    {type_cases: (string * thm) list, set_cases: (string * thm) list,
wenzelm@8376
    17
      type_induct: (string * thm) list, set_induct: (string * thm) list}
wenzelm@8308
    18
  val print_local_rules: Proof.context -> unit
wenzelm@8431
    19
  val vars_of: term -> term list
wenzelm@8695
    20
  val concls_of: thm -> term list
wenzelm@8308
    21
  val cases_type_global: string -> theory attribute
wenzelm@8308
    22
  val cases_set_global: string -> theory attribute
wenzelm@8308
    23
  val cases_type_local: string -> Proof.context attribute
wenzelm@8308
    24
  val cases_set_local: string -> Proof.context attribute
wenzelm@8308
    25
  val induct_type_global: string -> theory attribute
wenzelm@8308
    26
  val induct_set_global: string -> theory attribute
wenzelm@8308
    27
  val induct_type_local: string -> Proof.context attribute
wenzelm@8308
    28
  val induct_set_local: string -> Proof.context attribute
wenzelm@8337
    29
  val con_elim_tac: simpset -> tactic
wenzelm@8337
    30
  val con_elim_solved_tac: simpset -> tactic
wenzelm@6442
    31
  val setup: (theory -> theory) list
wenzelm@6442
    32
end;
wenzelm@6442
    33
wenzelm@6442
    34
structure InductMethod: INDUCT_METHOD =
wenzelm@6442
    35
struct
wenzelm@6442
    36
wenzelm@8337
    37
wenzelm@8308
    38
(** global and local induct data **)
wenzelm@6442
    39
wenzelm@8308
    40
(* rules *)
wenzelm@8308
    41
wenzelm@8308
    42
type rules = (string * thm) NetRules.T;
wenzelm@8308
    43
wenzelm@8308
    44
fun eq_rule ((s1:string, th1), (s2, th2)) = s1 = s2 andalso Thm.eq_thm (th1, th2);
wenzelm@8308
    45
wenzelm@8308
    46
val type_rules = NetRules.init eq_rule (Thm.concl_of o #2);
wenzelm@8308
    47
val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2);
wenzelm@8308
    48
wenzelm@8308
    49
fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name);
wenzelm@8308
    50
wenzelm@8308
    51
fun print_rules kind rs =
wenzelm@8308
    52
  let val thms = map snd (NetRules.rules rs)
wenzelm@8315
    53
  in Pretty.writeln (Pretty.big_list kind (map Display.pretty_thm thms)) end;
wenzelm@8308
    54
wenzelm@8308
    55
wenzelm@8308
    56
(* theory data kind 'HOL/induct_method' *)
wenzelm@8308
    57
wenzelm@8308
    58
structure GlobalInductArgs =
wenzelm@8308
    59
struct
wenzelm@8308
    60
  val name = "HOL/induct_method";
wenzelm@8308
    61
  type T = (rules * rules) * (rules * rules);
wenzelm@8308
    62
wenzelm@8308
    63
  val empty = ((type_rules, set_rules), (type_rules, set_rules));
wenzelm@8308
    64
  val copy = I;
wenzelm@8308
    65
  val prep_ext = I;
wenzelm@8308
    66
  fun merge (((casesT1, casesS1), (inductT1, inductS1)),
wenzelm@8308
    67
      ((casesT2, casesS2), (inductT2, inductS2))) =
wenzelm@8308
    68
    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
wenzelm@8308
    69
      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
wenzelm@8308
    70
wenzelm@8308
    71
  fun print _ ((casesT, casesS), (inductT, inductS)) =
wenzelm@8315
    72
    (print_rules "type cases:" casesT;
wenzelm@8315
    73
      print_rules "set cases:" casesS;
wenzelm@8315
    74
      print_rules "type induct:" inductT;
wenzelm@8315
    75
      print_rules "set induct:" inductS);
wenzelm@8376
    76
wenzelm@8376
    77
  fun dest ((casesT, casesS), (inductT, inductS)) =
wenzelm@8376
    78
    {type_cases = NetRules.rules casesT,
wenzelm@8376
    79
     set_cases = NetRules.rules casesS,
wenzelm@8376
    80
     type_induct = NetRules.rules inductT,
wenzelm@8376
    81
     set_induct = NetRules.rules inductS};
wenzelm@8308
    82
end;
wenzelm@8308
    83
wenzelm@8308
    84
structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
wenzelm@8308
    85
val print_global_rules = GlobalInduct.print;
wenzelm@8376
    86
val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
wenzelm@8308
    87
wenzelm@8308
    88
wenzelm@8308
    89
(* proof data kind 'HOL/induct_method' *)
wenzelm@8308
    90
wenzelm@8308
    91
structure LocalInductArgs =
wenzelm@8308
    92
struct
wenzelm@8308
    93
  val name = "HOL/induct_method";
wenzelm@8308
    94
  type T = GlobalInductArgs.T;
wenzelm@8278
    95
wenzelm@8308
    96
  fun init thy = GlobalInduct.get thy;
wenzelm@8308
    97
  fun print x = GlobalInductArgs.print x;
wenzelm@8308
    98
end;
wenzelm@8308
    99
wenzelm@8308
   100
structure LocalInduct = ProofDataFun(LocalInductArgs);
wenzelm@8308
   101
val print_local_rules = LocalInduct.print;
wenzelm@8376
   102
val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
wenzelm@8308
   103
wenzelm@8308
   104
wenzelm@8308
   105
(* access rules *)
wenzelm@8308
   106
wenzelm@8308
   107
val get_cases = #1 o LocalInduct.get;
wenzelm@8308
   108
val get_induct = #2 o LocalInduct.get;
wenzelm@8308
   109
wenzelm@8308
   110
val lookup_casesT = lookup_rule o #1 o get_cases;
wenzelm@8308
   111
val lookup_casesS = lookup_rule o #2 o get_cases;
wenzelm@8308
   112
val lookup_inductT = lookup_rule o #1 o get_induct;
wenzelm@8308
   113
val lookup_inductS = lookup_rule o #2 o get_induct;
wenzelm@8308
   114
wenzelm@8308
   115
wenzelm@8308
   116
wenzelm@8308
   117
(** attributes **)
wenzelm@8308
   118
wenzelm@8308
   119
local
wenzelm@8308
   120
wenzelm@8308
   121
fun mk_att f g name (x, thm) = (f (g (name, thm)) x, thm);
wenzelm@8308
   122
wenzelm@8308
   123
fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
wenzelm@8308
   124
fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
wenzelm@8308
   125
fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
wenzelm@8308
   126
fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
wenzelm@8308
   127
wenzelm@8308
   128
in
wenzelm@8308
   129
wenzelm@8308
   130
val cases_type_global = mk_att GlobalInduct.map add_casesT;
wenzelm@8308
   131
val cases_set_global = mk_att GlobalInduct.map add_casesS;
wenzelm@8308
   132
val induct_type_global = mk_att GlobalInduct.map add_inductT;
wenzelm@8308
   133
val induct_set_global = mk_att GlobalInduct.map add_inductS;
wenzelm@8308
   134
wenzelm@8308
   135
val cases_type_local = mk_att LocalInduct.map add_casesT;
wenzelm@8308
   136
val cases_set_local = mk_att LocalInduct.map add_casesS;
wenzelm@8308
   137
val induct_type_local = mk_att LocalInduct.map add_inductT;
wenzelm@8308
   138
val induct_set_local = mk_att LocalInduct.map add_inductS;
wenzelm@8308
   139
wenzelm@8308
   140
end;
wenzelm@8308
   141
wenzelm@8308
   142
wenzelm@8308
   143
wenzelm@8308
   144
(** misc utils **)
wenzelm@8278
   145
wenzelm@8695
   146
(* thms and terms *)
wenzelm@8695
   147
wenzelm@8695
   148
val concls_of = HOLogic.dest_conj o HOLogic.dest_Trueprop o Thm.concl_of;
wenzelm@8344
   149
wenzelm@8278
   150
fun vars_of tm =        (*ordered left-to-right, preferring right!*)
wenzelm@8308
   151
  Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
wenzelm@8278
   152
  |> Library.distinct |> rev;
wenzelm@8278
   153
wenzelm@8308
   154
fun type_name t =
wenzelm@8308
   155
  #1 (Term.dest_Type (Term.type_of t))
wenzelm@8308
   156
    handle TYPE _ => raise TERM ("Bad type of term argument", [t]);
wenzelm@8278
   157
wenzelm@8278
   158
wenzelm@8337
   159
(* simplifying cases rules *)
wenzelm@8337
   160
wenzelm@8337
   161
local
wenzelm@8337
   162
wenzelm@8337
   163
(*delete needless equality assumptions*)
wenzelm@8337
   164
val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
wenzelm@8337
   165
     (fn _ => [assume_tac 1]);
wenzelm@8337
   166
wenzelm@8337
   167
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
wenzelm@8337
   168
wenzelm@8337
   169
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
wenzelm@8337
   170
wenzelm@8337
   171
fun simp_case_tac ss = 
wenzelm@8337
   172
  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac];
wenzelm@8337
   173
wenzelm@8337
   174
in
wenzelm@8337
   175
wenzelm@8337
   176
fun con_elim_tac ss = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
wenzelm@8337
   177
wenzelm@8337
   178
fun con_elim_solved_tac ss =
wenzelm@8337
   179
  ALLGOALS (fn i => TRY (simp_case_tac ss i THEN_MAYBE no_tac)) THEN prune_params_tac;
wenzelm@8337
   180
wenzelm@8337
   181
end;
wenzelm@8337
   182
wenzelm@8337
   183
wenzelm@8278
   184
wenzelm@8278
   185
(** cases method **)
wenzelm@8278
   186
wenzelm@8308
   187
(*
wenzelm@8308
   188
  rule selection:
wenzelm@8308
   189
        cases         - classical case split
wenzelm@8376
   190
        cases t       - datatype exhaustion
wenzelm@8376
   191
  <x:A> cases ...     - set elimination
wenzelm@8451
   192
  ...   cases ... R   - explicit rule
wenzelm@8308
   193
*)
wenzelm@8278
   194
wenzelm@9066
   195
val case_split = RuleCases.name ["True", "False"] case_split_thm;
wenzelm@9066
   196
wenzelm@8344
   197
local
wenzelm@8344
   198
wenzelm@8308
   199
fun cases_var thm =
wenzelm@8308
   200
  (case try (hd o vars_of o hd o Logic.strip_assums_hyp o Library.last_elem o Thm.prems_of) thm of
wenzelm@8308
   201
    None => raise THM ("Malformed cases rule", 0, [thm])
wenzelm@8308
   202
  | Some x => x);
wenzelm@8308
   203
wenzelm@8337
   204
fun simplify_cases ctxt =
wenzelm@8337
   205
  Tactic.rule_by_tactic (con_elim_solved_tac (Simplifier.get_local_simpset ctxt));
wenzelm@8337
   206
wenzelm@8344
   207
fun cases_tac (ctxt, (simplified, args)) facts =
wenzelm@8308
   208
  let
wenzelm@8308
   209
    val sg = ProofContext.sign_of ctxt;
wenzelm@8308
   210
    val cert = Thm.cterm_of sg;
wenzelm@8278
   211
wenzelm@8308
   212
    fun inst_rule t thm =
wenzelm@8308
   213
      Drule.cterm_instantiate [(cert (cases_var thm), cert t)] thm;
wenzelm@6442
   214
wenzelm@8376
   215
    val cond_simp = if simplified then simplify_cases ctxt else I;
wenzelm@8376
   216
wenzelm@8376
   217
    fun find_cases th =
wenzelm@8376
   218
      NetRules.may_unify (#2 (get_cases ctxt))
wenzelm@8376
   219
        (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
wenzelm@8376
   220
wenzelm@8376
   221
    val rules =
wenzelm@8344
   222
      (case (args, facts) of
wenzelm@9066
   223
        ((None, None), []) => [RuleCases.add case_split]
wenzelm@8376
   224
      | ((Some t, None), []) =>
wenzelm@8308
   225
          let val name = type_name t in
wenzelm@8308
   226
            (case lookup_casesT ctxt name of
wenzelm@8308
   227
              None => error ("No cases rule for type: " ^ quote name)
wenzelm@8376
   228
            | Some thm => [(inst_rule t thm, RuleCases.get thm)])
wenzelm@8308
   229
          end
wenzelm@8376
   230
      | ((None, None), th :: _) => map (RuleCases.add o #2) (find_cases th)
wenzelm@8376
   231
      | ((Some t, None), th :: _) =>
wenzelm@8376
   232
          (case find_cases th of	(*may instantiate first rule only!*)
wenzelm@8376
   233
            (_, thm) :: _ => [(inst_rule t thm, RuleCases.get thm)]
wenzelm@8376
   234
          | [] => [])
wenzelm@8376
   235
      | ((None, Some thm), _) => [RuleCases.add thm]
wenzelm@8376
   236
      | ((Some t, Some thm), _) => [(inst_rule t thm, RuleCases.get thm)]);
wenzelm@8376
   237
wenzelm@8376
   238
    fun prep_rule (thm, cases) =
wenzelm@8376
   239
      Seq.map (rpair cases o cond_simp) (Method.multi_resolves facts [thm]);
wenzelm@8376
   240
  in Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end;
wenzelm@8278
   241
wenzelm@8344
   242
in
wenzelm@8344
   243
wenzelm@8671
   244
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
wenzelm@8278
   245
wenzelm@8344
   246
end;
wenzelm@8344
   247
wenzelm@8278
   248
wenzelm@8278
   249
wenzelm@8278
   250
(** induct method **)
wenzelm@8278
   251
wenzelm@8308
   252
(*
wenzelm@8308
   253
  rule selection:
wenzelm@8308
   254
        induct         - mathematical induction
wenzelm@8376
   255
        induct x       - datatype induction
wenzelm@8376
   256
  <x:A> induct ...     - set induction
wenzelm@8451
   257
  ...   induct ... R   - explicit rule
wenzelm@8308
   258
*)
wenzelm@8278
   259
wenzelm@8344
   260
local
wenzelm@8344
   261
wenzelm@8376
   262
infix 1 THEN_ALL_NEW_CASES;
wenzelm@8376
   263
wenzelm@8376
   264
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
wenzelm@8376
   265
  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
wenzelm@8540
   266
    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
wenzelm@8376
   267
wenzelm@8376
   268
wenzelm@8330
   269
fun induct_rule ctxt t =
wenzelm@8330
   270
  let val name = type_name t in
wenzelm@8330
   271
    (case lookup_inductT ctxt name of
wenzelm@8330
   272
      None => error ("No induct rule for type: " ^ quote name)
wenzelm@8332
   273
    | Some thm => (name, thm))
wenzelm@8330
   274
  end;
wenzelm@8330
   275
wenzelm@8332
   276
fun join_rules [(_, thm)] = thm
wenzelm@8330
   277
  | join_rules raw_thms =
wenzelm@8330
   278
      let
wenzelm@8332
   279
        val thms = (map (apsnd Drule.freeze_all) raw_thms);
wenzelm@8332
   280
        fun eq_prems ((_, th1), (_, th2)) =
wenzelm@8332
   281
          Term.aconvs (Thm.prems_of th1, Thm.prems_of th2);
wenzelm@8330
   282
      in
wenzelm@8332
   283
        (case Library.gen_distinct eq_prems thms of
wenzelm@8332
   284
          [(_, thm)] =>
wenzelm@8332
   285
            let
wenzelm@8332
   286
              val cprems = Drule.cprems_of thm;
wenzelm@8332
   287
              val asms = map Thm.assume cprems;
wenzelm@8332
   288
              fun strip (_, th) = Drule.implies_elim_list th asms;
wenzelm@8332
   289
            in
wenzelm@8332
   290
              foldr1 (fn (th, th') => [th, th'] MRS conjI) (map strip thms)
wenzelm@8332
   291
              |> Drule.implies_intr_list cprems
wenzelm@8332
   292
              |> Drule.standard
wenzelm@8332
   293
            end
wenzelm@8332
   294
        | [] => error "No rule given"
wenzelm@8332
   295
        | bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads)))
wenzelm@8330
   296
      end;
wenzelm@8330
   297
wenzelm@8376
   298
wenzelm@8344
   299
fun induct_tac (ctxt, (stripped, args)) facts =
wenzelm@8308
   300
  let
wenzelm@8308
   301
    val sg = ProofContext.sign_of ctxt;
wenzelm@8308
   302
    val cert = Thm.cterm_of sg;
wenzelm@8308
   303
wenzelm@8695
   304
    fun prep_var (x, Some t) = Some (cert x, cert t)
wenzelm@8695
   305
      | prep_var (_, None) = None;
wenzelm@8695
   306
wenzelm@8308
   307
    fun prep_inst (concl, ts) =
wenzelm@8308
   308
      let val xs = vars_of concl; val n = length xs - length ts in
wenzelm@8695
   309
        if n < 0 then error "More variables than given than in induction rule"
wenzelm@8695
   310
        else mapfilter prep_var (Library.drop (n, xs) ~~ ts)
wenzelm@8308
   311
      end;
wenzelm@8278
   312
wenzelm@8308
   313
    fun inst_rule insts thm =
wenzelm@8695
   314
      let val concls = concls_of thm in
wenzelm@8695
   315
        if length concls < length insts then
wenzelm@8695
   316
          error "More arguments than given than in induction rule"
wenzelm@8695
   317
        else Drule.cterm_instantiate (flat (map prep_inst (concls ~~ insts))) thm
wenzelm@8695
   318
      end;
wenzelm@8278
   319
wenzelm@8376
   320
    fun find_induct th =
wenzelm@8376
   321
      NetRules.may_unify (#2 (get_induct ctxt))
wenzelm@8376
   322
        (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
wenzelm@8376
   323
wenzelm@8376
   324
    val rules =
wenzelm@8308
   325
      (case (args, facts) of
wenzelm@8540
   326
        (([], None), []) => []
wenzelm@8376
   327
      | ((insts, None), []) =>
wenzelm@8695
   328
          let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts
wenzelm@8695
   329
            handle Library.LIST _ => error "Unable to figure out type induction rule"
wenzelm@8376
   330
          in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end
wenzelm@8376
   331
      | (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th)
wenzelm@8376
   332
      | ((insts, None), th :: _) =>
wenzelm@8376
   333
          (case find_induct th of	(*may instantiate first rule only!*)
wenzelm@8376
   334
	    (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
wenzelm@8376
   335
          | [] => [])
wenzelm@8376
   336
      | (([], Some thm), _) => [RuleCases.add thm]
wenzelm@8376
   337
      | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)]);
wenzelm@8376
   338
wenzelm@8376
   339
    fun prep_rule (thm, cases) =
wenzelm@8376
   340
      Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
wenzelm@8376
   341
    val tac = Method.resolveq_cases_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
wenzelm@8344
   342
  in
wenzelm@8688
   343
    if stripped then tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI])
wenzelm@8376
   344
    else tac
wenzelm@8344
   345
  end;
wenzelm@8344
   346
wenzelm@8344
   347
in
wenzelm@8278
   348
wenzelm@8671
   349
val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac);
wenzelm@8278
   350
wenzelm@8344
   351
end;
wenzelm@8344
   352
wenzelm@8278
   353
wenzelm@8278
   354
wenzelm@8278
   355
(** concrete syntax **)
wenzelm@8278
   356
wenzelm@8308
   357
val casesN = "cases";
wenzelm@8308
   358
val inductN = "induct";
wenzelm@8344
   359
wenzelm@8337
   360
val simplifiedN = "simplified";
wenzelm@8344
   361
val strippedN = "stripped";
wenzelm@8344
   362
wenzelm@8308
   363
val typeN = "type";
wenzelm@8308
   364
val setN = "set";
wenzelm@8308
   365
val ruleN = "rule";
wenzelm@8308
   366
wenzelm@8308
   367
wenzelm@8308
   368
(* attributes *)
wenzelm@8308
   369
wenzelm@8815
   370
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
wenzelm@8308
   371
wenzelm@8308
   372
fun attrib sign_of add_type add_set = Scan.depend (fn x =>
wenzelm@8308
   373
  let val sg = sign_of x in
wenzelm@8308
   374
    spec typeN >> (add_type o Sign.intern_tycon sg) ||
wenzelm@8308
   375
    spec setN  >> (add_set o Sign.intern_const sg)
wenzelm@8308
   376
  end >> pair x);
wenzelm@8308
   377
wenzelm@8308
   378
val cases_attr =
wenzelm@8308
   379
  (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
wenzelm@8308
   380
   Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
wenzelm@8308
   381
wenzelm@8308
   382
val induct_attr =
wenzelm@8308
   383
  (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
wenzelm@8308
   384
   Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
wenzelm@8308
   385
wenzelm@8308
   386
wenzelm@8308
   387
(* methods *)
wenzelm@8308
   388
wenzelm@8278
   389
local
wenzelm@6442
   390
wenzelm@8308
   391
fun err k get name =
wenzelm@8308
   392
  (case get name of Some x => x
wenzelm@8308
   393
  | None => error ("No rule for " ^ k ^ " " ^ quote name));
wenzelm@6442
   394
wenzelm@8308
   395
fun rule get_type get_set =
wenzelm@8308
   396
  Scan.depend (fn ctxt =>
wenzelm@8308
   397
    let val sg = ProofContext.sign_of ctxt in
wenzelm@8308
   398
      spec typeN >> (err typeN (get_type ctxt) o Sign.intern_tycon sg) ||
wenzelm@8308
   399
      spec setN >> (err setN (get_set ctxt) o Sign.intern_const sg)
wenzelm@8308
   400
    end >> pair ctxt) ||
wenzelm@8815
   401
  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
wenzelm@6442
   402
wenzelm@8308
   403
val cases_rule = rule lookup_casesT lookup_casesS;
wenzelm@8308
   404
val induct_rule = rule lookup_inductT lookup_inductS;
wenzelm@6442
   405
wenzelm@8815
   406
val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon;
wenzelm@8308
   407
val term = Scan.unless (Scan.lift kind) Args.local_term;
wenzelm@8695
   408
val term_dummy = Scan.unless (Scan.lift kind)
wenzelm@8695
   409
  (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
wenzelm@6446
   410
wenzelm@8344
   411
fun mode name =
wenzelm@8815
   412
  Scan.lift (Scan.optional (Args.parens (Args.$$$ name) >> K true) false);
wenzelm@8337
   413
wenzelm@8278
   414
in
wenzelm@8278
   415
wenzelm@8695
   416
val cases_args = Method.syntax (mode simplifiedN -- (Scan.option term -- Scan.option cases_rule));
wenzelm@8695
   417
val induct_args = Method.syntax
wenzelm@8695
   418
  (mode strippedN -- (Args.and_list (Scan.repeat term_dummy) -- Scan.option induct_rule));
wenzelm@8278
   419
wenzelm@8278
   420
end;
wenzelm@6446
   421
wenzelm@6446
   422
wenzelm@6442
   423
wenzelm@8278
   424
(** theory setup **)
wenzelm@6446
   425
wenzelm@8278
   426
val setup =
wenzelm@8308
   427
  [GlobalInduct.init, LocalInduct.init,
wenzelm@8308
   428
   Attrib.add_attributes
wenzelm@8308
   429
    [(casesN, cases_attr, "cases rule for type or set"),
wenzelm@8308
   430
     (inductN, induct_attr, "induction rule for type or set")],
wenzelm@8308
   431
   Method.add_methods
wenzelm@8308
   432
    [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
wenzelm@9066
   433
     ("induct", induct_meth oo induct_args, "induction on types or sets")],
wenzelm@9066
   434
   (#1 o PureThy.add_thms [(("case_split", case_split), [])])];
wenzelm@6442
   435
wenzelm@6442
   436
end;