added Code_Natural.thy
authorhaftmann
Mon Jul 26 11:10:35 2010 +0200 (2010-07-26 ago)
changeset 3796852fdcb76c0af
parent 37967 3e174df3f965
child 37969 3bf1fffcdd48
added Code_Natural.thy
src/HOL/IsaMakefile
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Code_Natural.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Jul 26 11:09:45 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jul 26 11:10:35 2010 +0200
     1.3 @@ -398,20 +398,19 @@
     1.4  $(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML		\
     1.5    $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
     1.6    Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
     1.7 -  Library/AssocList.thy							\
     1.8 -  Library/BigO.thy Library/Binomial.thy Library/Bit.thy			\
     1.9 -  Library/Boolean_Algebra.thy Library/Cardinality.thy			\
    1.10 +  Library/AssocList.thy	Library/BigO.thy Library/Binomial.thy		\
    1.11 +  Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
    1.12    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
    1.13 -  Library/Code_Integer.thy Library/ContNotDenum.thy			\
    1.14 -  Library/Continuity.thy Library/Convex.thy Library/Countable.thy	\
    1.15 -  Library/Diagonalize.thy Library/Dlist.thy Library/Efficient_Nat.thy	\
    1.16 -  Library/Enum.thy Library/Eval_Witness.thy Library/Executable_Set.thy	\
    1.17 -  Library/Float.thy Library/Formal_Power_Series.thy			\
    1.18 -  Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Fset.thy	\
    1.19 -  Library/FuncSet.thy Library/Fundamental_Theorem_Algebra.thy		\
    1.20 -  Library/Glbs.thy Library/Indicator_Function.thy			\
    1.21 -  Library/Infinite_Set.thy Library/Inner_Product.thy			\
    1.22 -  Library/Kleene_Algebra.thy						\
    1.23 +  Library/Code_Integer.thy Library/Code_Natural.thy			\
    1.24 +  Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
    1.25 +  Library/Countable.thy	Library/Diagonalize.thy Library/Dlist.thy	\
    1.26 +  Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
    1.27 +  Library/Executable_Set.thy Library/Float.thy				\
    1.28 +  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
    1.29 +  Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\
    1.30 +  Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
    1.31 +  Library/Indicator_Function.thy Library/Infinite_Set.thy		\
    1.32 +  Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
    1.33    Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
    1.34    Library/Lattice_Syntax.thy Library/Library.thy			\
    1.35    Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
     2.1 --- a/src/HOL/Library/Code_Integer.thy	Mon Jul 26 11:09:45 2010 +0200
     2.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Jul 26 11:10:35 2010 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Pretty integer literals for code generation *}
     2.5  
     2.6  theory Code_Integer
     2.7 -imports Main
     2.8 +imports Main Code_Natural
     2.9  begin
    2.10  
    2.11  text {*
    2.12 @@ -14,142 +14,6 @@
    2.13    operations for abstract integer operations.
    2.14  *}
    2.15  
    2.16 -text {*
    2.17 -  Preliminary: alternative representation of @{typ code_numeral}
    2.18 -  for @{text Haskell} and @{text Scala}.
    2.19 -*}
    2.20 -
    2.21 -code_include Haskell "Natural" {*
    2.22 -newtype Natural = Natural Integer deriving (Eq, Show, Read);
    2.23 -
    2.24 -instance Num Natural where {
    2.25 -  fromInteger k = Natural (if k >= 0 then k else 0);
    2.26 -  Natural n + Natural m = Natural (n + m);
    2.27 -  Natural n - Natural m = fromInteger (n - m);
    2.28 -  Natural n * Natural m = Natural (n * m);
    2.29 -  abs n = n;
    2.30 -  signum _ = 1;
    2.31 -  negate n = error "negate Natural";
    2.32 -};
    2.33 -
    2.34 -instance Ord Natural where {
    2.35 -  Natural n <= Natural m = n <= m;
    2.36 -  Natural n < Natural m = n < m;
    2.37 -};
    2.38 -
    2.39 -instance Real Natural where {
    2.40 -  toRational (Natural n) = toRational n;
    2.41 -};
    2.42 -
    2.43 -instance Enum Natural where {
    2.44 -  toEnum k = fromInteger (toEnum k);
    2.45 -  fromEnum (Natural n) = fromEnum n;
    2.46 -};
    2.47 -
    2.48 -instance Integral Natural where {
    2.49 -  toInteger (Natural n) = n;
    2.50 -  divMod n m = quotRem n m;
    2.51 -  quotRem (Natural n) (Natural m)
    2.52 -    | (m == 0) = (0, Natural n)
    2.53 -    | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
    2.54 -};
    2.55 -*}
    2.56 -
    2.57 -code_reserved Haskell Natural
    2.58 -
    2.59 -code_include Scala "Natural" {*
    2.60 -import scala.Math
    2.61 -
    2.62 -object Natural {
    2.63 -
    2.64 -  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    2.65 -  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    2.66 -  def apply(numeral: String): Natural = Natural(BigInt(numeral))
    2.67 -
    2.68 -}
    2.69 -
    2.70 -class Natural private(private val value: BigInt) {
    2.71 -
    2.72 -  override def hashCode(): Int = this.value.hashCode()
    2.73 -
    2.74 -  override def equals(that: Any): Boolean = that match {
    2.75 -    case that: Natural => this equals that
    2.76 -    case _ => false
    2.77 -  }
    2.78 -
    2.79 -  override def toString(): String = this.value.toString
    2.80 -
    2.81 -  def equals(that: Natural): Boolean = this.value == that.value
    2.82 -
    2.83 -  def as_BigInt: BigInt = this.value
    2.84 -  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    2.85 -      this.value.intValue
    2.86 -    else this.value.intValue
    2.87 -
    2.88 -  def +(that: Natural): Natural = new Natural(this.value + that.value)
    2.89 -  def -(that: Natural): Natural = Natural(this.value - that.value)
    2.90 -  def *(that: Natural): Natural = new Natural(this.value * that.value)
    2.91 -
    2.92 -  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    2.93 -    else {
    2.94 -      val (k, l) = this.value /% that.value
    2.95 -      (new Natural(k), new Natural(l))
    2.96 -    }
    2.97 -
    2.98 -  def <=(that: Natural): Boolean = this.value <= that.value
    2.99 -
   2.100 -  def <(that: Natural): Boolean = this.value < that.value
   2.101 -
   2.102 -}
   2.103 -*}
   2.104 -
   2.105 -code_reserved Scala Natural
   2.106 -
   2.107 -code_type code_numeral
   2.108 -  (Haskell "Natural.Natural")
   2.109 -  (Scala "Natural")
   2.110 -
   2.111 -setup {*
   2.112 -  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
   2.113 -    false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
   2.114 -*}
   2.115 -
   2.116 -code_instance code_numeral :: eq
   2.117 -  (Haskell -)
   2.118 -
   2.119 -code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   2.120 -  (Haskell infixl 6 "+")
   2.121 -  (Scala infixl 7 "+")
   2.122 -
   2.123 -code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   2.124 -  (Haskell infixl 6 "-")
   2.125 -  (Scala infixl 7 "-")
   2.126 -
   2.127 -code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   2.128 -  (Haskell infixl 7 "*")
   2.129 -  (Scala infixl 8 "*")
   2.130 -
   2.131 -code_const div_mod_code_numeral
   2.132 -  (Haskell "divMod")
   2.133 -  (Scala infixl 8 "/%")
   2.134 -
   2.135 -code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   2.136 -  (Haskell infixl 4 "==")
   2.137 -  (Scala infixl 5 "==")
   2.138 -
   2.139 -code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   2.140 -  (Haskell infix 4 "<=")
   2.141 -  (Scala infixl 4 "<=")
   2.142 -
   2.143 -code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   2.144 -  (Haskell infix 4 "<")
   2.145 -  (Scala infixl 4 "<")
   2.146 -
   2.147 -text {*
   2.148 -  Setup for @{typ int} proper.
   2.149 -*}
   2.150 -
   2.151 -
   2.152  code_type int
   2.153    (SML "IntInf.int")
   2.154    (OCaml "Big'_int.big'_int")
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Code_Natural.thy	Mon Jul 26 11:10:35 2010 +0200
     3.3 @@ -0,0 +1,145 @@
     3.4 +(*  Title:      HOL/Library/Code_Natural.thy
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +theory Code_Natural
     3.9 +imports Main
    3.10 +begin
    3.11 +
    3.12 +section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
    3.13 +
    3.14 +code_include Haskell "Natural"
    3.15 +{*import Data.Array.ST;
    3.16 +
    3.17 +newtype Natural = Natural Integer deriving (Eq, Show, Read);
    3.18 +
    3.19 +instance Num Natural where {
    3.20 +  fromInteger k = Natural (if k >= 0 then k else 0);
    3.21 +  Natural n + Natural m = Natural (n + m);
    3.22 +  Natural n - Natural m = fromInteger (n - m);
    3.23 +  Natural n * Natural m = Natural (n * m);
    3.24 +  abs n = n;
    3.25 +  signum _ = 1;
    3.26 +  negate n = error "negate Natural";
    3.27 +};
    3.28 +
    3.29 +instance Ord Natural where {
    3.30 +  Natural n <= Natural m = n <= m;
    3.31 +  Natural n < Natural m = n < m;
    3.32 +};
    3.33 +
    3.34 +instance Ix Natural where {
    3.35 +  range (Natural n, Natural m) = map Natural (range (n, m));
    3.36 +  index (Natural n, Natural m) (Natural q) = index (n, m) q;
    3.37 +  inRange (Natural n, Natural m) (Natural q) = inRange (n, m) q;
    3.38 +  rangeSize (Natural n, Natural m) = rangeSize (n, m);
    3.39 +};
    3.40 +
    3.41 +instance Real Natural where {
    3.42 +  toRational (Natural n) = toRational n;
    3.43 +};
    3.44 +
    3.45 +instance Enum Natural where {
    3.46 +  toEnum k = fromInteger (toEnum k);
    3.47 +  fromEnum (Natural n) = fromEnum n;
    3.48 +};
    3.49 +
    3.50 +instance Integral Natural where {
    3.51 +  toInteger (Natural n) = n;
    3.52 +  divMod n m = quotRem n m;
    3.53 +  quotRem (Natural n) (Natural m)
    3.54 +    | (m == 0) = (0, Natural n)
    3.55 +    | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
    3.56 +};*}
    3.57 +
    3.58 +code_reserved Haskell Natural
    3.59 +
    3.60 +code_include Scala "Natural" {*
    3.61 +import scala.Math
    3.62 +
    3.63 +object Natural {
    3.64 +
    3.65 +  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    3.66 +  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    3.67 +  def apply(numeral: String): Natural = Natural(BigInt(numeral))
    3.68 +
    3.69 +}
    3.70 +
    3.71 +class Natural private(private val value: BigInt) {
    3.72 +
    3.73 +  override def hashCode(): Int = this.value.hashCode()
    3.74 +
    3.75 +  override def equals(that: Any): Boolean = that match {
    3.76 +    case that: Natural => this equals that
    3.77 +    case _ => false
    3.78 +  }
    3.79 +
    3.80 +  override def toString(): String = this.value.toString
    3.81 +
    3.82 +  def equals(that: Natural): Boolean = this.value == that.value
    3.83 +
    3.84 +  def as_BigInt: BigInt = this.value
    3.85 +  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    3.86 +      this.value.intValue
    3.87 +    else error("Int value out of range: " + this.value.toString)
    3.88 +
    3.89 +  def +(that: Natural): Natural = new Natural(this.value + that.value)
    3.90 +  def -(that: Natural): Natural = Natural(this.value - that.value)
    3.91 +  def *(that: Natural): Natural = new Natural(this.value * that.value)
    3.92 +
    3.93 +  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    3.94 +    else {
    3.95 +      val (k, l) = this.value /% that.value
    3.96 +      (new Natural(k), new Natural(l))
    3.97 +    }
    3.98 +
    3.99 +  def <=(that: Natural): Boolean = this.value <= that.value
   3.100 +
   3.101 +  def <(that: Natural): Boolean = this.value < that.value
   3.102 +
   3.103 +}
   3.104 +*}
   3.105 +
   3.106 +code_reserved Scala Natural
   3.107 +
   3.108 +code_type code_numeral
   3.109 +  (Haskell "Natural.Natural")
   3.110 +  (Scala "Natural")
   3.111 +
   3.112 +setup {*
   3.113 +  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
   3.114 +    false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
   3.115 +*}
   3.116 +
   3.117 +code_instance code_numeral :: eq
   3.118 +  (Haskell -)
   3.119 +
   3.120 +code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   3.121 +  (Haskell infixl 6 "+")
   3.122 +  (Scala infixl 7 "+")
   3.123 +
   3.124 +code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   3.125 +  (Haskell infixl 6 "-")
   3.126 +  (Scala infixl 7 "-")
   3.127 +
   3.128 +code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   3.129 +  (Haskell infixl 7 "*")
   3.130 +  (Scala infixl 8 "*")
   3.131 +
   3.132 +code_const div_mod_code_numeral
   3.133 +  (Haskell "divMod")
   3.134 +  (Scala infixl 8 "/%")
   3.135 +
   3.136 +code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   3.137 +  (Haskell infixl 4 "==")
   3.138 +  (Scala infixl 5 "==")
   3.139 +
   3.140 +code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   3.141 +  (Haskell infix 4 "<=")
   3.142 +  (Scala infixl 4 "<=")
   3.143 +
   3.144 +code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   3.145 +  (Haskell infix 4 "<")
   3.146 +  (Scala infixl 4 "<")
   3.147 +
   3.148 +end