generalized lemma fold_image thanks to Peter Lammich
authorhaftmann
Wed Apr 03 10:15:43 2013 +0200 (2013-04-03)
changeset 515985dbe537087aa
parent 51597 c916828edc92
child 51599 1559e9266280
child 51601 8e80ecfa3652
generalized lemma fold_image thanks to Peter Lammich
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Apr 02 20:19:38 2013 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Apr 03 10:15:43 2013 +0200
     1.3 @@ -715,19 +715,52 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +end
     1.8 +
     1.9  text{* Other properties of @{const fold}: *}
    1.10  
    1.11  lemma fold_image:
    1.12 -  assumes "finite A" and "inj_on g A"
    1.13 +  assumes "inj_on g A"
    1.14    shows "fold f z (g ` A) = fold (f \<circ> g) z A"
    1.15 -using assms
    1.16 -proof induction
    1.17 -  case (insert a F)
    1.18 -    interpret comp_fun_commute "\<lambda>x. f (g x)" by default (simp add: comp_fun_commute)
    1.19 -    from insert show ?case by auto
    1.20 -qed simp
    1.21 -
    1.22 -end
    1.23 +proof (cases "finite A")
    1.24 +  case False with assms show ?thesis by (auto dest: finite_imageD simp add: fold_def)
    1.25 +next
    1.26 +  case True
    1.27 +  have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
    1.28 +  proof
    1.29 +    fix w
    1.30 +    show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q")
    1.31 +    proof
    1.32 +      assume ?P then show ?Q using assms
    1.33 +      proof (induct "g ` A" w arbitrary: A)
    1.34 +        case emptyI then show ?case by (auto intro: fold_graph.emptyI)
    1.35 +      next
    1.36 +        case (insertI x A r B)
    1.37 +        from `inj_on g B` `x \<notin> A` `insert x A = image g B` obtain x' A' where
    1.38 +          "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
    1.39 +          by (rule inj_img_insertE)
    1.40 +        from insertI.prems have "fold_graph (f o g) z A' r"
    1.41 +          by (auto intro: insertI.hyps)
    1.42 +        with `x' \<notin> A'` have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
    1.43 +          by (rule fold_graph.insertI)
    1.44 +        then show ?case by simp
    1.45 +      qed
    1.46 +    next
    1.47 +      assume ?Q then show ?P using assms
    1.48 +      proof induct
    1.49 +        case emptyI thus ?case by (auto intro: fold_graph.emptyI)
    1.50 +      next
    1.51 +        case (insertI x A r)
    1.52 +        from `x \<notin> A` insertI.prems have "g x \<notin> g ` A" by auto
    1.53 +        moreover from insertI have "fold_graph f z (g ` A) r" by simp
    1.54 +        ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
    1.55 +          by (rule fold_graph.insertI)
    1.56 +        then show ?case by simp
    1.57 +      qed
    1.58 +    qed
    1.59 +  qed
    1.60 +  with True assms show ?thesis by (auto simp add: fold_def)
    1.61 +qed
    1.62  
    1.63  lemma fold_cong:
    1.64    assumes "comp_fun_commute f" "comp_fun_commute g"
     2.1 --- a/src/HOL/Fun.thy	Tue Apr 02 20:19:38 2013 +0200
     2.2 +++ b/src/HOL/Fun.thy	Wed Apr 03 10:15:43 2013 +0200
     2.3 @@ -286,6 +286,22 @@
     2.4    "inj_on (f' o f) A \<Longrightarrow> inj_on f A"
     2.5  by(auto simp add: comp_inj_on inj_on_def)
     2.6  
     2.7 +lemma inj_img_insertE:
     2.8 +  assumes "inj_on f A"
     2.9 +  assumes "x \<notin> B" and "insert x B = f ` A"
    2.10 +  obtains x' A' where "x' \<notin> A'" and "A = insert x' A'"
    2.11 +    and "x = f x'" and "B = f ` A'" 
    2.12 +proof -
    2.13 +  from assms have "x \<in> f ` A" by auto
    2.14 +  then obtain x' where *: "x' \<in> A" "x = f x'" by auto
    2.15 +  then have "A = insert x' (A - {x'})" by auto
    2.16 +  with assms * have "B = f ` (A - {x'})"
    2.17 +    by (auto dest: inj_on_contraD)
    2.18 +  have "x' \<notin> A - {x'}" by simp
    2.19 +  from `x' \<notin> A - {x'}` `A = insert x' (A - {x'})` `x = f x'` `B = image f (A - {x'})`
    2.20 +  show ?thesis ..
    2.21 +qed
    2.22 +
    2.23  lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
    2.24    by auto
    2.25