[Rodin-b-sharp-user] Induction in proof

[George Z. <gg...@gm...>]

Hi all,

Im new to Rodin/event-b and have been exploring the interactive proof
system. I found myself stuck while trying to apply induction.

In the following, I define a set of natural numbers, mappings to/from this
set into the builtin set of natural numbers and show that it defines the
same set. However, when attempting to show that the mappings are
isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their
proofs require the induction hypothesis.

    CONTEXT
        Nat     ›
    SETS
        Nat     ›
    CONSTANTS
        zero     ›
        suc     ›
        toNat     ›
        fromNat     ›
        S     ›
    AXIOMS
        axm1:    zero ∈ Nat not theorem ›
        axm2:    suc ∈ Nat → Nat not theorem ›
        axm3:    toNat ∈ ℕ → Nat not theorem ›
        axm4:    toNat(0) = zero not theorem ›
        axm5:    ∀ n · n ∈ ℕ ⇒ toNat(n + 1) = suc(toNat(n)) not theorem ›
        axm6:    toNat(1) = suc(zero) theorem ›
        axm7:    fromNat ∈ Nat → ℕ not theorem ›
        axm8:    fromNat(zero) = 0 not theorem ›
        axm9:    ∀ n · n ∈ Nat ⇒ fromNat(suc(n)) = fromNat(n) + 1 not
theorem ›
        axm10:    fromNat(suc(zero)) = 1 theorem ›
        axm11:    ∀ s · s ⊆ ℕ ∧ 0 ∈ s ∧ (∀ n · n ∈ s ⇒ n + 1 ∈ s) ⇒ ℕ ⊆ s
not theorem ›
        axm12:    ∀ n · n ∈ ℕ ⇒ n = 0 ∨ (∃ m · m ∈ ℕ ∧ n = m + 1) theorem ›
        axm13:    S = { n ∣ n ∈ ℕ ∧ (∃ x · x ∈ Nat ∧ n = fromNat(x)) } not
theorem ›
        axm14:    S ⊆ ℕ theorem ›
        axm15:    0 ∈ S theorem ›
        axm16:    ∀ s · s ∈ S ⇒ s + 1 ∈ S theorem ›
        axm17:    ℕ ⊆ S theorem ›
        axm18:    ∀ n · n ∈ ℕ ⇒ fromNat(toNat(n)) = n theorem ›
        axm19:    ∀ x · x ∈ Nat ⇒ x = zero ∨ (∃ y · y ∈ Nat ∧ x = suc(y))
not theorem ›
        axm20:    ∀ x · x ∈ Nat ⇒ toNat(fromNat(x)) = x theorem ›
    END


A second small query I have is whether there is support for a type of all
sets? E.g. it is possible to write something of the form:
∀ A , B , f , a , a' · A ∈ SET ∧ B ∈ SET ∧ f ∈ A → B ∧ a ∈ A ∧ a' ∈ A ∧ a =
a' ⇒ f(a) = f(a')

Thanks,
George