author  haftmann 
Tue, 07 Feb 2017 22:15:05 +0100  
changeset 64997  067a6cca39f0 
parent 64242  93c6f0da5c70 
child 65552  f533820e7248 
permissions  rwrr 
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  5 
section \<open>Implementation of integer numbers by targetlanguage 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  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  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  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  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  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  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  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  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  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  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  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  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  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  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  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  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_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset

146 
code_identifier 
6646bb548c6b
migration from code_(consttypeclassinstance) 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_(consttypeclassinstance) 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 