src/HOL/Library/EfficientNat.thy
author haftmann
Wed, 22 Nov 2006 10:20:12 +0100
changeset 21454 a1937c51ed88
parent 21404 eb85850d3eb7
child 21546 268b6bed0cc8
permissions -rw-r--r--
dropped eq const
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Library/EfficientNat.thy
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     4
*)
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     5
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     6
header {* Implementation of natural numbers by integers *}
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     7
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     8
theory EfficientNat
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
     9
imports Main
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    10
begin
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    11
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    12
text {*
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    13
When generating code for functions on natural numbers, the canonical
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    14
representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    15
computations involving large numbers. The efficiency of the generated
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    16
code can be improved drastically by implementing natural numbers by
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    17
integers. To do this, just include this theory.
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    18
*}
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    19
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    20
subsection {* Logical rewrites *}
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    21
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    22
text {*
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    23
  A int-to-nat conversion with domain
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    24
  restricted to non-negative ints (in contrast to @{const nat}).
16770
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16295
diff changeset
    25
*}
1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents: 16295
diff changeset
    26
20641
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    27
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21287
diff changeset
    28
  nat_of_int :: "int \<Rightarrow> nat" where
20641
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    29
  "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
19889
2202a5648897 slight adaptions for code generator
haftmann
parents: 19828
diff changeset
    30
20839
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
    31
lemma nat_of_int_int:
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
    32
  "nat_of_int (int n) = n"
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
    33
  using zero_zle_int nat_of_int_def by simp
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
    34
19889
2202a5648897 slight adaptions for code generator
haftmann
parents: 19828
diff changeset
    35
text {*
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    36
  Case analysis on natural numbers is rephrased using a conditional
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    37
  expression:
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    38
*}
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    39
20839
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
    40
lemma [code unfold, code noinline]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    41
proof -
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    42
  have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))"
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    43
  proof -
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    44
    fix f g n
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    45
    show "nat_case f g n = (if n = 0 then f else g (n - 1))"
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    46
      by (cases n) simp_all
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    47
  qed
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    48
  show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    49
    by (rule eq_reflection ext rewrite)+ 
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    50
qed
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    51
20839
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
    52
lemma [code inline]:
21454
a1937c51ed88 dropped eq const
haftmann
parents: 21404
diff changeset
    53
  "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
a1937c51ed88 dropped eq const
haftmann
parents: 21404
diff changeset
    54
  by (cases n) (simp_all add: nat_of_int_int)
20839
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
    55
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    56
text {*
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    57
  Most standard arithmetic functions on natural numbers are implemented
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
    58
  using their counterparts on the integers:
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    59
*}
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
    60
20641
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    61
lemma [code func]: "0 = nat_of_int 0"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    62
  by (simp add: nat_of_int_def)
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    63
lemma [code func, code inline]:  "1 = nat_of_int 1"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    64
  by (simp add: nat_of_int_def)
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    65
lemma [code func]: "Suc n = n + 1"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    66
  by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    67
lemma [code, code inline]: "m + n = nat (int m + int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    68
  by arith
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    69
lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    70
  by (simp add: nat_of_int_def)
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    71
lemma [code, code inline]: "m - n = nat (int m - int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    72
  by arith
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    73
lemma [code, code inline]: "m * n = nat (int m * int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    74
  unfolding zmult_int by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    75
lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    76
proof -
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    77
  have "int (m * n) = int m * int n"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    78
    by (induct m) (simp_all add: zadd_zmult_distrib)
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    79
  then have "m * n = nat (int m * int n)" by auto
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    80
  also have "\<dots> = nat_of_int (int m * int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    81
  proof -
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    82
    have "int m \<ge> 0" and "int n \<ge> 0" by auto
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    83
    have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    84
    with nat_of_int_def show ?thesis by auto
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    85
  qed
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    86
  finally show ?thesis .
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    87
qed  
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    88
lemma [code]: "m div n = nat (int m div int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    89
  unfolding zdiv_int [symmetric] by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    90
lemma [code func]: "m div n = fst (Divides.divmod m n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    91
  unfolding divmod_def by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    92
lemma [code]: "m mod n = nat (int m mod int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    93
  unfolding zmod_int [symmetric] by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    94
