nominal2: Nominal/Ex/LetRec.thy@c24f86c595ca (annotated)

2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	1	theory LetRec
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2438 diff changeset	2	imports "../Nominal2"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
2311 4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	5	atom_decl name
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	6
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	7	nominal_datatype let_rec:
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	8	trm =
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	9	Var "name"
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	10	\| App "trm" "trm"
abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	11	\| Lam x::"name" t::"trm" bind (set) x in t
abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	12	\| Let_Rec bp::"bp" t::"trm" bind (set) "bn bp" in bp t
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	13	and bp =
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	14	Bp "name" "trm"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	binder
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	16	bn::"bp \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	where
2438 abafea9b39bb corrected bug with fv-function generation (that was the problem with recursive binders) Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	18	"bn (Bp x t) = {atom x}"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	20	thm let_rec.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	21	thm let_rec.induct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	22	thm let_rec.exhaust
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	23	thm let_rec.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	24	thm let_rec.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	25	thm let_rec.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	26	thm let_rec.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	27	thm let_rec.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	28	thm let_rec.size_eqvt
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2067 diff changeset	29
2067 ace7775cbd04 Experiments with equivariance. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2056 diff changeset	30
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 21 Jun 2011 10:37:43 +0900 (2011-06-21)
changeset 2880	c24f86c595ca
parent 2454	9ffee4eb1ae1
child 2877	3e82c1ced5e4
permissions	-rw-r--r--