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