nominal2: Nominal/Ex/ExPS7.thy@dcffc2f132c9 (annotated)

2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	1
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	theory ExPS7
2043 5098771ff041 ExPS7 in NewParser Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	3	imports "../NewParser"
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4	begin
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6	(* example 7 from Peter Sewell's bestiary *)
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8	atom_decl name
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	10	nominal_datatype exp =
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	11	Var name
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	12	\| Unit
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	13	\| Pair exp exp
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	14	\| LetRec l::"lrbs" e::"exp" bind_set "bs l" in l e
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	and lrb =
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	16	Assign name exp
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	and lrbs =
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	Single lrb
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	\| More lrb lrbs
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. 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: 2043 diff changeset	21	b :: "lrb \<Rightarrow> atom set" and
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	22	bs :: "lrbs \<Rightarrow> atom set"
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	where
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	24	"b (Assign x e) = {atom x}"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	25	\| "bs (Single a) = b a"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	26	\| "bs (More a as) = (b a) \<union> (bs as)"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	27
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	28	thm exp_lrb_lrbs.eq_iff
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	29	thm exp_lrb_lrbs.supp
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	30
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32	end
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 15 Jun 2010 09:12:54 +0200 (2010-06-15)
changeset 2266	dcffc2f132c9
parent 2120	2786ff1df475
child 2436	3885dc2669f9
permissions	-rw-r--r--