equal
deleted
inserted
replaced
278 |
278 |
279 section "unique association lists" |
279 section "unique association lists" |
280 |
280 |
281 constdefs |
281 constdefs |
282 unique :: "('a \<times> 'b) list \<Rightarrow> bool" |
282 unique :: "('a \<times> 'b) list \<Rightarrow> bool" |
283 "unique \<equiv> nodups \<circ> map fst" |
283 "unique \<equiv> distinct \<circ> map fst" |
284 |
284 |
285 lemma uniqueD [rule_format (no_asm)]: |
285 lemma uniqueD [rule_format (no_asm)]: |
286 "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'--> y=y'))" |
286 "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'--> y=y'))" |
287 apply (unfold unique_def o_def) |
287 apply (unfold unique_def o_def) |
288 apply (induct_tac "l") |
288 apply (induct_tac "l") |