--- a/src/HOL/Nominal/nominal_atoms.ML Sat Mar 22 18:15:09 2014 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Mar 22 18:16:54 2014 +0100
@@ -86,7 +86,7 @@
fun mk_Cons x xs =
let val T = fastype_of x
- in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
+ in Const (@{const_name Cons}, T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args);
fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args);
@@ -142,7 +142,7 @@
val stmnt3 = HOLogic.mk_Trueprop
(HOLogic.mk_not
- (Const ("Finite_Set.finite", HOLogic.mk_setT ak_type --> HOLogic.boolT) $
+ (Const (@{const_name finite}, HOLogic.mk_setT ak_type --> HOLogic.boolT) $
HOLogic.mk_UNIV ak_type))
val simp2 = [@{thm image_def},@{thm bex_UNIV}]@inject_thm
@@ -179,9 +179,9 @@
val b = Free ("b", T);
val c = Free ("c", T);
val ab = Free ("ab", HOLogic.mk_prodT (T, T))
- val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
+ val cif = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
val cswap_akname = Const (full_swap_name, swapT);
- val cswap = Const ("Nominal.swap", swapT)
+ val cswap = Const (@{const_name Nominal.swap}, swapT)
val name = swap_name ^ "_def";
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -215,7 +215,7 @@
val xs = Free ("xs", mk_permT T);
val a = Free ("a", T) ;
- val cnil = Const ("List.list.Nil", mk_permT T);
+ val cnil = Const (@{const_name Nil}, mk_permT T);
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (prm $ cnil $ a, a));
@@ -245,7 +245,7 @@
val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
val pi = Free ("pi", mk_permT T);
val a = Free ("a", T');
- val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
+ val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> T' --> T');
val thy'' = Sign.add_path "rec" thy'
val cperm_def = Const (Sign.full_bname thy'' perm_def_name, mk_permT T --> T' --> T');
val thy''' = Sign.parent_path thy'';
@@ -265,7 +265,7 @@
let
val ak_name_qu = Sign.full_bname thy5 (ak_name);
val i_type = Type(ak_name_qu,[]);
- val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT);
+ val cat = Const (@{const_name Nominal.at}, Term.itselfT i_type --> HOLogic.boolT);
val at_type = Logic.mk_type i_type;
fun proof ctxt =
simp_tac (put_simpset HOL_ss ctxt
@@ -290,14 +290,14 @@
val (pt_ax_classes,thy7) = fold_map (fn (ak_name, T) => fn thy =>
let
val cl_name = "pt_"^ak_name;
- val ty = TFree("'a",["HOL.type"]);
+ val ty = TFree("'a", @{sort type});
val x = Free ("x", ty);
val pi1 = Free ("pi1", mk_permT T);
val pi2 = Free ("pi2", mk_permT T);
- val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
- val cnil = Const ("List.list.Nil", mk_permT T);
- val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
- val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
+ val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> ty --> ty);
+ val cnil = Const (@{const_name Nil}, mk_permT T);
+ val cappend = Const (@{const_name append}, mk_permT T --> mk_permT T --> mk_permT T);
+ val cprm_eq = Const (@{const_name Nominal.prm_eq}, mk_permT T --> mk_permT T --> HOLogic.boolT);
(* nil axiom *)
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
(cperm $ cnil $ x, x));
@@ -309,7 +309,7 @@
(HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
in
- Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
+ Axclass.define_class (Binding.name cl_name, @{sort type}) []
[((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
((Binding.name (cl_name ^ "2"), []), [axiom2]),
((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
@@ -326,7 +326,8 @@
val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name);
val i_type1 = TFree("'x",[pt_name_qu]);
val i_type2 = Type(ak_name_qu,[]);
- val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
+ val cpt =
+ Const (@{const_name Nominal.pt}, (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val pt_type = Logic.mk_type i_type1;
val at_type = Logic.mk_type i_type2;
fun proof ctxt =
@@ -349,10 +350,10 @@
let
val cl_name = "fs_"^ak_name;
val pt_name = Sign.full_bname thy ("pt_"^ak_name);
- val ty = TFree("'a",["HOL.type"]);
+ val ty = TFree("'a",@{sort type});
val x = Free ("x", ty);
- val csupp = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
- val cfinite = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT)
+ val csupp = Const (@{const_name Nominal.supp}, ty --> HOLogic.mk_setT T);
+ val cfinite = Const (@{const_name finite}, HOLogic.mk_setT T --> HOLogic.boolT)
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
@@ -372,7 +373,7 @@
val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name);
val i_type1 = TFree("'x",[fs_name_qu]);
val i_type2 = Type(ak_name_qu,[]);
- val cfs = Const ("Nominal.fs",
+ val cfs = Const (@{const_name Nominal.fs},
(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val fs_type = Logic.mk_type i_type1;
val at_type = Logic.mk_type i_type2;
@@ -394,19 +395,19 @@
fold_map (fn (ak_name', T') => fn thy' =>
let
val cl_name = "cp_"^ak_name^"_"^ak_name';
- val ty = TFree("'a",["HOL.type"]);
+ val ty = TFree("'a",@{sort type});
val x = Free ("x", ty);
val pi1 = Free ("pi1", mk_permT T);
val pi2 = Free ("pi2", mk_permT T');
- val cperm1 = Const ("Nominal.perm", mk_permT T --> ty --> ty);
- val cperm2 = Const ("Nominal.perm", mk_permT T' --> ty --> ty);
- val cperm3 = Const ("Nominal.perm", mk_permT T --> mk_permT T' --> mk_permT T');
+ val cperm1 = Const (@{const_name Nominal.perm}, mk_permT T --> ty --> ty);
+ val cperm2 = Const (@{const_name Nominal.perm}, mk_permT T' --> ty --> ty);
+ val cperm3 = Const (@{const_name Nominal.perm}, mk_permT T --> mk_permT T' --> mk_permT T');
val ax1 = HOLogic.mk_Trueprop
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
in
- Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
+ Axclass.define_class (Binding.name cl_name, @{sort type}) []
[((Binding.name (cl_name ^ "1"), []), [ax1])] thy'
end) ak_names_types thy) ak_names_types thy12;
@@ -422,7 +423,7 @@
val i_type0 = TFree("'a",[cp_name_qu]);
val i_type1 = Type(ak_name_qu,[]);
val i_type2 = Type(ak_name_qu',[]);
- val ccp = Const ("Nominal.cp",
+ val ccp = Const (@{const_name Nominal.cp},
(Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
(Term.itselfT i_type2)-->HOLogic.boolT);
val at_type = Logic.mk_type i_type1;
@@ -456,7 +457,7 @@
val ak_name_qu' = Sign.full_bname thy' ak_name';
val i_type1 = Type(ak_name_qu,[]);
val i_type2 = Type(ak_name_qu',[]);
- val cdj = Const ("Nominal.disjoint",
+ val cdj = Const (@{const_name Nominal.disjoint},
(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val at_type = Logic.mk_type i_type1;
val at_type' = Logic.mk_type i_type2;
@@ -548,15 +549,14 @@
val pt_thm_unit = pt_unit_inst;
in
thy
- |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
- |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
- |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
- |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
- |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
- |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
- |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
- (pt_proof pt_thm_nprod)
- |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
+ |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+ |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
+ |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
+ |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+ |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
+ |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+ |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod)
+ |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (pt_proof pt_thm_unit)
end) ak_names thy13;
(******** fs_<ak> class instances ********)
@@ -614,12 +614,11 @@
val fs_thm_optn = fs_inst RS fs_option_inst;
in
thy
- |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
- |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
- |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
- (fs_proof fs_thm_nprod)
- |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
- |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+ |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (fs_proof fs_thm_unit)
+ |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
+ |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod)
+ |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
+ |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
end) ak_names thy20;
(******** cp_<ak>_<ai> class instances ********)
@@ -698,13 +697,13 @@
val cp_thm_set = cp_inst RS cp_set_inst;
in
thy'
- |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
+ |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (cp_proof cp_thm_unit)
|> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
- |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
- |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
- |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
- |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
- |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
+ |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
+ |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
+ |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+ |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+ |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
end) ak_names thy) ak_names thy25;
(* show that discrete nominal types are permutation types, finitely *)
--- a/src/HOL/Nominal/nominal_datatype.ML Sat Mar 22 18:15:09 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Mar 22 18:16:54 2014 +0100
@@ -90,13 +90,14 @@
val dj_cp = @{thm dj_cp};
-fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
- Type ("fun", [_, U])])) = (T, U);
+fun dest_permT (Type (@{type_name fun},
+ [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [T, _])]),
+ Type (@{type_name fun}, [_, U])])) = (T, U);
-fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
+fun permTs_of (Const (@{const_name Nominal.perm}, T) $ t $ u) = fst (dest_permT T) :: permTs_of u
| permTs_of _ = [];
-fun perm_simproc' ctxt (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
+fun perm_simproc' ctxt (Const (@{const_name Nominal.perm}, T) $ t $ (u as Const (@{const_name Nominal.perm}, U) $ r $ s)) =
let
val thy = Proof_Context.theory_of ctxt;
val (aT as Type (a, []), S) = dest_permT T;
@@ -140,23 +141,23 @@
let
val T = fastype_of1 (Ts, t);
val U = fastype_of1 (Ts, u)
- in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
+ in Const (@{const_name Nominal.perm}, T --> U --> U) $ t $ u end;
fun perm_of_pair (x, y) =
let
val T = fastype_of x;
val pT = mk_permT T
- in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
- HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
+ in Const (@{const_name Cons}, HOLogic.mk_prodT (T, T) --> pT --> pT) $
+ HOLogic.mk_prod (x, y) $ Const (@{const_name Nil}, pT)
end;
fun mk_not_sym ths = maps (fn th => case prop_of th of
_ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
| _ => [th]) ths;
-fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
+fun fresh_const T U = Const (@{const_name Nominal.fresh}, T --> U --> HOLogic.boolT);
fun fresh_star_const T U =
- Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
+ Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT);
fun gen_nominal_datatype prep_specs config dts thy =
let
@@ -185,8 +186,8 @@
(Sign.full_name thy n, Sign.full_name thy (Binding.suffix_name "_Rep" n))) dts;
val rps = map Library.swap ps;
- fun replace_types (Type ("Nominal.ABS", [T, U])) =
- Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
+ fun replace_types (Type (@{type_name ABS}, [T, U])) =
+ Type (@{type_name fun}, [T, Type (@{type_name noption}, [replace_types U])])
| replace_types (Type (s, Ts)) =
Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
| replace_types T = T;
@@ -208,14 +209,14 @@
(**** define permutation functions ****)
- val permT = mk_permT (TFree ("'x", HOLogic.typeS));
+ val permT = mk_permT (TFree ("'x", @{sort type}));
val pi = Free ("pi", permT);
val perm_types = map (fn (i, _) =>
let val T = nth_dtyp i
in permT --> T --> T end) descr;
val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
"perm_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
- val perm_names = replicate (length new_type_names) "Nominal.perm" @
+ val perm_names = replicate (length new_type_names) @{const_name Nominal.perm} @
map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
val perm_names_types = perm_names ~~ perm_types;
val perm_names_types' = perm_names' ~~ perm_types;
@@ -236,16 +237,16 @@
fold_rev (Term.abs o pair "x") Us
(Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
list_comb (x, map (fn (i, U) =>
- Const ("Nominal.perm", permT --> U --> U) $
- (Const ("List.rev", permT --> permT) $ pi) $
+ Const (@{const_name Nominal.perm}, permT --> U --> U) $
+ (Const (@{const_name rev}, permT --> permT) $ pi) $
Bound i) ((length Us - 1 downto 0) ~~ Us)))
end
- else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
+ else Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x
end;
in
(Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
(Free (nth perm_names_types' i) $
- Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
+ Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
list_comb (c, args),
list_comb (c, map perm_arg (dts ~~ args)))))
end) constrs
@@ -274,7 +275,7 @@
(map (fn (c as (s, T), x) =>
let val [T1, T2] = binder_types T
in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
- Const ("Nominal.perm", T) $ pi $ Free (x, T2))
+ Const (@{const_name Nominal.perm}, T) $ pi $ Free (x, T2))
end)
(perm_names_types ~~ perm_indnames))))
(fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
@@ -293,7 +294,7 @@
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map (fn ((s, T), x) => HOLogic.mk_eq
(Const (s, permT --> T --> T) $
- Const ("List.list.Nil", permT) $ Free (x, T),
+ Const (@{const_name Nil}, permT) $ Free (x, T),
Free (x, T)))
(perm_names ~~
map body_type perm_types ~~ perm_indnames)))))
@@ -326,7 +327,7 @@
(map (fn ((s, T), x) =>
let val perm = Const (s, permT --> T --> T)
in HOLogic.mk_eq
- (perm $ (Const ("List.append", permT --> permT --> permT) $
+ (perm $ (Const (@{const_name append}, permT --> permT --> permT) $
pi1 $ pi2) $ Free (x, T),
perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
end)
@@ -357,7 +358,7 @@
in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm
(Goal.prove_global_future thy2 [] []
(augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
- (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
+ (HOLogic.mk_Trueprop (Const (@{const_name Nominal.prm_eq},
permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map (fn ((s, T), x) =>
@@ -414,7 +415,7 @@
val pi2 = Free ("pi2", permT2);
val perm1 = Const (s, permT1 --> T --> T);
val perm2 = Const (s, permT2 --> T --> T);
- val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
+ val perm3 = Const (@{const_name Nominal.perm}, permT1 --> permT2 --> permT2)
in HOLogic.mk_eq
(perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
@@ -462,17 +463,17 @@
(map (fn (i, _) => Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr);
val big_rep_name =
space_implode "_" (Datatype_Prop.indexify_names (map_filter
- (fn (i, ("Nominal.noption", _, _)) => NONE
+ (fn (i, (@{type_name noption}, _, _)) => NONE
| (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
val _ = warning ("big_rep_name: " ^ big_rep_name);
fun strip_option (dtf as Datatype.DtType ("fun", [dt, Datatype.DtRec i])) =
(case AList.lookup op = descr i of
- SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
+ SOME (@{type_name noption}, _, [(_, [dt']), _]) =>
apfst (cons dt) (strip_option dt')
| _ => ([], dtf))
| strip_option (Datatype.DtType ("fun",
- [dt, Datatype.DtType ("Nominal.noption", [dt'])])) =
+ [dt, Datatype.DtType (@{type_name noption}, [dt'])])) =
apfst (cons dt) (strip_option dt')
| strip_option dt = ([], dt);
@@ -493,8 +494,8 @@
val free' = Datatype_Aux.app_bnds free (length Us);
fun mk_abs_fun T (i, t) =
let val U = fastype_of t
- in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
- Type ("Nominal.noption", [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
+ in (i + 1, Const (@{const_name Nominal.abs_fun}, [T, U, T] --->
+ Type (@{type_name noption}, [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
end
in (j + 1, j' + length Ts,
case dt'' of
@@ -513,7 +514,7 @@
val (intr_ts, (rep_set_names', recTs')) =
apfst flat (apsnd ListPair.unzip (ListPair.unzip (map_filter
- (fn ((_, ("Nominal.noption", _, _)), _) => NONE
+ (fn ((_, (@{type_name noption}, _, _)), _) => NONE
| ((i, (_, _, constrs)), rep_set_name) =>
let val T = nth_dtyp i
in SOME (map (make_intr rep_set_name T) constrs,
@@ -540,7 +541,7 @@
val abs_perm = Global_Theory.get_thms thy4 "abs_perm";
val perm_indnames' = map_filter
- (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
+ (fn (x, (_, (@{type_name noption}, _, _))) => NONE | (x, _) => SOME x)
(perm_indnames ~~ descr);
fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
@@ -553,7 +554,7 @@
val S = Const (s, T --> HOLogic.boolT);
val permT = mk_permT (Type (name, []))
in HOLogic.mk_imp (S $ Free (x, T),
- S $ (Const ("Nominal.perm", permT --> T --> T) $
+ S $ (Const (@{const_name Nominal.perm}, permT --> T --> T) $
Free ("pi", permT) $ Free (x, T)))
end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
(fn {context = ctxt, ...} => EVERY
@@ -581,15 +582,15 @@
(resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
let
val permT = mk_permT
- (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
+ (TFree (singleton (Name.variant_list (map fst tvs)) "'a", @{sort type}));
val pi = Free ("pi", permT);
val T = Type (Sign.full_name thy name, map TFree tvs);
in apfst (pair r o hd)
(Global_Theory.add_defs_unchecked true
[((Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals
- (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
+ (Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ Free ("x", T),
Const (Sign.intern_const thy ("Abs_" ^ Binding.name_of name), U --> T) $
- (Const ("Nominal.perm", permT --> U --> U) $ pi $
+ (Const (@{const_name Nominal.perm}, permT --> U --> U) $ pi $
(Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $
Free ("x", T))))), [])] thy)
end))
@@ -671,12 +672,12 @@
val T = fastype_of x;
val U = fastype_of t
in
- Const ("Nominal.abs_fun", T --> U --> T -->
- Type ("Nominal.noption", [U])) $ x $ t
+ Const (@{const_name Nominal.abs_fun}, T --> U --> T -->
+ Type (@{type_name noption}, [U])) $ x $ t
end;
val (ty_idxs, _) = List.foldl
- (fn ((i, ("Nominal.noption", _, _)), p) => p
+ (fn ((i, (@{type_name noption}, _, _)), p) => p
| ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
fun reindex (Datatype.DtType (s, dts)) = Datatype.DtType (s, map reindex dts)
@@ -691,7 +692,7 @@
in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
val (descr'', ndescr) = ListPair.unzip (map_filter
- (fn (i, ("Nominal.noption", _, _)) => NONE
+ (fn (i, (@{type_name noption}, _, _)) => NONE
| (i, (s, dts, constrs)) =>
let
val SOME index = AList.lookup op = ty_idxs i;
@@ -817,8 +818,8 @@
(augment_sort thy8
(pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
(HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
- Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
+ (Const (@{const_name Nominal.perm}, permT --> U --> U) $ pi $ (Rep $ x),
+ Rep $ (Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x)))))
(fn {context = ctxt, ...} =>
simp_tac (put_simpset HOL_basic_ss ctxt addsimps (perm_defs @ Abs_inverse_thms @
perm_closed_thms @ Rep_thms)) 1)
@@ -860,7 +861,7 @@
fun perm t =
let val T = fastype_of t
- in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
+ in Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ t end;
fun constr_arg (dts, dt) (j, l_args, r_args) =
let
@@ -977,7 +978,7 @@
val Ts = map fastype_of args1;
val c = list_comb (Const (cname, Ts ---> T), args1);
fun supp t =
- Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
+ Const (@{const_name Nominal.supp}, fastype_of t --> HOLogic.mk_setT atomT) $ t;
fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
val supp_thm = Goal.prove_global_future thy8 [] []
(augment_sort thy8 pt_cp_sort
@@ -1070,8 +1071,8 @@
(augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
(HOLogic.mk_Trueprop
(foldr1 HOLogic.mk_conj (map (fn (s, T) =>
- Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
- (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
+ Const (@{const_name finite}, HOLogic.mk_setT atomT --> HOLogic.boolT) $
+ (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT atomT) $ Free (s, T)))
(indnames ~~ recTs)))))
(fn {context = ctxt, ...} => Datatype_Aux.ind_tac dt_induct indnames 1 THEN
ALLGOALS (asm_full_simp_tac (ctxt addsimps
@@ -1112,10 +1113,10 @@
val pnames = if length descr'' = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
- val ind_sort = if null dt_atomTs then HOLogic.typeS
+ val ind_sort = if null dt_atomTs then @{sort type}
else Sign.minimize_sort thy9 (Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms));
val fsT = TFree ("'n", ind_sort);
- val fsT' = TFree ("'n", HOLogic.typeS);
+ val fsT' = TFree ("'n", @{sort type});
val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
(Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
@@ -1183,7 +1184,7 @@
val ind_prems' =
map (fn (_, f as Free (_, T)) => Logic.all (Free ("x", fsT'))
- (HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
+ (HOLogic.mk_Trueprop (Const (@{const_name finite},
Term.range_type T -->
HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
@@ -1345,7 +1346,7 @@
cut_facts_tac iprems 1,
(resolve_tac prems THEN_ALL_NEW
SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
- _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
+ _ $ (Const (@{const_name Nominal.fresh}, _) $ _ $ _) =>
simp_tac ind_ss1' i
| _ $ (Const (@{const_name Not}, _) $ _) =>
resolve_tac freshs2' i
@@ -1371,7 +1372,7 @@
map (fn (_, f) =>
let val f' = Logic.varify_global f
in (cterm_of thy9 f',
- cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
+ cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f')))
end) fresh_fs) induct_aux;
val induct = Goal.prove_global_future thy9 []
@@ -1398,7 +1399,7 @@
val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' used;
- val rec_sort = if null dt_atomTs then HOLogic.typeS else
+ val rec_sort = if null dt_atomTs then @{sort type} else
Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
@@ -1459,8 +1460,8 @@
HOLogic.mk_Trueprop (nth rec_preds i $ Free y)) (recs ~~ frees'');
val prems5 = mk_fresh3 (recs ~~ frees'') frees';
val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
- (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
- (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
+ (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+ (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT aT) $ Free y)))
frees'') atomTs;
val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
(fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
@@ -1534,7 +1535,7 @@
(Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
(fn {context = ctxt, ...} => dtac (Thm.instantiate ([],
[(cterm_of thy11 (Var (("pi", 0), permT)),
- cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
+ cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN
NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths)
in (ths, ths') end) dt_atomTs);
@@ -1545,9 +1546,9 @@
val name = Long_Name.base_name (fst (dest_Type aT));
val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
val aset = HOLogic.mk_setT aT;
- val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
+ val finite = Const (@{const_name finite}, aset --> HOLogic.boolT);
val fins = map (fn (f, T) => HOLogic.mk_Trueprop
- (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
+ (finite $ (Const (@{const_name Nominal.supp}, T --> aset) $ f)))
(rec_fns ~~ rec_fn_Ts)
in
map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm
@@ -1561,7 +1562,7 @@
val y = Free ("y" ^ string_of_int i, U)
in
HOLogic.mk_imp (R $ x $ y,
- finite $ (Const ("Nominal.supp", U --> aset) $ y))
+ finite $ (Const (@{const_name Nominal.supp}, U --> aset) $ y))
end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
(1 upto length recTs))))))
(fn {prems = fins, context = ctxt} =>
@@ -1573,8 +1574,8 @@
val finite_premss = map (fn aT =>
map (fn (f, T) => HOLogic.mk_Trueprop
- (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
- (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
+ (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+ (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT aT) $ f)))
(rec_fns ~~ rec_fn_Ts)) dt_atomTs;
val rec_fns' = map (augment_sort thy11 fs_cp_sort) rec_fns;
@@ -1613,7 +1614,7 @@
in EVERY
[rtac (Drule.cterm_instantiate
[(cterm_of thy11 S,
- cterm_of thy11 (Const ("Nominal.supp",
+ cterm_of thy11 (Const (@{const_name Nominal.supp},
fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
supports_fresh) 1,
simp_tac (put_simpset HOL_basic_ss context addsimps
@@ -1654,7 +1655,7 @@
val induct_aux_rec = Drule.cterm_instantiate
(map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
(map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
- Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
+ Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
fresh_fs @
map (fn (((P, T), (x, U)), Q) =>
(Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
@@ -1684,8 +1685,8 @@
val finite_ctxt_prems = map (fn aT =>
HOLogic.mk_Trueprop
- (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
- (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
+ (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+ (Const (@{const_name Nominal.supp}, fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
val rec_unique_thms = Datatype_Aux.split_conj_thm (Goal.prove
(Proof_Context.init_global thy11) (map fst rec_unique_frees)
@@ -1752,7 +1753,7 @@
| _ => false)
| _ => false) prems';
val fresh_prems = filter (fn th => case prop_of th of
- _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
+ _ $ (Const (@{const_name Nominal.fresh}, _) $ _ $ _) => true
| _ $ (Const (@{const_name Not}, _) $ _) => true
| _ => false) prems';
val Ts = map fastype_of boundsl;
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat Mar 22 18:15:09 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat Mar 22 18:16:54 2014 +0100
@@ -87,8 +87,8 @@
| get_inner_fresh_fun (v as Var _) = NONE
| get_inner_fresh_fun (Const _) = NONE
| get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t
- | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u)
- = SOME T
+ | get_inner_fresh_fun (Const (@{const_name Nominal.fresh_fun},
+ Type(@{type_name fun},[Type (@{type_name fun},[Type (T,_),_]),_])) $ u) = SOME T
| get_inner_fresh_fun (t $ u) =
let val a = get_inner_fresh_fun u in
if a = NONE then get_inner_fresh_fun t else a
--- a/src/HOL/Nominal/nominal_inductive.ML Sat Mar 22 18:15:09 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Sat Mar 22 18:16:54 2014 +0100
@@ -196,7 +196,7 @@
end) (Logic.strip_imp_prems raw_induct' ~~ avoids');
val atomTs = distinct op = (maps (map snd o #2) prems);
- val ind_sort = if null atomTs then HOLogic.typeS
+ val ind_sort = if null atomTs then @{sort type}
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
@@ -332,7 +332,7 @@
fun concat_perm pi1 pi2 =
let val T = fastype_of pi1
in if T = fastype_of pi2 then
- Const (@{const_name List.append}, T --> T --> T) $ pi1 $ pi2
+ Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
else pi2
end;
val pis'' = fold (concat_perm #> map) pis' pis;
--- a/src/HOL/Nominal/nominal_inductive2.ML Sat Mar 22 18:15:09 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Mar 22 18:16:54 2014 +0100
@@ -45,7 +45,7 @@
fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
(theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
- fn Const ("Nominal.perm", _) $ _ $ t =>
+ fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
then SOME perm_bool else NONE
| _ => NONE);
@@ -97,13 +97,13 @@
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
- Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
+ Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
(subst_bounds (pis, strip_all pis q))))
else NONE
| _ => NONE)
| inst_conj_all names ps pis t u =
if member (op aconv) ps (head_of u) then
- SOME (Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
+ SOME (Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
(subst_bounds (pis, strip_all pis t)))
else NONE
| inst_conj_all _ _ _ _ _ = NONE;
@@ -222,7 +222,7 @@
val atomTs = distinct op = (maps (map snd o #2) prems);
val atoms = map (fst o dest_Type) atomTs;
- val ind_sort = if null atomTs then HOLogic.typeS
+ val ind_sort = if null atomTs then @{sort type}
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
("fs_" ^ Long_Name.base_name a)) atoms));
val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
@@ -292,7 +292,7 @@
("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
- addsimprocs [mk_perm_bool_simproc ["Fun.id"],
+ addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
@@ -312,7 +312,7 @@
(** protect terms to avoid that fresh_star_prod_set interferes with **)
(** pairs used in introduction rules of inductive predicate **)
fun protect t =
- let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end;
+ let val T = fastype_of t in Const (@{const_name Fun.id}, T --> T) $ t end;
val p = foldr1 HOLogic.mk_prod (map protect ts);
val atom = fst (dest_Type T);
val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
@@ -393,7 +393,7 @@
fun concat_perm pi1 pi2 =
let val T = fastype_of pi1
in if T = fastype_of pi2 then
- Const ("List.append", T --> T --> T) $ pi1 $ pi2
+ Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
else pi2
end;
val pis'' = fold_rev (concat_perm #> map) pis' pis;
--- a/src/HOL/Nominal/nominal_permeq.ML Sat Mar 22 18:15:09 2014 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Sat Mar 22 18:16:54 2014 +0100
@@ -97,14 +97,15 @@
(* constant or when (f x) is a permuation with two or more arguments *)
fun applicable_app t =
(case (strip_comb t) of
- (Const ("Nominal.perm",_),ts) => (length ts) >= 2
+ (Const (@{const_name Nominal.perm},_),ts) => (length ts) >= 2
| (Const _,_) => false
| _ => true)
in
case redex of
(* case pi o (f x) == (pi o f) (pi o x) *)
- (Const("Nominal.perm",
- Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
+ (Const(@{const_name Nominal.perm},
+ Type(@{type_name fun},
+ [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(if (applicable_app f) then
let
val name = Long_Name.base_name n
@@ -124,13 +125,13 @@
fun applicable_fun t =
(case (strip_comb t) of
(Abs _ ,[]) => true
- | (Const ("Nominal.perm",_),_) => false
+ | (Const (@{const_name Nominal.perm},_),_) => false
| (Const _, _) => true
| _ => false)
in
case redex of
(* case pi o f == (%x. pi o (f ((rev pi)o x))) *)
- (Const("Nominal.perm",_) $ pi $ f) =>
+ (Const(@{const_name Nominal.perm},_) $ pi $ f) =>
(if applicable_fun f then SOME perm_fun_def else NONE)
| _ => NONE
end
@@ -190,9 +191,9 @@
fun perm_compose_simproc' ctxt redex =
(case redex of
- (Const ("Nominal.perm", Type ("fun", [Type ("List.list",
- [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
- Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $
+ (Const (@{const_name Nominal.perm}, Type (@{type_name fun}, [Type (@{type_name list},
+ [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm},
+ Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $
pi2 $ t)) =>
let
val thy = Proof_Context.theory_of ctxt
@@ -293,7 +294,7 @@
let val goal = nth (cprems_of st) (i - 1)
in
case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
- _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
+ _ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) =>
let
val cert = Thm.cterm_of (Thm.theory_of_thm st);
val ps = Logic.strip_params (term_of goal);
@@ -303,7 +304,7 @@
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
vs HOLogic.unit;
val s' = fold_rev Term.abs ps
- (Const ("Nominal.supp", fastype_of1 (Ts, s) -->
+ (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) -->
Term.range_type T) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
@@ -337,7 +338,7 @@
val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
case Logic.strip_assums_concl (term_of goal) of
- _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) =>
+ _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) =>
let
val cert = Thm.cterm_of (Thm.theory_of_thm st);
val ps = Logic.strip_params (term_of goal);
@@ -348,7 +349,7 @@
vs HOLogic.unit;
val s' =
fold_rev Term.abs ps
- (Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
+ (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));