nominal2: Nominal/Ex/Shallow.thy@374e2f90140c (annotated)

2570 1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Shallow
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../Nominal2"
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	(*
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	Various shallow binders
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	*)
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	atom_decl name
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	10
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	text {* binding lists of names *}
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	nominal_datatype trm1 =
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	Var1 "name"
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	\| App1 "trm1" "trm1"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	16	\| Lam1 xs::"name list" t::"trm1" binds xs in t
2570 1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
2622 e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2570 diff changeset	18	thm trm1.strong_exhaust
e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2570 diff changeset	19
2570 1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	text {* binding a finite set of names *}
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	nominal_datatype trm2 =
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	Var2 "name"
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	\| App2 "trm2" "trm2"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	26	\| Lam2 xs::"name fset" t::"trm2" binds (set) xs in t
2570 1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	27
2622 e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2570 diff changeset	28	thm trm2.strong_exhaust
2570 1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	text {* restricting a finite set of names *}
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	31
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	nominal_datatype trm3 =
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	Var3 "name"
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	\| App3 "trm3" "trm3"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	35	\| Lam3 xs::"name fset" t::"trm3" binds (set+) xs in t
2570 1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	36
2634 3ce1089cdbf3 changed res keyword to set+ for restrictions; comment by a referee Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	37	thm trm3.eq_iff
2570 1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	end
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	40
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	41
1c77e15c4259 added a test for the various shallow binders Christian Urban <urbanc@in.tum.de> parents: diff changeset	42

author	Christian Urban <urbanc@in.tum.de>
	Sun, 17 Jul 2011 11:33:09 +0100 (2011-07-17)
changeset 2970	374e2f90140c
parent 2950	0911cb7bf696
permissions	-rw-r--r--