author  Andreas Lochbihler 
Wed, 09 Oct 2013 15:33:20 +0200  
changeset 54317  da932f511746 
parent 52910  7bfe0df532a9 
child 54594  a2d1522cdd54 
permissions  rwrr 
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 

4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

3 
header {* Character and string types *} 
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 
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

6 
imports List 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 

49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

9 
subsection {* Characters and strings *} 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

10 

4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

11 
datatype nibble = 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

12 
Nibble0  Nibble1  Nibble2  Nibble3  Nibble4  Nibble5  Nibble6  Nibble7 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

13 
 Nibble8  Nibble9  NibbleA  NibbleB  NibbleC  NibbleD  NibbleE  NibbleF 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

14 

4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

15 
lemma UNIV_nibble: 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

16 
"UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

17 
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A") 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

18 
proof (rule UNIV_eq_I) 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

19 
fix x show "x \<in> ?A" by (cases x) simp_all 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

20 
qed 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

21 

49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

22 
lemma size_nibble [code, simp]: 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

23 
"size (x::nibble) = 0" by (cases x) simp_all 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

24 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

25 
lemma nibble_size [code, simp]: 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

26 
"nibble_size (x::nibble) = 0" by (cases x) simp_all 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

27 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

28 
instantiation nibble :: enum 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

29 
begin 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

30 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

31 
definition 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

32 
"Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

33 
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]" 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

34 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

35 
definition 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

36 
"Enum.enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

37 
\<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF" 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

38 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

39 
definition 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

40 
"Enum.enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

41 
\<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF" 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

42 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

43 
instance proof 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

44 
qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all) 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

45 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

46 
end 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

47 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

48 
lemma card_UNIV_nibble: 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

49 
"card (UNIV :: nibble set) = 16" 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

50 
by (simp add: card_UNIV_length_enum enum_nibble_def) 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

51 

51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

52 
primrec nat_of_nibble :: "nibble \<Rightarrow> nat" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

53 
where 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

54 
"nat_of_nibble Nibble0 = 0" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

55 
 "nat_of_nibble Nibble1 = 1" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

56 
 "nat_of_nibble Nibble2 = 2" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

57 
 "nat_of_nibble Nibble3 = 3" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

58 
 "nat_of_nibble Nibble4 = 4" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

59 
 "nat_of_nibble Nibble5 = 5" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

60 
 "nat_of_nibble Nibble6 = 6" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

61 
 "nat_of_nibble Nibble7 = 7" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

62 
 "nat_of_nibble Nibble8 = 8" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

63 
 "nat_of_nibble Nibble9 = 9" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

64 
 "nat_of_nibble NibbleA = 10" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

65 
 "nat_of_nibble NibbleB = 11" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

66 
 "nat_of_nibble NibbleC = 12" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

67 
 "nat_of_nibble NibbleD = 13" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

68 
 "nat_of_nibble NibbleE = 14" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

69 
 "nat_of_nibble NibbleF = 15" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

70 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

71 
definition nibble_of_nat :: "nat \<Rightarrow> nibble" where 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

72 
"nibble_of_nat n = Enum.enum ! (n mod 16)" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

73 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

74 
lemma nibble_of_nat_simps [simp]: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

75 
"nibble_of_nat 0 = Nibble0" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

76 
"nibble_of_nat 1 = Nibble1" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

77 
"nibble_of_nat 2 = Nibble2" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

78 
"nibble_of_nat 3 = Nibble3" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

79 
"nibble_of_nat 4 = Nibble4" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

80 
"nibble_of_nat 5 = Nibble5" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

81 
"nibble_of_nat 6 = Nibble6" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

82 
"nibble_of_nat 7 = Nibble7" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

83 
"nibble_of_nat 8 = Nibble8" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

84 
"nibble_of_nat 9 = Nibble9" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

85 
"nibble_of_nat 10 = NibbleA" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

86 
"nibble_of_nat 11 = NibbleB" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

87 
"nibble_of_nat 12 = NibbleC" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

88 
"nibble_of_nat 13 = NibbleD" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

89 
"nibble_of_nat 14 = NibbleE" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

90 
"nibble_of_nat 15 = NibbleF" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

91 
unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

92 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

93 
lemma nibble_of_nat_of_nibble [simp]: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

