[Hol-info] Re: Help for newbie

[Peter V. H. <ho...@sa...>]

I think you want to universally quantify the hypothesis that trains that
are not stopped have their door closed.

I have tried the following using the tactical FIRST_ASSUM:

- val _ = Hol_datatype `state = <| train: bool ; doors: bool |>`;
<<HOL message: Defined type: "state">>

- set_goal([``~((nextstate (st:state) (press_accelerate:'a)).train = stopped)``,
         ``!st:state. ~(st.train = stopped) ==> (st.doors = closed)``],
       ``(nextstate (st:state) (press_accelerate:'a)).doors = closed``);
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         (nextstate st press_accelerate).doors = closed
         ------------------------------------
           0.  !st. ~(st.train = stopped) ==> (st.doors = closed)
           1.  ~((nextstate st press_accelerate).train = stopped)

     : proofs
- e(FIRST_ASSUM MATCH_MP_TAC);
OK..
1 subgoal:
> val it =
    ~((nextstate st press_accelerate).train = stopped)
    ------------------------------------
      0.  !st. ~(st.train = stopped) ==> (st.doors = closed)
      1.  ~((nextstate st press_accelerate).train = stopped)
     : goalstack
- e(FIRST_ASSUM ACCEPT_TAC);
OK..

Goal proved.
 [.] |- ~((nextstate st press_accelerate).train = stopped)
> val it =
    Initial goal proved.
     [..] |- (nextstate st press_accelerate).doors = closed : goalstack

Peter

----------------------------------------------------------------------------
Peter Vincent Homeier         __     The above opinions are mine and not the
ho...@sa...   <;_><   opinions of University of Pennsylvania.
Home Page:   http://www.cis.upenn.edu/~homeier/
"In Your majesty ride prosperously because of truth, humility, and
righteousness; and Your right hand shall teach You awesome things." (Ps 45:4)