117 apply(drule_tac x="p" in meta_spec) |
117 apply(drule_tac x="p" in meta_spec) |
118 apply(drule_tac x="bs" in meta_spec) |
118 apply(drule_tac x="bs" in meta_spec) |
119 apply(auto simp add: yy1) |
119 apply(auto simp add: yy1) |
120 apply(rule_tac x="q \<bullet> x" in exI) |
120 apply(rule_tac x="q \<bullet> x" in exI) |
121 apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x") |
121 apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x") |
|
122 apply(simp) |
|
123 apply(rule supp_perm_eq) |
|
124 apply(rule fresh_star_supp_conv) |
|
125 apply(simp add: fresh_star_def) |
|
126 apply(simp add: Abs_fresh_iff) |
|
127 apply(auto) |
|
128 done |
|
129 |
|
130 lemma abs_rename_res: |
|
131 fixes x::"'a::fs" |
|
132 assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs" |
|
133 shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" |
|
134 using yy assms |
|
135 apply - |
|
136 apply(drule_tac x="p" in meta_spec) |
|
137 apply(drule_tac x="bs" in meta_spec) |
|
138 apply(auto simp add: yy1) |
|
139 apply(rule_tac x="q \<bullet> x" in exI) |
|
140 apply(subgoal_tac "(q \<bullet> ([bs]res. x)) = [bs]res. x") |
122 apply(simp) |
141 apply(simp) |
123 apply(rule supp_perm_eq) |
142 apply(rule supp_perm_eq) |
124 apply(rule fresh_star_supp_conv) |
143 apply(rule fresh_star_supp_conv) |
125 apply(simp add: fresh_star_def) |
144 apply(simp add: fresh_star_def) |
126 apply(simp add: Abs_fresh_iff) |
145 apply(simp add: Abs_fresh_iff) |