src/Tools/cong_tac.ML
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 55627 95c8ef02f04b
child 58956 a816aa3ff391
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
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@55627
    24
          val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
wenzelm@32733
    25
          val ps = Logic.strip_params (Thm.concl_of cong');
wenzelm@55627
    26
          val insts =
wenzelm@55627
    27
            [(f', f), (g', g), (x', x), (y', y)]
wenzelm@46219
    28
            |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
wenzelm@32733
    29
        in
wenzelm@55627
    30
          fn st =>
wenzelm@55627
    31
            compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
wenzelm@55627
    32
              handle THM _ => no_tac st
wenzelm@32733
    33
        end
wenzelm@32733
    34
    | _ => no_tac)
wenzelm@32733
    35
  end);
wenzelm@32733
    36
wenzelm@32733
    37
end;
wenzelm@32733
    38