296 qed |
296 qed |
297 qed |
297 qed |
298 then show "concat a \<approx> concat b" by auto |
298 then show "concat a \<approx> concat b" by auto |
299 qed |
299 qed |
300 |
300 |
301 |
|
302 |
|
303 |
|
304 lemma [quot_respect]: |
301 lemma [quot_respect]: |
305 shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter" |
302 shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter" |
306 by auto |
303 by auto |
307 |
304 |
308 text {* Distributive lattice with bot *} |
305 text {* Distributive lattice with bot *} |
309 |
|
310 lemma sub_list_not_eq: |
|
311 "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)" |
|
312 by (auto simp add: sub_list_def) |
|
313 |
|
314 lemma sub_list_refl: |
|
315 "sub_list x x" |
|
316 by (simp add: sub_list_def) |
|
317 |
|
318 lemma sub_list_trans: |
|
319 "sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z" |
|
320 by (simp add: sub_list_def) |
|
321 |
|
322 lemma sub_list_empty: |
|
323 "sub_list [] x" |
|
324 by (simp add: sub_list_def) |
|
325 |
|
326 lemma sub_list_append_left: |
|
327 "sub_list x (x @ y)" |
|
328 by (simp add: sub_list_def) |
|
329 |
|
330 lemma sub_list_append_right: |
|
331 "sub_list y (x @ y)" |
|
332 by (simp add: sub_list_def) |
|
333 |
|
334 lemma sub_list_inter_left: |
|
335 shows "sub_list (finter_raw x y) x" |
|
336 by (simp add: sub_list_def) |
|
337 |
|
338 lemma sub_list_inter_right: |
|
339 shows "sub_list (finter_raw x y) y" |
|
340 by (simp add: sub_list_def) |
|
341 |
|
342 lemma sub_list_list_eq: |
|
343 "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y" |
|
344 unfolding sub_list_def list_eq.simps by blast |
|
345 |
|
346 lemma sub_list_append: |
|
347 "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x" |
|
348 unfolding sub_list_def by auto |
|
349 |
|
350 lemma sub_list_inter: |
|
351 "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)" |
|
352 by (simp add: sub_list_def) |
|
353 |
306 |
354 lemma append_inter_distrib: |
307 lemma append_inter_distrib: |
355 "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)" |
308 "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)" |
356 apply (induct x) |
309 apply (induct x) |
357 apply (auto) |
310 apply (auto) |
415 |
368 |
416 instance |
369 instance |
417 proof |
370 proof |
418 fix x y z :: "'a fset" |
371 fix x y z :: "'a fset" |
419 show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x" |
372 show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x" |
420 unfolding less_fset_def by (lifting sub_list_not_eq) |
373 unfolding less_fset_def |
|
374 by (descending) (auto simp add: sub_list_def) |
421 show "x |\<subseteq>| x" by (descending) (simp add: sub_list_def) |
375 show "x |\<subseteq>| x" by (descending) (simp add: sub_list_def) |
422 show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def) |
376 show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def) |
423 show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def) |
377 show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def) |
424 show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def) |
378 show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def) |
425 show "x |\<inter>| y |\<subseteq>| x" |
379 show "x |\<inter>| y |\<subseteq>| x" |
704 by (induct xs) simp_all |
658 by (induct xs) simp_all |
705 |
659 |
706 lemma fcard_raw_delete: |
660 lemma fcard_raw_delete: |
707 "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
661 "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
708 by (auto simp add: fcard_raw_def memb_def) |
662 by (auto simp add: fcard_raw_def memb_def) |
709 |
|
710 lemma finter_raw_empty: |
|
711 "finter_raw l [] = []" |
|
712 by (induct l) (simp_all add: not_memb_nil) |
|
713 |
663 |
714 lemma inj_map_eq_iff: |
664 lemma inj_map_eq_iff: |
715 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
665 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
716 by (simp add: set_eq_iff[symmetric] inj_image_eq_iff) |
666 by (simp add: set_eq_iff[symmetric] inj_image_eq_iff) |
717 |
667 |
841 lemma in_fset: |
791 lemma in_fset: |
842 "x \<in> fset S \<equiv> x |\<in>| S" |
792 "x \<in> fset S \<equiv> x |\<in>| S" |
843 by (lifting memb_def[symmetric]) |
793 by (lifting memb_def[symmetric]) |
844 |
794 |
845 lemma none_fin_fempty: |
795 lemma none_fin_fempty: |
846 "(\<forall>x. x |\<notin>| S) = (S = {||})" |
796 "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}" |
847 by (lifting none_memb_nil) |
797 by (lifting none_memb_nil) |
848 |
798 |
849 lemma fset_cong: |
799 lemma fset_cong: |
850 "(S = T) = (fset S = fset T)" |
800 "S = T \<longleftrightarrow> fset S = fset T" |
851 by (lifting list_eq.simps) |
801 by (lifting list_eq.simps) |
852 |
802 |
853 |
803 |
854 section {* fcard *} |
804 section {* fcard *} |
855 |
805 |
856 lemma fcard_finsert_if [simp]: |
806 lemma fcard_finsert_if [simp]: |
857 shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))" |
807 shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))" |
858 by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb) |
808 by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb) |
859 |
809 |
860 lemma fcard_0[simp]: |
810 lemma fcard_0[simp]: |
861 shows "fcard S = 0 \<longleftrightarrow> S = {||}" |
811 shows "fcard S = 0 \<longleftrightarrow> S = {||}" |
862 by (descending) (simp add: fcard_raw_def) |
812 by (descending) (simp add: fcard_raw_def) |
863 |
813 |
864 lemma fcard_fempty[simp]: |
814 lemma fcard_fempty[simp]: |
865 shows "fcard {||} = 0" |
815 shows "fcard {||} = 0" |
1088 by (lifting fset_raw_removeAll_cases) |
1038 by (lifting fset_raw_removeAll_cases) |
1089 |
1039 |
1090 |
1040 |
1091 section {* finter *} |
1041 section {* finter *} |
1092 |
1042 |
1093 lemma finter_empty_l: "({||} |\<inter>| S) = {||}" |
1043 lemma finter_empty_l: |
1094 by (lifting finter_raw.simps(1)) |
1044 shows "{||} |\<inter>| S = {||}" |
1095 |
1045 by simp |
1096 lemma finter_empty_r: "(S |\<inter>| {||}) = {||}" |
1046 |
1097 by (lifting finter_raw_empty) |
1047 lemma finter_empty_r: |
|
1048 shows "S |\<inter>| {||} = {||}" |
|
1049 by simp |
1098 |
1050 |
1099 lemma finter_finsert: |
1051 lemma finter_finsert: |
1100 shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)" |
1052 shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)" |
1101 by (descending) (simp add: memb_def) |
1053 by (descending) (simp add: memb_def) |
1102 |
1054 |
1103 lemma fin_finter: |
1055 lemma fin_finter: |
1104 shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T" |
1056 shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T" |
1105 by (descending) (simp add: memb_def) |
1057 by (descending) (simp add: memb_def) |
1106 |
1058 |
1107 lemma fsubset_finsert: |
1059 lemma fsubset_finsert: |
1108 shows "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)" |
1060 shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys" |
1109 by (lifting sub_list_cons) |
1061 by (lifting sub_list_cons) |
1110 |
1062 |
1111 lemma |
1063 lemma |
1112 shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys" |
1064 shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys" |
1113 by (descending) (auto simp add: sub_list_def memb_def) |
1065 by (descending) (auto simp add: sub_list_def memb_def) |
1115 lemma fsubset_fin: |
1067 lemma fsubset_fin: |
1116 shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)" |
1068 shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)" |
1117 by (descending) (auto simp add: sub_list_def memb_def) |
1069 by (descending) (auto simp add: sub_list_def memb_def) |
1118 |
1070 |
1119 lemma fminus_fin: |
1071 lemma fminus_fin: |
1120 shows "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)" |
1072 shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys" |
1121 by (descending) (simp add: memb_def) |
1073 by (descending) (simp add: memb_def) |
1122 |
1074 |
1123 lemma fminus_red: |
1075 lemma fminus_red: |
1124 shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))" |
1076 shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))" |
1125 by (descending) (auto simp add: memb_def) |
1077 by (descending) (auto simp add: memb_def) |
1205 apply(simp add: memb_def) |
1157 apply(simp add: memb_def) |
1206 apply(rule finite_set_choice[simplified Ball_def]) |
1158 apply(rule finite_set_choice[simplified Ball_def]) |
1207 apply(simp_all) |
1159 apply(simp_all) |
1208 done |
1160 done |
1209 |
1161 |
1210 lemma fsubseteq_fempty: |
1162 lemma fsubseteq_fempty: |
1211 shows "xs |\<subseteq>| {||} = (xs = {||})" |
1163 shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}" |
1212 by (metis finter_empty_r le_iff_inf) |
1164 by (metis finter_empty_r le_iff_inf) |
1213 |
1165 |
1214 lemma not_fsubset_fnil: |
1166 lemma not_fsubset_fnil: |
1215 shows "\<not> xs |\<subset>| {||}" |
1167 shows "\<not> xs |\<subset>| {||}" |
1216 by (metis fset_simps(1) fsubset_set not_psubset_empty) |
1168 by (metis fset_simps(1) fsubset_set not_psubset_empty) |
1274 lemma fin_fnotin_fminus: |
1226 lemma fin_fnotin_fminus: |
1275 shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S" |
1227 shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S" |
1276 unfolding fin_set fminus_set |
1228 unfolding fin_set fminus_set |
1277 by blast |
1229 by blast |
1278 |
1230 |
1279 lemma fin_mdef: |
1231 lemma fin_mdef: |
1280 shows "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))" |
1232 shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})" |
1281 unfolding fin_set fset_simps fset_cong fminus_set |
1233 unfolding fin_set fset_simps fset_cong fminus_set |
1282 by blast |
1234 by blast |
1283 |
1235 |
1284 lemma fcard_fminus_finsert[simp]: |
1236 lemma fcard_fminus_finsert[simp]: |
1285 assumes "a |\<in>| A" and "a |\<notin>| B" |
1237 assumes "a |\<in>| A" and "a |\<notin>| B" |