nominal2: Nominal/Ex/Ex1rec.thy@f89773ab0685 (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
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	7	ML {* val _ = cheat_supp_eq := true *}
2094 56b849d348ae Recursive examples with relation composition Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2082 diff changeset	8	ML {* val _ = cheat_equivp := true *}
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	9
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	10	nominal_datatype lam =
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	11	Var "name"
a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	12	\| App "lam" "lam"
a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	13	\| Lam x::"name" t::"lam" bind_set x in t
a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	14	\| 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	15	and bp =
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	16	Bp "name" "lam"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	binder
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	18	bi::"bp \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	where
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	20	"bi (Bp x t) = {atom x}"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	22	thm lam_bp.fv
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	23	thm lam_bp.eq_iff[no_vars]
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	24	thm lam_bp.bn
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	25	thm lam_bp.perm
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	26	thm lam_bp.induct
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	27	thm lam_bp.inducts
3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	28	thm lam_bp.distinct
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	29	thm lam_bp.supp
1946 3395e87d94b8 tuned and made to compile Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	30	ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
2056 a58c73e39479 Ex1Rec. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1946 diff changeset	31	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	32
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2067 diff changeset	33
2067 ace7775cbd04 Experiments with equivariance. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2056 diff changeset	34
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Mon, 17 May 2010 16:29:33 +0200
changeset 2145	f89773ab0685
parent 2120	2786ff1df475
child 2311	4da5c5c29009
permissions	-rw-r--r--