nominal2: Nominal/ExLet.thy@36798cdbc452 (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
1638 36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	28	thm trm_lts.induct[no_vars]
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	29	thm trm_lts.inducts[no_vars]
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	thm trm_lts.distinct
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	thm trm_lts.fv[simplified trm_lts.supp]
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32
1638 36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	33	lemma
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	34	fixes t::trm
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	35	and l::lts
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	36	and c::"'a::fs"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	37	assumes a1: "\<And>name c. P1 c (Vr name)"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	38	and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	39	and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	40	and a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	41	and a5: "\<And>c. P2 c Lnil"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	42	and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	43	shows "P1 c t" and "P2 c l"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	44	proof -
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	45	have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	46	"(\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> l))"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	47	apply(induct rule: trm_lts.inducts)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	48	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	49	apply(rule a1)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	50	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	51	apply(rule a2)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	52	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	53	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	54	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	55	apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	56	apply(erule exE)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	57	apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	58	and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	59	apply(rule supp_perm_eq)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	60	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	61	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	62	apply(rule a3)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	63	apply(simp add: atom_eqvt)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	64	apply(subst permute_plus[symmetric])
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	65	apply(blast)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	66	apply(rule at_set_avoiding2_atom)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	67	apply(simp add: finite_supp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	68	apply(simp add: finite_supp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	69	apply(simp add: fresh_def)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	70	apply(simp add: trm_lts.fv[simplified trm_lts.supp])
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	71	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	72	apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Lt (p \<bullet> lts) (p \<bullet> trm)) \<sharp>* q")
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	73	apply(erule exE)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	74	apply(rule_tac t="Lt (p \<bullet> lts) (p \<bullet> trm)"
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	75	and s="q \<bullet> Lt (p \<bullet> lts) (p \<bullet> trm)" in subst)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	76	apply(rule supp_perm_eq)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	77	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	78	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	79	apply(rule a4)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	80	apply(simp add: eqvts)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	81	apply(subst permute_plus[symmetric])
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	82	apply(blast)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	83	apply(subst permute_plus[symmetric])
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	84	apply(blast)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	85	apply(rule at_set_avoiding2)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	86	apply(simp add: finite_supp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	87	defer
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	88	apply(simp add: finite_supp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	89	apply(simp add: finite_supp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	90	apply(simp add: fresh_star_def)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	91	apply(simp add: fresh_def)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	92	apply(simp add: trm_lts.fv[simplified trm_lts.supp])
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	93	defer
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	94	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	95	apply(rule a5)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	96	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	97	apply(rule a6)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	98	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	99	apply(simp)
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	100	oops
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	101
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	102
36798cdbc452 first attempt of strong induction for lets with assignments Christian Urban <urbanc@in.tum.de> parents: 1602 diff changeset	103
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	104	lemma lets_bla:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	105	"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	106	by (simp add: trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	107
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	108	lemma lets_ok:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	109	"(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	110	apply (simp add: trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	111	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	112	apply (simp_all add: alphas)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	113	apply (simp add: fresh_star_def eqvts)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	114	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	115
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	116	lemma lets_ok3:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	117	"x \<noteq> y \<Longrightarrow>
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	118	(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	119	(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	120	apply (simp add: alphas trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	121	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	122
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	123
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	124	lemma lets_not_ok1:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	125	"(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	126	(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	127	apply (simp add: alphas trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	128	apply (rule_tac x="0::perm" in exI)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	129	apply (simp add: fresh_star_def eqvts)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	130	apply blast
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	131	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	132
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	133	lemma lets_nok:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	134	"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	135	(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	136	(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	137	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	138	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	139
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	140
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	141	end
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	142
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	143
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	144

author	Christian Urban <urbanc@in.tum.de>
	Thu, 25 Mar 2010 08:05:03 +0100
changeset 1638	36798cdbc452
parent 1602	a7e60da429e2
child 1639	a98d03fb9d53
permissions	-rw-r--r--