# Theory FuncSet

theory FuncSet
imports Main

section

theory FuncSet
imports Main
abbrevs PiE =
and PIE =
begin

definition Pi ::
where

definition extensional ::
where

definition  ::
where

abbreviation funcset ::   (infixr  60)
where

syntax
::   (   10)
::   ( [0,0,3] 3)
translations

definition  ::
where

subsection

lemma Pi_I[intro!]:

lemma Pi_I'[simp]:

lemma funcsetI:

lemma Pi_mem:

lemma Pi_iff:
unfolding Pi_def by auto

lemma PiE [elim]:
by (auto simp: Pi_def)

lemma Pi_cong:
by (auto simp: Pi_def)

lemma funcset_id [simp]:
by auto

lemma funcset_mem:

lemma funcset_image:
by auto

lemma image_subset_iff_funcset:
by auto

lemma Pi_eq_empty[simp]:
apply auto
txt
apply (drule_tac x =  in spec)
apply auto
apply (cut_tac P =  in some_eq_ex)
apply auto
done

lemma Pi_empty [simp]:

lemma Pi_Int:
by auto

lemma Pi_UN:
fixes A ::
assumes
and mono:
shows
proof (intro set_eqI iffI)
fix f
assume
then have
by auto
from bchoice[OF this] obtain n where n:  if  for i
by auto
obtain k where k:  if  for i
using  finite_nat_set_iff_bounded_le[of ] by auto
have
proof (intro Pi_I)
fix i
assume
from mono[OF this, of  k] k[OF this] n[OF this]
show  by auto
qed
then show
by auto
qed auto

lemma Pi_UNIV [simp]:

text
lemma Pi_mono:
by auto

text
lemma Pi_anti_mono:
by auto

lemma prod_final:
assumes 1:
and 2:
shows
proof (rule Pi_I)
fix z
assume z:
have
by simp
also have
by (metis SigmaI PiE o_apply 1 2 z)
finally show  .
qed

lemma Pi_split_domain[simp]:
by (auto simp: Pi_def)

lemma Pi_split_insert_domain[simp]:
by (auto simp: Pi_def)

lemma Pi_cancel_fupd_range[simp]:
by (auto simp: Pi_def)

lemma Pi_cancel_fupd[simp]:
by (auto simp: Pi_def)

lemma Pi_fupd_iff:
apply auto
apply (drule_tac x=x in Pi_mem)
apply (simp_all split: if_split_asm)
apply (drule_tac x=i in Pi_mem)
apply (auto dest!: Pi_mem)
done

subsection

lemma funcset_compose:
by (simp add: Pi_def compose_def restrict_def)

lemma compose_assoc:
assumes
and
and
shows
using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def)

lemma compose_eq:

lemma surj_compose:
by (auto simp add: image_def compose_eq)

subsection

lemma restrict_cong:
by (auto simp: restrict_def fun_eq_iff simp_implies_def)

lemma restrict_in_funcset:

lemma restrictI[intro!]:

lemma restrict_apply[simp]:

lemma restrict_apply':
by simp

lemma restrict_ext:
by (simp add: fun_eq_iff Pi_def restrict_def)

lemma restrict_UNIV:

lemma inj_on_restrict_eq [simp]:

lemma Id_compose:
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)

lemma compose_Id:
by (auto simp add: fun_eq_iff compose_def extensional_def Pi_def)

lemma image_restrict_eq [simp]:

lemma restrict_restrict[simp]:
unfolding restrict_def by (simp add: fun_eq_iff)

lemma restrict_fupd[simp]:
by (auto simp: restrict_def)

lemma restrict_upd[simp]:
by (auto simp: fun_eq_iff)

lemma restrict_Pi_cancel:
by (auto simp: restrict_def Pi_def)

subsection

text

lemma bij_betwI:
assumes
and
and g_f:
and f_g:
shows
unfolding bij_betw_def
proof
show
by (metis g_f inj_on_def)
have
using  by auto
moreover
have
by auto (metis Pi_mem  f_g image_iff)
ultimately show
by blast
qed

lemma bij_betw_imp_funcset:

lemma inj_on_compose:
by (auto simp add: bij_betw_def inj_on_def compose_eq)

lemma bij_betw_compose:
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]:

subsection

lemma extensional_empty[simp]:
unfolding extensional_def by auto

lemma extensional_arb:

lemma restrict_extensional [simp]:

lemma compose_extensional [simp]:

lemma extensionalityI:
assumes
and
and
shows
using assms by (force simp add: fun_eq_iff extensional_def)

lemma extensional_restrict:
by (rule extensionalityI[OF restrict_extensional]) auto

lemma extensional_subset:
unfolding extensional_def by auto

