-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathWord8Auxiliary.thy
185 lines (142 loc) · 5.69 KB
/
Word8Auxiliary.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
chapter {* Generated by Lem from word8.lem. *}
theory "Word8Auxiliary"
imports
Main "~~/src/HOL/Library/Code_Target_Numeral"
"Lem_pervasives"
"Lem_word"
"Word8"
begin
(****************************************************)
(* *)
(* Lemmata *)
(* *)
(****************************************************)
lemma bs_to_w8_def_lemma:
" ((\<forall> seq.
W8 (integerFromBitSeq seq) =
(\<lambda> w . word_of_int (integerFromBitSeq w)) seq)) "
(* Theorem: bs_to_w8_def_lemma*)(* try *) by auto
lemma w8_to_bs_def_lemma:
" ((\<forall> i.
bitSeqFromInteger (Some (( 8 :: nat))) i =
(\<lambda> w . bitSeqFromInteger (Some 8) ( (sint w))) (W8 i))) "
(* Theorem: w8_to_bs_def_lemma*)(* try *) by auto
lemma word8ToNat_def_lemma:
" ((\<forall> w.
nat
(abs
(
(integerFromBitSeq
((\<lambda> w . bitSeqFromInteger (Some 8) ( (sint w))) w))))
= unat w)) "
(* Theorem: word8ToNat_def_lemma*)(* try *) by auto
lemma word8ToInt_def_lemma:
" ((\<forall> w.
(integerFromBitSeq
((\<lambda> w . bitSeqFromInteger (Some 8) ( (sint w))) w)) =
sint w)) "
(* Theorem: word8ToInt_def_lemma*)(* try *) by auto
lemma word8FromInteger_def_lemma:
" ((\<forall> i. W8 (i mod base) = (\<lambda> i . word_of_int ( i)) i)) "
(* Theorem: word8FromInteger_def_lemma*)(* try *) by auto
lemma word8FromInt_def_lemma:
" ((\<forall> i. W8 ( i mod base) = word_of_int i)) "
(* Theorem: word8FromInt_def_lemma*)(* try *) by auto
lemma word8FromBoollist_def_lemma:
" ((\<forall> lst.
(case bitSeqFromBoolList lst of
None => (\<lambda> w . word_of_int (integerFromBitSeq w))
(bitSeqFromInteger None (( 0 :: int)))
| Some a => (\<lambda> w . word_of_int (integerFromBitSeq w)) a
) = of_bl lst)) "
(* Theorem: word8FromBoollist_def_lemma*)(* try *) by auto
lemma boolListFromWord8_def_lemma:
" ((\<forall> w.
boolListFrombitSeq (( 8 :: nat))
((\<lambda> w . bitSeqFromInteger (Some 8) ( (sint w))) w) = to_bl w)) "
(* Theorem: boolListFromWord8_def_lemma*)(* try *) by auto
lemma word8FromNumeral_def_lemma:
" ((\<forall> w. W8 (( w :: int) mod base) = ((word_of_int w) :: 8 word))) "
(* Theorem: word8FromNumeral_def_lemma*)(* try *) by auto
lemma w8Less_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word8BinTest (op<) bs1 bs2 = word_sless bs1 bs2)) "
(* Theorem: w8Less_def_lemma*)(* try *) by auto
lemma w8LessEqual_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word8BinTest (op \<le>) bs1 bs2 = word_sle bs1 bs2)) "
(* Theorem: w8LessEqual_def_lemma*)(* try *) by auto
lemma w8Greater_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word8BinTest (op>) bs1 bs2 = word_sless bs2 bs1)) "
(* Theorem: w8Greater_def_lemma*)(* try *) by auto
lemma w8GreaterEqual_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word8BinTest (op \<ge>) bs1 bs2 = word_sle bs2 bs1)) "
(* Theorem: w8GreaterEqual_def_lemma*)(* try *) by auto
lemma w8Compare_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word8BinTest (genericCompare (op<) (op=)) bs1 bs2 =
(genericCompare word_sless w8Eq bs1 bs2))) "
(* Theorem: w8Compare_def_lemma*)(* try *) by auto
lemma word8Negate_def_lemma:
" (( word8UnaryOp (\<lambda> i. - i) = (\<lambda> i. - i))) "
(* Theorem: word8Negate_def_lemma*)(* try *) by auto
lemma word8Succ_def_lemma:
" (( word8UnaryOp (\<lambda> n. n + ( 1 :: int)) = (\<lambda> n. n + 1))) "
(* Theorem: word8Succ_def_lemma*)(* try *) by auto
lemma word8Pred_def_lemma:
" (( word8UnaryOp (\<lambda> n. n - ( 1 :: int)) = (\<lambda> n. n - 1))) "
(* Theorem: word8Pred_def_lemma*)(* try *) by auto
lemma word8Lnot_def_lemma:
" (( word8UnaryOp integerLnot = (\<lambda> w. (NOT w)))) "
(* Theorem: word8Lnot_def_lemma*)(* try *) by auto
lemma word8Add_def_lemma:
" (( word8BinOp (op+) = (op+))) "
(* Theorem: word8Add_def_lemma*)(* try *) by auto
lemma word8Minus_def_lemma:
" (( word8BinOp (op-) = (op-))) "
(* Theorem: word8Minus_def_lemma*)(* try *) by auto
lemma word8Mult_def_lemma:
" (( word8BinOp (op*) = (op*))) "
(* Theorem: word8Mult_def_lemma*)(* try *) by auto
lemma word8IntegerDivision_def_lemma:
" (( word8BinOp (op div) = (op div))) "
(* Theorem: word8IntegerDivision_def_lemma*)(* try *) by auto
lemma word8Division_def_lemma:
" (( word8BinOp (op div) = (op div))) "
(* Theorem: word8Division_def_lemma*)(* try *) by auto
lemma word8Remainder_def_lemma:
" (( word8BinOp (op mod) = (op mod))) "
(* Theorem: word8Remainder_def_lemma*)(* try *) by auto
lemma word8Land_def_lemma:
" (( word8BinOp integerLand = (op AND))) "
(* Theorem: word8Land_def_lemma*)(* try *) by auto
lemma word8Lor_def_lemma:
" (( word8BinOp integerLor = (op OR))) "
(* Theorem: word8Lor_def_lemma*)(* try *) by auto
lemma word8Lxor_def_lemma:
" (( word8BinOp integerLxor = (op XOR))) "
(* Theorem: word8Lxor_def_lemma*)(* try *) by auto
lemma word8Min_def_lemma:
" (( word8BinOp (min) = min)) "
(* Theorem: word8Min_def_lemma*)(* try *) by auto
lemma word8Max_def_lemma:
" (( word8BinOp (max) = max)) "
(* Theorem: word8Max_def_lemma*)(* try *) by auto
lemma word8Power_def_lemma:
" (( word8NatOp (op^) = (op^))) "
(* Theorem: word8Power_def_lemma*)(* try *) by auto
lemma word8Asr_def_lemma:
" (( word8NatOp integerAsr = (op>>>))) "
(* Theorem: word8Asr_def_lemma*)(* try *) by auto
lemma word8Lsr_def_lemma:
" (( word8NatOp integerAsr = (op>>))) "
(* Theorem: word8Lsr_def_lemma*)(* try *) by auto
lemma word8Lsl_def_lemma:
" (( word8NatOp integerLsl = (op<<))) "
(* Theorem: word8Lsl_def_lemma*)(* try *) by auto
lemma word8UGT_def_lemma:
" ((\<forall> a. \<forall> b. (unat a > unat b) = a > b)) "
(* Theorem: word8UGT_def_lemma*)(* try *) by auto
end