author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 49834  b27bbb021df1 
child 51143  0a2371e7ced3 
permissions  rwrr 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

1 
(* Author: Florian Haftmann, TU Muenchen *) 
24999  2 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

3 
header {* Type of target language numerals *} 
24999  4 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

5 
theory Code_Numeral 
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47108
diff
changeset

6 
imports Nat_Transfer Divides 
24999  7 
begin 
8 

9 
text {* 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

10 
Code numerals are isomorphic to HOL @{typ nat} but 
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

11 
mapped to targetlanguage builtin numerals. 
24999  12 
*} 
13 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

14 
subsection {* Datatype of target language numerals *} 
24999  15 

49834  16 
typedef code_numeral = "UNIV \<Colon> nat set" 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44821
diff
changeset

17 
morphisms nat_of of_nat .. 
24999  18 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

19 
lemma of_nat_nat_of [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

20 
"of_nat (nat_of k) = k" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

21 
by (rule nat_of_inverse) 
24999  22 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

23 
lemma nat_of_of_nat [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

24 
"nat_of (of_nat n) = n" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

25 
by (rule of_nat_inverse) (rule UNIV_I) 
24999  26 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

27 
lemma [measure_function]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

28 
"is_measure nat_of" by (rule is_measure_trivial) 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

29 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

30 
lemma code_numeral: 
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

31 
"(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))" 
24999  32 
proof 
25767  33 
fix n :: nat 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

34 
assume "\<And>n\<Colon>code_numeral. PROP P n" 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

35 
then show "PROP P (of_nat n)" . 
24999  36 
next 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

37 
fix n :: code_numeral 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

38 
assume "\<And>n\<Colon>nat. PROP P (of_nat n)" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

39 
then have "PROP P (of_nat (nat_of n))" . 
25767  40 
then show "PROP P n" by simp 
24999  41 
qed 
42 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

43 
lemma code_numeral_case: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

44 
assumes "\<And>n. k = of_nat n \<Longrightarrow> P" 
26140  45 
shows P 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

46 
by (rule assms [of "nat_of k"]) simp 
26140  47 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

48 
lemma code_numeral_induct_raw: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

49 
assumes "\<And>n. P (of_nat n)" 
26140  50 
shows "P k" 
51 
proof  

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

52 
from assms have "P (of_nat (nat_of k))" . 
26140  53 
then show ?thesis by simp 
54 
qed 

55 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

56 
lemma nat_of_inject [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

57 
"nat_of k = nat_of l \<longleftrightarrow> k = l" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

58 
by (rule nat_of_inject) 
26140  59 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

60 
lemma of_nat_inject [simp]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

61 
"of_nat n = of_nat m \<longleftrightarrow> n = m" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

62 
by (rule of_nat_inject) (rule UNIV_I)+ 
26140  63 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

64 
instantiation code_numeral :: zero 
26140  65 
begin 
66 

28562  67 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

68 
"0 = of_nat 0" 
26140  69 

70 
instance .. 

71 

72 
end 

73 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

74 
definition Suc where [simp]: 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

75 
"Suc k = of_nat (Nat.Suc (nat_of k))" 
26140  76 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

77 
rep_datatype "0 \<Colon> code_numeral" Suc 
26140  78 
proof  
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

79 
fix P :: "code_numeral \<Rightarrow> bool" 
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

80 
fix k :: code_numeral 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

81 
assume "P 0" then have init: "P (of_nat 0)" by simp 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

82 
assume "\<And>k. P k \<Longrightarrow> P (Suc k)" 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

83 
then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc (of_nat n))" . 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

84 
then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Nat.Suc n))" by simp 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

85 
from init step have "P (of_nat (nat_of k))" 
34915  86 
by (induct ("nat_of k")) simp_all 
26140  87 
then show "P k" by simp 
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26304
diff
changeset

88 
qed simp_all 
26140  89 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

90 
declare code_numeral_case [case_names nat, cases type: code_numeral] 
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

91 
declare code_numeral.induct [case_names nat, induct type: code_numeral] 
26140  92 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

