equal
deleted
inserted
replaced
11 lemmas [simp] = Let_def |
11 lemmas [simp] = Let_def |
12 |
12 |
13 section "unique" |
13 section "unique" |
14 |
14 |
15 constdefs |
15 constdefs |
16 |
|
17 unique :: "('a \<times> 'b) list => bool" |
16 unique :: "('a \<times> 'b) list => bool" |
18 "unique == nodups \<circ> map fst" |
17 "unique == nodups \<circ> map fst" |
19 |
18 |
20 |
19 |
21 lemma fst_in_set_lemma [rule_format (no_asm)]: |
20 lemma fst_in_set_lemma [rule_format (no_asm)]: |
22 "(x, y) : set xys --> x : fst ` set xys" |
21 "(x, y) : set xys --> x : fst ` set xys" |
23 apply (induct_tac "xys") |
22 apply (induct_tac "xys") |
69 apply (induct_tac "t") |
68 apply (induct_tac "t") |
70 apply auto |
69 apply auto |
71 done |
70 done |
72 |
71 |
73 end |
72 end |
74 |
|