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