src/HOL/Library/FuncSet.thy
 changeset 59425 c5e79df8cc21 parent 58881 b9556a055632 child 61359 e985b52c3eb3
```     1.1 --- a/src/HOL/Library/FuncSet.thy	Thu Jan 22 13:21:45 2015 +0100
1.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Jan 22 14:51:08 2015 +0100
1.3 @@ -405,16 +405,20 @@
1.4  lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
1.5    unfolding PiE_def extensional_def by auto
1.6
1.7 -lemma PiE_insert_eq:
1.8 -  assumes "x \<notin> S"
1.9 -  shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.10 +lemma PiE_insert_eq: "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.11  proof -
1.12    {
1.13 -    fix f assume "f \<in> PiE (insert x S) T"
1.14 +    fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
1.15      with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.16        by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
1.17    }
1.18 -  then show ?thesis
1.19 +  moreover
1.20 +  {
1.21 +    fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
1.22 +    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.23 +      by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
1.24 +  }
1.25 +  ultimately show ?thesis
1.26      using assms by (auto intro: PiE_fun_upd)
1.27  qed
1.28
```