2 imports "../Nominal-General/Nominal2_Base" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 FSet |
4 FSet |
5 begin |
5 begin |
6 |
6 |
7 lemma permute_rsp_fset[quot_respect]: |
7 lemma permute_fset_rsp[quot_respect]: |
8 shows "(op = ===> list_eq ===> list_eq) permute permute" |
8 shows "(op = ===> list_eq ===> list_eq) permute permute" |
9 apply(simp) |
9 by (simp add: set_eqvt[symmetric]) |
10 apply(clarify) |
|
11 apply(rule_tac p="-x" in permute_boolE) |
|
12 apply(perm_simp add: permute_minus_cancel) |
|
13 apply(simp) |
|
14 done |
|
15 |
10 |
16 instantiation fset :: (pt) pt |
11 instantiation fset :: (pt) pt |
17 begin |
12 begin |
18 |
13 |
19 quotient_definition |
14 quotient_definition |
31 end |
26 end |
32 |
27 |
33 lemma permute_fset[simp, eqvt]: |
28 lemma permute_fset[simp, eqvt]: |
34 fixes S::"('a::pt) fset" |
29 fixes S::"('a::pt) fset" |
35 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
30 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
36 and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
31 and "(p \<bullet> finsert x S) = finsert (p \<bullet> x) (p \<bullet> S)" |
37 by (lifting permute_list.simps) |
32 by (lifting permute_list.simps) |
38 |
33 |
39 lemma fmap_eqvt[eqvt]: |
34 lemma fmap_eqvt[eqvt]: |
40 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
35 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
41 by (lifting map_eqvt) |
36 by (lifting map_eqvt) |
42 |
37 |
43 lemma fset_eqvt[eqvt]: |
38 lemma fset_eqvt[eqvt]: |
44 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
39 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
45 by (lifting set_eqvt) |
40 by (lifting set_eqvt) |
46 |
41 |
47 lemma supp_fset: |
42 lemma supp_fset [simp]: |
48 shows "supp (fset S) = supp S" |
43 shows "supp (fset S) = supp S" |
49 unfolding supp_def |
44 unfolding supp_def |
50 by (perm_simp) (simp add: fset_cong) |
45 by (perm_simp) (simp add: fset_cong) |
51 |
46 |
52 lemma supp_fempty: |
47 lemma supp_fempty [simp]: |
53 shows "supp {||} = {}" |
48 shows "supp {||} = {}" |
54 unfolding supp_def |
49 unfolding supp_def |
55 by simp |
50 by simp |
56 |
51 |
57 lemma supp_finsert: |
52 lemma supp_finsert [simp]: |
58 fixes x::"'a::fs" |
53 fixes x::"'a::fs" |
59 and S::"'a fset" |
54 and S::"'a fset" |
60 shows "supp (finsert x S) = supp x \<union> supp S" |
55 shows "supp (finsert x S) = supp x \<union> supp S" |
61 apply(subst supp_fset[symmetric]) |
56 apply(subst supp_fset[symmetric]) |
62 apply(simp add: supp_fset) |
57 apply(simp add: supp_fset supp_of_fin_insert) |
63 apply(simp add: supp_of_fin_insert) |
|
64 apply(simp add: supp_fset) |
|
65 done |
58 done |
66 |
59 |
|
60 lemma fset_finite_supp: |
|
61 fixes S::"('a::fs) fset" |
|
62 shows "finite (supp S)" |
|
63 by (induct S) (simp_all add: finite_supp) |
|
64 |
|
65 |
|
66 subsection {* finite sets are fs-types *} |
67 |
67 |
68 instance fset :: (fs) fs |
68 instance fset :: (fs) fs |
69 apply (default) |
69 apply (default) |
70 apply (induct_tac x rule: fset_induct) |
70 apply (rule fset_finite_supp) |
71 apply (simp add: supp_fempty) |
|
72 apply (simp add: supp_finsert) |
|
73 apply (simp add: finite_supp) |
|
74 done |
71 done |
75 |
72 |
76 lemma atom_fmap_cong: |
73 lemma atom_fmap_cong: |
77 shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y" |
74 shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y" |
78 apply(rule inj_fmap_eq_iff) |
75 apply(rule inj_fmap_eq_iff) |