Theory FuncSet

theory FuncSet
imports Main
(*  Title:      HOL/Library/FuncSet.thy
Author: Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
*)


header {* Pi and Function Sets *}

theory FuncSet
imports Hilbert_Choice Main
begin

definition
Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where
"Pi A B = {f. ∀x. x ∈ A --> f x ∈ B x}"

definition
extensional :: "'a set => ('a => 'b) set" where
"extensional A = {f. ∀x. x~:A --> f x = undefined}"

definition
"restrict" :: "['a => 'b, 'a set] => ('a => 'b)" where
"restrict f A = (%x. if x ∈ A then f x else undefined)"

abbreviation
funcset :: "['a set, 'b set] => ('a => 'b) set"
(infixr "->" 60) where
"A -> B == Pi A (%_. B)"

notation (xsymbols)
funcset (infixr "->" 60)

syntax
"_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
"_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3)

syntax (xsymbols)
"_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3Π _∈_./ _)" 10)
"_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3λ_∈_./ _)" [0,0,3] 3)

syntax (HTML output)
"_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3Π _∈_./ _)" 10)
"_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3λ_∈_./ _)" [0,0,3] 3)

translations
"PI x:A. B" == "CONST Pi A (%x. B)"
"%x:A. f" == "CONST restrict (%x. f) A"

definition
"compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" where
"compose A g f = (λx∈A. g (f x))"


subsection{*Basic Properties of @{term Pi}*}

lemma Pi_I[intro!]: "(!!x. x ∈ A ==> f x ∈ B x) ==> f ∈ Pi A B"
by (simp add: Pi_def)

lemma Pi_I'[simp]: "(!!x. x : A --> f x : B x) ==> f : Pi A B"
by(simp add:Pi_def)

lemma funcsetI: "(!!x. x ∈ A ==> f x ∈ B) ==> f ∈ A -> B"
by (simp add: Pi_def)

lemma Pi_mem: "[|f: Pi A B; x ∈ A|] ==> f x ∈ B x"
by (simp add: Pi_def)

lemma Pi_iff: "f ∈ Pi I X <-> (∀i∈I. f i ∈ X i)"
unfolding Pi_def by auto

lemma PiE [elim]:
"f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
by(auto simp: Pi_def)

lemma Pi_cong:
"(!! w. w ∈ A ==> f w = g w) ==> f ∈ Pi A B <-> g ∈ Pi A B"
by (auto simp: Pi_def)

lemma funcset_id [simp]: "(λx. x) ∈ A -> A"
by auto

lemma funcset_mem: "[|f ∈ A -> B; x ∈ A|] ==> f x ∈ B"
by (simp add: Pi_def)

lemma funcset_image: "f ∈ A->B ==> f ` A ⊆ B"
by auto

lemma image_subset_iff_funcset: "F ` A ⊆ B <-> F ∈ A -> B"
by auto

lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (∃x∈A. B x = {})"
apply (simp add: Pi_def, auto)
txt{*Converse direction requires Axiom of Choice to exhibit a function
picking an element from each non-empty @{term "B x"}*}

apply (drule_tac x = "%u. SOME y. y ∈ B u" in spec, auto)
apply (cut_tac P= "%y. y ∈ B x" in some_eq_ex, auto)
done

lemma Pi_empty [simp]: "Pi {} B = UNIV"
by (simp add: Pi_def)

lemma Pi_Int: "Pi I E ∩ Pi I F = (Π i∈I. E i ∩ F i)"
by auto

lemma Pi_UN:
fixes A :: "nat => 'i => 'a set"
assumes "finite I" and mono: "!!i n m. i ∈ I ==> n ≤ m ==> A n i ⊆ A m i"
shows "(\<Union>n. Pi I (A n)) = (Π i∈I. \<Union>n. A n i)"
proof (intro set_eqI iffI)
fix f assume "f ∈ (Π i∈I. \<Union>n. A n i)"
then have "∀i∈I. ∃n. f i ∈ A n i" by auto
from bchoice[OF this] obtain n where n: "!!i. i ∈ I ==> f i ∈ (A (n i) i)" by auto
obtain k where k: "!!i. i ∈ I ==> n i ≤ k"
using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
have "f ∈ Pi I (A k)"
proof (intro Pi_I)
fix i assume "i ∈ I"
from mono[OF this, of "n i" k] k[OF this] n[OF this]
show "f i ∈ A k i" by auto
qed
then show "f ∈ (\<Union>n. Pi I (A n))" by auto
qed auto

lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
by (simp add: Pi_def)

