nominal2: Nominal/Ex/Ex1.thy@90779aefbf1a (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
2561 7926f1cb45eb respectfulness for permute_bn functions Christian Urban <urbanc@in.tum.de> parents: 2475 diff changeset	9	declare [[STEPS = 100]]
7926f1cb45eb respectfulness for permute_bn functions Christian Urban <urbanc@in.tum.de> parents: 2475 diff changeset	10
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	nominal_datatype foo =
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	Foo0 "name"
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2147 diff changeset	13	\| 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	14	and bar =
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	Bar0 "name"
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2147 diff changeset	16	\| 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	17	binder
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	bv
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	where
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	"bv (Bar0 x) = {}"
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	\| "bv (Bar1 v x b) = {atom v}"
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22
2593 25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2561 diff changeset	23	thm foo_bar.perm_bn_alpha
25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2561 diff changeset	24	thm foo_bar.perm_bn_simps
25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2561 diff changeset	25	thm foo_bar.bn_finite
25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2561 diff changeset	26
25dcb2b1329e ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof Christian Urban <urbanc@in.tum.de> parents: 2561 diff changeset	27	thm foo_bar.eq_iff
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	28	thm foo_bar.distinct
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	29	thm foo_bar.induct
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	30	thm foo_bar.inducts
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	31	thm foo_bar.exhaust
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	32	thm foo_bar.fv_defs
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	33	thm foo_bar.bn_defs
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	34	thm foo_bar.perm_simps
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	35	thm foo_bar.eq_iff
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	36	thm foo_bar.fv_bn_eqvt
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	37	thm foo_bar.size_eqvt
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	38	thm foo_bar.supports
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	39	thm foo_bar.fsupp
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	40	thm foo_bar.supp
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	41
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	42	lemma
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	43	"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	44	apply(simp only: foo_bar.fv_defs)
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	45	apply(simp only: foo_bar.bn_defs)
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	46	apply(simp only: supp_at_base)
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	47	apply(simp)
9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	48	done
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2045 diff changeset	49
2045 6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	50	end
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	51
6800fcaafa2a Separate Term8, as it may work soon. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	52

author	Christian Urban <urbanc@in.tum.de>
	Wed, 08 Dec 2010 17:07:08 +0000 (2010-12-08)
changeset 2603	90779aefbf1a
parent 2593	25dcb2b1329e
child 2611	3d101f2f817c
permissions	-rw-r--r--