(Maybe) a typo in Examples/prog.ml ?

[zidongtuili]

hol-light/Examples/prog.ml

Line 734 in 7381e2e

[VC_UNPACK_TAC; VC_UNPACK_TAC; STATE_GEN_TAC'];

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