### Abstract

We apply data refinement to implement the real numbers, where we support all numbers in the field extension Q[sqrt(b)], i.e., all numbers of the form p + q * sqrt(b) for rational numbers p and q and some fixed natural number b. To this end, we also developed algorithms to precisely compute roots of a rational number, and to perform a factorization of natural numbers which eliminates duplicate prime factors.

Our results have been used to certify termination proofs which involve polynomial interpretations over the reals.

### License

GNU Lesser General Public License (LGPL)

### History

July 11, 2014
  Moved NthRoot_Impl to Sqrt-Babylonian.

### Topics

- Mathematics/Analysis

### Session Real_Impl

- Real_Impl_Auxiliary
- Prime_Product
- Real_Impl
- Real_Unique_Impl

### Depends on

- Deriving class instances for datatypes
- Haskell’s Show Class in Isabelle/HOL
- Computing N-th Roots using the Babylonian Method

### Used by

- Complex Bounded Operators
- QR Decomposition

### Auto-related entries

- Real Exponents as the Limits of Sequences of Rational Exponents

## Cite

×

Real_Impl-AFP

    @article{Real_Impl-AFP,
      author  = {René Thiemann},
      title   = {Implementing field extensions of the form Q[sqrt(b)]},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Real_Impl.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Feb 11, 2014 : Isabelle2013-2