equal
deleted
inserted
replaced
155 apply auto |
155 apply auto |
156 done |
156 done |
157 |
157 |
158 lemma fst_splitE [elim!]: |
158 lemma fst_splitE [elim!]: |
159 "[| fst s' = x'; !!x s. [| s' = (x,s); x = x' |] ==> Q |] ==> Q" |
159 "[| fst s' = x'; !!x s. [| s' = (x,s); x = x' |] ==> Q |] ==> Q" |
160 apply (cut_tac p = "s'" in surjective_pairing) |
160 by (cases s') auto |
161 apply auto |
|
162 done |
|
163 |
161 |
164 lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l" |
162 lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l" |
165 apply (induct_tac "l") |
163 apply (induct_tac "l") |
166 apply auto |
164 apply auto |
167 done |
165 done |