Theory NatGenIntEx_ZF
section ‹Generalizations - an example application›
theory NatGenIntEx_ZF imports ZF.Int Generalization_ZF
begin
text‹This theory shows an example application of of the setup for
generalization presented in ‹Generalization_ZF.››
text ‹In this example I show that integers can be considered
as a generalization of natural numbers. The next ‹interpretion›
shows that we can use theorems proven in the ‹generalization›
locale to sets ‹nat›, ‹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 ‹generalization1› locale
from within ‹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