equal
deleted
inserted
replaced
55 | "finter_raw (x # xs) ys = |
55 | "finter_raw (x # xs) ys = |
56 (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)" |
56 (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)" |
57 |
57 |
58 |
58 |
59 definition |
59 definition |
60 fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
60 diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
61 where |
61 where |
62 "fminus_raw xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]" |
62 "diff_list xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]" |
63 |
63 |
64 |
64 |
65 definition |
65 definition |
66 rsp_fold |
66 rsp_fold |
67 where |
67 where |
81 |
81 |
82 lemma set_finter_raw[simp]: |
82 lemma set_finter_raw[simp]: |
83 shows "set (finter_raw xs ys) = set xs \<inter> set ys" |
83 shows "set (finter_raw xs ys) = set xs \<inter> set ys" |
84 by (induct xs) (auto simp add: memb_def) |
84 by (induct xs) (auto simp add: memb_def) |
85 |
85 |
86 lemma set_fminus_raw[simp]: |
86 lemma set_diff_list[simp]: |
87 shows "set (fminus_raw xs ys) = (set xs - set ys)" |
87 shows "set (diff_list xs ys) = (set xs - set ys)" |
88 by (auto simp add: fminus_raw_def) |
88 by (auto simp add: diff_list_def) |
89 |
89 |
90 |
90 |
91 section {* Quotient composition lemmas *} |
91 section {* Quotient composition lemmas *} |
92 |
92 |
93 lemma list_all2_refl1: |
93 lemma list_all2_refl1: |
206 |
206 |
207 lemma removeAll_rsp[quot_respect]: |
207 lemma removeAll_rsp[quot_respect]: |
208 shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll" |
208 shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll" |
209 by simp |
209 by simp |
210 |
210 |
211 lemma fminus_raw_rsp[quot_respect]: |
211 lemma diff_list_rsp[quot_respect]: |
212 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw" |
212 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list" |
213 by simp |
213 by simp |
214 |
214 |
215 lemma card_list_rsp[quot_respect]: |
215 lemma card_list_rsp[quot_respect]: |
216 shows "(op \<approx> ===> op =) card_list card_list" |
216 shows "(op \<approx> ===> op =) card_list card_list" |
217 by (simp add: card_list_def) |
217 by (simp add: card_list_def) |
344 "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)" |
344 "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)" |
345 |
345 |
346 quotient_definition |
346 quotient_definition |
347 "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
347 "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
348 is |
348 is |
349 "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
349 "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
350 |
350 |
351 lemma append_finter_raw_distrib: |
351 lemma append_finter_raw_distrib: |
352 "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)" |
352 "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)" |
353 apply (induct x) |
353 apply (induct x) |
354 apply (auto) |
354 apply (auto) |
718 |
718 |
719 |
719 |
720 (* FIXME: is this in any case a useful lemma *) |
720 (* FIXME: is this in any case a useful lemma *) |
721 lemma fin_mdef: |
721 lemma fin_mdef: |
722 shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})" |
722 shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})" |
723 by (descending) (auto simp add: memb_def fminus_raw_def) |
723 by (descending) (auto simp add: memb_def diff_list_def) |
724 |
724 |
725 |
725 |
726 subsection {* fset *} |
726 subsection {* fset *} |
727 |
727 |
728 lemma fset_simps[simp]: |
728 lemma fset_simps[simp]: |
754 shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys" |
754 shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys" |
755 by (lifting set_append) |
755 by (lifting set_append) |
756 |
756 |
757 lemma fminus_set [simp]: |
757 lemma fminus_set [simp]: |
758 shows "fset (xs - ys) = fset xs - fset ys" |
758 shows "fset (xs - ys) = fset xs - fset ys" |
759 by (lifting set_fminus_raw) |
759 by (lifting set_diff_list) |
760 |
760 |
761 |
761 |
762 subsection {* funion *} |
762 subsection {* funion *} |
763 |
763 |
764 lemmas [simp] = |
764 lemmas [simp] = |