nominal2: Nominal/Ex/Ex1.thy@67b3933c3190 (annotated)

2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	1	theory Ex1
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	2	imports "../Nominal2"
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	5	(* free names in bar are bound in foo *)
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	atom_decl name
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	nominal_datatype foo =
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	Foo0 "name"
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2147 diff changeset	11	\| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	and bar =
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	Bar0 "name"
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2147 diff changeset	14	\| Bar1 "name" s::"name" b::"bar" bind (set) s in b
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	binder
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	bv
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	where
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	"bv (Bar0 x) = {}"
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	\| "bv (Bar1 v x b) = {atom v}"
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	21
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	22	thm foo_bar.fv_defs[no_vars] foo_bar.bn_defs[no_vars]
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	23
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	24	lemma
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	25	"fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	26	apply(simp only: foo_bar.fv_defs)
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	27	apply(simp only: foo_bar.bn_defs)
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	28	apply(simp only: supp_at_base)
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	29	apply(simp)
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	30	done
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2045 diff changeset	31
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32	end
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34

author	Christian Urban <urbanc@in.tum.de>
	Sat, 04 Sep 2010 06:10:04 +0800 (2010-09-03)
changeset 2467	67b3933c3190
parent 2454	9ffee4eb1ae1
child 2475	486d4647bb37
permissions	-rw-r--r--