equal
deleted
inserted
replaced
|
1 (* Title: Quotient.thy |
|
2 Author: Cezary Kaliszyk |
|
3 Author: Christian Urban |
|
4 |
|
5 provides a reasoning infrastructure for the type of finite sets |
|
6 *) |
1 theory FSet |
7 theory FSet |
2 imports Quotient Quotient_List List |
8 imports Quotient Quotient_List List |
3 begin |
9 begin |
4 |
10 |
5 fun |
11 fun |
7 where |
13 where |
8 "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |
14 "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |
9 |
15 |
10 lemma list_eq_equivp: |
16 lemma list_eq_equivp: |
11 shows "equivp list_eq" |
17 shows "equivp list_eq" |
12 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
18 unfolding equivp_reflp_symp_transp |
|
19 unfolding reflp_def symp_def transp_def |
13 by auto |
20 by auto |
14 |
21 |
15 quotient_type |
22 quotient_type |
16 'a fset = "'a list" / "list_eq" |
23 'a fset = "'a list" / "list_eq" |
17 by (rule list_eq_equivp) |
24 by (rule list_eq_equivp) |
46 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
53 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
47 |
54 |
48 abbreviation |
55 abbreviation |
49 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
56 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
50 where |
57 where |
51 "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)" |
58 "x |\<notin>| S \<equiv> \<not>(x |\<in>| S)" |
52 |
59 |
53 lemma memb_rsp[quot_respect]: |
60 lemma memb_rsp[quot_respect]: |
54 shows "(op = ===> op \<approx> ===> op =) memb memb" |
61 shows "(op = ===> op \<approx> ===> op =) memb memb" |
55 by (auto simp add: memb_def) |
62 by (auto simp add: memb_def) |
56 |
63 |
64 |
71 |
65 section {* Augmenting an fset -- @{const finsert} *} |
72 section {* Augmenting an fset -- @{const finsert} *} |
66 |
73 |
67 lemma nil_not_cons: |
74 lemma nil_not_cons: |
68 shows |
75 shows |
69 "\<not>[] \<approx> x # xs" |
76 "\<not> ([] \<approx> x # xs)" |
70 "\<not>x # xs \<approx> []" |
77 "\<not> (x # xs \<approx> [])" |
71 by auto |
78 by auto |
72 |
79 |
73 lemma not_memb_nil: |
80 lemma not_memb_nil: |
74 "\<not>memb x []" |
81 "\<not> memb x []" |
75 by (simp add: memb_def) |
82 by (simp add: memb_def) |
76 |
83 |
77 lemma memb_cons_iff: |
84 lemma memb_cons_iff: |
78 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
85 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
79 by (induct xs) (auto simp add: memb_def) |
86 by (induct xs) (auto simp add: memb_def) |
129 using a |
136 using a |
130 by (induct xs) (auto simp add: memb_def) |
137 by (induct xs) (auto simp add: memb_def) |
131 |
138 |
132 lemma fcard_raw_not_memb: |
139 lemma fcard_raw_not_memb: |
133 fixes x :: "'a" |
140 fixes x :: "'a" |
134 shows "\<not>(memb x xs) \<longleftrightarrow> (fcard_raw (x # xs) = Suc (fcard_raw xs))" |
141 shows "\<not>(memb x xs) \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)" |
135 by auto |
142 by auto |
136 |
143 |
137 lemma fcard_raw_suc: |
144 lemma fcard_raw_suc: |
138 fixes xs :: "'a list" |
145 fixes xs :: "'a list" |
139 assumes c: "fcard_raw xs = Suc n" |
146 assumes c: "fcard_raw xs = Suc n" |
176 apply simp |
183 apply simp |
177 by (metis memb_def subset_empty subset_insert) |
184 by (metis memb_def subset_empty subset_insert) |
178 |
185 |
179 lemma fcard_raw_1: |
186 lemma fcard_raw_1: |
180 fixes a :: "'a list" |
187 fixes a :: "'a list" |
181 shows "(fcard_raw xs = 1) = (\<exists>x. xs \<approx> [x])" |
188 shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])" |
182 apply auto |
189 apply (auto dest!: fcard_raw_suc) |
183 apply (drule fcard_raw_suc) |
|
184 apply clarify |
|
185 apply (simp add: fcard_raw_0) |
190 apply (simp add: fcard_raw_0) |
186 apply (rule_tac x="x" in exI) |
191 apply (rule_tac x="x" in exI) |
187 apply simp |
192 apply simp |
188 apply (subgoal_tac "set xs = {x}") |
193 apply (subgoal_tac "set xs = {x}") |
189 apply (erule singleton_fcard_1) |
194 apply (erule singleton_fcard_1) |
221 lemma map_append: |
226 lemma map_append: |
222 "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)" |
227 "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)" |
223 by simp |
228 by simp |
224 |
229 |
225 lemma memb_append: |
230 lemma memb_append: |
226 "memb x (xs @ ys) = (memb x xs \<or> memb x ys)" |
231 "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys" |
227 by (induct xs) (simp_all add: not_memb_nil memb_cons_iff) |
232 by (induct xs) (simp_all add: not_memb_nil memb_cons_iff) |
228 |
233 |
229 text {* raw section *} |
234 text {* raw section *} |
230 |
235 |
231 lemma map_rsp[quot_respect]: |
236 lemma map_rsp[quot_respect]: |
373 lemma finter_raw_empty: |
378 lemma finter_raw_empty: |
374 "finter_raw l [] = []" |
379 "finter_raw l [] = []" |
375 by (induct l) (simp_all add: not_memb_nil) |
380 by (induct l) (simp_all add: not_memb_nil) |
376 |
381 |
377 lemma memb_finter_raw: |
382 lemma memb_finter_raw: |
378 "memb x (finter_raw xs ys) = (memb x xs \<and> memb x ys)" |
383 "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys" |
379 apply (induct xs) |
384 apply (induct xs) |
380 apply (simp add: not_memb_nil) |
385 apply (simp add: not_memb_nil) |
381 apply (simp add: finter_raw.simps) |
386 apply (simp add: finter_raw.simps) |
382 apply (simp add: memb_cons_iff) |
387 apply (simp add: memb_cons_iff) |
383 apply auto |
388 apply auto |