This line should be [VC_UNPACK_TAC; VC_UNPACK_TAC; GEN_TAC];(same as 728)
When matching a pattern which already contains MEASURE, GEN_TAC should be used instead.
Example:
`correct
T
var m,n;
do [invariant 0<=m ; measure m]
(if 0<n then n:=0;
m:= PRE m)
while 0<m
end
n=0`;;
With e VC_TAC, it outputs:
`m' = m /\ n' = n /\ ~(0 < n)
==> 0 <= PRE m /\ MEASURE (\(m,n). m) (PRE m,n) (m',n')`
`m' = m /\ n' = n /\ 0 < n
==> 0 <= PRE m /\ MEASURE (\(m,n). m) (PRE m,0) (m',n')`
`~(0 < m) /\ 0 <= m ==> n = 0`
`WF (MEASURE (\(m,n). m))`
This is because the match to correct p (ADO i (MEASURE m) c e) q failed, correct p (ADO i v c e) q was used instead,
With e (MATCH_MP_TAC VC_ADO_MEASURE THEN REPEAT CONJ_TAC THENL [VC_UNPACK_TAC; VC_UNPACK_TAC; GEN_TAC]), the output is:
`correct ((\(m,n). T) AND (\s. X = (\(m,n). m) s))
(IF (\(m,n). 0 < n) (Assign (\(m,n). m,0)) Seq Assign (\(m,n). PRE m,n))
((\(m,n). 0 <= m) AND (\s. (\(m,n). m) s < X))`
`~(0 < m) /\ 0 <= m ==> n = 0`
Where no MEASURE is found, and continue with VC_TAC, all VC goals will be generated normally
https://github.com/jrh13/hol-light/blob/7381e2e76a090a2e9fb311d0f7ae7a8c132f9fce/Examples/prog.ml#L734
This line should be [VC_UNPACK_TAC; VC_UNPACK_TAC; GEN_TAC];(same as 728)
When matching a pattern which already contains MEASURE, GEN_TAC should be used instead.
Example:
With e VC_TAC, it outputs:
This is because the match to
correct p (ADO i (MEASURE m) c e) qfailed,correct p (ADO i v c e) qwas used instead,With e (MATCH_MP_TAC VC_ADO_MEASURE THEN REPEAT CONJ_TAC THENL [VC_UNPACK_TAC; VC_UNPACK_TAC; GEN_TAC]), the output is:
Where no MEASURE is found, and continue with VC_TAC, all VC goals will be generated normally