nominal2: Nominal/Ex/TypeVarsTest.thy@324b148fc6b5 (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"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2888 diff changeset	23	\| Lam x::"name" l::"('a, 'b, 'c) lam" binds x in l
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2571 diff changeset	24	\| Foo "'a" "'b"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2888 diff changeset	25	\| Bar x::"'c" l::"('a, 'b, 'c) lam" binds 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
2888 eda5aeb056a6 fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package Christian Urban <urbanc@in.tum.de> parents: 2730 diff changeset	42	nominal_datatype ('alpha, 'beta, 'gamma) psi =
2730 eebc24b9cf39 added a lemma about fresh_star and Abs Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	43	PsiNil
2888 eda5aeb056a6 fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package Christian Urban <urbanc@in.tum.de> parents: 2730 diff changeset	44	\| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi"
2730 eebc24b9cf39 added a lemma about fresh_star and Abs Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	45
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	46
3029 6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	47	nominal_datatype 'a foo =
6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	48	Node x::"name" f::"'a foo" binds x in f
6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	49	\| Leaf "'a"
6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	50
6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	51	term "Leaf"
6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	52
6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	53
6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	54
6fd3fc3254ee deleted PNil Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	55
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	end
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	57
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	58
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: diff changeset	59

author	Christian Urban <urbanc@in.tum.de>
	Sat, 26 Nov 2011 09:48:14 +0000
changeset 3053	324b148fc6b5
parent 3029	6fd3fc3254ee
child 3065	51ef8a3cb6ef
child 3071	11f6a561eb4b
permissions	-rw-r--r--