src/HOL/Library/Code_Natural.thy
changeset 38968 e55deaa22fff
parent 38857 97775f3e8722
child 39272 0b61951d2682
     1.1 --- a/src/HOL/Library/Code_Natural.thy	Wed Sep 01 09:03:34 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Natural.thy	Wed Sep 01 11:09:50 2010 +0200
     1.3 @@ -56,47 +56,45 @@
     1.4  code_reserved Haskell Natural
     1.5  
     1.6  code_include Scala "Natural"
     1.7 -{*import scala.Math
     1.8 -
     1.9 -object Nat {
    1.10 +{*object Natural {
    1.11  
    1.12 -  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    1.13 -  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    1.14 -  def apply(numeral: String): Nat = Nat(BigInt(numeral))
    1.15 +  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    1.16 +  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    1.17 +  def apply(numeral: String): Natural = Natural(BigInt(numeral))
    1.18  
    1.19  }
    1.20  
    1.21 -class Nat private(private val value: BigInt) {
    1.22 +class Natural private(private val value: BigInt) {
    1.23  
    1.24    override def hashCode(): Int = this.value.hashCode()
    1.25  
    1.26    override def equals(that: Any): Boolean = that match {
    1.27 -    case that: Nat => this equals that
    1.28 +    case that: Natural => this equals that
    1.29      case _ => false
    1.30    }
    1.31  
    1.32    override def toString(): String = this.value.toString
    1.33  
    1.34 -  def equals(that: Nat): Boolean = this.value == that.value
    1.35 +  def equals(that: Natural): Boolean = this.value == that.value
    1.36  
    1.37    def as_BigInt: BigInt = this.value
    1.38    def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    1.39        this.value.intValue
    1.40      else error("Int value out of range: " + this.value.toString)
    1.41  
    1.42 -  def +(that: Nat): Nat = new Nat(this.value + that.value)
    1.43 -  def -(that: Nat): Nat = Nat(this.value - that.value)
    1.44 -  def *(that: Nat): Nat = new Nat(this.value * that.value)
    1.45 +  def +(that: Natural): Natural = new Natural(this.value + that.value)
    1.46 +  def -(that: Natural): Natural = Natural(this.value - that.value)
    1.47 +  def *(that: Natural): Natural = new Natural(this.value * that.value)
    1.48  
    1.49 -  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
    1.50 +  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    1.51      else {
    1.52        val (k, l) = this.value /% that.value
    1.53 -      (new Nat(k), new Nat(l))
    1.54 +      (new Natural(k), new Natural(l))
    1.55      }
    1.56  
    1.57 -  def <=(that: Nat): Boolean = this.value <= that.value
    1.58 +  def <=(that: Natural): Boolean = this.value <= that.value
    1.59  
    1.60 -  def <(that: Nat): Boolean = this.value < that.value
    1.61 +  def <(that: Natural): Boolean = this.value < that.value
    1.62  
    1.63  }
    1.64  *}
    1.65 @@ -105,7 +103,7 @@
    1.66  
    1.67  code_type code_numeral
    1.68    (Haskell "Natural.Natural")
    1.69 -  (Scala "Natural.Nat")
    1.70 +  (Scala "Natural")
    1.71  
    1.72  setup {*
    1.73    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}