nominal2: Nominal/Ex/Classical.thy@6d2859aeebba (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
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	50	nominal_primrec
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)
0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	70	apply(simp only: crename_graph_def)
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)
2889 0435c4dfd6f6 expanded the example Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	80	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	81	apply(rule conjI)
2892 a9f3600c9ae6 Speed-up the completeness proof. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2891 diff changeset	82	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	83	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	84	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	85	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	86	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	87	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	88	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	89	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	90	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	91	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	92	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
d66430c7c4f1 an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders. Christian Urban <urbanc@in.tum.de> parents: 2899 diff changeset	93	apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	94	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	95	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	96	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	97	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	98	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	99	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	100	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	101	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	102	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	103	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	104	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	105	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	106	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	107	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	108	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	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(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	111	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	112	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	113	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	114	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	115	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	116	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	117	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	118	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	119	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	120	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	121	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	122	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	123	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	124	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	125	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	126	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	127	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	128	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	129	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	130	apply(blast)
fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	131	apply(elim conjE)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	132	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	133	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	134	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	135	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	136	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	137	apply(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	138	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	139	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	140	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	141	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	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(elim conjE)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	144	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	145	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	146	apply(erule 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)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	149	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	150	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	151	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	152	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	153	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	154	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	155	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	156	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	157	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	158	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	159	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	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(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	162	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	163	apply(rule conjI)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	164	apply(erule conjE)+
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	165	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	166	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	167	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	168	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	169	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	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(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	172	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	173	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	174	apply(erule conjE)+
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 (N, da, ea)")
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	176	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	177	apply(erule Abs_lst1_fcb2)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	178	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	179	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	180	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	181	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	182	apply(blast)
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	defer
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	185	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	186	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	187	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	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)
2899 fe290b4e508f except for the interated binder case, finished definition in Calssical.thy Christian Urban <urbanc@in.tum.de> parents: 2892 diff changeset	190	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	191	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	192	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	193	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	194	apply(blast)
2901 754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	195	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	196	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	197	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	198	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	199	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	200	apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	201	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	202	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	203	apply(blast)
754aa24006c8 did all cases, except the multiple binder case Christian Urban <urbanc@in.tum.de> parents: 2900 diff changeset	204	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	205	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	206	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	207	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	208	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	209	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	210	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	211	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	212	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	213	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	214	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	215	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	216	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	217	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	218
2973 d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	219	termination (eqvt)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	220	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	221
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	222	nominal_primrec
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	223	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	224	where
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	225	"(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	226	\| "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	227	\| "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	228	\| "(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	229	\| "(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	230	\| "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	231	(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	232	\| "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	233	(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	234	\| "(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	235	\| "(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	236	\| "\<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	237	(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	238	\| "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	239	\| "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	240	(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	241	apply(simp only: eqvt_def)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	242	apply(simp only: nrename_graph_def)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	243	apply (rule, perm_simp, rule)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	244	apply(rule TrueI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	245	-- "covered all cases"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	246	apply(case_tac x)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	247	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	248	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	249	apply(metis)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	250	-- "compatibility"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	251	apply(simp_all)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	252	apply(rule conjI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	253	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	254	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	255	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	256	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	257	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	258	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	259	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	260	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	261	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	262	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	263	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	264	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	265	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	266	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	267	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	268	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	269	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	270	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	271	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	272	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	273	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	274	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	275	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	276	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	277	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	278	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	279	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	280	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	281	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	282	apply(rule conjI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	283	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	284	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	285	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	286	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	287	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	288	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	289	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	290	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	291	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	292	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	293	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	294	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	295	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	296	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	297	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	298	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	299	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	300	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	301	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	302	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	303	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	304	apply(erule 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)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	307	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	308	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	309	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	310	apply(blast)
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)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	317	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	318	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	319	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	320	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	321	apply(elim conjE)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	322	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	323	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	324	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	325	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	326	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	327	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	328	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	329	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	330	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	331	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	332	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	333	apply(elim conjE)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	334	apply(rule conjI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	335	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	336	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	337	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	338	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	339	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	340	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	341	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	342	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	343	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	344	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	345	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	346	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	347	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	348	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	349	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	350	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	351	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	352	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	353	apply(erule conjE)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	354	apply(erule Abs_lst_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	355	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	356	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	357	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	358	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	359	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	360	apply(erule conjE)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	361	apply(rule conjI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	362	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	363	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	364	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	365	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	366	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	367	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	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(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	372	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	373	apply(erule Abs_lst1_fcb2)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	374	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	375	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	376	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	377	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	378	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	379	apply(blast)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	380	done
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	381
2973 d1038e67923a added a flag (eqvt) to termination proofs arising fron nominal_primrecs Christian Urban <urbanc@in.tum.de> parents: 2950 diff changeset	382	termination (eqvt)
2947 7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	383	by lexicographic_order
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	384
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	385	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	386
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	387
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	388	nominal_primrec
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	389	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	390	where
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	391	"(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	392	\| "\<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	393	(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	394	\| "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	395	\| "\<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	396	(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	397	\| "\<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	398	(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	399	\| "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	400	(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	401	\| "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	402	(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	403	\| "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	404	\| "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	405	\| "\<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	406	(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	407	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	408	\| "\<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	409	\| "\<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	410	(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	411	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	412	apply(simp only: eqvt_def)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	413	apply(simp only: substn_graph_def)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	414	apply (rule, perm_simp, rule)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	415	apply(rule TrueI)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	416	-- "covered all cases"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	417	apply(case_tac x)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	418	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	419	apply (simp_all add: fresh_star_def fresh_Pair)[12]
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	420	apply(metis)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	421	apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	422	apply(auto simp add: fresh_Pair)[1]
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	423	apply(metis)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	424	apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	425	apply(auto simp add: fresh_Pair)[1]
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	426	apply(rule obtain_fresh)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	427	apply(auto)[1]
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	428	apply(metis)+
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	429	-- "compatibility"
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	430	apply(all_trivials)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	431	apply(simp)
7ab36bc29cc2 added another example which seems difficult to define Christian Urban <urbanc@in.tum.de> parents: 2943 diff changeset	432	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	433
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	434	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	435
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	436
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	437

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Fri, 19 Aug 2011 11:01:52 +0900
changeset 2995	6d2859aeebba
parent 2975	c62e26830420
child 3071	11f6a561eb4b
child 3183	313e6f2cdd89
permissions	-rw-r--r--