-
Notifications
You must be signed in to change notification settings - Fork 1
/
read_hex.thy
54 lines (47 loc) · 1.37 KB
/
read_hex.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
theory read_hex
imports "HOL-SPARK.SPARK"
begin
spark_open "b2stest/parse_file/read_hex"
spark_vc procedure_read_hex_6
proof -
from `source_first <= source_index` sdiv_pos_pos
have "(source_index - source_first) sdiv 2 =
(source_index - source_first) div 2"
by simp
moreover
from `source_first <= source_index` sdiv_pos_pos
have "(source_index + 2 - source_first) sdiv 2 =
(source_index + 2 - source_first) div 2"
by simp
ultimately show ?thesis by (simp add: div_pos_geq)
qed
spark_vc procedure_read_hex_13
proof -
from `source_index >= source_first`
`source_index < source_last`
`target__index__subtype__1__last >=
(source_last - source_first + 1) sdiv 2`
sdiv_pos_pos
have "(source_index - source_first) sdiv 2 <
target__index__subtype__1__last"
by simp
then show ?thesis by simp
qed
spark_vc procedure_read_hex_17
proof -
from `source_index >= source_first`
`source_index < source_last`
`target__index__subtype__1__last >=
(source_last - source_first + 1) sdiv 2`
show ?thesis by (simp add: sdiv_pos_pos)
qed
spark_vc procedure_read_hex_18
proof -
from `source_index >= source_first`
`source_index < source_last`
`target__index__subtype__1__last >=
(source_last - source_first + 1) sdiv 2`
show ?thesis by (simp add: sdiv_pos_pos)
qed
spark_end
end