text{*Covariance of Pi-sets in their second argument*}
lemma Pi_mono: "(!!x. x ∈ A ==> B x <= C x) ==> Pi A B <= Pi A C"
by auto

text{*Contravariance of Pi-sets in their first argument*}
lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
by auto

lemma prod_final:
assumes 1: "fst o f ∈ Pi A B" and 2: "snd o f ∈ Pi A C"
shows "f ∈ (Π z ∈ A. B z × C z)"
proof (rule Pi_I)
fix z
assume z: "z ∈ A"
have "f z = (fst (f z), snd (f z))"
by simp
also have "... ∈ B z × C z"
by (metis SigmaI PiE o_apply 1 2 z)
finally show "f z ∈ B z × C z" .
qed

lemma Pi_split_domain[simp]: "x ∈ Pi (I ∪ J) X <-> x ∈ Pi I X ∧ x ∈ Pi J X"
by (auto simp: Pi_def)

lemma Pi_split_insert_domain[simp]: "x ∈ Pi (insert i I) X <-> x ∈ Pi I X ∧ x i ∈ X i"
by (auto simp: Pi_def)

lemma Pi_cancel_fupd_range[simp]: "i ∉ I ==> x ∈ Pi I (B(i := b)) <-> x ∈ Pi I B"
by (auto simp: Pi_def)

lemma Pi_cancel_fupd[simp]: "i ∉ I ==> x(i := a) ∈ Pi I B <-> x ∈ Pi I B"
by (auto simp: Pi_def)

lemma Pi_fupd_iff: "i ∈ I ==> f ∈ Pi I (B(i := A)) <-> f ∈ Pi (I - {i}) B ∧ f i ∈ A"
apply auto
apply (drule_tac x=x in Pi_mem)
apply (simp_all split: split_if_asm)
apply (drule_tac x=i in Pi_mem)
apply (auto dest!: Pi_mem)
done

subsection{*Composition With a Restricted Domain: @{term compose}*}

lemma funcset_compose:
"[| f ∈ A -> B; g ∈ B -> C |]==> compose A g f ∈ A -> C"
by (simp add: Pi_def compose_def restrict_def)

lemma compose_assoc:
"[| f ∈ A -> B; g ∈ B -> C; h ∈ C -> D |]
==> compose A h (compose A g f) = compose A (compose B h g) f"

by (simp add: fun_eq_iff Pi_def compose_def restrict_def)

lemma compose_eq: "x ∈ A ==> compose A g f x = g(f(x))"
by (simp add: compose_def restrict_def)

lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
by (auto simp add: image_def compose_eq)


subsection{*Bounded Abstraction: @{term restrict}*}

lemma restrict_in_funcset: "(!!x. x ∈ A ==> f x ∈ B) ==> (λx∈A. f x) ∈ A -> B"
by (simp add: Pi_def restrict_def)

lemma restrictI[intro!]: "(!!x. x ∈ A ==> f x ∈ B x) ==> (λx∈A. f x) ∈ Pi A B"
by (simp add: Pi_def restrict_def)

lemma restrict_apply [simp]:
"(λy∈A. f y) x = (if x ∈ A then f x else undefined)"
by (simp add: restrict_def)

lemma restrict_ext:
"(!!x. x ∈ A ==> f x = g x) ==> (λx∈A. f x) = (λx∈A. g x)"
by (simp add: fun_eq_iff Pi_def restrict_def)

lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
by (simp add: inj_on_def restrict_def)

lemma Id_compose:
"[|f ∈ A -> B; f ∈ extensional A|] ==> compose A (λy∈B. y) f = f"
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)

lemma compose_Id:
"[|g ∈ A -> B; g ∈ extensional A|] ==> compose A g (λx∈A. x) = g"
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)

lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
by (auto simp add: restrict_def)

lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A ∩ B)"
unfolding restrict_def by (simp add: fun_eq_iff)

lemma restrict_fupd[simp]: "i ∉ I ==> restrict (f (i := x)) I = restrict f I"
by (auto simp: restrict_def)

lemma restrict_upd[simp]:
"i ∉ I ==> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
by (auto simp: fun_eq_iff)

lemma restrict_Pi_cancel: "restrict x I ∈ Pi I A <-> x ∈ Pi I A"
by (auto simp: restrict_def Pi_def)


subsection{*Bijections Between Sets*}

text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
the theorems belong here, or need at least @{term Hilbert_Choice}.*}


