Definition natural number "1,2,3,4,5,6,7,8,9,10"

[CoghettoR]

Can you help me find, in ZF or IzarMathLib the definition of the natural numbers "3,4,5,6,7,8,9,10" (using succ)?

I already found "1" and "2" in ZF.Bool.thy

abbreviation
  one (<1>) where
  "1 ≡ succ(0)"

abbreviation
  two (<2>) where
  "2 ≡ succ(1)"

I already found "2"..."9" in IsarMathLib.Complex_ZF.thy

 fixes two ("𝟮")
  defines two_def[simp]: "𝟮 ≡ 𝟭 \<ca> 𝟭"

  fixes three ("𝟯")
  defines three_def[simp]: "𝟯 ≡ 𝟮\<ca>𝟭"

  fixes four ("𝟰")
  defines four_def[simp]: "𝟰 ≡ 𝟯\<ca>𝟭"

  fixes five ("𝟱")
  defines five_def[simp]: "𝟱 ≡ 𝟰\<ca>𝟭"

  fixes six ("𝟲")
  defines six_def[simp]: "𝟲 ≡ 𝟱\<ca>𝟭"

  fixes seven ("𝟳")
  defines seven_def[simp]: "𝟳 ≡ 𝟲\<ca>𝟭"

  fixes eight ("𝟴")
  defines eight_def[simp]: "𝟴 ≡ 𝟳\<ca>𝟭"

  fixes nine ("𝟵")
  defines nine_def[simp]: "𝟵 ≡ 𝟴\<ca>𝟭"

Informally, I suspect that the definitions for 1 and 2 are equivalent but I can't show it formally. Any help is welcome. Thank you in advance.

[dan323]

I do not understand your question.

[CoghettoR]

1. I am looking for the following definitions, if they exist, in Isabelle.ZF (or IsarMathLib)

abbreviation
  three (<3>) where
  "3 ≡ succ(2)"
abbreviation
  four (<4>) where
  "4 ≡ succ(3)"
abbreviation
  five (<5>) where
  "5 ≡ succ(4)"
[...]

2. I am looking for a bijection/equivalence between these numbers and the following natural numbers defined otherwise:

0⇩R

fixes rone ("𝟭⇩R")
  defines rone_def[simp]: "𝟭⇩R ≡ TheNeutralElement(R,M)"
[...]

and

0 

abbreviation
  one (<1>) where
  "1 ≡ succ(0)"
[...]

3. I am looking for an equivalence between the addition of the natural numbers defined by "succ" with the addition of the natural numbers contained in the reals as defined in IsarMathLib ("IsAmodelOfReals").

[SKolodynski]

My apologies for not responding sooner, I forgot to update my e-mail on GitHub and I was not getting notifications for a couple of months. Indeed, mathematicians like to think that the natural numbers 0, 1, 1+1, ... embedded in reals and the natural numbers of the set theory (i.e. 0, {0},{0,{0}}, ...) are kind of the same in the sense that if we prove something about the former we automatically get the analogue for the latter. I am guessing that in Mizar with its soft typing system it is probably possible. In Isabelle/ZF the best approximation (that I can think of) is through locales and the sublocale command. The sublocale command expresses the idea "the theorems proven in this context are valid in that context when applied to these objects with notation mapped like this". In case of natural numbers one would set up a locale called presburger that assumes Presburger Arithmetic axioms and show some theorems there. Then one could prove a sublocale real0 < presburger ... statement about the natural numbers embedded in reals. This set would be probably defined using the notion of InductiveSequence. All this has not been done yet in IsarMathLib.

[SKolodynski]

Actually I have noticed that IsarMathLib does have a definition of natural numbers embedded in reals in the MMIsar0 locale (please ignore that error message on the page, I have to fix that). I will copy that definition to the real0 locale before the next release.