src/Tools/cong_tac.ML
changeset 32733 71618deaf777
child 46219 426ed18eba43
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/cong_tac.ML	Mon Sep 28 22:47:34 2009 +0200
@@ -0,0 +1,37 @@
+(*  Title:      Tools/cong_tac.ML
+    Author:     Stefan Berghofer, TU Muenchen
+
+Congruence tactic based on explicit instantiation.
+*)
+
+signature CONG_TAC =
+sig
+  val cong_tac: thm -> int -> tactic
+end;
+
+structure Cong_Tac: CONG_TAC =
+struct
+
+fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
+  let
+    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
+    val goal = Thm.term_of cgoal;
+  in
+    (case Logic.strip_assums_concl goal of
+      _ $ (_ $ (f $ x) $ (g $ y)) =>
+        let
+          val cong' = Thm.lift_rule cgoal cong;
+          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
+            Logic.strip_assums_concl (Thm.prop_of cong');
+          val ps = Logic.strip_params (Thm.concl_of cong');
+          val insts = [(f', f), (g', g), (x', x), (y', y)]
+            |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
+        in
+          fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
+            handle THM _ => no_tac st
+        end
+    | _ => no_tac)
+  end);
+
+end;
+