nominal2: Nominal/Ex/ExPS3.thy@37480540c1af (annotated)

1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory ExPS3
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	2	imports "../Parser"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	(* example 3 from Peter Sewell's bestiary *)
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	atom_decl name
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	ML {* val _ = recursive := false *}
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	nominal_datatype exp =
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	VarP "name"
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	\| AppP "exp" "exp"
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	\| LamP x::"name" e::"exp" bind x in e
1656 c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	14	\| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	and pat3 =
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	PVar "name"
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	\| PUnit
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	\| PPair "pat3" "pat3"
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	binder
1656 c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	20	bp :: "pat3 \<Rightarrow> atom set"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	where
1656 c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	22	"bp (PVar x) = {atom x}"
c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	23	\| "bp (PUnit) = {}"
c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	24	\| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	thm exp_pat3.fv
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	thm exp_pat3.eq_iff
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	thm exp_pat3.bn
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	thm exp_pat3.perm
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	thm exp_pat3.induct
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	thm exp_pat3.distinct
1604 5ab97f43ec24 More modification needed for compilation Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	32	thm exp_pat3.fv
1656 c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	33	thm exp_pat3.supp
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	end
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38

author	Christian Urban <urbanc@in.tum.de>
	Tue, 13 Apr 2010 07:40:54 +0200
changeset 1818	37480540c1af
parent 1773	c0eac04ae3b4
child 2053	58e13de342a5
permissions	-rw-r--r--