src/Tools/induct_tacs.ML
author wenzelm
Mon Jun 23 15:51:38 2008 +0200 (2008-06-23)
changeset 27326 d3beec370964
child 27328 1f0ac20db386
permissions -rw-r--r--
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
     1 (*  Title:      HOL/Tools/induct_tacs.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Unstructured induction and cases analysis.
     6 *)
     7 
     8 signature INDUCT_TACS =
     9 sig
    10   val case_tac: Proof.context -> string -> int -> tactic
    11   val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
    12   val induct_tac: Proof.context -> string option list list -> int -> tactic
    13   val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
    14   val setup: theory -> theory
    15 end
    16 
    17 structure InductTacs: INDUCT_TACS =
    18 struct
    19 
    20 (* case analysis *)
    21 
    22 fun check_type ctxt t =
    23   let
    24     val u = singleton (Variable.polymorphic ctxt) t;
    25     val U = Term.fastype_of u;
    26     val _ = Term.is_TVar U andalso
    27       error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
    28   in (u, U) end;
    29 
    30 fun gen_case_tac ctxt0 (s, opt_rule) i st =
    31   let
    32     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    33     val rule =
    34       (case opt_rule of
    35         SOME rule => rule
    36       | NONE =>
    37           (case Induct.find_casesT ctxt
    38               (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of
    39             rule :: _ => rule
    40           | [] => @{thm case_split}));
    41     val _ = Method.trace ctxt [rule];
    42 
    43     val xi =
    44       (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
    45         Var (xi, _) :: _ => xi
    46       | _ => raise THM ("Malformed cases rule", 0, [rule]));
    47   in res_inst_tac ctxt [(xi, s)] rule i st end
    48   handle THM _ => Seq.empty;
    49 
    50 fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
    51 fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
    52 
    53 
    54 (* induction *)
    55 
    56 local
    57 
    58 fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
    59   | prep_var _ = NONE;
    60 
    61 fun prep_inst (concl, xs) =
    62   let val vs = Induct.vars_of concl
    63   in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    64 
    65 in
    66 
    67 fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
    68   let
    69     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    70     val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
    71 
    72     fun induct_var name =
    73       let
    74         val t = Syntax.read_term ctxt name;
    75         val (x, _) = Term.dest_Free t handle TERM _ =>
    76           error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t);
    77         val eq_x = fn Free (y, _) => x = y | _ => false;
    78         val _ =
    79           if Term.exists_subterm eq_x concl then ()
    80           else error ("No such variable in subgoal: " ^ Syntax.string_of_term ctxt t);
    81         val _ =
    82           if (exists o Term.exists_subterm) eq_x prems then
    83             warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
    84           else ();
    85       in #1 (check_type ctxt t) end;
    86 
    87     val argss = map (map (Option.map induct_var)) varss;
    88     val _ = forall null argss andalso raise THM ("No induction arguments", 0, []);
    89 
    90     val rule =
    91       (case opt_rules of
    92         SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
    93       | NONE =>
    94           (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
    95             (_, rule) :: _ => rule
    96           | [] => raise THM ("No induction rules", 0, [])));
    97 
    98     val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
    99     val _ = Method.trace ctxt [rule'];
   100 
   101     val concls = Logic.dest_conjunctions (Thm.concl_of rule);
   102     val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
   103       error "Induction rule has different numbers of variables";
   104   in res_inst_tac ctxt insts rule' i st end
   105   handle THM _ => Seq.empty;
   106 
   107 end;
   108 
   109 fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);
   110 fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules);
   111 
   112 
   113 (* method syntax *)
   114 
   115 local
   116 
   117 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
   118 val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
   119 val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
   120 
   121 val varss =
   122   Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
   123 
   124 in
   125 
   126 val setup =
   127   Method.add_methods
   128    [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
   129       "unstructured case analysis on types"),
   130     ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
   131       "unstructured induction on types")];
   132 
   133 end;
   134 
   135 end;
   136