IOA/example/Spec.thy
author clasohm
Tue, 24 Oct 1995 14:59:17 +0100
changeset 251 f04b33ce250f
parent 249 492493334e0f
permissions -rw-r--r--
added calls of init_html and make_chart
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
168
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
     1
(*  Title:      HOL/IOA/example/Spec.thy
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
     2
    ID:         $Id$
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
     3
    Author:     Tobias Nipkow & Konrad Slind
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
     4
    Copyright   1994  TU Muenchen
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
     5
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
     6
The specification of reliable transmission
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
     7
*)
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
     8
156
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     9
Spec = List + IOA + Action +
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    10
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    11
consts
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    12
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    13
spec_sig   :: "'m action signature"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    14
spec_trans :: "('m action, 'm list)transition set"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    15
spec_ioa   :: "('m action, 'm list)ioa"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    16
168
44ff2275d44f Added headers and made various small mods.
nipkow
parents: 156
diff changeset
    17
defs
156
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    18
249
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    19
sig_def "spec_sig == <UN m.{S_msg(m)}, 
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    20
                     UN m.{R_msg(m)}, 
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    21
                     {}>"
156
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    22
249
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    23
trans_def "spec_trans ==                           
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    24
 {tr. let s = fst(tr);                            
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    25
          t = snd(snd(tr))                        
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    26
      in                                          
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    27
      case fst(snd(tr))                           
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    28
      of                                          
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    29
      S_msg(m) => t = s@[m]  |                    
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    30
      R_msg(m) => s = (m#t)  |                    
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    31
      S_pkt(pkt) => False |                    
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    32
      R_pkt(pkt) => False |                    
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    33
      S_ack(b) => False |                      
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    34
      R_ack(b) => False |                      
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    35
      C_m_s => False |                            
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    36
      C_m_r => False |                            
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    37
      C_r_s => False |                            
492493334e0f removed \...\ inside strings
clasohm
parents: 168
diff changeset
    38
      C_r_r(m) => False}"
156
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    39
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    40
ioa_def "spec_ioa == <spec_sig, {[]}, spec_trans>"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    41
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    42
end