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