src/Provers/induct_method.ML
author wenzelm
Wed Apr 04 23:29:33 2007 +0200 (2007-04-04)
changeset 22596 d0d2af4db18f
parent 21879 a3efbae45735
child 22826 0f4c501a691e
permissions -rw-r--r--
rep_thm/cterm/ctyp: removed obsolete sign field;
     1 (*  Title:      Provers/induct_method.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Proof by cases and induction on sets and types.
     6 *)
     7 
     8 signature INDUCT_METHOD_DATA =
     9 sig
    10   val cases_default: thm
    11   val atomize: thm list
    12   val rulify: thm list
    13   val rulify_fallback: thm list
    14 end;
    15 
    16 signature INDUCT_METHOD =
    17 sig
    18   val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    19   val add_defs: (string option * term) option list -> Proof.context ->
    20     (term option list * thm list) * Proof.context
    21   val atomize_term: theory -> term -> term
    22   val atomize_tac: int -> tactic
    23   val inner_atomize_tac: int -> tactic
    24   val rulified_term: thm -> theory * term
    25   val rulify_tac: int -> tactic
    26   val internalize: int -> thm -> thm
    27   val guess_instance: thm -> int -> thm -> thm Seq.seq
    28   val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    29     thm list -> int -> cases_tactic
    30   val induct_tac: Proof.context -> bool -> (string option * term) option list list ->
    31     (string * typ) list list -> term option list -> thm list option -> thm list -> int ->
    32     cases_tactic
    33   val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
    34     thm option -> thm list -> int -> cases_tactic
    35   val setup: theory -> theory
    36 end;
    37 
    38 functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
    39 struct
    40 
    41 val meta_spec = thm "Pure.meta_spec";
    42 val all_conjunction = thm "Pure.all_conjunction";
    43 val imp_conjunction = thm "Pure.imp_conjunction";
    44 val conjunction_imp = thm "Pure.conjunction_imp";
    45 val conjunction_congs = [all_conjunction, imp_conjunction];
    46 
    47 
    48 
    49 (** misc utils **)
    50 
    51 (* alignment *)
    52 
    53 fun align_left msg xs ys =
    54   let val m = length xs and n = length ys
    55   in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
    56 
    57 fun align_right msg xs ys =
    58   let val m = length xs and n = length ys
    59   in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
    60 
    61 
    62 (* prep_inst *)
    63 
    64 fun prep_inst thy align tune (tm, ts) =
    65   let
    66     val cert = Thm.cterm_of thy;
    67     fun prep_var (x, SOME t) =
    68           let
    69             val cx = cert x;
    70             val {T = xT, thy, ...} = Thm.rep_cterm cx;
    71             val ct = cert (tune t);
    72           in
    73             if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
    74             else error (Pretty.string_of (Pretty.block
    75              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
    76               Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
    77               Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
    78           end
    79       | prep_var (_, NONE) = NONE;
    80     val xs = InductAttrib.vars_of tm;
    81   in
    82     align "Rule has fewer variables than instantiations given" xs ts
    83     |> map_filter prep_var
    84   end;
    85 
    86 
    87 (* trace_rules *)
    88 
    89 fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
    90   | trace_rules ctxt _ rules = Method.trace ctxt rules;
    91 
    92 
    93 (* make_cases *)
    94 
    95 fun make_cases is_open rule =
    96   RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
    97 
    98 fun warn_open true = warning "Encountered open rule cases -- deprecated"
    99   | warn_open false = ();
   100 
   101 
   102 
   103 (** cases method **)
   104 
   105 (*
   106   rule selection scheme:
   107           cases         - default case split
   108     `x:A` cases ...     - set cases
   109           cases t       - type cases
   110     ...   cases ... r   - explicit rule
   111 *)
   112 
   113 local
   114 
   115 fun find_casesT ctxt ((SOME t :: _) :: _) = InductAttrib.find_casesT ctxt (Term.fastype_of t)
   116   | find_casesT _ _ = [];
   117 
   118 fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt (Thm.concl_of fact)
   119   | find_casesS _ _ = [];
   120 
   121 in
   122 
   123 fun cases_tac ctxt is_open insts opt_rule facts =
   124   let
   125     val _ = warn_open is_open;
   126     val thy = ProofContext.theory_of ctxt;
   127     val cert = Thm.cterm_of thy;
   128 
   129     fun inst_rule r =
   130       if null insts then `RuleCases.get r
   131       else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
   132         |> maps (prep_inst thy align_left I)
   133         |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
   134 
   135     val ruleq =
   136       (case opt_rule of
   137         SOME r => Seq.single (inst_rule r)
   138       | NONE =>
   139           (find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default])
   140           |> tap (trace_rules ctxt InductAttrib.casesN)
   141           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   142   in
   143     fn i => fn st =>
   144       ruleq
   145       |> Seq.maps (RuleCases.consume [] facts)
   146       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   147         CASES (make_cases is_open rule cases)
   148           (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
   149   end;
   150 
   151 end;
   152 
   153 
   154 
   155 (** induct method **)
   156 
   157 (* atomize *)
   158 
   159 fun atomize_term thy =
   160   MetaSimplifier.rewrite_term thy Data.atomize []
   161   #> ObjectLogic.drop_judgment thy;
   162 
   163 val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
   164 
   165 val atomize_tac = Goal.rewrite_goal_tac Data.atomize;
   166 
   167 val inner_atomize_tac =
   168   Goal.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
   169 
   170 
   171 (* rulify *)
   172 
   173 fun rulify_term thy =
   174   MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
   175   MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
   176 
   177 fun rulified_term thm =
   178   let
   179     val thy = Thm.theory_of_thm thm;
   180     val rulify = rulify_term thy;
   181     val (As, B) = Logic.strip_horn (Thm.prop_of thm);
   182   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
   183 
   184 val rulify_tac =
   185   Goal.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
   186   Goal.rewrite_goal_tac Data.rulify_fallback THEN'
   187   Goal.conjunction_tac THEN_ALL_NEW
   188   (Goal.rewrite_goal_tac [conjunction_imp] THEN' Goal.norm_hhf_tac);
   189 
   190 
   191 (* prepare rule *)
   192 
   193 fun rule_instance thy inst rule =
   194   Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
   195 
   196 fun internalize k th =
   197   th |> Thm.permute_prems 0 k
   198   |> Drule.fconv_rule (Drule.concl_conv (Thm.nprems_of th - k) atomize_cterm);
   199 
   200 
   201 (* guess rule instantiation -- cannot handle pending goal parameters *)
   202 
   203 local
   204 
   205 fun dest_env thy (env as Envir.Envir {iTs, ...}) =
   206   let
   207     val cert = Thm.cterm_of thy;
   208     val certT = Thm.ctyp_of thy;
   209     val pairs = Envir.alist_of env;
   210     val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
   211     val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
   212   in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
   213 
   214 in
   215 
   216 fun guess_instance rule i st =
   217   let
   218     val {thy, maxidx, ...} = Thm.rep_thm st;
   219     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
   220     val params = rev (rename_wrt_term goal (Logic.strip_params goal));
   221   in
   222     if not (null params) then
   223       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
   224         commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params));
   225       Seq.single rule)
   226     else
   227       let
   228         val rule' = Thm.incr_indexes (maxidx + 1) rule;
   229         val concl = Logic.strip_assums_concl goal;
   230       in
   231         Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
   232           (Envir.empty (#maxidx (Thm.rep_thm rule')))
   233         |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
   234       end
   235   end handle Subscript => Seq.empty;
   236 
   237 end;
   238 
   239 
   240 (* special renaming of rule parameters *)
   241 
   242 fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
   243       let
   244         val x = ProofContext.revert_skolem ctxt z;
   245         fun index i [] = []
   246           | index i (y :: ys) =
   247               if x = y then x ^ string_of_int i :: index (i + 1) ys
   248               else y :: index i ys;
   249         fun rename_params [] = []
   250           | rename_params ((y, Type (U, _)) :: ys) =
   251               (if U = T then x else y) :: rename_params ys
   252           | rename_params ((y, _) :: ys) = y :: rename_params ys;
   253         fun rename_asm A =
   254           let
   255             val xs = rename_params (Logic.strip_params A);
   256             val xs' =
   257               (case List.filter (equal x) xs of
   258                 [] => xs | [_] => xs | _ => index 1 xs);
   259           in Logic.list_rename_params (xs', A) end;
   260         fun rename_prop p =
   261           let val (As, C) = Logic.strip_horn p
   262           in Logic.list_implies (map rename_asm As, C) end;
   263         val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
   264         val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
   265       in [RuleCases.save thm thm'] end
   266   | special_rename_params _ _ ths = ths;
   267 
   268 
   269 (* fix_tac *)
   270 
   271 local
   272 
   273 fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
   274   | goal_prefix 0 _ = Term.dummy_pattern propT
   275   | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
   276   | goal_prefix _ _ = Term.dummy_pattern propT;
   277 
   278 fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
   279   | goal_params 0 _ = 0
   280   | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
   281   | goal_params _ _ = 0;
   282 
   283 fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
   284   let
   285     val thy = ProofContext.theory_of ctxt;
   286     val cert = Thm.cterm_of thy;
   287     val certT = Thm.ctyp_of thy;
   288 
   289     val v = Free (x, T);
   290     fun spec_rule prfx (xs, body) =
   291       meta_spec
   292       |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1)
   293       |> Thm.lift_rule (cert prfx)
   294       |> `(Thm.prop_of #> Logic.strip_assums_concl)
   295       |-> (fn pred $ arg =>
   296         Drule.cterm_instantiate
   297           [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
   298            (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
   299 
   300     fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
   301       | goal_concl 0 xs B =
   302           if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
   303           else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
   304       | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
   305       | goal_concl _ _ _ = NONE;
   306   in
   307     (case goal_concl n [] goal of
   308       SOME concl =>
   309         (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
   310     | NONE => all_tac)
   311   end);
   312 
   313 fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule
   314   (Drule.goals_conv (Library.equal i)
   315     (Drule.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
   316 
   317 in
   318 
   319 fun fix_tac _ _ [] = K all_tac
   320   | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
   321      (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
   322       (miniscope_tac (goal_params n goal))) i);
   323 
   324 end;
   325 
   326 
   327 (* add_defs *)
   328 
   329 fun add_defs def_insts =
   330   let
   331     fun add (SOME (SOME x, t)) ctxt =
   332           let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
   333           in ((SOME lhs, [th]), ctxt') end
   334       | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
   335       | add NONE ctxt = ((NONE, []), ctxt);
   336   in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
   337 
   338 
   339 (* induct_tac *)
   340 
   341 (*
   342   rule selection scheme:
   343     `x:A` induct ...     - set induction
   344           induct x       - type induction
   345     ...   induct ... r   - explicit rule
   346 *)
   347 
   348 local
   349 
   350 fun find_inductT ctxt insts =
   351   fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts)
   352     |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]]
   353   |> filter_out (forall PureThy.is_internal);
   354 
   355 fun find_inductS ctxt (fact :: _) = map single (InductAttrib.find_inductS ctxt (Thm.concl_of fact))
   356   | find_inductS _ _ = [];
   357 
   358 in
   359 
   360 fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
   361   let
   362     val _ = warn_open is_open;
   363     val thy = ProofContext.theory_of ctxt;
   364     val cert = Thm.cterm_of thy;
   365 
   366     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
   367     val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
   368 
   369     fun inst_rule (concls, r) =
   370       (if null insts then `RuleCases.get r
   371        else (align_left "Rule has fewer conclusions than arguments given"
   372           (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
   373         |> maps (prep_inst thy align_right (atomize_term thy))
   374         |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
   375       |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
   376 
   377     val ruleq =
   378       (case opt_rule of
   379         SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
   380       | NONE =>
   381           (find_inductS ctxt facts @
   382             map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts))
   383           |> map_filter (RuleCases.mutual_rule ctxt)
   384           |> tap (trace_rules ctxt InductAttrib.inductN o map #2)
   385           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   386 
   387     fun rule_cases rule =
   388       RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule);
   389   in
   390     (fn i => fn st =>
   391       ruleq
   392       |> Seq.maps (RuleCases.consume (flat defs) facts)
   393       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   394         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   395           (CONJUNCTS (ALLGOALS
   396             (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
   397               THEN' fix_tac defs_ctxt
   398                 (nth concls (j - 1) + more_consumes)
   399                 (nth_list arbitrary (j - 1))))
   400           THEN' inner_atomize_tac) j))
   401         THEN' atomize_tac) i st |> Seq.maps (fn st' =>
   402             guess_instance (internalize more_consumes rule) i st'
   403             |> Seq.map (rule_instance thy taking)
   404             |> Seq.maps (fn rule' =>
   405               CASES (rule_cases rule' cases)
   406                 (Tactic.rtac rule' i THEN
   407                   PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
   408     THEN_ALL_NEW_CASES rulify_tac
   409   end;
   410 
   411 end;
   412 
   413 
   414 
   415 (** coinduct method **)
   416 
   417 (*
   418   rule selection scheme:
   419     goal "x:A" coinduct ...   - set coinduction
   420                coinduct x     - type coinduction
   421                coinduct ... r - explicit rule
   422 *)
   423 
   424 local
   425 
   426 fun find_coinductT ctxt (SOME t :: _) = InductAttrib.find_coinductT ctxt (Term.fastype_of t)
   427   | find_coinductT _ _ = [];
   428 
   429 fun find_coinductS ctxt goal = InductAttrib.find_coinductS ctxt (Logic.strip_assums_concl goal);
   430 
   431 in
   432 
   433 fun coinduct_tac ctxt is_open inst taking opt_rule facts =
   434   let
   435     val _ = warn_open is_open;
   436     val thy = ProofContext.theory_of ctxt;
   437     val cert = Thm.cterm_of thy;
   438 
   439     fun inst_rule r =
   440       if null inst then `RuleCases.get r
   441       else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r
   442         |> pair (RuleCases.get r);
   443 
   444     fun ruleq goal =
   445       (case opt_rule of
   446         SOME r => Seq.single (inst_rule r)
   447       | NONE =>
   448           (find_coinductS ctxt goal @ find_coinductT ctxt inst)
   449           |> tap (trace_rules ctxt InductAttrib.coinductN)
   450           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   451   in
   452     SUBGOAL_CASES (fn (goal, i) => fn st =>
   453       ruleq goal
   454       |> Seq.maps (RuleCases.consume [] facts)
   455       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   456         guess_instance rule i st
   457         |> Seq.map (rule_instance thy taking)
   458         |> Seq.maps (fn rule' =>
   459           CASES (make_cases is_open rule' cases)
   460             (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   461   end;
   462 
   463 end;
   464 
   465 
   466 
   467 (** concrete syntax **)
   468 
   469 val openN = "open";
   470 val arbitraryN = "arbitrary";
   471 val takingN = "taking";
   472 val ruleN = "rule";
   473 
   474 local
   475 
   476 fun single_rule [rule] = rule
   477   | single_rule _ = error "Single rule expected";
   478 
   479 fun named_rule k arg get =
   480   Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :--
   481     (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
   482       (case get (Context.proof_of context) name of SOME x => x
   483       | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2;
   484 
   485 fun rule get_type get_set =
   486   named_rule InductAttrib.typeN Args.tyname get_type ||
   487   named_rule InductAttrib.setN Args.const get_set ||
   488   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
   489 
   490 val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS >> single_rule;
   491 val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
   492 val coinduct_rule =
   493   rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule;
   494 
   495 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
   496 
   497 val def_inst =
   498   ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
   499       -- Args.term) >> SOME ||
   500     inst >> Option.map (pair NONE);
   501 
   502 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
   503   error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
   504 
   505 fun unless_more_args scan = Scan.unless (Scan.lift
   506   ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
   507     Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan;
   508 
   509 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   510   Args.and_list1 (Scan.repeat (unless_more_args free))) [];
   511 
   512 val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
   513   Scan.repeat1 (unless_more_args inst)) [];
   514 
   515 in
   516 
   517 fun cases_meth src =
   518   Method.syntax (Args.mode openN --
   519     (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
   520   #> (fn ((is_open, (insts, opt_rule)), ctxt) =>
   521     Method.METHOD_CASES (fn facts =>
   522       Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
   523 
   524 fun induct_meth src =
   525   Method.syntax (Args.mode openN --
   526     (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
   527     (arbitrary -- taking -- Scan.option induct_rule))) src
   528   #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) =>
   529     Method.RAW_METHOD_CASES (fn facts =>
   530       Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
   531 
   532 fun coinduct_meth src =
   533   Method.syntax (Args.mode openN --
   534     (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
   535   #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) =>
   536     Method.RAW_METHOD_CASES (fn facts =>
   537       Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
   538 
   539 end;
   540 
   541 
   542 
   543 (** theory setup **)
   544 
   545 val setup =
   546   Method.add_methods
   547     [(InductAttrib.casesN, cases_meth, "case analysis on types or sets"),
   548      (InductAttrib.inductN, induct_meth, "induction on types or sets"),
   549      (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")];
   550 
   551 end;