src/HOL/Library/ML_Int.thy
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24354 0fdabe28f0e6
child 24700 291665d063e4
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
     1 (*  ID:         $Id$
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Built-in integers for ML *}
     6 
     7 theory ML_Int
     8 imports List
     9 begin
    10 
    11 subsection {* Datatype of built-in integers *}
    12 
    13 datatype ml_int = ml_int_of_int int
    14 
    15 lemmas [code func del] = ml_int.recs ml_int.cases
    16 
    17 fun
    18   int_of_ml_int :: "ml_int \<Rightarrow> int"
    19 where
    20   "int_of_ml_int (ml_int_of_int k) = k"
    21 lemmas [code func del] = int_of_ml_int.simps
    22 
    23 lemma ml_int_id [simp]:
    24   "ml_int_of_int (int_of_ml_int k) = k"
    25   by (cases k) simp_all
    26 
    27 lemma ml_int:
    28   "(\<And>k\<Colon>ml_int. PROP P k) \<equiv> (\<And>k\<Colon>int. PROP P (ml_int_of_int k))"
    29 proof
    30   fix k :: int
    31   assume "\<And>k\<Colon>ml_int. PROP P k"
    32   then show "PROP P (ml_int_of_int k)" .
    33 next
    34   fix k :: ml_int
    35   assume "\<And>k\<Colon>int. PROP P (ml_int_of_int k)"
    36   then have "PROP P (ml_int_of_int (int_of_ml_int k))" .
    37   then show "PROP P k" by simp
    38 qed
    39 
    40 lemma [code func]: "size (k\<Colon>ml_int) = 0"
    41   by (cases k) simp_all
    42 
    43 
    44 subsection {* Built-in integers as datatype on numerals *}
    45 
    46 instance ml_int :: number
    47   "number_of \<equiv> ml_int_of_int" ..
    48 
    49 lemmas [code inline] = number_of_ml_int_def [symmetric]
    50 
    51 code_datatype "number_of \<Colon> int \<Rightarrow> ml_int"
    52 
    53 lemma number_of_ml_int_id [simp]:
    54   "number_of (int_of_ml_int k) = k"
    55   unfolding number_of_ml_int_def by simp
    56 
    57 
    58 subsection {* Basic arithmetic *}
    59 
    60 instance ml_int :: zero
    61   [simp]: "0 \<equiv> ml_int_of_int 0" ..
    62 lemmas [code func del] = zero_ml_int_def
    63 
    64 instance ml_int :: one
    65   [simp]: "1 \<equiv> ml_int_of_int 1" ..
    66 lemmas [code func del] = one_ml_int_def
    67 
    68 instance ml_int :: plus
    69   [simp]: "k + l \<equiv> ml_int_of_int (int_of_ml_int k + int_of_ml_int l)" ..
    70 lemmas [code func del] = plus_ml_int_def
    71 lemma plus_ml_int_code [code func]:
    72   "ml_int_of_int k + ml_int_of_int l = ml_int_of_int (k + l)"
    73   unfolding plus_ml_int_def by simp
    74 
    75 instance ml_int :: minus
    76   [simp]: "- k \<equiv> ml_int_of_int (- int_of_ml_int k)"
    77   [simp]: "k - l \<equiv> ml_int_of_int (int_of_ml_int k - int_of_ml_int l)" ..
    78 lemmas [code func del] = uminus_ml_int_def minus_ml_int_def
    79 lemma uminus_ml_int_code [code func]:
    80   "- ml_int_of_int k \<equiv> ml_int_of_int (- k)"
    81   unfolding uminus_ml_int_def by simp
    82 lemma minus_ml_int_code [code func]:
    83   "ml_int_of_int k - ml_int_of_int l = ml_int_of_int (k - l)"
    84   unfolding minus_ml_int_def by simp
    85 
    86 instance ml_int :: times
    87   [simp]: "k * l \<equiv> ml_int_of_int (int_of_ml_int k * int_of_ml_int l)" ..
    88 lemmas [code func del] = times_ml_int_def
    89 lemma times_ml_int_code [code func]:
    90   "ml_int_of_int k * ml_int_of_int l = ml_int_of_int (k * l)"
    91   unfolding times_ml_int_def by simp
    92 
    93 instance ml_int :: ord
    94   [simp]: "k \<le> l \<equiv> int_of_ml_int k \<le> int_of_ml_int l"
    95   [simp]: "k < l \<equiv> int_of_ml_int k < int_of_ml_int l" ..
    96 lemmas [code func del] = less_eq_ml_int_def less_ml_int_def
    97 lemma less_eq_ml_int_code [code func]:
    98   "ml_int_of_int k \<le> ml_int_of_int l \<longleftrightarrow> k \<le> l"
    99   unfolding less_eq_ml_int_def by simp
   100 lemma less_ml_int_code [code func]:
   101   "ml_int_of_int k < ml_int_of_int l \<longleftrightarrow> k < l"
   102   unfolding less_ml_int_def by simp
   103 
   104 instance ml_int :: ring_1
   105   by default (auto simp add: left_distrib right_distrib)
   106 
   107 lemma of_nat_ml_int: "of_nat n = ml_int_of_int (of_nat n)"
   108 proof (induct n)
   109   case 0 show ?case by simp
   110 next
   111   case (Suc n)
   112   then have "int_of_ml_int (ml_int_of_int (int n))
   113     = int_of_ml_int (of_nat n)" by simp
   114   then have "int n = int_of_ml_int (of_nat n)" by simp
   115   then show ?case by simp
   116 qed
   117 
   118 instance ml_int :: number_ring
   119   by default
   120     (simp_all add: left_distrib number_of_ml_int_def of_int_of_nat of_nat_ml_int)
   121 
   122 lemma zero_ml_int_code [code inline, code func]:
   123   "(0\<Colon>ml_int) = Numeral0"
   124   by simp
   125 
   126 lemma one_ml_int_code [code inline, code func]:
   127   "(1\<Colon>ml_int) = Numeral1"
   128   by simp
   129 
   130 instance ml_int :: abs
   131   "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
   132 
   133 
   134 subsection {* Conversion to @{typ nat} *}
   135 
   136 definition
   137   nat_of_ml_int :: "ml_int \<Rightarrow> nat"
   138 where
   139   "nat_of_ml_int = nat o int_of_ml_int"
   140 
   141 definition
   142   nat_of_ml_int_aux :: "ml_int \<Rightarrow> nat \<Rightarrow> nat" where
   143   "nat_of_ml_int_aux i n = nat_of_ml_int i + n"
   144 
   145 lemma nat_of_ml_int_aux_code [code]:
   146   "nat_of_ml_int_aux i n = (if i \<le> 0 then n else nat_of_ml_int_aux (i - 1) (Suc n))"
   147   by (auto simp add: nat_of_ml_int_aux_def nat_of_ml_int_def)
   148 
   149 lemma nat_of_ml_int_code [code]:
   150   "nat_of_ml_int i = nat_of_ml_int_aux i 0"
   151   by (simp add: nat_of_ml_int_aux_def)
   152 
   153 
   154 subsection {* ML interface *}
   155 
   156 ML {*
   157 structure ML_Int =
   158 struct
   159 
   160 fun mk k = @{term ml_int_of_int} $ HOLogic.mk_number @{typ ml_int} k;
   161 
   162 end;
   163 *}
   164 
   165 
   166 subsection {* Code serialization *}
   167 
   168 code_type ml_int
   169   (SML "int")
   170 
   171 setup {*
   172   CodeTarget.add_pretty_numeral "SML" false
   173     @{const_name ml_int_of_int}
   174     @{const_name Numeral.B0} @{const_name Numeral.B1}
   175     @{const_name Numeral.Pls} @{const_name Numeral.Min}
   176     @{const_name Numeral.Bit}
   177 *}
   178 
   179 code_reserved SML int
   180 
   181 code_const "op + \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
   182   (SML "Int.+ ((_), (_))")
   183 
   184 code_const "uminus \<Colon> ml_int \<Rightarrow> ml_int"
   185   (SML "Int.~")
   186 
   187 code_const "op - \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
   188   (SML "Int.- ((_), (_))")
   189 
   190 code_const "op * \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
   191   (SML "Int.* ((_), (_))")
   192 
   193 code_const "op = \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
   194   (SML "!((_ : Int.int) = _)")
   195 
   196 code_const "op \<le> \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
   197   (SML "Int.<= ((_), (_))")
   198 
   199 code_const "op < \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
   200   (SML "Int.< ((_), (_))")
   201 
   202 end
   203 
   204