lemma bij_betwI:
assumes "f ∈ A -> B" and "g ∈ B -> A"
and g_f: "!!x. x∈A ==> g (f x) = x" and f_g: "!!y. y∈B ==> f (g y) = y"
shows "bij_betw f A B"
unfolding bij_betw_def
proof
show "inj_on f A" by (metis g_f inj_on_def)
next
have "f ` A ⊆ B" using `f ∈ A -> B` by auto
moreover
have "B ⊆ f ` A" by auto (metis Pi_mem `g ∈ B -> A` f_g image_iff)
ultimately show "f ` A = B" by blast
qed

lemma bij_betw_imp_funcset: "bij_betw f A B ==> f ∈ A -> B"
by (auto simp add: bij_betw_def)

lemma inj_on_compose:
"[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
by (auto simp add: bij_betw_def inj_on_def compose_eq)

lemma bij_betw_compose:
"[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
apply (simp add: bij_betw_def compose_eq inj_on_compose)
apply (auto simp add: compose_def image_def)
done

lemma bij_betw_restrict_eq [simp]:
"bij_betw (restrict f A) A B = bij_betw f A B"
by (simp add: bij_betw_def)


subsection{*Extensionality*}

lemma extensional_empty[simp]: "extensional {} = {λx. undefined}"
unfolding extensional_def by auto

lemma extensional_arb: "[|f ∈ extensional A; x∉ A|] ==> f x = undefined"
by (simp add: extensional_def)

lemma restrict_extensional [simp]: "restrict f A ∈ extensional A"
by (simp add: restrict_def extensional_def)

lemma compose_extensional [simp]: "compose A f g ∈ extensional A"
by (simp add: compose_def)

lemma extensionalityI:
"[| f ∈ extensional A; g ∈ extensional A;
!!x. x∈A ==> f x = g x |] ==> f = g"

by (force simp add: fun_eq_iff extensional_def)

lemma extensional_restrict: "f ∈ extensional A ==> restrict f A = f"
by(rule extensionalityI[OF restrict_extensional]) auto

lemma extensional_subset: "f ∈ extensional A ==> A ⊆ B ==> f ∈ extensional B"
unfolding extensional_def by auto

lemma inv_into_funcset: "f ` A = B ==> (λx∈B. inv_into A f x) : B -> A"
by (unfold inv_into_def) (fast intro: someI2)

lemma compose_inv_into_id:
"bij_betw f A B ==> compose A (λy∈B. inv_into A f y) f = (λx∈A. x)"
apply (simp add: bij_betw_def compose_def)
apply (rule restrict_ext, auto)
done

lemma compose_id_inv_into:
"f ` A = B ==> compose B f (λy∈B. inv_into A f y) = (λx∈B. x)"
apply (simp add: compose_def)
apply (rule restrict_ext)
apply (simp add: f_inv_into_f)
done

lemma extensional_insert[intro, simp]:
assumes "a ∈ extensional (insert i I)"
shows "a(i := b) ∈ extensional (insert i I)"
using assms unfolding extensional_def by auto

lemma extensional_Int[simp]:
"extensional I ∩ extensional I' = extensional (I ∩ I')"
unfolding extensional_def by auto

lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
by (auto simp: extensional_def)

lemma restrict_extensional_sub[intro]: "A ⊆ B ==> restrict f A ∈ extensional B"
unfolding restrict_def extensional_def by auto

lemma extensional_insert_undefined[intro, simp]:
"a ∈ extensional (insert i I) ==> a(i := undefined) ∈ extensional I"
unfolding extensional_def by auto

lemma extensional_insert_cancel[intro, simp]:
"a ∈ extensional I ==> a ∈ extensional (insert i I)"
unfolding extensional_def by auto


subsection{*Cardinality*}

lemma card_inj: "[|f ∈ A->B; inj_on f A; finite B|] ==> card(A) ≤ card(B)"
by (rule card_inj_on_le) auto

lemma card_bij:
"[|f ∈ A->B; inj_on f A;
g ∈ B->A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"

by (blast intro: card_inj order_antisym)

subsection {* Extensional Function Spaces *}

definition PiE :: "'a set => ('a => 'b set) => ('a => 'b) set" where
"PiE S T = Pi S T ∩ extensional S"

abbreviation "PiE A B ≡ PiE A B"

syntax "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10)

syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3ΠE _∈_./ _)" 10)

syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3ΠE _∈_./ _)" 10)

translations "PIE x:A. B" == "CONST PiE A (%x. B)"

abbreviation extensional_funcset :: "'a set => 'b set => ('a => 'b) set" (infixr "->E" 60) where
"A ->E B ≡ (ΠE i∈A. B)"

notation (xsymbols)
extensional_funcset (infixr "->E" 60)

