|
From: Peter V. H. <ho...@sa...> - 2004-11-12 18:39:49
|
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)
|