val aut_simps = [cockpit_def,cockpit_asig_def,cockpit_trans_def,
cockpit_initial_def,cockpit_hide_def,
Al_before_Ack_def,Al_before_Ack_asig_def,
Al_before_Ack_initial_def,Al_before_Ack_trans_def,
Info_while_Al_def,Info_while_Al_asig_def,
Info_while_Al_initial_def,Info_while_Al_trans_def,
Info_before_Al_def,Info_before_Al_asig_def,
Info_before_Al_initial_def,Info_before_Al_trans_def];
(* to prove, that info is always set at the recent alarm *)
Goal "cockpit =<| Info_while_Al";
by (is_sim_tac aut_simps 1);
qed"cockpit_implements_Info_while_Al";
(* to prove that before any alarm arrives (and after each acknowledgment),
info remains at None *)
Goal "cockpit =<| Info_before_Al";
by (is_sim_tac aut_simps 1);
qed"cockpit_implements_Info_before_Al";
(* to prove that before any alarm would be acknowledged, it must be arrived *)
Goal "cockpit_hide =<| Al_before_Ack";
by (is_sim_tac aut_simps 1);
by Auto_tac;
qed"cockpit_implements_Al_before_Ack";