94 
"nibble_of_nat (nat_of_nibble x) = x" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

95 
by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

96 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

97 
lemma nat_of_nibble_of_nat [simp]: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

98 
"nat_of_nibble (nibble_of_nat n) = n mod 16" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

99 
by (cases "nibble_of_nat n") 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

100 
(simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

101 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

102 
lemma inj_nat_of_nibble: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

103 
"inj nat_of_nibble" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

104 
by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

105 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

106 
lemma nat_of_nibble_eq_iff: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

107 
"nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

108 
by (rule inj_eq) (rule inj_nat_of_nibble) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

109 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

110 
lemma nat_of_nibble_less_16: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

111 
"nat_of_nibble x < 16" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

112 
by (cases x) auto 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

113 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

114 
lemma nibble_of_nat_mod_16: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

115 
"nibble_of_nat (n mod 16) = nibble_of_nat n" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

116 
by (simp add: nibble_of_nat_def) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

117 

31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

118 
datatype char = Char nibble nibble 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

119 
 "Note: canonical order of character encoding coincides with standard term ordering" 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

120 

4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

121 
syntax 
46483  122 
"_Char" :: "str_position => char" ("CHR _") 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

123 

42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
41750
diff
changeset

124 
type_synonym string = "char list" 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

125 

4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

126 
syntax 
46483  127 
"_String" :: "str_position => string" ("_") 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

128 

48891  129 
ML_file "Tools/string_syntax.ML" 
35123  130 
setup String_Syntax.setup 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

131 

49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

132 
lemma UNIV_char: 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

133 
"UNIV = image (split Char) (UNIV \<times> UNIV)" 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

134 
proof (rule UNIV_eq_I) 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

135 
fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

136 
qed 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

137 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

138 
lemma size_char [code, simp]: 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

139 
"size (c::char) = 0" by (cases c) simp 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

140 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

141 
lemma char_size [code, simp]: 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

142 
"char_size (c::char) = 0" by (cases c) simp 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

143 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

144 
instantiation char :: enum 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

145 
begin 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

146 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

147 
definition 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

148 
"Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2, 
31484  149 
Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5, 
150 
Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8, 

151 
Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB, 

152 
Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE, 

153 
Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1, 

154 
Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4, 

155 
Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7, 

156 
Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA, 

157 
Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD, 

158 
Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'', 

159 
Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'', 

160 
Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','', 

161 
CHR '''', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', 

162 
CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'', 

163 
CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'', 

164 
CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'', 

165 
CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'', 

166 
CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'', 

167 
CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC, 

168 
CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'', 

169 
CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'', 

170 
CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'', 

171 
CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'', 

172 
CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR '''', CHR ''}'', CHR ''~'', 

173 
Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1, 

174 
Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4, 

175 
Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7, 

176 
Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA, 

177 
Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD, 

178 
Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0, 

179 
Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3, 

180 
Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6, 

181 
Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9, 

182 
Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC, 

183 
Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF, 

184 
Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2, 

185 
Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5, 

186 
Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8, 

187 
Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB, 

188 
Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE, 

189 
Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1, 

190 
Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4, 

191 
Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7, 

192 
Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA, 

193 
Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD, 

194 
Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0, 

195 
Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3, 

196 
Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6, 

197 
Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9, 

198 
Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC, 

199 
Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF, 

200 
Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2, 

201 
Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5, 

202 
Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8, 

203 
Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB, 

204 
Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE, 

205 
Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1, 

206 
Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4, 

207 
Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7, 

208 
Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA, 

209 
Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD, 

210 
Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0, 

211 
Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3, 

212 
Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6, 

213 
Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9, 

214 
Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC, 

215 
Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]" 

216 

49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

217 
definition 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

218 
"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

219 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

220 
definition 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

221 
"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

222 

51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

223 
lemma enum_char_product_enum_nibble: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

224 
"(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

225 
by (simp add: enum_char_def enum_nibble_def) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

226 

49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

227 
instance proof 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

228 
show UNIV: "UNIV = set (Enum.enum :: char list)" 
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

229 
by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV) 
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

230 
show "distinct (Enum.enum :: char list)" 
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

231 
by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct) 
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

232 
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

233 
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

234 
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

235 
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

236 
qed 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

237 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

238 
end 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

239 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

240 
lemma card_UNIV_char: 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

241 
"card (UNIV :: char set) = 256" 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

