equal
deleted
inserted
replaced
3 "../Nominal-General/Nominal2_Atoms" |
3 "../Nominal-General/Nominal2_Atoms" |
4 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Eqvt" |
5 FSet |
5 FSet |
6 begin |
6 begin |
7 |
7 |
8 lemma "p \<bullet> {} = {}" |
|
9 apply(perm_simp) |
|
10 by simp |
|
11 |
|
12 lemma permute_rsp_fset[quot_respect]: |
8 lemma permute_rsp_fset[quot_respect]: |
13 "(op = ===> list_eq ===> list_eq) permute permute" |
9 shows "(op = ===> list_eq ===> list_eq) permute permute" |
14 apply (simp add: eqvts[symmetric]) |
10 apply(simp) |
15 apply clarify |
11 apply(clarify) |
16 apply (subst permute_minus_cancel(1)[symmetric, of "xb"]) |
12 apply(simp add: eqvts[symmetric]) |
17 apply (subst mem_eqvt[symmetric]) |
13 apply(subst permute_minus_cancel(1)[symmetric, of "xb"]) |
18 apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"]) |
14 apply(subst mem_eqvt[symmetric]) |
19 apply (subst mem_eqvt[symmetric]) |
15 apply(subst (2) permute_minus_cancel(1)[symmetric, of "xb"]) |
20 apply (erule_tac x="- x \<bullet> xb" in allE) |
16 apply(subst mem_eqvt[symmetric]) |
21 apply simp |
17 apply(simp) |
22 done |
18 done |
23 |
19 |
24 instantiation fset :: (pt) pt |
20 instantiation fset :: (pt) pt |
25 begin |
21 begin |
26 |
22 |
38 by (lifting permute_plus [where 'a="'a list"]) |
34 by (lifting permute_plus [where 'a="'a list"]) |
39 qed |
35 qed |
40 |
36 |
41 end |
37 end |
42 |
38 |
43 lemma "p \<bullet> {} = {}" |
|
44 apply(perm_simp) |
|
45 by simp |
|
46 |
|
47 lemma permute_fset[simp]: |
39 lemma permute_fset[simp]: |
48 fixes S::"('a::pt) fset" |
40 fixes S::"('a::pt) fset" |
49 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
41 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
50 and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
42 and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
51 by (lifting permute_list.simps) |
43 by (lifting permute_list.simps) |
52 |
44 |
53 lemma "p \<bullet> {} = {}" |
|
54 apply(perm_simp) |
|
55 by simp |
|
56 |
|
57 ML {* @{term "{}"} ; @{term "{||}"} *} |
|
58 |
|
59 declare permute_fset[eqvt] |
45 declare permute_fset[eqvt] |
60 |
|
61 lemma "p \<bullet> {} = {}" |
|
62 apply(perm_simp) |
|
63 by simp |
|
64 |
|
65 |
46 |
66 lemma fmap_eqvt[eqvt]: |
47 lemma fmap_eqvt[eqvt]: |
67 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
48 shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
68 by (lifting map_eqvt) |
49 by (lifting map_eqvt) |
69 |
50 |
78 lemma supp_fset_to_set: |
59 lemma supp_fset_to_set: |
79 shows "supp (fset_to_set S) = supp S" |
60 shows "supp (fset_to_set S) = supp S" |
80 unfolding supp_def |
61 unfolding supp_def |
81 by (perm_simp) (simp add: fset_cong) |
62 by (perm_simp) (simp add: fset_cong) |
82 |
63 |
|
64 lemma supp_fempty: |
|
65 shows "supp {||} = {}" |
|
66 unfolding supp_def |
|
67 by simp |
|
68 |
83 lemma supp_finsert: |
69 lemma supp_finsert: |
84 fixes x::"'a::fs" |
70 fixes x::"'a::fs" |
85 shows "supp (finsert x S) = supp x \<union> supp S" |
71 shows "supp (finsert x S) = supp x \<union> supp S" |
86 apply(subst supp_fset_to_set[symmetric]) |
72 apply(subst supp_fset_to_set[symmetric]) |
87 apply(simp add: supp_fset_to_set) |
73 apply(simp add: supp_fset_to_set) |
88 apply(simp add: supp_of_fin_insert) |
74 apply(simp add: supp_of_fin_insert) |
89 apply(simp add: supp_fset_to_set) |
75 apply(simp add: supp_fset_to_set) |
90 done |
76 done |
91 |
77 |
92 lemma supp_fempty: |
|
93 shows "supp {||} = {}" |
|
94 unfolding supp_def |
|
95 by simp |
|
96 |
78 |
97 instance fset :: (fs) fs |
79 instance fset :: (fs) fs |
98 apply (default) |
80 apply (default) |
99 apply (induct_tac x rule: fset_induct) |
81 apply (induct_tac x rule: fset_induct) |
100 apply (simp add: supp_fempty) |
82 apply (simp add: supp_fempty) |
123 apply (simp add: supp_finsert) |
105 apply (simp add: supp_finsert) |
124 apply (simp add: supp_at_base) |
106 apply (simp add: supp_at_base) |
125 done |
107 done |
126 |
108 |
127 lemma fresh_star_atom: |
109 lemma fresh_star_atom: |
128 "fset_to_set s \<sharp>* (a :: _ :: at_base) \<Longrightarrow> atom a \<sharp> fset_to_set s" |
110 fixes a::"'a::at_base" |
129 apply (induct s) |
111 shows "fset_to_set S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset_to_set S" |
|
112 apply (induct S) |
130 apply (simp add: fresh_set_empty) |
113 apply (simp add: fresh_set_empty) |
131 apply simp |
114 apply simp |
132 apply (unfold fresh_def) |
115 apply (unfold fresh_def) |
133 apply (simp add: supp_atom_insert) |
116 apply (simp add: supp_atom_insert) |
134 apply (rule conjI) |
117 apply (rule conjI) |
138 apply (simp add: supp_at_base supp_atom) |
121 apply (simp add: supp_at_base supp_atom) |
139 apply clarify |
122 apply clarify |
140 apply auto |
123 apply auto |
141 done |
124 done |
142 |
125 |
143 lemma "p \<bullet> {} = {}" |
|
144 apply(perm_simp) |
|
145 by simp |
|
146 |
|
147 end |
126 end |