equal
deleted
inserted
replaced
48 lemma [code]: |
48 lemma [code]: |
49 "set xs = Set (remdups xs)" |
49 "set xs = Set (remdups xs)" |
50 by simp |
50 by simp |
51 |
51 |
52 lemma [code]: |
52 lemma [code]: |
53 "x \<in> Set xs \<longleftrightarrow> member xs x" |
53 "x \<in> Set xs \<longleftrightarrow> List.member xs x" |
54 "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x" |
54 "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x" |
55 by (simp_all add: mem_iff) |
55 by (simp_all add: member_def) |
56 |
56 |
57 definition is_empty :: "'a set \<Rightarrow> bool" where |
57 definition is_empty :: "'a set \<Rightarrow> bool" where |
58 [simp]: "is_empty A \<longleftrightarrow> A = {}" |
58 [simp]: "is_empty A \<longleftrightarrow> A = {}" |
59 |
59 |
60 lemma [code_unfold]: |
60 lemma [code_unfold]: |
83 #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool") |
83 #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool") |
84 #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat") |
84 #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat") |
85 *} |
85 *} |
86 |
86 |
87 lemma is_empty_Set [code]: |
87 lemma is_empty_Set [code]: |
88 "is_empty (Set xs) \<longleftrightarrow> null xs" |
88 "is_empty (Set xs) \<longleftrightarrow> List.null xs" |
89 by (simp add: empty_null) |
89 by (simp add: null_def) |
90 |
90 |
91 lemma empty_Set [code]: |
91 lemma empty_Set [code]: |
92 "empty = Set []" |
92 "empty = Set []" |
93 by simp |
93 by simp |
94 |
94 |
110 "project P (Set xs) = Set (filter P xs)" |
110 "project P (Set xs) = Set (filter P xs)" |
111 by (simp add: project_set) |
111 by (simp add: project_set) |
112 |
112 |
113 lemma Ball_Set [code]: |
113 lemma Ball_Set [code]: |
114 "Ball (Set xs) P \<longleftrightarrow> list_all P xs" |
114 "Ball (Set xs) P \<longleftrightarrow> list_all P xs" |
115 by (simp add: ball_set) |
115 by (simp add: list_all_iff) |
116 |
116 |
117 lemma Bex_Set [code]: |
117 lemma Bex_Set [code]: |
118 "Bex (Set xs) P \<longleftrightarrow> list_ex P xs" |
118 "Bex (Set xs) P \<longleftrightarrow> list_ex P xs" |
119 by (simp add: bex_set) |
119 by (simp add: list_ex_iff) |
120 |
120 |
121 lemma card_Set [code]: |
121 lemma card_Set [code]: |
122 "card (Set xs) = length (remdups xs)" |
122 "card (Set xs) = length (remdups xs)" |
123 proof - |
123 proof - |
124 have "card (set (remdups xs)) = length (remdups xs)" |
124 have "card (set (remdups xs)) = length (remdups xs)" |