src/HOL/IOA/ABP/Env.thy
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1376 92f83b9d17e1
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
     1 (*  Title:      HOL/IOA/example/Impl.thy
     2 by (Action.action.induct_tac "a" 1);
     3     ID:         $Id$
     4     Author:     Tobias Nipkow & Konrad Slind
     5     Copyright   1994  TU Muenchen
     6 
     7 The environment
     8 *)
     9 
    10 Env = IOA + Action +
    11 
    12 types
    13 
    14 'm env_state = "bool"
    15 (*              give next bit to system  *)
    16 
    17 consts
    18 
    19 env_asig   :: 'm action signature
    20 env_trans  :: ('m action, 'm env_state)transition set
    21 env_ioa    :: ('m action, 'm env_state)ioa
    22 next       :: 'm env_state => bool
    23 
    24 defs
    25 
    26 env_asig_def
    27   "env_asig == ({Next},                 
    28                UN m. {S_msg(m)},       
    29                {})"
    30 
    31 env_trans_def "env_trans ==                                           
    32  {tr. let s = fst(tr);                                               
    33           t = snd(snd(tr))                                           
    34       in case fst(snd(tr))                                           
    35       of                                                             
    36       Next       => t=True |                                         
    37       S_msg(m)   => s=True & t=False |                               
    38       R_msg(m)   => False |                                          
    39       S_pkt(pkt) => False |                                          
    40       R_pkt(pkt) => False |                                          
    41       S_ack(b)   => False |                                          
    42       R_ack(b)   => False}"
    43 
    44 env_ioa_def "env_ioa == 
    45  (env_asig, {True}, env_trans)"
    46 
    47 end
    48