header {*\isaheader{NatGenIntEx\_ZF.thy} *}
theory NatGenIntEx_ZF imports Int_ZF Generalization_ZF
begin
text{*This theory shows an example application of of the setup for
generalization presented in @{text "Generalization_ZF."}*}
text {* In this example I show that integers can be considered
as a generalization of natural numbers. The next @{text "interpretion"}
shows that we can use theorems proven in the @{text "generalization"}
locale to sets @{text "nat"}, @{text "int"} and the natural embedding
of natural numbers into integers.*}
interpretation int_interpr:
generalization "nat" "int" "{⟨n,int_of(n)⟩. n ∈ nat}"
proof -
let ?f = "{⟨n,int_of(n)⟩. n ∈ nat}"
have "?f ∈ inj(nat,int)"
proof -
have I: "?f: nat → int" using ZF_fun_from_total by simp
moreover from I have "∀n∈nat. ?f`(n)= int_of(n)"
using ZF_fun_from_tot_val by simp
moreover have "∀n∈nat.∀m∈nat. int_of(n)=int_of(m) ⟶ n=m"
using int_of_inject by simp
ultimately show ?thesis using inj_def by simp
qed
then show "generalization(nat,int,?f)" using generalization_def by simp
qed
text {*Next we prove that ZF generalization is an arbitrary generalization.
This allows to access notions defined in @{text "generalization1"} locale
from within @{text "generalization"} locale.*}
sublocale
generalization ⊆ generalization1 small big embed zf_newbig zf_move
proof
show "zf_move∈bij(big, zf_newbig)" using zf_move_bij by auto
show "zf_move O embed = id(small)" using zf_embed_move by auto
qed
abbreviation "int_obj ≡ int_interpr.zf_newbig"
text {* Naturals are a subset of integers.*}
lemma "nat ⊆ int_obj" using int_interpr.small_less_zf_newbig by auto
text {*An example of defining an operation on the generalization set.*}
definition add where
"add(x,y) ≡ int_interpr.zf_move`(int_interpr.ret`x $+ int_interpr.ret`y)"
end