nominal2: Nominal/Ex/ExPS6.thy@fab7f09dda22 (annotated)

1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory ExPS6
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@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 6 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
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	9	(* Is this binding structure supported - I think not
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	10	because e1 occurs twice as body *)
1604 5ab97f43ec24 More modification needed for compilation Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	11
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	12	nominal_datatype exp =
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	13	Var name
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	14	\| Pair exp exp
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	15	\| LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	16	and pat =
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	17	PVar name
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	18	\| PUnit
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	19	\| PPair pat pat
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	binder
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	21	bp :: "pat \<Rightarrow> atom list"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	where
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	23	"bp (PVar x) = [atom x]"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	24	\| "bp (PUnit) = []"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	25	\| "bp (PPair p1 p2) = bp p1 @ bp p2"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	27	thm exp_pat.fv
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	28	thm exp_pat.eq_iff
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	29	thm exp_pat.bn
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	30	thm exp_pat.perm
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	31	thm exp_pat.induct
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	32	thm exp_pat.distinct
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	33	thm exp_pat.supp
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	34
2120 2786ff1df475 fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy Christian Urban <urbanc@in.tum.de> parents: 2105 diff changeset	35
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	36
1600 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	end
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
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Thu, 17 Jun 2010 09:25:44 +0200
changeset 2282	fab7f09dda22
parent 2120	2786ff1df475
permissions	-rw-r--r--