# Theory HyperArith

Up to index of Isabelle/HOL/HOL-Complex

theory HyperArith
imports HyperDef
uses (hypreal_arith.ML)
begin

    (*  Title:      HOL/HyperArith.thy
        ID:         $Id: HyperArith.thy,v 1.18 2005/09/15 21:46:22 huffman Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1999  University of Cambridge
    *)

    header{*Binary arithmetic and Simplification for the Hyperreals*}

    theory HyperArith
    imports HyperDef
    uses ("hypreal_arith.ML")
    begin

    subsection{*Numerals and Arithmetic*}

    use "hypreal_arith.ML"

    setup hypreal_arith_setup

    subsection{*Absolute Value Function for the Hyperreals*}

    lemma hrabs_add_less:
         "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
    by (simp add: abs_if split: split_if_asm)

    text{*used once in NSA*}
    lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
    by (blast intro!: order_le_less_trans abs_ge_zero)

    lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x"
    by (simp add: abs_if)

    (* Needed in Geom.ML *)
    lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
    by (simp add: abs_if split add: split_if_asm)

    lemma hypreal_of_real_hrabs:
        "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
    by (rule star_of_abs [symmetric])

    subsection{*Embedding the Naturals into the Hyperreals*}

    constdefs
      hypreal_of_nat   :: "nat => hypreal"
       "hypreal_of_nat m == of_nat m"

    lemma SNat_eq: "Nats = {n. ∃N. n = hypreal_of_nat N}"
    by (force simp add: hypreal_of_nat_def Nats_def)

    lemma hypreal_of_nat_add [simp]:
         "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n"
    by (simp add: hypreal_of_nat_def)

    lemma hypreal_of_nat_mult: "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n"
    by (simp add: hypreal_of_nat_def)
    declare hypreal_of_nat_mult [simp]

    lemma hypreal_of_nat_less_iff:
          "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"
    apply (simp add: hypreal_of_nat_def)
    done
    declare hypreal_of_nat_less_iff [symmetric, simp]

    (*------------------------------------------------------------*)
    (* naturals embedded in hyperreals                            *)
    (* is a hyperreal c.f. NS extension                           *)
    (*------------------------------------------------------------*)

    lemma hypreal_of_nat_eq:
         "hypreal_of_nat (n::nat) = hypreal_of_real (real n)"
    apply (induct n)
    apply (simp_all add: hypreal_of_nat_def real_of_nat_def)
    done

    lemma hypreal_of_nat:
         "hypreal_of_nat m = star_n (%n. real m)"
    apply (fold star_of_def)
    apply (induct m)
    apply (simp_all add: hypreal_of_nat_def real_of_nat_def star_n_add)
    done

    lemma hypreal_of_nat_Suc:
         "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
    by (simp add: hypreal_of_nat_def)

    (*"neg" is used in rewrite rules for binary comparisons*)
    lemma hypreal_of_nat_number_of [simp]:
         "hypreal_of_nat (number_of v :: nat) =
             (if neg (number_of v :: int) then 0
              else (number_of v :: hypreal))"
    by (simp add: hypreal_of_nat_eq)

    lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
    by (simp add: hypreal_of_nat_def)

    lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
    by (simp add: hypreal_of_nat_def)

    lemma hypreal_of_nat_le_iff [simp]:
         "(hypreal_of_nat n ≤ hypreal_of_nat m) = (n ≤ m)"
    by (simp add: hypreal_of_nat_def)

    lemma hypreal_of_nat_ge_zero [simp]: "0 ≤ hypreal_of_nat n"
    by (simp add: hypreal_of_nat_def)

    (*
    FIXME: we should declare this, as for type int, but many proofs would break.
    It replaces x+-y by x-y.
    Addsimps [symmetric hypreal_diff_def]
    *)

    ML
    {*
    val hypreal_of_nat_def = thm"hypreal_of_nat_def";

    val hrabs_add_less = thm "hrabs_add_less";
    val hrabs_disj = thm "hrabs_disj";
    val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj";
    val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs";
    val hypreal_of_nat_add = thm "hypreal_of_nat_add";
    val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
    val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
    val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
    val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
    val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
    val hypreal_of_nat_one = thm "hypreal_of_nat_one";
    val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
    val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
    val hypreal_of_nat = thm"hypreal_of_nat";
    *}

    end

### Numerals and Arithmetic

### Absolute Value Function for the Hyperreals

lemma hrabs_add_less:

      [| ¦x¦ < r; ¦y¦ < s |] ==> ¦x + y¦ < r + s

lemma hrabs_less_gt_zero:

      ¦x¦ < r ==> 0 < r

lemma hrabs_disj:

      ¦x¦ = x ∨ ¦x¦ = - x

lemma hrabs_add_lemma_disj:

      y + - x + (y + - z) = ¦x + - z¦ ==> y = z ∨ x = y

lemma hypreal_of_real_hrabs:

      ¦star_of r¦ = star_of ¦r¦

### Embedding the Naturals into the Hyperreals

lemma SNat_eq:

      Nats = {n. ∃N. n = hypreal_of_nat N}

lemma hypreal_of_nat_add:

      hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n

lemma hypreal_of_nat_mult:

      hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n

lemma hypreal_of_nat_less_iff:

      (n < m) = (hypreal_of_nat n < hypreal_of_nat m)

lemma hypreal_of_nat_eq:

      hypreal_of_nat n = star_of (real n)

lemma hypreal_of_nat:

      hypreal_of_nat m = star_n (%n. real m)

lemma hypreal_of_nat_Suc:

      hypreal_of_nat (Suc n) = hypreal_of_nat n + 1

lemma hypreal_of_nat_number_of:

      hypreal_of_nat (number_of v) = (if neg (number_of v) then 0 else number_of v)

lemma hypreal_of_nat_zero:

      hypreal_of_nat 0 = 0

lemma hypreal_of_nat_one:

      hypreal_of_nat 1 = 1

lemma hypreal_of_nat_le_iff:

      (hypreal_of_nat n ≤ hypreal_of_nat m) = (n ≤ m)

lemma hypreal_of_nat_ge_zero:

      0 ≤ hypreal_of_nat n