nominal2: Nominal/Ex/Ex1rec.thy@92dc6cfa3a95 (annotated)

1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Ex1rec
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	2	imports "../NewParser"
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	declare [[STEPS = 9]]
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
2311 4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	7	atom_decl name
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	8
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	9	nominal_datatype lam =
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	10	Var "name"
a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	11	\| App "lam" "lam"
a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	12	\| Lam x::"name" t::"lam" bind_set x in t
a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	13	\| Let bp::"bp" t::"lam" bind_set "bi bp" in bp t
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	14	and bp =
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	15	Bp "name" "lam"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	binder
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	17	bi::"bp \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	where
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	19	"bi (Bp x t) = {atom x}"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20
2311 4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	21
4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	22	thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros
4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	23
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	24	thm lam_bp.fv
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	25	thm lam_bp.eq_iff[no_vars]
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	26	thm lam_bp.bn
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	27	thm lam_bp.perm
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	28	thm lam_bp.induct
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	29	thm lam_bp.inducts
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	30	thm lam_bp.distinct
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	31	thm lam_bp.supp
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	32	ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	33	thm lam_bp.fv[simplified lam_bp.supp(1-2)]
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2067 diff changeset	35
2067 ace7775cbd04 Experiments with equivariance. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2056 diff changeset	36
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40

author	Christian Urban <urbanc@in.tum.de>
	Wed, 25 Aug 2010 22:55:42 +0800
changeset 2434	92dc6cfa3a95
parent 2311	4da5c5c29009
permissions	-rw-r--r--