--- 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
--- 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}
--- 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'')
--- 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;
--- 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 *)
--- 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 =
--- 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 #>
--- 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 *)