88 (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b" |
88 (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b" |
89 by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto |
89 by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto |
90 |
90 |
91 lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] |
91 lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] |
92 |
92 |
93 lemma Abs_lst_fcb: |
|
94 fixes xs ys :: "'a :: fs" |
|
95 and S T :: "'b :: fs" |
|
96 assumes e: "(Abs_lst (ba xs) T) = (Abs_lst (ba ys) S)" |
|
97 and f1: "\<And>x. x \<in> set (ba xs) \<Longrightarrow> x \<sharp> f xs T" |
|
98 and f2: "\<And>x. supp T - set (ba xs) = supp S - set (ba ys) \<Longrightarrow> x \<in> set (ba ys) \<Longrightarrow> x \<sharp> f xs T" |
|
99 and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> p \<bullet> ba xs = ba ys \<Longrightarrow> supp p \<subseteq> set (ba xs) \<union> set (ba ys) \<Longrightarrow> p \<bullet> (f xs T) = f ys S" |
|
100 shows "f xs T = f ys S" |
|
101 using e apply - |
|
102 apply(subst (asm) Abs_eq_iff2) |
|
103 apply(simp add: alphas) |
|
104 apply(elim exE conjE) |
|
105 apply(rule trans) |
|
106 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
107 apply(rule fresh_star_supp_conv) |
|
108 apply(drule fresh_star_perm_set_conv) |
|
109 apply(rule finite_Diff) |
|
110 apply(rule finite_supp) |
|
111 apply(subgoal_tac "(set (ba xs) \<union> set (ba ys)) \<sharp>* f xs T") |
|
112 apply(metis Un_absorb2 fresh_star_Un) |
|
113 apply(subst fresh_star_Un) |
|
114 apply(rule conjI) |
|
115 apply(simp add: fresh_star_def f1) |
|
116 apply(simp add: fresh_star_def f2) |
|
117 apply(simp add: eqv) |
|
118 done |
|
119 |
|
120 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
93 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
121 by (simp add: permute_pure) |
94 by (simp add: permute_pure) |
122 |
95 |
123 (* TODO: should be provided by nominal *) |
96 (* TODO: should be provided by nominal *) |
124 lemmas [eqvt] = trm_assn.fv_bn_eqvt |
97 lemmas [eqvt] = trm_assn.fv_bn_eqvt |