93 
lemma code_numeral_decr [termination_simp]: 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

94 
"k \<noteq> of_nat 0 \<Longrightarrow> nat_of k  Nat.Suc 0 < nat_of k" 
30245
e67f42ac1157
consequent rewrite of index_size, size [index] to nat_of; support pseudoprimrec sepcifications with fun
haftmann
parents:
29823
diff
changeset

95 
by (cases k) simp 
e67f42ac1157
consequent rewrite of index_size, size [index] to nat_of; support pseudoprimrec sepcifications with fun
haftmann
parents:
29823
diff
changeset

96 

e67f42ac1157
consequent rewrite of index_size, size [index] to nat_of; support pseudoprimrec sepcifications with fun
haftmann
parents:
29823
diff
changeset

97 
lemma [simp, code]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

98 
"code_numeral_size = nat_of" 
26140  99 
proof (rule ext) 
100 
fix k 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

101 
have "code_numeral_size k = nat_size (nat_of k)" 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

102 
by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_def, simp_all) 
34915  103 
also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

104 
finally show "code_numeral_size k = nat_of k" . 
26140  105 
qed 
106 

30245
e67f42ac1157
consequent rewrite of index_size, size [index] to nat_of; support pseudoprimrec sepcifications with fun
haftmann
parents:
29823
diff
changeset

107 
lemma [simp, code]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

108 
"size = nat_of" 
26140  109 
proof (rule ext) 
110 
fix k 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

111 
show "size k = nat_of k" 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

112 
by (induct k) (simp_all del: zero_code_numeral_def Suc_def, simp_all) 
26140  113 
qed 
114 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

115 
lemmas [code del] = code_numeral.recs code_numeral.cases 
30245
e67f42ac1157
consequent rewrite of index_size, size [index] to nat_of; support pseudoprimrec sepcifications with fun
haftmann
parents:
29823
diff
changeset

116 

28562  117 
lemma [code]: 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37958
diff
changeset

118 
"HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37958
diff
changeset

119 
by (cases k, cases l) (simp add: equal) 
24999  120 

28351  121 
lemma [code nbe]: 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37958
diff
changeset

122 
"HOL.equal (k::code_numeral) k \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37958
diff
changeset

123 
by (rule equal_refl) 
28351  124 

24999  125 

126 
subsection {* Basic arithmetic *} 

127 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34944
diff
changeset

128 
instantiation code_numeral :: "{minus, linordered_semidom, semiring_div, linorder}" 
25767  129 
begin 
24999  130 

28562  131 
definition [simp, code del]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

132 
"(1\<Colon>code_numeral) = of_nat 1" 
24999  133 

28562  134 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

135 
"n + m = of_nat (nat_of n + nat_of m)" 
25767  136 

28562  137 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

138 
"n  m = of_nat (nat_of n  nat_of m)" 
25767  139 

28562  140 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

141 
"n * m = of_nat (nat_of n * nat_of m)" 
25767  142 

28562  143 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

144 
"n div m = of_nat (nat_of n div nat_of m)" 
24999  145 

28562  146 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

147 
"n mod m = of_nat (nat_of n mod nat_of m)" 
24999  148 

28562  149 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

150 
"n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m" 
24999  151 

28562  152 
definition [simp, code del]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

153 
"n < m \<longleftrightarrow> nat_of n < nat_of m" 
24999  154 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

155 
instance proof 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49834
diff
changeset

156 
qed (auto simp add: code_numeral distrib_right intro: mult_commute) 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

157 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

158 
end 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

159 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

160 
lemma nat_of_numeral [simp]: "nat_of (numeral k) = numeral k" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

161 
by (induct k rule: num_induct) (simp_all add: numeral_inc) 
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45694
diff
changeset

162 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

163 
definition Num :: "num \<Rightarrow> code_numeral" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

164 
where [simp, code_abbrev]: "Num = numeral" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

165 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

166 
code_datatype "0::code_numeral" Num 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

167 

46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45694
diff
changeset

