src/Tools/cong_tac.ML
author wenzelm
Mon Sep 28 22:47:34 2009 +0200 (2009-09-28)
changeset 32733 71618deaf777
child 46219 426ed18eba43
permissions -rw-r--r--
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
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@32733
     9
  val cong_tac: 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@32733
    15
fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
wenzelm@32733
    16
  let
wenzelm@32733
    17
    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
wenzelm@32733
    18
    val goal = Thm.term_of cgoal;
wenzelm@32733
    19
  in
wenzelm@32733
    20
    (case Logic.strip_assums_concl goal of
wenzelm@32733
    21
      _ $ (_ $ (f $ x) $ (g $ y)) =>
wenzelm@32733
    22
        let
wenzelm@32733
    23
          val cong' = Thm.lift_rule cgoal cong;
wenzelm@32733
    24
          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
wenzelm@32733
    25
            Logic.strip_assums_concl (Thm.prop_of cong');
wenzelm@32733
    26
          val ps = Logic.strip_params (Thm.concl_of cong');
wenzelm@32733
    27
          val insts = [(f', f), (g', g), (x', x), (y', y)]
wenzelm@32733
    28
            |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
wenzelm@32733
    29
        in
wenzelm@32733
    30
          fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
wenzelm@32733
    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