wenzelm@32733: (*  Title:      Tools/cong_tac.ML
wenzelm@32733:     Author:     Stefan Berghofer, TU Muenchen
wenzelm@32733: 
wenzelm@32733: Congruence tactic based on explicit instantiation.
wenzelm@32733: *)
wenzelm@32733: 
wenzelm@32733: signature CONG_TAC =
wenzelm@32733: sig
wenzelm@32733:   val cong_tac: thm -> int -> tactic
wenzelm@32733: end;
wenzelm@32733: 
wenzelm@32733: structure Cong_Tac: CONG_TAC =
wenzelm@32733: struct
wenzelm@32733: 
wenzelm@32733: fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
wenzelm@32733:   let
wenzelm@32733:     val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
wenzelm@32733:     val goal = Thm.term_of cgoal;
wenzelm@32733:   in
wenzelm@32733:     (case Logic.strip_assums_concl goal of
wenzelm@32733:       _ $ (_ $ (f $ x) $ (g $ y)) =>
wenzelm@32733:         let
wenzelm@32733:           val cong' = Thm.lift_rule cgoal cong;
wenzelm@32733:           val _ $ (_ $ (f' $ x') $ (g' $ y')) =
wenzelm@32733:             Logic.strip_assums_concl (Thm.prop_of cong');
wenzelm@32733:           val ps = Logic.strip_params (Thm.concl_of cong');
wenzelm@32733:           val insts = [(f', f), (g', g), (x', x), (y', y)]
wenzelm@32733:             |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
wenzelm@32733:         in
wenzelm@32733:           fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
wenzelm@32733:             handle THM _ => no_tac st
wenzelm@32733:         end
wenzelm@32733:     | _ => no_tac)
wenzelm@32733:   end);
wenzelm@32733: 
wenzelm@32733: end;
wenzelm@32733: