src/Tools/cong_tac.ML
author traytel
Thu Sep 29 09:37:59 2011 +0200 (2011-09-29)
changeset 45102 7bb89635eb51
parent 32733 71618deaf777
child 46219 426ed18eba43
permissions -rw-r--r--
correct coercion generation in case of unknown map functions
     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')) =
    25             Logic.strip_assums_concl (Thm.prop_of cong');
    26           val ps = Logic.strip_params (Thm.concl_of cong');
    27           val insts = [(f', f), (g', g), (x', x), (y', y)]
    28             |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
    29         in
    30           fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
    31             handle THM _ => no_tac st
    32         end
    33     | _ => no_tac)
    34   end);
    35 
    36 end;
    37