moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);

--- a/src/HOL/HOL.thy	Mon Sep 28 21:35:57 2009 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 28 22:47:34 2009 +0200
@@ -15,6 +15,7 @@
   "~~/src/Tools/IsaPlanner/rw_inst.ML"
   "~~/src/Tools/intuitionistic.ML"
   "~~/src/Tools/project_rule.ML"
+  "~~/src/Tools/cong_tac.ML"
   "~~/src/Provers/hypsubst.ML"
   "~~/src/Provers/splitter.ML"
   "~~/src/Provers/classical.ML"
@@ -240,15 +241,15 @@
   by (rule subst)
 
 
-subsubsection {*Congruence rules for application*}
+subsubsection {* Congruence rules for application *}
 
-(*similar to AP_THM in Gordon's HOL*)
+text {* Similar to @{text AP_THM} in Gordon's HOL. *}
 lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
 apply (erule subst)
 apply (rule refl)
 done
 
-(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
+text {* Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}. *}
 lemma arg_cong: "x=y ==> f(x)=f(y)"
 apply (erule subst)
 apply (rule refl)
@@ -259,13 +260,15 @@
 apply (rule refl)
 done
 
-lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
+lemma cong: "[| f = g; (x::'a) = y |] ==> f x = g y"
 apply (erule subst)+
 apply (rule refl)
 done
 
+ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *}
 
-subsubsection {*Equality of booleans -- iff*}
+
+subsubsection {* Equality of booleans -- iff *}
 
 lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q"
   by (iprover intro: iff [THEN mp, THEN mp] impI assms)

--- a/src/HOL/IsaMakefile	Mon Sep 28 21:35:57 2009 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 28 22:47:34 2009 +0200
@@ -87,30 +87,31 @@
   $(SRC)/Provers/hypsubst.ML \
   $(SRC)/Provers/quantifier1.ML \
   $(SRC)/Provers/splitter.ML \
-  $(SRC)/Tools/IsaPlanner/isand.ML \
-  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
-  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
-  $(SRC)/Tools/IsaPlanner/zipper.ML \
-  $(SRC)/Tools/atomize_elim.ML \
-  $(SRC)/Tools/auto_solve.ML \
   $(SRC)/Tools/Code/code_haskell.ML \
   $(SRC)/Tools/Code/code_ml.ML \
   $(SRC)/Tools/Code/code_preproc.ML \
   $(SRC)/Tools/Code/code_printer.ML \
   $(SRC)/Tools/Code/code_target.ML \
   $(SRC)/Tools/Code/code_thingol.ML \
+  $(SRC)/Tools/Code_Generator.thy \
+  $(SRC)/Tools/IsaPlanner/isand.ML \
+  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
+  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
+  $(SRC)/Tools/IsaPlanner/zipper.ML \
+  $(SRC)/Tools/atomize_elim.ML \
+  $(SRC)/Tools/auto_solve.ML \
   $(SRC)/Tools/coherent.ML \
+  $(SRC)/Tools/cong_tac.ML \
   $(SRC)/Tools/eqsubst.ML \
   $(SRC)/Tools/induct.ML \
+  $(SRC)/Tools/induct_tacs.ML \
   $(SRC)/Tools/intuitionistic.ML \
-  $(SRC)/Tools/induct_tacs.ML \
+  $(SRC)/Tools/more_conv.ML \
   $(SRC)/Tools/nbe.ML \
+  $(SRC)/Tools/project_rule.ML \
   $(SRC)/Tools/quickcheck.ML \
-  $(SRC)/Tools/project_rule.ML \
   $(SRC)/Tools/random_word.ML \
   $(SRC)/Tools/value.ML \
-  $(SRC)/Tools/Code_Generator.thy \
-  $(SRC)/Tools/more_conv.ML \
   HOL.thy \
   Tools/hologic.ML \
   Tools/recfun_codegen.ML \
@@ -130,9 +131,9 @@
   Inductive.thy \
   Lattices.thy \
   Nat.thy \
+  Option.thy \
   OrderedGroup.thy \
   Orderings.thy \
-  Option.thy \
   Plain.thy \
   Power.thy \
   Predicate.thy \
@@ -215,8 +216,8 @@
   Equiv_Relations.thy \
   Groebner_Basis.thy \
   Hilbert_Choice.thy \
+  Int.thy \
   IntDiv.thy \
-  Int.thy \
   List.thy \
   Main.thy \
   Map.thy \
@@ -280,8 +281,8 @@
 
 $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
   Archimedean_Field.thy \
+  Complex.thy \
   Complex_Main.thy \
-  Complex.thy \
   Deriv.thy \
   Fact.thy \
   GCD.thy \
@@ -294,18 +295,18 @@
   MacLaurin.thy \
   Nat_Transfer.thy \
   NthRoot.thy \
+  PReal.thy \
+  Parity.thy \
+  RComplete.thy \
+  Rational.thy \
+  Real.thy \
+  RealDef.thy \
+  RealPow.thy \
+  RealVector.thy \
   SEQ.thy \
   Series.thy \
   Taylor.thy \
   Transcendental.thy \
-  Parity.thy \
-  PReal.thy \
-  Rational.thy \
-  RComplete.thy \
-  RealDef.thy \
-  RealPow.thy \
-  Real.thy \
-  RealVector.thy \
   Tools/float_syntax.ML \
   Tools/transfer.ML \
   Tools/Qelim/ferrante_rackoff_data.ML \

--- a/src/HOL/Nominal/nominal_permeq.ML	Mon Sep 28 21:35:57 2009 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Sep 28 22:47:34 2009 +0200
@@ -228,11 +228,7 @@
         addsimprocs [perm_compose_simproc]) i,
       asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st);
 
-
-(* applying Stefan's smart congruence tac *)
-fun apply_cong_tac i = 
-    ("application of congruence",
-     (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
+fun apply_cong_tac i = ("application of congruence", cong_tac i);
 
 
 (* unfolds the definition of permutations     *)

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 21:35:57 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 22:47:34 2009 +0200
@@ -35,7 +35,6 @@
 
   val app_bnds : term -> int -> term
 
-  val cong_tac : int -> tactic
   val indtac : thm -> string list -> int -> tactic
   val exh_tac : (string -> thm) -> int -> tactic
 
@@ -112,21 +111,6 @@
 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
 
 
-fun cong_tac i st = (case Logic.strip_assums_concl
-  (List.nth (prems_of st, i - 1)) of
-    _ $ (_ $ (f $ x) $ (g $ y)) =>
-      let
-        val cong' = Thm.lift_rule (Thm.cprem_of st i) cong;
-        val _ $ (_ $ (f' $ x') $ (g' $ y')) =
-          Logic.strip_assums_concl (prop_of cong');
-        val insts = map (pairself (cterm_of (Thm.theory_of_thm st)) o
-          apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
-            apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
-      in compose_tac (false, cterm_instantiate insts cong', 2) i st
-        handle THM _ => no_tac st
-      end
-  | _ => no_tac st);
-
 (* instantiate induction rule *)
 
 fun indtac indrule indnames i st =

--- /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;
+