-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathWord160Auxiliary.thy
186 lines (143 loc) · 5.9 KB
/
Word160Auxiliary.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
186
chapter {* Generated by Lem from word160.lem. *}
theory "Word160Auxiliary"
imports
Main "~~/src/HOL/Library/Code_Target_Numeral"
"Lem_pervasives"
"Lem_word"
"Word160"
begin
(****************************************************)
(* *)
(* Lemmata *)
(* *)
(****************************************************)
lemma bs_to_w160_def_lemma:
" ((\<forall> seq.
W160 (integerFromBitSeq seq) =
(\<lambda> w . word_of_int (integerFromBitSeq w)) seq)) "
(* Theorem: bs_to_w160_def_lemma*)(* try *) by auto
lemma w160_to_bs_def_lemma:
" ((\<forall> i.
bitSeqFromInteger (Some (( 160 :: nat))) i =
(\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) (W160 i))) "
(* Theorem: w160_to_bs_def_lemma*)(* try *) by auto
lemma word160ToNat_def_lemma:
" ((\<forall> w.
nat
(abs
(
(integerFromBitSeq
((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w))))
= unat w)) "
(* Theorem: word160ToNat_def_lemma*)(* try *) by auto
lemma word160ToInt_def_lemma:
" ((\<forall> w.
(integerFromBitSeq
((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w)) =
sint w)) "
(* Theorem: word160ToInt_def_lemma*)(* try *) by auto
lemma word160FromInteger_def_lemma:
" ((\<forall> i. W160 (i mod base) = (\<lambda> i . word_of_int ( i)) i)) "
(* Theorem: word160FromInteger_def_lemma*)(* try *) by auto
lemma word160FromInt_def_lemma:
" ((\<forall> i. W160 ( i mod base) = word_of_int i)) "
(* Theorem: word160FromInt_def_lemma*)(* try *) by auto
lemma word160FromBoollist_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: word160FromBoollist_def_lemma*)(* try *) by auto
lemma boolListFromWord160_def_lemma:
" ((\<forall> w.
boolListFrombitSeq (( 160 :: nat))
((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w) =
to_bl w)) "
(* Theorem: boolListFromWord160_def_lemma*)(* try *) by auto
lemma word160FromNumeral_def_lemma:
" ((\<forall> w. W160 (( w :: int) mod base) = ((word_of_int w) :: 160 word))) "
(* Theorem: word160FromNumeral_def_lemma*)(* try *) by auto
lemma w160Less_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word160BinTest (op<) bs1 bs2 = word_sless bs1 bs2)) "
(* Theorem: w160Less_def_lemma*)(* try *) by auto
lemma w160LessEqual_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word160BinTest (op \<le>) bs1 bs2 = word_sle bs1 bs2)) "
(* Theorem: w160LessEqual_def_lemma*)(* try *) by auto
lemma w160Greater_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word160BinTest (op>) bs1 bs2 = word_sless bs2 bs1)) "
(* Theorem: w160Greater_def_lemma*)(* try *) by auto
lemma w160GreaterEqual_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word160BinTest (op \<ge>) bs1 bs2 = word_sle bs2 bs1)) "
(* Theorem: w160GreaterEqual_def_lemma*)(* try *) by auto
lemma w160Compare_def_lemma:
" ((\<forall> bs1. \<forall> bs2.
word160BinTest (genericCompare (op<) (op=)) bs1 bs2 =
(genericCompare word_sless w160Eq bs1 bs2))) "
(* Theorem: w160Compare_def_lemma*)(* try *) by auto
lemma word160Negate_def_lemma:
" (( word160UnaryOp (\<lambda> i. - i) = (\<lambda> i. - i))) "
(* Theorem: word160Negate_def_lemma*)(* try *) by auto
lemma word160Succ_def_lemma:
" (( word160UnaryOp (\<lambda> n. n + ( 1 :: int)) = (\<lambda> n. n + 1))) "
(* Theorem: word160Succ_def_lemma*)(* try *) by auto
lemma word160Pred_def_lemma:
" (( word160UnaryOp (\<lambda> n. n - ( 1 :: int)) = (\<lambda> n. n - 1))) "
(* Theorem: word160Pred_def_lemma*)(* try *) by auto
lemma word160Lnot_def_lemma:
" (( word160UnaryOp integerLnot = (\<lambda> w. (NOT w)))) "
(* Theorem: word160Lnot_def_lemma*)(* try *) by auto
lemma word160Add_def_lemma:
" (( word160BinOp (op+) = (op+))) "
(* Theorem: word160Add_def_lemma*)(* try *) by auto
lemma word160Minus_def_lemma:
" (( word160BinOp (op-) = (op-))) "
(* Theorem: word160Minus_def_lemma*)(* try *) by auto
lemma word160Mult_def_lemma:
" (( word160BinOp (op*) = (op*))) "
(* Theorem: word160Mult_def_lemma*)(* try *) by auto
lemma word160IntegerDivision_def_lemma:
" (( word160BinOp (op div) = (op div))) "
(* Theorem: word160IntegerDivision_def_lemma*)(* try *) by auto
lemma word160Division_def_lemma:
" (( word160BinOp (op div) = (op div))) "
(* Theorem: word160Division_def_lemma*)(* try *) by auto
lemma word160Remainder_def_lemma:
" (( word160BinOp (op mod) = (op mod))) "
(* Theorem: word160Remainder_def_lemma*)(* try *) by auto
lemma word160Land_def_lemma:
" (( word160BinOp integerLand = (op AND))) "
(* Theorem: word160Land_def_lemma*)(* try *) by auto
lemma word160Lor_def_lemma:
" (( word160BinOp integerLor = (op OR))) "
(* Theorem: word160Lor_def_lemma*)(* try *) by auto
lemma word160Lxor_def_lemma:
" (( word160BinOp integerLxor = (op XOR))) "
(* Theorem: word160Lxor_def_lemma*)(* try *) by auto
lemma word160Min_def_lemma:
" (( word160BinOp (min) = min)) "
(* Theorem: word160Min_def_lemma*)(* try *) by auto
lemma word160Max_def_lemma:
" (( word160BinOp (max) = max)) "
(* Theorem: word160Max_def_lemma*)(* try *) by auto
lemma word160Power_def_lemma:
" (( word160NatOp (op^) = (op^))) "
(* Theorem: word160Power_def_lemma*)(* try *) by auto
lemma word160Asr_def_lemma:
" (( word160NatOp integerAsr = (op>>>))) "
(* Theorem: word160Asr_def_lemma*)(* try *) by auto
lemma word160Lsr_def_lemma:
" (( word160NatOp integerAsr = (op>>))) "
(* Theorem: word160Lsr_def_lemma*)(* try *) by auto
lemma word160Lsl_def_lemma:
" (( word160NatOp integerLsl = (op<<))) "
(* Theorem: word160Lsl_def_lemma*)(* try *) by auto
lemma word160UGT_def_lemma:
" ((\<forall> a. \<forall> b. (unat a > unat b) = a > b)) "
(* Theorem: word160UGT_def_lemma*)(* try *) by auto
end