nominal2: Nominal-General/nominal_library.ML@24ae81462f3e (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
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	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	10	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	11
1899 8e0bfb14f6bf optimised the code of define_raw_perm Christian Urban <urbanc@in.tum.de> parents: 1896 diff changeset	12	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	13	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	14	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	15	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	16
9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	17	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	18	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	19	end
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	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	23	struct
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	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	26	@{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	27
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	28	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	29	@{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	30
1899 8e0bfb14f6bf optimised the code of define_raw_perm Christian Urban <urbanc@in.tum.de> parents: 1896 diff changeset	31	fun perm_ty ty = @{typ perm} --> ty --> ty
8e0bfb14f6bf optimised the code of define_raw_perm Christian Urban <urbanc@in.tum.de> parents: 1896 diff changeset	32
1871 c704d129862b moved some general function into nominal_library.ML Christian Urban <urbanc@in.tum.de> parents: 1834 diff changeset	33	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	34	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	35
c704d129862b moved some general function into nominal_library.ML Christian Urban <urbanc@in.tum.de> parents: 1834 diff changeset	36	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	37
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	38	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	39	\| 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	40
1834 9909cc3566c5 moved a couple of more functions to the library Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	41	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	42	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	43
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	end (* structure *)
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	45
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	open Nominal_Library;

author	Christian Urban <urbanc@in.tum.de>
	Wed, 21 Apr 2010 21:31:07 +0200
changeset 1931	24ae81462f3e
parent 1899	8e0bfb14f6bf
child 1962	84a13d1e2511
permissions	-rw-r--r--