header {* An example of generalization *}
theory int_obj_ex
imports Generalization
begin
text {*
In this example I show that integers can be considered as a generalization of natural numbers.
*}
interpretation int_interpr: ZF_generalization "nat" "int" "(lam n:nat. int_of(n))"
proof
show "Lambda(nat, int_of)∈inj(nat, int)" using int_of_inject unfolding inj_def by auto
qed
abbreviation "int_obj ≡ int_interpr.newbig_param"
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::"[i,i]=>i"
where "add(x,y) == int_interpr.move_param`(int_interpr.ret`x $+ int_interpr.ret`y)"
end