src/HOLCF/IOA/ex/TrivEx2.thy
author mueller
Thu, 22 Apr 1999 11:06:35 +0200
changeset 6470 f3015fd68d66
child 12218 6597093b77e7
permissions -rw-r--r--
moved this trivial example to new ex dir;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/TrivEx.thy
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     2
    ID:         $Id$
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     3
    Author:     Olaf Mueller
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     4
    Copyright   1995  TU Muenchen
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     5
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     6
Trivial Abstraction Example with fairness
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     7
*)
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     8
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     9
TrivEx2 = Abstraction + IOA +
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    10
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    11
datatype action = INC
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    12
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    13
consts
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    14
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    15
C_asig   ::  "action signature"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    16
C_trans  :: (action, nat)transition set
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    17
C_ioa    :: (action, nat)ioa
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    18
C_live_ioa :: (action, nat)live_ioa
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    19
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    20
A_asig   :: "action signature"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    21
A_trans  :: (action, bool)transition set
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    22
A_ioa    :: (action, bool)ioa
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    23
A_live_ioa :: (action, bool)live_ioa
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    24
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    25
h_abs    :: "nat => bool"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    26
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    27
defs
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    28
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    29
C_asig_def
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    30
  "C_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    31
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    32
C_trans_def "C_trans ==                                           
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    33
 {tr. let s = fst(tr);                                               
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    34
          t = snd(snd(tr))                                           
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    35
      in case fst(snd(tr))                                           
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    36
      of                                                             
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    37
      INC       => t = Suc(s)}"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    38
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    39
C_ioa_def "C_ioa == 
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    40
 (C_asig, {0}, C_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    41
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    42
C_live_ioa_def 
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    43
  "C_live_ioa == (C_ioa, WF C_ioa {INC})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    44
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    45
A_asig_def
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    46
  "A_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    47
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    48
A_trans_def "A_trans ==                                           
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    49
 {tr. let s = fst(tr);                                               
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    50
          t = snd(snd(tr))                                           
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    51
      in case fst(snd(tr))                                           
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    52
      of                                                             
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    53
      INC       => t = True}"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    54
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    55
A_ioa_def "A_ioa == 
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    56
 (A_asig, {False}, A_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    57
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    58
A_live_ioa_def 
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    59
  "A_live_ioa == (A_ioa, WF A_ioa {INC})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    60
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    61
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    62
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    63
h_abs_def
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    64
  "h_abs n == n~=0"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    65
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    66
rules
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    67
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    68
MC_result
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    69
  "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    70
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    71
end