src/HOL/Library/Code_Target_Int.thy
author haftmann
Tue, 07 Feb 2017 22:15:05 +0100
changeset 64997 067a6cca39f0
parent 64242 93c6f0da5c70
child 65552 f533820e7248
permissions -rw-r--r--
dedicated computation preprocessing rules for nat, int implemented by target language literals
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_Int.thy
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Implementation of integer numbers by target-language integers\<close>
50023
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_Int
61856
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
     8
imports "../GCD"
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
code_datatype int_of_integer
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    12
54891
2f4491f15fe6 examples how to avoid the "code, code del" antipattern
haftmann
parents: 54796
diff changeset
    13
declare [[code drop: integer_of_int]]
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    14
55736
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54891
diff changeset
    15
context
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54891
diff changeset
    16
includes integer.lifting
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54891
diff changeset
    17
begin
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54891
diff changeset
    18
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    19
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    20
  "integer_of_int (int_of_integer k) = k"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    21
  by transfer rule
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    22
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    23
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    24
  "Int.Pos = int_of_integer \<circ> integer_of_num"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    25
  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
    26
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    27
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    28
  "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    29
  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
    30
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    31
lemma [code_abbrev]:
51095
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    32
  "int_of_integer (numeral k) = Int.Pos k"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    33
  by transfer simp
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_abbrev]:
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54227
diff changeset
    36
  "int_of_integer (- numeral k) = Int.Neg k"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    37
  by transfer simp
64997
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    38
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    39
context
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    40
begin  
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    41
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    42
qualified definition positive :: "num \<Rightarrow> int"
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    43
  where [simp]: "positive = numeral"
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    44
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    45
qualified definition negative :: "num \<Rightarrow> int"
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    46
  where [simp]: "negative = uminus \<circ> numeral"
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    47
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    48
lemma [code_computation_unfold]:
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    49
  "numeral = positive"
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    50
  "Int.Pos = positive"
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    51
  "Int.Neg = negative"
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    52
  by (simp_all add: fun_eq_iff)
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    53
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    54
end
067a6cca39f0 dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents: 64242
diff changeset
    55
51095
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    56
lemma [code, symmetric, code_post]:
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    57
  "0 = int_of_integer 0"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    58
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    59
51095
7ae79f2e3cc7 explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents: 50023
diff changeset
    60
lemma [code, symmetric, code_post]:
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    61
  "1 = int_of_integer 1"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    62
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    63
58099
7f232ae7de7c convenient printing of (- 1 :: integer) after code evaluation
haftmann
parents: 57512
diff changeset
    64
lemma [code_post]:
7f232ae7de7c convenient printing of (- 1 :: integer) after code evaluation
haftmann
parents: 57512
diff changeset
    65
  "int_of_integer (- 1) = - 1"
7f232ae7de7c convenient printing of (- 1 :: integer) after code evaluation
haftmann
parents: 57512
diff changeset
    66
  by simp
7f232ae7de7c convenient printing of (- 1 :: integer) after code evaluation
haftmann
parents: 57512
diff changeset
    67
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    68
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    69
  "k + l = int_of_integer (of_int k + of_int l)"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    70
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    71
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    72
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    73
  "- k = int_of_integer (- of_int k)"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    74
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    75
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    76
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    77
  "k - l = int_of_integer (of_int k - of_int l)"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    78
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    79
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    80
lemma [code]:
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51114
diff changeset
    81
  "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
    82
  by transfer simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    83
54891
2f4491f15fe6 examples how to avoid the "code, code del" antipattern
haftmann
parents: 54796
diff changeset
    84
declare [[code drop: Int.sub]]
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    85
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    86
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    87
  "k * l = int_of_integer (of_int k * of_int l)"
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    88
  by simp
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    89
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    90
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    91
  "k div l = int_of_integer (of_int k div of_int l)"
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    92
  by simp
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    93
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    94
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    95
  "k mod l = int_of_integer (of_int k mod of_int l)"
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    96
  by simp
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    97
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
    98
lemma [code]:
61275
053ec04ea866 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents: 60868
diff changeset
    99
  "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)"
053ec04ea866 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents: 60868
diff changeset
   100
  unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv
053ec04ea866 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents: 60868
diff changeset
   101
  by transfer simp
053ec04ea866 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents: 60868
diff changeset
   102
053ec04ea866 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents: 60868
diff changeset
   103
lemma [code]:
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   104
  "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
   105
  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
   106
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   107
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   108
  "k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
   109
  by transfer rule
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   110
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   111
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   112
  "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
51114
3e913a575dc6 type lifting setup for code numeral types
haftmann
parents: 51095
diff changeset
   113
  by transfer rule
61856
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   114
63351
e5d08b1d8fea avoid overlapping equations for gcd, lcm on integers
haftmann
parents: 61856
diff changeset
   115
declare [[code drop: "gcd :: int \<Rightarrow> _" "lcm :: int \<Rightarrow> _"]]
e5d08b1d8fea avoid overlapping equations for gcd, lcm on integers
haftmann
parents: 61856
diff changeset
   116
61856
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   117
lemma gcd_int_of_integer [code]:
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   118
  "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   119
by transfer rule
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   120
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   121
lemma lcm_int_of_integer [code]:
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   122
  "lcm (int_of_integer x) (int_of_integer y) = int_of_integer (lcm x y)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   123
by transfer rule
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 61275
diff changeset
   124
55736
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54891
diff changeset
   125
end
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   126
54796
cdc6d8cbf770 avoid clashes of fact names
haftmann
parents: 54489
diff changeset
   127
lemma (in ring_1) of_int_code_if:
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   128
  "of_int k = (if k = 0 then 0
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   129
     else if k < 0 then - of_int (- k)
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   130
     else let
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60500
diff changeset
   131
       l = 2 * of_int (k div 2);
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60500
diff changeset
   132
       j = k mod 2
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60500
diff changeset
   133
     in if j = 0 then l else l + 1)"
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   134
proof -
64242
93c6f0da5c70 more standardized theorem names for facts involving the div and mod identity
haftmann
parents: 63351
diff changeset
   135
  from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   136
  show ?thesis
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60500
diff changeset
   137
    by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   138
qed
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   139
54796
cdc6d8cbf770 avoid clashes of fact names
haftmann
parents: 54489
diff changeset
   140
declare of_int_code_if [code]
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   141
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   142
lemma [code]:
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   143
  "nat = nat_of_integer \<circ> of_int"
55736
f1ed1e9cd080 unregister lifting setup following the best practice of Lifting
kuncar
parents: 54891
diff changeset
   144
  including integer.lifting 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
   145
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   146
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
   147
  code_module Code_Target_Int \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   148
    (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
   149
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff changeset
   150
end