Theory ZF_Addons

Up to index of Isabelle/ZF/gen

theory ZF_Addons
imports Main_ZF

header {* Some addons to Isabelle/ZF *}

theory ZF_Addons
imports Main_ZF
begin


text {* We need to add some additional lemmas to Isabelle/ZF before proceed. *}

(** Proof by Larry Paulson **)
lemma inj_inj_range: "f∈inj(A,B) ==> f∈inj(A,range(f))"
apply (unfold inj_def)
apply (auto simp add: Pi_iff function_def)
done

(** Proof by Larry Paulson **)
lemma inj_bij_range: "f∈inj(A,B) ==> f∈bij(A,range(f))"
apply (auto simp add: bij_def inj_inj_range)
apply (blast intro: inj_is_fun fun_is_surj elim:)
done

lemma range_subset: "f: A->B ==> range(f) ⊆ B"
proof -
assume "f: A->B"
hence "f∈Pow(A×B)" by (simp add: Pi_def)
hence "f ⊆ A×B" by auto
moreover
hence "range(A×B) ⊆ B" by auto
ultimately show "range(f) ⊆ B" by auto
qed

lemma lam_is_fun: "f = (lam x:d. b(x)) ==> f: d->range(f)"
proof -
assume eq: "f = (lam x:d. b(x))"
have dom: "domain(f) = d" using domain_lam by (auto simp add: eq)
with eq have "function(f)" using function_lam by auto
moreover
with eq have "relation(f)" using relation_lam by auto
ultimately have "f: domain(f)->range(f)" by (rule function_imp_Pi)
with dom show ?thesis by auto
qed

lemma comp_fun2:
"[| g: A->B1; f: B0->C; B1⊆B0 |] ==> (f O g) : A->C"

proof -
assume "g: A->B1" "f: B0->C" "B1⊆B0"
with `g: A->B1` have "g: A->B0" by auto (rule fun_weaken_type)
from `g: A->B0` `f: B0->C` show "(f O g) : A->C" using comp_fun by auto
qed

text {*
This lemma superceedes the lemma @{term comp_eq_id_iff} in Isabelle/ZF:
*}

lemma comp_eq_id_iff1:
"[| g: B->A; f: A->C |] ==> (∀y∈B. f`(g`y) = y) <-> f O g = id(B)"

proof -
assume "g: B->A" "f: A->C"
hence "f O g: B->C" by (rule comp_fun)
moreover
have "id(B): B->B" by (rule id_type)
ultimately have m: "(∀y∈B. (f O g)`y = id(B)`y) <-> f O g = id(B)" by (rule fun_extension_iff)
from `g: B->A` have c [simp]: "∀y∈B. (f O g)`y = f`(g`y)" by auto
have i [simp]: "∀y∈B. id(B)`y = y" by auto
from m show "(∀y∈B. f`(g`y) = y) <-> f O g = id(B)" by simp
qed

lemma right_comp_id_any: "r O id(C) = restrict(r,C)"
unfolding restrict_def by auto

end