src/Tools/induct.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 24865 62c48c4bee48
child 24920 2a45e400fdad
permissions -rw-r--r--
simplified interfaces for outer syntax;
     1 (*  Title:      Tools/induct.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Proof by cases and induction.
     6 *)
     7 
     8 signature INDUCT_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 =
    17 sig
    18   (*rule declarations*)
    19   val vars_of: term -> term list
    20   val dest_rules: Proof.context ->
    21     {type_cases: (string * thm) list, pred_cases: (string * thm) list,
    22       type_induct: (string * thm) list, pred_induct: (string * thm) list,
    23       type_coinduct: (string * thm) list, pred_coinduct: (string * thm) list}
    24   val print_rules: Proof.context -> unit
    25   val lookup_casesT: Proof.context -> string -> thm option
    26   val lookup_casesP: Proof.context -> string -> thm option
    27   val lookup_inductT: Proof.context -> string -> thm option
    28   val lookup_inductP: Proof.context -> string -> thm option
    29   val lookup_coinductT: Proof.context -> string -> thm option
    30   val lookup_coinductP: Proof.context -> string -> thm option
    31   val find_casesT: Proof.context -> typ -> thm list
    32   val find_casesP: Proof.context -> term -> thm list
    33   val find_inductT: Proof.context -> typ -> thm list
    34   val find_inductP: Proof.context -> term -> thm list
    35   val find_coinductT: Proof.context -> typ -> thm list
    36   val find_coinductP: Proof.context -> term -> thm list
    37   val cases_type: string -> attribute
    38   val cases_pred: string -> attribute
    39   val induct_type: string -> attribute
    40   val induct_pred: string -> attribute
    41   val coinduct_type: string -> attribute
    42   val coinduct_pred: string -> attribute
    43   val casesN: string
    44   val inductN: string
    45   val coinductN: string
    46   val typeN: string
    47   val predN: string
    48   val setN: string
    49   (*proof methods*)
    50   val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    51   val add_defs: (string option * term) option list -> Proof.context ->
    52     (term option list * thm list) * Proof.context
    53   val atomize_term: theory -> term -> term
    54   val atomize_tac: int -> tactic
    55   val inner_atomize_tac: int -> tactic
    56   val rulified_term: thm -> theory * term
    57   val rulify_tac: int -> tactic
    58   val internalize: int -> thm -> thm
    59   val guess_instance: thm -> int -> thm -> thm Seq.seq
    60   val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    61     thm list -> int -> cases_tactic
    62   val induct_tac: Proof.context -> bool -> (string option * term) option list list ->
    63     (string * typ) list list -> term option list -> thm list option -> thm list -> int ->
    64     cases_tactic
    65   val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
    66     thm option -> thm list -> int -> cases_tactic
    67   val setup: theory -> theory
    68 end;
    69 
    70 functor InductFun(Data: INDUCT_DATA): INDUCT =
    71 struct
    72 
    73 
    74 (** misc utils **)
    75 
    76 (* encode_type -- for indexing purposes *)
    77 
    78 fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
    79   | encode_type (TFree (a, _)) = Free (a, dummyT)
    80   | encode_type (TVar (a, _)) = Var (a, dummyT);
    81 
    82 
    83 (* variables -- ordered left-to-right, preferring right *)
    84 
    85 fun vars_of tm =
    86   rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
    87 
    88 local
    89 
    90 val mk_var = encode_type o #2 o Term.dest_Var;
    91 
    92 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
    93   raise THM ("No variables in conclusion of rule", 0, [thm]);
    94 
    95 in
    96 
    97 fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
    98   raise THM ("No variables in major premise of rule", 0, [thm]);
    99 
   100 val left_var_concl = concl_var hd;
   101 val right_var_concl = concl_var List.last;
   102 
   103 end;
   104 
   105 
   106 
   107 (** induct data **)
   108 
   109 (* rules *)
   110 
   111 type rules = (string * thm) NetRules.T;
   112 
   113 val init_rules =
   114   NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
   115     Thm.eq_thm_prop (th1, th2));
   116 
   117 fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
   118 
   119 fun pretty_rules ctxt kind rs =
   120   let val thms = map snd (NetRules.rules rs)
   121   in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
   122 
   123 
   124 (* context data *)
   125 
   126 structure Induct = GenericDataFun
   127 (
   128   type T = (rules * rules) * (rules * rules) * (rules * rules);
   129   val empty =
   130     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
   131      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   132      (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
   133   val extend = I;
   134   fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
   135       ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
   136     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)),
   137       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)),
   138       (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2)));
   139 );
   140 
   141 val get_local = Induct.get o Context.Proof;
   142 
   143 fun dest_rules ctxt =
   144   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
   145     {type_cases = NetRules.rules casesT,
   146      pred_cases = NetRules.rules casesP,
   147      type_induct = NetRules.rules inductT,
   148      pred_induct = NetRules.rules inductP,
   149      type_coinduct = NetRules.rules coinductT,
   150      pred_coinduct = NetRules.rules coinductP}
   151   end;
   152 
   153 fun print_rules ctxt =
   154   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
   155    [pretty_rules ctxt "coinduct type:" coinductT,
   156     pretty_rules ctxt "coinduct pred:" coinductP,
   157     pretty_rules ctxt "induct type:" inductT,
   158     pretty_rules ctxt "induct pred:" inductP,
   159     pretty_rules ctxt "cases type:" casesT,
   160     pretty_rules ctxt "cases pred:" casesP]
   161     |> Pretty.chunks |> Pretty.writeln
   162   end;
   163 
   164 val _ =
   165   OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
   166     OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   167       Toplevel.keep (print_rules o Toplevel.context_of)));
   168 
   169 
   170 (* access rules *)
   171 
   172 val lookup_casesT = lookup_rule o #1 o #1 o get_local;
   173 val lookup_casesP = lookup_rule o #2 o #1 o get_local;
   174 val lookup_inductT = lookup_rule o #1 o #2 o get_local;
   175 val lookup_inductP = lookup_rule o #2 o #2 o get_local;
   176 val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
   177 val lookup_coinductP = lookup_rule o #2 o #3 o get_local;
   178 
   179 
   180 fun find_rules which how ctxt x =
   181   map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
   182 
   183 val find_casesT = find_rules (#1 o #1) encode_type;
   184 val find_casesP = find_rules (#2 o #1) I;
   185 val find_inductT = find_rules (#1 o #2) encode_type;
   186 val find_inductP = find_rules (#2 o #2) I;
   187 val find_coinductT = find_rules (#1 o #3) encode_type;
   188 val find_coinductP = find_rules (#2 o #3) I;
   189 
   190 
   191 
   192 (** attributes **)
   193 
   194 local
   195 
   196 fun mk_att f g name arg =
   197   let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
   198 
   199 fun map1 f (x, y, z) = (f x, y, z);
   200 fun map2 f (x, y, z) = (x, f y, z);
   201 fun map3 f (x, y, z) = (x, y, f z);
   202 
   203 fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
   204 fun add_casesP rule x = map1 (apsnd (NetRules.insert rule)) x;
   205 fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
   206 fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x;
   207 fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
   208 fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x;
   209 
   210 fun consumes0 x = RuleCases.consumes_default 0 x;
   211 fun consumes1 x = RuleCases.consumes_default 1 x;
   212 
   213 in
   214 
   215 val cases_type = mk_att add_casesT consumes0;
   216 val cases_pred = mk_att add_casesP consumes1;
   217 val induct_type = mk_att add_inductT consumes0;
   218 val induct_pred = mk_att add_inductP consumes1;
   219 val coinduct_type = mk_att add_coinductT consumes0;
   220 val coinduct_pred = mk_att add_coinductP consumes1;
   221 
   222 end;
   223 
   224 
   225 
   226 (** attribute syntax **)
   227 
   228 val casesN = "cases";
   229 val inductN = "induct";
   230 val coinductN = "coinduct";
   231 
   232 val typeN = "type";
   233 val predN = "pred";
   234 val setN = "set";
   235 
   236 local
   237 
   238 fun spec k arg =
   239   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   240   Scan.lift (Args.$$$ k) >> K "";
   241 
   242 fun attrib add_type add_pred = Attrib.syntax
   243  (spec typeN Args.tyname >> add_type ||
   244   spec predN Args.const >> add_pred ||
   245   spec setN Args.const >> add_pred);
   246 
   247 val cases_att = attrib cases_type cases_pred;
   248 val induct_att = attrib induct_type induct_pred;
   249 val coinduct_att = attrib coinduct_type coinduct_pred;
   250 
   251 in
   252 
   253 val attrib_setup = Attrib.add_attributes
   254  [(casesN, cases_att, "declaration of cases rule for type or predicate/set"),
   255   (inductN, induct_att, "declaration of induction rule for type or predicate/set"),
   256   (coinductN, coinduct_att, "declaration of coinduction rule for type or predicate/set")];
   257 
   258 end;
   259 
   260 
   261 
   262 (** method utils **)
   263 
   264 (* alignment *)
   265 
   266 fun align_left msg xs ys =
   267   let val m = length xs and n = length ys
   268   in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
   269 
   270 fun align_right msg xs ys =
   271   let val m = length xs and n = length ys
   272   in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
   273 
   274 
   275 (* prep_inst *)
   276 
   277 fun prep_inst thy align tune (tm, ts) =
   278   let
   279     val cert = Thm.cterm_of thy;
   280     fun prep_var (x, SOME t) =
   281           let
   282             val cx = cert x;
   283             val {T = xT, thy, ...} = Thm.rep_cterm cx;
   284             val ct = cert (tune t);
   285           in
   286             if Type.could_unify (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
   287             else error (Pretty.string_of (Pretty.block
   288              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
   289               Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
   290               Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
   291           end
   292       | prep_var (_, NONE) = NONE;
   293     val xs = vars_of tm;
   294   in
   295     align "Rule has fewer variables than instantiations given" xs ts
   296     |> map_filter prep_var
   297   end;
   298 
   299 
   300 (* trace_rules *)
   301 
   302 fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
   303   | trace_rules ctxt _ rules = Method.trace ctxt rules;
   304 
   305 
   306 (* make_cases *)
   307 
   308 fun make_cases is_open rule =
   309   RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
   310 
   311 fun warn_open true = legacy_feature "open rule cases in proof method"
   312   | warn_open false = ();
   313 
   314 
   315 
   316 (** cases method **)
   317 
   318 (*
   319   rule selection scheme:
   320           cases         - default case split
   321     `A t` cases ...     - predicate/set cases
   322           cases t       - type cases
   323     ...   cases ... r   - explicit rule
   324 *)
   325 
   326 local
   327 
   328 fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t)
   329   | get_casesT _ _ = [];
   330 
   331 fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact)
   332   | get_casesP _ _ = [];
   333 
   334 in
   335 
   336 fun cases_tac ctxt is_open insts opt_rule facts =
   337   let
   338     val _ = warn_open is_open;
   339     val thy = ProofContext.theory_of ctxt;
   340     val cert = Thm.cterm_of thy;
   341 
   342     fun inst_rule r =
   343       if null insts then `RuleCases.get r
   344       else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
   345         |> maps (prep_inst thy align_left I)
   346         |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
   347 
   348     val ruleq =
   349       (case opt_rule of
   350         SOME r => Seq.single (inst_rule r)
   351       | NONE =>
   352           (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
   353           |> tap (trace_rules ctxt casesN)
   354           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   355   in
   356     fn i => fn st =>
   357       ruleq
   358       |> Seq.maps (RuleCases.consume [] facts)
   359       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   360         CASES (make_cases is_open rule cases)
   361           (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
   362   end;
   363 
   364 end;
   365 
   366 
   367 
   368 (** induct method **)
   369 
   370 val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}];
   371 
   372 
   373 (* atomize *)
   374 
   375 fun atomize_term thy =
   376   MetaSimplifier.rewrite_term thy Data.atomize []
   377   #> ObjectLogic.drop_judgment thy;
   378 
   379 val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
   380 
   381 val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
   382 
   383 val inner_atomize_tac =
   384   Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
   385 
   386 
   387 (* rulify *)
   388 
   389 fun rulify_term thy =
   390   MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
   391   MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
   392 
   393 fun rulified_term thm =
   394   let
   395     val thy = Thm.theory_of_thm thm;
   396     val rulify = rulify_term thy;
   397     val (As, B) = Logic.strip_horn (Thm.prop_of thm);
   398   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
   399 
   400 val rulify_tac =
   401   Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
   402   Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
   403   Goal.conjunction_tac THEN_ALL_NEW
   404   (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
   405 
   406 
   407 (* prepare rule *)
   408 
   409 fun rule_instance thy inst rule =
   410   Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
   411 
   412 fun internalize k th =
   413   th |> Thm.permute_prems 0 k
   414   |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
   415 
   416 
   417 (* guess rule instantiation -- cannot handle pending goal parameters *)
   418 
   419 local
   420 
   421 fun dest_env thy (env as Envir.Envir {iTs, ...}) =
   422   let
   423     val cert = Thm.cterm_of thy;
   424     val certT = Thm.ctyp_of thy;
   425     val pairs = Envir.alist_of env;
   426     val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
   427     val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
   428   in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
   429 
   430 in
   431 
   432 fun guess_instance rule i st =
   433   let
   434     val {thy, maxidx, ...} = Thm.rep_thm st;
   435     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
   436     val params = rev (rename_wrt_term goal (Logic.strip_params goal));
   437   in
   438     if not (null params) then
   439       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
   440         commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params));
   441       Seq.single rule)
   442     else
   443       let
   444         val rule' = Thm.incr_indexes (maxidx + 1) rule;
   445         val concl = Logic.strip_assums_concl goal;
   446       in
   447         Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
   448           (Envir.empty (#maxidx (Thm.rep_thm rule')))
   449         |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
   450       end
   451   end handle Subscript => Seq.empty;
   452 
   453 end;
   454 
   455 
   456 (* special renaming of rule parameters *)
   457 
   458 fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
   459       let
   460         val x = ProofContext.revert_skolem ctxt z;
   461         fun index i [] = []
   462           | index i (y :: ys) =
   463               if x = y then x ^ string_of_int i :: index (i + 1) ys
   464               else y :: index i ys;
   465         fun rename_params [] = []
   466           | rename_params ((y, Type (U, _)) :: ys) =
   467               (if U = T then x else y) :: rename_params ys
   468           | rename_params ((y, _) :: ys) = y :: rename_params ys;
   469         fun rename_asm A =
   470           let
   471             val xs = rename_params (Logic.strip_params A);
   472             val xs' =
   473               (case List.filter (equal x) xs of
   474                 [] => xs | [_] => xs | _ => index 1 xs);
   475           in Logic.list_rename_params (xs', A) end;
   476         fun rename_prop p =
   477           let val (As, C) = Logic.strip_horn p
   478           in Logic.list_implies (map rename_asm As, C) end;
   479         val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
   480         val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
   481       in [RuleCases.save thm thm'] end
   482   | special_rename_params _ _ ths = ths;
   483 
   484 
   485 (* fix_tac *)
   486 
   487 local
   488 
   489 fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
   490   | goal_prefix 0 _ = Term.dummy_pattern propT
   491   | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
   492   | goal_prefix _ _ = Term.dummy_pattern propT;
   493 
   494 fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
   495   | goal_params 0 _ = 0
   496   | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
   497   | goal_params _ _ = 0;
   498 
   499 fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
   500   let
   501     val thy = ProofContext.theory_of ctxt;
   502     val cert = Thm.cterm_of thy;
   503     val certT = Thm.ctyp_of thy;
   504 
   505     val v = Free (x, T);
   506     fun spec_rule prfx (xs, body) =
   507       @{thm Pure.meta_spec}
   508       |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1)
   509       |> Thm.lift_rule (cert prfx)
   510       |> `(Thm.prop_of #> Logic.strip_assums_concl)
   511       |-> (fn pred $ arg =>
   512         Drule.cterm_instantiate
   513           [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
   514            (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
   515 
   516     fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
   517       | goal_concl 0 xs B =
   518           if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
   519           else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
   520       | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
   521       | goal_concl _ _ _ = NONE;
   522   in
   523     (case goal_concl n [] goal of
   524       SOME concl =>
   525         (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
   526     | NONE => all_tac)
   527   end);
   528 
   529 fun miniscope_tac p = CONVERSION o
   530   Conv.forall_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
   531 
   532 in
   533 
   534 fun fix_tac _ _ [] = K all_tac
   535   | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
   536      (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
   537       (miniscope_tac (goal_params n goal) ctxt)) i);
   538 
   539 end;
   540 
   541 
   542 (* add_defs *)
   543 
   544 fun add_defs def_insts =
   545   let
   546     fun add (SOME (SOME x, t)) ctxt =
   547           let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
   548           in ((SOME lhs, [th]), ctxt') end
   549       | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
   550       | add NONE ctxt = ((NONE, []), ctxt);
   551   in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
   552 
   553 
   554 (* induct_tac *)
   555 
   556 (*
   557   rule selection scheme:
   558     `A x` induct ...     - predicate/set induction
   559           induct x       - type induction
   560     ...   induct ... r   - explicit rule
   561 *)
   562 
   563 local
   564 
   565 fun get_inductT ctxt insts =
   566   fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts)
   567     |> map (find_inductT ctxt o Term.fastype_of)) [[]]
   568   |> filter_out (forall PureThy.is_internal);
   569 
   570 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   571   | get_inductP _ _ = [];
   572 
   573 in
   574 
   575 fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
   576   let
   577     val _ = warn_open is_open;
   578     val thy = ProofContext.theory_of ctxt;
   579     val cert = Thm.cterm_of thy;
   580 
   581     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
   582     val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
   583 
   584     fun inst_rule (concls, r) =
   585       (if null insts then `RuleCases.get r
   586        else (align_left "Rule has fewer conclusions than arguments given"
   587           (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
   588         |> maps (prep_inst thy align_right (atomize_term thy))
   589         |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
   590       |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
   591 
   592     val ruleq =
   593       (case opt_rule of
   594         SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
   595       | NONE =>
   596           (get_inductP ctxt facts @
   597             map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
   598           |> map_filter (RuleCases.mutual_rule ctxt)
   599           |> tap (trace_rules ctxt inductN o map #2)
   600           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   601 
   602     fun rule_cases rule =
   603       RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule);
   604   in
   605     (fn i => fn st =>
   606       ruleq
   607       |> Seq.maps (RuleCases.consume (flat defs) facts)
   608       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   609         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   610           (CONJUNCTS (ALLGOALS
   611             (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
   612               THEN' fix_tac defs_ctxt
   613                 (nth concls (j - 1) + more_consumes)
   614                 (nth_list arbitrary (j - 1))))
   615           THEN' inner_atomize_tac) j))
   616         THEN' atomize_tac) i st |> Seq.maps (fn st' =>
   617             guess_instance (internalize more_consumes rule) i st'
   618             |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
   619             |> Seq.maps (fn rule' =>
   620               CASES (rule_cases rule' cases)
   621                 (Tactic.rtac rule' i THEN
   622                   PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
   623     THEN_ALL_NEW_CASES rulify_tac
   624   end;
   625 
   626 end;
   627 
   628 
   629 
   630 (** coinduct method **)
   631 
   632 (*
   633   rule selection scheme:
   634     goal "A x" coinduct ...   - predicate/set coinduction
   635                coinduct x     - type coinduction
   636                coinduct ... r - explicit rule
   637 *)
   638 
   639 local
   640 
   641 fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t)
   642   | get_coinductT _ _ = [];
   643 
   644 fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal);
   645 
   646 fun main_prop_of th =
   647   if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
   648 
   649 in
   650 
   651 fun coinduct_tac ctxt is_open inst taking opt_rule facts =
   652   let
   653     val _ = warn_open is_open;
   654     val thy = ProofContext.theory_of ctxt;
   655     val cert = Thm.cterm_of thy;
   656 
   657     fun inst_rule r =
   658       if null inst then `RuleCases.get r
   659       else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_of r, inst)) r
   660         |> pair (RuleCases.get r);
   661 
   662     fun ruleq goal =
   663       (case opt_rule of
   664         SOME r => Seq.single (inst_rule r)
   665       | NONE =>
   666           (get_coinductP ctxt goal @ get_coinductT ctxt inst)
   667           |> tap (trace_rules ctxt coinductN)
   668           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   669   in
   670     SUBGOAL_CASES (fn (goal, i) => fn st =>
   671       ruleq goal
   672       |> Seq.maps (RuleCases.consume [] facts)
   673       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   674         guess_instance rule i st
   675         |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
   676         |> Seq.maps (fn rule' =>
   677           CASES (make_cases is_open rule' cases)
   678             (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   679   end;
   680 
   681 end;
   682 
   683 
   684 
   685 (** concrete syntax **)
   686 
   687 val openN = "open";
   688 val arbitraryN = "arbitrary";
   689 val takingN = "taking";
   690 val ruleN = "rule";
   691 
   692 local
   693 
   694 fun single_rule [rule] = rule
   695   | single_rule _ = error "Single rule expected";
   696 
   697 fun named_rule k arg get =
   698   Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
   699     (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
   700       (case get (Context.proof_of context) name of SOME x => x
   701       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
   702 
   703 fun rule get_type get_pred =
   704   named_rule typeN Args.tyname get_type ||
   705   named_rule predN Args.const get_pred ||
   706   named_rule setN Args.const get_pred ||
   707   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
   708 
   709 val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;
   710 val induct_rule = rule lookup_inductT lookup_inductP;
   711 val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule;
   712 
   713 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
   714 
   715 val def_inst =
   716   ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
   717       -- Args.term) >> SOME ||
   718     inst >> Option.map (pair NONE);
   719 
   720 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
   721   error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
   722 
   723 fun unless_more_args scan = Scan.unless (Scan.lift
   724   ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
   725     Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
   726 
   727 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   728   Args.and_list1 (Scan.repeat (unless_more_args free))) [];
   729 
   730 val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
   731   Scan.repeat1 (unless_more_args inst)) [];
   732 
   733 in
   734 
   735 fun cases_meth src =
   736   Method.syntax (Args.mode openN --
   737     (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
   738   #> (fn ((is_open, (insts, opt_rule)), ctxt) =>
   739     Method.METHOD_CASES (fn facts =>
   740       Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
   741 
   742 fun induct_meth src =
   743   Method.syntax (Args.mode openN --
   744     (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
   745     (arbitrary -- taking -- Scan.option induct_rule))) src
   746   #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) =>
   747     Method.RAW_METHOD_CASES (fn facts =>
   748       Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
   749 
   750 fun coinduct_meth src =
   751   Method.syntax (Args.mode openN --
   752     (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
   753   #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) =>
   754     Method.RAW_METHOD_CASES (fn facts =>
   755       Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
   756 
   757 end;
   758 
   759 
   760 
   761 (** theory setup **)
   762 
   763 val setup =
   764   attrib_setup #>
   765   Method.add_methods
   766     [(casesN, cases_meth, "case analysis on types or predicates/sets"),
   767      (inductN, induct_meth, "induction on types or predicates/sets"),
   768      (coinductN, coinduct_meth, "coinduction on types or predicates/sets")];
   769 
   770 end;