equal
deleted
inserted
replaced
122 |
122 |
123 lemma Bex_Set [code]: |
123 lemma Bex_Set [code]: |
124 "Bex (Set xs) P \<longleftrightarrow> list_ex P xs" |
124 "Bex (Set xs) P \<longleftrightarrow> list_ex P xs" |
125 by (simp add: list_ex_iff) |
125 by (simp add: list_ex_iff) |
126 |
126 |
|
127 lemma |
|
128 [code, code del]: "card S = card S" .. |
|
129 |
127 lemma card_Set [code]: |
130 lemma card_Set [code]: |
128 "card (Set xs) = length (remdups xs)" |
131 "card (Set xs) = length (remdups xs)" |
129 proof - |
132 proof - |
130 have "card (set (remdups xs)) = length (remdups xs)" |
133 have "card (set (remdups xs)) = length (remdups xs)" |
131 by (rule distinct_card) simp |
134 by (rule distinct_card) simp |