src/HOL/Library/Code_Natural.thy
changeset 39007 567b94f8bb6e
parent 39004 f9cd27cbe8a4
child 39008 741ca0c98f6f
equal deleted inserted replaced
39006:f9837065b5e8 39007:567b94f8bb6e
     7 begin
     7 begin
     8 
     8 
     9 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
     9 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
    10 
    10 
    11 code_include Haskell "Natural"
    11 code_include Haskell "Natural"
    12 {*import Data.Array.ST;
    12 {*newtype Natural = Natural Integer deriving (Eq, Show, Read);
    13 
       
    14 newtype Natural = Natural Integer deriving (Eq, Show, Read);
       
    15 
    13 
    16 instance Num Natural where {
    14 instance Num Natural where {
    17   fromInteger k = Natural (if k >= 0 then k else 0);
    15   fromInteger k = Natural (if k >= 0 then k else 0);
    18   Natural n + Natural m = Natural (n + m);
    16   Natural n + Natural m = Natural (n + m);
    19   Natural n - Natural m = fromInteger (n - m);
    17   Natural n - Natural m = fromInteger (n - m);
    52     | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
    50     | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
    53 };*}
    51 };*}
    54 
    52 
    55 code_reserved Haskell Natural
    53 code_reserved Haskell Natural
    56 
    54 
    57 code_include Scala "Natural" {*
    55 code_include Scala "Natural"
    58 import scala.Math
    56 {*import scala.Math
    59 
    57 
    60 object Nat {
    58 object Nat {
    61 
    59 
    62   def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    60   def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    63   def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    61   def apply(numeral: Int): Nat = Nat(BigInt(numeral))