242 
by (simp add: card_UNIV_length_enum enum_char_def) 
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

243 

51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

244 
definition nat_of_char :: "char \<Rightarrow> nat" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

245 
where 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

246 
"nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

247 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

248 
lemma nat_of_char_Char: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

249 
"nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

250 
by (simp add: nat_of_char_def) 
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

251 

f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

252 
setup {* 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

253 
let 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

254 
val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51160
diff
changeset

255 
val simpset = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51160
diff
changeset

256 
put_simpset HOL_ss @{context} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51160
diff
changeset

257 
addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one}; 
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

258 
fun mk_code_eqn x y = 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

259 
Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char} 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

260 
> simplify simpset; 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

261 
val code_eqns = map_product mk_code_eqn nibbles nibbles; 
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

262 
in 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

263 
Global_Theory.note_thmss "" 
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

264 
[((@{binding nat_of_char_simps}, []), [(code_eqns, [])])] 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

265 
#> snd 
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

266 
end 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

267 
*} 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

268 

51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

269 
declare nat_of_char_simps [code] 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

270 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

271 
lemma nibble_of_nat_of_char_div_16: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

272 
"nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

273 
by (cases c) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

274 
(simp add: nat_of_char_def add_commute nat_of_nibble_less_16) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

275 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

276 
lemma nibble_of_nat_nat_of_char: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

277 
"nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

278 
proof (cases c) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

279 
case (Char x y) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

280 
then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

281 
by (simp add: nibble_of_nat_mod_16) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

282 
then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

283 
by (simp only: nibble_of_nat_mod_16) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

284 
with Char show ?thesis by (simp add: nat_of_char_def add_commute) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

285 
qed 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

286 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

287 
code_datatype Char  {* drop case certificate for char *} 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

288 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

289 
lemma char_case_code [code]: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

290 
"char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

291 
by (cases c) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

