--- a/src/HOL/Nominal/nominal_atoms.ML Fri Apr 28 15:53:47 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Fri Apr 28 15:54:34 2006 +0200
@@ -1,4 +1,9 @@
-(* $Id$ *)
+(* Title: HOL/Nominal/nominal_atoms.ML
+ ID: $Id$
+ Author: Christian Urban and Stefan Berghofer, TU Muenchen
+
+Declaration of atom types to be used in nominal datatypes.
+*)
signature NOMINAL_ATOMS =
sig
@@ -80,7 +85,7 @@
val ab = Free ("ab", HOLogic.mk_prodT (T, T))
val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
val cswap_akname = Const (swap_name, swapT);
- val cswap = Const ("nominal.swap", swapT)
+ val cswap = Const ("Nominal.swap", swapT)
val name = "swap_"^ak_name^"_def";
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -136,7 +141,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 ("Nominal.perm", mk_permT T --> T' --> T');
val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T --> T' --> T');
val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
@@ -154,7 +159,7 @@
let
val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
val i_type = Type(ak_name_qu,[]);
- val cat = Const ("nominal.at",(Term.itselfT i_type) --> HOLogic.boolT);
+ val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT);
val at_type = Logic.mk_type i_type;
val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy5
[Name "at_def",
@@ -185,10 +190,10 @@
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 cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
val cnil = Const ("List.list.Nil", mk_permT T);
val cappend = Const ("List.op @",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 cprm_eq = Const ("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));
@@ -217,7 +222,7 @@
val pt_name_qu = Sign.full_name (sign_of 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 ("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;
val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy7
@@ -243,7 +248,7 @@
val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
val ty = TFree("'a",["HOL.type"]);
val x = Free ("x", ty);
- val csupp = Const ("nominal.supp", ty --> HOLogic.mk_setT T);
+ val csupp = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
@@ -263,7 +268,7 @@
val fs_name_qu = Sign.full_name (sign_of 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 ("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;
@@ -290,9 +295,9 @@
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 ("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 ax1 = HOLogic.mk_Trueprop
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
@@ -313,7 +318,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 ("Nominal.cp",
(Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
(Term.itselfT i_type2)-->HOLogic.boolT);
val at_type = Logic.mk_type i_type1;
@@ -344,7 +349,7 @@
val ak_name_qu' = Sign.full_name (sign_of 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 ("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;
@@ -436,11 +441,11 @@
in
thy
|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
- |> AxClass.prove_arity ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
+ |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
|> AxClass.prove_arity ("Datatype.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 ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
- |> AxClass.prove_arity ("nominal.nprod",[[cls_name],[cls_name]],[cls_name])
+ |> 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 ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
@@ -502,7 +507,7 @@
thy
|> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
|> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
- |> AxClass.prove_arity ("nominal.nprod",[[cls_name],[cls_name]],[cls_name])
+ |> 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 ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
@@ -586,7 +591,7 @@
|> 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 ("Datatype.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 ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
end) ak_names thy) ak_names thy25;
(* show that discrete nominal types are permutation types, finitely *)
@@ -609,7 +614,7 @@
fold (fn ak_name => fn thy =>
let
val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
- val supp_def = thm "nominal.supp_def";
+ val supp_def = thm "Nominal.supp_def";
val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
in
@@ -620,7 +625,7 @@
fold (fn ak_name' => (fold (fn ak_name => fn thy =>
let
val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
- val supp_def = thm "nominal.supp_def";
+ val supp_def = thm "Nominal.supp_def";
val simp_s = HOL_ss addsimps [defn];
val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
in
@@ -646,32 +651,32 @@
(* abbreviations for some lemmas *)
(*===============================*)
- val abs_fun_pi = thm "nominal.abs_fun_pi";
- val abs_fun_pi_ineq = thm "nominal.abs_fun_pi_ineq";
- val abs_fun_eq = thm "nominal.abs_fun_eq";
- val dj_perm_forget = thm "nominal.dj_perm_forget";
- val dj_pp_forget = thm "nominal.dj_perm_perm_forget";
- val fresh_iff = thm "nominal.fresh_abs_fun_iff";
- val fresh_iff_ineq = thm "nominal.fresh_abs_fun_iff_ineq";
- val abs_fun_supp = thm "nominal.abs_fun_supp";
- val abs_fun_supp_ineq = thm "nominal.abs_fun_supp_ineq";
- val pt_swap_bij = thm "nominal.pt_swap_bij";
- val pt_fresh_fresh = thm "nominal.pt_fresh_fresh";
- val pt_bij = thm "nominal.pt_bij";
- val pt_perm_compose = thm "nominal.pt_perm_compose";
- val pt_perm_compose' = thm "nominal.pt_perm_compose'";
- val perm_app = thm "nominal.pt_fun_app_eq";
- val at_fresh = thm "nominal.at_fresh";
- val at_calc = thms "nominal.at_calc";
- val at_supp = thm "nominal.at_supp";
- val dj_supp = thm "nominal.dj_supp";
- val fresh_left_ineq = thm "nominal.pt_fresh_left_ineq";
- val fresh_left = thm "nominal.pt_fresh_left";
- val fresh_bij_ineq = thm "nominal.pt_fresh_bij_ineq";
- val fresh_bij = thm "nominal.pt_fresh_bij";
- val pt_pi_rev = thm "nominal.pt_pi_rev";
- val pt_rev_pi = thm "nominal.pt_rev_pi";
- val fresh_fun_eqvt = thm "nominal.fresh_fun_equiv";
+ val abs_fun_pi = thm "Nominal.abs_fun_pi";
+ val abs_fun_pi_ineq = thm "Nominal.abs_fun_pi_ineq";
+ val abs_fun_eq = thm "Nominal.abs_fun_eq";
+ val dj_perm_forget = thm "Nominal.dj_perm_forget";
+ val dj_pp_forget = thm "Nominal.dj_perm_perm_forget";
+ val fresh_iff = thm "Nominal.fresh_abs_fun_iff";
+ val fresh_iff_ineq = thm "Nominal.fresh_abs_fun_iff_ineq";
+ val abs_fun_supp = thm "Nominal.abs_fun_supp";
+ val abs_fun_supp_ineq = thm "Nominal.abs_fun_supp_ineq";
+ val pt_swap_bij = thm "Nominal.pt_swap_bij";
+ val pt_fresh_fresh = thm "Nominal.pt_fresh_fresh";
+ val pt_bij = thm "Nominal.pt_bij";
+ val pt_perm_compose = thm "Nominal.pt_perm_compose";
+ val pt_perm_compose' = thm "Nominal.pt_perm_compose'";
+ val perm_app = thm "Nominal.pt_fun_app_eq";
+ val at_fresh = thm "Nominal.at_fresh";
+ val at_calc = thms "Nominal.at_calc";
+ val at_supp = thm "Nominal.at_supp";
+ val dj_supp = thm "Nominal.dj_supp";
+ val fresh_left_ineq = thm "Nominal.pt_fresh_left_ineq";
+ val fresh_left = thm "Nominal.pt_fresh_left";
+ val fresh_bij_ineq = thm "Nominal.pt_fresh_bij_ineq";
+ val fresh_bij = thm "Nominal.pt_fresh_bij";
+ val pt_pi_rev = thm "Nominal.pt_pi_rev";
+ val pt_rev_pi = thm "Nominal.pt_rev_pi";
+ val fresh_fun_eqvt = thm "Nominal.fresh_fun_equiv";
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
(* types; this allows for example to use abs_perm (which is a *)
--- a/src/HOL/Nominal/nominal_package.ML Fri Apr 28 15:53:47 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Fri Apr 28 15:54:34 2006 +0200
@@ -1,4 +1,9 @@
-(* $Id$ *)
+(* Title: HOL/Nominal/nominal_package.ML
+ ID: $Id$
+ Author: Stefan Berghofer and Christian Urban, TU Muenchen
+
+Nominal datatype package for Isabelle/HOL.
+*)
signature NOMINAL_PACKAGE =
sig
@@ -97,10 +102,10 @@
fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
Type ("fun", [_, U])])) = (T, U);
-fun permTs_of (Const ("nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
+fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
| permTs_of _ = [];
-fun perm_simproc' thy ss (Const ("nominal.perm", T) $ t $ (u as Const ("nominal.perm", U) $ r $ s)) =
+fun perm_simproc' thy ss (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
let
val (aT as Type (a, []), S) = dest_permT T;
val (bT as Type (b, []), _) = dest_permT U
@@ -172,8 +177,8 @@
(Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) 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 ("Nominal.ABS", [T, U])) =
+ Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
| replace_types (Type (s, Ts)) =
Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
| replace_types T = T;
@@ -203,7 +208,7 @@
val perm_types = map (fn (i, _) =>
let val T = nth_dtyp i
in permT --> T --> T end) descr;
- val perm_names = replicate (length new_type_names) "nominal.perm" @
+ val perm_names = replicate (length new_type_names) "Nominal.perm" @
DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
("perm_" ^ name_of_typ (nth_dtyp i)))
(length new_type_names upto length descr - 1));
@@ -224,11 +229,11 @@
in list_abs (map (pair "x") Us,
Const (List.nth (perm_names_types, body_index dt)) $ pi $
list_comb (x, map (fn (i, U) =>
- Const ("nominal.perm", permT --> U --> U) $
+ Const ("Nominal.perm", permT --> U --> U) $
(Const ("List.rev", permT --> permT) $ pi) $
Bound i) ((length Us - 1 downto 0) ~~ Us)))
end
- else Const ("nominal.perm", permT --> T --> T) $ pi $ x
+ else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
end;
in
(("", HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -261,7 +266,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 ("Nominal.perm", T) $ pi $ Free (x, T2))
end)
(perm_names_types ~~ perm_indnames))))
(fn _ => EVERY [indtac induction perm_indnames 1,
@@ -345,7 +350,7 @@
(Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
in List.take (map standard (split_conj_thm
(Goal.prove thy2 [] [] (Logic.mk_implies
- (HOLogic.mk_Trueprop (Const ("nominal.prm_eq",
+ (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map (fn ((s, T), x) =>
@@ -402,7 +407,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 ("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)))
@@ -444,16 +449,16 @@
(map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
val big_rep_name =
space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
- (fn (i, ("nominal.noption", _, _)) => NONE
+ (fn (i, ("Nominal.noption", _, _)) => NONE
| (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
val _ = warning ("big_rep_name: " ^ big_rep_name);
fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
(case AList.lookup op = descr i of
- SOME ("nominal.noption", _, [(_, [dt']), _]) =>
+ SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
apfst (cons dt) (strip_option dt')
| _ => ([], dtf))
- | strip_option (DtType ("fun", [dt, DtType ("nominal.noption", [dt'])])) =
+ | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) =
apfst (cons dt) (strip_option dt')
| strip_option dt = ([], dt);
@@ -474,8 +479,8 @@
val free' = 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])) $ mk_Free "y" T i $ t)
+ in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
+ Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
end
in (j + 1, j' + length Ts,
case dt'' of
@@ -496,7 +501,7 @@
val (intr_ts, ind_consts) =
apfst List.concat (ListPair.unzip (List.mapPartial
- (fn ((_, ("nominal.noption", _, _)), _) => NONE
+ (fn ((_, ("Nominal.noption", _, _)), _) => NONE
| ((i, (_, _, constrs)), rep_set_name) =>
let val T = nth_dtyp i
in SOME (map (make_intr rep_set_name T) constrs,
@@ -514,7 +519,7 @@
val _ = warning "proving closure under permutation...";
val perm_indnames' = List.mapPartial
- (fn (x, (_, ("nominal.noption", _, _))) => NONE | (x, _) => SOME x)
+ (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
(perm_indnames ~~ descr);
fun mk_perm_closed name = map (fn th => standard (th RS mp))
@@ -527,7 +532,7 @@
val T = HOLogic.dest_setT (fastype_of S);
val permT = mk_permT (Type (name, []))
in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
- HOLogic.mk_mem (Const ("nominal.perm", permT --> T --> T) $
+ HOLogic.mk_mem (Const ("Nominal.perm", permT --> T --> T) $
Free ("pi", permT) $ Free (x, T), S))
end) (ind_consts ~~ perm_indnames'))))
(fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
@@ -561,9 +566,9 @@
val Const (_, Type (_, [U])) = c
in apfst (pair r o hd)
(PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
- (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
+ (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
- (Const ("nominal.perm", permT --> U --> U) $ pi $
+ (Const ("Nominal.perm", permT --> U --> U) $ pi $
(Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
Free ("x", T))))), [])] thy)
end))
@@ -637,12 +642,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 ("Nominal.abs_fun", T --> U --> T -->
+ Type ("Nominal.noption", [U])) $ x $ t
end;
val (ty_idxs, _) = foldl
- (fn ((i, ("nominal.noption", _, _)), p) => p
+ (fn ((i, ("Nominal.noption", _, _)), p) => p
| ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
@@ -657,7 +662,7 @@
in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
val (descr'', ndescr) = ListPair.unzip (List.mapPartial
- (fn (i, ("nominal.noption", _, _)) => NONE
+ (fn (i, ("Nominal.noption", _, _)) => NONE
| (i, (s, dts, constrs)) =>
let
val SOME index = AList.lookup op = ty_idxs i;
@@ -682,7 +687,7 @@
Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
val recTs' = List.mapPartial
- (fn ((_, ("nominal.noption", _, _)), T) => NONE
+ (fn ((_, ("Nominal.noption", _, _)), T) => NONE
| (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
val recTs = get_rec_types descr'' sorts';
val newTs' = Library.take (length new_type_names, recTs');
@@ -783,8 +788,8 @@
val pi = Free ("pi", permT);
in
standard (Goal.prove thy8 [] [] (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 ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
+ Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x))))
(fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
perm_closed_thms @ Rep_thms)) 1))
end) Rep_thms;
@@ -829,7 +834,7 @@
fun perm t =
let val T = fastype_of t
- in Const ("nominal.perm", permT --> T --> T) $ pi $ t end;
+ in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
fun constr_arg (dt, (j, l_args, r_args)) =
let
@@ -949,9 +954,9 @@
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 ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
fun fresh t =
- Const ("nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
+ Const ("Nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
Free ("a", atomT) $ t;
val supp_thm = standard (Goal.prove thy8 [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -1060,7 +1065,7 @@
in map standard (List.take
(split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop
(foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem
- (Const ("nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
+ (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT))))
(indnames ~~ recTs))))
(fn _ => indtac dt_induct indnames 1 THEN
@@ -1139,7 +1144,7 @@
val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
map (make_ind_prem fsT (fn T => fn t => fn u =>
- Const ("nominal.fresh", T --> fsT --> HOLogic.boolT) $ t $ u) i T)
+ 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);
@@ -1167,7 +1172,7 @@
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 ("Nominal.perm", T --> U --> U) $ t $ u end;
val aux_ind_vars =
(DatatypeProp.indexify_names (replicate (length dt_atomTs) "pi") ~~
@@ -1213,7 +1218,7 @@
(Const ("insert", T --> S --> S) $
(foldr (mk_perm (T :: Ts)) (Bound (n - i - j)) prms) $
(Const ("op Un", S --> S --> S) $ (f $ Bound (n - k - p)) $
- (Const ("nominal.supp", U --> S) $
+ (Const ("Nominal.supp", U --> S) $
foldr (mk_perm (T :: Ts)) (Bound (n - i')) prms))))))
end;
@@ -1304,7 +1309,7 @@
map (fn (_, f) =>
let val f' = Logic.varify f
in (cterm_of thy9 f',
- cterm_of thy9 (Const ("nominal.supp", fastype_of f')))
+ cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
end) fresh_fs) induct_aux;
val induct = standard (Goal.prove thy9 [] ind_prems ind_concl
@@ -1352,7 +1357,7 @@
fun partition_cargs idxs xs = map (fn (i, j) =>
(List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
- fun mk_fresh_fun (a, t) = Const ("nominal.fresh_fun",
+ fun mk_fresh_fun (a, t) = Const ("Nominal.fresh_fun",
(fastype_of a --> fastype_of t) --> fastype_of t) $ lambda a t;
fun make_rec_intr T rec_set ((rec_intr_ts, l), ((cname, cargs), idxs)) =
--- a/src/HOL/Nominal/nominal_permeq.ML Fri Apr 28 15:53:47 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Apr 28 15:54:34 2006 +0200
@@ -1,7 +1,10 @@
-(* $Id$ *)
+(* Title: HOL/Nominal/nominal_permeq.ML
+ ID: $Id$
+ Author: Christian Urban, TU Muenchen
-(* METHODS FOR SIMPLIFYING PERMUTATIONS AND *)
-(* FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
+Methods for simplifying permutations and
+for analysing equations involving permutations.
+*)
local
@@ -10,8 +13,8 @@
fun dynamic_thm ss name = ProofContext.get_thm (Simplifier.the_context ss) (Name name);
(* a tactic simplyfying permutations *)
-val perm_fun_def = thm "nominal.perm_fun_def"
-val perm_eq_app = thm "nominal.pt_fun_app_eq"
+val perm_fun_def = thm "Nominal.perm_fun_def"
+val perm_eq_app = thm "Nominal.pt_fun_app_eq"
fun perm_eval_tac ss i =
let
@@ -22,7 +25,7 @@
(* more arguments *)
fun applicable t =
(case (strip_comb t) of
- (Const ("nominal.perm",_),ts) => (length ts) >= 2
+ (Const ("Nominal.perm",_),ts) => (length ts) >= 2
| (Const _,_) => false
| _ => true)
@@ -30,7 +33,7 @@
(case redex of
(* case pi o (f x) == (pi o f) (pi o x) *)
(* special treatment according to the head of f *)
- (Const("nominal.perm",
+ (Const("Nominal.perm",
Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(case (applicable f) of
false => NONE
@@ -42,14 +45,14 @@
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
(* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
- | (Const("nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
+ | (Const("Nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
(* no redex otherwise *)
| _ => NONE) end
val perm_eval =
Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval"
- ["nominal.perm pi x"] perm_eval_simproc;
+ ["Nominal.perm pi x"] perm_eval_simproc;
(* these lemmas are created dynamically according to the atom types *)
val perm_swap = dynamic_thms ss "perm_swap"
@@ -80,8 +83,8 @@
let
fun perm_compose_simproc sg ss redex =
(case redex of
- (Const ("nominal.perm", Type ("fun", [Type ("List.list",
- [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("nominal.perm",
+ (Const ("Nominal.perm", Type ("fun", [Type ("List.list",
+ [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $
pi2 $ t)) =>
let
@@ -107,7 +110,7 @@
val perm_compose =
Simplifier.simproc (the_context()) "perm_compose"
- ["nominal.perm pi1 (nominal.perm pi2 t)"] perm_compose_simproc;
+ ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc;
val ss' = Simplifier.theory_context (the_context ()) empty_ss
@@ -133,7 +136,7 @@
(* %x. pi o (f ((rev pi) o x)) = rhs *)
fun unfold_perm_fun_def_tac i =
let
- val perm_fun_def = thm "nominal.perm_fun_def"
+ val perm_fun_def = thm "Nominal.perm_fun_def"
in
("unfolding of permutations on functions",
rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
@@ -148,7 +151,7 @@
(* should be able to analyse pi o fresh_fun () = fresh_fun instances *)
fun fresh_fun_eqvt_tac i =
let
- val fresh_fun_equiv = thm "nominal.fresh_fun_equiv_ineq"
+ val fresh_fun_equiv = thm "Nominal.fresh_fun_equiv_ineq"
in
("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i)
end
@@ -184,9 +187,9 @@
(* and strips off the intros, then applies perm_full_simp_tac *)
fun supports_tac tactical ss i =
let
- val supports_def = thm "nominal.op supports_def";
- val fresh_def = thm "nominal.fresh_def";
- val fresh_prod = thm "nominal.fresh_prod";
+ val supports_def = thm "Nominal.op supports_def";
+ val fresh_def = thm "Nominal.fresh_def";
+ val fresh_prod = thm "Nominal.fresh_prod";
val simps = [supports_def,symmetric fresh_def,fresh_prod]
in
EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i),
@@ -215,7 +218,7 @@
let val goal = List.nth(cprems_of st, i-1)
in
case Logic.strip_assums_concl (term_of goal) of
- _ $ (Const ("op :", _) $ (Const ("nominal.supp", T) $ x) $
+ _ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $
Const ("Finite_Set.Finites", _)) =>
let
val cert = Thm.cterm_of (sign_of_thm st);
@@ -226,7 +229,7 @@
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
HOLogic.unit vs;
val s' = list_abs (ps,
- Const ("nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
+ Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (prems_of supports_rule'));