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