lemma [code func]: "m mod n = snd (Divides.divmod m n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    95
  unfolding divmod_def by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    96
lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    97
  by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    98
lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
    99
  by simp
21454
a1937c51ed88 dropped eq const
haftmann
parents: 21404
diff changeset
   100
lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
a1937c51ed88 dropped eq const
haftmann
parents: 21404
diff changeset
   101
  by simp
20641
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   102
lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   103
proof (cases "k < 0")
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   104
  case True then show ?thesis by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   105
next
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   106
  case False then show ?thesis by (simp add: nat_of_int_def)
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   107
qed
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20453
diff changeset
   108
lemma [code func]:
20641
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   109
  "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   110
proof -
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   111
  have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   112
  proof -
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   113
    assume prem: "n > 0"
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   114
    then have "int n - 1 \<ge> 0" by auto
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   115
    then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def)
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   116
    with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   117
  qed
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   118
  then show ?thesis unfolding int_aux_def by simp
12554634e552 improvements for codegen 2
haftmann
parents: 20597
diff changeset
   119
qed
20356
21e7e9093940 improvements for 2nd codegenerator
haftmann
parents: 20287
diff changeset
   120
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   121
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   122
subsection {* Code generator setup for basic functions *}
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   123
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   124
text {*
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   125
  @{typ nat} is no longer a datatype but embedded into the integers.
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   126
*}
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   127
20839
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
   128
code_const "0::nat"
21113
5b76e541cc0a adapted to new serializer syntax
haftmann
parents: 21046
diff changeset
   129
  (SML "!(0 : IntInf.int)")
5b76e541cc0a adapted to new serializer syntax
haftmann
parents: 21046
diff changeset
   130
  (Haskell "0")
20839
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
   131
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
   132
code_const "Suc"
21125
9b7d35ca1eef adapted to new serializer syntax
haftmann
parents: 21113
diff changeset
   133
  (SML "IntInf.+ ((_), 1)")
9b7d35ca1eef adapted to new serializer syntax
haftmann
parents: 21113
diff changeset
   134
  (Haskell "!((_) + 1)")
20839
ed49d8709959 improvements for code_gen
haftmann
parents: 20713
diff changeset
   135
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   136
setup {*
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   137
  CodegenData.del_datatype "nat"
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   138
*}
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   139
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   140
types_code
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   141
  nat ("int")
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   142
attach (term_of) {*
20713
823967ef47f1 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents: 20700
diff changeset
   143
fun term_of_nat 0 = Const ("HOL.zero", HOLogic.natT)
823967ef47f1 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents: 20700
diff changeset
   144
  | term_of_nat 1 = Const ("HOL.one", HOLogic.natT)
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   145
  | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   146
      HOLogic.mk_binum (IntInf.fromInt i);
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   147
*}
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   148
attach (test) {*
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   149
fun gen_nat i = random_range 0 i;
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   150
*}
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   151
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   152
code_type nat
21113
5b76e541cc0a adapted to new serializer syntax
haftmann
parents: 21046
diff changeset
   153
  (SML "IntInf.int")
