src/Tools/cong_tac.ML
author wenzelm
Thu Feb 20 19:32:20 2014 +0100 (2014-02-20)
changeset 55627 95c8ef02f04b
parent 46219 426ed18eba43
child 58956 a816aa3ff391
permissions -rw-r--r--
tuned whitespace;
     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: thm -> int -> tactic
    10 end;
    11 
    12 structure Cong_Tac: CONG_TAC =
    13 struct
    14 
    15 fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
    16   let
    17     val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
    18     val goal = Thm.term_of cgoal;
    19   in
    20     (case Logic.strip_assums_concl goal of
    21       _ $ (_ $ (f $ x) $ (g $ y)) =>
    22         let
    23           val cong' = Thm.lift_rule cgoal cong;
    24           val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
    25           val ps = Logic.strip_params (Thm.concl_of cong');
    26           val insts =
    27             [(f', f), (g', g), (x', x), (y', y)]
    28             |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
    29         in
    30           fn st =>
    31             compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
    32               handle THM _ => no_tac st
    33         end
    34     | _ => no_tac)
    35   end);
    36 
    37 end;
    38