# HG changeset patch
# User haftmann
# Date 1369985432 -7200
# Node ID 329c4143815462d06322e86040afde0a24997cf5
# Parent  9b4c04da53b14afbad66e07840c4519a416a39e4
reflection without evaluation

diff -r 9b4c04da53b1 -r 329c41438154 src/HOL/Tools/reflection.ML
--- a/src/HOL/Tools/reflection.ML	Fri May 31 09:30:32 2013 +0200
+++ b/src/HOL/Tools/reflection.ML	Fri May 31 09:30:32 2013 +0200
@@ -8,8 +8,10 @@
 sig
   val reify: Proof.context -> thm list -> conv
   val reify_tac: Proof.context -> thm list -> term option -> int -> tactic
-  val reflect: Proof.context -> thm list -> thm list -> conv -> conv
-  val reflection_tac: Proof.context -> thm list -> thm list -> conv -> term option -> int -> tactic
+  val reflect: Proof.context -> thm list -> thm list -> conv
+  val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
+  val reflect_with_eval: Proof.context -> thm list -> thm list -> conv -> conv
+  val reflection_with_eval_tac: Proof.context -> thm list -> thm list -> conv -> term option -> int -> tactic
   val get_default: Proof.context -> { reification_eqs: thm list, correctness_thms: thm list }
   val add_reification_eq: attribute
   val del_reification_eq: attribute
@@ -30,7 +32,7 @@
 
 val pure_subst = @{lemma "x == y ==> PROP P y ==> PROP P x" by simp}
 
-fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn { context, concl, ... } =>
+fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn { concl, ... } =>
   let
     val ct = case some_t
      of NONE => Thm.dest_arg concl
@@ -208,7 +210,7 @@
           | get_nths (Abs (_, _, t')) = get_nths t'
           | get_nths _ = I;
 
-        fun tryeqs [] bds = error "Can not find the atoms equation"
+        fun tryeqs [] bds = error "Cannot find the atoms equation"
           | tryeqs (eq :: eqs) bds = ((
               let
                 val rhs = eq |> prop_of |> HOLogic.dest_Trueprop  |> HOLogic.dest_eq |> snd;
@@ -297,10 +299,19 @@
     val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
   in Thm.transitive th'' th' end;
 
+fun reify_tac ctxt eqs =
+  lift_conv ctxt (reify ctxt eqs);
+
 fun subst_correctness corr_thms ct =
   Conv.rewrs_conv (map (Thm.symmetric o mk_eq) corr_thms) ct
     handle CTERM _ => error "No suitable correctness theorem found";
 
+fun reflect ctxt corr_thms eqs =
+  (reify ctxt eqs) then_conv (subst_correctness corr_thms)
+
+fun reflection_tac ctxt corr_thms eqs =
+  lift_conv ctxt (reflect ctxt corr_thms eqs);
+
 fun first_arg_conv conv =
   let
     fun conv' ct =
@@ -309,14 +320,11 @@
       else Conv.combination_conv Conv.all_conv conv ct;
   in conv' end;
 
-fun reflect ctxt corr_thms eqs conv =
-  (reify ctxt eqs) then_conv (subst_correctness corr_thms)
-  then_conv (first_arg_conv conv) then_conv (dereify ctxt eqs);
+fun reflect_with_eval ctxt corr_thms eqs conv =
+  (reflect ctxt corr_thms eqs) then_conv (first_arg_conv conv) then_conv (dereify ctxt eqs);
 
-fun reify_tac ctxt eqs = lift_conv ctxt (reify ctxt eqs);
-
-fun reflection_tac ctxt corr_thms eqs conv =
-  lift_conv ctxt (reflect ctxt corr_thms eqs conv);
+fun reflection_with_eval_tac ctxt corr_thms eqs conv =
+  lift_conv ctxt (reflect_with_eval ctxt corr_thms eqs conv);
 
 structure Data = Generic_Data
 (
@@ -356,9 +364,6 @@
       get_default ctxt;
     val corr_thms = fold Thm.add_thm user_thms default_thms;
     val eqs = fold Thm.add_thm user_eqs default_eqs; 
-    val conv = Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt);
-      (*FIXME why Code_Evaluation.dynamic_conv? very specific*)
-  in reflection_tac ctxt corr_thms eqs conv end;
+  in reflection_tac ctxt corr_thms eqs end;
 
-
-end
+end;