-
Notifications
You must be signed in to change notification settings - Fork 85
/
Copy pathcfTacticsScript.sml
158 lines (134 loc) · 4.02 KB
/
cfTacticsScript.sml
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
(*
Lemmas that aid the tactics for reasoning about CF-based goals in HOL.
*)
open preamble
open set_sepTheory helperLib ConseqConv ml_translatorTheory
open cfHeapsBaseTheory cfHeapsTheory cfHeapsBaseLib cfStoreTheory
open cfNormaliseTheory cfAppTheory cfTheory
open cfTacticsBaseLib cfHeapsLib
val _ = new_theory "cfTactics"
(*
Theorem xret_lemma:
!H Q.
(H ==>> Q v * GC) ==>
local (\H' Q'. H' ==>> Q' v) H Q
Proof
rpt strip_tac \\ irule (Q.SPEC `GC` local_gc_pre_on) \\
fs [local_is_local] \\ first_assum hchanges \\ hinst \\
irule local_elim \\ fs [] \\ hsimpl
QED*)
Theorem xret_lemma:
!H Q R.
H ==>> Q v * GC /\ R Q ==>
local (\H' Q'. H' ==>> Q' v /\ R Q') H Q
Proof
rpt strip_tac \\ irule (Q.SPEC `GC` local_gc_pre_on) \\
fs [local_is_local] \\ first_assum hchanges \\ hinst \\
irule local_elim \\ fs [] \\ hsimpl
QED
(* todo: does it even happen? *)
Theorem xret_lemma_unify:
!v H. local (\H' Q'. H' ==>> Q' v) H (\x. cond (x = v) * H)
Proof
rpt strip_tac \\ irule local_elim \\ fs [] \\ hsimpl
QED
(*
Theorem xret_no_gc_lemma:
!v H Q.
(H ==>> Q v) ==>
local (\H' Q'. H' ==>> Q' v) H Q
Proof
fs [local_elim]
QED
*)
Theorem xret_no_gc_lemma:
!v H Q R.
H ==>> Q v /\ R Q ==>
local (\H' Q'. H' ==>> Q' v /\ R Q') H Q
Proof
fs [local_elim]
QED
(*------------------------------------------------------------------*)
(* Automatic rewrites *)
Theorem INT_Litv[simp]:
INT i (Litv (IntLit k)) = (i = k)
Proof
fs [INT_def] \\ eq_tac \\ fs []
QED
Theorem NUM_Litv[simp]:
NUM n (Litv (IntLit k)) = (k = &n)
Proof
fs [NUM_def] \\ eq_tac \\ fs []
QED
Theorem CHAR_Litv[simp]:
CHAR c (Litv (Char c')) = (c = c')
Proof
fs [CHAR_def] \\ eq_tac \\ fs []
QED
Theorem STRING_Litv[simp]:
STRING_TYPE s (Litv (StrLit s')) = (s = strlit s')
Proof
Cases_on`s` \\ fs [STRING_TYPE_def] \\ eq_tac \\ fs []
QED
Theorem WORD8_Litv[simp]:
WORD w (Litv (Word8 w')) = (w = w')
Proof
fs [WORD_def, w2w_def] \\ eq_tac \\ fs []
QED
Theorem WORD64_Litv[simp]:
WORD w (Litv (Word64 w')) = (w = w')
Proof
fs [WORD_def, w2w_def] \\ eq_tac \\ fs []
QED
Theorem UNIT_Conv[simp]:
UNIT_TYPE () (Conv NONE []) = T
Proof
fs [UNIT_TYPE_def]
QED
Theorem BOOL_T_Conv[simp]:
BOOL T (Conv (SOME (TypeStamp "True" bool_type_num)) []) = T
Proof
fs [BOOL_def, semanticPrimitivesTheory.Boolv_def]
QED
Theorem BOOL_F_Conv[simp]:
BOOL F (Conv (SOME (TypeStamp "False" bool_type_num)) []) = T
Proof
fs [BOOL_def, semanticPrimitivesTheory.Boolv_def]
QED
Theorem BOOL_Boolv[simp]:
BOOL b (Boolv bv) = (b = bv)
Proof
fs [BOOL_def, semanticPrimitivesTheory.Boolv_def] \\
every_case_tac \\ fs []
QED
(*------------------------------------------------------------------*)
(* Used for cleaning up after unfolding [build_cases] (in cf_match) *)
Theorem exists_v_of_pat_norest_length:
!envC pat insts v.
(?insts wildcards. v_of_pat_norest envC pat insts wildcards = SOME v) <=>
(?insts wildcards. LENGTH insts = LENGTH (pat_bindings pat []) /\
LENGTH wildcards = pat_wildcards pat /\
v_of_pat_norest envC pat insts wildcards = SOME v)
Proof
rpt strip_tac \\ eq_tac \\ fs [] \\ rpt strip_tac \\ instantiate \\
progress v_of_pat_norest_insts_length \\
progress v_of_pat_norest_wildcards_count \\ fs []
QED
Theorem forall_v_of_pat_norest_length:
!envC pat insts v P.
(!insts wildcards. v_of_pat_norest envC pat insts wildcards = SOME v ==> P insts) <=>
(!insts wildcards. LENGTH insts = LENGTH (pat_bindings pat []) ==>
LENGTH wildcards = pat_wildcards pat ==>
v_of_pat_norest envC pat insts wildcards = SOME v ==>
P insts)
Proof
rpt strip_tac \\ eq_tac \\ fs [] \\ rpt strip_tac \\
progress v_of_pat_norest_insts_length \\
progress v_of_pat_norest_wildcards_count \\
first_assum progress
QED
Theorem BOOL_T =
EVAL ``BOOL T (Conv (SOME (TypeStamp "True" 0)) [])``
Theorem BOOL_F =
EVAL ``BOOL F (Conv (SOME (TypeStamp "False" 0)) [])``
val _ = export_theory()