nominal2: Nominal/Ex/Lambda.thy@fd5eec72c3f5 (annotated)

1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	1	theory Lambda
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	2	imports "../NewParser" Quotient_Option
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	7	nominal_datatype lam =
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	8	Var "name"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	9	\| App "lam" "lam"
2041 3842464ee03b Move 2 more to NewParser Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1954 diff changeset	10	\| Lam x::"name" l::"lam" bind_set x in l
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11
1845 b7423c6b5564 deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell Christian Urban <urbanc@in.tum.de> parents: 1835 diff changeset	12	thm lam.fv
b7423c6b5564 deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell Christian Urban <urbanc@in.tum.de> parents: 1835 diff changeset	13	thm lam.supp
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	14	lemmas supp_fn' = lam.fv[simplified lam.supp]
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	15
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	16	declare lam.perm[eqvt]
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	17
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2041 diff changeset	18
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	19	section {* Strong Induction Principles*}
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20
2041 3842464ee03b Move 2 more to NewParser Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1954 diff changeset	21	(*
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	22	Old way of establishing strong induction
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	23	principles by chosing a fresh name.
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	24	*)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	lemma
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	fixes c::"'a::fs"
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	27	assumes a1: "\<And>name c. P c (Var name)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	28	and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	29	and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	30	shows "P c lam"
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	proof -
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	32	have "\<And>p. P c (p \<bullet> lam)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	33	apply(induct lam arbitrary: c rule: lam.induct)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	34	apply(perm_simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	apply(rule a1)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	36	apply(perm_simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	apply(rule a2)
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	38	apply(assumption)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	apply(assumption)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	40	apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))")
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	defer
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	apply(simp add: fresh_def)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	43	apply(rule_tac X="supp (c, Lam (p \<bullet> name) (p \<bullet> lam))" in obtain_at_base)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44	apply(simp add: supp_Pair finite_supp)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45	apply(blast)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	46	apply(erule exE)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	47	apply(rule_tac t="p \<bullet> Lam name lam" and
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	48	s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lam name lam" in subst)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	49	apply(simp del: lam.perm)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	50	apply(subst lam.perm)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	51	apply(subst (2) lam.perm)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	52	apply(rule flip_fresh_fresh)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	53	apply(simp add: fresh_def)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	54	apply(simp only: supp_fn')
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	55	apply(simp)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	56	apply(simp add: fresh_Pair)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	57	apply(simp)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	58	apply(rule a3)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	59	apply(simp add: fresh_Pair)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61	apply(simp)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	62	done
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	63	then have "P c (0 \<bullet> lam)" by blast
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	64	then show "P c lam" by simp
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	qed
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	66
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	67	(*
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	68	New way of establishing strong induction
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	69	principles by using a appropriate permutation.
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	70	*)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	71	lemma
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	72	fixes c::"'a::fs"
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	73	assumes a1: "\<And>name c. P c (Var name)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	74	and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	75	and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	76	shows "P c lam"
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	77	proof -
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	78	have "\<And>p. P c (p \<bullet> lam)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	79	apply(induct lam arbitrary: c rule: lam.induct)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	80	apply(perm_simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	81	apply(rule a1)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	82	apply(perm_simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	83	apply(rule a2)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	84	apply(assumption)
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	85	apply(assumption)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	86	apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q")
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	87	apply(erule exE)
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	88	apply(rule_tac t="p \<bullet> Lam name lam" and
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	89	s="q \<bullet> p \<bullet> Lam name lam" in subst)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	90	defer
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	91	apply(simp)
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	92	apply(rule a3)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	93	apply(simp add: eqvts fresh_star_def)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	94	apply(drule_tac x="q + p" in meta_spec)
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	95	apply(simp)
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	96	apply(rule at_set_avoiding2)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	97	apply(simp add: finite_supp)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	98	apply(simp add: finite_supp)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	99	apply(simp add: finite_supp)
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	100	apply(perm_simp)
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	101	apply(simp add: fresh_star_def fresh_def supp_fn')
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	102	apply(rule supp_perm_eq)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	103	apply(simp)
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	104	done
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	105	then have "P c (0 \<bullet> lam)" by blast
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	106	then show "P c lam" by simp
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	107	qed
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	108
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	109	section {* Typing *}
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	110
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	111	nominal_datatype ty =
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	112	TVar string
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	113	\| TFun ty ty
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	114
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	115	notation
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	116	TFun ("_ \<rightarrow> _")
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	117
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	118	declare ty.perm[eqvt]
1805 f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	119
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	120	inductive
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	121	valid :: "(name \<times> ty) list \<Rightarrow> bool"
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	122	where
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	123	"valid []"
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	124	\| "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"
f187f20f0a79 a few tests Christian Urban <urbanc@in.tum.de> parents: 1800 diff changeset	125
1828 f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	126	inductive
f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	127	typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	128	where
f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	129	t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	130	\| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
1828 f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	131	\| t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
f374ffd50c7c preliminary tests Christian Urban <urbanc@in.tum.de> parents: 1818 diff changeset	132
1831 16653e702d89 first working version of the automatic equivariance procedure Christian Urban <urbanc@in.tum.de> parents: 1828 diff changeset	133	equivariance valid
16653e702d89 first working version of the automatic equivariance procedure Christian Urban <urbanc@in.tum.de> parents: 1828 diff changeset	134	equivariance typing
1816 56cebe7f8e24 some small tunings (incompleted work in Lambda.thy) Christian Urban <urbanc@in.tum.de> parents: 1814 diff changeset	135
1831 16653e702d89 first working version of the automatic equivariance procedure Christian Urban <urbanc@in.tum.de> parents: 1828 diff changeset	136	thm valid.eqvt
16653e702d89 first working version of the automatic equivariance procedure Christian Urban <urbanc@in.tum.de> parents: 1828 diff changeset	137	thm typing.eqvt
1811 ae176476b525 implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1810 diff changeset	138	thm eqvts
ae176476b525 implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1810 diff changeset	139	thm eqvts_raw
ae176476b525 implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1810 diff changeset	140
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	141	thm typing.induct[of "\<Gamma>" "t" "T", no_vars]
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	142
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	143	lemma
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	144	fixes c::"'a::fs"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	145	assumes a: "\<Gamma> \<turnstile> t : T"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	146	and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	147	and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk>
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	148	\<Longrightarrow> P c \<Gamma> (App t1 t2) T2"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	149	and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>atom x \<sharp> c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk>
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	150	\<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	151	shows "P c \<Gamma> t T"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	152	proof -
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	153	from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	154	proof (induct)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	155	case (t_Var \<Gamma> x T p c)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	156	then show ?case
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	157	apply -
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	158	apply(perm_strict_simp)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	159	apply(rule a1)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	160	apply(drule_tac p="p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	161	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	162	apply(assumption)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	163	apply(rotate_tac 1)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	164	apply(drule_tac p="p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	165	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	166	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	167	done
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	168	next
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	169	case (t_App \<Gamma> t1 T1 T2 t2 p c)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	170	then show ?case
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	171	apply -
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	172	apply(perm_strict_simp)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	173	apply(rule a2)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	174	apply(drule_tac p="p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	175	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	176	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	177	apply(assumption)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	178	apply(rotate_tac 2)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	179	apply(drule_tac p="p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	180	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	181	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	182	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	183	done
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	184	next
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	185	case (t_Lam x \<Gamma> T1 t T2 p c)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	186	then show ?case
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	187	apply -
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	188	apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and>
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	189	supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	190	apply(erule exE)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	191	apply(rule_tac t="p \<bullet> \<Gamma>" and s="(q + p) \<bullet> \<Gamma>" in subst)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	192	apply(simp only: permute_plus)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	193	apply(rule supp_perm_eq)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	194	apply(simp add: supp_Pair fresh_star_union)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	195	apply(rule_tac t="p \<bullet> Lam x t" and s="(q + p) \<bullet> Lam x t" in subst)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	196	apply(simp only: permute_plus)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	197	apply(rule supp_perm_eq)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	198	apply(simp add: supp_Pair fresh_star_union)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	199	apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	200	apply(simp only: permute_plus)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	201	apply(rule supp_perm_eq)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	202	apply(simp add: supp_Pair fresh_star_union)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	203	apply(simp (no_asm) only: eqvts)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	204	apply(rule a3)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	205	apply(simp only: eqvts permute_plus)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	206	apply(simp add: fresh_star_def)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	207	apply(drule_tac p="q + p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	208	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	209	apply(assumption)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	210	apply(rotate_tac 1)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	211	apply(drule_tac p="q + p" in permute_boolI)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	212	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	213	apply(assumption)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	214	apply(drule_tac x="d" in meta_spec)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	215	apply(drule_tac x="q + p" in meta_spec)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	216	apply(perm_strict_simp add: permute_minus_cancel)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	217	apply(assumption)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	218	apply(rule at_set_avoiding2)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	219	apply(simp add: finite_supp)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	220	apply(simp add: finite_supp)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	221	apply(simp add: finite_supp)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	222	apply(rule_tac p="-p" in permute_boolE)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	223	apply(perm_strict_simp add: permute_minus_cancel)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	224	(* supplied by the user *)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	225	apply(simp add: fresh_star_prod)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	226	apply(simp add: fresh_star_def)
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	227	sorry
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	228	qed
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	229	then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" .
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	230	then show "P c \<Gamma> t T" by simp
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	231	qed
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	232
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	233
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	234
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	235
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	236
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	237
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	238
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	239	inductive
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	240	tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	241	for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	242	where
1835 636de31888a6 tuned and removed dead code Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	243	aa: "tt r a a"
636de31888a6 tuned and removed dead code Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	244	\| bb: "tt r a b ==> tt r a c"
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	245
1835 636de31888a6 tuned and removed dead code Christian Urban <urbanc@in.tum.de> parents: 1833 diff changeset	246	(* PROBLEM: derived eqvt-theorem does not conform with [eqvt]
1833 2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	247	equivariance tt
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	248	*)
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file Christian Urban <urbanc@in.tum.de> parents: 1831 diff changeset	249
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	250
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	251	inductive
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	252	alpha_lam_raw'
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	253	where
1861 226b797868dc some tuning of eqvt-infrastructure Christian Urban <urbanc@in.tum.de> parents: 1845 diff changeset	254	a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
226b797868dc some tuning of eqvt-infrastructure Christian Urban <urbanc@in.tum.de> parents: 1845 diff changeset	255	\| a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	256	alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
1865 b71b838b0a75 Finished proof in Lambda.thy Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1863 diff changeset	257	\| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
1810 894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	258	alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
894930834ca8 fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ Christian Urban <urbanc@in.tum.de> parents: 1805 diff changeset	259
1866 6d4e4bf9bce6 automatic proofs for equivariance of alphas Christian Urban <urbanc@in.tum.de> parents: 1865 diff changeset	260	equivariance alpha_lam_raw'
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	261
1861 226b797868dc some tuning of eqvt-infrastructure Christian Urban <urbanc@in.tum.de> parents: 1845 diff changeset	262	thm eqvts_raw
226b797868dc some tuning of eqvt-infrastructure Christian Urban <urbanc@in.tum.de> parents: 1845 diff changeset	263
1800 78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	264	section {* size function *}
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	265
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	266	lemma size_eqvt_raw:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	267	fixes t::"lam_raw"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	268	shows "size (pi \<bullet> t) = size t"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	269	apply (induct rule: lam_raw.inducts)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	270	apply simp_all
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	271	done
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	272
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	273	instantiation lam :: size
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	274	begin
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	275
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	276	quotient_definition
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	277	"size_lam :: lam \<Rightarrow> nat"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	278	is
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	279	"size :: lam_raw \<Rightarrow> nat"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	280
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	281	lemma size_rsp:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	282	"alpha_lam_raw x y \<Longrightarrow> size x = size y"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	283	apply (induct rule: alpha_lam_raw.inducts)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	284	apply (simp_all only: lam_raw.size)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	285	apply (simp_all only: alphas)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	286	apply clarify
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	287	apply (simp_all only: size_eqvt_raw)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	288	done
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	289
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	290	lemma [quot_respect]:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	291	"(alpha_lam_raw ===> op =) size size"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	292	by (simp_all add: size_rsp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	293
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	294	lemma [quot_preserve]:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	295	"(rep_lam ---> id) size = size"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	296	by (simp_all add: size_lam_def)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	297
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	298	instance
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	299	by default
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	300
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	301	end
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	302
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	303	lemmas size_lam[simp] =
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	304	lam_raw.size(4)[quot_lifted]
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	305	lam_raw.size(5)[quot_lifted]
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	306	lam_raw.size(6)[quot_lifted]
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	307
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	308	(* is this needed? *)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	309	lemma [measure_function]:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	310	"is_measure (size::lam\<Rightarrow>nat)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	311	by (rule is_measure_trivial)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	312
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	313	section {* Matching *}
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	314
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	315	definition
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	316	MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	317	where
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	318	"MATCH M d x \<equiv> if (\<exists>!r. \<exists>q. M q = (True, x, r)) then (THE r. \<exists>q. M q = (True, x, r)) else d"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	319
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	320	(*
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	321	lemma MATCH_eqvt:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	322	shows "p \<bullet> (MATCH M d x) = MATCH (p \<bullet> M) (p \<bullet> d) (p \<bullet> x)"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	323	unfolding MATCH_def
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	324	apply(perm_simp the_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	325	apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	326	apply(simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	327	thm eqvts_raw
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	328	apply(subst if_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	329	apply(subst ex1_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	330	apply(subst permute_fun_def)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	331	apply(subst ex_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	332	apply(subst permute_fun_def)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	333	apply(subst eq_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	334	apply(subst permute_fun_app_eq[where f="M"])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	335	apply(simp only: permute_minus_cancel)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	336	apply(subst permute_prod.simps)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	337	apply(subst permute_prod.simps)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	338	apply(simp only: permute_minus_cancel)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	339	apply(simp only: permute_bool_def)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	340	apply(simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	341	apply(subst ex1_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	342	apply(subst permute_fun_def)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	343	apply(subst ex_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	344	apply(subst permute_fun_def)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	345	apply(subst eq_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	346
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	347	apply(simp only: eqvts)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	348	apply(simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	349	apply(subgoal_tac "(p \<bullet> (\<exists>!r. \<exists>q. M q = (True, x, r))) = (\<exists>!r. \<exists>q. (p \<bullet> M) q = (True, p \<bullet> x, r))")
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	350	apply(drule sym)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	351	apply(simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	352	apply(rule impI)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	353	apply(simp add: perm_bool)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	354	apply(rule trans)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	355	apply(rule pt_the_eqvt[OF pta at])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	356	apply(assumption)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	357	apply(simp add: pt_ex_eqvt[OF pt at])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	358	apply(simp add: pt_eq_eqvt[OF ptb at])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	359	apply(rule cheat)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	360	apply(rule trans)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	361	apply(rule pt_ex1_eqvt)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	362	apply(rule pta)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	363	apply(rule at)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	364	apply(simp add: pt_ex_eqvt[OF pt at])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	365	apply(simp add: pt_eq_eqvt[OF ptb at])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	366	apply(subst pt_pi_rev[OF pta at])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	367	apply(subst pt_fun_app_eq[OF pt at])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	368	apply(subst pt_pi_rev[OF pt at])
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	369	apply(simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	370	done
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	371
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	372	lemma MATCH_cng:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	373	assumes a: "M1 = M2" "d1 = d2"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	374	shows "MATCH M1 d1 x = MATCH M2 d2 x"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	375	using a by simp
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	376
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	377	lemma MATCH_eq:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	378	assumes a: "t = l x" "G x" "\<And>x'. t = l x' \<Longrightarrow> G x' \<Longrightarrow> r x' = r x"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	379	shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = r x"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	380	using a
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	381	unfolding MATCH_def
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	382	apply(subst if_P)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	383	apply(rule_tac a="r x" in ex1I)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	384	apply(rule_tac x="x" in exI)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	385	apply(blast)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	386	apply(erule exE)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	387	apply(drule_tac x="q" in meta_spec)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	388	apply(auto)[1]
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	389	apply(rule the_equality)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	390	apply(blast)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	391	apply(erule exE)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	392	apply(drule_tac x="q" in meta_spec)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	393	apply(auto)[1]
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	394	done
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	395
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	396	lemma MATCH_eq2:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	397	assumes a: "t = l x1 x2" "G x1 x2" "\<And>x1' x2'. t = l x1' x2' \<Longrightarrow> G x1' x2' \<Longrightarrow> r x1' x2' = r x1 x2"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	398	shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = r x1 x2"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	399	sorry
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	400
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	401	lemma MATCH_neq:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	402	assumes a: "\<And>x. t = l x \<Longrightarrow> G x \<Longrightarrow> False"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	403	shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = d"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	404	using a
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	405	unfolding MATCH_def
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	406	apply(subst if_not_P)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	407	apply(blast)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	408	apply(rule refl)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	409	done
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	410
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	411	lemma MATCH_neq2:
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	412	assumes a: "\<And>x1 x2. t = l x1 x2 \<Longrightarrow> G x1 x2 \<Longrightarrow> False"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	413	shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = d"
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	414	using a
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	415	unfolding MATCH_def
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	416	apply(subst if_not_P)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	417	apply(auto)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	418	done
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	419	*)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	420
1954 23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	421	ML {*
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	422	fun mk_avoids ctxt params name set =
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	423	let
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	424	val (_, ctxt') = ProofContext.add_fixes
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	425	(map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	426	fun mk s =
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	427	let
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	428	val t = Syntax.read_term ctxt' s;
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	429	val t' = list_abs_free (params, t) \|>
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	430	funpow (length params) (fn Abs (_, _, t) => t)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	431	in (t', HOLogic.dest_setT (fastype_of t)) end
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	432	handle TERM _ =>
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	433	error ("Expression " ^ quote s ^ " to be avoided in case " ^
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	434	quote name ^ " is not a set type");
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	435	fun add_set p [] = [p]
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	436	\| add_set (t, T) ((u, U) :: ps) =
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	437	if T = U then
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	438	let val S = HOLogic.mk_setT T
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	439	in (Const (@{const_name sup}, S --> S --> S) $ u $ t, T) :: ps
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	440	end
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	441	else (u, U) :: add_set (t, T) ps
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	442	in
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	443	(mk #> add_set) set
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	444	end;
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	445	*}
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	446
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	447
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	448	ML {*
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	449	writeln (commas (map (Syntax.string_of_term @{context} o fst)
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	450	(mk_avoids @{context} [] "t_Var" "{x}" [])))
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	451	*}
23480003f9c5 some changes to the paper Christian Urban <urbanc@in.tum.de> parents: 1950 diff changeset	452
1947 51f411b1197d tuned and cleaned Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	453
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	454	ML {*
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	455
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	456	fun prove_strong_ind (pred_name, avoids) ctxt =
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	457	Proof.theorem NONE (K I) [] ctxt
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	458
2169 61a89e41c55b Renamings. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2162 diff changeset	459	local structure P = Parse and K = Keyword in
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	460
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	461	val _ =
2169 61a89e41c55b Renamings. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2162 diff changeset	462	Outer_Syntax.local_theory_to_proof "nominal_inductive"
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	463	"proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	464	(P.xname -- (Scan.optional (P.$$$ "avoids" \|-- P.enum1 "\|" (P.name --
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	465	(P.$$$ ":" \|-- P.and_list1 P.term))) []) >> prove_strong_ind)
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	466
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	467	end;
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	468
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	469	*}
0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	470
1950 7de54c9f81ac eliminated command so that all compiles Christian Urban <urbanc@in.tum.de> parents: 1949 diff changeset	471	(*
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	472	nominal_inductive typing
1950 7de54c9f81ac eliminated command so that all compiles Christian Urban <urbanc@in.tum.de> parents: 1949 diff changeset	473	*)
1949 0b692f37a771 changed theorem_i to theorem....requires new Isabelle Christian Urban <urbanc@in.tum.de> parents: 1947 diff changeset	474
2157 a1d27083e688 subst experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	475	(* Substitution *)
2159 ce00205e07ab Single variable substitution Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2158 diff changeset	476
2161 64f353098721 More subst experminets Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2160 diff changeset	477	definition new where
2162 d76667e51d30 more subst experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2161 diff changeset	478	"new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)"
2161 64f353098721 More subst experminets Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2160 diff changeset	479
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	480	primrec match_Var_raw where
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	481	"match_Var_raw (Var_raw x) = Some x"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	482	\| "match_Var_raw (App_raw x y) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	483	\| "match_Var_raw (Lam_raw n t) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	484
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	485	quotient_definition
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	486	"match_Var :: lam \<Rightarrow> name option"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	487	is match_Var_raw
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	488
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	489	lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	490	apply rule
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	491	apply (induct_tac a b rule: alpha_lam_raw.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	492	apply simp_all
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	493	done
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	494
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	495	lemmas match_Var_simps = match_Var_raw.simps[quot_lifted]
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	496
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	497	primrec match_App_raw where
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	498	"match_App_raw (Var_raw x) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	499	\| "match_App_raw (App_raw x y) = Some (x, y)"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	500	\| "match_App_raw (Lam_raw n t) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	501
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	502	quotient_definition
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	503	"match_App :: lam \<Rightarrow> (lam \<times> lam) option"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	504	is match_App_raw
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	505
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	506	lemma [quot_respect]:
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	507	"(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	508	apply (intro fun_relI)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	509	apply (induct_tac a b rule: alpha_lam_raw.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	510	apply simp_all
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	511	done
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	512
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	513	lemmas match_App_simps = match_App_raw.simps[quot_lifted]
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	514
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	515	primrec match_Lam_raw where
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	516	"match_Lam_raw (S :: atom set) (Var_raw x) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	517	\| "match_Lam_raw S (App_raw x y) = None"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	518	\| "match_Lam_raw S (Lam_raw n t) = (let z = new (S \<union> (fv_lam_raw t - {atom n})) in Some (z, (n \<leftrightarrow> z) \<bullet> t))"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	519
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	520	quotient_definition
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	521	"match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	522	is match_Lam_raw
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	523
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	524	lemma swap_fresh:
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	525	assumes a: "fv_lam_raw t \<sharp>* p"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	526	shows "alpha_lam_raw (p \<bullet> t) t"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	527	using a apply (induct t)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	528	apply (simp add: supp_at_base fresh_star_def)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	529	apply (rule alpha_lam_raw.intros)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	530	apply (metis Rep_name_inverse atom_eqvt atom_name_def fresh_perm)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	531	apply (simp)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	532	apply (simp only: fresh_star_union)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	533	apply clarify
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	534	apply (rule alpha_lam_raw.intros)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	535	apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	536	apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	537	apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	538	apply (rule alpha_lam_raw.intros)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	539	sorry
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	540
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	541	lemma [quot_respect]:
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	542	"(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	543	proof (intro fun_relI, clarify)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	544	fix S t s
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	545	assume a: "alpha_lam_raw t s"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	546	show "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S t) (match_Lam_raw S s)"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	547	using a proof (induct t s rule: alpha_lam_raw.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	548	case goal1 show ?case by simp
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	549	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	550	case goal2 show ?case by simp
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	551	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	552	case (goal3 x t y s)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	553	then obtain p where "({atom x}, t) \<approx>gen (\<lambda>x1 x2. alpha_lam_raw x1 x2 \<and>
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	554	option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S x1)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	555	(match_Lam_raw S x2)) fv_lam_raw p ({atom y}, s)" ..
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	556	then have
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	557	c: "fv_lam_raw t - {atom x} = fv_lam_raw s - {atom y}" and
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	558	d: "(fv_lam_raw t - {atom x}) \<sharp>* p" and
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	559	e: "alpha_lam_raw (p \<bullet> t) s" and
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	560	f: "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S (p \<bullet> t)) (match_Lam_raw S s)" and
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	561	g: "p \<bullet> {atom x} = {atom y}" unfolding alphas(1) by - (elim conjE, assumption)+
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	562	let ?z = "new (S \<union> (fv_lam_raw t - {atom x}))"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	563	have h: "?z = new (S \<union> (fv_lam_raw s - {atom y}))" using c by simp
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	564	show ?case
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	565	unfolding match_Lam_raw.simps Let_def option_rel.simps prod_rel.simps split_conv
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	566	proof
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	567	show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	568	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	569	have "atom y \<sharp> p" sorry
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	570	have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	571	then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" using swap_fresh by auto
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	572	then have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	573	have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	574	then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	575	then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	576	((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h .
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	577	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	578	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	579	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	580
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	581	lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted]
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	582
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	583	lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	584	by (induct x rule: lam.induct) (simp_all add: match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	585
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	586	lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	587	apply (induct x rule: lam.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	588	apply (simp_all add: match_Lam_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	589	apply (simp add: Let_def)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	590	apply (erule conjE)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	591	apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S")
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	592	apply (rule conjI)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	593	apply (simp add: lam.eq_iff)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	594	apply (rule_tac x="(name \<leftrightarrow> z)" in exI)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	595	apply (simp add: alphas)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	596	apply (simp add: eqvts)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	597	apply (simp only: lam.fv(3)[symmetric])
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	598	apply (subgoal_tac "Lam name lam = Lam z s")
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	599	apply (simp del: lam.fv)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	600	prefer 3
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	601	apply (thin_tac "(name \<leftrightarrow> new (S \<union> (fv_lam lam - {atom name}))) \<bullet> lam = s")
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	602	apply (simp only: new_def)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	603	apply (subgoal_tac "\<forall>a \<in> S. atom z \<noteq> a")
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	604	apply (simp only: fresh_def)
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	605	(thm supp_finite_atom_fset)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	606	sorry
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	607
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	608	function subst where
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	609	"subst v s t = (
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	610	case match_Var t of Some n \<Rightarrow> if n = v then s else Var n \| None \<Rightarrow>
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	611	case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) \| None \<Rightarrow>
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	612	case match_Lam (supp (v,s)) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) \| None \<Rightarrow> undefined)"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	613	by pat_completeness auto
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	614
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	615	termination apply (relation "measure (\<lambda>(_, _, t). size t)")
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	616	apply auto[1]
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	617	apply (case_tac a) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	618	apply (frule lam_some) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	619	apply (case_tac a) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	620	apply (frule app_some) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	621	apply (case_tac a) apply simp
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	622	apply (frule app_some) apply simp
2165 e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	623	done
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	624
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	625	lemmas lam_exhaust = lam_raw.exhaust[quot_lifted]
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	626
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	627	lemma subst_eqvt:
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	628	"p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	629	proof (induct v s t rule: subst.induct)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	630	case (1 v s t)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	631	show ?case proof (cases t rule: lam_exhaust)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	632	fix n
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	633	assume "t = Var n"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	634	then show ?thesis by (simp add: match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	635	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	636	fix l r
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	637	assume "t = App l r"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	638	then show ?thesis
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	639	apply (simp only:)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	640	apply (subst subst.simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	641	apply (subst match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	642	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	643	apply (subst match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	644	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	645	apply (simp only: prod.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	646	apply (simp only: lam.perm)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	647	apply (subst (3) subst.simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	648	apply (subst match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	649	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	650	apply (subst match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	651	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	652	apply (simp only: prod.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	653	apply (subst 1(2)[of "(l, r)" "l" "r"])
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	654	apply (simp add: match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	655	apply (simp add: match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	656	apply (rule refl)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	657	apply (subst 1(3)[of "(l, r)" "l" "r"])
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	658	apply (simp add: match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	659	apply (simp add: match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	660	apply (rule refl)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	661	apply (rule refl)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	662	done
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	663	next
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	664	fix n t'
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	665	assume "t = Lam n t'"
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	666	then show ?thesis
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	667	apply (simp only: )
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	668	apply (simp only: lam.perm)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	669	apply (subst subst.simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	670	apply (subst match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	671	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	672	apply (subst match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	673	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	674	apply (subst match_Lam_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	675	apply (simp only: Let_def)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	676	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	677	apply (simp only: prod.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	678	apply (subst (2) subst.simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	679	apply (subst match_Var_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	680	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	681	apply (subst match_App_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	682	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	683	apply (subst match_Lam_simps)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	684	apply (simp only: Let_def)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	685	apply (simp only: option.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	686	apply (simp only: prod.cases)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	687	apply (simp only: lam.perm)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	688	apply (simp only: lam.eq_iff)
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	689	sorry
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	690	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	691	qed
e838f7d90f81 Function experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	692
2161 64f353098721 More subst experminets Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2160 diff changeset	693
2172 fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	694	lemma subst_proper_eqs:
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	695	"subst y s (Var x) = (if x = y then s else (Var x))"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	696	"subst y s (App l r) = App (subst y s l) (subst y s r)"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	697	"atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)"
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	698	apply (subst subst.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	699	apply (simp only: match_Var_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	700	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	701	apply (subst subst.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	702	apply (simp only: match_App_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	703	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	704	apply (simp only: prod.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	705	apply (simp only: match_Var_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	706	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	707	apply (subst subst.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	708	apply (simp only: match_Lam_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	709	apply (simp only: match_Var_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	710	apply (simp only: match_App_simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	711	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	712	apply (simp only: Let_def)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	713	apply (simp only: option.simps)
fd5eec72c3f5 More on Function-defined subst. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2170 diff changeset	714	apply (simp only: prod.simps)
2157 a1d27083e688 subst experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	715	sorry
a1d27083e688 subst experiments Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2120 diff changeset	716
1594 892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	717	end
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	718
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	719
892fcdb96c96 Move LamEx out of Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	720

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Fri, 21 May 2010 11:55:22 +0200 (2010-05-21)
changeset 2172	fd5eec72c3f5
parent 2170	1fe84fd8f8a4
child 2173	477293d841e8
permissions	-rw-r--r--