equal
deleted
inserted
replaced
38 "(p \<bullet> {||}) = ({||} :: 'a::pt fset)" |
38 "(p \<bullet> {||}) = ({||} :: 'a::pt fset)" |
39 "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)" |
39 "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)" |
40 by (lifting permute_list.simps) |
40 by (lifting permute_list.simps) |
41 |
41 |
42 lemma fmap_eqvt[eqvt]: |
42 lemma fmap_eqvt[eqvt]: |
43 shows "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)" |
43 shows "p \<bullet> (fmap f l) = fmap (p \<bullet> f) (p \<bullet> l)" |
44 by (lifting map_eqvt) |
44 by (lifting map_eqvt) |
45 |
45 |
46 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)" |
46 lemma fset_to_set_eqvt[eqvt]: |
|
47 shows "p \<bullet> (fset_to_set x) = fset_to_set (p \<bullet> x)" |
47 by (lifting set_eqvt) |
48 by (lifting set_eqvt) |
48 |
49 |
49 lemma fin_fset_to_set: |
50 lemma fin_fset_to_set: |
50 "finite (fset_to_set x)" |
51 shows "finite (fset_to_set x)" |
51 by (induct x) (simp_all) |
52 by (induct x) (simp_all) |
52 |
53 |
53 lemma supp_fset_to_set: |
54 lemma supp_fset_to_set: |
54 "supp (fset_to_set x) = supp x" |
55 "supp (fset_to_set x) = supp x" |
55 apply (simp add: supp_def) |
56 apply (simp add: supp_def) |
62 apply(rule inj_fmap_eq_iff) |
63 apply(rule inj_fmap_eq_iff) |
63 apply(simp add: inj_on_def) |
64 apply(simp add: inj_on_def) |
64 done |
65 done |
65 |
66 |
66 lemma supp_fmap_atom: |
67 lemma supp_fmap_atom: |
67 "supp (fmap atom x) = supp x" |
68 shows "supp (fmap atom x) = supp x" |
68 apply (simp add: supp_def) |
69 unfolding supp_def |
69 apply (simp add: eqvts eqvts_raw atom_fmap_cong) |
70 apply (perm_simp) |
|
71 apply (simp add: atom_fmap_cong) |
70 done |
72 done |
71 |
73 |
72 lemma supp_atom_insert: |
74 lemma supp_atom_insert: |
73 "finite (xs :: atom set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs" |
75 "finite (xs :: atom set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs" |
74 apply (simp add: supp_finite_atom_set) |
76 apply (simp add: supp_finite_atom_set) |
82 done |
84 done |
83 |
85 |
84 lemma atom_eqvt_raw: |
86 lemma atom_eqvt_raw: |
85 fixes p::"perm" |
87 fixes p::"perm" |
86 shows "(p \<bullet> atom) = atom" |
88 shows "(p \<bullet> atom) = atom" |
87 by (simp add: expand_fun_eq permute_fun_def atom_eqvt) |
89 apply(perm_simp) |
|
90 apply(simp) |
|
91 done |
88 |
92 |
89 lemma supp_finite_at_set: |
93 lemma supp_finite_at_set: |
90 fixes S::"('a :: at) set" |
94 fixes S::"('a :: at) set" |
91 assumes a: "finite S" |
95 assumes a: "finite S" |
92 shows "supp S = atom ` S" |
96 shows "supp S = atom ` S" |