combined reify_data.ML into reflection.ML;
authorhaftmann
Sun Apr 21 10:41:18 2013 +0200 (2013-04-21)
changeset 51723da12e44b2d65
parent 51722 3da99469cc1b
child 51724 80f9906ede19
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
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Reflection.thy
src/HOL/Library/reflection.ML
src/HOL/Library/reify_data.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sat Apr 20 20:57:49 2013 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Apr 21 10:41:18 2013 +0200
     1.3 @@ -3533,7 +3533,7 @@
     1.4                        rtac @{thm impI}] i)
     1.5        THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
     1.6        THEN DETERM (TRY (filter_prems_tac (K false) i))
     1.7 -      THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
     1.8 +      THEN DETERM (Reflection.gen_reify_tac ctxt form_equations NONE i)
     1.9        THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
    1.10        THEN gen_eval_tac (approximation_conv ctxt) ctxt i))
    1.11   *} "real number approximation"
    1.12 @@ -3632,7 +3632,7 @@
    1.13        THEN DETERM (TRY (filter_prems_tac (K false) 1)))
    1.14  
    1.15    fun reify_form context term = apply_tactic context term
    1.16 -     (Reflection.genreify_tac @{context} form_equations NONE 1)
    1.17 +     (Reflection.gen_reify_tac @{context} form_equations NONE 1)
    1.18  
    1.19    fun approx_form prec ctxt t =
    1.20            realify t
    1.21 @@ -3650,7 +3650,7 @@
    1.22         |> foldr1 HOLogic.mk_conj))
    1.23  
    1.24    fun approx_arith prec ctxt t = realify t
    1.25 -       |> Reflection.genreif ctxt form_equations
    1.26 +       |> Reflection.gen_reify ctxt form_equations
    1.27         |> prop_of
    1.28         |> HOLogic.dest_Trueprop
    1.29         |> HOLogic.dest_eq |> snd
     2.1 --- a/src/HOL/Library/Reflection.thy	Sat Apr 20 20:57:49 2013 +0200
     2.2 +++ b/src/HOL/Library/Reflection.thy	Sun Apr 21 10:41:18 2013 +0200
     2.3 @@ -8,15 +8,12 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -ML_file "reify_data.ML"
     2.8  ML_file "reflection.ML"
     2.9  
    2.10 -setup {* Reify_Data.setup *}
    2.11 -
    2.12  method_setup reify = {*
    2.13    Attrib.thms --
    2.14      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
    2.15 -  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ fst (Reify_Data.get ctxt)) to))
    2.16 +      (fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to))
    2.17  *} "partial automatic reification"
    2.18  
    2.19  method_setup reflection = {*
    2.20 @@ -28,17 +25,12 @@
    2.21    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    2.22    val terms = thms >> map (term_of o Drule.dest_term);
    2.23  in
    2.24 -  thms --
    2.25 -  Scan.optional (keyword rulesN |-- thms) [] --
    2.26 -  Scan.option (keyword onlyN |-- Args.term) >>
    2.27 -  (fn ((eqs, ths), to) => fn ctxt =>
    2.28 -    let
    2.29 -      val (ceqs, cths) = Reify_Data.get ctxt
    2.30 -      val corr_thms = ths @ cths
    2.31 -      val raw_eqs = eqs @ ceqs
    2.32 -    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
    2.33 +  thms -- Scan.optional (keyword rulesN |-- thms) [] --
    2.34 +    Scan.option (keyword onlyN |-- Args.term) >>
    2.35 +  (fn ((user_eqs, user_thms), to) => fn ctxt =>
    2.36 +        SIMPLE_METHOD' (Reflection.default_reflection_tac ctxt user_thms user_eqs to))
    2.37  end
    2.38 -*}
    2.39 +*} "partial automatic reflection"
    2.40  
    2.41  end
    2.42  
     3.1 --- a/src/HOL/Library/reflection.ML	Sat Apr 20 20:57:49 2013 +0200
     3.2 +++ b/src/HOL/Library/reflection.ML	Sun Apr 21 10:41:18 2013 +0200
     3.3 @@ -6,11 +6,17 @@
     3.4  
     3.5  signature REFLECTION =
     3.6  sig
     3.7 -  val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
     3.8 -  val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
     3.9 +  val gen_reify: Proof.context -> thm list -> term -> thm
    3.10 +  val gen_reify_tac: Proof.context -> thm list -> term option -> int -> tactic
    3.11    val gen_reflection_tac: Proof.context -> (cterm -> thm)
    3.12      -> thm list -> thm list -> term option -> int -> tactic
    3.13 -  val genreif : Proof.context -> thm list -> term -> thm
    3.14 +  val get_default: Proof.context -> { reification_eqs: thm list, correctness_thms: thm list }
    3.15 +  val add_reification_eq: attribute
    3.16 +  val del_reification_eq: attribute
    3.17 +  val add_correctness_thm: attribute
    3.18 +  val del_correctness_thm: attribute
    3.19 +  val default_reify_tac: Proof.context -> thm list -> term option -> int -> tactic
    3.20 +  val default_reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
    3.21  end;
    3.22  
    3.23  structure Reflection : REFLECTION =
    3.24 @@ -69,11 +75,9 @@
    3.25    in  (vs', cong') end;
    3.26   (* congs is a list of pairs (P,th) where th is a theorem for *)
    3.27          (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *)
    3.28 +
    3.29  val FWD = curry (op OF);
    3.30  
    3.31 -
    3.32 -exception REIF of string;
    3.33 -
    3.34  fun dest_listT (Type (@{type_name "list"}, [T])) = T;
    3.35  
    3.36  fun rearrange congs =
    3.37 @@ -84,7 +88,7 @@
    3.38      val (yes,no) = List.partition P congs
    3.39    in no @ yes end
    3.40  
    3.41 -fun genreif ctxt raw_eqs t =
    3.42 +fun gen_reify ctxt eqs t =
    3.43    let
    3.44      fun index_of t bds =
    3.45        let
    3.46 @@ -154,7 +158,7 @@
    3.47                   map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    3.48                val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
    3.49              in ((fts ~~ (replicate (length fts) ctxt),
    3.50 -                 Library.apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
    3.51 +                 apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
    3.52              end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
    3.53        end;
    3.54  
    3.55 @@ -233,40 +237,32 @@
    3.56    (* Generic reification procedure: *)
    3.57    (* creates all needed cong rules and then just uses the theorem synthesis *)
    3.58  
    3.59 -    fun mk_congs ctxt raw_eqs =
    3.60 +    fun mk_congs ctxt eqs =
    3.61        let
    3.62 -        val fs = fold_rev (fn eq =>
    3.63 -                           insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop
    3.64 -                           |> HOLogic.dest_eq |> fst |> strip_comb
    3.65 -                           |> fst)) raw_eqs []
    3.66 -        val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)
    3.67 -                            ) fs []
    3.68 -        val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
    3.69 -        val thy = Proof_Context.theory_of ctxt'
    3.70 -        val cert = cterm_of thy
    3.71 -        val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t)))))
    3.72 -                    (tys ~~ vs)
    3.73 -        val is_Var = can dest_Var
    3.74 -        fun insteq eq vs =
    3.75 +        val fs = fold_rev (fn eq => insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop
    3.76 +          |> HOLogic.dest_eq |> fst |> strip_comb
    3.77 +          |> fst)) eqs [];
    3.78 +        val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs [];
    3.79 +        val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt;
    3.80 +        val thy = Proof_Context.theory_of ctxt';
    3.81 +        val cert = cterm_of thy;
    3.82 +        val vstys = map (fn (t, v) => (t, SOME (cert (Free (v, t))))) (tys ~~ vs);
    3.83 +        fun prep_eq eq =
    3.84            let
    3.85 -            val subst = map (fn (v as Var(_, t)) => (cert v, (the o the) (AList.lookup (op =) vstys t)))
    3.86 -                        (filter is_Var vs)
    3.87 -          in Thm.instantiate ([],subst) eq
    3.88 -          end
    3.89 +            val (_, _ :: vs) = eq |> prop_of |> HOLogic.dest_Trueprop
    3.90 +              |> HOLogic.dest_eq |> fst |> strip_comb;
    3.91 +            val subst = map (fn (v as Var (_, t)) =>
    3.92 +              (cert v, (the o the) (AList.lookup (op =) vstys t))) (filter is_Var vs);
    3.93 +          in Thm.instantiate ([], subst) eq end;
    3.94 +        val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
    3.95 +        val bds = AList.make (K ([], [])) tys;
    3.96 +      in (ps ~~ Variable.export ctxt' ctxt congs, bds) end
    3.97  
    3.98 -        val bds = AList.make (fn _ => ([],[])) tys
    3.99 -        val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop
   3.100 -                                   |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl
   3.101 -                                   |> (insteq eq)) raw_eqs
   3.102 -        val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs)
   3.103 -      in (ps ~~ (Variable.export ctxt' ctxt congs), bds)
   3.104 -      end
   3.105 -
   3.106 -    val (congs, bds) = mk_congs ctxt raw_eqs
   3.107 +    val (congs, bds) = mk_congs ctxt eqs
   3.108      val congs = rearrange congs
   3.109 -    val (th, bds) = divide_and_conquer' (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) bds
   3.110 -    fun is_listVar (Var (_,t)) = can dest_listT t
   3.111 -         | is_listVar _ = false
   3.112 +    val (th, bds) = divide_and_conquer' (decomp_genreif (mk_decompatom eqs) congs) (t,ctxt) bds
   3.113 +    fun is_listVar (Var (_, t)) = can dest_listT t
   3.114 +      | is_listVar _ = false
   3.115      val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
   3.116                    |> strip_comb |> snd |> filter is_listVar
   3.117      val cert = cterm_of (Proof_Context.theory_of ctxt)
   3.118 @@ -276,29 +272,28 @@
   3.119      val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
   3.120      val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
   3.121                 (fn _ => simp_tac ctxt 1)
   3.122 -  in FWD trans [th'',th']
   3.123 +  in FWD trans [th'',th'] end
   3.124 +
   3.125 +fun gen_reflect ctxt conv corr_thms eqs t =
   3.126 +  let
   3.127 +    val reify_thm = gen_reify ctxt eqs t;
   3.128 +    fun try_corr thm =
   3.129 +      SOME (FWD trans [reify_thm, thm RS sym]) handle THM _ => NONE;
   3.130 +    val thm = case get_first try_corr corr_thms
   3.131 +     of NONE => error "No suitable correctness theorem found"
   3.132 +      | SOME thm => thm;
   3.133 +    val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) thm;
   3.134 +    val rth = conv ft;
   3.135 +  in
   3.136 +    thm
   3.137 +    |> simplify (put_simpset HOL_basic_ss ctxt addsimps [rth])
   3.138 +    |> simplify (put_simpset HOL_basic_ss ctxt addsimps eqs addsimps @{thms nth_Cons_0 nth_Cons_Suc})
   3.139    end
   3.140  
   3.141 -
   3.142 -fun genreflect ctxt conv corr_thms raw_eqs t =
   3.143 -  let
   3.144 -    val reifth = genreif ctxt raw_eqs t
   3.145 -    fun trytrans [] = error "No suitable correctness theorem found"
   3.146 -      | trytrans (th::ths) =
   3.147 -           (FWD trans [reifth, th RS sym] handle THM _ => trytrans ths)
   3.148 -    val th = trytrans corr_thms
   3.149 -    val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th
   3.150 -    val rth = conv ft
   3.151 -  in
   3.152 -    simplify
   3.153 -      (put_simpset HOL_basic_ss ctxt addsimps raw_eqs addsimps @{thms nth_Cons_0 nth_Cons_Suc})
   3.154 -      (simplify (put_simpset HOL_basic_ss ctxt addsimps [rth]) th)
   3.155 -  end
   3.156 -
   3.157 -fun genreify_tac ctxt eqs to = SUBGOAL (fn (goal, i) =>
   3.158 +fun gen_reify_tac ctxt eqs to = SUBGOAL (fn (goal, i) =>
   3.159    let
   3.160      val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
   3.161 -    val th = genreif ctxt eqs t RS ssubst
   3.162 +    val th = gen_reify ctxt eqs t RS ssubst
   3.163    in rtac th i end);
   3.164  
   3.165      (* Reflection calls reification and uses the correctness *)
   3.166 @@ -306,11 +301,50 @@
   3.167  fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) =>
   3.168    let
   3.169      val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
   3.170 -    val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
   3.171 +    val th = gen_reflect ctxt conv corr_thms raw_eqs t RS ssubst
   3.172    in rtac th i THEN TRY (rtac TrueI i) end);  (* FIXME THEN_ALL_NEW !? *)
   3.173  
   3.174 -fun reflection_tac ctxt = gen_reflection_tac ctxt
   3.175 -  (Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt));
   3.176 -  (*FIXME why Code_Evaluation.dynamic_conv?  very specific...*)
   3.177 +structure Data = Generic_Data
   3.178 +(
   3.179 +  type T = thm list * thm list;
   3.180 +  val empty = ([], []);
   3.181 +  val extend = I;
   3.182 +  fun merge ((ths1, rths1), (ths2, rths2)) =
   3.183 +    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
   3.184 +);
   3.185 +
   3.186 +fun get_default ctxt =
   3.187 +  let
   3.188 +    val (reification_eqs, correctness_thms) = Data.get (Context.Proof ctxt);
   3.189 +  in { reification_eqs = reification_eqs, correctness_thms = correctness_thms } end;
   3.190 +
   3.191 +val add_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
   3.192 +val del_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
   3.193 +val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
   3.194 +val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
   3.195 +
   3.196 +val _ = Context.>> (Context.map_theory
   3.197 +  (Attrib.setup @{binding reify}
   3.198 +    (Attrib.add_del add_reification_eq del_reification_eq) "declare reification equations" #>
   3.199 +  Attrib.setup @{binding reflection}
   3.200 +    (Attrib.add_del add_correctness_thm del_correctness_thm) "declare reflection correctness theorems"));
   3.201 +
   3.202 +fun default_reify_tac ctxt user_eqs =
   3.203 +  let
   3.204 +    val { reification_eqs = default_eqs, correctness_thms = _ } =
   3.205 +      get_default ctxt;
   3.206 +    val eqs = user_eqs @ default_eqs; (*FIXME fold update?*)
   3.207 +  in gen_reify_tac ctxt eqs end;
   3.208 +
   3.209 +fun default_reflection_tac ctxt user_thms user_eqs =
   3.210 +  let
   3.211 +    val { reification_eqs = default_eqs, correctness_thms = default_thms } =
   3.212 +      get_default ctxt;
   3.213 +    val corr_thms = user_thms @ default_thms; (*FIXME fold update?*)
   3.214 +    val eqs = user_eqs @ default_eqs; (*FIXME fold update?*)
   3.215 +    val conv = Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt);
   3.216 +      (*FIXME why Code_Evaluation.dynamic_conv? very specific*)
   3.217 +  in gen_reflection_tac ctxt conv corr_thms eqs end;
   3.218 +
   3.219  
   3.220  end
     4.1 --- a/src/HOL/Library/reify_data.ML	Sat Apr 20 20:57:49 2013 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,40 +0,0 @@
     4.4 -(*  Title:      HOL/Library/reify_data.ML
     4.5 -    Author:     Amine Chaieb, TU Muenchen
     4.6 -
     4.7 -Data for the reification and reflection methods.
     4.8 -*)
     4.9 -
    4.10 -signature REIFY_DATA =
    4.11 -sig
    4.12 -  val get: Proof.context -> thm list * thm list
    4.13 -  val add: attribute
    4.14 -  val del: attribute
    4.15 -  val radd: attribute
    4.16 -  val rdel: attribute
    4.17 -  val setup: theory -> theory
    4.18 -end;
    4.19 -
    4.20 -structure Reify_Data : REIFY_DATA =
    4.21 -struct
    4.22 -
    4.23 -structure Data = Generic_Data
    4.24 -(
    4.25 -  type T = thm list * thm list;
    4.26 -  val empty = ([], []);
    4.27 -  val extend = I;
    4.28 -  fun merge ((ths1, rths1), (ths2, rths2)) =
    4.29 -    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
    4.30 -);
    4.31 -
    4.32 -val get = Data.get o Context.Proof;
    4.33 -
    4.34 -val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
    4.35 -val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
    4.36 -val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
    4.37 -val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
    4.38 -
    4.39 -val setup =
    4.40 -  Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
    4.41 -  Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
    4.42 -
    4.43 -end;