168 
lemma one_code_numeral_code [code]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

169 
"(1\<Colon>code_numeral) = Numeral1" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

170 
by simp 
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45694
diff
changeset

171 

9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45694
diff
changeset

172 
lemma [code_abbrev]: "Numeral1 = (1\<Colon>code_numeral)" 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

173 
using one_code_numeral_code .. 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

174 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

175 
lemma plus_code_numeral_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

176 
"of_nat n + of_nat m = of_nat (n + m)" 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

177 
by simp 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

178 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

179 
lemma minus_code_numeral_code [code nbe]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

180 
"of_nat n  of_nat m = of_nat (n  m)" 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

181 
by simp 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

182 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

183 
lemma times_code_numeral_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

184 
"of_nat n * of_nat m = of_nat (n * m)" 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

185 
by simp 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

186 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

187 
lemma less_eq_code_numeral_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

188 
"of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m" 
25767  189 
by simp 
24999  190 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

191 
lemma less_code_numeral_code [code nbe]: 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

192 
"of_nat n < of_nat m \<longleftrightarrow> n < m" 
25767  193 
by simp 
24999  194 

31266  195 
lemma code_numeral_zero_minus_one: 
196 
"(0::code_numeral)  1 = 0" 

197 
by simp 

198 

199 
lemma Suc_code_numeral_minus_one: 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

200 
"Suc n  1 = n" 
31266  201 
by simp 
26140  202 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

203 
lemma of_nat_code [code]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

204 
"of_nat = Nat.of_nat" 
25918  205 
proof 
206 
fix n :: nat 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

207 
have "Nat.of_nat n = of_nat n" 
25918  208 
by (induct n) simp_all 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

209 
then show "of_nat n = Nat.of_nat n" 
25918  210 
by (rule sym) 
211 
qed 

212 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

213 
lemma code_numeral_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1" 
25928  214 
by (cases i) auto 
215 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

216 
definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> nat" where 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

217 
"nat_of_aux i n = nat_of i + n" 
25928  218 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

219 
lemma nat_of_aux_code [code]: 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

220 
"nat_of_aux i n = (if i = 0 then n else nat_of_aux (i  1) (Nat.Suc n))" 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

221 
by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero) 
25928  222 

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

223 
lemma nat_of_code [code]: 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

224 
"nat_of i = nat_of_aux i 0" 
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
28708
diff
changeset

225 
by (simp add: nat_of_aux_def) 
25918  226 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

227 
definition div_mod :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

228 
[code del]: "div_mod n m = (n div m, n mod m)" 
26009  229 

28562  230 
lemma [code]: 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

231 
"div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))" 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

232 
unfolding div_mod_def by auto 
26009  233 

28562  234 
lemma [code]: 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

235 
"n div m = fst (div_mod n m)" 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

236 
unfolding div_mod_def by simp 
26009  237 

28562  238 
lemma [code]: 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

239 
"n mod m = snd (div_mod n m)" 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

240 
unfolding div_mod_def by simp 
26009  241 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

242 
definition int_of :: "code_numeral \<Rightarrow> int" where 
31192  243 
"int_of = Nat.of_nat o nat_of" 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

244 

31192  245 
lemma int_of_code [code]: 
246 
"int_of k = (if k = 0 then 0 

247 
else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))" 

33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

248 
proof  
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

249 
have "(nat_of k div 2) * 2 + nat_of k mod 2 = nat_of k" 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

250 
by (rule mod_div_equality) 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

251 
then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

252 
by simp 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

253 
then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" 
44821  254 
unfolding of_nat_mult of_nat_add by simp 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

255 
then show ?thesis by (auto simp add: int_of_def mult_ac) 
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

256 
qed 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

257 

a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

258 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

259 
hide_const (open) of_nat nat_of Suc int_of 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

260 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

261 

28228  262 
subsection {* Code generator setup *} 
24999  263 

37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

264 
text {* Implementation of code numerals by bounded integers *} 
25767  265 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