292 
(simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

293 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

294 
lemma [code]: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

295 
"char_rec = char_case" 
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

296 
by (simp add: fun_eq_iff split: char.split) 
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset

297 

51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

298 
definition char_of_nat :: "nat \<Rightarrow> char" where 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

299 
"char_of_nat n = Enum.enum ! (n mod 256)" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

300 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

301 
lemma char_of_nat_Char_nibbles: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

302 
"char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

303 
proof  
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

304 
from mod_mult2_eq [of n 16 16] 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

305 
have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

306 
then show ?thesis 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

307 
by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

308 
card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

309 
qed 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

310 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

311 
lemma char_of_nat_of_char [simp]: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

312 
"char_of_nat (nat_of_char c) = c" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

313 
by (cases c) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

314 
(simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

315 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

316 
lemma nat_of_char_of_nat [simp]: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

317 
"nat_of_char (char_of_nat n) = n mod 256" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

318 
proof  
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

319 
have "n mod 256 = n mod (16 * 16)" by simp 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

320 
then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

321 
then show ?thesis 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

322 
by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

323 
qed 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

324 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

325 
lemma inj_nat_of_char: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

326 
"inj nat_of_char" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

327 
by (rule inj_on_inverseI) (rule char_of_nat_of_char) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

328 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

329 
lemma nat_of_char_eq_iff: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

330 
"nat_of_char c = nat_of_char d \<longleftrightarrow> c = d" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

331 
by (rule inj_eq) (rule inj_nat_of_char) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

332 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

333 
lemma nat_of_char_less_256: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

334 
"nat_of_char c < 256" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

335 
proof (cases c) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

336 
case (Char x y) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

337 
with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y] 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

338 
show ?thesis by (simp add: nat_of_char_def) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

339 
qed 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

340 

599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

341 
lemma char_of_nat_mod_256: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

342 
"char_of_nat (n mod 256) = char_of_nat n" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

343 
proof  
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

344 
from nibble_of_nat_mod_16 [of "n mod 256"] 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

345 
have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

346 
with nibble_of_nat_mod_16 [of n] 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

347 
have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

348 
have "n mod 256 = n mod (16 * 16)" by simp 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

349 
then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

350 
show ?thesis 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

351 
by (simp add: char_of_nat_Char_nibbles *) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

352 
(simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **) 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

353 
qed 
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

354 

31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

355 

39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

356 
subsection {* Strings as dedicated type *} 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

357 

49834  358 
typedef literal = "UNIV :: string set" 
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

359 
morphisms explode STR .. 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

360 

548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

361 
instantiation literal :: size 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

362 
begin 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

363 

39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

364 
definition size_literal :: "literal \<Rightarrow> nat" 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

365 
where 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

366 
[code]: "size_literal (s\<Colon>literal) = 0" 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

367 

39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

368 
instance .. 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

369 

548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

370 
end 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

371 

548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

372 
instantiation literal :: equal 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

373 
begin 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

374 

39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

375 
definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

376 
where 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

377 
"equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2" 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

378 

39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

379 
instance 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

380 
proof 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

381 
qed (auto simp add: equal_literal_def explode_inject) 
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

382 

548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

383 
end 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

384 

52365
95186e6e4bf4
reflexive nbe equation for equality on String.literal
haftmann
parents:
51717
diff
changeset

385 
lemma [code nbe]: 
95186e6e4bf4
reflexive nbe equation for equality on String.literal
haftmann
parents:
51717
diff
changeset

386 
fixes s :: "String.literal" 
95186e6e4bf4
reflexive nbe equation for equality on String.literal
haftmann
parents:
51717
diff
changeset

387 
shows "HOL.equal s s \<longleftrightarrow> True" 
95186e6e4bf4
reflexive nbe equation for equality on String.literal
haftmann
parents:
51717
diff
changeset

388 
by (simp add: equal) 
95186e6e4bf4
reflexive nbe equation for equality on String.literal
haftmann
parents:
51717
diff
changeset

389 

51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

390 
lemma STR_inject' [simp]: 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

391 
"STR xs = STR ys \<longleftrightarrow> xs = ys" 
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49972
diff
changeset

392 
by (simp add: STR_inject) 
39274
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
39272
diff
changeset

393 

b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
39272
diff
changeset

394 

31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

395 
subsection {* Code generator *} 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

396 

48891  397 
ML_file "Tools/string_code.ML" 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

398 

33237  399 
code_reserved SML string 
400 
code_reserved OCaml string 

34886  401 
code_reserved Scala string 
33237  402 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

403 
code_printing 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

404 
type_constructor literal \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

405 
(SML) "string" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

406 
and (OCaml) "string" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

407 
and (Haskell) "String" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

408 
and (Scala) "String" 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

409 

4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

410 
setup {* 
34886  411 
fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"] 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

412 
*} 
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

413 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

414 
code_printing 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

415 
class_instance literal :: equal \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

416 
(Haskell)  
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

417 
 constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

418 
(SML) "!((_ : string) = _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

419 
and (OCaml) "!((_ : string) = _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

420 
and (Haskell) infix 4 "==" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52365
diff
changeset

421 
and (Scala) infixl 5 "==" 
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset

422 

52910
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

423 
setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *} 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

424 

7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

425 
definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

426 
where [simp, code del]: "abort _ f = f ()" 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

427 

54317
da932f511746
add congruence rule to prevent code_simp from looping
Andreas Lochbihler
parents:
52910
diff
changeset

428 
lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f" 
da932f511746
add congruence rule to prevent code_simp from looping
Andreas Lochbihler
parents:
52910
diff
changeset

429 
by simp 
da932f511746
add congruence rule to prevent code_simp from looping
Andreas Lochbihler
parents:
52910
diff
changeset

430 

52910
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

431 
setup {* Sign.map_naming Name_Space.parent_path *} 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

432 

54317
da932f511746
add congruence rule to prevent code_simp from looping
Andreas Lochbihler
parents:
52910
diff
changeset

433 
setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *} 
da932f511746
add congruence rule to prevent code_simp from looping
Andreas Lochbihler
parents:
52910
diff
changeset

434 

52910
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

435 
code_printing constant Code.abort \<rightharpoonup> 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

436 
(SML) "!(raise/ Fail/ _)" 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

437 
and (OCaml) "failwith" 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

438 
and (Haskell) "error" 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

439 
and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }" 
7bfe0df532a9
abort execution of generated code with explicit exception message
Andreas Lochbihler
parents:
52435
diff
changeset

440 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35123
diff
changeset

441 
hide_type (open) literal 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31176
diff
changeset

442 

39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

443 
end 
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset

444 