equal
deleted
inserted
replaced
62 |
62 |
63 text {* |
63 text {* |
64 tests by cu |
64 tests by cu |
65 *} |
65 *} |
66 |
66 |
67 |
|
68 lemma yy: |
67 lemma yy: |
69 assumes a: "p \<bullet> bs \<inter> bs = {}" |
68 assumes a: "p \<bullet> bs \<inter> bs = {}" |
70 and b: "finite bs" |
69 and b: "finite bs" |
71 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
70 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
72 using b a |
71 using b a |
97 apply(erule conjE)+ |
96 apply(erule conjE)+ |
98 apply(drule sym) |
97 apply(drule sym) |
99 apply(simp add: mem_permute_iff) |
98 apply(simp add: mem_permute_iff) |
100 apply(simp add: mem_permute_iff) |
99 apply(simp add: mem_permute_iff) |
101 done |
100 done |
|
101 |
|
102 |
102 |
103 |
103 lemma Abs_rename_set: |
104 lemma Abs_rename_set: |
104 fixes x::"'a::fs" |
105 fixes x::"'a::fs" |
105 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
106 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
106 and b: "finite bs" |
107 and b: "finite bs" |
215 |
216 |
216 lemma test6: |
217 lemma test6: |
217 fixes c::"'a::fs" |
218 fixes c::"'a::fs" |
218 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
219 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
219 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
220 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
220 and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" |
221 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
221 and "\<exists>a1 trm1 a2 trm2. ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P" |
222 and "\<exists>a1 trm1 a2 trm2. ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P" |
222 and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P" |
223 and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P" |
223 shows "P" |
224 shows "P" |
224 apply(rule_tac y="y" in foo.exhaust(1)) |
225 apply(rule_tac y="y" in foo.exhaust(1)) |
225 apply(rule assms(1)) |
226 apply(rule assms(1)) |
228 apply(rule assms(2)) |
229 apply(rule assms(2)) |
229 apply(rule exI)+ |
230 apply(rule exI)+ |
230 apply(assumption) |
231 apply(assumption) |
231 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)") |
232 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)") |
232 apply(erule exE) |
233 apply(erule exE) |
233 apply(rule assms(3)) |
|
234 apply(insert Abs_rename_list)[1] |
234 apply(insert Abs_rename_list)[1] |
235 apply(drule_tac x="p" in meta_spec) |
235 apply(drule_tac x="p" in meta_spec) |
236 apply(drule_tac x="[atom name]" in meta_spec) |
236 apply(drule_tac x="[atom name]" in meta_spec) |
237 apply(drule_tac x="trm" in meta_spec) |
237 apply(drule_tac x="trm" in meta_spec) |
238 apply(simp only: fresh_star_Pair set.simps) |
238 apply(simp only: fresh_star_Pair set.simps) |
239 apply(drule meta_mp) |
239 apply(drule meta_mp) |
240 apply(simp) |
240 apply(simp) |
241 apply(erule exE) |
241 apply(erule exE) |
242 apply(rule exI)+ |
242 apply(rule assms(3)) |
243 apply(perm_simp) |
243 apply(perm_simp) |
244 apply(erule conjE)+ |
244 apply(erule conjE)+ |
245 apply(rule conjI) |
245 apply(assumption) |
246 apply(assumption) |
246 apply(clarify) |
247 apply(simp add: foo.eq_iff) |
247 apply(simp (no_asm) add: foo.eq_iff) |
|
248 apply(perm_simp) |
|
249 apply(assumption) |
248 apply(rule at_set_avoiding1) |
250 apply(rule at_set_avoiding1) |
249 apply(simp) |
251 apply(simp) |
250 apply(simp add: finite_supp) |
252 apply(simp add: finite_supp) |
251 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
253 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
252 apply(erule exE) |
254 apply(erule exE) |