src/HOLCF/IOA/ex/TrivEx2.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12218 6597093b77e7
child 17244 0b2ff9541727
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:      HOLCF/IOA/TrivEx.thy
     2     ID:         $Id$
     3     Author:     Olaf Müller
     4 
     5 Trivial Abstraction Example with fairness.
     6 *)
     7 
     8 TrivEx2 = Abstraction + IOA +
     9 
    10 datatype action = INC
    11 
    12 consts
    13 
    14 C_asig   ::  "action signature"
    15 C_trans  :: (action, nat)transition set
    16 C_ioa    :: (action, nat)ioa
    17 C_live_ioa :: (action, nat)live_ioa
    18 
    19 A_asig   :: "action signature"
    20 A_trans  :: (action, bool)transition set
    21 A_ioa    :: (action, bool)ioa
    22 A_live_ioa :: (action, bool)live_ioa
    23 
    24 h_abs    :: "nat => bool"
    25 
    26 defs
    27 
    28 C_asig_def
    29   "C_asig == ({},{INC},{})"
    30 
    31 C_trans_def "C_trans ==                                           
    32  {tr. let s = fst(tr);                                               
    33           t = snd(snd(tr))                                           
    34       in case fst(snd(tr))                                           
    35       of                                                             
    36       INC       => t = Suc(s)}"
    37 
    38 C_ioa_def "C_ioa == 
    39  (C_asig, {0}, C_trans,{},{})"
    40 
    41 C_live_ioa_def 
    42   "C_live_ioa == (C_ioa, WF C_ioa {INC})"
    43 
    44 A_asig_def
    45   "A_asig == ({},{INC},{})"
    46 
    47 A_trans_def "A_trans ==                                           
    48  {tr. let s = fst(tr);                                               
    49           t = snd(snd(tr))                                           
    50       in case fst(snd(tr))                                           
    51       of                                                             
    52       INC       => t = True}"
    53 
    54 A_ioa_def "A_ioa == 
    55  (A_asig, {False}, A_trans,{},{})"
    56 
    57 A_live_ioa_def 
    58   "A_live_ioa == (A_ioa, WF A_ioa {INC})"
    59 
    60 
    61 
    62 h_abs_def
    63   "h_abs n == n~=0"
    64 
    65 rules
    66 
    67 MC_result
    68   "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
    69 
    70 end