lemma extensional_funcset_def: "extensional_funcset S T = (S -> T) ∩ extensional S"
by (simp add: PiE_def)

lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
unfolding PiE_def by simp

lemma PiE_empty_range[simp]: "i ∈ I ==> F i = {} ==> (PIE i:I. F i) = {}"
unfolding PiE_def by auto

lemma PiE_eq_empty_iff:
"PiE I F = {} <-> (∃i∈I. F i = {})"
proof
assume "PiE I F = {}"
show "∃i∈I. F i = {}"
proof (rule ccontr)
assume "¬ ?thesis"
then have "∀i. ∃y. (i ∈ I --> y ∈ F i) ∧ (i ∉ I --> y = undefined)" by auto
from choice[OF this]
obtain f where " ∀x. (x ∈ I --> f x ∈ F x) ∧ (x ∉ I --> f x = undefined)" ..
then have "f ∈ PiE I F" by (auto simp: extensional_def PiE_def)
with `PiE I F = {}` show False by auto
qed
qed (auto simp: PiE_def)

lemma PiE_arb: "f ∈ PiE S T ==> x ∉ S ==> f x = undefined"
unfolding PiE_def by auto (auto dest!: extensional_arb)

lemma PiE_mem: "f ∈ PiE S T ==> x ∈ S ==> f x ∈ T x"
unfolding PiE_def by auto

lemma PiE_fun_upd: "y ∈ T x ==> f ∈ PiE S T ==> f(x := y) ∈ PiE (insert x S) T"
unfolding PiE_def extensional_def by auto

lemma fun_upd_in_PiE: "x ∉ S ==> f ∈ PiE (insert x S) T ==> f(x := undefined) ∈ PiE S T"
unfolding PiE_def extensional_def by auto

lemma PiE_insert_eq:
assumes "x ∉ S"
shows "PiE (insert x S) T = (λ(y, g). g(x := y)) ` (T x × PiE S T)"
proof -
{
fix f assume "f ∈ PiE (insert x S) T"
with assms have "f ∈ (λ(y, g). g(x := y)) ` (T x × PiE S T)"
by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
}
then show ?thesis using assms by (auto intro: PiE_fun_upd)
qed

lemma PiE_Int: "(PiE I A) ∩ (PiE I B) = PiE I (λx. A x ∩ B x)"
by (auto simp: PiE_def)

lemma PiE_cong:
"(!!i. i∈I ==> A i = B i) ==> PiE I A = PiE I B"
unfolding PiE_def by (auto simp: Pi_cong)

lemma PiE_E [elim]:
"f ∈ PiE A B ==> (x ∈ A ==> f x ∈ B x ==> Q) ==> (x ∉ A ==> f x = undefined ==> Q) ==> Q"
by(auto simp: Pi_def PiE_def extensional_def)

lemma PiE_I[intro!]: "(!!x. x ∈ A ==> f x ∈ B x) ==> (!!x. x ∉ A ==> f x = undefined) ==> f ∈ PiE A B"
by (simp add: PiE_def extensional_def)

lemma PiE_mono: "(!!x. x ∈ A ==> B x ⊆ C x) ==> PiE A B ⊆ PiE A C"
by auto

lemma PiE_iff: "f ∈ PiE I X <-> (∀i∈I. f i ∈ X i) ∧ f ∈ extensional I"
by (simp add: PiE_def Pi_iff)

lemma PiE_restrict[simp]: "f ∈ PiE A B ==> restrict f A = f"
by (simp add: extensional_restrict PiE_def)

lemma restrict_PiE[simp]: "restrict f I ∈ PiE I S <-> f ∈ Pi I S"
by (auto simp: PiE_iff)

lemma PiE_eq_subset:
assumes ne: "!!i. i ∈ I ==> F i ≠ {}" "!!i. i ∈ I ==> F' i ≠ {}"
assumes eq: "PiE I F = PiE I F'" and "i ∈ I"
shows "F i ⊆ F' i"
proof
fix x assume "x ∈ F i"
with ne have "∀j. ∃y. ((j ∈ I --> y ∈ F j ∧ (i = j --> x = y)) ∧ (j ∉ I --> y = undefined))"
by auto
from choice[OF this] obtain f
where f: " ∀j. (j ∈ I --> f j ∈ F j ∧ (i = j --> x = f j)) ∧ (j ∉ I --> f j = undefined)" ..
then have "f ∈ PiE I F" by (auto simp: extensional_def PiE_def)
then have "f ∈ PiE I F'" using assms by simp
then show "x ∈ F' i" using f `i ∈ I` by (auto simp: PiE_def)
qed

