--- a/TFL/rules.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/TFL/rules.ML Tue Jul 11 12:16:54 2006 +0200
@@ -513,8 +513,8 @@
let val eq = Logic.strip_imp_concl body
val (f,args) = S.strip_comb (get_lhs eq)
val (vstrl,_) = S.strip_abs f
- val names = variantlist (map (#1 o dest_Free) vstrl,
- add_term_names(body, []))
+ val names =
+ Name.variant_list (add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
in get (rst, n+1, (names,n)::L) end
handle TERM _ => get (rst, n+1, L)
| U.ERR _ => get (rst, n+1, L);
--- a/TFL/usyntax.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/TFL/usyntax.ML Tue Jul 11 12:16:54 2006 +0200
@@ -240,7 +240,7 @@
fun dest_abs used (a as Abs(s, ty, M)) =
let
- val s' = variant used s;
+ val s' = Name.variant used s;
val v = Free(s', ty);
in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
end
--- a/src/HOL/Import/hol4rews.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Import/hol4rews.ML Tue Jul 11 12:16:54 2006 +0200
@@ -735,7 +735,7 @@
then F defname (* name_def *)
else if not (pdefname mem used)
then F pdefname (* name_primdef *)
- else F (variant used pdefname) (* last resort *)
+ else F (Name.variant used pdefname) (* last resort *)
end
end
--- a/src/HOL/Import/shuffler.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Jul 11 12:16:54 2006 +0200
@@ -253,7 +253,7 @@
val (type_inst,_) =
Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
let
- val v' = variant used v
+ val v' = Name.variant used v
in
((w,TFree(v',S))::inst,v'::used)
end)
@@ -322,7 +322,7 @@
then
let
val cert = cterm_of sg
- val v = Free(variant (add_term_free_names(t,[])) "v",xT)
+ val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
val cv = cert v
val ct = cert t
val th = (assume ct)
@@ -385,7 +385,7 @@
Type("fun",[aT,bT]) =>
let
val cert = cterm_of sg
- val vname = variant (add_term_free_names(t,[])) "v"
+ val vname = Name.variant (add_term_free_names(t,[])) "v"
val v = Free(vname,aT)
val cv = cert v
val ct = cert t
--- a/src/HOL/Library/EfficientNat.thy Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy Tue Jul 11 12:16:54 2006 +0200
@@ -153,7 +153,7 @@
fun remove_suc thy thms =
let
val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
- val vname = variant (map fst
+ val vname = Name.variant (map fst
(fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
fun lhs_of th = snd (Thm.dest_comb
@@ -206,7 +206,7 @@
fun remove_suc_clause thy thms =
let
val Suc_clause' = Thm.transfer thy Suc_clause;
- val vname = variant (map fst
+ val vname = Name.variant (map fst
(fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
| find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Jul 11 12:16:54 2006 +0200
@@ -252,7 +252,7 @@
let val used = add_term_names (t, [])
and vars = term_vars t;
fun newName (Var(ix,_), (pairs,used)) =
- let val v = variant used (string_of_indexname ix)
+ let val v = Name.variant used (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
val (alist, _) = foldr newName ([], used) vars;
fun mk_inst (Var(v,T)) = (Var(v,T),
--- a/src/HOL/Nominal/nominal_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -553,7 +553,7 @@
QUIET_BREADTH_FIRST (has_fewer_prems 1)
(resolve_tac rep_intrs 1))) thy |> (fn (r, thy) =>
let
- val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
+ val permT = mk_permT (TFree (Name.variant tvs "'a", HOLogic.typeS));
val pi = Free ("pi", permT);
val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
val T = Type (Sign.intern_type thy name, tvs');
@@ -1096,11 +1096,11 @@
val recs = List.filter is_rec_type cargs;
val Ts = map (typ_of_dtyp descr'' sorts') cargs;
val recTs' = map (typ_of_dtyp descr'' sorts') recs;
- val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
+ val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val frees' = partition_cargs idxs frees;
- val z = (variant tnames "z", fsT);
+ val z = (Name.variant tnames "z", fsT);
fun mk_prem ((dt, s), T) =
let
@@ -1126,7 +1126,7 @@
Const ("Nominal.fresh", T --> fsT --> HOLogic.boolT) $ t $ u) i T)
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
val tnames = DatatypeProp.make_tnames recTs;
- val zs = variantlist (replicate (length descr'') "z", tnames);
+ val zs = Name.variant_list tnames (replicate (length descr'') "z");
val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
(map (fn ((((i, _), T), tname), z) =>
make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Jul 11 12:16:54 2006 +0200
@@ -280,7 +280,7 @@
val recTs = get_rec_types descr' sorts;
val used = foldr add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
- val T' = TFree (variant used "'t", HOLogic.typeS);
+ val T' = TFree (Name.variant used "'t", HOLogic.typeS);
fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
--- a/src/HOL/Tools/datatype_codegen.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Jul 11 12:16:54 2006 +0200
@@ -219,7 +219,7 @@
| pcase gr ((cname, cargs)::cs) (t::ts) (U::Us) =
let
val j = length cargs;
- val xs = variantlist (replicate j "x", names);
+ val xs = Name.variant_list names (replicate j "x");
val Us' = Library.take (j, fst (strip_type U));
val frees = map Free (xs ~~ Us');
val (gr0, cp) = invoke_codegen thy defs dep module false
--- a/src/HOL/Tools/datatype_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -609,7 +609,7 @@
val size_names = DatatypeProp.indexify_names
(map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)));
- val freeT = TFree (variant used "'t", HOLogic.typeS);
+ val freeT = TFree (Name.variant used "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let val Ts = map (typ_of_dtyp descr' sorts) cargs
--- a/src/HOL/Tools/datatype_prop.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Tue Jul 11 12:16:54 2006 +0200
@@ -108,7 +108,7 @@
val recs = List.filter is_rec_type cargs;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val recTs' = map (typ_of_dtyp descr' sorts) recs;
- val tnames = variantlist (make_tnames Ts, pnames);
+ val tnames = Name.variant_list pnames (make_tnames Ts);
val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
@@ -136,7 +136,7 @@
fun make_casedist_prem T (cname, cargs) =
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val frees = variantlist (make_tnames Ts, ["P", "y"]) ~~ Ts;
+ val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
val free_ts = map Free frees
in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
(HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
@@ -158,7 +158,7 @@
let
val descr' = List.concat descr;
- val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
+ val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~
replicate (length descr') HOLogic.typeS);
val reccomb_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) =>
@@ -234,7 +234,7 @@
val recTs = get_rec_types descr' sorts;
val used = foldr add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
- val T' = TFree (variant used "'t", HOLogic.typeS);
+ val T' = TFree (Name.variant used "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -319,7 +319,7 @@
val recTs = get_rec_types descr' sorts;
val used' = foldr add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
- val T' = TFree (variant used' "'t", HOLogic.typeS);
+ val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
fun make_split (((_, (_, _, constrs)), T), comb_t) =
@@ -330,7 +330,7 @@
fun process_constr (((cname, cargs), f), (t1s, t2s)) =
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val frees = map Free (variantlist (make_tnames Ts, used) ~~ Ts);
+ val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
val eqn = HOLogic.mk_eq (Free ("x", T),
list_comb (Const (cname, Ts ---> T), frees));
val P' = P $ list_comb (f, frees)
@@ -437,7 +437,7 @@
fun mk_clause ((f, g), (cname, _)) =
let
val (Ts, _) = strip_type (fastype_of f);
- val tnames = variantlist (make_tnames Ts, used);
+ val tnames = Name.variant_list used (make_tnames Ts);
val frees = map Free (tnames ~~ Ts)
in
list_all_free (tnames ~~ Ts, Logic.mk_implies
@@ -472,7 +472,7 @@
fun mk_eqn T (cname, cargs) =
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val tnames = variantlist (make_tnames Ts, ["v"]);
+ val tnames = Name.variant_list ["v"] (make_tnames Ts);
val frees = tnames ~~ Ts
in
foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
--- a/src/HOL/Tools/datatype_realizer.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Jul 11 12:16:54 2006 +0200
@@ -63,7 +63,7 @@
(fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) =>
let
val Ts = map (typ_of_dtyp descr sorts) cargs;
- val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
+ val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
val frees = tnames ~~ Ts;
@@ -171,8 +171,7 @@
fun make_casedist_prem T (cname, cargs) =
let
val Ts = map (typ_of_dtyp descr sorts) cargs;
- val frees = variantlist
- (DatatypeProp.make_tnames Ts, ["P", "y"]) ~~ Ts;
+ val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT)
in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Jul 11 12:16:54 2006 +0200
@@ -392,7 +392,7 @@
fun mk_thm i =
let
val Ts = map (TFree o rpair HOLogic.typeS)
- (variantlist (replicate i "'t", used));
+ (Name.variant_list used (replicate i "'t"));
val f = Free ("f", Ts ---> U)
in Goal.prove_global sign [] [] (Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.list_all
--- a/src/HOL/Tools/function_package/fundef_prep.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Tue Jul 11 12:16:54 2006 +0200
@@ -2,7 +2,7 @@
ID: $Id$
Author: Alexander Krauss, TU Muenchen
-A package for general recursive function definitions.
+A package for general recursive function definitions.
Preparation step: makes auxiliary definitions and generates
proof obligations.
*)
@@ -10,20 +10,16 @@
signature FUNDEF_PREP =
sig
val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
- -> FundefCommon.prep_result * theory
+ -> FundefCommon.prep_result * theory
end
-
-
-
-
structure FundefPrep (*: FUNDEF_PREP*) =
struct
open FundefCommon
-open FundefAbbrev
+open FundefAbbrev
(* Theory dependencies. *)
val Pair_inject = thm "Product_Type.Pair_inject";
@@ -39,30 +35,30 @@
fun split_list3 [] = ([],[],[])
- | split_list3 ((x,y,z)::xyzs) =
+ | split_list3 ((x,y,z)::xyzs) =
let
- val (xs, ys, zs) = split_list3 xyzs
+ val (xs, ys, zs) = split_list3 xyzs
in
- (x::xs,y::ys,z::zs)
+ (x::xs,y::ys,z::zs)
end
fun build_tree thy f congs ctx (qs, gs, lhs, rhs) =
let
- (* FIXME: Save precomputed dependencies in a theory data slot *)
- val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
+ (* FIXME: Save precomputed dependencies in a theory data slot *)
+ val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
- val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx
+ val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx
in
- FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
+ FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
end
fun find_calls tree =
let
fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
- | add_Ri _ _ _ _ = raise Match
- in
+ | add_Ri _ _ _ _ = raise Match
+ in
rev (FundefCtxTree.traverse_tree add_Ri tree [])
end
@@ -71,68 +67,68 @@
(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
fun mk_primed_vars thy glrs =
let
- val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
+ val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
- fun rename_vars (qs,gs,lhs,rhs) =
- let
- val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
- val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
- in
- (qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
- end
+ fun rename_vars (qs,gs,lhs,rhs) =
+ let
+ val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
+ val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
+ in
+ (qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
+ end
in
- map rename_vars glrs
+ map rename_vars glrs
end
(* Chooses fresh free names, declares G and R, defines f and returns a record
- with all the information *)
+ with all the information *)
fun setup_context f glrs defname thy =
let
- val Const (f_fullname, fT) = f
- val fname = Sign.base_name f_fullname
+ val Const (f_fullname, fT) = f
+ val fname = Sign.base_name f_fullname
- val domT = domain_type fT
- val ranT = range_type fT
+ val domT = domain_type fT
+ val ranT = range_type fT
- val GT = mk_relT (domT, ranT)
- val RT = mk_relT (domT, domT)
- val G_name = defname ^ "_graph"
- val R_name = defname ^ "_rel"
+ val GT = mk_relT (domT, ranT)
+ val RT = mk_relT (domT, domT)
+ val G_name = defname ^ "_graph"
+ val R_name = defname ^ "_rel"
val gfixes = [("h_fd", domT --> ranT),
- ("y_fd", ranT),
- ("x_fd", domT),
- ("z_fd", domT),
- ("a_fd", domT),
- ("D_fd", HOLogic.mk_setT domT),
- ("P_fd", domT --> boolT),
- ("Pb_fd", boolT),
- ("f_fd", fT)]
+ ("y_fd", ranT),
+ ("x_fd", domT),
+ ("z_fd", domT),
+ ("a_fd", domT),
+ ("D_fd", HOLogic.mk_setT domT),
+ ("P_fd", domT --> boolT),
+ ("Pb_fd", boolT),
+ ("f_fd", fT)]
val (fxnames, ctx) = (ProofContext.init thy)
|> ProofContext.add_fixes_i (map (fn (n,T) => (n, SOME T, NoSyn)) gfixes)
val [h, y, x, z, a, D, P, Pbool, fvar] = map (fn (n,(_,T)) => Free (n, T)) (fxnames ~~ gfixes)
-
+
val Free (fvarname, _) = fvar
- val glrs' = mk_primed_vars thy glrs
+ val glrs' = mk_primed_vars thy glrs
- val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
+ val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
- val G = Const (Sign.full_name thy G_name, GT)
- val R = Const (Sign.full_name thy R_name, RT)
- val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
+ val G = Const (Sign.full_name thy G_name, GT)
+ val R = Const (Sign.full_name thy R_name, RT)
+ val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
- val f_eq = Logic.mk_equals (f $ x,
- Const ("The", (ranT --> boolT) --> ranT) $
- Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
+ val f_eq = Logic.mk_equals (f $ x,
+ Const ("The", (ranT --> boolT) --> ranT) $
+ Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
- val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
+ val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
in
- (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy)
+ (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy)
end
@@ -142,8 +138,8 @@
(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
(implies $ Trueprop (mk_eq (lhs, lhs'))
- $ Trueprop (mk_eq (rhs, rhs')))
- |> fold_rev (curry Logic.mk_implies) (gs @ gs')
+ $ Trueprop (mk_eq (rhs, rhs')))
+ |> fold_rev (curry Logic.mk_implies) (gs @ gs')
|> fold_rev mk_forall (qs @ qs')
(* all proof obligations *)
@@ -153,35 +149,35 @@
fun mk_completeness names glrs =
let
- val Names {domT, x, Pbool, ...} = names
+ val Names {domT, x, Pbool, ...} = names
- fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
- |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
- |> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev mk_forall qs
+ fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
+ |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev mk_forall qs
in
- Trueprop Pbool
- |> fold_rev (curry Logic.mk_implies o mk_case) glrs
+ Trueprop Pbool
+ |> fold_rev (curry Logic.mk_implies o mk_case) glrs
|> mk_forall_rename (x, "x")
|> mk_forall_rename (Pbool, "P")
end
-fun inductive_def_wrap defs (thy, const) =
- let
+fun inductive_def_wrap defs (thy, const) =
+ let
val qdefs = map dest_all_all defs
- val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
- InductivePackage.add_inductive_i true (*verbose*)
- false (*add_consts*)
- "" (* no altname *)
- false (* no coind *)
- false (* elims, please *)
- false (* induction thm please *)
- [const] (* the constant *)
- (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
- [] (* no special monos *)
- thy
+ val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
+ InductivePackage.add_inductive_i true (*verbose*)
+ false (*add_consts*)
+ "" (* no altname *)
+ false (* no coind *)
+ false (* elims, please *)
+ false (* induction thm please *)
+ [const] (* the constant *)
+ (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
+ [] (* no special monos *)
+ thy
(* It would be nice if this worked... But this is actually HO-Unification... *)
(* fun inst (qs, intr) intr_gen =
@@ -191,7 +187,7 @@
|> fold_rev (forall_intr o cterm_of thy) qs*)
fun inst (qs, intr) intr_gen =
- intr_gen
+ intr_gen
|> Thm.freezeT
|> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs
@@ -208,10 +204,10 @@
(*
- * "!!qs xs. CS ==> G => (r, lhs) : R"
+ * "!!qs xs. CS ==> G => (r, lhs) : R"
*)
fun mk_RIntro R (qs, gs, lhs, rhs) (rcfix, rcassm, rcarg) =
- mk_relmem (rcarg, lhs) R
+ mk_relmem (rcarg, lhs) R
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev (mk_forall o Free) rcfix
@@ -236,32 +232,32 @@
fun mk_clause_info thy names no (qs,gs,lhs,rhs) tree RCs GIntro_thm RIntro_thms =
let
- val Names {G, h, f, fvar, x, ...} = names
-
- val cqs = map (cterm_of thy) qs
- val ags = map (assume o cterm_of thy) gs
+ val Names {G, h, f, fvar, x, ...} = names
+
+ val cqs = map (cterm_of thy) qs
+ val ags = map (assume o cterm_of thy) gs
val used = [] (* XXX *)
(* FIXME: What is the relationship between this and mk_primed_vars? *)
- val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
- val cqs' = map (cterm_of thy) qs'
+ val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
+ val cqs' = map (cterm_of thy) qs'
- val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
- val ags' = map (assume o cterm_of thy o rename_vars) gs
- val lhs' = rename_vars lhs
- val rhs' = rename_vars rhs
+ val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
+ val ags' = map (assume o cterm_of thy o rename_vars) gs
+ val lhs' = rename_vars lhs
+ val rhs' = rename_vars rhs
val lGI = GIntro_thm
|> forall_elim (cterm_of thy f)
|> fold forall_elim cqs
|> fold implies_elim_swp ags
-
+
(* FIXME: Can be removed when inductive-package behaves nicely. *)
- val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [])
+ val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [])
(term_frees (snd (dest_all_all (prop_of GIntro_thm))))
-
- fun mk_call_info (rcfix, rcassm, rcarg) RI =
- let
+
+ fun mk_call_info (rcfix, rcassm, rcarg) RI =
+ let
val crcfix = map (cterm_of thy o Free) rcfix
val llRI = RI
@@ -270,32 +266,32 @@
|> fold implies_elim_swp ags
|> fold implies_elim_swp rcassm
- val h_assum =
+ val h_assum =
mk_relmem (rcarg, h $ rcarg) G
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (mk_forall o Free) rcfix
|> Pattern.rewrite_term thy [(f, h)] []
- val Gh = assume (cterm_of thy h_assum)
- val Gh' = assume (cterm_of thy (rename_vars h_assum))
- in
- RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
- end
+ val Gh = assume (cterm_of thy h_assum)
+ val Gh' = assume (cterm_of thy (rename_vars h_assum))
+ in
+ RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
+ end
- val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+ val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
val RC_infos = map2 mk_call_info RCs RIntro_thms
in
- ClauseInfo
- {
- no=no,
- qs=qs, gs=gs, lhs=lhs, rhs=rhs,
- cqs=cqs, ags=ags,
- cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs',
- lGI=lGI, RCs=RC_infos,
- tree=tree, case_hyp = case_hyp,
+ ClauseInfo
+ {
+ no=no,
+ qs=qs, gs=gs, lhs=lhs, rhs=rhs,
+ cqs=cqs, ags=ags,
+ cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs',
+ lGI=lGI, RCs=RC_infos,
+ tree=tree, case_hyp = case_hyp,
ordcqs'=ordcqs'
- }
+ }
end
@@ -311,9 +307,9 @@
fun store_compat_thms 0 thms = []
| store_compat_thms n thms =
let
- val (thms1, thms2) = chop n thms
+ val (thms1, thms2) = chop n thms
in
- (thms1 :: store_compat_thms (n - 1) thms2)
+ (thms1 :: store_compat_thms (n - 1) thms2)
end
@@ -326,32 +322,32 @@
(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
(* if j < i, then turn around *)
fun get_compat_thm thy cts clausei clausej =
- let
- val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
- val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
+ let
+ val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
+ val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
- val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
+ val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
in if j < i then
- let
- val compat = lookup_compat_thm j i cts
- in
- compat (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
+ let
+ val compat = lookup_compat_thm j i cts
+ in
+ compat (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
|> fold forall_elim (qsj' @ qsi) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
- |> fold implies_elim_swp gsj'
- |> fold implies_elim_swp gsi
- |> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
- end
+ |> fold implies_elim_swp gsj'
+ |> fold implies_elim_swp gsi
+ |> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
+ end
else
- let
- val compat = lookup_compat_thm i j cts
- in
- compat (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
+ let
+ val compat = lookup_compat_thm i j cts
+ in
+ compat (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
|> fold forall_elim (qsi @ qsj') (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
- |> fold implies_elim_swp gsi
- |> fold implies_elim_swp gsj'
- |> implies_elim_swp (assume lhsi_eq_lhsj')
- |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
- end
+ |> fold implies_elim_swp gsi
+ |> fold implies_elim_swp gsj'
+ |> implies_elim_swp (assume lhsi_eq_lhsj')
+ |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
+ end
end
@@ -359,29 +355,29 @@
(* Generates the replacement lemma with primed variables. A problem here is that one should not do
the complete requantification at the end to replace the variables. One should find a way to be more efficient
here. *)
-fun mk_replacement_lemma thy (names:naming_context) ih_elim clause =
- let
- val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
- val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
+fun mk_replacement_lemma thy (names:naming_context) ih_elim clause =
+ let
+ val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
+ val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
- val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
+ val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
- val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
- val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
- val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
+ val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
+ val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
+ val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
- val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
+ val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
- val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
+ val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
- val replace_lemma = (eql RS meta_eq_to_obj_eq)
- |> implies_intr (cprop_of case_hyp)
- |> fold_rev (implies_intr o cprop_of) h_assums
- |> fold_rev (implies_intr o cprop_of) ags
- |> fold_rev forall_intr cqs
- |> fold forall_elim cqs'
- |> fold implies_elim_swp ags'
- |> fold implies_elim_swp h_assums'
+ val replace_lemma = (eql RS meta_eq_to_obj_eq)
+ |> implies_intr (cprop_of case_hyp)
+ |> fold_rev (implies_intr o cprop_of) h_assums
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> fold_rev forall_intr cqs
+ |> fold forall_elim cqs'
+ |> fold implies_elim_swp ags'
+ |> fold implies_elim_swp h_assums'
in
replace_lemma
end
@@ -391,84 +387,84 @@
fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
let
- val Names {f, h, y, ...} = names
- val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
- val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
+ val Names {f, h, y, ...} = names
+ val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
+ val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
- val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
- val compat = get_compat_thm thy compat_store clausei clausej
- val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
+ val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
+ val compat = get_compat_thm thy compat_store clausei clausej
+ val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
- val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
- val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
+ val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
+ val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
- val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
+ val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
in
- (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
+ (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
|> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
- |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
- |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
- |> implies_intr (cprop_of y_eq_rhsj'h)
- |> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
- |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
- |> implies_elim_swp eq_pairs
- |> fold_rev (implies_intr o cprop_of) Ghsj'
- |> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
- |> implies_intr (cprop_of eq_pairs)
- |> fold_rev forall_intr ordcqs'j
+ |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
+ |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
+ |> implies_intr (cprop_of y_eq_rhsj'h)
+ |> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
+ |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
+ |> implies_elim_swp eq_pairs
+ |> fold_rev (implies_intr o cprop_of) Ghsj'
+ |> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
+ |> implies_intr (cprop_of eq_pairs)
+ |> fold_rev forall_intr ordcqs'j
end
fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
let
- val Names {x, y, G, fvar, f, ranT, ...} = names
- val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
+ val Names {x, y, G, fvar, f, ranT, ...} = names
+ val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
- val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
+ val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
- fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
+ fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
|> fold_rev (implies_intr o cprop_of) CCas
- |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
- val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
- |> fold (curry op COMP o prep_RC) RCs
+ val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
+ |> fold (curry op COMP o prep_RC) RCs
- val a = cterm_of thy (mk_prod (lhs, y))
- val P = cterm_of thy (mk_eq (y, rhs))
- val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
+ val a = cterm_of thy (mk_prod (lhs, y))
+ val P = cterm_of thy (mk_eq (y, rhs))
+ val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
- val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
+ val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
- val uniqueness = G_cases
+ val uniqueness = G_cases
|> forall_elim a
|> forall_elim P
- |> implies_elim_swp a_in_G
- |> fold implies_elim_swp unique_clauses
- |> implies_intr (cprop_of a_in_G)
- |> forall_intr (cterm_of thy y)
+ |> implies_elim_swp a_in_G
+ |> fold implies_elim_swp unique_clauses
+ |> implies_intr (cprop_of a_in_G)
+ |> forall_intr (cterm_of thy y)
- val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
+ val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
- val exactly_one =
- ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
- |> curry (op COMP) existence
- |> curry (op COMP) uniqueness
- |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
- |> implies_intr (cprop_of case_hyp)
- |> fold_rev (implies_intr o cprop_of) ags
- |> fold_rev forall_intr cqs
+ val exactly_one =
+ ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
+ |> curry (op COMP) existence
+ |> curry (op COMP) uniqueness
+ |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
+ |> implies_intr (cprop_of case_hyp)
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> fold_rev forall_intr cqs
- val function_value =
- existence
- |> fold_rev (implies_intr o cprop_of) ags
- |> implies_intr ihyp
- |> implies_intr (cprop_of case_hyp)
- |> forall_intr (cterm_of thy x)
- |> forall_elim (cterm_of thy lhs)
- |> curry (op RS) refl
+ val function_value =
+ existence
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> implies_intr ihyp
+ |> implies_intr (cprop_of case_hyp)
+ |> forall_intr (cterm_of thy x)
+ |> forall_elim (cterm_of thy lhs)
+ |> curry (op RS) refl
in
- (exactly_one, function_value)
+ (exactly_one, function_value)
end
@@ -476,45 +472,45 @@
fun prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim =
let
- val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
+ val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
+
+ val f_def_fr = Thm.freezeT f_def
- val f_def_fr = Thm.freezeT f_def
+ val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)]
+ [SOME (cterm_of thy f), SOME (cterm_of thy G)])
+ #> curry op COMP (forall_intr_vars f_def_fr)
- val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)]
- [SOME (cterm_of thy f), SOME (cterm_of thy G)])
- #> curry op COMP (forall_intr_vars f_def_fr)
-
- val inst_ex1_ex = instantiate_and_def ex1_implies_ex
- val inst_ex1_un = instantiate_and_def ex1_implies_un
- val inst_ex1_iff = instantiate_and_def ex1_implies_iff
+ val inst_ex1_ex = instantiate_and_def ex1_implies_ex
+ val inst_ex1_un = instantiate_and_def ex1_implies_un
+ val inst_ex1_iff = instantiate_and_def ex1_implies_iff
+
+ (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
+ val ihyp = all domT $ Abs ("z", domT,
+ implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
+ $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+ Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
+ |> cterm_of thy
- (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
- val ihyp = all domT $ Abs ("z", domT,
- implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
- $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
- Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
- |> cterm_of thy
-
- val ihyp_thm = assume ihyp |> forall_elim_vars 0
- val ih_intro = ihyp_thm RS inst_ex1_ex
- val ih_elim = ihyp_thm RS inst_ex1_un
+ val ihyp_thm = assume ihyp |> forall_elim_vars 0
+ val ih_intro = ihyp_thm RS inst_ex1_ex
+ val ih_elim = ihyp_thm RS inst_ex1_un
- val _ = Output.debug "Proving Replacement lemmas..."
- val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
+ val _ = Output.debug "Proving Replacement lemmas..."
+ val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
+
+ val _ = Output.debug "Proving cases for unique existence..."
+ val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
- val _ = Output.debug "Proving cases for unique existence..."
- val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
-
- val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
- val graph_is_function = complete
+ val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
+ val graph_is_function = complete
|> forall_elim_vars 0
- |> fold (curry op COMP) ex1s
- |> implies_intr (ihyp)
- |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
- |> forall_intr (cterm_of thy x)
- |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
+ |> fold (curry op COMP) ex1s
+ |> implies_intr (ihyp)
+ |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
+ |> forall_intr (cterm_of thy x)
+ |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
|> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
- |> Drule.close_derivation
+ |> Drule.close_derivation
val goal = complete COMP (graph_is_function COMP conjunctionI)
|> Drule.close_derivation
@@ -539,9 +535,9 @@
fun prepare_fundef thy congs defname f qglrs used =
let
val (names, thy) = setup_context f qglrs defname thy
- val Names {G, R, ctx, glrs', fvar, ...} = names
+ val Names {G, R, ctx, glrs', fvar, ...} = names
-
+
val n = length qglrs
val trees = map (build_tree thy f congs ctx) qglrs
val RCss = map find_calls trees
@@ -558,16 +554,16 @@
val R_intross = map2 (fn qglr => map (mk_RIntro R qglr)) qglrs RCss
val G_intros = map2 (mk_GIntro thy f fvar G) qglrs RCss
-
+
val (GIntro_thms, (thy, _, G_elim)) = inductive_def_wrap G_intros (thy, G)
val (RIntro_thmss, (thy, _, R_elim)) = fold_burrow inductive_def_wrap R_intross (thy, R)
-
+
val clauses = map6 (mk_clause_info thy names) (1 upto n) qglrs trees RCss GIntro_thms RIntro_thmss
-
+
val (goal, goalI, ex1_iff, values) = prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim
in
- (Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
- thy)
+ (Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
+ thy)
end
--- a/src/HOL/Tools/inductive_codegen.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Jul 11 12:16:54 2006 +0200
@@ -343,7 +343,7 @@
fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
NONE => ((names, (s, [s])::vs), s)
- | SOME xs => let val s' = variant names s in
+ | SOME xs => let val s' = Name.variant names s in
((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
fun distinct_v (nvs, Var ((s, 0), T)) =
@@ -407,7 +407,7 @@
fun check_constrt ((names, eqs), t) =
if is_constrt thy t then ((names, eqs), t) else
- let val s = variant names "x";
+ let val s = Name.variant names "x";
in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
fun compile_eq (gr, (s, t)) =
--- a/src/HOL/Tools/inductive_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -324,7 +324,7 @@
fun mk_elims cs cTs params intr_ts intr_names =
let
val used = foldr add_term_names [] intr_ts;
- val [aname, pname] = variantlist (["a", "P"], used);
+ val [aname, pname] = Name.variant_list used ["a", "P"];
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
fun dest_intr r =
@@ -359,8 +359,8 @@
(* predicates for induction rule *)
- val preds = map Free (variantlist (if length cs < 2 then ["P"] else
- map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
+ val preds = map Free (Name.variant_list used (if length cs < 2 then ["P"] else
+ map (fn i => "P" ^ string_of_int i) (1 upto length cs)) ~~
map (fn T => T --> HOLogic.boolT) cTs);
(* transform an introduction rule into a premise for induction rule *)
@@ -697,7 +697,7 @@
val fp_name = if coind then gfp_name else lfp_name;
val used = foldr add_term_names [] intr_ts;
- val [sname, xname] = variantlist (["S", "x"], used);
+ val [sname, xname] = Name.variant_list used ["S", "x"];
(* transform an introduction rule into a conjunction *)
(* [| t : ... S_i ... ; ... |] ==> u : S_j *)
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 11 12:16:54 2006 +0200
@@ -35,7 +35,7 @@
fun strip_all t =
let
fun strip used (Const ("all", _) $ Abs (s, T, t)) =
- let val s' = variant used s
+ let val s' = Name.variant used s
in strip (s'::used) (subst_bound (Free (s', T), t)) end
| strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
| strip _ t = t;
@@ -152,7 +152,7 @@
fun fun_of ts rts args used (prem :: prems) =
let
val T = Extraction.etype_of thy vs [] prem;
- val [x, r] = variantlist (["x", "r"], used)
+ val [x, r] = Name.variant_list used ["x", "r"]
in if T = Extraction.nullT
then fun_of ts rts args used prems
else if is_rec prem then
@@ -248,7 +248,7 @@
handle DatatypeAux.Datatype_Empty name' =>
let
val name = Sign.base_name name';
- val dname = variant used "Dummy"
+ val dname = Name.variant used "Dummy"
in
thy
|> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
--- a/src/HOL/Tools/record_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/record_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -1315,7 +1315,7 @@
val fieldTs = (map snd fields);
val alphas_zeta = alphas@[zeta];
val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
- val vT = TFree (variant alphas_zeta "'v", HOLogic.typeS);
+ val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
val extT_name = suffix ext_typeN name
val extT = Type (extT_name, alphas_zetaTs);
val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]);
@@ -1385,8 +1385,8 @@
val ext = mk_ext vars_more;
val s = Free (rN, extT);
val w = Free (wN, extT);
- val P = Free (variant variants "P", extT-->HOLogic.boolT);
- val C = Free (variant variants "C", HOLogic.boolT);
+ val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
+ val C = Free (Name.variant variants "C", HOLogic.boolT);
val inject_prop =
let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
@@ -1411,7 +1411,7 @@
(*updates*)
fun mk_upd_prop (i,(c,T)) =
- let val x' = Free (variant variants (base c ^ "'"),T)
+ let val x' = Free (Name.variant variants (base c ^ "'"),T)
val args' = nth_update (i, x') vars_more
in mk_upd updN c x' ext === mk_ext args' end;
val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
@@ -1422,7 +1422,7 @@
in s === mk_ext args end;
val split_meta_prop =
- let val P = Free (variant variants "P", extT-->Term.propT) in
+ let val P = Free (Name.variant variants "P", extT-->Term.propT) in
Logic.mk_equals
(All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
end;
@@ -1479,7 +1479,7 @@
fun upd_convs_prf_opt () =
let
fun mkrefl (c,T) = Thm.reflexive
- (cterm_of defs_thy (Free (variant variants (base c ^ "'"),T)));
+ (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T)));
val refls = map mkrefl fields_more;
val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
val dest_convs' = map mk_meta_eq dest_convs;
@@ -1595,7 +1595,7 @@
val parent_names = map fst parent_fields;
val parent_types = map snd parent_fields;
val parent_fields_len = length parent_fields;
- val parent_variants = variantlist (map base parent_names, [moreN, rN, rN ^ "'", wN]);
+ val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
val parent_vars = ListPair.map Free (parent_variants, parent_types);
val parent_len = length parents;
val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
@@ -1607,7 +1607,7 @@
val alphas_fields = foldr add_typ_tfree_names [] types;
val alphas_ext = alphas inter alphas_fields;
val len = length fields;
- val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::wN::parent_variants);
+ val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields);
val vars = ListPair.map Free (variants, types);
val named_vars = names ~~ vars;
val idxs = 0 upto (len - 1);
@@ -1622,7 +1622,7 @@
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
- val zeta = variant alphas "'z";
+ val zeta = Name.variant alphas "'z";
val moreT = TFree (zeta, HOLogic.typeS);
val more = Free (moreN, moreT);
val full_moreN = full moreN;
@@ -1779,9 +1779,9 @@
(* prepare propositions *)
val _ = timing_msg "record preparing propositions";
- val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
- val C = Free (variant all_variants "C", HOLogic.boolT);
- val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT);
+ val P = Free (Name.variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
+ val C = Free (Name.variant all_variants "C", HOLogic.boolT);
+ val P_unit = Free (Name.variant all_variants "P", recT0-->HOLogic.boolT);
(*selectors*)
val sel_conv_props =
@@ -1789,7 +1789,7 @@
(*updates*)
fun mk_upd_prop (i,(c,T)) =
- let val x' = Free (variant all_variants (base c ^ "'"),T)
+ let val x' = Free (Name.variant all_variants (base c ^ "'"),T)
val args' = nth_update (parent_fields_len + i, x') all_vars_more
in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
@@ -1819,7 +1819,7 @@
(*split*)
val split_meta_prop =
- let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in
+ let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
Logic.mk_equals
(All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
end;
--- a/src/HOL/Tools/res_axioms.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML Tue Jul 11 12:16:54 2006 +0200
@@ -145,7 +145,7 @@
end
| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) =
(*Universal quant: insert a free variable into body and continue*)
- let val fname = variant (add_term_names (p,[])) a
+ let val fname = Name.variant (add_term_names (p,[])) a
in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end
| dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
| dec_sko (Const ("op |", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
@@ -157,7 +157,7 @@
fun assume_skofuns th =
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
- let val name = variant (add_term_names (p,[])) (gensym "sko_")
+ let val name = Name.variant (add_term_names (p,[])) (gensym "sko_")
val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
val args = term_frees xtp \\ skos (*the formal parameters*)
val Ts = map type_of args
@@ -172,7 +172,7 @@
end
| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
(*Universal quant: insert a free variable into body and continue*)
- let val fname = variant (add_term_names (p,[])) a
+ let val fname = Name.variant (add_term_names (p,[])) a
in dec_sko (subst_bound (Free(fname,T), p)) defs end
| dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
| dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
--- a/src/HOL/Tools/split_rule.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/split_rule.ML Tue Jul 11 12:16:54 2006 +0200
@@ -81,7 +81,7 @@
fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
let
val Ts = HOLogic.prodT_factors T;
- val ys = Term.variantlist (replicate (length Ts) a, xs);
+ val ys = Name.variant_list xs (replicate (length Ts) a);
in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
(map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
end
--- a/src/HOLCF/domain/theorems.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOLCF/domain/theorems.ML Tue Jul 11 12:16:54 2006 +0200
@@ -476,7 +476,7 @@
val arg1 = (con1, args1);
val arg2 =
(con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
- (args2, variantlist (map vname args2,map vname args1)));
+ (args2, Name.variant_list (map vname args1) (map vname args2)));
in [dist arg1 arg2, dist arg2 arg1] end;
fun distincts [] = []
| distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
--- a/src/HOLCF/fixrec_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOLCF/fixrec_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -142,7 +142,7 @@
in pre_build f rhs' (v::vs) taken' end
| Const(c,T) =>
let
- val n = variant taken "v";
+ val n = Name.variant taken "v";
fun result_type (Type("Cfun.->",[_,T])) (x::xs) = result_type T xs
| result_type T _ = T;
val v = Free(n, result_type T vs);
--- a/src/Provers/IsaPlanner/isand.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Provers/IsaPlanner/isand.ML Tue Jul 11 12:16:54 2006 +0200
@@ -204,7 +204,7 @@
val tvars = List.foldr Term.add_term_tvars [] ts;
val (names',renamings) =
List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
- let val n2 = Term.variant Ns n in
+ let val n2 = Name.variant Ns n in
(n2::Ns, (tv, (n2,s))::Rs)
end) (tfree_names @ names,[]) tvars;
in renamings end;
@@ -237,7 +237,7 @@
val Ns = List.foldr Term.add_term_names names ts;
val (_,renamings) =
Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
- let val n2 = Term.variant Ns n in
+ let val n2 = Name.variant Ns n in
(n2 :: Ns, (v, (n2,ty)) :: Rs)
end) ((Ns,[]), vars);
in renamings end;
@@ -436,7 +436,7 @@
val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
val names = Term.add_term_names (t,varnames);
val fvs = map Free
- ((Term.variantlist (map fst alls, names))
+ (Name.variant_list names (map fst alls)
~~ (map snd alls));
in ((subst_bounds (fvs,t)), fvs) end;
@@ -448,7 +448,7 @@
val body = Term.strip_all_body gt;
val alls = rev (Term.strip_all_vars gt);
val fvs = map Free
- ((Term.variantlist (map fst alls, names))
+ (Name.variant_list names (map fst alls)
~~ (map snd alls));
in ((subst_bounds (fvs,body)), fvs) end;
--- a/src/Provers/IsaPlanner/rw_inst.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Provers/IsaPlanner/rw_inst.ML Tue Jul 11 12:16:54 2006 +0200
@@ -109,7 +109,7 @@
val names = usednames_of_thm rule;
val (fromnames,tonames,names2,Ts') =
Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
- let val n2 = Term.variant names n in
+ let val n2 = Name.variant names n in
(ctermify (Free(faken,ty)) :: rnf,
ctermify (Free(n2,ty)) :: rnt,
n2 :: names,
@@ -156,7 +156,7 @@
val vars_to_fix = Library.union (termvars, cond_vs);
val (renamings, names2) =
foldr (fn (((n,i),ty), (vs, names')) =>
- let val n' = Term.variant names' n in
+ let val n' = Name.variant names' n in
((((n,i),ty), Free (n', ty)) :: vs, n'::names')
end)
([], names) vars_to_fix;
@@ -164,7 +164,7 @@
(* make a new fresh typefree instantiation for the given tvar *)
fun new_tfree (tv as (ix,sort), (pairs,used)) =
- let val v = variant used (string_of_indexname ix)
+ let val v = Name.variant used (string_of_indexname ix)
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
--- a/src/Provers/eqsubst.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Provers/eqsubst.ML Tue Jul 11 12:16:54 2006 +0200
@@ -180,7 +180,7 @@
fun fakefree_badbounds Ts t =
let val (FakeTs,Ts,newnames) =
List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
- let val newname = Term.variant usednames n
+ let val newname = Name.variant usednames n
in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
(newname,ty)::Ts,
newname::usednames) end)
--- a/src/Pure/Proof/proofchecker.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/Proof/proofchecker.ML Tue Jul 11 12:16:54 2006 +0200
@@ -62,7 +62,7 @@
| thm_of vs Hs (Abst (s, SOME T, prf)) =
let
- val x = variant (names @ map fst vs) s;
+ val x = Name.variant (names @ map fst vs) s;
val thm = thm_of ((x, T) :: vs) Hs prf
in
Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
--- a/src/Pure/Tools/codegen_thingol.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Jul 11 12:16:54 2006 +0200
@@ -370,7 +370,7 @@
fun invent seed used =
let
- val x = Term.variant used seed
+ val x = Name.variant used seed
in (x, x :: used) end;
fun eta_expand (c as (_, (_, ty)), es) k =
--- a/src/Pure/codegen.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/codegen.ML Tue Jul 11 12:16:54 2006 +0200
@@ -337,7 +337,7 @@
fun preprocess_term thy t =
let
- val x = Free (variant (add_term_names (t, [])) "x", fastype_of t);
+ val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
(* fake definition *)
val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
(Logic.mk_equals (x, t));
@@ -539,7 +539,7 @@
val (illegal, alt_names) = split_list (map_filter (fn s =>
let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
val ps = (reserved @ illegal) ~~
- variantlist (map (suffix "'") reserved @ alt_names, names);
+ Name.variant_list names (map (suffix "'") reserved @ alt_names);
fun rename_id s = AList.lookup (op =) ps s |> the_default s;
@@ -688,9 +688,9 @@
separate (Pretty.brk 1) (p :: ps) @ [Pretty.str ")"])
else Pretty.block (separate (Pretty.brk 1) (p :: ps));
-fun new_names t xs = variantlist (map mk_id xs,
- map (fst o fst o dest_Var) (term_vars t) union
- add_term_names (t, ThmDatabase.ml_reserved));
+fun new_names t xs = Name.variant_list
+ (map (fst o fst o dest_Var) (term_vars t) union
+ add_term_names (t, ThmDatabase.ml_reserved)) (map mk_id xs);
fun new_name t x = hd (new_names t [x]);
--- a/src/Pure/proofterm.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/proofterm.ML Tue Jul 11 12:16:54 2006 +0200
@@ -568,8 +568,8 @@
(([], [], [], []), prf);
val fs' = map (fst o dest_Free) fs;
val vs' = map (fst o dest_Var) vs;
- val names = vs' ~~ variantlist (map fst vs', fs');
- val names' = Tvs ~~ variantlist (map fst Tvs, Tfs);
+ val names = vs' ~~ Name.variant_list fs' (map fst vs');
+ val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs);
val rnames = map swap names;
val rnames' = map swap names';
in
@@ -607,7 +607,7 @@
val fs = Term.fold_types (Term.fold_atyps
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
val ixns = add_term_tvar_ixns (t, []);
- val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
+ val fmap = fs ~~ Name.variant_list (map #1 ixns) (map fst fs)
fun thaw (f as (a, S)) =
(case AList.lookup (op =) fmap f of
NONE => TFree f
@@ -619,7 +619,7 @@
local
fun new_name (ix, (pairs,used)) =
- let val v = variant used (string_of_indexname ix)
+ let val v = Name.variant used (string_of_indexname ix)
in ((ix, v) :: pairs, v :: used) end;
fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
--- a/src/Pure/pure_thy.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/pure_thy.ML Tue Jul 11 12:16:54 2006 +0200
@@ -441,7 +441,7 @@
(fn Var ((x, j), _) => if i = j then curry (op ins_string) x else I | _ => I);
val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
val vars = strip_vars prop;
- val cvars = (Term.variantlist (map #1 vars, used), vars)
+ val cvars = (Name.variant_list used (map #1 vars), vars)
|> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T)));
in fold Thm.forall_elim cvars th end;
--- a/src/Pure/thm.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/thm.ML Tue Jul 11 12:16:54 2006 +0200
@@ -1343,7 +1343,7 @@
val short = length iparams - length cs;
val newnames =
if short < 0 then error "More names than abstractions!"
- else variantlist (Library.take (short, iparams), cs) @ cs;
+ else Name.variant_list cs (Library.take (short, iparams)) @ cs;
val freenames = map (#1 o dest_Free) (term_frees Bi);
val newBi = Logic.list_rename_params (newnames, Bi);
in
--- a/src/Pure/type.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/type.ML Tue Jul 11 12:16:54 2006 +0200
@@ -233,7 +233,7 @@
val fs = Term.fold_types (Term.fold_atyps
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
val ixns = add_term_tvar_ixns (t, []);
- val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
+ val fmap = fs ~~ map (rpair 0) (Name.variant_list (map #1 ixns) (map fst fs))
fun thaw (f as (a, S)) =
(case AList.lookup (op =) fmap f of
NONE => TFree f
@@ -246,7 +246,7 @@
local
fun new_name (ix, (pairs, used)) =
- let val v = variant used (string_of_indexname ix)
+ let val v = Name.variant used (string_of_indexname ix)
in ((ix, v) :: pairs, v :: used) end;
fun freeze_one alist (ix, sort) =
--- a/src/ZF/Tools/inductive_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -100,7 +100,7 @@
Sign.string_of_term sign t);
(*** Construct the fixedpoint definition ***)
- val mk_variant = variant (foldr add_term_names [] intr_tms);
+ val mk_variant = Name.variant (foldr add_term_names [] intr_tms);
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
--- a/src/ZF/Tools/primrec_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -147,7 +147,7 @@
(** make definition **)
(*the recursive argument*)
- val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
+ val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
Ind_Syntax.iT)
val def_tm = Logic.mk_equals