summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Tue, 04 May 2010 10:49:46 +0200 | |

changeset 36638 | 4fed34e1dddd |

parent 36636 | 7dded80a953f (current diff) |

parent 36637 | 74a5c04bf29d (diff) |

child 36639 | 6243b49498ea |

merged

--- a/src/HOL/Finite_Set.thy Tue May 04 09:25:38 2010 +0200 +++ b/src/HOL/Finite_Set.thy Tue May 04 10:49:46 2010 +0200 @@ -1729,12 +1729,10 @@ qed lemma insert [simp]: - assumes "finite A" and "x \<notin> A" - shows "F (insert x A) = (if A = {} then x else x * F A)" -proof (cases "A = {}") - case True then show ?thesis by simp -next - case False then obtain b where "b \<in> A" by blast + assumes "finite A" and "x \<notin> A" and "A \<noteq> {}" + shows "F (insert x A) = x * F A" +proof - + from `A \<noteq> {}` obtain b where "b \<in> A" by blast then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert) with `finite A` have "finite B" by simp interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof @@ -1828,8 +1826,6 @@ (simp_all add: assoc in_idem `finite A`) qed -declare insert [simp del] - lemma eq_fold_idem': assumes "finite A" shows "F (insert a A) = fold (op *) a A" @@ -1839,13 +1835,13 @@ qed lemma insert_idem [simp]: - assumes "finite A" - shows "F (insert x A) = (if A = {} then x else x * F A)" + assumes "finite A" and "A \<noteq> {}" + shows "F (insert x A) = x * F A" proof (cases "x \<in> A") - case False with `finite A` show ?thesis by (rule insert) + case False from `finite A` `x \<notin> A` `A \<noteq> {}` show ?thesis by (rule insert) next - case True then have "A \<noteq> {}" by auto - with `finite A` show ?thesis by (simp add: in_idem insert_absorb True) + case True + from `finite A` `A \<noteq> {}` show ?thesis by (simp add: in_idem insert_absorb True) qed lemma union_idem: