35 Definitions for membership, sublist, cardinality, |
35 Definitions for membership, sublist, cardinality, |
36 intersection, difference and respectful fold over |
36 intersection, difference and respectful fold over |
37 lists. |
37 lists. |
38 *} |
38 *} |
39 |
39 |
40 fun |
40 definition |
41 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
41 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
42 where |
42 where |
43 "memb x xs \<longleftrightarrow> x \<in> set xs" |
43 [simp]: "memb x xs \<longleftrightarrow> x \<in> set xs" |
44 |
44 |
45 fun |
45 definition |
46 sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
46 sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
47 where |
47 where |
48 "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys" |
48 [simp]: "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys" |
49 |
49 |
50 fun |
50 definition |
51 card_list :: "'a list \<Rightarrow> nat" |
51 card_list :: "'a list \<Rightarrow> nat" |
52 where |
52 where |
53 "card_list xs = card (set xs)" |
53 [simp]: "card_list xs = card (set xs)" |
54 |
54 |
55 fun |
55 definition |
56 inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
56 inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
57 where |
57 where |
58 "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]" |
58 [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]" |
59 |
59 |
60 fun |
60 definition |
61 diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
61 diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
62 where |
62 where |
63 "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]" |
63 [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]" |
64 |
64 |
65 definition |
65 definition |
66 rsp_fold |
66 rsp_fold |
67 where |
67 where |
68 "rsp_fold f \<equiv> \<forall>u v w. (f u (f v w) = f v (f u w))" |
68 "rsp_fold f \<equiv> \<forall>u v w. (f u (f v w) = f v (f u w))" |
1016 show thesis using b f g by simp |
1016 show thesis using b f g by simp |
1017 next |
1017 next |
1018 assume h: "x \<noteq> a" |
1018 assume h: "x \<noteq> a" |
1019 then have f: "\<not> memb x (a # ys)" using d by auto |
1019 then have f: "\<not> memb x (a # ys)" using d by auto |
1020 have g: "a # xs \<approx> x # (a # ys)" using e h by auto |
1020 have g: "a # xs \<approx> x # (a # ys)" using e h by auto |
1021 show thesis using b f g by (simp del: memb.simps) |
1021 show thesis using b f g by (simp del: memb_def) |
1022 qed |
1022 qed |
1023 qed |
1023 qed |
1024 then show thesis using a c by blast |
1024 then show thesis using a c by blast |
1025 qed |
1025 qed |
1026 |
1026 |
1156 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
1156 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
1157 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
1157 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
1158 *} |
1158 *} |
1159 |
1159 |
1160 no_notation |
1160 no_notation |
1161 list_eq (infix "\<approx>" 50) |
1161 list_eq (infix "\<approx>" 50) and |
1162 and list_eq2 (infix "\<approx>2" 50) |
1162 list_eq2 (infix "\<approx>2" 50) |
1163 |
1163 |
1164 end |
1164 end |