# HG changeset patch # User haftmann # Date 1369985432 -7200 # Node ID 3d7472b6b720ad383f9da93fc8a35019e5cc1fa1 # Parent 47d138cae708d1a149a0e145efecfd9c35a82437 tuned diff -r 47d138cae708 -r 3d7472b6b720 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 @@ -43,8 +43,7 @@ let val Const (fN, _) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> strip_comb |> fst; - val thy = Proof_Context.theory_of ctxt; - val cert = Thm.cterm_of thy; + val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); val ((_, [th']), ctxt') = Variable.import true [th] ctxt; val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')); fun add_fterms (t as t1 $ t2) = @@ -103,7 +102,7 @@ val tt = HOLogic.listT (fastype_of t); in (case AList.lookup Type.could_unify bds tt of - NONE => error "index_of : type not found in environements!" + NONE => error "index_of: type not found in environements!" | SOME (tbs, tats) => let val i = find_index (fn t' => t' = t) tats; @@ -130,13 +129,14 @@ let val thy = Proof_Context.theory_of ctxt; val cert = cterm_of thy; + val certT = ctyp_of thy; fun tryabsdecomp (s, ctxt) bds = (case s of Abs (_, xT, ta) => let val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt; val (xn, ta) = Syntax_Trans.variant_abs (raw_xn, xT, ta); (* FIXME !? *) - val x = Free(xn, xT); + val x = Free (xn, xT); val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of NONE => error "tryabsdecomp: Type not found in the Environement" | SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT, (x :: bsT, atsT)) bds); @@ -156,8 +156,6 @@ [] => tryabsdecomp (t, ctxt) bds | ((vns, cong) :: congs) => (let - val cert = cterm_of thy; - val certy = ctyp_of thy; val (tyenv, tmenv) = Pattern.match thy ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) @@ -166,7 +164,7 @@ val (fts, its) = (map (snd o snd) fnvs, 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); + val ctyenv = map (fn ((vn, vi), (s, ty)) => (certT (TVar((vn, vi), s)), certT ty)) (Vartab.dest tyenv); in ((fts ~~ replicate (length fts) ctxt, apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds) @@ -254,15 +252,15 @@ |> 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); + val cert = cterm_of (Proof_Context.theory_of ctxt'); + val subst = + the o AList.lookup (op =) (map2 (fn T => fn v => (T, cert (Free (v, T)))) tys vs); fun prep_eq eq = let 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); + val subst = map_filter (fn (v as Var (_, T)) => SOME (cert v, subst T) + | _ => NONE) 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; @@ -271,10 +269,10 @@ val (congs, bds) = mk_congs ctxt eqs; val congs = rearrange congs; val (th, bds) = divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (t,ctxt) bds; - fun is_listVar (Var (_, t)) = can dest_listT t - | is_listVar _ = false; + fun is_list_var (Var (_, t)) = can dest_listT t + | is_list_var _ = false; val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd - |> strip_comb |> snd |> filter is_listVar; + |> strip_comb |> snd |> filter is_list_var; val cert = cterm_of (Proof_Context.theory_of ctxt); val cvs = map (fn (v as Var(_, t)) => (cert v, the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars; @@ -282,13 +280,13 @@ 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'] end; + in FWD trans [th'', th'] end; fun reflect ctxt conv corr_thms eqs t = let val reify_thm = reify ctxt eqs t; - fun try_corr thm = - SOME (FWD trans [reify_thm, thm RS sym]) handle THM _ => NONE; + fun try_corr corr_thm = + SOME (FWD trans [reify_thm, corr_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;