IOA/example/Channels.ML

Added headers and made various small mods.

(*  Title:      HOL/IOA/example/Channels.ML
    ID:         $Id$
    Author:     Tobias Nipkow & Konrad Slind
    Copyright   1994  TU Muenchen

Derived rules
*)

local
val SS = action_ss addsimps 
                (Channels.srch_asig_def :: 
                 Channels.rsch_asig_def :: 
                 actions_def :: asig_projections @ set_lemmas)
in

val in_srch_asig = prove_goal Channels.thy
     "S_msg(m) ~: actions(srch_asig)        &    \
     \ R_msg(m) ~: actions(srch_asig)        &    \
     \ S_pkt(pkt) : actions(srch_asig)    &    \
     \ R_pkt(pkt) : actions(srch_asig)    &    \
     \ S_ack(b) ~: actions(srch_asig)     &    \
     \ R_ack(b) ~: actions(srch_asig)     &    \
     \ C_m_s ~: actions(srch_asig)           &    \
     \ C_m_r ~: actions(srch_asig)           &    \
     \ C_r_s ~: actions(srch_asig)           &    \
     \ C_r_r(m) ~: actions(srch_asig)"
  (fn _ => [simp_tac SS 1]);

val in_rsch_asig = prove_goal Channels.thy
      "S_msg(m) ~: actions(rsch_asig)         & \
     \ R_msg(m) ~: actions(rsch_asig)         & \
     \ S_pkt(pkt) ~: actions(rsch_asig)    & \
     \ R_pkt(pkt) ~: actions(rsch_asig)    & \
     \ S_ack(b) : actions(rsch_asig)       & \
     \ R_ack(b) : actions(rsch_asig)       & \
     \ C_m_s ~: actions(rsch_asig)            & \
     \ C_m_r ~: actions(rsch_asig)            & \
     \ C_r_s ~: actions(rsch_asig)            & \
     \ C_r_r(m) ~: actions(rsch_asig)"
  (fn _ => [simp_tac SS 1]);

end;