# HG changeset patch # User wenzelm # Date 1320525416 -3600 # Node ID 8b1604119bc0f22fd681229e5b16ea368b5a0c21 # Parent 257d0b179f0d1defd5fc6b95243a8e7701c95910# Parent 7fb63b469cd290eaf604c08fe364235cdb83ca29 merged diff -r 257d0b179f0d -r 8b1604119bc0 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Nov 05 12:01:21 2011 +0000 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Nov 05 21:36:56 2011 +0100 @@ -75,7 +75,7 @@ (map mk_partial_term_of (frees ~~ tys)) (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty)) val insts = - map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) + map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), narrowing_term, rhs] val cty = Thm.ctyp_of thy ty; in @@ -93,9 +93,10 @@ val cs = (map o apsnd o apsnd o map o map_atyps) (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco); - val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) + val var_insts = + map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"}, - @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty] + @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]; val var_eq = @{thm partial_term_of_anything} |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts diff -r 257d0b179f0d -r 8b1604119bc0 src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Sat Nov 05 12:01:21 2011 +0000 +++ b/src/HOL/Tools/code_evaluation.ML Sat Nov 05 21:36:56 2011 +0100 @@ -59,8 +59,10 @@ val t = list_comb (Const (c, tys ---> ty), map Free (Name.invent_names Name.context "a" tys)); val (arg, rhs) = - pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) - (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) + pairself (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) + (t, + map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) + (HOLogic.reflect_term t)); val cty = Thm.ctyp_of thy ty; in @{thm term_of_anything} diff -r 257d0b179f0d -r 8b1604119bc0 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sat Nov 05 12:01:21 2011 +0000 +++ b/src/Pure/Isar/class.ML Sat Nov 05 21:36:56 2011 +0100 @@ -344,7 +344,7 @@ val c' = Sign.full_name thy b; val rhs' = Pattern.rewrite_term thy unchecks [] rhs; val ty' = Term.fastype_of rhs'; - val rhs'' = map_types Logic.varifyT_global rhs'; + val rhs'' = Logic.varify_types_global rhs'; in thy |> Sign.add_abbrev (#1 prmode) (b, rhs'') diff -r 257d0b179f0d -r 8b1604119bc0 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sat Nov 05 12:01:21 2011 +0000 +++ b/src/Pure/Isar/code.ML Sat Nov 05 21:36:56 2011 +0100 @@ -131,12 +131,14 @@ let val c' = AxClass.unoverload_const thy (c, ty); val ty_decl = Sign.the_const_type thy c'; - in if Sign.typ_equiv thy - (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty)) then c' - else error ("Type\n" ^ string_of_typ thy ty - ^ "\nof constant " ^ quote c - ^ "\nis too specific compared to declared type\n" - ^ string_of_typ thy ty_decl) + in + if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty)) + then c' + else + error ("Type\n" ^ string_of_typ thy ty ^ + "\nof constant " ^ quote c ^ + "\nis too specific compared to declared type\n" ^ + string_of_typ thy ty_decl) end; fun check_const thy = check_unoverload thy o check_bare_const thy; @@ -403,16 +405,18 @@ let val _ = Thm.cterm_of thy (Const (c, raw_ty)); val ty = subst_signature thy c raw_ty; - val ty_decl = (Logic.unvarifyT_global o const_typ thy) c; + val ty_decl = Logic.unvarifyT_global (const_typ thy c); fun last_typ c_ty ty = let val tfrees = Term.add_tfreesT ty []; val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty)) handle TYPE _ => no_constr thy "bad type" c_ty val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else (); - val _ = if has_duplicates (eq_fst (op =)) vs + val _ = + if has_duplicates (eq_fst (op =)) vs then no_constr thy "duplicate type variables in datatype" c_ty else (); - val _ = if length tfrees <> length vs + val _ = + if length tfrees <> length vs then no_constr thy "type variables missing in datatype" c_ty else (); in (tyco, vs) end; val (tyco, _) = last_typ (c, ty) ty_decl; @@ -692,7 +696,8 @@ val _ = (fst o dest_Var) param handle TERM _ => bad "Not an abstype certificate"; val _ = if param = rhs then () else bad "Not an abstype certificate"; - val ((tyco, sorts), (abs, (vs, ty'))) = analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty); + val ((tyco, sorts), (abs, (vs, ty'))) = + analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty); val ty = domain_type ty'; val (vs', _) = logical_typscheme thy (abs, ty'); in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end; @@ -849,7 +854,7 @@ let val vs = fst (typscheme_abs thy abs_thm); val (_, concrete_thm) = concretify_abs thy tyco abs_thm; - in (vs, add_rhss_of_eqn thy (map_types Logic.unvarifyT_global (Thm.prop_of concrete_thm)) []) end; + in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end; fun equations_of_cert thy (cert as Equations (cert_thm, propers)) = let @@ -865,7 +870,7 @@ let val (_, ((abs, _), _)) = get_abstype_spec thy tyco; val tyscm = typscheme_projection thy t; - val t' = map_types Logic.varifyT_global t; + val t' = Logic.varify_types_global t; fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE)); in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end | equations_of_cert thy (Abstract (abs_thm, tyco)) = @@ -882,7 +887,7 @@ (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd) o snd o equations_of_cert thy) cert | pretty_cert thy (Projection (t, _)) = - [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)] + [Syntax.pretty_term_global thy (Logic.varify_types_global t)] | pretty_cert thy (Abstract (abs_thm, _)) = [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm]; @@ -1255,8 +1260,8 @@ in thy |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert)))) - |> change_fun_spec false rep ((K o Proj) - (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco)) + |> change_fun_spec false rep + (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco))) |> Abstype_Interpretation.data (tyco, serial ()) end; diff -r 257d0b179f0d -r 8b1604119bc0 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sat Nov 05 12:01:21 2011 +0000 +++ b/src/Pure/Isar/element.ML Sat Nov 05 21:36:56 2011 +0100 @@ -46,18 +46,9 @@ val transform_witness: morphism -> witness -> witness val conclude_witness: witness -> thm val pretty_witness: Proof.context -> witness -> Pretty.T - val instT_type: typ Symtab.table -> typ -> typ - val instT_term: typ Symtab.table -> term -> term - val instT_thm: theory -> typ Symtab.table -> thm -> thm val instT_morphism: theory -> typ Symtab.table -> morphism - val inst_term: typ Symtab.table * term Symtab.table -> term -> term - val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism - val satisfy_thm: witness list -> thm -> thm val satisfy_morphism: witness list -> morphism - val satisfy_facts: witness list -> - (Attrib.binding * (thm list * Attrib.src list) list) list -> - (Attrib.binding * (thm list * Attrib.src list) list) list val eq_morphism: theory -> thm list -> morphism option val transfer_morphism: theory -> morphism val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> @@ -350,7 +341,7 @@ if AList.defined (op =) insts a then insts else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts); val insts = - Term.fold_types (Term.fold_atyps (fn TFree v => add_inst v | _ => I)) + (Term.fold_types o Term.fold_atyps) (fn TFree v => add_inst v | _ => I) (Thm.full_prop_of th) []; in th @@ -374,19 +365,26 @@ (* instantiate types *) -fun instT_type env = - if Symtab.is_empty env then I - else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x)); +fun instT_type_same env = + if Symtab.is_empty env then Same.same + else + Term_Subst.map_atypsT_same + (fn TFree (a, _) => (case Symtab.lookup env a of SOME T => T | NONE => raise Same.SAME) + | _ => raise Same.SAME); -fun instT_term env = - if Symtab.is_empty env then I - else Term.map_types (instT_type env); +fun instT_term_same env = + if Symtab.is_empty env then Same.same + else Term_Subst.map_types_same (instT_type_same env); + +val instT_type = Same.commit o instT_type_same; +val instT_term = Same.commit o instT_term_same; -fun instT_subst env th = (Thm.fold_terms o Term.fold_types o Term.fold_atyps) - (fn T as TFree (a, _) => - let val T' = the_default T (Symtab.lookup env a) - in if T = T' then I else insert (op =) (a, T') end - | _ => I) th []; +fun instT_subst env th = + (Thm.fold_terms o Term.fold_types o Term.fold_atyps) + (fn T as TFree (a, _) => + let val T' = the_default T (Symtab.lookup env a) + in if T = T' then I else insert (eq_fst (op =)) (a, T') end + | _ => I) th []; fun instT_thm thy env th = if Symtab.is_empty env then th @@ -409,32 +407,28 @@ fun inst_term (envT, env) = if Symtab.is_empty env then instT_term envT else - let - val instT = instT_type envT; - fun inst (Const (x, T)) = Const (x, instT T) - | inst (Free (x, T)) = - (case Symtab.lookup env x of - NONE => Free (x, instT T) - | SOME t => t) - | inst (Var (xi, T)) = Var (xi, instT T) - | inst (b as Bound _) = b - | inst (Abs (x, T, t)) = Abs (x, instT T, inst t) - | inst (t $ u) = inst t $ inst u; - in Envir.beta_norm o inst end; + instT_term envT #> + Same.commit (Term_Subst.map_aterms_same + (fn Free (x, _) => (case Symtab.lookup env x of SOME t => t | NONE => raise Same.SAME) + | _ => raise Same.SAME)) #> + Envir.beta_norm; + +fun inst_subst (envT, env) th = + (Thm.fold_terms o Term.fold_aterms) + (fn Free (x, T) => + let + val T' = instT_type envT T; + val t = Free (x, T'); + val t' = the_default t (Symtab.lookup env x); + in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end + | _ => I) th []; fun inst_thm thy (envT, env) th = if Symtab.is_empty env then instT_thm thy envT th else let val substT = instT_subst envT th; - val subst = (Thm.fold_terms o Term.fold_aterms) - (fn Free (x, T) => - let - val T' = instT_type envT T; - val t = Free (x, T'); - val t' = the_default t (Symtab.lookup env x); - in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end - | _ => I) th []; + val subst = inst_subst (envT, env) th; in if null substT andalso null subst then th else th |> hyps_rule @@ -443,25 +437,25 @@ Conv.fconv_rule (Thm.beta_conversion true)) end; -fun inst_morphism thy envs = +fun inst_morphism thy (envT, env) = let val thy_ref = Theory.check_thy thy in Morphism.morphism {binding = [], - typ = [instT_type (#1 envs)], - term = [inst_term envs], - fact = [map (fn th => inst_thm (Theory.deref thy_ref) envs th)]} + typ = [instT_type envT], + term = [inst_term (envT, env)], + fact = [map (fn th => inst_thm (Theory.deref thy_ref) (envT, env) th)]} end; (* satisfy hypotheses *) -fun satisfy_thm witns thm = thm |> fold (fn hyp => +fun satisfy_thm witns thm = + thm |> fold (fn hyp => (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of NONE => I | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm)); val satisfy_morphism = Morphism.thm_morphism o satisfy_thm; -val satisfy_facts = facts_map o transform_ctxt o satisfy_morphism; (* rewriting with equalities *) diff -r 257d0b179f0d -r 8b1604119bc0 src/Pure/drule.ML --- a/src/Pure/drule.ML Sat Nov 05 12:01:21 2011 +0000 +++ b/src/Pure/drule.ML Sat Nov 05 21:36:56 2011 +0100 @@ -816,50 +816,47 @@ -(*** Instantiate theorem th, reading instantiations in theory thy ****) +(** variations on Thm.instantiate **) fun instantiate_normalize instpair th = Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); -(*Left-to-right replacements: tpairs = [...,(vi,ti),...]. - Instantiates distinct Vars by terms, inferring type instantiations. *) +(*Left-to-right replacements: tpairs = [..., (vi, ti), ...]. + Instantiates distinct Vars by terms, inferring type instantiations.*) local - fun add_types ((ct,cu), (thy,tye,maxidx)) = + fun add_types (ct, cu) (thy, tye, maxidx) = let - val thyt = Thm.theory_of_cterm ct; - val thyu = Thm.theory_of_cterm cu; - val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct; - val {t = u, T = U, maxidx = maxu, ...} = Thm.rep_cterm cu; - val maxi = Int.max(maxidx, Int.max(maxt, maxu)); - val thy' = Theory.merge(thy, Theory.merge(thyt, thyu)) - val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) - handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^ - Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^ - "\nof variable " ^ - Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^ - "\ncannot be unified with type\n" ^ - Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^ - Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u), - [T, U], [t, u]) - in (thy', tye', maxi') end; + val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct; + val {t = u, T = U, maxidx = maxu, ...} = Thm.rep_cterm cu; + val maxi = Int.max (maxidx, Int.max (maxt, maxu)); + val thy' = Theory.merge (thy, Theory.merge (Thm.theory_of_cterm ct, Thm.theory_of_cterm cu)); + val (tye', maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) + handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^ + Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^ + "\nof variable " ^ + Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^ + "\ncannot be unified with type\n" ^ + Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^ + Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u), + [T, U], [t, u]) + in (thy', tye', maxi') end; in + fun cterm_instantiate [] th = th - | cterm_instantiate ctpairs0 th = - let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0 - fun instT(ct,cu) = - let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of - in (inst ct, inst cu) end - fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy (Envir.norm_type tye T)) - in instantiate_normalize (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end - handle TERM _ => - raise THM("cterm_instantiate: incompatible theories",0,[th]) - | TYPE (msg, _, _) => raise THM(msg, 0, [th]) + | cterm_instantiate ctpairs th = + let + val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0); + val certT = ctyp_of thy; + val instT = + Vartab.fold (fn (xi, (S, T)) => + cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye []; + val inst = map (pairself (Thm.instantiate_cterm (instT, []))) ctpairs; + in instantiate_normalize (instT, inst) th end + handle TERM (msg, _) => raise THM (msg, 0, [th]) + | TYPE (msg, _, _) => raise THM (msg, 0, [th]); end; - -(** variations on instantiate **) - (* instantiate by left-to-right occurrence of variables *) fun instantiate' cTs cts thm = diff -r 257d0b179f0d -r 8b1604119bc0 src/Pure/goal.ML --- a/src/Pure/goal.ML Sat Nov 05 12:01:21 2011 +0000 +++ b/src/Pure/goal.ML Sat Nov 05 21:36:56 2011 +0100 @@ -168,8 +168,7 @@ val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees; val global_prop = - cert (Term.map_types Logic.varifyT_global - (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) + cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) |> Thm.weaken_sorts (Variable.sorts_of ctxt); val global_result = result |> Future.map (Drule.flexflex_unique #> diff -r 257d0b179f0d -r 8b1604119bc0 src/Pure/logic.ML --- a/src/Pure/logic.ML Sat Nov 05 12:01:21 2011 +0000 +++ b/src/Pure/logic.ML Sat Nov 05 21:36:56 2011 +0100 @@ -73,6 +73,8 @@ val assum_problems: int * term -> (term -> term) * term list * term val varifyT_global: typ -> typ val unvarifyT_global: typ -> typ + val varify_types_global: term -> term + val unvarify_types_global: term -> term val varify_global: term -> term val unvarify_global: term -> term val get_goal: term -> int -> term @@ -524,13 +526,20 @@ val varifyT_global = Same.commit varifyT_global_same; val unvarifyT_global = Same.commit unvarifyT_global_same; +fun varify_types_global tm = tm + |> Same.commit (Term_Subst.map_types_same varifyT_global_same) + handle TYPE (msg, _, _) => raise TERM (msg, [tm]); + +fun unvarify_types_global tm = tm + |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same) + handle TYPE (msg, _, _) => raise TERM (msg, [tm]); + fun varify_global tm = tm |> Same.commit (Term_Subst.map_aterms_same (fn Free (x, T) => Var ((x, 0), T) | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) | _ => raise Same.SAME)) - |> Same.commit (Term_Subst.map_types_same varifyT_global_same) - handle TYPE (msg, _, _) => raise TERM (msg, [tm]); + |> varify_types_global; fun unvarify_global tm = tm |> Same.commit (Term_Subst.map_aterms_same @@ -538,8 +547,7 @@ | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) | Free (x, _) => raise TERM (bad_fixed x, [tm]) | _ => raise Same.SAME)) - |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same) - handle TYPE (msg, _, _) => raise TERM (msg, [tm]); + |> unvarify_types_global; (* goal states *)