lemma PiE_eq_iff_not_empty:
assumes ne: "!!i. i ∈ I ==> F i ≠ {}" "!!i. i ∈ I ==> F' i ≠ {}"
shows "PiE I F = PiE I F' <-> (∀i∈I. F i = F' i)"
proof (intro iffI ballI)
fix i assume eq: "PiE I F = PiE I F'" and i: "i ∈ I"
show "F i = F' i"
using PiE_eq_subset[of I F F', OF ne eq i]
using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
by auto
qed (auto simp: PiE_def)

lemma PiE_eq_iff:
"PiE I F = PiE I F' <-> (∀i∈I. F i = F' i) ∨ ((∃i∈I. F i = {}) ∧ (∃i∈I. F' i = {}))"
proof (intro iffI disjCI)
assume eq[simp]: "PiE I F = PiE I F'"
assume "¬ ((∃i∈I. F i = {}) ∧ (∃i∈I. F' i = {}))"
then have "(∀i∈I. F i ≠ {}) ∧ (∀i∈I. F' i ≠ {})"
using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
with PiE_eq_iff_not_empty[of I F F'] show "∀i∈I. F i = F' i" by auto
next
assume "(∀i∈I. F i = F' i) ∨ (∃i∈I. F i = {}) ∧ (∃i∈I. F' i = {})"
then show "PiE I F = PiE I F'"
using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
qed

lemma extensional_funcset_fun_upd_restricts_rangeI:
"∀y ∈ S. f x ≠ f y ==> f : (insert x S) ->E T ==> f(x := undefined) : S ->E (T - {f x})"
unfolding extensional_funcset_def extensional_def
apply auto
apply (case_tac "x = xa")
apply auto
done

lemma extensional_funcset_fun_upd_extends_rangeI:
assumes "a ∈ T" "f ∈ S ->E (T - {a})"
shows "f(x := a) ∈ (insert x S) ->E T"
using assms unfolding extensional_funcset_def extensional_def by auto

subsubsection {* Injective Extensional Function Spaces *}

lemma extensional_funcset_fun_upd_inj_onI:
assumes "f ∈ S ->E (T - {a})" "inj_on f S"
shows "inj_on (f(x := a)) S"
using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)

lemma extensional_funcset_extend_domain_inj_on_eq:
assumes "x ∉ S"
shows"{f. f ∈ (insert x S) ->E T ∧ inj_on f (insert x S)} =
(%(y, g). g(x:=y)) ` {(y, g). y ∈ T ∧ g ∈ S ->E (T - {y}) ∧ inj_on g S}"

proof -
from assms show ?thesis
apply (auto del: PiE_I PiE_E)
apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
apply (auto simp add: image_iff inj_on_def)
apply (rule_tac x="xa x" in exI)
apply (auto intro: PiE_mem del: PiE_I PiE_E)
apply (rule_tac x="xa(x := undefined)" in exI)
apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
apply (auto dest!: PiE_mem split: split_if_asm)
done
qed

lemma extensional_funcset_extend_domain_inj_onI:
assumes "x ∉ S"
shows "inj_on (λ(y, g). g(x := y)) {(y, g). y ∈ T ∧ g ∈ S ->E (T - {y}) ∧ inj_on g S}"
proof -
from assms show ?thesis
apply (auto intro!: inj_onI)
apply (metis fun_upd_same)
by (metis assms PiE_arb fun_upd_triv fun_upd_upd)
qed


subsubsection {* Cardinality *}

lemma finite_PiE: "finite S ==> (!!i. i ∈ S ==> finite (T i)) ==> finite (PIE i : S. T i)"
by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)

lemma inj_combinator: "x ∉ S ==> inj_on (λ(y, g). g(x := y)) (T x × PiE S T)"
proof (safe intro!: inj_onI ext)
fix f y g z assume "x ∉ S" and fg: "f ∈ PiE S T" "g ∈ PiE S T"
assume "f(x := y) = g(x := z)"
then have *: "!!i. (f(x := y)) i = (g(x := z)) i"
unfolding fun_eq_iff by auto
from this[of x] show "y = z" by simp
fix i from *[of i] `x ∉ S` fg show "f i = g i"
by (auto split: split_if_asm simp: PiE_def extensional_def)
qed

lemma card_PiE:
"finite S ==> card (PIE i : S. T i) = (∏ i∈S. card (T i))"
proof (induct rule: finite_induct)
case empty then show ?case by auto
next
case (insert x S) then show ?case
by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
qed

end