266 
code_type code_numeral 
24999  267 
(SML "int") 
31377  268 
(OCaml "Big'_int.big'_int") 
37947  269 
(Haskell "Integer") 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

270 
(Scala "BigInt") 
24999  271 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37958
diff
changeset

272 
code_instance code_numeral :: equal 
24999  273 
(Haskell ) 
274 

275 
setup {* 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

276 
Numeral.add_code @{const_name Num} 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

277 
false Code_Printer.literal_naive_numeral "SML" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

278 
#> fold (Numeral.add_code @{const_name Num} 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

279 
false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"] 
24999  280 
*} 
281 

25918  282 
code_reserved SML Int int 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

283 
code_reserved Eval Integer 
24999  284 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

285 
code_const "0::code_numeral" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

286 
(SML "0") 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

287 
(OCaml "Big'_int.zero'_big'_int") 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

288 
(Haskell "0") 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

289 
(Scala "BigInt(0)") 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

290 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

291 
code_const "plus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" 
25928  292 
(SML "Int.+/ ((_),/ (_))") 
31377  293 
(OCaml "Big'_int.add'_big'_int") 
24999  294 
(Haskell infixl 6 "+") 
34886  295 
(Scala infixl 7 "+") 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

296 
(Eval infixl 8 "+") 
24999  297 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

298 
code_const "minus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

299 
(SML "Int.max/ (0 : int,/ Int./ ((_),/ (_)))") 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

300 
(OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)") 
48431
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
47255
diff
changeset

301 
(Haskell "Prelude.max/ (0 :: Integer)/ (_/ / _)") 
34886  302 
(Scala "!(_/ / _).max(0)") 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

303 
(Eval "Integer.max/ 0/ (_/ / _)") 
24999  304 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

305 
code_const "times \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" 
25928  306 
(SML "Int.*/ ((_),/ (_))") 
31377  307 
(OCaml "Big'_int.mult'_big'_int") 
24999  308 
(Haskell infixl 7 "*") 
34886  309 
(Scala infixl 8 "*") 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

310 
(Eval infixl 8 "*") 
24999  311 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

312 
code_const Code_Numeral.div_mod 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

313 
(SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))") 
34898
62d70417f8ce
allow individual printing of numerals during code serialization
haftmann
parents:
34886
diff
changeset

314 
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") 
26009  315 
(Haskell "divMod") 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

316 
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") 
39818  317 
(Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Integer.div'_mod n m))") 
25928  318 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37958
diff
changeset

319 
code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" 
24999  320 
(SML "!((_ : Int.int) = _)") 
31377  321 
(OCaml "Big'_int.eq'_big'_int") 
39272  322 
(Haskell infix 4 "==") 
34886  323 
(Scala infixl 5 "==") 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

324 
(Eval "!((_ : int) = _)") 
24999  325 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

326 
code_const "less_eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" 
25928  327 
(SML "Int.<=/ ((_),/ (_))") 
31377  328 
(OCaml "Big'_int.le'_big'_int") 
24999  329 
(Haskell infix 4 "<=") 
34898
62d70417f8ce
allow individual printing of numerals during code serialization
haftmann
parents:
34886
diff
changeset

330 
(Scala infixl 4 "<=") 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

331 
(Eval infixl 6 "<=") 
24999  332 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

333 
code_const "less \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" 
25928  334 
(SML "Int.</ ((_),/ (_))") 
31377  335 
(OCaml "Big'_int.lt'_big'_int") 
24999  336 
(Haskell infix 4 "<") 
34898
62d70417f8ce
allow individual printing of numerals during code serialization
haftmann
parents:
34886
diff
changeset

337 
(Scala infixl 4 "<") 
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset

338 
(Eval infixl 6 "<") 
24999  339 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

340 
code_modulename SML 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

341 
Code_Numeral Arith 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

342 

d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

343 
code_modulename OCaml 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

344 
Code_Numeral Arith 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

345 

d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

346 
code_modulename Haskell 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

347 
Code_Numeral Arith 
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

348 

24999  349 
end 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

350 