# Theory FuncSet

Up to index of Isabelle/HOL/HOL-Algebra

theory FuncSet
imports Main
`(*  Title:      HOL/Library/FuncSet.thy    Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn*)header {* Pi and Function Sets *}theory FuncSetimports Hilbert_Choice Mainbegindefinition  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 autolemma 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 autolemma 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 autolemma image_subset_iff_funcset: "F ` A ⊆ B <-> F ∈ A -> B"  by autolemma 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 functionpicking 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)donelemma 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 autolemma 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 autoqed autolemma 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 autotext{*Contravariance of Pi-sets in their first argument*}lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"by autolemma 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" .qedlemma 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)  donesubsection{*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 ofthe 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_defproof  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 blastqedlemma 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)donelemma 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 autolemma 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]) autolemma extensional_subset: "f ∈ extensional A ==> A ⊆ B ==> f ∈ extensional B"  unfolding extensional_def by autolemma 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)donelemma 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)donelemma extensional_insert[intro, simp]:  assumes "a ∈ extensional (insert i I)"  shows "a(i := b) ∈ extensional (insert i I)"  using assms unfolding extensional_def by autolemma extensional_Int[simp]:  "extensional I ∩ extensional I' = extensional (I ∩ I')"  unfolding extensional_def by autolemma 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 autolemma extensional_insert_undefined[intro, simp]:  "a ∈ extensional (insert i I) ==> a(i := undefined) ∈ extensional I"  unfolding extensional_def by autolemma extensional_insert_cancel[intro, simp]:  "a ∈ extensional I ==> a ∈ extensional (insert i I)"  unfolding extensional_def by autosubsection{*Cardinality*}lemma card_inj: "[|f ∈ A->B; inj_on f A; finite B|] ==> card(A) ≤ card(B)"by (rule card_inj_on_le) autolemma 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 "Pi⇣E 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 Pi⇣E 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 simplemma PiE_empty_range[simp]: "i ∈ I ==> F i = {} ==> (PIE i:I. F i) = {}"  unfolding PiE_def by autolemma PiE_eq_empty_iff:  "Pi⇣E I F = {} <-> (∃i∈I. F i = {})"proof  assume "Pi⇣E 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] guess f ..    then have "f ∈ Pi⇣E I F" by (auto simp: extensional_def PiE_def)    with `Pi⇣E I F = {}` show False by auto  qedqed (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 autolemma PiE_fun_upd: "y ∈ T x ==> f ∈ PiE S T ==> f(x := y) ∈ PiE (insert x S) T"  unfolding PiE_def extensional_def by autolemma fun_upd_in_PiE: "x ∉ S ==> f ∈ PiE (insert x S) T ==> f(x := undefined) ∈ PiE S T"  unfolding PiE_def extensional_def by autolemma 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)qedlemma PiE_Int: "(Pi⇣E I A) ∩ (Pi⇣E I B) = Pi⇣E I (λx. A x ∩ B x)"  by (auto simp: PiE_def)lemma PiE_cong:  "(!!i. i∈I ==> A i = B i) ==> Pi⇣E I A = Pi⇣E 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 autolemma 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: "Pi⇣E I F = Pi⇣E 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] guess f .. note f = this  then have "f ∈ Pi⇣E I F" by (auto simp: extensional_def PiE_def)  then have "f ∈ Pi⇣E I F'" using assms by simp  then show "x ∈ F' i" using f `i ∈ I` by (auto simp: PiE_def)qedlemma PiE_eq_iff_not_empty:  assumes ne: "!!i. i ∈ I ==> F i ≠ {}" "!!i. i ∈ I ==> F' i ≠ {}"  shows "Pi⇣E I F = Pi⇣E I F' <-> (∀i∈I. F i = F' i)"proof (intro iffI ballI)  fix i assume eq: "Pi⇣E I F = Pi⇣E 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 autoqed (auto simp: PiE_def)lemma PiE_eq_iff:  "Pi⇣E I F = Pi⇣E I F' <-> (∀i∈I. F i = F' i) ∨ ((∃i∈I. F i = {}) ∧ (∃i∈I. F' i = {}))"proof (intro iffI disjCI)  assume eq[simp]: "Pi⇣E I F = Pi⇣E 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 autonext  assume "(∀i∈I. F i = F' i) ∨ (∃i∈I. F i = {}) ∧ (∃i∈I. F' i = {})"  then show "Pi⇣E I F = Pi⇣E I F'"    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)qedlemma 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  donelemma 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 autosubsubsection {* 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)    doneqedlemma 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 × Pi⇣E S T)"proof (safe intro!: inj_onI ext)  fix f y g z assume "x ∉ S" and fg: "f ∈ Pi⇣E S T" "g ∈ Pi⇣E 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)qedlemma 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 autonext  case (insert x S) then show ?case    by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)qedend`