nominal2: Nominal-General/nominal_library.ML@0c9ef14e9ba4 (annotated)

1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	(* Title: nominal_library.ML
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	Author: Christian Urban
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	3
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	Basic function for nominal.
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	*)
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	signature NOMINAL_LIBRARY =
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	sig
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	9
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	10
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	val mk_minus: term -> term
1896 996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	12	val mk_plus: term -> term -> term
996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	13
1899 8e0bfb14f6bf optimised the code of define_raw_perm Christian Urban <urbanc@in.tum.de> parents: 1896 diff changeset	14	val perm_ty: typ -> typ
1871 c704d129862b moved some general function into nominal_library.ML Christian Urban <urbanc@in.tum.de> parents: 1834 diff changeset	15	val mk_perm_ty: typ -> term -> term -> term
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	val mk_perm: term -> term -> term
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	17	val dest_perm: term -> term * term
9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	18
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	19	val mk_sort_of: term -> term
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	20	val mk_atom_ty: typ -> term -> term
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	21	val mk_atom: term -> term
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	22
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	23	val mk_equiv: thm -> thm
9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	24	val safe_mk_equiv: thm -> thm
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	end
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	27
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	structure Nominal_Library: NOMINAL_LIBRARY =
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	struct
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	30
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	fun mk_minus p =
1896 996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	32	@{term "uminus::perm => perm"} $ p
996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	33
996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	34	fun mk_plus p q =
996d4411e95e tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) Christian Urban <urbanc@in.tum.de> parents: 1871 diff changeset	35	@{term "plus::perm => perm => perm"} $ p $ q
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	36
1963 0c9ef14e9ba4 some tuning Christian Urban <urbanc@in.tum.de> parents: 1962 diff changeset	37	fun perm_ty ty = @{typ "perm"} --> ty --> ty
1871 c704d129862b moved some general function into nominal_library.ML Christian Urban <urbanc@in.tum.de> parents: 1834 diff changeset	38	fun mk_perm_ty ty p trm =
1899 8e0bfb14f6bf optimised the code of define_raw_perm Christian Urban <urbanc@in.tum.de> parents: 1896 diff changeset	39	Const (@{const_name "permute"}, perm_ty ty) $ p $ trm
1871 c704d129862b moved some general function into nominal_library.ML Christian Urban <urbanc@in.tum.de> parents: 1834 diff changeset	40	fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	41
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	42	fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	43	\| dest_perm t = raise TERM ("dest_perm", [t])
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	44
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	45
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	46	fun mk_sort_of t = @{term "sort_of"} $ t;
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	47
1963 0c9ef14e9ba4 some tuning Christian Urban <urbanc@in.tum.de> parents: 1962 diff changeset	48	fun atom_ty ty = ty --> @{typ "atom"}
0c9ef14e9ba4 some tuning Christian Urban <urbanc@in.tum.de> parents: 1962 diff changeset	49	fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	50	fun mk_atom t = mk_atom_ty (fastype_of t) t;
84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	51
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	52	fun mk_equiv r = r RS @{thm eq_reflection};
9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	53	fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	54
1962 84a13d1e2511 moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base Christian Urban <urbanc@in.tum.de> parents: 1899 diff changeset	55
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	end (* structure *)
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	57
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	open Nominal_Library;

author	Christian Urban <urbanc@in.tum.de>
	Tue, 27 Apr 2010 22:45:50 +0200
changeset 1963	0c9ef14e9ba4
parent 1962	84a13d1e2511
child 1979	760257a66604
permissions	-rw-r--r--