equal
deleted
inserted
replaced
2 imports "../Nominal-General/Nominal2_Base" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 lemma atom_map_fset_cong: |
|
8 shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y" |
|
9 apply(rule inj_map_fset_cong) |
|
10 apply(simp add: inj_on_def) |
|
11 done |
|
12 |
7 |
13 lemma supp_map_fset_atom: |
|
14 shows "supp (map_fset atom S) = supp S" |
|
15 unfolding supp_def |
|
16 apply(perm_simp) |
|
17 apply(simp add: atom_map_fset_cong) |
|
18 done |
|
19 |
|
20 lemma supp_at_fset: |
|
21 fixes S::"('a::at_base) fset" |
|
22 shows "supp S = fset (map_fset atom S)" |
|
23 apply (induct S) |
|
24 apply (simp add: supp_empty_fset) |
|
25 apply (simp add: supp_insert_fset) |
|
26 apply (simp add: supp_at_base) |
|
27 done |
|
28 |
|
29 lemma fresh_star_atom: |
|
30 fixes a::"'a::at_base" |
|
31 shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S" |
|
32 apply (induct S) |
|
33 apply (simp add: fresh_set_empty) |
|
34 apply simp |
|
35 apply (unfold fresh_def) |
|
36 apply (simp add: supp_of_finite_insert) |
|
37 apply (rule conjI) |
|
38 apply (unfold fresh_star_def) |
|
39 apply simp |
|
40 apply (unfold fresh_def) |
|
41 apply (simp add: supp_at_base supp_atom) |
|
42 apply clarify |
|
43 apply auto |
|
44 done |
|
45 |
8 |
46 end |
9 end |