nominal2: Nominal/Ex/ExPS3.thy@1a9dbfe04f7d (annotated)

1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory ExPS3
2053 58e13de342a5 ExPS3 in NewParser Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	2	imports "../NewParser"
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
2053 58e13de342a5 ExPS3 in NewParser Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	9	ML {* val _ = cheat_equivp := true *}
58e13de342a5 ExPS3 in NewParser Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	10	ML {* val _ = cheat_alpha_bn_rsp := true *}
58e13de342a5 ExPS3 in NewParser Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	11
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	nominal_datatype exp =
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	13	Var "name"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	14	\| App "exp" "exp"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	15	\| Lam x::"name" e::"exp" bind_set x in e
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	16	\| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	17	and pat =
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	PVar "name"
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	\| PUnit
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	20	\| PPair "pat" "pat"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	binder
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	22	bp :: "pat \<Rightarrow> atom set"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	where
1656 c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	24	"bp (PVar x) = {atom x}"
c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	25	\| "bp (PUnit) = {}"
c9d3dda79fe3 Removed remaining cheats + some cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1604 diff changeset	26	\| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	28	thm exp_pat.fv
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	29	thm exp_pat.eq_iff
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	30	thm exp_pat.bn
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	31	thm exp_pat.perm
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	32	thm exp_pat.induct
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	33	thm exp_pat.distinct
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	34	thm exp_pat.fv
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	35	thm exp_pat.supp(1-2)
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	36
2120 2786ff1df475 fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy Christian Urban <urbanc@in.tum.de> parents: 2114 diff changeset	37
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2053 diff changeset	38
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40	end
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43

author	Christian Urban <urbanc@in.tum.de>
	Mon, 07 Jun 2010 16:17:35 +0200
changeset 2216	1a9dbfe04f7d
parent 2120	2786ff1df475
child 2436	3885dc2669f9
permissions	-rw-r--r--