nominal2: Nominal/Ex/TypeVarsTest.thy@34df2cffe259 (annotated)

2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory TypeVarsTest
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2440 diff changeset	2	imports "../Nominal2"
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	5	(* a nominal datatype with type variables and sorts *)
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	6
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	7
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	8	(* the sort constraints need to be attached to the *)
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	9	(* first occurence of the type variables on the *)
2622 e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	10	(* right-hand side *)
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	11
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	atom_decl name
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	13
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	class s1
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	class s2
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	16
2571 f0252365936c proved that bn functions return a finite set Christian Urban <urbanc@in.tum.de> parents: 2557 diff changeset	17	instance nat :: s1 ..
f0252365936c proved that bn functions return a finite set Christian Urban <urbanc@in.tum.de> parents: 2557 diff changeset	18	instance int :: s2 ..
f0252365936c proved that bn functions return a finite set Christian Urban <urbanc@in.tum.de> parents: 2557 diff changeset	19
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	20	nominal_datatype ('a, 'b, 'c) lam =
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	Var "name"
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	22	\| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam"
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	23	\| Lam x::"name" l::"('a, 'b, 'c) lam" bind x in l
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	24	\| Foo "'a" "'b"
2622 e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	25	\| Bar x::"'c" l::"('a, 'b, 'c) lam" bind x in l (* Bar binds a polymorphic atom *)
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	26
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	27	term Foo
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	28	term Bar
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	thm lam.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	thm lam.induct
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	32	thm lam.exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	33	thm lam.strong_exhaust
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	thm lam.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	thm lam.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	thm lam.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	thm lam.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	thm lam.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	thm lam.size_eqvt
2557 781fbc8c0591 fixed locally the problem with the function package; all tests work again Christian Urban <urbanc@in.tum.de> parents: 2556 diff changeset	40
2730 eebc24b9cf39 added a lemma about fresh_star and Abs Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	41	(* FIXME: only works for type variables 'a 'b 'c *)
eebc24b9cf39 added a lemma about fresh_star and Abs Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	42
eebc24b9cf39 added a lemma about fresh_star and Abs Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	43	nominal_datatype ('a, 'b, 'c) psi =
eebc24b9cf39 added a lemma about fresh_star and Abs Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	44	PsiNil
eebc24b9cf39 added a lemma about fresh_star and Abs Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	45	\| Output "'a" "'a" "('a, 'b, 'c) psi"
eebc24b9cf39 added a lemma about fresh_star and Abs Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	46
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	47
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	end
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	49
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	50
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	51

author	Christian Urban <urbanc@in.tum.de>
	Wed, 16 Mar 2011 20:42:14 +0100 (2011-03-16)
changeset 2745	34df2cffe259
parent 2730	eebc24b9cf39
child 2888	eda5aeb056a6
permissions	-rw-r--r--