equal
deleted
inserted
replaced
144 apply (subst Abs_eq_iff) |
144 apply (subst Abs_eq_iff) |
145 apply (rule_tac x="0::perm" in exI) |
145 apply (rule_tac x="0::perm" in exI) |
146 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
146 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
147 apply (simp add: alphas fresh_star_zero) |
147 apply (simp add: alphas fresh_star_zero) |
148 apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa") |
148 apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa") |
|
149 apply(simp) |
149 apply blast |
150 apply blast |
150 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)") |
151 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)") |
151 apply (simp add: supp_Pair eqvts eqvts_raw) |
152 apply (simp add: supp_Pair eqvts eqvts_raw) |
152 apply auto[1] |
153 apply auto[1] |
153 apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'") |
154 apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'") |
269 apply(simp add: ty.supp supp_at_base) |
270 apply(simp add: ty.supp supp_at_base) |
270 apply(simp add: fresh_star_def) |
271 apply(simp add: fresh_star_def) |
271 apply(drule_tac x="atom name" in bspec) |
272 apply(drule_tac x="atom name" in bspec) |
272 apply(auto)[1] |
273 apply(auto)[1] |
273 apply(simp add: fresh_def supp_perm) |
274 apply(simp add: fresh_def supp_perm) |
274 apply(perm_simp) |
|
275 apply(auto) |
|
276 done |
275 done |
277 |
276 |
278 nominal_primrec |
277 nominal_primrec |
279 generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _") |
278 generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _") |
280 where |
279 where |