src/HOL/Library/Code_Target_Nat.thy
author haftmann
Fri, 04 Jul 2014 20:18:47 +0200
changeset 57512 cc97b347b301
parent 55736 f1ed1e9cd080
child 58881 b9556a055632
permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Code_Target_Nat.thy
51113
222fb6cb2c3e factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents: 51095
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
     3
*)
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
     4
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
     5
header {* Implementation of natural numbers by target-language integers *}
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
     6
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
     7
theory Code_Target_Nat
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51114
diff changeset
     8
imports Code_Abstract_Nat
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
     9
begin
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    10
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    11
subsection {* Implementation for @{typ nat} *}
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    12
55736
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54796
diff changeset
    13
context
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54796
diff changeset
    14
includes natural.lifting integer.lifting
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54796
diff changeset
    15
begin
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54796
diff changeset
    16
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    17
lift_definition Nat :: "integer \<Rightarrow> nat"
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    18
  is nat
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    19
  .
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    20
51095
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    21
lemma [code_post]:
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    22
  "Nat 0 = 0"
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    23
  "Nat 1 = 1"
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    24
  "Nat (numeral k) = numeral k"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    25
  by (transfer, simp)+
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    26
51095
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    27
lemma [code_abbrev]:
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    28
  "integer_of_nat = of_nat"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    29
  by transfer rule
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    30
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    31
lemma [code_unfold]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    32
  "Int.nat (int_of_integer k) = nat_of_integer k"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    33
  by transfer rule
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    34
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    35
lemma [code abstype]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    36
  "Code_Target_Nat.Nat (integer_of_nat n) = n"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    37
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    38
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    39
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    40
  "integer_of_nat (nat_of_integer k) = max 0 k"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    41
  by transfer auto
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    42
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    43
lemma [code_abbrev]:
51095
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    44
  "nat_of_integer (numeral k) = nat_of_num k"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    45
  by transfer (simp add: nat_of_num_numeral)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    46
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    47
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    48
  "integer_of_nat (nat_of_num n) = integer_of_num n"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    49
  by transfer (simp add: nat_of_num_numeral)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    50
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    51
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    52
  "integer_of_nat 0 = 0"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    53
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    54
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    55
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    56
  "integer_of_nat 1 = 1"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    57
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    58
51113
222fb6cb2c3e factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents: 51095
diff changeset
    59
lemma [code]:
222fb6cb2c3e factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents: 51095
diff changeset
    60
  "Suc n = n + 1"
222fb6cb2c3e factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents: 51095
diff changeset
    61
  by simp
222fb6cb2c3e factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents: 51095
diff changeset
    62
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    63
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    64
  "integer_of_nat (m + n) = of_nat m + of_nat n"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    65
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    66
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    67
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    68
  "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    69
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    70
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    71
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    72
  "integer_of_nat (m * n) = of_nat m * of_nat n"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    73
  by transfer (simp add: of_nat_mult)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    74
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    75
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    76
  "integer_of_nat (m div n) = of_nat m div of_nat n"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    77
  by transfer (simp add: zdiv_int)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    78
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    79
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    80
  "integer_of_nat (m mod n) = of_nat m mod of_nat n"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    81
  by transfer (simp add: zmod_int)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    82
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    83
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    84
  "Divides.divmod_nat m n = (m div n, m mod n)"
54796
cdc6d8cbf770 avoid clashes of fact names
haftmann
parents: 53027
diff changeset
    85
  by (fact divmod_nat_div_mod)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    86
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    87
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    88
  "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
    89
  by transfer (simp add: equal)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    90
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    91
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    92
  "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    93
  by simp
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    94
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    95
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    96
  "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    97
  by simp
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    98
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    99
lemma num_of_nat_code [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   100
  "num_of_nat = num_of_integer \<circ> of_nat"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51113
diff changeset
   101
  by transfer (simp add: fun_eq_iff)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   102
55736
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54796
diff changeset
   103
end
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54796
diff changeset
   104
54796
cdc6d8cbf770 avoid clashes of fact names
haftmann
parents: 53027
diff changeset
   105
lemma (in semiring_1) of_nat_code_if:
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   106
  "of_nat n = (if n = 0 then 0
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   107
     else let
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   108
       (m, q) = divmod_nat n 2;
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   109
       m' = 2 * of_nat m
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   110
     in if q = 0 then m' else m' + 1)"
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   111
proof -
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   112
  from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   113
  show ?thesis
54796
cdc6d8cbf770 avoid clashes of fact names
haftmann
parents: 53027
diff changeset
   114
    by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 55736
diff changeset
   115
      (simp add: * mult.commute of_nat_mult add.commute)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   116
qed
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   117
54796
cdc6d8cbf770 avoid clashes of fact names
haftmann
parents: 53027
diff changeset
   118
declare of_nat_code_if [code]
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   119
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   120
definition int_of_nat :: "nat \<Rightarrow> int" where
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   121
  [code_abbrev]: "int_of_nat = of_nat"
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   122
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   123
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   124
  "int_of_nat n = int_of_integer (of_nat n)"
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   125
  by (simp add: int_of_nat_def)
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   126
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   127
lemma [code abstract]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   128
  "integer_of_nat (nat k) = max 0 (integer_of_int k)"
55736
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54796
diff changeset
   129
  including integer.lifting by transfer auto
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   130
53027
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   131
lemma term_of_nat_code [code]:
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   132
  -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   133
        instead of @{term Code_Target_Nat.Nat} such that reconstructed
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   134
        terms can be fed back to the code generator *}
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   135
  "term_of_class.term_of n =
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   136
   Code_Evaluation.App
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   137
     (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   138
        (typerep.Typerep (STR ''fun'')
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   139
           [typerep.Typerep (STR ''Code_Numeral.integer'') [],
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   140
         typerep.Typerep (STR ''Nat.nat'') []]))
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   141
     (term_of_class.term_of (integer_of_nat n))"
54796
cdc6d8cbf770 avoid clashes of fact names
haftmann
parents: 53027
diff changeset
   142
  by (simp add: term_of_anything)
53027
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   143
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   144
lemma nat_of_integer_code_post [code_post]:
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   145
  "nat_of_integer 0 = 0"
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   146
  "nat_of_integer 1 = 1"
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   147
  "nat_of_integer (numeral k) = numeral k"
55736
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54796
diff changeset
   148
  including integer.lifting by (transfer, simp)+
53027
1774d569b604 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents: 52435
diff changeset
   149
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   150
code_identifier
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   151
  code_module Code_Target_Nat \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   152
    (SML) Arith and (OCaml) Arith and (Haskell) Arith
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   153
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   154
end