# HG changeset patch
# User haftmann
# Date 1366533678 -7200
# Node ID da12e44b2d652b8562d98cb34ee18771cc8fd786
# Parent  3da99469cc1b33f51aee3535ac6a92d785c97eb5
combined reify_data.ML into reflection.ML;
attempt to establish a more accessible and more consistent terminology;
more ML code in ML file rather than setup theory;
ML slightly tuned wrt. Isabelle coding conventions

diff -r 3da99469cc1b -r da12e44b2d65 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sat Apr 20 20:57:49 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Apr 21 10:41:18 2013 +0200
@@ -3533,7 +3533,7 @@
                       rtac @{thm impI}] i)
       THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
       THEN DETERM (TRY (filter_prems_tac (K false) i))
-      THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
+      THEN DETERM (Reflection.gen_reify_tac ctxt form_equations NONE i)
       THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
       THEN gen_eval_tac (approximation_conv ctxt) ctxt i))
  *} "real number approximation"
@@ -3632,7 +3632,7 @@
       THEN DETERM (TRY (filter_prems_tac (K false) 1)))
 
   fun reify_form context term = apply_tactic context term
-     (Reflection.genreify_tac @{context} form_equations NONE 1)
+     (Reflection.gen_reify_tac @{context} form_equations NONE 1)
 
   fun approx_form prec ctxt t =
           realify t
@@ -3650,7 +3650,7 @@
        |> foldr1 HOLogic.mk_conj))
 
   fun approx_arith prec ctxt t = realify t
-       |> Reflection.genreif ctxt form_equations
+       |> Reflection.gen_reify ctxt form_equations
        |> prop_of
        |> HOLogic.dest_Trueprop
        |> HOLogic.dest_eq |> snd
diff -r 3da99469cc1b -r da12e44b2d65 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Sat Apr 20 20:57:49 2013 +0200
+++ b/src/HOL/Library/Reflection.thy	Sun Apr 21 10:41:18 2013 +0200
@@ -8,15 +8,12 @@
 imports Main
 begin
 
-ML_file "reify_data.ML"
 ML_file "reflection.ML"
 
-setup {* Reify_Data.setup *}
-
 method_setup reify = {*
   Attrib.thms --
     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
-  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ fst (Reify_Data.get ctxt)) to))
+      (fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to))
 *} "partial automatic reification"
 
 method_setup reflection = {*
@@ -28,17 +25,12 @@
   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   val terms = thms >> map (term_of o Drule.dest_term);
 in
-  thms --
-  Scan.optional (keyword rulesN |-- thms) [] --
-  Scan.option (keyword onlyN |-- Args.term) >>
-  (fn ((eqs, ths), to) => fn ctxt =>
-    let
-      val (ceqs, cths) = Reify_Data.get ctxt
-      val corr_thms = ths @ cths
-      val raw_eqs = eqs @ ceqs
-    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
+  thms -- Scan.optional (keyword rulesN |-- thms) [] --
+    Scan.option (keyword onlyN |-- Args.term) >>
+  (fn ((user_eqs, user_thms), to) => fn ctxt =>
+        SIMPLE_METHOD' (Reflection.default_reflection_tac ctxt user_thms user_eqs to))
 end
-*}
+*} "partial automatic reflection"
 
 end
 
diff -r 3da99469cc1b -r da12e44b2d65 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Sat Apr 20 20:57:49 2013 +0200
+++ b/src/HOL/Library/reflection.ML	Sun Apr 21 10:41:18 2013 +0200
@@ -6,11 +6,17 @@
 
 signature REFLECTION =
 sig
-  val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
-  val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
+  val gen_reify: Proof.context -> thm list -> term -> thm
+  val gen_reify_tac: Proof.context -> thm list -> term option -> int -> tactic
   val gen_reflection_tac: Proof.context -> (cterm -> thm)
     -> thm list -> thm list -> term option -> int -> tactic
-  val genreif : Proof.context -> thm list -> term -> thm
+  val get_default: Proof.context -> { reification_eqs: thm list, correctness_thms: thm list }
+  val add_reification_eq: attribute
+  val del_reification_eq: attribute
+  val add_correctness_thm: attribute
+  val del_correctness_thm: attribute
+  val default_reify_tac: Proof.context -> thm list -> term option -> int -> tactic
+  val default_reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
 end;
 
 structure Reflection : REFLECTION =
@@ -69,11 +75,9 @@
   in  (vs', cong') end;
  (* congs is a list of pairs (P,th) where th is a theorem for *)
         (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *)
+
 val FWD = curry (op OF);
 
-
-exception REIF of string;
-
 fun dest_listT (Type (@{type_name "list"}, [T])) = T;
 
 fun rearrange congs =
@@ -84,7 +88,7 @@
     val (yes,no) = List.partition P congs
   in no @ yes end
 
-fun genreif ctxt raw_eqs t =
+fun gen_reify ctxt eqs t =
   let
     fun index_of t bds =
       let
@@ -154,7 +158,7 @@
                  map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
               val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
             in ((fts ~~ (replicate (length fts) ctxt),
-                 Library.apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
+                 apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
             end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
       end;
 
@@ -233,40 +237,32 @@
   (* Generic reification procedure: *)
   (* creates all needed cong rules and then just uses the theorem synthesis *)
 
-    fun mk_congs ctxt raw_eqs =
+    fun mk_congs ctxt eqs =
       let
-        val fs = fold_rev (fn eq =>
-                           insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop
-                           |> HOLogic.dest_eq |> fst |> strip_comb
-                           |> fst)) raw_eqs []
-        val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)
-                            ) fs []
-        val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
-        val thy = Proof_Context.theory_of ctxt'
-        val cert = cterm_of thy
-        val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t)))))
-                    (tys ~~ vs)
-        val is_Var = can dest_Var
-        fun insteq eq vs =
+        val fs = fold_rev (fn eq => insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop
+          |> HOLogic.dest_eq |> fst |> strip_comb
+          |> fst)) eqs [];
+        val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs [];
+        val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt;
+        val thy = Proof_Context.theory_of ctxt';
+        val cert = cterm_of thy;
+        val vstys = map (fn (t, v) => (t, SOME (cert (Free (v, t))))) (tys ~~ vs);
+        fun prep_eq eq =
           let
