|
1 theory Nominal2_FSet |
|
2 imports FSet Nominal2_Supp |
|
3 begin |
|
4 |
|
5 lemma permute_rsp_fset[quot_respect]: |
|
6 "(op = ===> op \<approx> ===> op \<approx>) permute permute" |
|
7 apply (simp add: eqvts[symmetric]) |
|
8 apply clarify |
|
9 apply (subst permute_minus_cancel(1)[symmetric, of "xb"]) |
|
10 apply (subst mem_eqvt[symmetric]) |
|
11 apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"]) |
|
12 apply (subst mem_eqvt[symmetric]) |
|
13 apply (erule_tac x="- x \<bullet> xb" in allE) |
|
14 apply simp |
|
15 done |
|
16 |
|
17 instantiation FSet.fset :: (pt) pt |
|
18 begin |
|
19 |
|
20 term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
21 |
|
22 quotient_definition |
|
23 "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
24 is |
|
25 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
26 |
|
27 lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x" |
|
28 by (rule permute_zero) |
|
29 |
|
30 lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x" |
|
31 by (lifting permute_list_zero) |
|
32 |
|
33 lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x" |
|
34 by (rule permute_plus) |
|
35 |
|
36 lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x" |
|
37 by (lifting permute_list_plus) |
|
38 |
|
39 instance |
|
40 apply default |
|
41 apply (rule permute_fset_zero) |
|
42 apply (rule permute_fset_plus) |
|
43 done |
|
44 |
|
45 end |
|
46 |
|
47 lemma permute_fset[simp,eqvt]: |
|
48 "p \<bullet> ({||} :: 'a :: pt fset) = {||}" |
|
49 "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)" |
|
50 by (lifting permute_list.simps) |
|
51 |
|
52 lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)" |
|
53 apply (induct l) |
|
54 apply (simp_all) |
|
55 apply (simp only: eqvt_apply) |
|
56 done |
|
57 |
|
58 lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)" |
|
59 by (lifting map_eqvt) |
|
60 |
|
61 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)" |
|
62 by (lifting set_eqvt) |
|
63 |
|
64 lemma supp_fset_to_set: |
|
65 "supp (fset_to_set x) = supp x" |
|
66 apply (simp add: supp_def) |
|
67 apply (simp add: eqvts) |
|
68 apply (simp add: fset_cong) |
|
69 done |
|
70 |
|
71 lemma atom_fmap_cong: |
|
72 shows "(fmap atom x = fmap atom y) = (x = y)" |
|
73 apply(rule inj_fmap_eq_iff) |
|
74 apply(simp add: inj_on_def) |
|
75 done |
|
76 |
|
77 lemma supp_fmap_atom: |
|
78 "supp (fmap atom x) = supp x" |
|
79 apply (simp add: supp_def) |
|
80 apply (simp add: eqvts eqvts_raw atom_fmap_cong) |
|
81 done |
|
82 |
|
83 (*lemma "\<not> (memb x S) \<Longrightarrow> \<not> (memb y T) \<Longrightarrow> ((x # S) \<approx> (y # T)) = (x = y \<and> S \<approx> T)"*) |
|
84 |
|
85 lemma infinite_Un: |
|
86 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
87 by simp |
|
88 |
|
89 lemma supp_insert: "supp (insert (x :: 'a :: fs) xs) = supp x \<union> supp xs" |
|
90 oops |
|
91 |
|
92 lemma supp_finsert: |
|
93 "supp (finsert (x :: 'a :: fs) S) = supp x \<union> supp S" |
|
94 apply (subst supp_fset_to_set[symmetric]) |
|
95 apply simp |
|
96 (* apply (simp add: supp_insert supp_fset_to_set) *) |
|
97 oops |
|
98 |
|
99 instance fset :: (fs) fs |
|
100 apply (default) |
|
101 apply (induct_tac x rule: fset_induct) |
|
102 apply (simp add: supp_def eqvts) |
|
103 (* apply (simp add: supp_finsert) *) |
|
104 (* apply default ? *) |
|
105 oops |
|
106 |
|
107 end |