nominal2: Nominal/Ex/Let.thy@51f75d24bd73 (annotated)

2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	1	theory Let
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2449 diff changeset	2	imports "../Nominal2"
1600 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	atom_decl name
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	nominal_datatype trm =
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	8	Var "name"
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	9	\| App "trm" "trm"
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	10	\| Lam x::"name" t::"trm" bind x in t
2490 320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	11	\| Let as::"assn" t::"trm" bind "bn as" in t
320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	12	and assn =
320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	13	ANil
320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	14	\| ACons "name" "trm" "assn"
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	binder
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	bn
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	where
2490 320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	18	"bn ANil = []"
320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	19	\| "bn (ACons x t as) = (atom x) # (bn as)"
320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	20
320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	21	thm trm_assn.fv_defs
2492 5ac9a74d22fd post-processed eq_iff and supp threormes according to the fv-supp equality Christian Urban <urbanc@in.tum.de> parents: 2490 diff changeset	22	thm trm_assn.eq_iff
2490 320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	23	thm trm_assn.bn_defs
320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	24	thm trm_assn.perm_simps
2492 5ac9a74d22fd post-processed eq_iff and supp threormes according to the fv-supp equality Christian Urban <urbanc@in.tum.de> parents: 2490 diff changeset	25	thm trm_assn.induct
5ac9a74d22fd post-processed eq_iff and supp threormes according to the fv-supp equality Christian Urban <urbanc@in.tum.de> parents: 2490 diff changeset	26	thm trm_assn.inducts
2490 320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	27	thm trm_assn.distinct
320775fa47ca some experiments Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	28	thm trm_assn.supp
2493 2e174807c891 added postprocessed fresh-lemmas for constructors Christian Urban <urbanc@in.tum.de> parents: 2492 diff changeset	29	thm trm_assn.fresh
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2562 diff changeset	30	thm trm_assn.exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2562 diff changeset	31	thm trm_assn.strong_exhaust
2494 11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: 2493 diff changeset	32
2498 c7534584a7a0 use also induct_schema for the Let-example (permute_bn is used) Christian Urban <urbanc@in.tum.de> parents: 2494 diff changeset	33	(*
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	34	lemma lets_bla:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	35	"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	36	by (simp add: trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	37
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	38	lemma lets_ok:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	39	"(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	40	apply (simp add: trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	41	apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
2039 39df91a90f87 Move ExLet to NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1774 diff changeset	42	apply (simp_all add: alphas eqvts supp_at_base fresh_star_def)
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	43	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	44
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	45	lemma lets_ok3:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	46	"x \<noteq> y \<Longrightarrow>
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	47	(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	48	(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	49	apply (simp add: alphas trm_lts.eq_iff)
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	50	done
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
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	53	lemma lets_not_ok1:
1685 721d92623c9d Lets finally abstract lists. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1658 diff changeset	54	"x \<noteq> y \<Longrightarrow>
721d92623c9d Lets finally abstract lists. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1658 diff changeset	55	(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	56	(Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
1685 721d92623c9d Lets finally abstract lists. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1658 diff changeset	57	apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	58	done
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	59
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	60	lemma lets_nok:
a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	61	"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	62	(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	63	(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	64	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	65	done
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	66	*)
1602 a7e60da429e2 Move Let properties to ExLet Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1600 diff changeset	67
1600 e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	68	end
e33e37fd4c7d More reorganization. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	69
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

author	Christian Urban <urbanc@in.tum.de>
	Thu, 06 Jan 2011 14:53:38 +0000 (2011-01-06)
changeset 2646	51f75d24bd73
parent 2630	8268b277d240
child 2670	3c493c951388
permissions	-rw-r--r--