src/Tools/cong_tac.ML
author wenzelm
Sun Jul 26 17:24:54 2015 +0200 (2015-07-26)
changeset 60784 4f590c08fd5d
parent 59642 929984c529d3
permissions -rw-r--r--
updated to infer_instantiate;
wenzelm@32733
     1
(*  Title:      Tools/cong_tac.ML
wenzelm@32733
     2
    Author:     Stefan Berghofer, TU Muenchen
wenzelm@32733
     3
wenzelm@32733
     4
Congruence tactic based on explicit instantiation.
wenzelm@32733
     5
*)
wenzelm@32733
     6
wenzelm@32733
     7
signature CONG_TAC =
wenzelm@32733
     8
sig
wenzelm@58956
     9
  val cong_tac: Proof.context -> thm -> int -> tactic
wenzelm@32733
    10
end;
wenzelm@32733
    11
wenzelm@32733
    12
structure Cong_Tac: CONG_TAC =
wenzelm@32733
    13
struct
wenzelm@32733
    14
wenzelm@58956
    15
fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
wenzelm@32733
    16
  let
wenzelm@32733
    17
    val goal = Thm.term_of cgoal;
wenzelm@32733
    18
  in
wenzelm@32733
    19
    (case Logic.strip_assums_concl goal of
wenzelm@32733
    20
      _ $ (_ $ (f $ x) $ (g $ y)) =>
wenzelm@32733
    21
        let
wenzelm@32733
    22
          val cong' = Thm.lift_rule cgoal cong;
wenzelm@55627
    23
          val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
wenzelm@32733
    24
          val ps = Logic.strip_params (Thm.concl_of cong');
wenzelm@55627
    25
          val insts =
wenzelm@60784
    26
            [(f', f), (g', g), (x', x), (y', y)] |> map (fn (t, u) =>
wenzelm@60784
    27
              (#1 (dest_Var (head_of t)), Thm.cterm_of ctxt (fold_rev Term.abs ps u)));
wenzelm@32733
    28
        in
wenzelm@55627
    29
          fn st =>
wenzelm@60784
    30
            compose_tac ctxt (false, infer_instantiate ctxt insts cong', 2) i st
wenzelm@55627
    31
              handle THM _ => no_tac st
wenzelm@32733
    32
        end
wenzelm@32733
    33
    | _ => no_tac)
wenzelm@32733
    34
  end);
wenzelm@32733
    35
wenzelm@32733
    36
end;
wenzelm@32733
    37