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