src/HOL/IOA/NTP/Abschannel.ML
author paulson
Mon, 07 Oct 1996 10:28:44 +0200
changeset 2056 93c093620c28
parent 1328 9a449a91425d
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/IOA/NTP/Abschannel.ML
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     2
    ID:         $Id$
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow and Olaf Mueller
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     4
    Copyright   1994  TU Muenchen
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     5
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     6
Derived rules
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     7
*)
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     8
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     9
open Abschannel;
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    10
1328
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    11
val unfold_renaming = 
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    12
 [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, 
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    13
   ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def, 
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    14
   actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, 
1328
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    15
   trans_of_def] @ asig_projections;
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    16
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    17
goal Abschannel.thy
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    18
     "S_msg(m) ~: actions(srch_asig)        &    \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    19
     \ R_msg(m) ~: actions(srch_asig)        &    \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    20
     \ S_pkt(pkt) : actions(srch_asig)    &    \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    21
     \ R_pkt(pkt) : actions(srch_asig)    &    \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    22
     \ S_ack(b) ~: actions(srch_asig)     &    \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    23
     \ R_ack(b) ~: actions(srch_asig)     &    \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    24
     \ C_m_s ~: actions(srch_asig)           &    \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    25
     \ C_m_r ~: actions(srch_asig)           &    \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    26
     \ C_r_s ~: actions(srch_asig)  & C_r_r(m) ~: actions(srch_asig)";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    27
1328
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    28
by(simp_tac (!simpset addsimps unfold_renaming) 1);
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    29
qed"in_srch_asig";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    30
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    31
goal Abschannel.thy
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    32
      "S_msg(m) ~: actions(rsch_asig)         & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    33
     \ R_msg(m) ~: actions(rsch_asig)         & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    34
     \ S_pkt(pkt) ~: actions(rsch_asig)    & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    35
     \ R_pkt(pkt) ~: actions(rsch_asig)    & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    36
     \ S_ack(b) : actions(rsch_asig)       & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    37
     \ R_ack(b) : actions(rsch_asig)       & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    38
     \ C_m_s ~: actions(rsch_asig)            & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    39
     \ C_m_r ~: actions(rsch_asig)            & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    40
     \ C_r_s ~: actions(rsch_asig)            & \
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    41
     \ C_r_r(m) ~: actions(rsch_asig)";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    42
1328
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    43
by(simp_tac (!simpset addsimps unfold_renaming) 1);
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    44
qed"in_rsch_asig";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    45
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    46
goal Abschannel.thy "srch_ioa = (srch_asig, {{|}}, srch_trans)";
1328
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    47
by(simp_tac (!simpset addsimps unfold_renaming) 1);
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    48
qed"srch_ioa_thm";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    49
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    50
goal Abschannel.thy "rsch_ioa = (rsch_asig, {{|}}, rsch_trans)";
1328
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    51
by(simp_tac (!simpset addsimps unfold_renaming) 1);
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    52
qed"rsch_ioa_thm";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    53