author | nipkow |
Mon, 13 Sep 2010 11:13:15 +0200 | |
changeset 39302 | d7728f65b353 |
parent 39198 | f967a16dfcdd |
child 39994 | 7bd8013b903f |
permissions | -rw-r--r-- |
36524
3909002beca5
Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36465
diff
changeset
|
1 |
(* Title: HOL/Quotient_Examples/FSet.thy |
36465 | 2 |
Author: Cezary Kaliszyk, TU Munich |
3 |
Author: Christian Urban, TU Munich |
|
36280 | 4 |
|
36465 | 5 |
A reasoning infrastructure for the type of finite sets. |
36280 | 6 |
*) |
36465 | 7 |
|
36280 | 8 |
theory FSet |
36465 | 9 |
imports Quotient_List |
36280 | 10 |
begin |
11 |
||
12 |
text {* Definiton of List relation and the quotient type *} |
|
13 |
||
14 |
fun |
|
15 |
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50) |
|
16 |
where |
|
17 |
"list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |
|
18 |
||
19 |
lemma list_eq_equivp: |
|
20 |
shows "equivp list_eq" |
|
21 |
unfolding equivp_reflp_symp_transp |
|
22 |
unfolding reflp_def symp_def transp_def |
|
23 |
by auto |
|
24 |
||
25 |
quotient_type |
|
26 |
'a fset = "'a list" / "list_eq" |
|
27 |
by (rule list_eq_equivp) |
|
28 |
||
29 |
text {* Raw definitions *} |
|
30 |
||
31 |
definition |
|
32 |
memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
|
33 |
where |
|
34 |
"memb x xs \<equiv> x \<in> set xs" |
|
35 |
||
36 |
definition |
|
37 |
sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
38 |
where |
|
39 |
"sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)" |
|
40 |
||
41 |
fun |
|
42 |
fcard_raw :: "'a list \<Rightarrow> nat" |
|
43 |
where |
|
44 |
fcard_raw_nil: "fcard_raw [] = 0" |
|
45 |
| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))" |
|
46 |
||
47 |
primrec |
|
48 |
finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
49 |
where |
|
50 |
"finter_raw [] l = []" |
|
51 |
| "finter_raw (h # t) l = |
|
52 |
(if memb h l then h # (finter_raw t l) else finter_raw t l)" |
|
53 |
||
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
54 |
primrec |
36280 | 55 |
delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" |
56 |
where |
|
57 |
"delete_raw [] x = []" |
|
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
58 |
| "delete_raw (a # xs) x = (if (a = x) then delete_raw xs x else a # (delete_raw xs x))" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
59 |
|
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
60 |
primrec |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
61 |
fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
62 |
where |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
63 |
"fminus_raw l [] = l" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
64 |
| "fminus_raw l (h # t) = fminus_raw (delete_raw l h) t" |
36280 | 65 |
|
66 |
definition |
|
67 |
rsp_fold |
|
68 |
where |
|
69 |
"rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))" |
|
70 |
||
71 |
primrec |
|
72 |
ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" |
|
73 |
where |
|
74 |
"ffold_raw f z [] = z" |
|
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
75 |
| "ffold_raw f z (a # xs) = |
36280 | 76 |
(if (rsp_fold f) then |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
77 |
if memb a xs then ffold_raw f z xs |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
78 |
else f a (ffold_raw f z xs) |
36280 | 79 |
else z)" |
80 |
||
81 |
text {* Composition Quotient *} |
|
82 |
||
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
83 |
lemma list_all2_refl: |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
84 |
shows "(list_all2 op \<approx>) r r" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
85 |
by (rule list_all2_refl) (metis equivp_def fset_equivp) |
36280 | 86 |
|
87 |
lemma compose_list_refl: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
88 |
shows "(list_all2 op \<approx> OOO op \<approx>) r r" |
36280 | 89 |
proof |
36465 | 90 |
have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
91 |
show "list_all2 op \<approx> r r" by (rule list_all2_refl) |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
92 |
with * show "(op \<approx> OO list_all2 op \<approx>) r r" .. |
36280 | 93 |
qed |
94 |
||
95 |
lemma Quotient_fset_list: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
96 |
shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)" |
36280 | 97 |
by (fact list_quotient[OF Quotient_fset]) |
98 |
||
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
99 |
lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys" |
36280 | 100 |
by (rule eq_reflection) auto |
101 |
||
102 |
lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
|
103 |
unfolding list_eq.simps |
|
104 |
by (simp only: set_map set_in_eq) |
|
105 |
||
106 |
lemma quotient_compose_list[quot_thm]: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
107 |
shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
36280 | 108 |
(abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
109 |
unfolding Quotient_def comp_def |
|
110 |
proof (intro conjI allI) |
|
111 |
fix a r s |
|
112 |
show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a" |
|
113 |
by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id) |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
114 |
have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
115 |
by (rule list_all2_refl) |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
116 |
have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
36280 | 117 |
by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
118 |
show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
119 |
by (rule, rule list_all2_refl) (rule c) |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
120 |
show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and> |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
121 |
(list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
36280 | 122 |
proof (intro iffI conjI) |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
123 |
show "(list_all2 op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl) |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
124 |
show "(list_all2 op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl) |
36280 | 125 |
next |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
126 |
assume a: "(list_all2 op \<approx> OOO op \<approx>) r s" |
36465 | 127 |
then have b: "map abs_fset r \<approx> map abs_fset s" |
128 |
proof (elim pred_compE) |
|
36280 | 129 |
fix b ba |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
130 |
assume c: "list_all2 op \<approx> r b" |
36280 | 131 |
assume d: "b \<approx> ba" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
132 |
assume e: "list_all2 op \<approx> ba s" |
36280 | 133 |
have f: "map abs_fset r = map abs_fset b" |
134 |
using Quotient_rel[OF Quotient_fset_list] c by blast |
|
135 |
have "map abs_fset ba = map abs_fset s" |
|
136 |
using Quotient_rel[OF Quotient_fset_list] e by blast |
|
137 |
then have g: "map abs_fset s = map abs_fset ba" by simp |
|
138 |
then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp |
|
139 |
qed |
|
140 |
then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
|
141 |
using Quotient_rel[OF Quotient_fset] by blast |
|
142 |
next |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
143 |
assume a: "(list_all2 op \<approx> OOO op \<approx>) r r \<and> (list_all2 op \<approx> OOO op \<approx>) s s |
36280 | 144 |
\<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
145 |
then have s: "(list_all2 op \<approx> OOO op \<approx>) s s" by simp |
36280 | 146 |
have d: "map abs_fset r \<approx> map abs_fset s" |
147 |
by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) |
|
148 |
have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)" |
|
149 |
by (rule map_rel_cong[OF d]) |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
150 |
have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
151 |
by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl[of s]]) |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
152 |
have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s" |
36280 | 153 |
by (rule pred_compI) (rule b, rule y) |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
154 |
have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
155 |
by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl[of r]]) |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
156 |
then show "(list_all2 op \<approx> OOO op \<approx>) r s" |
36280 | 157 |
using a c pred_compI by simp |
158 |
qed |
|
159 |
qed |
|
160 |
||
161 |
text {* Respectfullness *} |
|
162 |
||
163 |
lemma [quot_respect]: |
|
164 |
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
|
165 |
by auto |
|
166 |
||
167 |
lemma [quot_respect]: |
|
168 |
shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
|
169 |
by (auto simp add: sub_list_def) |
|
170 |
||
171 |
lemma memb_rsp[quot_respect]: |
|
172 |
shows "(op = ===> op \<approx> ===> op =) memb memb" |
|
173 |
by (auto simp add: memb_def) |
|
174 |
||
175 |
lemma nil_rsp[quot_respect]: |
|
176 |
shows "[] \<approx> []" |
|
177 |
by simp |
|
178 |
||
179 |
lemma cons_rsp[quot_respect]: |
|
180 |
shows "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
|
181 |
by simp |
|
182 |
||
183 |
lemma map_rsp[quot_respect]: |
|
184 |
shows "(op = ===> op \<approx> ===> op \<approx>) map map" |
|
185 |
by auto |
|
186 |
||
187 |
lemma set_rsp[quot_respect]: |
|
188 |
"(op \<approx> ===> op =) set set" |
|
189 |
by auto |
|
190 |
||
191 |
lemma list_equiv_rsp[quot_respect]: |
|
192 |
shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
|
193 |
by auto |
|
194 |
||
195 |
lemma not_memb_nil: |
|
196 |
shows "\<not> memb x []" |
|
197 |
by (simp add: memb_def) |
|
198 |
||
199 |
lemma memb_cons_iff: |
|
200 |
shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
|
201 |
by (induct xs) (auto simp add: memb_def) |
|
202 |
||
203 |
lemma memb_finter_raw: |
|
204 |
"memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys" |
|
205 |
by (induct xs) (auto simp add: not_memb_nil memb_cons_iff) |
|
206 |
||
207 |
lemma [quot_respect]: |
|
208 |
"(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw" |
|
209 |
by (simp add: memb_def[symmetric] memb_finter_raw) |
|
210 |
||
211 |
lemma memb_delete_raw: |
|
212 |
"memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)" |
|
213 |
by (induct xs arbitrary: x y) (auto simp add: memb_def) |
|
214 |
||
215 |
lemma [quot_respect]: |
|
216 |
"(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw" |
|
217 |
by (simp add: memb_def[symmetric] memb_delete_raw) |
|
218 |
||
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
219 |
lemma fminus_raw_memb: "memb x (fminus_raw xs ys) = (memb x xs \<and> \<not> memb x ys)" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
220 |
by (induct ys arbitrary: xs) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
221 |
(simp_all add: not_memb_nil memb_delete_raw memb_cons_iff) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
222 |
|
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
223 |
lemma [quot_respect]: |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
224 |
"(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
225 |
by (simp add: memb_def[symmetric] fminus_raw_memb) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
226 |
|
36280 | 227 |
lemma fcard_raw_gt_0: |
228 |
assumes a: "x \<in> set xs" |
|
229 |
shows "0 < fcard_raw xs" |
|
230 |
using a by (induct xs) (auto simp add: memb_def) |
|
231 |
||
232 |
lemma fcard_raw_delete_one: |
|
233 |
shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
|
234 |
by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def) |
|
235 |
||
236 |
lemma fcard_raw_rsp_aux: |
|
237 |
assumes a: "xs \<approx> ys" |
|
238 |
shows "fcard_raw xs = fcard_raw ys" |
|
239 |
using a |
|
36465 | 240 |
proof (induct xs arbitrary: ys) |
241 |
case Nil |
|
242 |
show ?case using Nil.prems by simp |
|
243 |
next |
|
244 |
case (Cons a xs) |
|
245 |
have a: "a # xs \<approx> ys" by fact |
|
246 |
have b: "\<And>ys. xs \<approx> ys \<Longrightarrow> fcard_raw xs = fcard_raw ys" by fact |
|
247 |
show ?case proof (cases "a \<in> set xs") |
|
248 |
assume c: "a \<in> set xs" |
|
249 |
have "\<forall>x. (x \<in> set xs) = (x \<in> set ys)" |
|
250 |
proof (intro allI iffI) |
|
251 |
fix x |
|
252 |
assume "x \<in> set xs" |
|
253 |
then show "x \<in> set ys" using a by auto |
|
254 |
next |
|
255 |
fix x |
|
256 |
assume d: "x \<in> set ys" |
|
257 |
have e: "(x \<in> set (a # xs)) = (x \<in> set ys)" using a by simp |
|
258 |
show "x \<in> set xs" using c d e unfolding list_eq.simps by simp blast |
|
259 |
qed |
|
260 |
then show ?thesis using b c by (simp add: memb_def) |
|
261 |
next |
|
262 |
assume c: "a \<notin> set xs" |
|
263 |
have d: "xs \<approx> [x\<leftarrow>ys . x \<noteq> a] \<Longrightarrow> fcard_raw xs = fcard_raw [x\<leftarrow>ys . x \<noteq> a]" using b by simp |
|
264 |
have "Suc (fcard_raw xs) = fcard_raw ys" |
|
265 |
proof (cases "a \<in> set ys") |
|
266 |
assume e: "a \<in> set ys" |
|
267 |
have f: "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)" using a c |
|
268 |
by (auto simp add: fcard_raw_delete_one) |
|
269 |
have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e) |
|
270 |
then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def) |
|
271 |
next |
|
272 |
case False then show ?thesis using a c d by auto |
|
273 |
qed |
|
274 |
then show ?thesis using a c d by (simp add: memb_def) |
|
275 |
qed |
|
276 |
qed |
|
36280 | 277 |
|
278 |
lemma fcard_raw_rsp[quot_respect]: |
|
279 |
shows "(op \<approx> ===> op =) fcard_raw fcard_raw" |
|
280 |
by (simp add: fcard_raw_rsp_aux) |
|
281 |
||
282 |
lemma memb_absorb: |
|
283 |
shows "memb x xs \<Longrightarrow> x # xs \<approx> xs" |
|
284 |
by (induct xs) (auto simp add: memb_def) |
|
285 |
||
286 |
lemma none_memb_nil: |
|
287 |
"(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
|
288 |
by (simp add: memb_def) |
|
289 |
||
290 |
lemma not_memb_delete_raw_ident: |
|
291 |
shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs" |
|
292 |
by (induct xs) (auto simp add: memb_def) |
|
293 |
||
294 |
lemma memb_commute_ffold_raw: |
|
295 |
"rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))" |
|
296 |
apply (induct b) |
|
297 |
apply (simp_all add: not_memb_nil) |
|
298 |
apply (auto) |
|
299 |
apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff) |
|
300 |
done |
|
301 |
||
302 |
lemma ffold_raw_rsp_pre: |
|
303 |
"\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b" |
|
304 |
apply (induct a arbitrary: b) |
|
305 |
apply (simp add: memb_absorb memb_def none_memb_nil) |
|
306 |
apply (simp) |
|
307 |
apply (rule conjI) |
|
308 |
apply (rule_tac [!] impI) |
|
309 |
apply (rule_tac [!] conjI) |
|
310 |
apply (rule_tac [!] impI) |
|
311 |
apply (subgoal_tac "\<forall>e. memb e a2 = memb e b") |
|
312 |
apply (simp) |
|
313 |
apply (simp add: memb_cons_iff memb_def) |
|
314 |
apply (auto)[1] |
|
315 |
apply (drule_tac x="e" in spec) |
|
316 |
apply (blast) |
|
317 |
apply (case_tac b) |
|
318 |
apply (simp_all) |
|
319 |
apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
|
320 |
apply (simp only:) |
|
321 |
apply (rule_tac f="f a1" in arg_cong) |
|
322 |
apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
|
323 |
apply (simp) |
|
324 |
apply (simp add: memb_delete_raw) |
|
325 |
apply (auto simp add: memb_cons_iff)[1] |
|
326 |
apply (erule memb_commute_ffold_raw) |
|
327 |
apply (drule_tac x="a1" in spec) |
|
328 |
apply (simp add: memb_cons_iff) |
|
329 |
apply (simp add: memb_cons_iff) |
|
330 |
apply (case_tac b) |
|
331 |
apply (simp_all) |
|
332 |
done |
|
333 |
||
334 |
lemma [quot_respect]: |
|
335 |
"(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
|
336 |
by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
|
337 |
||
338 |
lemma concat_rsp_pre: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
339 |
assumes a: "list_all2 op \<approx> x x'" |
36280 | 340 |
and b: "x' \<approx> y'" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
341 |
and c: "list_all2 op \<approx> y' y" |
36280 | 342 |
and d: "\<exists>x\<in>set x. xa \<in> set x" |
343 |
shows "\<exists>x\<in>set y. xa \<in> set x" |
|
344 |
proof - |
|
345 |
obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
346 |
have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a]) |
36280 | 347 |
then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto |
36465 | 348 |
have "ya \<in> set y'" using b h by simp |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
349 |
then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element) |
36280 | 350 |
then show ?thesis using f i by auto |
351 |
qed |
|
352 |
||
353 |
lemma [quot_respect]: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
354 |
shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
36280 | 355 |
proof (rule fun_relI, elim pred_compE) |
356 |
fix a b ba bb |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
357 |
assume a: "list_all2 op \<approx> a ba" |
36280 | 358 |
assume b: "ba \<approx> bb" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
359 |
assume c: "list_all2 op \<approx> bb b" |
36280 | 360 |
have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
361 |
fix x |
|
362 |
show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
363 |
assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
|
364 |
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
365 |
next |
|
366 |
assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
367 |
have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a]) |
36280 | 368 |
have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
369 |
have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c]) |
36280 | 370 |
show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
371 |
qed |
|
372 |
qed |
|
373 |
then show "concat a \<approx> concat b" by simp |
|
374 |
qed |
|
375 |
||
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
376 |
lemma [quot_respect]: |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
377 |
"((op =) ===> op \<approx> ===> op \<approx>) filter filter" |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
378 |
by auto |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
379 |
|
36280 | 380 |
text {* Distributive lattice with bot *} |
381 |
||
382 |
lemma append_inter_distrib: |
|
383 |
"x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)" |
|
384 |
apply (induct x) |
|
385 |
apply (simp_all add: memb_def) |
|
386 |
apply (simp add: memb_def[symmetric] memb_finter_raw) |
|
36465 | 387 |
apply (auto simp add: memb_def) |
388 |
done |
|
36280 | 389 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
390 |
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" |
36280 | 391 |
begin |
392 |
||
393 |
quotient_definition |
|
394 |
"bot :: 'a fset" is "[] :: 'a list" |
|
395 |
||
396 |
abbreviation |
|
397 |
fempty ("{||}") |
|
398 |
where |
|
399 |
"{||} \<equiv> bot :: 'a fset" |
|
400 |
||
401 |
quotient_definition |
|
402 |
"less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)" |
|
403 |
is |
|
404 |
"sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" |
|
405 |
||
406 |
abbreviation |
|
407 |
f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) |
|
408 |
where |
|
409 |
"xs |\<subseteq>| ys \<equiv> xs \<le> ys" |
|
410 |
||
411 |
definition |
|
412 |
less_fset: |
|
413 |
"(xs :: 'a fset) < ys \<equiv> xs \<le> ys \<and> xs \<noteq> ys" |
|
414 |
||
415 |
abbreviation |
|
416 |
f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) |
|
417 |
where |
|
418 |
"xs |\<subset>| ys \<equiv> xs < ys" |
|
419 |
||
420 |
quotient_definition |
|
421 |
"sup \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)" |
|
422 |
is |
|
423 |
"(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
|
424 |
||
425 |
abbreviation |
|
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
426 |
funion (infixl "|\<union>|" 65) |
36280 | 427 |
where |
428 |
"xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys" |
|
429 |
||
430 |
quotient_definition |
|
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
431 |
"inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)" |
36280 | 432 |
is |
433 |
"finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
|
434 |
||
435 |
abbreviation |
|
436 |
finter (infixl "|\<inter>|" 65) |
|
437 |
where |
|
438 |
"xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys" |
|
439 |
||
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
440 |
quotient_definition |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
441 |
"minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
442 |
is |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
443 |
"fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
444 |
|
36280 | 445 |
instance |
446 |
proof |
|
447 |
fix x y z :: "'a fset" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
448 |
show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
449 |
unfolding less_fset |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
450 |
by (descending) (auto simp add: sub_list_def) |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
451 |
show "x |\<subseteq>| x" by (descending) (simp add: sub_list_def) |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
452 |
show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def) |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
453 |
show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def) |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
454 |
show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def) |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
455 |
show "x |\<inter>| y |\<subseteq>| x" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
456 |
by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
457 |
show "x |\<inter>| y |\<subseteq>| y" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
458 |
by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
459 |
show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
460 |
by (descending) (rule append_inter_distrib) |
36280 | 461 |
next |
462 |
fix x y z :: "'a fset" |
|
463 |
assume a: "x |\<subseteq>| y" |
|
464 |
assume b: "y |\<subseteq>| z" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
465 |
show "x |\<subseteq>| z" using a b |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
466 |
by (descending) (simp add: sub_list_def) |
36280 | 467 |
next |
468 |
fix x y :: "'a fset" |
|
469 |
assume a: "x |\<subseteq>| y" |
|
470 |
assume b: "y |\<subseteq>| x" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
471 |
show "x = y" using a b |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
472 |
by (descending) (unfold sub_list_def list_eq.simps, blast) |
36280 | 473 |
next |
474 |
fix x y z :: "'a fset" |
|
475 |
assume a: "y |\<subseteq>| x" |
|
476 |
assume b: "z |\<subseteq>| x" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
477 |
show "y |\<union>| z |\<subseteq>| x" using a b |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
478 |
by (descending) (simp add: sub_list_def) |
36280 | 479 |
next |
480 |
fix x y z :: "'a fset" |
|
481 |
assume a: "x |\<subseteq>| y" |
|
482 |
assume b: "x |\<subseteq>| z" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
483 |
show "x |\<subseteq>| y |\<inter>| z" using a b |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
484 |
by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) |
36280 | 485 |
qed |
486 |
||
487 |
end |
|
488 |
||
489 |
section {* Finsert and Membership *} |
|
490 |
||
491 |
quotient_definition |
|
492 |
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
493 |
is "op #" |
|
494 |
||
495 |
syntax |
|
496 |
"@Finset" :: "args => 'a fset" ("{|(_)|}") |
|
497 |
||
498 |
translations |
|
499 |
"{|x, xs|}" == "CONST finsert x {|xs|}" |
|
500 |
"{|x|}" == "CONST finsert x {||}" |
|
501 |
||
502 |
quotient_definition |
|
503 |
fin (infix "|\<in>|" 50) |
|
504 |
where |
|
505 |
"fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
|
506 |
||
507 |
abbreviation |
|
508 |
fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) |
|
509 |
where |
|
510 |
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
|
511 |
||
36465 | 512 |
section {* Other constants on the Quotient Type *} |
36280 | 513 |
|
514 |
quotient_definition |
|
36465 | 515 |
"fcard :: 'a fset \<Rightarrow> nat" |
36280 | 516 |
is |
517 |
"fcard_raw" |
|
518 |
||
519 |
quotient_definition |
|
520 |
"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
|
521 |
is |
|
522 |
"map" |
|
523 |
||
524 |
quotient_definition |
|
36465 | 525 |
"fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
36280 | 526 |
is "delete_raw" |
527 |
||
528 |
quotient_definition |
|
36465 | 529 |
"fset_to_set :: 'a fset \<Rightarrow> 'a set" |
36280 | 530 |
is "set" |
531 |
||
532 |
quotient_definition |
|
533 |
"ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
|
534 |
is "ffold_raw" |
|
535 |
||
536 |
quotient_definition |
|
537 |
"fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
|
538 |
is |
|
539 |
"concat" |
|
540 |
||
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
541 |
quotient_definition |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
542 |
"ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
543 |
is |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
544 |
"filter" |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
545 |
|
36280 | 546 |
text {* Compositional Respectfullness and Preservation *} |
547 |
||
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
548 |
lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []" |
36280 | 549 |
by (fact compose_list_refl) |
550 |
||
551 |
lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []" |
|
552 |
by simp |
|
553 |
||
554 |
lemma [quot_respect]: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
555 |
"(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op # op #" |
36280 | 556 |
apply auto |
557 |
apply (simp add: set_in_eq) |
|
558 |
apply (rule_tac b="x # b" in pred_compI) |
|
559 |
apply auto |
|
560 |
apply (rule_tac b="x # ba" in pred_compI) |
|
561 |
apply auto |
|
562 |
done |
|
563 |
||
564 |
lemma [quot_preserve]: |
|
565 |
"(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
566 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset] |
36280 | 567 |
abs_o_rep[OF Quotient_fset] map_id finsert_def) |
568 |
||
569 |
lemma [quot_preserve]: |
|
570 |
"((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
571 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset] |
36280 | 572 |
abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
573 |
||
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
574 |
lemma list_all2_app_l: |
36280 | 575 |
assumes a: "reflp R" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
576 |
and b: "list_all2 R l r" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
577 |
shows "list_all2 R (z @ l) (z @ r)" |
36280 | 578 |
by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]]) |
579 |
||
580 |
lemma append_rsp2_pre0: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
581 |
assumes a:"list_all2 op \<approx> x x'" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
582 |
shows "list_all2 op \<approx> (x @ z) (x' @ z)" |
36280 | 583 |
using a apply (induct x x' rule: list_induct2') |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
584 |
by simp_all (rule list_all2_refl) |
36280 | 585 |
|
586 |
lemma append_rsp2_pre1: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
587 |
assumes a:"list_all2 op \<approx> x x'" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
588 |
shows "list_all2 op \<approx> (z @ x) (z @ x')" |
36280 | 589 |
using a apply (induct x x' arbitrary: z rule: list_induct2') |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
590 |
apply (rule list_all2_refl) |
36280 | 591 |
apply (simp_all del: list_eq.simps) |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
592 |
apply (rule list_all2_app_l) |
36280 | 593 |
apply (simp_all add: reflp_def) |
594 |
done |
|
595 |
||
596 |
lemma append_rsp2_pre: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
597 |
assumes a:"list_all2 op \<approx> x x'" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
598 |
and b: "list_all2 op \<approx> z z'" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
599 |
shows "list_all2 op \<approx> (x @ z) (x' @ z')" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
600 |
apply (rule list_all2_transp[OF fset_equivp]) |
36280 | 601 |
apply (rule append_rsp2_pre0) |
602 |
apply (rule a) |
|
603 |
using b apply (induct z z' rule: list_induct2') |
|
604 |
apply (simp_all only: append_Nil2) |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
605 |
apply (rule list_all2_refl) |
36280 | 606 |
apply simp_all |
607 |
apply (rule append_rsp2_pre1) |
|
608 |
apply simp |
|
609 |
done |
|
610 |
||
611 |
lemma [quot_respect]: |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
612 |
"(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op @ op @" |
36280 | 613 |
proof (intro fun_relI, elim pred_compE) |
614 |
fix x y z w x' z' y' w' :: "'a list list" |
|
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
615 |
assume a:"list_all2 op \<approx> x x'" |
36280 | 616 |
and b: "x' \<approx> y'" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
617 |
and c: "list_all2 op \<approx> y' y" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
618 |
assume aa: "list_all2 op \<approx> z z'" |
36280 | 619 |
and bb: "z' \<approx> w'" |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
620 |
and cc: "list_all2 op \<approx> w' w" |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
621 |
have a': "list_all2 op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto |
36280 | 622 |
have b': "x' @ z' \<approx> y' @ w'" using b bb by simp |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
623 |
have c': "list_all2 op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto |
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
624 |
have d': "(op \<approx> OO list_all2 op \<approx>) (x' @ z') (y @ w)" |
36280 | 625 |
by (rule pred_compI) (rule b', rule c') |
37492
ab36b1a50ca8
Replace 'list_rel' by 'list_all2'; they are equivalent.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36675
diff
changeset
|
626 |
show "(list_all2 op \<approx> OOO op \<approx>) (x @ z) (y @ w)" |
36280 | 627 |
by (rule pred_compI) (rule a', rule d') |
628 |
qed |
|
629 |
||
630 |
text {* Raw theorems. Finsert, memb, singleron, sub_list *} |
|
631 |
||
632 |
lemma nil_not_cons: |
|
633 |
shows "\<not> ([] \<approx> x # xs)" |
|
634 |
and "\<not> (x # xs \<approx> [])" |
|
635 |
by auto |
|
636 |
||
637 |
lemma no_memb_nil: |
|
638 |
"(\<forall>x. \<not> memb x xs) = (xs = [])" |
|
639 |
by (simp add: memb_def) |
|
640 |
||
641 |
lemma memb_consI1: |
|
642 |
shows "memb x (x # xs)" |
|
643 |
by (simp add: memb_def) |
|
644 |
||
645 |
lemma memb_consI2: |
|
646 |
shows "memb x xs \<Longrightarrow> memb x (y # xs)" |
|
647 |
by (simp add: memb_def) |
|
648 |
||
649 |
lemma singleton_list_eq: |
|
650 |
shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
|
651 |
by (simp add: id_simps) auto |
|
652 |
||
653 |
lemma sub_list_cons: |
|
654 |
"sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
|
655 |
by (auto simp add: memb_def sub_list_def) |
|
656 |
||
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
657 |
lemma fminus_raw_red: "fminus_raw (x # xs) ys = (if memb x ys then fminus_raw xs ys else x # (fminus_raw xs ys))" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
658 |
by (induct ys arbitrary: xs x) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
659 |
(simp_all add: not_memb_nil memb_delete_raw memb_cons_iff) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
660 |
|
36280 | 661 |
text {* Cardinality of finite sets *} |
662 |
||
663 |
lemma fcard_raw_0: |
|
664 |
shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []" |
|
665 |
by (induct xs) (auto simp add: memb_def) |
|
666 |
||
667 |
lemma fcard_raw_not_memb: |
|
668 |
shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)" |
|
669 |
by auto |
|
670 |
||
671 |
lemma fcard_raw_suc: |
|
672 |
assumes a: "fcard_raw xs = Suc n" |
|
673 |
shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n" |
|
674 |
using a |
|
675 |
by (induct xs) (auto simp add: memb_def split: if_splits) |
|
676 |
||
677 |
lemma singleton_fcard_1: |
|
678 |
shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1" |
|
679 |
by (induct xs) (auto simp add: memb_def subset_insert) |
|
680 |
||
681 |
lemma fcard_raw_1: |
|
682 |
shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])" |
|
683 |
apply (auto dest!: fcard_raw_suc) |
|
684 |
apply (simp add: fcard_raw_0) |
|
685 |
apply (rule_tac x="x" in exI) |
|
686 |
apply simp |
|
687 |
apply (subgoal_tac "set xs = {x}") |
|
688 |
apply (drule singleton_fcard_1) |
|
689 |
apply auto |
|
690 |
done |
|
691 |
||
692 |
lemma fcard_raw_suc_memb: |
|
693 |
assumes a: "fcard_raw A = Suc n" |
|
694 |
shows "\<exists>a. memb a A" |
|
695 |
using a |
|
696 |
by (induct A) (auto simp add: memb_def) |
|
697 |
||
698 |
lemma memb_card_not_0: |
|
699 |
assumes a: "memb a A" |
|
700 |
shows "\<not>(fcard_raw A = 0)" |
|
701 |
proof - |
|
702 |
have "\<not>(\<forall>x. \<not> memb x A)" using a by auto |
|
703 |
then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp |
|
704 |
then show ?thesis using fcard_raw_0[of A] by simp |
|
705 |
qed |
|
706 |
||
707 |
text {* fmap *} |
|
708 |
||
709 |
lemma map_append: |
|
710 |
"map f (xs @ ys) \<approx> (map f xs) @ (map f ys)" |
|
711 |
by simp |
|
712 |
||
713 |
lemma memb_append: |
|
714 |
"memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys" |
|
715 |
by (induct xs) (simp_all add: not_memb_nil memb_cons_iff) |
|
716 |
||
717 |
lemma fset_raw_strong_cases: |
|
36465 | 718 |
obtains "xs = []" |
719 |
| x ys where "\<not> memb x ys" and "xs \<approx> x # ys" |
|
720 |
proof (induct xs arbitrary: x ys) |
|
721 |
case Nil |
|
722 |
then show thesis by simp |
|
723 |
next |
|
724 |
case (Cons a xs) |
|
725 |
have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact |
|
726 |
have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact |
|
727 |
have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b) |
|
728 |
have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis" |
|
729 |
proof - |
|
730 |
fix x :: 'a |
|
731 |
fix ys :: "'a list" |
|
732 |
assume d:"\<not> memb x ys" |
|
733 |
assume e:"xs \<approx> x # ys" |
|
734 |
show thesis |
|
735 |
proof (cases "x = a") |
|
736 |
assume h: "x = a" |
|
737 |
then have f: "\<not> memb a ys" using d by simp |
|
738 |
have g: "a # xs \<approx> a # ys" using e h by auto |
|
739 |
show thesis using b f g by simp |
|
740 |
next |
|
741 |
assume h: "x \<noteq> a" |
|
742 |
then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto |
|
743 |
have g: "a # xs \<approx> x # (a # ys)" using e h by auto |
|
744 |
show thesis using b f g by simp |
|
745 |
qed |
|
746 |
qed |
|
747 |
then show thesis using a c by blast |
|
748 |
qed |
|
36280 | 749 |
|
750 |
section {* deletion *} |
|
751 |
||
752 |
lemma memb_delete_raw_ident: |
|
753 |
shows "\<not> memb x (delete_raw xs x)" |
|
754 |
by (induct xs) (auto simp add: memb_def) |
|
755 |
||
756 |
lemma fset_raw_delete_raw_cases: |
|
757 |
"xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)" |
|
758 |
by (induct xs) (auto simp add: memb_def) |
|
759 |
||
760 |
lemma fdelete_raw_filter: |
|
761 |
"delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]" |
|
762 |
by (induct xs) simp_all |
|
763 |
||
764 |
lemma fcard_raw_delete: |
|
765 |
"fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
|
766 |
by (simp add: fdelete_raw_filter fcard_raw_delete_one) |
|
767 |
||
36465 | 768 |
lemma set_cong: |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
769 |
shows "(x \<approx> y) = (set x = set y)" |
36280 | 770 |
by auto |
771 |
||
772 |
lemma inj_map_eq_iff: |
|
773 |
"inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
774 |
by (simp add: set_eq_iff[symmetric] inj_image_eq_iff) |
36280 | 775 |
|
776 |
text {* alternate formulation with a different decomposition principle |
|
777 |
and a proof of equivalence *} |
|
778 |
||
779 |
inductive |
|
780 |
list_eq2 |
|
781 |
where |
|
782 |
"list_eq2 (a # b # xs) (b # a # xs)" |
|
783 |
| "list_eq2 [] []" |
|
784 |
| "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs" |
|
785 |
| "list_eq2 (a # a # xs) (a # xs)" |
|
786 |
| "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)" |
|
787 |
| "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3" |
|
788 |
||
789 |
lemma list_eq2_refl: |
|
790 |
shows "list_eq2 xs xs" |
|
791 |
by (induct xs) (auto intro: list_eq2.intros) |
|
792 |
||
793 |
lemma cons_delete_list_eq2: |
|
794 |
shows "list_eq2 (a # (delete_raw A a)) (if memb a A then A else a # A)" |
|
795 |
apply (induct A) |
|
796 |
apply (simp add: memb_def list_eq2_refl) |
|
797 |
apply (case_tac "memb a (aa # A)") |
|
798 |
apply (simp_all only: memb_cons_iff) |
|
799 |
apply (case_tac [!] "a = aa") |
|
800 |
apply (simp_all) |
|
801 |
apply (case_tac "memb a A") |
|
802 |
apply (auto simp add: memb_def)[2] |
|
803 |
apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
|
804 |
apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) |
|
805 |
apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident) |
|
806 |
done |
|
807 |
||
808 |
lemma memb_delete_list_eq2: |
|
809 |
assumes a: "memb e r" |
|
810 |
shows "list_eq2 (e # delete_raw r e) r" |
|
811 |
using a cons_delete_list_eq2[of e r] |
|
812 |
by simp |
|
813 |
||
814 |
lemma delete_raw_rsp: |
|
815 |
"xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x" |
|
816 |
by (simp add: memb_def[symmetric] memb_delete_raw) |
|
817 |
||
818 |
lemma list_eq2_equiv: |
|
819 |
"(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)" |
|
820 |
proof |
|
821 |
show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto |
|
822 |
next |
|
823 |
{ |
|
824 |
fix n |
|
825 |
assume a: "fcard_raw l = n" and b: "l \<approx> r" |
|
826 |
have "list_eq2 l r" |
|
827 |
using a b |
|
828 |
proof (induct n arbitrary: l r) |
|
829 |
case 0 |
|
830 |
have "fcard_raw l = 0" by fact |
|
831 |
then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
|
832 |
then have z: "l = []" using no_memb_nil by auto |
|
833 |
then have "r = []" using `l \<approx> r` by simp |
|
834 |
then show ?case using z list_eq2_refl by simp |
|
835 |
next |
|
836 |
case (Suc m) |
|
837 |
have b: "l \<approx> r" by fact |
|
838 |
have d: "fcard_raw l = Suc m" by fact |
|
36465 | 839 |
then have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb) |
36280 | 840 |
then obtain a where e: "memb a l" by auto |
841 |
then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto |
|
842 |
have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp |
|
843 |
have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp |
|
36465 | 844 |
have "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g]) |
845 |
then have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)) |
|
36280 | 846 |
have i: "list_eq2 l (a # delete_raw l a)" |
847 |
by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]]) |
|
848 |
have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h]) |
|
849 |
then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp |
|
850 |
qed |
|
851 |
} |
|
852 |
then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast |
|
853 |
qed |
|
854 |
||
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
855 |
text {* Set *} |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
856 |
|
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
857 |
lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)" |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
858 |
unfolding sub_list_def by auto |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
859 |
|
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
860 |
lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)" |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
861 |
by (auto simp add: sub_list_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
862 |
|
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
863 |
lemma fcard_raw_set: "fcard_raw xs = card (set xs)" |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
864 |
by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
865 |
|
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
866 |
lemma memb_set: "memb x xs = (x \<in> set xs)" |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
867 |
by (simp only: memb_def) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
868 |
|
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
869 |
lemma filter_set: "set (filter P xs) = P \<inter> (set xs)" |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
870 |
by (induct xs, simp) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
871 |
(metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
872 |
|
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
873 |
lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}" |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
874 |
by (induct xs) auto |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
875 |
|
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
876 |
lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys" |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
877 |
by (induct xs) (simp_all add: memb_def) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
878 |
|
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
879 |
lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
880 |
by (induct ys arbitrary: xs) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
881 |
(simp_all add: fminus_raw.simps delete_raw_set, blast) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
882 |
|
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
883 |
text {* Raw theorems of ffilter *} |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
884 |
|
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
885 |
lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)" |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
886 |
unfolding sub_list_def memb_def by auto |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
887 |
|
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
888 |
lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)" |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
889 |
unfolding memb_def by auto |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
890 |
|
36280 | 891 |
text {* Lifted theorems *} |
892 |
||
893 |
lemma not_fin_fnil: "x |\<notin>| {||}" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
894 |
by (descending) (simp add: memb_def) |
36280 | 895 |
|
896 |
lemma fin_finsert_iff[simp]: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
897 |
"x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
898 |
by (descending) (simp add: memb_def) |
36280 | 899 |
|
900 |
lemma |
|
901 |
shows finsertI1: "x |\<in>| finsert x S" |
|
902 |
and finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
903 |
by (lifting memb_consI1 memb_consI2) |
36280 | 904 |
|
905 |
lemma finsert_absorb[simp]: |
|
906 |
shows "x |\<in>| S \<Longrightarrow> finsert x S = S" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
907 |
by (descending) (auto simp add: memb_def) |
36280 | 908 |
|
909 |
lemma fempty_not_finsert[simp]: |
|
910 |
"{||} \<noteq> finsert x S" |
|
911 |
"finsert x S \<noteq> {||}" |
|
912 |
by (lifting nil_not_cons) |
|
913 |
||
914 |
lemma finsert_left_comm: |
|
915 |
"finsert x (finsert y S) = finsert y (finsert x S)" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
916 |
by (descending) (auto) |
36280 | 917 |
|
918 |
lemma finsert_left_idem: |
|
919 |
"finsert x (finsert x S) = finsert x S" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
920 |
by (descending) (auto) |
36280 | 921 |
|
922 |
lemma fsingleton_eq[simp]: |
|
923 |
shows "{|x|} = {|y|} \<longleftrightarrow> x = y" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
924 |
by (descending) (auto) |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
925 |
|
36280 | 926 |
|
927 |
text {* fset_to_set *} |
|
928 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
929 |
lemma fset_to_set_simps [simp]: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
930 |
fixes h::"'a" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
931 |
shows "fset_to_set {||} = ({} :: 'a set)" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
932 |
and "fset_to_set (finsert h t) = insert h (fset_to_set t)" |
36280 | 933 |
by (lifting set.simps) |
934 |
||
935 |
lemma in_fset_to_set: |
|
936 |
"x \<in> fset_to_set S \<equiv> x |\<in>| S" |
|
937 |
by (lifting memb_def[symmetric]) |
|
938 |
||
939 |
lemma none_fin_fempty: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
940 |
"(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}" |
36280 | 941 |
by (lifting none_memb_nil) |
942 |
||
943 |
lemma fset_cong: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
944 |
"S = T \<longleftrightarrow> fset_to_set S = fset_to_set T" |
36280 | 945 |
by (lifting set_cong) |
946 |
||
947 |
text {* fcard *} |
|
948 |
||
949 |
lemma fcard_fempty [simp]: |
|
950 |
shows "fcard {||} = 0" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
951 |
by (descending) (simp) |
36280 | 952 |
|
953 |
lemma fcard_finsert_if [simp]: |
|
954 |
shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))" |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
955 |
by (descending) (simp) |
36280 | 956 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
957 |
lemma fcard_0: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
958 |
"fcard S = 0 \<longleftrightarrow> S = {||}" |
36280 | 959 |
by (lifting fcard_raw_0) |
960 |
||
961 |
lemma fcard_1: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
962 |
shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})" |
36280 | 963 |
by (lifting fcard_raw_1) |
964 |
||
36465 | 965 |
lemma fcard_gt_0: |
36280 | 966 |
shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S" |
967 |
by (lifting fcard_raw_gt_0) |
|
968 |
||
36465 | 969 |
lemma fcard_not_fin: |
36280 | 970 |
shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))" |
971 |
by (lifting fcard_raw_not_memb) |
|
972 |
||
973 |
lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n" |
|
974 |
by (lifting fcard_raw_suc) |
|
975 |
||
976 |
lemma fcard_delete: |
|
977 |
"fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)" |
|
978 |
by (lifting fcard_raw_delete) |
|
979 |
||
980 |
lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A" |
|
981 |
by (lifting fcard_raw_suc_memb) |
|
982 |
||
983 |
lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0" |
|
984 |
by (lifting memb_card_not_0) |
|
985 |
||
986 |
text {* funion *} |
|
987 |
||
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36280
diff
changeset
|
988 |
lemmas [simp] = |
36465 | 989 |
sup_bot_left[where 'a="'a fset", standard] |
990 |
sup_bot_right[where 'a="'a fset", standard] |
|
36280 | 991 |
|
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36280
diff
changeset
|
992 |
lemma funion_finsert[simp]: |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36280
diff
changeset
|
993 |
shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)" |
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36280
diff
changeset
|
994 |
by (lifting append.simps(2)) |
36280 | 995 |
|
996 |
lemma singleton_union_left: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
997 |
shows "{|a|} |\<union>| S = finsert a S" |
36280 | 998 |
by simp |
999 |
||
1000 |
lemma singleton_union_right: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1001 |
shows "S |\<union>| {|a|} = finsert a S" |
36280 | 1002 |
by (subst sup.commute) simp |
1003 |
||
1004 |
section {* Induction and Cases rules for finite sets *} |
|
1005 |
||
1006 |
lemma fset_strong_cases: |
|
36465 | 1007 |
obtains "xs = {||}" |
1008 |
| x ys where "x |\<notin>| ys" and "xs = finsert x ys" |
|
36280 | 1009 |
by (lifting fset_raw_strong_cases) |
1010 |
||
1011 |
lemma fset_exhaust[case_names fempty finsert, cases type: fset]: |
|
1012 |
shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
|
1013 |
by (lifting list.exhaust) |
|
1014 |
||
1015 |
lemma fset_induct_weak[case_names fempty finsert]: |
|
1016 |
shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S" |
|
1017 |
by (lifting list.induct) |
|
1018 |
||
1019 |
lemma fset_induct[case_names fempty finsert, induct type: fset]: |
|
36465 | 1020 |
assumes prem1: "P {||}" |
36280 | 1021 |
and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" |
1022 |
shows "P S" |
|
1023 |
proof(induct S rule: fset_induct_weak) |
|
1024 |
case fempty |
|
1025 |
show "P {||}" by (rule prem1) |
|
1026 |
next |
|
1027 |
case (finsert x S) |
|
1028 |
have asm: "P S" by fact |
|
1029 |
show "P (finsert x S)" |
|
1030 |
by (cases "x |\<in>| S") (simp_all add: asm prem2) |
|
1031 |
qed |
|
1032 |
||
1033 |
lemma fset_induct2: |
|
1034 |
"P {||} {||} \<Longrightarrow> |
|
1035 |
(\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow> |
|
1036 |
(\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow> |
|
1037 |
(\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow> |
|
1038 |
P xsa ysa" |
|
1039 |
apply (induct xsa arbitrary: ysa) |
|
1040 |
apply (induct_tac x rule: fset_induct) |
|
1041 |
apply simp_all |
|
1042 |
apply (induct_tac xa rule: fset_induct) |
|
1043 |
apply simp_all |
|
1044 |
done |
|
1045 |
||
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1046 |
lemma fset_fcard_induct: |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1047 |
assumes a: "P {||}" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1048 |
and b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1049 |
shows "P zs" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1050 |
proof (induct zs) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1051 |
show "P {||}" by (rule a) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1052 |
next |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1053 |
fix x :: 'a and zs :: "'a fset" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1054 |
assume h: "P zs" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1055 |
assume "x |\<notin>| zs" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1056 |
then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1057 |
then show "P (finsert x zs)" using b h by simp |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1058 |
qed |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1059 |
|
36280 | 1060 |
text {* fmap *} |
1061 |
||
1062 |
lemma fmap_simps[simp]: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1063 |
fixes f::"'a \<Rightarrow> 'b" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1064 |
shows "fmap f {||} = {||}" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1065 |
and "fmap f (finsert x S) = finsert (f x) (fmap f S)" |
36280 | 1066 |
by (lifting map.simps) |
1067 |
||
1068 |
lemma fmap_set_image: |
|
1069 |
"fset_to_set (fmap f S) = f ` (fset_to_set S)" |
|
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1070 |
by (induct S) simp_all |
36280 | 1071 |
|
1072 |
lemma inj_fmap_eq_iff: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1073 |
"inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T" |
36280 | 1074 |
by (lifting inj_map_eq_iff) |
1075 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1076 |
lemma fmap_funion: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1077 |
shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T" |
36280 | 1078 |
by (lifting map_append) |
1079 |
||
1080 |
lemma fin_funion: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1081 |
shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T" |
36280 | 1082 |
by (lifting memb_append) |
1083 |
||
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1084 |
text {* to_set *} |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1085 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1086 |
lemma fin_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1087 |
shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset_to_set xs" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1088 |
by (lifting memb_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1089 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1090 |
lemma fnotin_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1091 |
shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset_to_set xs" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1092 |
by (simp add: fin_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1093 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1094 |
lemma fcard_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1095 |
shows "fcard xs = card (fset_to_set xs)" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1096 |
by (lifting fcard_raw_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1097 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1098 |
lemma fsubseteq_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1099 |
shows "xs |\<subseteq>| ys \<longleftrightarrow> fset_to_set xs \<subseteq> fset_to_set ys" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1100 |
by (lifting sub_list_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1101 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1102 |
lemma fsubset_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1103 |
shows "xs |\<subset>| ys \<longleftrightarrow> fset_to_set xs \<subset> fset_to_set ys" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1104 |
unfolding less_fset by (lifting sub_list_neq_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1105 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1106 |
lemma ffilter_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1107 |
shows "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1108 |
by (lifting filter_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1109 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1110 |
lemma fdelete_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1111 |
shows "fset_to_set (fdelete xs x) = fset_to_set xs - {x}" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1112 |
by (lifting delete_raw_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1113 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1114 |
lemma finter_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1115 |
shows "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1116 |
by (lifting inter_raw_set) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1117 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1118 |
lemma funion_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1119 |
shows "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1120 |
by (lifting set_append) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1121 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1122 |
lemma fminus_set: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1123 |
shows "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1124 |
by (lifting fminus_raw_set) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1125 |
|
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1126 |
lemmas fset_to_set_trans = |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1127 |
fin_set fnotin_set fcard_set fsubseteq_set fsubset_set |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1128 |
finter_set funion_set ffilter_set fset_to_set_simps |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1129 |
fset_cong fdelete_set fmap_set_image fminus_set |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1130 |
|
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1131 |
|
36280 | 1132 |
text {* ffold *} |
1133 |
||
1134 |
lemma ffold_nil: "ffold f z {||} = z" |
|
1135 |
by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"]) |
|
1136 |
||
1137 |
lemma ffold_finsert: "ffold f z (finsert a A) = |
|
1138 |
(if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)" |
|
1139 |
by (lifting ffold_raw.simps(2)[where 'a="'b" and 'b="'a"]) |
|
1140 |
||
1141 |
lemma fin_commute_ffold: |
|
1142 |
"\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete b h))" |
|
1143 |
by (lifting memb_commute_ffold_raw) |
|
1144 |
||
1145 |
text {* fdelete *} |
|
1146 |
||
36465 | 1147 |
lemma fin_fdelete: |
36280 | 1148 |
shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y" |
1149 |
by (lifting memb_delete_raw) |
|
1150 |
||
36465 | 1151 |
lemma fin_fdelete_ident: |
36280 | 1152 |
shows "x |\<notin>| fdelete S x" |
1153 |
by (lifting memb_delete_raw_ident) |
|
1154 |
||
36465 | 1155 |
lemma not_memb_fdelete_ident: |
36280 | 1156 |
shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S" |
1157 |
by (lifting not_memb_delete_raw_ident) |
|
1158 |
||
1159 |
lemma fset_fdelete_cases: |
|
1160 |
shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))" |
|
1161 |
by (lifting fset_raw_delete_raw_cases) |
|
1162 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1163 |
text {* finite intersection *} |
36280 | 1164 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1165 |
lemma finter_empty_l: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1166 |
shows "{||} |\<inter>| S = {||}" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1167 |
by simp |
36280 | 1168 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1169 |
|
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1170 |
lemma finter_empty_r: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1171 |
shows "S |\<inter>| {||} = {||}" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1172 |
by simp |
36280 | 1173 |
|
1174 |
lemma finter_finsert: |
|
1175 |
"finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)" |
|
1176 |
by (lifting finter_raw.simps(2)) |
|
1177 |
||
1178 |
lemma fin_finter: |
|
1179 |
"x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T" |
|
1180 |
by (lifting memb_finter_raw) |
|
1181 |
||
1182 |
lemma fsubset_finsert: |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1183 |
shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys" |
36280 | 1184 |
by (lifting sub_list_cons) |
1185 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1186 |
lemma |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1187 |
shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys" |
36280 | 1188 |
by (lifting sub_list_def[simplified memb_def[symmetric]]) |
1189 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1190 |
lemma fsubset_fin: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1191 |
shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)" |
36280 | 1192 |
by (rule meta_eq_to_obj_eq) |
1193 |
(lifting sub_list_def[simplified memb_def[symmetric]]) |
|
1194 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1195 |
lemma fminus_fin: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1196 |
shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1197 |
by (lifting fminus_raw_memb) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1198 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1199 |
lemma fminus_red: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1200 |
shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1201 |
by (lifting fminus_raw_red) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1202 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1203 |
lemma fminus_red_fin [simp]: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1204 |
shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1205 |
by (simp add: fminus_red) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1206 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1207 |
lemma fminus_red_fnotin[simp]: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1208 |
shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1209 |
by (simp add: fminus_red) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1210 |
|
36280 | 1211 |
lemma expand_fset_eq: |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1212 |
shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
36280 | 1213 |
by (lifting list_eq.simps[simplified memb_def[symmetric]]) |
1214 |
||
1215 |
(* We cannot write it as "assumes .. shows" since Isabelle changes |
|
1216 |
the quantifiers to schematic variables and reintroduces them in |
|
1217 |
a different order *) |
|
1218 |
lemma fset_eq_cases: |
|
1219 |
"\<lbrakk>a1 = a2; |
|
1220 |
\<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P; |
|
1221 |
\<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P; |
|
1222 |
\<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P; |
|
1223 |
\<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P; |
|
1224 |
\<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk> |
|
1225 |
\<Longrightarrow> P" |
|
1226 |
by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]]) |
|
1227 |
||
1228 |
lemma fset_eq_induct: |
|
1229 |
assumes "x1 = x2" |
|
1230 |
and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))" |
|
1231 |
and "P {||} {||}" |
|
1232 |
and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs" |
|
1233 |
and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)" |
|
1234 |
and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)" |
|
1235 |
and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3" |
|
1236 |
shows "P x1 x2" |
|
1237 |
using assms |
|
1238 |
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) |
|
1239 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1240 |
section {* fconcat *} |
36280 | 1241 |
|
1242 |
lemma fconcat_empty: |
|
1243 |
shows "fconcat {||} = {||}" |
|
1244 |
by (lifting concat.simps(1)) |
|
1245 |
||
1246 |
lemma fconcat_insert: |
|
1247 |
shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
|
1248 |
by (lifting concat.simps(2)) |
|
1249 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1250 |
lemma |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1251 |
shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys" |
36280 | 1252 |
by (lifting concat_append) |
1253 |
||
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1254 |
|
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1255 |
section {* ffilter *} |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1256 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1257 |
lemma subseteq_filter: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1258 |
shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1259 |
by (lifting sub_list_filter) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1260 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1261 |
lemma eq_ffilter: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1262 |
shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1263 |
by (lifting list_eq_filter) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1264 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1265 |
lemma subset_ffilter: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1266 |
shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs" |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1267 |
unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1268 |
|
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1269 |
section {* lemmas transferred from Finite_Set theory *} |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1270 |
|
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1271 |
text {* finiteness for finite sets holds *} |
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1272 |
lemma finite_fset: "finite (fset_to_set S)" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1273 |
by (induct S) auto |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1274 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1275 |
lemma fset_choice: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1276 |
shows "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1277 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1278 |
by (rule finite_set_choice[simplified Ball_def, OF finite_fset]) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1279 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1280 |
lemma fsubseteq_fnil: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1281 |
shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1282 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1283 |
by (rule subset_empty) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1284 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1285 |
lemma not_fsubset_fnil: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1286 |
shows "\<not> xs |\<subset>| {||}" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1287 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1288 |
by (rule not_psubset_empty) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1289 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1290 |
lemma fcard_mono: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1291 |
shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1292 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1293 |
by (rule card_mono[OF finite_fset]) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1294 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1295 |
lemma fcard_fseteq: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1296 |
shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1297 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1298 |
by (rule card_seteq[OF finite_fset]) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1299 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1300 |
lemma psubset_fcard_mono: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1301 |
shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1302 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1303 |
by (rule psubset_card_mono[OF finite_fset]) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1304 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1305 |
lemma fcard_funion_finter: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1306 |
shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1307 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1308 |
by (rule card_Un_Int[OF finite_fset finite_fset]) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1309 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1310 |
lemma fcard_funion_disjoint: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1311 |
shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1312 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1313 |
by (rule card_Un_disjoint[OF finite_fset finite_fset]) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1314 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1315 |
lemma fcard_delete1_less: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1316 |
shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1317 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1318 |
by (rule card_Diff1_less[OF finite_fset]) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1319 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1320 |
lemma fcard_delete2_less: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1321 |
shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1322 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1323 |
by (rule card_Diff2_less[OF finite_fset]) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1324 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1325 |
lemma fcard_delete1_le: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1326 |
shows "fcard (fdelete xs x) \<le> fcard xs" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1327 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1328 |
by (rule card_Diff1_le[OF finite_fset]) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1329 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1330 |
lemma fcard_psubset: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1331 |
shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1332 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1333 |
by (rule card_psubset[OF finite_fset]) |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1334 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1335 |
lemma fcard_fmap_le: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1336 |
shows "fcard (fmap f xs) \<le> fcard xs" |
36646
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1337 |
unfolding fset_to_set_trans |
8687bc6608d6
Translating lemmas from Finite_Set to FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36639
diff
changeset
|
1338 |
by (rule card_image_le[OF finite_fset]) |
36639
6243b49498ea
added function ffilter and some lemmas from Finite_Set to the FSet theory
bulwahn
parents:
36524
diff
changeset
|
1339 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1340 |
lemma fin_fminus_fnotin: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1341 |
shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1342 |
unfolding fset_to_set_trans |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1343 |
by blast |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1344 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1345 |
lemma fin_fnotin_fminus: |
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1346 |
shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1347 |
unfolding fset_to_set_trans |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1348 |
by blast |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1349 |
|
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1350 |
lemma fin_mdef: "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})" |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1351 |
unfolding fset_to_set_trans |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1352 |
by blast |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1353 |
|
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1354 |
lemma fcard_fminus_finsert[simp]: |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1355 |
assumes "a |\<in>| A" and "a |\<notin>| B" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1356 |
shows "fcard(A - finsert a B) = fcard(A - B) - 1" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1357 |
using assms unfolding fset_to_set_trans |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1358 |
by (rule card_Diff_insert[OF finite_fset]) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1359 |
|
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1360 |
lemma fcard_fminus_fsubset: |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1361 |
assumes "B |\<subseteq>| A" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1362 |
shows "fcard (A - B) = fcard A - fcard B" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1363 |
using assms unfolding fset_to_set_trans |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1364 |
by (rule card_Diff_subset[OF finite_fset]) |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1365 |
|
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1366 |
lemma fcard_fminus_subset_finter: |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1367 |
"fcard (A - B) = fcard A - fcard (A |\<inter>| B)" |
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1368 |
unfolding fset_to_set_trans |
37634
2116425cebc8
cleaned by using descending instead of lifting
Christian Urban <urbanc@in.tum.de>
parents:
37492
diff
changeset
|
1369 |
by (rule card_Diff_subset_Int) (fold finter_set, rule finite_fset) |
36675
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1370 |
|
806ea6e282e4
fminus and some more theorems ported from Finite_Set.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36646
diff
changeset
|
1371 |
|
36280 | 1372 |
ML {* |
36465 | 1373 |
fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
36280 | 1374 |
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
1375 |
*} |
|
1376 |
||
1377 |
no_notation |
|
1378 |
list_eq (infix "\<approx>" 50) |
|
1379 |
||
1380 |
end |