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