5b76e541cc0a adapted to new serializer syntax
haftmann
parents: 21046
diff changeset
   154
  (Haskell "Integer")
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   155
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   156
consts_code
20713
823967ef47f1 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents: 20700
diff changeset
   157
  "HOL.zero" :: nat ("0")
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   158
  Suc ("(_ + 1)")
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   159
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   160
text {*
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   161
  Since natural numbers are implemented
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   162
  using integers, the coercion function @{const "int"} of type
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   163
  @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function,
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   164
  likewise @{const nat_of_int} of type @{typ "int \<Rightarrow> nat"}.
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   165
  For the @{const "nat"} function for converting an integer to a natural
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   166
  number, we give a specific implementation using an ML function that
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   167
  returns its input value, provided that it is non-negative, and otherwise
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   168
  returns @{text "0"}.
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   169
*}
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   170
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   171
consts_code
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   172
  int ("(_)")
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   173
  nat ("\<module>nat")
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   174
attach {*
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   175
fun nat i = if i < 0 then 0 else i;
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   176
*}
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   177
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   178
code_const int
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   179
  (SML "_")
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   180
  (Haskell "_")
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   181
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   182
code_const nat_of_int
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   183
  (SML "_")
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   184
  (Haskell "_")
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   185
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   186
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   187
subsection {* Preprocessors *}
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   188
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   189
text {*
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   190
  In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   191
  a constructor term. Therefore, all occurrences of this term in a position
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   192
  where a pattern is expected (i.e.\ on the left-hand side of a recursion
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   193
  equation or in the arguments of an inductive relation in an introduction
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   194
  rule) must be eliminated.
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   195
  This can be accomplished by applying the following transformation rules:
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   196
*}
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   197
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   198
theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   199
  f n = (if n = 0 then g else h (n - 1))"
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   200
  by (case_tac n) simp_all
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   201
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   202
theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   203
  by (case_tac n) simp_all
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   204
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   205
text {*
20700
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   206
  The rules above are built into a preprocessor that is plugged into
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   207
  the code generator. Since the preprocessor for introduction rules
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   208
  does not know anything about modes, some of the modes that worked
7e3450c10c2d updated theory description
haftmann
parents: 20641
diff changeset
   209
  for the canonical representation of natural numbers may no longer work.
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   210
*}
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   211
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   212
(*<*)
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   213
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   214
ML {*
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   215
local
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   216
  val Suc_if_eq = thm "Suc_if_eq";
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   217
  val Suc_clause = thm "Suc_clause";
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   218
  fun contains_suc t = member (op =) (term_consts t) "Suc";
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   219
in
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   220
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   221
fun remove_suc thy thms =
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   222
  let
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   223
    val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 19889
diff changeset
   224
    val vname = Name.variant (map fst
20196
9a19e4de6e2e renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
wenzelm
parents: 20105
diff changeset
   225
      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16770
diff changeset
   226
    val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   227
    fun lhs_of th = snd (Thm.dest_comb
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   228
      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   229
    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   230
    fun find_vars ct = (case term_of ct of
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   231
        (Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   232
      | _ $ _ =>
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   233
        let val (ct1, ct2) = Thm.dest_comb ct
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   234
        in 
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   235
          map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   236
          map (apfst (Thm.capply ct1)) (find_vars ct2)
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   237
        end
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   238
      | _ => []);
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   239
    val eqs = List.concat (map
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   240
      (fn th => map (pair th) (find_vars (lhs_of th))) thms);
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   241
    fun mk_thms (th, (ct, cv')) =
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   242
      let
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   243
        val th' =
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   244
          Thm.implies_elim
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   245
           (Drule.fconv_rule (Thm.beta_conversion true)
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   246
             (Drule.instantiate'
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15396
diff changeset
   247
               [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   248
                 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   249
               Suc_if_eq')) (Thm.forall_intr cv' th)
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   250
      in
21287
a713ae348e8a tuned Variable.trade;
wenzelm
parents: 21191
diff changeset
   251
        case map_filter (fn th'' =>
20287
8cbcb46c3c09 replaced obsolete standard/freeze_all by Variable.trade;
wenzelm
parents: 20196
diff changeset
   252
            SOME (th'', singleton
21287
a713ae348e8a tuned Variable.trade;
wenzelm
parents: 21191
diff changeset
   253
              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   254
          handle THM _ => NONE) thms of
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   255
            [] => NONE
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   256
          | thps =>
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   257
              let val (ths1, ths2) = split_list thps
20951
868120282837 gen_rem(s) abandoned in favour of remove / subtract
haftmann
parents: 20839
diff changeset
   258
              in SOME (subtract eq_thm (th :: ths1) thms @ ths2) end
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   259
      end
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   260
  in
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   261
    case get_first mk_thms eqs of
16900
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   262
      NONE => thms
e294033d1c0f Rewrote function remove_suc, since it failed on some equations
berghofe
parents: 16861
diff changeset
   263
    | SOME x => remove_suc thy x
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   264
  end;
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   265
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   266
fun eqn_suc_preproc thy ths =
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   267
  let
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   268
    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   269
  in
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   270
    if forall (can dest) ths andalso
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   271
      exists (contains_suc o dest) ths
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   272
    then remove_suc thy ths else ths
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   273
  end;
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   274
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   275
fun remove_suc_clause thy thms =
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   276
  let
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   277
    val Suc_clause' = Thm.transfer thy Suc_clause;
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 19889
diff changeset
   278
    val vname = Name.variant (map fst
20196
9a19e4de6e2e renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
wenzelm
parents: 20105
diff changeset
   279
      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15396
diff changeset
   280
    fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15396
diff changeset
   281
      | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15396
diff changeset
   282
      | find_var _ = NONE;
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   283
    fun find_thm th =
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   284
      let val th' = ObjectLogic.atomize_thm th
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   285
      in Option.map (pair (th, th')) (find_var (prop_of th')) end
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   286
  in
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   287
    case get_first find_thm thms of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15396
diff changeset
   288
      NONE => thms
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15396
diff changeset
   289
    | SOME ((th, th'), (Sucv, v)) =>
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   290
        let
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16770
diff changeset
   291
          val cert = cterm_of (Thm.theory_of_thm th);
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   292
          val th'' = ObjectLogic.rulify (Thm.implies_elim
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   293
            (Drule.fconv_rule (Thm.beta_conversion true)
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   294
              (Drule.instantiate' []
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15396
diff changeset
   295
                [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   296
                   abstract_over (Sucv,
19828
f1dccc547595 Removed "code del" declarations again.
berghofe
parents: 19791
diff changeset
   297
                     HOLogic.dest_Trueprop (prop_of th')))))),
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15396
diff changeset
   298
                 SOME (cert v)] Suc_clause'))
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   299
            (Thm.forall_intr (cert v) th'))
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   300
        in
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   301
          remove_suc_clause thy (map (fn th''' =>
19617
7cb4b67d4b97 avoid raw equality on type thm;
wenzelm
parents: 19603
diff changeset
   302
            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   303
        end
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   304
  end;
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   305
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   306
fun clause_suc_preproc thy ths =
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   307
  let
19828
f1dccc547595 Removed "code del" declarations again.
berghofe
parents: 19791
diff changeset
   308
    val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   309
  in
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   310
    if forall (can (dest o concl_of)) ths andalso
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   311
      exists (fn th => member (op =) (foldr add_term_consts
21287
a713ae348e8a tuned Variable.trade;
wenzelm
parents: 21191
diff changeset
   312
        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
15396
0a36ccb79481 Preprocessors now transfer theorems to current theory in order to
berghofe
parents: 15323
diff changeset
   313
    then remove_suc_clause thy ths else ths
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   314
  end;
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   315
19791
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   316
end; (*local*)
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   317
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   318
fun lift_obj_eq f thy =
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   319
  map (fn thm => thm RS meta_eq_to_obj_eq)
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   320
  #> f thy
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   321
  #> map (fn thm => thm RS HOL.eq_reflection)
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   322
*}
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   323
ab326de16ad5 refined code generation
haftmann
parents: 19617
diff changeset
   324
setup {*
19603
9801b391c8b3 added preprocs for CodegenTheorems
haftmann
parents: 19481
diff changeset
   325
  Codegen.add_preprocessor eqn_suc_preproc
9801b391c8b3 added preprocs for CodegenTheorems
haftmann
parents: 19481
diff changeset
   326
  #> Codegen.add_preprocessor clause_suc_preproc
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
   327
  #> CodegenData.add_preproc (lift_obj_eq eqn_suc_preproc)
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20523
diff changeset
   328
  #> CodegenData.add_preproc (lift_obj_eq clause_suc_preproc)
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   329
*}
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   330
(*>*)
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   331
21191
c00161fbf990 code generator module naming improved
haftmann
parents: 21125
diff changeset
   332
subsection {* Module names *}
c00161fbf990 code generator module naming improved
haftmann
parents: 21125
diff changeset
   333
c00161fbf990 code generator module naming improved
haftmann
parents: 21125
diff changeset
   334
code_modulename SML
c00161fbf990 code generator module naming improved
haftmann
parents: 21125
diff changeset
   335
  Nat Integer
c00161fbf990 code generator module naming improved
haftmann
parents: 21125
diff changeset
   336
  EfficientNat Integer
c00161fbf990 code generator module naming improved
haftmann
parents: 21125
diff changeset
   337
15323
6c10fe1c0e17 Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff changeset
   338
end