equal
deleted
inserted
replaced
1 theory Abs |
1 theory Abs |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd" |
3 begin |
3 begin |
4 |
4 |
5 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
5 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
6 lemma in_permute_iff: |
|
7 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
|
8 apply(unfold mem_def permute_fun_def)[1] |
|
9 apply(simp add: permute_bool_def) |
|
10 done |
|
11 |
|
12 lemma fresh_plus: |
|
13 fixes p q::perm |
|
14 shows "\<lbrakk>a \<sharp> p; a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)" |
|
15 unfolding fresh_def |
|
16 using supp_plus_perm |
|
17 by(auto) |
|
18 |
|
19 lemma fresh_star_plus: |
6 lemma fresh_star_plus: |
20 fixes p q::perm |
7 fixes p q::perm |
21 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
8 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
22 unfolding fresh_star_def |
9 unfolding fresh_star_def |
23 by (simp add: fresh_plus) |
10 by (simp add: fresh_plus_perm) |
24 |
11 |
25 |
12 |
26 lemma fresh_star_permute_iff: |
13 lemma fresh_star_permute_iff: |
27 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
14 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
28 apply(simp add: fresh_star_def) |
15 apply(simp add: fresh_star_def) |
32 apply(simp add: eqvts del: permute_eqvt) |
19 apply(simp add: eqvts del: permute_eqvt) |
33 apply(simp add: fresh_permute_iff) |
20 apply(simp add: fresh_permute_iff) |
34 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1]) |
21 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1]) |
35 apply(simp) |
22 apply(simp) |
36 apply(drule_tac x="- p \<bullet> xa" in bspec) |
23 apply(drule_tac x="- p \<bullet> xa" in bspec) |
37 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1]) |
24 apply(rule_tac ?p1="p" in mem_permute_iff[THEN iffD1]) |
38 apply(simp) |
25 apply(simp) |
39 apply(simp) |
26 apply(simp) |
40 done |
27 done |
41 |
|
42 lemma fresh_minus_perm: |
|
43 fixes p::perm |
|
44 shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p" |
|
45 apply(simp add: fresh_def) |
|
46 apply(simp only: supp_minus_perm) |
|
47 done |
|
48 |
28 |
49 fun |
29 fun |
50 alpha_gen |
30 alpha_gen |
51 where |
31 where |
52 alpha_gen[simp del]: |
32 alpha_gen[simp del]: |