# HG changeset patch # User haftmann # Date 1364976943 -7200 # Node ID 5dbe537087aaafb5577a831cde89f31f18c4eca7 # Parent c916828edc92695feebdba1a32c087baaa78104d generalized lemma fold_image thanks to Peter Lammich diff -r c916828edc92 -r 5dbe537087aa src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Apr 02 20:19:38 2013 +0200 +++ b/src/HOL/Finite_Set.thy Wed Apr 03 10:15:43 2013 +0200 @@ -715,19 +715,52 @@ then show ?thesis by simp qed +end + text{* Other properties of @{const fold}: *} lemma fold_image: - assumes "finite A" and "inj_on g A" + assumes "inj_on g A" shows "fold f z (g ` A) = fold (f \ g) z A" -using assms -proof induction - case (insert a F) - interpret comp_fun_commute "\x. f (g x)" by default (simp add: comp_fun_commute) - from insert show ?case by auto -qed simp - -end +proof (cases "finite A") + case False with assms show ?thesis by (auto dest: finite_imageD simp add: fold_def) +next + case True + have "fold_graph f z (g ` A) = fold_graph (f \ g) z A" + proof + fix w + show "fold_graph f z (g ` A) w \ fold_graph (f \ g) z A w" (is "?P \ ?Q") + proof + assume ?P then show ?Q using assms + proof (induct "g ` A" w arbitrary: A) + case emptyI then show ?case by (auto intro: fold_graph.emptyI) + next + case (insertI x A r B) + from `inj_on g B` `x \ A` `insert x A = image g B` obtain x' A' where + "x' \ A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'" + by (rule inj_img_insertE) + from insertI.prems have "fold_graph (f o g) z A' r" + by (auto intro: insertI.hyps) + with `x' \ A'` have "fold_graph (f \ g) z (insert x' A') ((f \ g) x' r)" + by (rule fold_graph.insertI) + then show ?case by simp + qed + next + assume ?Q then show ?P using assms + proof induct + case emptyI thus ?case by (auto intro: fold_graph.emptyI) + next + case (insertI x A r) + from `x \ A` insertI.prems have "g x \ g ` A" by auto + moreover from insertI have "fold_graph f z (g ` A) r" by simp + ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)" + by (rule fold_graph.insertI) + then show ?case by simp + qed + qed + qed + with True assms show ?thesis by (auto simp add: fold_def) +qed lemma fold_cong: assumes "comp_fun_commute f" "comp_fun_commute g" diff -r c916828edc92 -r 5dbe537087aa src/HOL/Fun.thy --- a/src/HOL/Fun.thy Tue Apr 02 20:19:38 2013 +0200 +++ b/src/HOL/Fun.thy Wed Apr 03 10:15:43 2013 +0200 @@ -286,6 +286,22 @@ "inj_on (f' o f) A \ inj_on f A" by(auto simp add: comp_inj_on inj_on_def) +lemma inj_img_insertE: + assumes "inj_on f A" + assumes "x \ B" and "insert x B = f ` A" + obtains x' A' where "x' \ A'" and "A = insert x' A'" + and "x = f x'" and "B = f ` A'" +proof - + from assms have "x \ f ` A" by auto + then obtain x' where *: "x' \ A" "x = f x'" by auto + then have "A = insert x' (A - {x'})" by auto + with assms * have "B = f ` (A - {x'})" + by (auto dest: inj_on_contraD) + have "x' \ A - {x'}" by simp + from `x' \ A - {x'}` `A = insert x' (A - {x'})` `x = f x'` `B = image f (A - {x'})` + show ?thesis .. +qed + lemma surj_def: "surj f \ (\y. \x. y = f x)" by auto