nominal2: Nominal/Ex/LF.thy@6ba52f3a1542 (annotated)

2083 9568f9f31822 tuned file names for examples Christian Urban <urbanc@in.tum.de> parents: 2082 diff changeset	1	theory LF
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2440 diff changeset	2	imports "../Nominal2"
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6	atom_decl ident
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	8	nominal_datatype lf:
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	9	kind =
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	10	Type
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	11	\| KPi "ty" n::"name" k::"kind" bind n in k
1348 2e2a3cd58f64 Ported LF to the parser interface. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1344 diff changeset	12	and ty =
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	13	TConst "ident"
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	14	\| TApp "ty" "trm"
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	15	\| TPi "ty" n::"name" ty::"ty" bind n in ty
1348 2e2a3cd58f64 Ported LF to the parser interface. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1344 diff changeset	16	and trm =
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	17	Const "ident"
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	18	\| Var "name"
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	19	\| App "trm" "trm"
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	20	\| Lam "ty" n::"name" t::"trm" bind n in t
994 333c24bd595d More in the LF example in the new nominal way, all is clear until support. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 993 diff changeset	21
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	22	thm lf.distinct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	23	thm lf.induct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	24	thm lf.inducts
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	25	thm lf.exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	26	thm lf.strong_exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	27	thm lf.fv_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	28	thm lf.bn_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	29	thm lf.perm_simps
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	30	thm lf.eq_iff
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	31	thm lf.fv_bn_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	32	thm lf.size_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	33	thm lf.supports
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	34	thm lf.fsupp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	35	thm lf.supp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	36	thm lf.fresh
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	37	thm lf.fresh[simplified]
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	38
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2059 diff changeset	39
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2059 diff changeset	40
985 ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	end
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44
ef8a2b0b237a Ported existing part of LF to new permutations and alphas. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45

author	Christian Urban <urbanc@in.tum.de>
	Sat, 09 Apr 2011 13:44:49 +0800 (2011-04-09)
changeset 2758	6ba52f3a1542
parent 2617	e44551d067e6
child 2779	3c769bf10e63
permissions	-rw-r--r--