nominal2: Nominal/ExLet.thy@a7e60da429e2 (annotated)

1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory ExLet
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	imports "Parser"
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	text {* example 3 or example 5 from Terms.thy *}
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	atom_decl name
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	ML {* val _ = recursive := false *}
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	nominal_datatype trm =
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	Vr "name"
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	\| Ap "trm" "trm"
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	\| Lm x::"name" t::"trm" bind x in t
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	14	\| Lt a::"lts" t::"trm" bind "bn a" in t
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	and lts =
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	16	Lnil
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	17	\| Lcons "name" "trm" "lts"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	binder
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	bn
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	where
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	21	"bn Lnil = {}"
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	22	\| "bn (Lcons x t l) = {atom x} \<union> (bn l)"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	thm trm_lts.fv
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	thm trm_lts.eq_iff
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	thm trm_lts.bn
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	thm trm_lts.perm
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	thm trm_lts.induct
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	thm trm_lts.distinct
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	thm trm_lts.fv[simplified trm_lts.supp]
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	32	lemma lets_bla:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	33	"x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	34	by (simp add: trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	35
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	36	lemma lets_ok:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	37	"(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	38	apply (simp add: trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	39	apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	40	apply (simp_all add: alphas)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	41	apply (simp add: fresh_star_def eqvts)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	42	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	43
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	44	lemma lets_ok3:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	45	"x \<noteq> y \<Longrightarrow>
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	46	(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	47	(Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	48	apply (simp add: alphas trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	49	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	50
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	51
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	52	lemma lets_not_ok1:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	53	"(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	54	(Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	55	apply (simp add: alphas trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	56	apply (rule_tac x="0::perm" in exI)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	57	apply (simp add: fresh_star_def eqvts)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	58	apply blast
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	59	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	60
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	61	lemma lets_nok:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	62	"x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	63	(Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	64	(Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	65	apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	66	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	67
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	68
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	69	end
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	70
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	71
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	72

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 23 Mar 2010 09:13:17 +0100
changeset 1602	a7e60da429e2
parent 1600	e33e37fd4c7d
child 1638	36798cdbc452
permissions	-rw-r--r--