src/HOLCF/IOA/meta_theory/TL.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 5976 44290b71a85f
child 12028 52aa183c15bb
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1997  TU Muenchen
     5 
     6 A General Temporal Logic
     7 
     8 *)   
     9 
    10 
    11 		       
    12 TL = Pred + Sequence +  
    13 
    14 default term
    15 
    16 types
    17 
    18 'a temporal      = 'a Seq predicate
    19 
    20  
    21 consts
    22 
    23 
    24 suffix     :: "'a Seq => 'a Seq => bool"
    25 tsuffix    :: "'a Seq => 'a Seq => bool"
    26 
    27 validT     :: "'a Seq predicate => bool"
    28 
    29 unlift     ::  "'a lift => 'a"
    30 
    31 Init         ::"'a predicate => 'a temporal"          ("<_>" [0] 1000)
    32 
    33 Box          ::"'a temporal => 'a temporal"   ("[] (_)" [80] 80)
    34 Diamond      ::"'a temporal => 'a temporal"   ("<> (_)" [80] 80)
    35 Next         ::"'a temporal => 'a temporal"   
    36 Leadsto      ::"'a temporal => 'a temporal => 'a temporal"  (infixr "~>" 22)
    37 
    38 syntax (symbols)
    39    "Box"        ::"'a temporal => 'a temporal"   ("\\<box> (_)" [80] 80)
    40    "Diamond"    ::"'a temporal => 'a temporal"   ("\\<diamond> (_)" [80] 80)
    41    "Leadsto"    ::"'a temporal => 'a temporal => 'a temporal"  (infixr "\\<leadsto>" 22)
    42  
    43 defs
    44 
    45 
    46 unlift_def
    47   "unlift x == (case x of 
    48                  Undef   => arbitrary
    49                | Def y   => y)"
    50 
    51 (* this means that for nil and UU the effect is unpredictable *)
    52 Init_def
    53   "Init P s ==  (P (unlift (HD$s)))" 
    54 
    55 suffix_def
    56   "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)" 
    57 
    58 tsuffix_def
    59   "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
    60 
    61 Box_def
    62   "([] P) s == ! s2. tsuffix s2 s --> P s2"
    63 
    64 Next_def
    65   "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
    66 
    67 Diamond_def
    68   "<> P == .~ ([] (.~ P))"
    69 
    70 Leadsto_def
    71    "P ~> Q == ([] (P .--> (<> Q)))"  
    72 
    73 validT_def
    74   "validT P == ! s. s~=UU & s~=nil --> (s |= P)"
    75 
    76 end