src/HOL/Finite_Set.thy
 changeset 48632 c028cf680a3e parent 48619 558e4e77ce69 child 48891 c0eafbd55de3
equal inserted replaced
48631:81c81f13d152 48632:c028cf680a3e
`  1786   from `A \<noteq> {}` obtain b where "b \<in> A" by blast`
`  1786   from `A \<noteq> {}` obtain b where "b \<in> A" by blast`
`  1787   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)`
`  1787   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)`
`  1788   with `finite A` have "finite B" by simp`
`  1788   with `finite A` have "finite B" by simp`
`  1789   interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof`
`  1789   interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof`
`  1790   qed (simp_all add: fun_eq_iff ac_simps)`
`  1790   qed (simp_all add: fun_eq_iff ac_simps)`
`  1792   from `finite B` fold.comp_fun_commute' [of B x]`
`  1791   from `finite B` fold.comp_fun_commute' [of B x]`
`  1793     have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp`
`  1792     have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp`
`  1794   then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute)`
`  1793   then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute)`
`  1795   from `finite B` * fold.insert [of B b]`
`  1794   from `finite B` * fold.insert [of B b]`
`  1796     have "(\<lambda>x. fold op * x (insert b B)) = (\<lambda>x. fold op * x B) \<circ> op * b" by simp`
`  1795     have "(\<lambda>x. fold op * x (insert b B)) = (\<lambda>x. fold op * x B) \<circ> op * b" by simp`