Theory int_obj_ex

Up to index of Isabelle/ZF/gen

theory int_obj_ex
imports Generalization

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