lemma inv_into_funcset:
by (unfold inv_into_def) (fast intro: someI2)

lemma compose_inv_into_id:
apply (rule restrict_ext, auto)
done

lemma compose_id_inv_into:
apply (rule restrict_ext)
done

lemma extensional_insert[intro, simp]:
assumes
shows
using assms unfolding extensional_def by auto

lemma extensional_Int[simp]:
unfolding extensional_def by auto

lemma extensional_UNIV[simp]:
by (auto simp: extensional_def)

lemma restrict_extensional_sub[intro]:
unfolding restrict_def extensional_def by auto

lemma extensional_insert_undefined[intro, simp]:

unfolding extensional_def by auto

lemma extensional_insert_cancel[intro, simp]:

unfolding extensional_def by auto

subsection

lemma card_inj:
by (rule card_inj_on_le) auto

lemma card_bij:
assumes
and
and
shows
using assms by (blast intro: card_inj order_antisym)

subsection

definition PiE ::
where

abbreviation

syntax
::   ( 10)
translations

abbreviation extensional_funcset ::  (infixr  60)
where

lemma extensional_funcset_def:

lemma PiE_empty_domain[simp]:
unfolding PiE_def by simp

lemma PiE_UNIV_domain:
unfolding PiE_def by simp

lemma PiE_empty_range[simp]:
unfolding PiE_def by auto

lemma PiE_eq_empty_iff:
proof
assume
show
proof (rule ccontr)
assume
then have
by auto
from choice[OF this]
obtain f where  ..
then have
by (auto simp: extensional_def PiE_def)
with  show False
by auto
qed
qed (auto simp: PiE_def)

lemma PiE_arb:
unfolding PiE_def by auto (auto dest!: extensional_arb)

lemma PiE_mem:
unfolding PiE_def by auto

lemma PiE_fun_upd:
unfolding PiE_def extensional_def by auto

lemma fun_upd_in_PiE:
unfolding PiE_def extensional_def by auto

lemma PiE_insert_eq:
proof -
{
fix f assume
then have
by (auto intro!: image_eqI[where x=] intro: fun_upd_in_PiE PiE_mem)
}
moreover
{
fix f assume
then have
by (auto intro!: image_eqI[where x=] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
}
ultimately show ?thesis
by (auto intro: PiE_fun_upd)
qed

lemma PiE_Int:
by (auto simp: PiE_def)

lemma PiE_cong:
unfolding PiE_def by (auto simp: Pi_cong)

lemma PiE_E [elim]:
assumes
obtains  and
|  and
using assms by (auto simp: Pi_def PiE_def extensional_def)

lemma PiE_I[intro!]:

lemma PiE_mono:
by auto

lemma PiE_iff:

lemma PiE_restrict[simp]:

lemma restrict_PiE[simp]:
by (auto simp: PiE_iff)

lemma PiE_eq_subset:
assumes ne:
and eq:
and
shows
proof
fix x
assume
with ne have
by auto
from choice[OF this] obtain f
where f:  ..
then have
by (auto simp: extensional_def PiE_def)
then have
using assms by simp
then show
using f  by (auto simp: PiE_def)
qed

lemma PiE_eq_iff_not_empty:
assumes ne:
shows
proof (intro iffI ballI)
fix i
assume eq:
assume i:
show
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:

proof (intro iffI disjCI)
assume eq[simp]:
assume
then have
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
by auto
next
assume
then show
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:

unfolding extensional_funcset_def extensional_def
apply auto
apply (case_tac )
apply auto
done

lemma extensional_funcset_fun_upd_extends_rangeI:
assumes
shows
using assms unfolding extensional_funcset_def extensional_def by auto

subsubsection

lemma extensional_funcset_fun_upd_inj_onI:
assumes
and
shows
using assms
unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)

lemma extensional_funcset_extend_domain_inj_on_eq:
assumes
shows
using assms
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= in exI)
apply (auto intro: PiE_mem del: PiE_I PiE_E)
apply (rule_tac x= in exI)
apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
apply (auto dest!: PiE_mem split: if_split_asm)
done

lemma extensional_funcset_extend_domain_inj_onI:
assumes
shows
using assms
apply (auto intro!: inj_onI)
apply (metis fun_upd_same)
apply (metis assms PiE_arb fun_upd_triv fun_upd_upd)
done

subsubsection

lemma finite_PiE:
by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)

lemma inj_combinator:
proof (safe intro!: inj_onI ext)
fix f y g z
assume
assume fg:
assume
then have *:
unfolding fun_eq_iff by auto
from this[of x] show  by simp
fix i from *[of i]  fg show
by (auto split: if_split_asm simp: PiE_def extensional_def)
qed

lemma card_PiE:
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