author | wenzelm |
Wed, 22 Apr 2020 19:22:43 +0200 | |
changeset 71787 | acfe72ff00c2 |
parent 71535 | b612edee9b0c |
child 71822 | 67cc2319104f |
permissions | -rw-r--r-- |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
2 |
|
60758 | 3 |
section \<open>Character and string types\<close> |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
4 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
5 |
theory String |
55969 | 6 |
imports Enum |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
7 |
begin |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
8 |
|
68028 | 9 |
subsection \<open>Strings as list of bytes\<close> |
10 |
||
11 |
text \<open> |
|
12 |
When modelling strings, we follow the approach given |
|
69593 | 13 |
in \<^url>\<open>https://utf8everywhere.org/\<close>: |
68028 | 14 |
|
15 |
\<^item> Strings are a list of bytes (8 bit). |
|
16 |
||
17 |
\<^item> Byte values from 0 to 127 are US-ASCII. |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
18 |
|
68028 | 19 |
\<^item> Byte values from 128 to 255 are uninterpreted blobs. |
20 |
\<close> |
|
21 |
||
22 |
subsubsection \<open>Bytes as datatype\<close> |
|
23 |
||
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
24 |
context unique_euclidean_semiring_with_bit_shifts |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
25 |
begin |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
26 |
|
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
27 |
lemma bit_horner_sum_iff: |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
28 |
\<open>bit (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) n \<longleftrightarrow> n < length bs \<and> bs ! n\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
29 |
proof (induction bs arbitrary: n) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
30 |
case Nil |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
31 |
then show ?case |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
32 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
33 |
next |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
34 |
case (Cons b bs) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
35 |
show ?case |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
36 |
proof (cases n) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
37 |
case 0 |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
38 |
then show ?thesis |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
39 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
40 |
next |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
41 |
case (Suc m) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
42 |
with bit_rec [of _ n] Cons.prems Cons.IH [of m] |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
43 |
show ?thesis by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
44 |
qed |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
45 |
qed |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
46 |
|
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
47 |
lemma take_bit_horner_sum_eq: |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
48 |
\<open>take_bit n (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) = foldr (\<lambda>b k. of_bool b + k * 2) (take n bs) 0\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
49 |
proof (induction bs arbitrary: n) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
50 |
case Nil |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
51 |
then show ?case |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
52 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
53 |
next |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
54 |
case (Cons b bs) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
55 |
show ?case |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
56 |
proof (cases n) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
57 |
case 0 |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
58 |
then show ?thesis |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
59 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
60 |
next |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
61 |
case (Suc m) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
62 |
with take_bit_rec [of n] Cons.prems Cons.IH [of m] |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
63 |
show ?thesis by (simp add: ac_simps) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
64 |
qed |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
65 |
qed |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
66 |
|
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
67 |
lemma (in semiring_bit_shifts) take_bit_eq_horner_sum: |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
68 |
\<open>take_bit n a = foldr (\<lambda>b k. of_bool b + k * 2) (map (bit a) [0..<n]) 0\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
69 |
proof (induction a arbitrary: n rule: bits_induct) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
70 |
case (stable a) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
71 |
have *: \<open>((\<lambda>k. k * 2) ^^ n) 0 = 0\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
72 |
by (induction n) simp_all |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
73 |
from stable have \<open>bit a = (\<lambda>_. odd a)\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
74 |
by (simp add: stable_imp_bit_iff_odd fun_eq_iff) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
75 |
then have \<open>map (bit a) [0..<n] = replicate n (odd a)\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
76 |
by (simp add: map_replicate_const) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
77 |
with stable show ?case |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
78 |
by (simp add: stable_imp_take_bit_eq mask_eq_seq_sum *) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
79 |
next |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
80 |
case (rec a b) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
81 |
show ?case |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
82 |
proof (cases n) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
83 |
case 0 |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
84 |
then show ?thesis |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
85 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
86 |
next |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
87 |
case (Suc m) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
88 |
have \<open>map (bit (of_bool b + 2 * a)) [0..<Suc m] = b # map (bit (of_bool b + 2 * a)) [Suc 0..<Suc m]\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
89 |
by (simp only: upt_conv_Cons) simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
90 |
also have \<open>\<dots> = b # map (bit a) [0..<m]\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
91 |
by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
92 |
finally show ?thesis |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
93 |
using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
94 |
qed |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
95 |
qed |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
96 |
|
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
97 |
end |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
98 |
|
68028 | 99 |
datatype char = |
100 |
Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool) |
|
101 |
(digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool) |
|
102 |
||
103 |
context comm_semiring_1 |
|
104 |
begin |
|
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
105 |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
106 |
definition of_char :: \<open>char \<Rightarrow> 'a\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
107 |
where \<open>of_char c = foldr (\<lambda>b k. of_bool b + k * 2) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
108 |
[digit0 c, digit1 c, digit2 c, digit3 c, digit4 c, digit5 c, digit6 c, digit7 c] 0\<close> |
68028 | 109 |
|
110 |
lemma of_char_Char [simp]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
111 |
\<open>of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
112 |
foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
113 |
by (simp add: of_char_def) |
68028 | 114 |
|
115 |
end |
|
116 |
||
71094 | 117 |
context unique_euclidean_semiring_with_bit_shifts |
68028 | 118 |
begin |
119 |
||
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
120 |
definition char_of :: \<open>'a \<Rightarrow> char\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
121 |
where \<open>char_of n = Char (odd n) (bit n 1) (bit n 2) (bit n 3) (bit n 4) (bit n 5) (bit n 6) (bit n 7)\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
122 |
|
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
123 |
lemma char_of_take_bit_eq: |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
124 |
\<open>char_of (take_bit n m) = char_of m\<close> if \<open>n \<ge> 8\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
125 |
using that by (simp add: char_of_def bit_take_bit_iff) |
68028 | 126 |
|
127 |
lemma char_of_char [simp]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
128 |
\<open>char_of (of_char c) = c\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
129 |
by (simp only: of_char_def char_of_def bit_horner_sum_iff) simp |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
130 |
|
68028 | 131 |
lemma char_of_comp_of_char [simp]: |
132 |
"char_of \<circ> of_char = id" |
|
133 |
by (simp add: fun_eq_iff) |
|
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
134 |
|
68028 | 135 |
lemma inj_of_char: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
136 |
\<open>inj of_char\<close> |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
137 |
proof (rule injI) |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
138 |
fix c d |
68028 | 139 |
assume "of_char c = of_char d" |
140 |
then have "char_of (of_char c) = char_of (of_char d)" |
|
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
141 |
by simp |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
142 |
then show "c = d" |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
143 |
by simp |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
144 |
qed |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
145 |
|
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
146 |
lemma of_char_eqI: |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
147 |
\<open>c = d\<close> if \<open>of_char c = of_char d\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
148 |
using that inj_of_char by (simp add: inj_eq) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
149 |
|
68028 | 150 |
lemma of_char_eq_iff [simp]: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
151 |
\<open>of_char c = of_char d \<longleftrightarrow> c = d\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
152 |
by (auto intro: of_char_eqI) |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
153 |
|
68028 | 154 |
lemma of_char_of [simp]: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
155 |
\<open>of_char (char_of a) = a mod 256\<close> |
68028 | 156 |
proof - |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
157 |
have \<open>[0..<8] = [0, Suc 0, 2, 3, 4, 5, 6, 7 :: nat]\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
158 |
by (simp add: upt_eq_Cons_conv) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
159 |
then have \<open>[odd a, bit a 1, bit a 2, bit a 3, bit a 4, bit a 5, bit a 6, bit a 7] = map (bit a) [0..<8]\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
160 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
161 |
then have \<open>of_char (char_of a) = take_bit 8 a\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
162 |
by (simp only: char_of_def of_char_def char.sel take_bit_eq_horner_sum) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
163 |
then show ?thesis |
68028 | 164 |
by (simp add: take_bit_eq_mod) |
165 |
qed |
|
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
166 |
|
68028 | 167 |
lemma char_of_mod_256 [simp]: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
168 |
\<open>char_of (n mod 256) = char_of n\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
169 |
by (rule of_char_eqI) simp |
68028 | 170 |
|
171 |
lemma of_char_mod_256 [simp]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
172 |
\<open>of_char c mod 256 = of_char c\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
173 |
proof - |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
174 |
have \<open>of_char (char_of (of_char c)) mod 256 = of_char (char_of (of_char c))\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
175 |
by (simp only: of_char_of) simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
176 |
then show ?thesis |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
177 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
178 |
qed |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
179 |
|
68028 | 180 |
lemma char_of_quasi_inj [simp]: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
181 |
\<open>char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
182 |
proof |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
183 |
assume ?Q |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
184 |
then show ?P |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
185 |
by (auto intro: of_char_eqI) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
186 |
next |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
187 |
assume ?P |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
188 |
then have \<open>of_char (char_of m) = of_char (char_of n)\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
189 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
190 |
then show ?Q |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
191 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
192 |
qed |
68028 | 193 |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
194 |
lemma char_of_eq_iff: |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
195 |
\<open>char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
196 |
by (auto intro: of_char_eqI simp add: take_bit_eq_mod) |
68028 | 197 |
|
198 |
lemma char_of_nat [simp]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
199 |
\<open>char_of (of_nat n) = char_of n\<close> |
68028 | 200 |
by (simp add: char_of_def String.char_of_def drop_bit_of_nat) |
68033
ad4b8b6892c3
uniform tagging for printable and non-printable literals
haftmann
parents:
68028
diff
changeset
|
201 |
|
68028 | 202 |
end |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
203 |
|
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
204 |
lemma inj_on_char_of_nat [simp]: |
68028 | 205 |
"inj_on char_of {0::nat..<256}" |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
206 |
by (rule inj_onI) simp |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
207 |
|
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
208 |
lemma nat_of_char_less_256 [simp]: |
68028 | 209 |
"of_char c < (256 :: nat)" |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
210 |
proof - |
68028 | 211 |
have "of_char c mod (256 :: nat) < 256" |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
212 |
by arith |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
213 |
then show ?thesis by simp |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
214 |
qed |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
215 |
|
68028 | 216 |
lemma range_nat_of_char: |
217 |
"range of_char = {0::nat..<256}" |
|
218 |
proof (rule; rule) |
|
219 |
fix n :: nat |
|
220 |
assume "n \<in> range of_char" |
|
221 |
then show "n \<in> {0..<256}" |
|
222 |
by auto |
|
223 |
next |
|
224 |
fix n :: nat |
|
225 |
assume "n \<in> {0..<256}" |
|
226 |
then have "n = of_char (char_of n)" |
|
227 |
by simp |
|
228 |
then show "n \<in> range of_char" |
|
229 |
by (rule range_eqI) |
|
230 |
qed |
|
231 |
||
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
232 |
lemma UNIV_char_of_nat: |
68028 | 233 |
"UNIV = char_of ` {0::nat..<256}" |
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
234 |
proof - |
68028 | 235 |
have "range (of_char :: char \<Rightarrow> nat) = of_char ` char_of ` {0::nat..<256}" |
236 |
by (auto simp add: range_nat_of_char intro!: image_eqI) |
|
237 |
with inj_of_char [where ?'a = nat] show ?thesis |
|
238 |
by (simp add: inj_image_eq_iff) |
|
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
239 |
qed |
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
240 |
|
62597 | 241 |
lemma card_UNIV_char: |
242 |
"card (UNIV :: char set) = 256" |
|
243 |
by (auto simp add: UNIV_char_of_nat card_image) |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
244 |
|
68028 | 245 |
context |
246 |
includes lifting_syntax integer.lifting natural.lifting |
|
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
247 |
begin |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
248 |
|
68028 | 249 |
lemma [transfer_rule]: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
250 |
\<open>(pcr_integer ===> (=)) char_of char_of\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
251 |
by (unfold char_of_def) transfer_prover |
68028 | 252 |
|
253 |
lemma [transfer_rule]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
254 |
\<open>((=) ===> pcr_integer) of_char of_char\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
255 |
by (unfold of_char_def) transfer_prover |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
256 |
|
68028 | 257 |
lemma [transfer_rule]: |
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
258 |
\<open>(pcr_natural ===> (=)) char_of char_of\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
259 |
by (unfold char_of_def) transfer_prover |
68028 | 260 |
|
261 |
lemma [transfer_rule]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
262 |
\<open>((=) ===> pcr_natural) of_char of_char\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
263 |
by (unfold of_char_def) transfer_prover |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
264 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
265 |
end |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
266 |
|
68028 | 267 |
lifting_update integer.lifting |
268 |
lifting_forget integer.lifting |
|
64630
96015aecfeba
emphasize dedicated rewrite rules for congruences
haftmann
parents:
63950
diff
changeset
|
269 |
|
68028 | 270 |
lifting_update natural.lifting |
271 |
lifting_forget natural.lifting |
|
62364
9209770bdcdf
more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents:
61799
diff
changeset
|
272 |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
273 |
syntax |
62597 | 274 |
"_Char" :: "str_position \<Rightarrow> char" ("CHR _") |
62678 | 275 |
"_Char_ord" :: "num_const \<Rightarrow> char" ("CHR _") |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
276 |
|
42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
41750
diff
changeset
|
277 |
type_synonym string = "char list" |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
278 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
279 |
syntax |
68028 | 280 |
"_String" :: "str_position \<Rightarrow> string" ("_") |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
281 |
|
69605 | 282 |
ML_file \<open>Tools/string_syntax.ML\<close> |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
283 |
|
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
284 |
instantiation char :: enum |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
285 |
begin |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
286 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
287 |
definition |
68028 | 288 |
"Enum.enum = [ |
289 |
CHR 0x00, CHR 0x01, CHR 0x02, CHR 0x03, |
|
62678 | 290 |
CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07, |
291 |
CHR 0x08, CHR 0x09, CHR ''\<newline>'', CHR 0x0B, |
|
292 |
CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F, |
|
293 |
CHR 0x10, CHR 0x11, CHR 0x12, CHR 0x13, |
|
294 |
CHR 0x14, CHR 0x15, CHR 0x16, CHR 0x17, |
|
295 |
CHR 0x18, CHR 0x19, CHR 0x1A, CHR 0x1B, |
|
296 |
CHR 0x1C, CHR 0x1D, CHR 0x1E, CHR 0x1F, |
|
297 |
CHR '' '', CHR ''!'', CHR 0x22, CHR ''#'', |
|
298 |
CHR ''$'', CHR ''%'', CHR ''&'', CHR 0x27, |
|
62597 | 299 |
CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', |
300 |
CHR '','', CHR ''-'', CHR ''.'', CHR ''/'', |
|
301 |
CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', |
|
302 |
CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', |
|
303 |
CHR ''8'', CHR ''9'', CHR '':'', CHR '';'', |
|
304 |
CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', |
|
305 |
CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'', |
|
306 |
CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', |
|
307 |
CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'', |
|
308 |
CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'', |
|
309 |
CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', |
|
310 |
CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'', |
|
311 |
CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', |
|
62678 | 312 |
CHR 0x5C, CHR '']'', CHR ''^'', CHR ''_'', |
313 |
CHR 0x60, CHR ''a'', CHR ''b'', CHR ''c'', |
|
62597 | 314 |
CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', |
315 |
CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'', |
|
316 |
CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', |
|
317 |
CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'', |
|
318 |
CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'', |
|
319 |
CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', |
|
62678 | 320 |
CHR ''|'', CHR ''}'', CHR ''~'', CHR 0x7F, |
321 |
CHR 0x80, CHR 0x81, CHR 0x82, CHR 0x83, |
|
322 |
CHR 0x84, CHR 0x85, CHR 0x86, CHR 0x87, |
|
323 |
CHR 0x88, CHR 0x89, CHR 0x8A, CHR 0x8B, |
|
324 |
CHR 0x8C, CHR 0x8D, CHR 0x8E, CHR 0x8F, |
|
325 |
CHR 0x90, CHR 0x91, CHR 0x92, CHR 0x93, |
|
326 |
CHR 0x94, CHR 0x95, CHR 0x96, CHR 0x97, |
|
327 |
CHR 0x98, CHR 0x99, CHR 0x9A, CHR 0x9B, |
|
328 |
CHR 0x9C, CHR 0x9D, CHR 0x9E, CHR 0x9F, |
|
329 |
CHR 0xA0, CHR 0xA1, CHR 0xA2, CHR 0xA3, |
|
330 |
CHR 0xA4, CHR 0xA5, CHR 0xA6, CHR 0xA7, |
|
331 |
CHR 0xA8, CHR 0xA9, CHR 0xAA, CHR 0xAB, |
|
332 |
CHR 0xAC, CHR 0xAD, CHR 0xAE, CHR 0xAF, |
|
333 |
CHR 0xB0, CHR 0xB1, CHR 0xB2, CHR 0xB3, |
|
334 |
CHR 0xB4, CHR 0xB5, CHR 0xB6, CHR 0xB7, |
|
335 |
CHR 0xB8, CHR 0xB9, CHR 0xBA, CHR 0xBB, |
|
336 |
CHR 0xBC, CHR 0xBD, CHR 0xBE, CHR 0xBF, |
|
337 |
CHR 0xC0, CHR 0xC1, CHR 0xC2, CHR 0xC3, |
|
338 |
CHR 0xC4, CHR 0xC5, CHR 0xC6, CHR 0xC7, |
|
339 |
CHR 0xC8, CHR 0xC9, CHR 0xCA, CHR 0xCB, |
|
340 |
CHR 0xCC, CHR 0xCD, CHR 0xCE, CHR 0xCF, |
|
341 |
CHR 0xD0, CHR 0xD1, CHR 0xD2, CHR 0xD3, |
|
342 |
CHR 0xD4, CHR 0xD5, CHR 0xD6, CHR 0xD7, |
|
343 |
CHR 0xD8, CHR 0xD9, CHR 0xDA, CHR 0xDB, |
|
344 |
CHR 0xDC, CHR 0xDD, CHR 0xDE, CHR 0xDF, |
|
345 |
CHR 0xE0, CHR 0xE1, CHR 0xE2, CHR 0xE3, |
|
346 |
CHR 0xE4, CHR 0xE5, CHR 0xE6, CHR 0xE7, |
|
347 |
CHR 0xE8, CHR 0xE9, CHR 0xEA, CHR 0xEB, |
|
348 |
CHR 0xEC, CHR 0xED, CHR 0xEE, CHR 0xEF, |
|
349 |
CHR 0xF0, CHR 0xF1, CHR 0xF2, CHR 0xF3, |
|
350 |
CHR 0xF4, CHR 0xF5, CHR 0xF6, CHR 0xF7, |
|
351 |
CHR 0xF8, CHR 0xF9, CHR 0xFA, CHR 0xFB, |
|
352 |
CHR 0xFC, CHR 0xFD, CHR 0xFE, CHR 0xFF]" |
|
31484 | 353 |
|
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
354 |
definition |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
355 |
"Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
356 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
357 |
definition |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
358 |
"Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
359 |
|
62597 | 360 |
lemma enum_char_unfold: |
68028 | 361 |
"Enum.enum = map char_of [0..<256]" |
62597 | 362 |
proof - |
68028 | 363 |
have "map (of_char :: char \<Rightarrow> nat) Enum.enum = [0..<256]" |
364 |
by (simp add: enum_char_def of_char_def upt_conv_Cons_Cons numeral_2_eq_2 [symmetric]) |
|
365 |
then have "map char_of (map (of_char :: char \<Rightarrow> nat) Enum.enum) = |
|
366 |
map char_of [0..<256]" |
|
367 |
by simp |
|
368 |
then show ?thesis |
|
369 |
by simp |
|
62597 | 370 |
qed |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset
|
371 |
|
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
372 |
instance proof |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
373 |
show UNIV: "UNIV = set (Enum.enum :: char list)" |
62597 | 374 |
by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan) |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
375 |
show "distinct (Enum.enum :: char list)" |
62597 | 376 |
by (auto simp add: enum_char_unfold distinct_map intro: inj_onI) |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
377 |
show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
378 |
by (simp add: UNIV enum_all_char_def list_all_iff) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
379 |
show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
380 |
by (simp add: UNIV enum_ex_char_def list_ex_iff) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
381 |
qed |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
382 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
383 |
end |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
384 |
|
68028 | 385 |
lemma linorder_char: |
386 |
"class.linorder (\<lambda>c d. of_char c \<le> (of_char d :: nat)) (\<lambda>c d. of_char c < (of_char d :: nat))" |
|
387 |
by standard auto |
|
388 |
||
389 |
text \<open>Optimized version for execution\<close> |
|
390 |
||
391 |
definition char_of_integer :: "integer \<Rightarrow> char" |
|
392 |
where [code_abbrev]: "char_of_integer = char_of" |
|
393 |
||
394 |
definition integer_of_char :: "char \<Rightarrow> integer" |
|
395 |
where [code_abbrev]: "integer_of_char = of_char" |
|
396 |
||
62597 | 397 |
lemma char_of_integer_code [code]: |
68028 | 398 |
"char_of_integer k = (let |
399 |
(q0, b0) = bit_cut_integer k; |
|
400 |
(q1, b1) = bit_cut_integer q0; |
|
401 |
(q2, b2) = bit_cut_integer q1; |
|
402 |
(q3, b3) = bit_cut_integer q2; |
|
403 |
(q4, b4) = bit_cut_integer q3; |
|
404 |
(q5, b5) = bit_cut_integer q4; |
|
405 |
(q6, b6) = bit_cut_integer q5; |
|
406 |
(_, b7) = bit_cut_integer q6 |
|
407 |
in Char b0 b1 b2 b3 b4 b5 b6 b7)" |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
408 |
by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq bit_iff_odd_drop_bit drop_bit_eq_div) |
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset
|
409 |
|
68028 | 410 |
lemma integer_of_char_code [code]: |
411 |
"integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = |
|
412 |
((((((of_bool b7 * 2 + of_bool b6) * 2 + |
|
413 |
of_bool b5) * 2 + of_bool b4) * 2 + |
|
414 |
of_bool b3) * 2 + of_bool b2) * 2 + |
|
415 |
of_bool b1) * 2 + of_bool b0" |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
416 |
by (simp add: integer_of_char_def of_char_def) |
66331 | 417 |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
418 |
|
68028 | 419 |
subsection \<open>Strings as dedicated type for target language code generation\<close> |
420 |
||
421 |
subsubsection \<open>Logical specification\<close> |
|
422 |
||
423 |
context |
|
424 |
begin |
|
425 |
||
426 |
qualified definition ascii_of :: "char \<Rightarrow> char" |
|
427 |
where "ascii_of c = Char (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) False" |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
428 |
|
68028 | 429 |
qualified lemma ascii_of_Char [simp]: |
430 |
"ascii_of (Char b0 b1 b2 b3 b4 b5 b6 b7) = Char b0 b1 b2 b3 b4 b5 b6 False" |
|
431 |
by (simp add: ascii_of_def) |
|
432 |
||
433 |
qualified lemma not_digit7_ascii_of [simp]: |
|
434 |
"\<not> digit7 (ascii_of c)" |
|
435 |
by (simp add: ascii_of_def) |
|
436 |
||
437 |
qualified lemma ascii_of_idem: |
|
438 |
"ascii_of c = c" if "\<not> digit7 c" |
|
439 |
using that by (cases c) simp |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
440 |
|
68028 | 441 |
qualified lemma char_of_ascii_of [simp]: |
442 |
"of_char (ascii_of c) = take_bit 7 (of_char c :: nat)" |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
443 |
by (cases c) (simp only: ascii_of_Char of_char_Char take_bit_horner_sum_eq, simp) |
68028 | 444 |
|
445 |
qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}" |
|
446 |
morphisms explode Abs_literal |
|
447 |
proof |
|
448 |
show "[] \<in> {cs. \<forall>c\<in>set cs. \<not> digit7 c}" |
|
449 |
by simp |
|
450 |
qed |
|
451 |
||
452 |
qualified setup_lifting type_definition_literal |
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
59483
diff
changeset
|
453 |
|
68028 | 454 |
qualified lift_definition implode :: "string \<Rightarrow> literal" |
455 |
is "map ascii_of" |
|
456 |
by auto |
|
457 |
||
458 |
qualified lemma implode_explode_eq [simp]: |
|
459 |
"String.implode (String.explode s) = s" |
|
460 |
proof transfer |
|
461 |
fix cs |
|
462 |
show "map ascii_of cs = cs" if "\<forall>c\<in>set cs. \<not> digit7 c" |
|
463 |
using that |
|
464 |
by (induction cs) (simp_all add: ascii_of_idem) |
|
465 |
qed |
|
466 |
||
467 |
qualified lemma explode_implode_eq [simp]: |
|
468 |
"String.explode (String.implode cs) = map ascii_of cs" |
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
59483
diff
changeset
|
469 |
by transfer rule |
54594
a2d1522cdd54
setup lifting/transfer for String.literal
Andreas Lochbihler
parents:
54317
diff
changeset
|
470 |
|
68028 | 471 |
end |
472 |
||
473 |
||
474 |
subsubsection \<open>Syntactic representation\<close> |
|
475 |
||
476 |
text \<open> |
|
477 |
Logical ground representations for literals are: |
|
478 |
||
69272 | 479 |
\<^enum> \<open>0\<close> for the empty literal; |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66190
diff
changeset
|
480 |
|
69272 | 481 |
\<^enum> \<open>Literal b0 \<dots> b6 s\<close> for a literal starting with one |
68028 | 482 |
character and continued by another literal. |
483 |
||
484 |
Syntactic representations for literals are: |
|
485 |
||
69272 | 486 |
\<^enum> Printable text as string prefixed with \<open>STR\<close>; |
68028 | 487 |
|
69272 | 488 |
\<^enum> A single ascii value as numerical hexadecimal value prefixed with \<open>STR\<close>. |
68028 | 489 |
\<close> |
490 |
||
491 |
instantiation String.literal :: zero |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
492 |
begin |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
493 |
|
68028 | 494 |
context |
495 |
begin |
|
496 |
||
497 |
qualified lift_definition zero_literal :: String.literal |
|
498 |
is Nil |
|
499 |
by simp |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
500 |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
501 |
instance .. |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
502 |
|
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
503 |
end |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
504 |
|
68028 | 505 |
end |
506 |
||
507 |
context |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
508 |
begin |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
509 |
|
68028 | 510 |
qualified abbreviation (output) empty_literal :: String.literal |
511 |
where "empty_literal \<equiv> 0" |
|
512 |
||
513 |
qualified lift_definition Literal :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal" |
|
514 |
is "\<lambda>b0 b1 b2 b3 b4 b5 b6 cs. Char b0 b1 b2 b3 b4 b5 b6 False # cs" |
|
515 |
by auto |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
516 |
|
68028 | 517 |
qualified lemma Literal_eq_iff [simp]: |
518 |
"Literal b0 b1 b2 b3 b4 b5 b6 s = Literal c0 c1 c2 c3 c4 c5 c6 t |
|
519 |
\<longleftrightarrow> (b0 \<longleftrightarrow> c0) \<and> (b1 \<longleftrightarrow> c1) \<and> (b2 \<longleftrightarrow> c2) \<and> (b3 \<longleftrightarrow> c3) |
|
520 |
\<and> (b4 \<longleftrightarrow> c4) \<and> (b5 \<longleftrightarrow> c5) \<and> (b6 \<longleftrightarrow> c6) \<and> s = t" |
|
521 |
by transfer simp |
|
522 |
||
523 |
qualified lemma empty_neq_Literal [simp]: |
|
524 |
"empty_literal \<noteq> Literal b0 b1 b2 b3 b4 b5 b6 s" |
|
525 |
by transfer simp |
|
526 |
||
527 |
qualified lemma Literal_neq_empty [simp]: |
|
528 |
"Literal b0 b1 b2 b3 b4 b5 b6 s \<noteq> empty_literal" |
|
529 |
by transfer simp |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
530 |
|
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
531 |
end |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
532 |
|
68028 | 533 |
code_datatype "0 :: String.literal" String.Literal |
534 |
||
535 |
syntax |
|
536 |
"_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _") |
|
68033
ad4b8b6892c3
uniform tagging for printable and non-printable literals
haftmann
parents:
68028
diff
changeset
|
537 |
"_Ascii" :: "num_const \<Rightarrow> String.literal" ("STR _") |
54594
a2d1522cdd54
setup lifting/transfer for String.literal
Andreas Lochbihler
parents:
54317
diff
changeset
|
538 |
|
69605 | 539 |
ML_file \<open>Tools/literal.ML\<close> |
68028 | 540 |
|
52365
95186e6e4bf4
reflexive nbe equation for equality on String.literal
haftmann
parents:
51717
diff
changeset
|
541 |
|
68028 | 542 |
subsubsection \<open>Operations\<close> |
543 |
||
544 |
instantiation String.literal :: plus |
|
67730 | 545 |
begin |
546 |
||
68028 | 547 |
context |
548 |
begin |
|
549 |
||
550 |
qualified lift_definition plus_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal" |
|
551 |
is "(@)" |
|
552 |
by auto |
|
67730 | 553 |
|
554 |
instance .. |
|
555 |
||
556 |
end |
|
557 |
||
68028 | 558 |
end |
67730 | 559 |
|
68028 | 560 |
instance String.literal :: monoid_add |
561 |
by (standard; transfer) simp_all |
|
562 |
||
563 |
instantiation String.literal :: size |
|
67729 | 564 |
begin |
565 |
||
68028 | 566 |
context |
567 |
includes literal.lifting |
|
568 |
begin |
|
569 |
||
570 |
lift_definition size_literal :: "String.literal \<Rightarrow> nat" |
|
571 |
is length . |
|
572 |
||
573 |
end |
|
67729 | 574 |
|
575 |
instance .. |
|
576 |
||
577 |
end |
|
578 |
||
68028 | 579 |
instantiation String.literal :: equal |
580 |
begin |
|
581 |
||
582 |
context |
|
583 |
begin |
|
584 |
||
585 |
qualified lift_definition equal_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" |
|
586 |
is HOL.equal . |
|
587 |
||
588 |
instance |
|
589 |
by (standard; transfer) (simp add: equal) |
|
590 |
||
591 |
end |
|
592 |
||
593 |
end |
|
594 |
||
595 |
instantiation String.literal :: linorder |
|
596 |
begin |
|
67729 | 597 |
|
68028 | 598 |
context |
599 |
begin |
|
600 |
||
601 |
qualified lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" |
|
602 |
is "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))" |
|
603 |
. |
|
604 |
||
605 |
qualified lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" |
|
606 |
is "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))" |
|
607 |
. |
|
608 |
||
609 |
instance proof - |
|
610 |
from linorder_char interpret linorder "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))" |
|
611 |
"ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool" |
|
612 |
by (rule linorder.lexordp_linorder) |
|
613 |
show "PROP ?thesis" |
|
614 |
by (standard; transfer) (simp_all add: less_le_not_le linear) |
|
615 |
qed |
|
616 |
||
617 |
end |
|
618 |
||
619 |
end |
|
67730 | 620 |
|
68028 | 621 |
lemma infinite_literal: |
622 |
"infinite (UNIV :: String.literal set)" |
|
623 |
proof - |
|
624 |
define S where "S = range (\<lambda>n. replicate n CHR ''A'')" |
|
625 |
have "inj_on String.implode S" |
|
626 |
proof (rule inj_onI) |
|
627 |
fix cs ds |
|
628 |
assume "String.implode cs = String.implode ds" |
|
629 |
then have "String.explode (String.implode cs) = String.explode (String.implode ds)" |
|
630 |
by simp |
|
631 |
moreover assume "cs \<in> S" and "ds \<in> S" |
|
632 |
ultimately show "cs = ds" |
|
633 |
by (auto simp add: S_def) |
|
634 |
qed |
|
635 |
moreover have "infinite S" |
|
636 |
by (auto simp add: S_def dest: finite_range_imageI [of _ length]) |
|
637 |
ultimately have "infinite (String.implode ` S)" |
|
638 |
by (simp add: finite_image_iff) |
|
639 |
then show ?thesis |
|
640 |
by (auto intro: finite_subset) |
|
641 |
qed |
|
642 |
||
643 |
||
644 |
subsubsection \<open>Executable conversions\<close> |
|
645 |
||
646 |
context |
|
647 |
begin |
|
648 |
||
649 |
qualified lift_definition asciis_of_literal :: "String.literal \<Rightarrow> integer list" |
|
650 |
is "map of_char" |
|
651 |
. |
|
652 |
||
69879 | 653 |
qualified lemma asciis_of_zero [simp, code]: |
654 |
"asciis_of_literal 0 = []" |
|
655 |
by transfer simp |
|
656 |
||
657 |
qualified lemma asciis_of_Literal [simp, code]: |
|
658 |
"asciis_of_literal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) = |
|
659 |
of_char (Char b0 b1 b2 b3 b4 b5 b6 False) # asciis_of_literal s " |
|
660 |
by transfer simp |
|
661 |
||
68028 | 662 |
qualified lift_definition literal_of_asciis :: "integer list \<Rightarrow> String.literal" |
663 |
is "map (String.ascii_of \<circ> char_of)" |
|
664 |
by auto |
|
55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
55015
diff
changeset
|
665 |
|
69879 | 666 |
qualified lemma literal_of_asciis_Nil [simp, code]: |
667 |
"literal_of_asciis [] = 0" |
|
668 |
by transfer simp |
|
669 |
||
670 |
qualified lemma literal_of_asciis_Cons [simp, code]: |
|
671 |
"literal_of_asciis (k # ks) = (case char_of k |
|
672 |
of Char b0 b1 b2 b3 b4 b5 b6 b7 \<Rightarrow> String.Literal b0 b1 b2 b3 b4 b5 b6 (literal_of_asciis ks))" |
|
673 |
by (simp add: char_of_def) (transfer, simp add: char_of_def) |
|
674 |
||
68028 | 675 |
qualified lemma literal_of_asciis_of_literal [simp]: |
676 |
"literal_of_asciis (asciis_of_literal s) = s" |
|
677 |
proof transfer |
|
678 |
fix cs |
|
679 |
assume "\<forall>c\<in>set cs. \<not> digit7 c" |
|
680 |
then show "map (String.ascii_of \<circ> char_of) (map of_char cs) = cs" |
|
681 |
by (induction cs) (simp_all add: String.ascii_of_idem) |
|
682 |
qed |
|
683 |
||
684 |
qualified lemma explode_code [code]: |
|
685 |
"String.explode s = map char_of (asciis_of_literal s)" |
|
686 |
by transfer simp |
|
687 |
||
688 |
qualified lemma implode_code [code]: |
|
689 |
"String.implode cs = literal_of_asciis (map of_char cs)" |
|
690 |
by transfer simp |
|
64994
6e4c05e8edbb
computation preprocessing rules to allow literals as input for computations
haftmann
parents:
64630
diff
changeset
|
691 |
|
69879 | 692 |
qualified lemma equal_literal [code]: |
693 |
"HOL.equal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) |
|
694 |
(String.Literal a0 a1 a2 a3 a4 a5 a6 r) |
|
695 |
\<longleftrightarrow> (b0 \<longleftrightarrow> a0) \<and> (b1 \<longleftrightarrow> a1) \<and> (b2 \<longleftrightarrow> a2) \<and> (b3 \<longleftrightarrow> a3) |
|
696 |
\<and> (b4 \<longleftrightarrow> a4) \<and> (b5 \<longleftrightarrow> a5) \<and> (b6 \<longleftrightarrow> a6) \<and> (s = r)" |
|
697 |
by (simp add: equal) |
|
68028 | 698 |
|
69879 | 699 |
end |
68028 | 700 |
|
701 |
||
702 |
subsubsection \<open>Technical code generation setup\<close> |
|
703 |
||
704 |
text \<open>Alternative constructor for generated computations\<close> |
|
705 |
||
706 |
context |
|
707 |
begin |
|
708 |
||
709 |
qualified definition Literal' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal" |
|
710 |
where [simp]: "Literal' = String.Literal" |
|
711 |
||
712 |
lemma [code]: |
|
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
713 |
\<open>Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
714 |
[foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
715 |
proof - |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
716 |
have \<open>foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0 = of_char (Char b0 b1 b2 b3 b4 b5 b6 False)\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
717 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
718 |
moreover have \<open>Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
719 |
[of_char (Char b0 b1 b2 b3 b4 b5 b6 False)] + s\<close> |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
720 |
by (unfold Literal'_def) (transfer, simp only: list.simps comp_apply char_of_char, simp) |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
721 |
ultimately show ?thesis |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
722 |
by simp |
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71094
diff
changeset
|
723 |
qed |
64994
6e4c05e8edbb
computation preprocessing rules to allow literals as input for computations
haftmann
parents:
64630
diff
changeset
|
724 |
|
6e4c05e8edbb
computation preprocessing rules to allow literals as input for computations
haftmann
parents:
64630
diff
changeset
|
725 |
lemma [code_computation_unfold]: |
68028 | 726 |
"String.Literal = Literal'" |
727 |
by simp |
|
64994
6e4c05e8edbb
computation preprocessing rules to allow literals as input for computations
haftmann
parents:
64630
diff
changeset
|
728 |
|
68028 | 729 |
end |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
730 |
|
69879 | 731 |
code_reserved SML string String Char List |
68028 | 732 |
code_reserved OCaml string String Char List |
733 |
code_reserved Haskell Prelude |
|
34886 | 734 |
code_reserved Scala string |
33237 | 735 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
736 |
code_printing |
68028 | 737 |
type_constructor String.literal \<rightharpoonup> |
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
738 |
(SML) "string" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
739 |
and (OCaml) "string" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
740 |
and (Haskell) "String" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
741 |
and (Scala) "String" |
68028 | 742 |
| constant "STR ''''" \<rightharpoonup> |
743 |
(SML) "\"\"" |
|
744 |
and (OCaml) "\"\"" |
|
745 |
and (Haskell) "\"\"" |
|
746 |
and (Scala) "\"\"" |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
747 |
|
60758 | 748 |
setup \<open> |
68028 | 749 |
fold Literal.add_code ["SML", "OCaml", "Haskell", "Scala"] |
60758 | 750 |
\<close> |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
751 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
752 |
code_printing |
68028 | 753 |
constant "(+) :: String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal" \<rightharpoonup> |
754 |
(SML) infixl 18 "^" |
|
755 |
and (OCaml) infixr 6 "^" |
|
756 |
and (Haskell) infixr 5 "++" |
|
757 |
and (Scala) infixl 7 "+" |
|
758 |
| constant String.literal_of_asciis \<rightharpoonup> |
|
69879 | 759 |
(SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))" |
69743 | 760 |
and (OCaml) "!(let xs = _ |
761 |
and chr k = |
|
69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69879
diff
changeset
|
762 |
let l = Z.to'_int k |
69743 | 763 |
in if 0 <= l && l < 128 |
764 |
then Char.chr l |
|
765 |
else failwith \"Non-ASCII character in literal\" |
|
766 |
in String.init (List.length xs) (List.nth (List.map chr xs)))" |
|
68028 | 767 |
and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)" |
768 |
and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))" |
|
769 |
| constant String.asciis_of_literal \<rightharpoonup> |
|
69879 | 770 |
(SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)" |
69743 | 771 |
and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in |
69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69879
diff
changeset
|
772 |
if k < 128 then Z.of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])" |
68028 | 773 |
and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))" |
774 |
and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))" |
|
775 |
| class_instance String.literal :: equal \<rightharpoonup> |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
776 |
(Haskell) - |
68028 | 777 |
| constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
778 |
(SML) "!((_ : string) = _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
779 |
and (OCaml) "!((_ : string) = _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
780 |
and (Haskell) infix 4 "==" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset
|
781 |
and (Scala) infixl 5 "==" |
68028 | 782 |
| constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |
783 |
(SML) "!((_ : string) <= _)" |
|
784 |
and (OCaml) "!((_ : string) <= _)" |
|
69743 | 785 |
and (Haskell) infix 4 "<=" |
69593 | 786 |
\<comment> \<open>Order operations for \<^typ>\<open>String.literal\<close> work in Haskell only |
68028 | 787 |
if no type class instance needs to be generated, because String = [Char] in Haskell |
69593 | 788 |
and \<^typ>\<open>char list\<close> need not have the same order as \<^typ>\<open>String.literal\<close>.\<close> |
68028 | 789 |
and (Scala) infixl 4 "<=" |
790 |
and (Eval) infixl 6 "<=" |
|
791 |
| constant "(<) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |
|
792 |
(SML) "!((_ : string) < _)" |
|
793 |
and (OCaml) "!((_ : string) < _)" |
|
794 |
and (Haskell) infix 4 "<" |
|
795 |
and (Scala) infixl 4 "<" |
|
796 |
and (Eval) infixl 6 "<" |
|
797 |
||
798 |
||
799 |
subsubsection \<open>Code generation utility\<close> |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
800 |
|
60758 | 801 |
setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close> |
52910
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset
|
802 |
|
68028 | 803 |
definition abort :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" |
804 |
where [simp]: "abort _ f = f ()" |
|
52910
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset
|
805 |
|
68028 | 806 |
declare [[code drop: Code.abort]] |
807 |
||
808 |
lemma abort_cong: |
|
809 |
"msg = msg' \<Longrightarrow> Code.abort msg f = Code.abort msg' f" |
|
810 |
by simp |
|
54317
da932f511746
add congruence rule to prevent code_simp from looping
Andreas Lochbihler
parents:
52910
diff
changeset
|
811 |
|
60758 | 812 |
setup \<open>Sign.map_naming Name_Space.parent_path\<close> |
52910
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset
|
813 |
|
60758 | 814 |
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close> |
54317
da932f511746
add congruence rule to prevent code_simp from looping
Andreas Lochbihler
parents:
52910
diff
changeset
|
815 |
|
68028 | 816 |
code_printing |
817 |
constant Code.abort \<rightharpoonup> |
|
52910
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset
|
818 |
(SML) "!(raise/ Fail/ _)" |
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset
|
819 |
and (OCaml) "failwith" |
59483
ddb73392356e
explicit type annotation avoids problems with Haskell type inference
haftmann
parents:
58889
diff
changeset
|
820 |
and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)" |
68028 | 821 |
and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }" |
822 |
||
52910
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset
|
823 |
|
68028 | 824 |
subsubsection \<open>Finally\<close> |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31176
diff
changeset
|
825 |
|
68028 | 826 |
lifting_update literal.lifting |
827 |
lifting_forget literal.lifting |
|
57437 | 828 |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
829 |
end |