nominal2: Nominal/Ex/Classical.thy@de5c9a0040ec (annotated)

1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Classical
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	2	imports "../Nominal2"
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	5	(* example from Urban's PhD *)
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	atom_decl name
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	atom_decl coname
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	nominal_datatype trm =
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	11	Ax "name" "coname"
2891 304dfe6cc83a the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl Christian Urban <urbanc@in.tum.de> parents: 2889 diff changeset	12	\| Cut c::"coname" t1::"trm" n::"name" t2::"trm" bind n in t1, bind c in t2
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	13	("Cut <_>._ '(_')._" [100,100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	14	\| NotR n::"name" t::"trm" "coname" bind n in t
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	15	("NotR '(_')._ _" [100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	16	\| NotL c::"coname" t::"trm" "name" bind c in t
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	17	("NotL <_>._ _" [100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	18	\| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	19	("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	20	\| AndL1 n::"name" t::"trm" "name" bind n in t
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	21	("AndL1 '(_')._ _" [100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	22	\| AndL2 n::"name" t::"trm" "name" bind n in t
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	23	("AndL2 '(_')._ _" [100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	24	\| OrR1 c::"coname" t::"trm" "coname" bind c in t
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	25	("OrR1 <_>._ _" [100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	26	\| OrR2 c::"coname" t::"trm" "coname" bind c in t
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	27	("OrR2 <_>._ _" [100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	28	\| OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name" bind n1 in t1, bind n2 in t2
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	29	("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	30	\| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	31	("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100)
2902 9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2901 diff changeset	32	\| ImpR n::"name" c::"coname" t::"trm" "coname" bind n c in t
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	33	("ImpR '(_').<_>._ _" [100,100,100,100] 100)
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	34
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	35	thm trm.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	36	thm trm.induct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	37	thm trm.exhaust
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	38	thm trm.strong_exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	39	thm trm.strong_exhaust[simplified]
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	40	thm trm.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	41	thm trm.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	42	thm trm.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	43	thm trm.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	44	thm trm.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	45	thm trm.size_eqvt
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	46	thm trm.supp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	47	thm trm.supp[simplified]
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	48
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	49	lemma Abs_lst1_fcb2:
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	50	fixes a b :: "'a :: at"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	51	and S T :: "'b :: fs"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	52	and c::"'c::fs"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	53	assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"
2902 9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2901 diff changeset	54	and fcb1: "atom a \<sharp> f a T c"
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	55	and fresh: "{atom a, atom b} \<sharp>* c"
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	56	and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c"
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	57	and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c"
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	58	shows "f a T c = f b S c"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	59	proof -
2903 e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	60	have fcb2: "atom b \<sharp> f b S c"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	61	using e[symmetric]
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	62	apply(simp add: Abs_eq_iff2)
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	63	apply(erule exE)
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	64	apply(simp add: alphas)
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	65	apply(rule_tac p="p" in permute_boolE)
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	66	apply(simp add: fresh_eqvt)
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	67	apply(subst perm2)
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	68	using fresh
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	69	apply(auto simp add: fresh_star_def)[1]
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	70	apply(simp add: atom_eqvt)
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	71	apply(rule fcb1)
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	72	done
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	73	have fin1: "finite (supp (f a T c))"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	74	apply(rule_tac S="supp (a, T, c)" in supports_finite)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	75	apply(simp add: supports_def)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	76	apply(simp add: fresh_def[symmetric])
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	77	apply(clarify)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	78	apply(subst perm1)
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	79	apply(simp add: supp_swap fresh_star_def)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	80	apply(simp add: swap_fresh_fresh fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	81	apply(simp add: finite_supp)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	82	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	83	have fin2: "finite (supp (f b S c))"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	84	apply(rule_tac S="supp (b, S, c)" in supports_finite)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	85	apply(simp add: supports_def)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	86	apply(simp add: fresh_def[symmetric])
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	87	apply(clarify)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	88	apply(subst perm2)
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	89	apply(simp add: supp_swap fresh_star_def)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	90	apply(simp add: swap_fresh_fresh fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	91	apply(simp add: finite_supp)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	92	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	93	obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	94	using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"]
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	95	apply(auto simp add: finite_supp supp_Pair fin1 fin2)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	96	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	97	have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	98	apply(simp (no_asm_use) only: flip_def)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	99	apply(subst swap_fresh_fresh)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	100	apply(simp add: Abs_fresh_iff)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	101	using fr
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	102	apply(simp add: Abs_fresh_iff)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	103	apply(subst swap_fresh_fresh)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	104	apply(simp add: Abs_fresh_iff)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	105	using fr
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	106	apply(simp add: Abs_fresh_iff)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	107	apply(rule e)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	108	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	109	then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	110	apply (simp add: swap_atom flip_def)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	111	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	112	then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	113	by (simp add: Abs1_eq_iff)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	114	have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	115	unfolding flip_def
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	116	apply(rule sym)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	117	apply(rule swap_fresh_fresh)
2902 9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2901 diff changeset	118	using fcb1
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	119	apply(simp)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	120	using fr
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	121	apply(simp add: fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	122	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	123	also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	124	unfolding flip_def
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	125	apply(subst perm1)
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	126	using fresh fr
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	127	apply(simp add: supp_swap fresh_star_def fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	128	apply(simp)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	129	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	130	also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	131	also have "... = (b \<leftrightarrow> d) \<bullet> f b S c"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	132	unfolding flip_def
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	133	apply(subst perm2)
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	134	using fresh fr
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	135	apply(simp add: supp_swap fresh_star_def fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	136	apply(simp)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	137	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	138	also have "... = f b S c"
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	139	apply(rule flip_fresh_fresh)
2902 9c3f6a4d95d4 another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy Christian Urban <urbanc@in.tum.de> parents: 2901 diff changeset	140	using fcb2
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	141	apply(simp)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	142	using fr
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	143	apply(simp add: fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	144	done
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	145	finally show ?thesis by simp
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	146	qed
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	147
2903 e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	148	lemma Abs_lst_fcb2:
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	149	fixes as bs :: "atom list"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	150	and x y :: "'b :: fs"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	151	and c::"'c::fs"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	152	assumes e: "(Abs_lst as x) = (Abs_lst bs y)"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	153	and fcb1: "(set as) \<sharp>* f as x c"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	154	and fcb2: "(set bs) \<sharp>* f bs y c"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	155	and fresh1: "set as \<sharp>* c"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	156	and fresh2: "set bs \<sharp>* c"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	157	and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	158	and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
e26c6c728b9e only one of the fcb precondistions are needed (probably the same with the perm-conditions) Christian Urban <urbanc@in.tum.de> parents: 2902 diff changeset	159	shows "f as x c = f bs y c"
2909 de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	160	proof -
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	161	have fin1: "finite (supp (f as x c))"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	162	apply(rule_tac S="supp (as, x, c)" in supports_finite)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	163	apply(simp add: supports_def)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	164	apply(simp add: fresh_def[symmetric])
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	165	apply(clarify)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	166	apply(subst perm1)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	167	apply(simp add: supp_swap fresh_star_def)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	168	apply(simp add: swap_fresh_fresh fresh_Pair)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	169	apply(simp add: finite_supp)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	170	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	171	have fin2: "finite (supp (f bs y c))"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	172	apply(rule_tac S="supp (bs, y, c)" in supports_finite)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	173	apply(simp add: supports_def)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	174	apply(simp add: fresh_def[symmetric])
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	175	apply(clarify)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	176	apply(subst perm2)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	177	apply(simp add: supp_swap fresh_star_def)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	178	apply(simp add: swap_fresh_fresh fresh_Pair)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	179	apply(simp add: finite_supp)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	180	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	181	obtain q::"perm" where
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	182	fr1: "(q \<bullet> (set as)) \<sharp>* (as, bs, x, y, c, f as x c, f bs y c)" and
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	183	fr2: "supp q \<sharp>* Abs_lst as x" and
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	184	inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	185	using at_set_avoiding3[where xs="set as" and c="(as, bs, x, y, c, f as x c, f bs y c)"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	186	and x="Abs_lst as x"]
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	187	apply(simp add: supp_Pair finite_supp fin1 fin2 Abs_fresh_star)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	188	apply(erule exE)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	189	apply(erule conjE)+
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	190	apply(drule fresh_star_supp_conv)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	191	apply(blast)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	192	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	193	have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	194	also have "\<dots> = Abs_lst as x"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	195	apply(rule perm_supp_eq)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	196	apply(simp add: fr2)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	197	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	198	finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using e by simp
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	199	then obtain r::perm where
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	200	qq1: "q \<bullet> x = r \<bullet> y" and
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	201	qq2: "q \<bullet> as = r \<bullet> bs" and
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	202	qq3: "supp r \<subseteq> (set (q \<bullet> as) \<union> set bs)"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	203	apply -
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	204	apply(drule_tac sym)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	205	apply(simp only: Abs_eq_iff2 alphas)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	206	apply(erule exE)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	207	apply(erule conjE)+
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	208	apply(drule_tac x="p" in meta_spec)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	209	apply(simp)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	210	apply(blast)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	211	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	212	have "f as x c = q \<bullet> (f as x c)"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	213	apply(rule sym)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	214	apply(rule perm_supp_eq)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	215	using inc fcb1 fr1
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	216	apply(simp add: set_eqvt)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	217	apply(simp add: fresh_star_Pair)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	218	apply(auto simp add: fresh_star_def)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	219	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	220	also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	221	apply(subst perm1)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	222	using inc fresh1 fr1
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	223	apply(simp add: set_eqvt)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	224	apply(simp add: fresh_star_Pair)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	225	apply(auto simp add: fresh_star_def)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	226	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	227	also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	228	also have "\<dots> = r \<bullet> (f bs y c)"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	229	apply(rule sym)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	230	apply(subst perm2)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	231	using qq3 fresh2 fr1
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	232	apply(simp add: set_eqvt)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	233	apply(simp add: fresh_star_Pair)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	234	apply(auto simp add: fresh_star_def)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	235	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	236	also have "... = f bs y c"
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	237	apply(rule perm_supp_eq)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	238	using qq3 fr1 fcb2
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	239	apply(simp add: set_eqvt)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	240	apply(simp add: fresh_star_Pair)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	241	apply(auto simp add: fresh_star_def)
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	242	done
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	243	finally show ?thesis by simp
de5c9a0040ec fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. Christian Urban <urbanc@in.tum.de> parents: 2904 diff changeset	244	qed
2892 a9f3600c9ae6 Speed-up the completeness proof. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2891 diff changeset	245
2904 eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	246	lemma supp_zero_perm_zero:
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	247	shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0"
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	248	by (metis supp_perm_singleton supp_zero_perm)
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	249
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	250	lemma permute_atom_list_id:
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	251	shows "p \<bullet> l = l \<longleftrightarrow> supp p \<inter> set l = {}"
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	252	by (induct l) (auto simp add: supp_Nil supp_perm)
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	253
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	254	lemma Abs_lst_binder_length:
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	255	shows "[xs]lst. T = [ys]lst. S \<Longrightarrow> length xs = length ys"
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	256	by (auto simp add: Abs_eq_iff alphas length_eqvt[symmetric] permute_pure)
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	257
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	258	lemma Abs_lst_binder_eq:
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	259	shows "Abs_lst l T = Abs_lst l S \<longleftrightarrow> T = S"
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	260	by (rule, simp_all add: Abs_eq_iff2 alphas)
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	261	(metis fresh_star_zero inf_absorb1 permute_atom_list_id supp_perm_eq
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	262	supp_zero_perm_zero)
eb322a392461 equality of lst_binder and a few helper lemmas Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2903 diff changeset	263
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	264	nominal_primrec
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	265	crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	266	where
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	267	"(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	268	\| "atom a \<sharp> (d, e) \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	269	\| "(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	270	\| "atom a \<sharp> (d, e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	271	\| "\<lbrakk>atom a \<sharp> (d, e); atom b \<sharp> (d, e)\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[d\<turnstile>c>e] =
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	272	(if c=d then AndR <a>.(M[d\<turnstile>c>e]) <b>.(N[d \<turnstile>c>e]) e else AndR <a>.(M[d\<turnstile>c>e]) <b>.(N[d\<turnstile>c>e]) c)"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	273	\| "(AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	274	\| "(AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	275	\| "atom a \<sharp> (d, e) \<Longrightarrow> (OrR1 <a>.M b)[d\<turnstile>c>e] =
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	276	(if b=d then OrR1 <a>.(M[d\<turnstile>c>e]) e else OrR1 <a>.(M[d\<turnstile>c>e]) b)"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	277	\| "atom a \<sharp> (d, e) \<Longrightarrow> (OrR2 <a>.M b)[d\<turnstile>c>e] =
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	278	(if b=d then OrR2 <a>.(M[d\<turnstile>c>e]) e else OrR2 <a>.(M[d\<turnstile>c>e]) b)"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	279	\| "(OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	280	\| "atom a \<sharp> (d, e) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] =
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	281	(if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	282	\| "atom a \<sharp> (d, e) \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	283	apply(simp only: eqvt_def)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	284	apply(simp only: crename_graph_def)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	285	apply (rule, perm_simp, rule)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	286	apply(rule TrueI)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	287	-- "covered all cases"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	288	apply(case_tac x)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	289	apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust)
2892 a9f3600c9ae6 Speed-up the completeness proof. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2891 diff changeset	290	apply (simp_all add: fresh_star_def)[12]
a9f3600c9ae6 Speed-up the completeness proof. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2891 diff changeset	291	apply(metis)+
2891 304dfe6cc83a the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl Christian Urban <urbanc@in.tum.de> parents: 2889 diff changeset	292	-- "compatibility"
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	293	apply(simp_all)
2891 304dfe6cc83a the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl Christian Urban <urbanc@in.tum.de> parents: 2889 diff changeset	294	apply(rule conjI)
2892 a9f3600c9ae6 Speed-up the completeness proof. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2891 diff changeset	295	apply(elim conjE)
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	296	apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
2891 304dfe6cc83a the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl Christian Urban <urbanc@in.tum.de> parents: 2889 diff changeset	297	apply(simp add: Abs_fresh_iff)
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	298	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	299	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	300	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	301	apply(elim conjE)
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	302	apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	303	apply(simp add: Abs_fresh_iff)
2900 d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	304	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	305	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	306	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	307	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	308	apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	309	apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	310	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	311	apply(simp add: Abs_fresh_iff)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	312	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	313	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	314	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	315	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	316	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	317	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	318	apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	319	apply(simp add: Abs_fresh_iff)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	320	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	321	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	322	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	323	apply(rule conjI)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	324	apply(elim conjE)
fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	325	apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	326	apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	327	apply(erule Abs_lst1_fcb2)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	328	apply(simp add: Abs_fresh_iff)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	329	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	330	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	331	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	332	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	333	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	334	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	335	apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	336	apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	337	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	338	apply(simp add: Abs_fresh_iff)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	339	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	340	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	341	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	342	apply(blast)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	343	apply(blast)
fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	344	apply(elim conjE)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	345	apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	346	apply(simp add: Abs_fresh_iff)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	347	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	348	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	349	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	350	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	351	apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	352	apply(simp add: Abs_fresh_iff)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	353	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	354	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	355	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	356	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	357	apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	358	apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	359	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	360	apply(simp add: Abs_fresh_iff)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	361	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	362	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	363	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	364	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	365	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	366	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	367	apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	368	apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	369	apply(erule Abs_lst1_fcb2)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	370	apply(simp add: Abs_fresh_iff)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	371	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	372	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	373	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	374	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	375	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	376	apply(rule conjI)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	377	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	378	apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	379	apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	380	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	381	apply(simp add: Abs_fresh_iff)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	382	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	383	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	384	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	385	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	386	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	387	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	388	apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	389	apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	390	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	391	apply(simp add: Abs_fresh_iff)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	392	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	393	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	394	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	395	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	396	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	397	defer
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	398	apply(erule conjE)+
fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	399	apply(rule conjI)
fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	400	apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	401	apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	402	apply(erule Abs_lst1_fcb2)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	403	apply(simp add: Abs_fresh_iff)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	404	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	405	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	406	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	407	apply(blast)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	408	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	409	apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	410	apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	411	apply(erule Abs_lst1_fcb2)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	412	apply(simp add: Abs_fresh_iff)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	413	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	414	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	415	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	416	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	417	apply(blast)
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	418	oops
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	419
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	420	end
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	421
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	422
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	423

author	Christian Urban <urbanc@in.tum.de>
	Mon, 27 Jun 2011 19:15:18 +0100
changeset 2909	de5c9a0040ec
parent 2904	eb322a392461
child 2910	ae6455351572
permissions	-rw-r--r--