nominal2: Nominal/Ex/Classical.thy@e2da10806a34 (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
2926 37c0d7953cba moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through Christian Urban <urbanc@in.tum.de> parents: 2914 diff changeset	5
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	6	(* 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	7
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 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	9	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	10
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	11	nominal_datatype trm =
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	12	Ax "name" "coname"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	13	\| Cut c::"coname" t1::"trm" n::"name" t2::"trm" binds n in t1, binds c in t2
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	14	("Cut <_>._ '(_')._" [100,100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	15	\| NotR n::"name" t::"trm" "coname" binds n in t
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	16	("NotR '(_')._ _" [100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	17	\| NotL c::"coname" t::"trm" "name" binds c in t
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	18	("NotL <_>._ _" [100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	19	\| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" binds c1 in t1, binds c2 in t2
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	20	("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	21	\| AndL1 n::"name" t::"trm" "name" binds n in t
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	22	("AndL1 '(_')._ _" [100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	23	\| AndL2 n::"name" t::"trm" "name" binds n in t
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	24	("AndL2 '(_')._ _" [100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	25	\| OrR1 c::"coname" t::"trm" "coname" binds c in t
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	26	("OrR1 <_>._ _" [100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	27	\| OrR2 c::"coname" t::"trm" "coname" binds c in t
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	28	("OrR2 <_>._ _" [100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	29	\| OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name" binds n1 in t1, binds n2 in t2
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	30	("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	31	\| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" binds c in t1, binds n in t2
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	32	("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100)
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2947 diff changeset	33	\| ImpR n::"name" c::"coname" t::"trm" "coname" binds n c in t
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	34	("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	35
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	36	thm trm.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	37	thm trm.induct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	38	thm trm.exhaust
2617 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
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	40	thm trm.strong_exhaust[simplified]
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	41	thm trm.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	42	thm trm.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	43	thm trm.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	44	thm trm.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	45	thm trm.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	46	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	47	thm trm.supp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	48	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	49
3235 5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3197 diff changeset	50	nominal_function
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	51	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	52	where
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	53	"(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	54	\| "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	55	\| "(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	56	\| "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	57	\| "\<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	58	(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	59	\| "(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	60	\| "(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	61	\| "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	62	(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	63	\| "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	64	(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	65	\| "(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	66	\| "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	67	(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	68	\| "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	69	apply(simp only: eqvt_def)
3197 25d11b449e92 definition of an auxiliary graph in nominal-primrec definitions Christian Urban <urbanc@in.tum.de> parents: 3192 diff changeset	70	apply(simp only: crename_graph_aux_def)
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	71	apply (rule, perm_simp, rule)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	72	apply(rule TrueI)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	73	-- "covered all cases"
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	74	apply(case_tac x)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	75	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	76	apply (simp_all add: fresh_star_def)[12]
a9f3600c9ae6 Speed-up the completeness proof. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2891 diff changeset	77	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	78	-- "compatibility"
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	79	apply(all_trivials)
3192 14c7d7e29c44 added a simproc for alpha-equivalence to the simplifier Christian Urban <urbanc@in.tum.de> parents: 3183 diff changeset	80	using [[simproc del: alpha_lst]]
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	81	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	82	apply(rule conjI)
2892 a9f3600c9ae6 Speed-up the completeness proof. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2891 diff changeset	83	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	84	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	85	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	86	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	87	apply(simp add: eqvt_at_def)
313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	88	apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	89	apply(clarify)
313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	90	apply(simp add: eqvt_at_def)
313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	91	apply(simp add: 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	92	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	93	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	94	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	95	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	96	apply(simp add: eqvt_at_def)
313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	97	apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	98	apply(simp add: eqvt_at_def)
313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	99	apply(simp add: 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	100	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	101	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	102	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	103	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	104	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	105	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	106	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	107	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	108	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	109	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	110	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	111	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	112	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	113	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	114	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	115	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	116	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	117	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	118	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	119	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	120	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	121	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	122	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	123	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	124	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	125	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	126	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	127	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	128	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	129	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	130	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	131	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	132	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	133	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	134	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	135	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	136	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	137	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	138	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	139	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	140	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	141	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	142	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	143	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	144	apply(blast)
fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	145	apply(elim conjE)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	146	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	147	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	148	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	149	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	150	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	151	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	152	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	153	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	154	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	155	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	156	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	157	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	158	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	159	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	160	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	161	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	162	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	163	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	164	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	165	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	166	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	167	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	168	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	169	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	170	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	171	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	172	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	173	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	174	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	175	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	176	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	177	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	178	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	179	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	180	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	181	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	182	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	183	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	184	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	185	apply(rule conjI)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	186	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	187	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	188	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	189	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	190	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	191	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	192	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	193	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	194	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	195	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	196	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	197	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	198	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	199	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	200	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	201	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	202	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	203	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	204	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	205	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	206	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	207	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	208	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	209	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	210	defer
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	211	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	212	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	213	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	214	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	215	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	216	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	217	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	218	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	219	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	220	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	221	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	222	apply(blast)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	223	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	224	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	225	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	226	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	227	apply(simp add: Abs_fresh_iff)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	228	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	229	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	230	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	231	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	232	apply(simp add: eqvt_at_def)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	233	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	234	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	235	apply(blast)
2910 ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	236	apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	237	apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	238	apply(erule conjE)+
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	239	apply(erule Abs_lst_fcb2)
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	240	apply(simp add: Abs_fresh_star)
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	241	apply(simp add: Abs_fresh_star)
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	242	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	243	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	244	apply(simp add: eqvt_at_def)
2910 ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	245	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	246	apply(simp add: eqvt_at_def)
2910 ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	247	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	248	apply(blast)
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	249	apply(blast)
ae6455351572 completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier) Christian Urban <urbanc@in.tum.de> parents: 2909 diff changeset	250	done
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	251
3236 e2da10806a34 changed nominal_primrec to nominal_function and termination to nominal_termination Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3235 diff changeset	252	nominal_termination (eqvt)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	253	by lexicographic_order
2926 37c0d7953cba moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through Christian Urban <urbanc@in.tum.de> parents: 2914 diff changeset	254
3235 5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3197 diff changeset	255	nominal_function
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	256	nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	257	where
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	258	"(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	259	\| "atom x \<sharp> (u, v) \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	260	\| "atom x \<sharp> (u, v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	261	\| "(NotL <a>.M x)[u\<turnstile>n>v] = (if x=u then NotL <a>.(M[u\<turnstile>n>v]) v else NotL <a>.(M[u\<turnstile>n>v]) x)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	262	\| "(AndR <a>.M <b>.N c)[u\<turnstile>n>v] = AndR <a>.(M[u\<turnstile>n>v]) <b>.(N[u\<turnstile>n>v]) c"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	263	\| "atom x \<sharp> (u, v) \<Longrightarrow> (AndL1 (x).M y)[u\<turnstile>n>v] =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	264	(if y=u then AndL1 (x).(M[u\<turnstile>n>v]) v else AndL1 (x).(M[u\<turnstile>n>v]) y)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	265	\| "atom x \<sharp> (u, v) \<Longrightarrow> (AndL2 (x).M y)[u\<turnstile>n>v] =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	266	(if y=u then AndL2 (x).(M[u\<turnstile>n>v]) v else AndL2 (x).(M[u\<turnstile>n>v]) y)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	267	\| "(OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	268	\| "(OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	269	\| "\<lbrakk>atom x \<sharp> (u, v); atom y \<sharp> (u, v)\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[u\<turnstile>n>v] =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	270	(if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	271	\| "atom x \<sharp> (u, v) \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	272	\| "atom x \<sharp> (u, v) \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	273	(if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	274	apply(simp only: eqvt_def)
3197 25d11b449e92 definition of an auxiliary graph in nominal-primrec definitions Christian Urban <urbanc@in.tum.de> parents: 3192 diff changeset	275	apply(simp only: nrename_graph_aux_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	276	apply (rule, perm_simp, rule)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	277	apply(rule TrueI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	278	-- "covered all cases"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	279	apply(case_tac x)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	280	apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	281	apply (simp_all add: fresh_star_def)[12]
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	282	apply(metis)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	283	-- "compatibility"
3192 14c7d7e29c44 added a simproc for alpha-equivalence to the simplifier Christian Urban <urbanc@in.tum.de> parents: 3183 diff changeset	284	using [[simproc del: alpha_lst]]
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	285	apply(simp_all)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	286	apply(rule conjI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	287	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	288	apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	289	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	290	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	291	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	292	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	293	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	294	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	295	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	296	apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	297	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	298	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	299	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	300	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	301	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	302	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	303	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	304	apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	305	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	306	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	307	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	308	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	309	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	310	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	311	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	312	apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	313	apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	314	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	315	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	316	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	317	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	318	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	319	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	320	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	321	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	322	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	323	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	324	apply(rule conjI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	325	apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	326	apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	327	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	328	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	329	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	330	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	331	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	332	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	333	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	334	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	335	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	336	apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	337	apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	338	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	339	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	340	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	341	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	342	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	343	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	344	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	345	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	346	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	347	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	348	apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	349	apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	350	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	351	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	352	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	353	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	354	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	355	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	356	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	357	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	358	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	359	apply(elim conjE)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	360	apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	361	apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	362	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	363	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	364	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	365	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	366	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	367	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	368	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	369	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	370	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	371	apply(elim conjE)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	372	apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	373	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	374	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	375	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	376	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	377	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	378	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	379	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	380	apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	381	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	382	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	383	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	384	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	385	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	386	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	387	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	388	apply(rule conjI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	389	apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	390	apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	391	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	392	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	393	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	394	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	395	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	396	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	397	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	398	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	399	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	400	apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	401	apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	402	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	403	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	404	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	405	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	406	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	407	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	408	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	409	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	410	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	411	apply(erule conjE)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	412	apply(erule Abs_lst_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	413	apply(simp add: Abs_fresh_star)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	414	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	415	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	416	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	417	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	418	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	419	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	420	apply(erule conjE)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	421	apply(rule conjI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	422	apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	423	apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	424	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	425	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	426	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	427	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	428	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	429	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	430	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	431	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	432	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	433	apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	434	apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	435	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	436	apply(simp add: Abs_fresh_iff)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	437	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	438	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	439	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
3183 313e6f2cdd89 added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often Christian Urban <urbanc@in.tum.de> parents: 2975 diff changeset	440	apply(simp add: eqvt_at_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	441	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	442	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	443	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	444	done
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	445
3236 e2da10806a34 changed nominal_primrec to nominal_function and termination to nominal_termination Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3235 diff changeset	446	nominal_termination (eqvt)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	447	by lexicographic_order
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	448
2975 c62e26830420 preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec Christian Urban <urbanc@in.tum.de> parents: 2973 diff changeset	449	thm crename.eqvt nrename.eqvt
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	450
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	451
3235 5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3197 diff changeset	452	nominal_function
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	453	substn :: "trm \<Rightarrow> name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	454	where
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	455	"(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	456	\| "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	457	(if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	458	\| "atom x\<sharp> (y, P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	459	\| "\<lbrakk>atom a\<sharp> (c, P); atom x' \<sharp> (M, y, P)\<rbrakk> \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	460	(if x=y then Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x' else NotL <a>.(M{y:=<c>.P}) x)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	461	\| "\<lbrakk>atom a \<sharp> (c, P); atom b \<sharp> (c, P)\<rbrakk> \<Longrightarrow>
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	462	(AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	463	\| "atom x \<sharp> (y, P) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	464	(if z=y then Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z' else AndL1 (x).(M{y:=<c>.P}) z)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	465	\| "atom x \<sharp> (y, P) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	466	(if z=y then Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z' else AndL2 (x).(M{y:=<c>.P}) z)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	467	\| "atom a \<sharp> (c, P) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	468	\| "atom a \<sharp> (c, P) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	469	\| "\<lbrakk>atom x \<sharp> (y, P); atom u \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	470	(if z=y then Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z'
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	471	else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	472	\| "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	473	\| "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} =
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	474	(if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z'
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	475	else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	476	apply(simp only: eqvt_def)
3197 25d11b449e92 definition of an auxiliary graph in nominal-primrec definitions Christian Urban <urbanc@in.tum.de> parents: 3192 diff changeset	477	apply(simp only: substn_graph_aux_def)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	478	apply (rule, perm_simp, rule)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	479	apply(rule TrueI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	480	-- "covered all cases"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	481	apply(case_tac x)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	482	apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	483	apply (simp_all add: fresh_star_def fresh_Pair)[12]
3192 14c7d7e29c44 added a simproc for alpha-equivalence to the simplifier Christian Urban <urbanc@in.tum.de> parents: 3183 diff changeset	484	apply(metis)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	485	oops
2926 37c0d7953cba moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through Christian Urban <urbanc@in.tum.de> parents: 2914 diff changeset	486
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	487	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	488
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	489
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	490

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 19 May 2014 16:45:46 +0100
changeset 3236	e2da10806a34
parent 3235	5ebd327ffb96
permissions	-rw-r--r--