-            val subst = map (fn (v as Var(_, t)) => (cert v, (the o the) (AList.lookup (op =) vstys t)))
-                        (filter is_Var vs)
-          in Thm.instantiate ([],subst) eq
-          end
+            val (_, _ :: vs) = eq |> prop_of |> HOLogic.dest_Trueprop
+              |> HOLogic.dest_eq |> fst |> strip_comb;
+            val subst = map (fn (v as Var (_, t)) =>
+              (cert v, (the o the) (AList.lookup (op =) vstys t))) (filter is_Var vs);
+          in Thm.instantiate ([], subst) eq end;
+        val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
+        val bds = AList.make (K ([], [])) tys;
+      in (ps ~~ Variable.export ctxt' ctxt congs, bds) end
 
-        val bds = AList.make (fn _ => ([],[])) tys
-        val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop
-                                   |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl
-                                   |> (insteq eq)) raw_eqs
-        val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs)
-      in (ps ~~ (Variable.export ctxt' ctxt congs), bds)
-      end
-
-    val (congs, bds) = mk_congs ctxt raw_eqs
+    val (congs, bds) = mk_congs ctxt eqs
     val congs = rearrange congs
-    val (th, bds) = divide_and_conquer' (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) bds
-    fun is_listVar (Var (_,t)) = can dest_listT t
-         | is_listVar _ = false
+    val (th, bds) = divide_and_conquer' (decomp_genreif (mk_decompatom eqs) congs) (t,ctxt) bds
+    fun is_listVar (Var (_, t)) = can dest_listT t
+      | is_listVar _ = false
     val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
                   |> strip_comb |> snd |> filter is_listVar
     val cert = cterm_of (Proof_Context.theory_of ctxt)
@@ -276,29 +272,28 @@
     val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
     val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
                (fn _ => simp_tac ctxt 1)
-  in FWD trans [th'',th']
+  in FWD trans [th'',th'] end
+
+fun gen_reflect ctxt conv corr_thms eqs t =
+  let
+    val reify_thm = gen_reify ctxt eqs t;
+    fun try_corr thm =
+      SOME (FWD trans [reify_thm, thm RS sym]) handle THM _ => NONE;
+    val thm = case get_first try_corr corr_thms
+     of NONE => error "No suitable correctness theorem found"
+      | SOME thm => thm;
+    val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) thm;
+    val rth = conv ft;
+  in
+    thm
+    |> simplify (put_simpset HOL_basic_ss ctxt addsimps [rth])
+    |> simplify (put_simpset HOL_basic_ss ctxt addsimps eqs addsimps @{thms nth_Cons_0 nth_Cons_Suc})
   end
 
-
-fun genreflect ctxt conv corr_thms raw_eqs t =
-  let
-    val reifth = genreif ctxt raw_eqs t
-    fun trytrans [] = error "No suitable correctness theorem found"
-      | trytrans (th::ths) =
-           (FWD trans [reifth, th RS sym] handle THM _ => trytrans ths)
-    val th = trytrans corr_thms
-    val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th
-    val rth = conv ft
-  in
-    simplify
-      (put_simpset HOL_basic_ss ctxt addsimps raw_eqs addsimps @{thms nth_Cons_0 nth_Cons_Suc})
-      (simplify (put_simpset HOL_basic_ss ctxt addsimps [rth]) th)
-  end
-
-fun genreify_tac ctxt eqs to = SUBGOAL (fn (goal, i) =>
+fun gen_reify_tac ctxt eqs to = SUBGOAL (fn (goal, i) =>
   let
     val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
-    val th = genreif ctxt eqs t RS ssubst
+    val th = gen_reify ctxt eqs t RS ssubst
   in rtac th i end);
 
     (* Reflection calls reification and uses the correctness *)
@@ -306,11 +301,50 @@
 fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) =>
   let
     val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
-    val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
+    val th = gen_reflect ctxt conv corr_thms raw_eqs t RS ssubst
   in rtac th i THEN TRY (rtac TrueI i) end);  (* FIXME THEN_ALL_NEW !? *)
 
-fun reflection_tac ctxt = gen_reflection_tac ctxt
-  (Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt));
-  (*FIXME why Code_Evaluation.dynamic_conv?  very specific...*)
+structure Data = Generic_Data
+(
+  type T = thm list * thm list;
+  val empty = ([], []);
+  val extend = I;
+  fun merge ((ths1, rths1), (ths2, rths2)) =
+    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
+);
+
+fun get_default ctxt =
+  let
+    val (reification_eqs, correctness_thms) = Data.get (Context.Proof ctxt);
+  in { reification_eqs = reification_eqs, correctness_thms = correctness_thms } end;
+
+val add_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
+val del_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
+val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
+val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
+
+val _ = Context.>> (Context.map_theory
+  (Attrib.setup @{binding reify}
+    (Attrib.add_del add_reification_eq del_reification_eq) "declare reification equations" #>
+  Attrib.setup @{binding reflection}
+    (Attrib.add_del add_correctness_thm del_correctness_thm) "declare reflection correctness theorems"));
+
+fun default_reify_tac ctxt user_eqs =
+  let
+    val { reification_eqs = default_eqs, correctness_thms = _ } =
+      get_default ctxt;
+    val eqs = user_eqs @ default_eqs; (*FIXME fold update?*)
+  in gen_reify_tac ctxt eqs end;
+
+fun default_reflection_tac ctxt user_thms user_eqs =
+  let
+    val { reification_eqs = default_eqs, correctness_thms = default_thms } =
+      get_default ctxt;
+    val corr_thms = user_thms @ default_thms; (*FIXME fold update?*)
+    val eqs = user_eqs @ default_eqs; (*FIXME fold update?*)
+    val conv = Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt);
+      (*FIXME why Code_Evaluation.dynamic_conv? very specific*)
+  in gen_reflection_tac ctxt conv corr_thms eqs end;
+
 
 end
diff -r 3da99469cc1b -r da12e44b2d65 src/HOL/Library/reify_data.ML
--- a/src/HOL/Library/reify_data.ML	Sat Apr 20 20:57:49 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(*  Title:      HOL/Library/reify_data.ML
-    Author:     Amine Chaieb, TU Muenchen
-
-Data for the reification and reflection methods.
-*)
-
-signature REIFY_DATA =
-sig
-  val get: Proof.context -> thm list * thm list
-  val add: attribute
-  val del: attribute
-  val radd: attribute
-  val rdel: attribute
-  val setup: theory -> theory
-end;
-
-structure Reify_Data : REIFY_DATA =
-struct
-
-structure Data = Generic_Data
-(
-  type T = thm list * thm list;
-  val empty = ([], []);
-  val extend = I;
-  fun merge ((ths1, rths1), (ths2, rths2)) =
-    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
-);
-
-val get = Data.get o Context.Proof;
-
-val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
-val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
-val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
-val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
-
-val setup =
-  Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
-  Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
-
-end;