# HG changeset patch
# User haftmann
# Date 1166426494 -3600
# Node ID cfc07819bb4713f6c4f16bc1fc784ef193db8d38
# Parent  e871f57b1adbdf74b4379bae820a530805c8ff19
added gen_reflection_tac

diff -r e871f57b1adb -r cfc07819bb47 src/HOL/ex/reflection.ML
--- a/src/HOL/ex/reflection.ML	Mon Dec 18 08:21:33 2006 +0100
+++ b/src/HOL/ex/reflection.ML	Mon Dec 18 08:21:34 2006 +0100
@@ -8,6 +8,8 @@
 signature REFLECTION = sig
   val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
   val reflection_tac: Proof.context -> thm list -> term option -> int -> tactic
+  val gen_reflection_tac: Proof.context -> (cterm -> thm)
+    -> thm list -> term option -> int -> tactic
 end;
 
 structure Reflection : REFLECTION
@@ -279,10 +281,10 @@
  in FWD trans [th'',th']
  end;
 
-fun genreflect ctxt corr_thm raw_eqs t =
+fun genreflect ctxt conv corr_thm raw_eqs t =
     let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym]
         val ft = (snd o Thm.dest_comb o snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) th
-        val rth = NBE.normalization_conv ft
+        val rth = conv ft
     in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
                 (simplify (HOL_basic_ss addsimps [rth]) th)
     end
@@ -297,11 +299,14 @@
 
     (* Reflection calls reification and uses the correctness *)
         (* theorem assumed to be the dead of the list *)
- fun reflection_tac ctxt (corr_thm::raw_eqs) to i =
-    (fn st =>
-        let val P = (HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)))
-            val t = (case to of NONE => P | SOME x => x)
-            val th = (genreflect ctxt corr_thm raw_eqs t) RS ssubst
-        in rtac th i st end);
+fun gen_reflection_tac ctxt conv (corr_thm :: raw_eqs) to i = (fn st =>
+  let
+    val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1));
+    val t = the_default P to;
+    val th = genreflect ctxt conv corr_thm raw_eqs t
+      RS ssubst;
+  in rtac th i st end);
+
+fun reflection_tac ctxt = gen_reflection_tac ctxt NBE.normalization_conv;
 
 end