src/HOL/Finite_Set.thy
changeset 48632 c028cf680a3e
parent 48619 558e4e77ce69
child 48891 c0eafbd55de3
equal deleted 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)
  1791   thm fold.comp_fun_commute' [of B b, simplified fun_eq_iff, simplified]
       
  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