src/HOL/TLA/TLA.thy
author wenzelm
Wed Oct 08 12:15:59 1997 +0200 (1997-10-08)
changeset 3808 8489375c6198
parent 3807 82a99b090d9d
child 6255 db63752140c7
permissions -rw-r--r--
symbols syntax;
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:        TLA/TLA.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: TLA
wenzelm@3807
     7
    Logic Image: HOL
wenzelm@3807
     8
wenzelm@3807
     9
The temporal level of TLA.
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@3807
    12
TLA  =  Action + WF_Rel +
wenzelm@3807
    13
wenzelm@3807
    14
types
wenzelm@3807
    15
    behavior
wenzelm@3807
    16
    temporal = "behavior form"
wenzelm@3807
    17
wenzelm@3807
    18
arities
wenzelm@3807
    19
    behavior :: world
wenzelm@3807
    20
wenzelm@3807
    21
consts
wenzelm@3807
    22
  (* get first 2 states of behavior *)
wenzelm@3807
    23
  fst_st     :: "behavior => state"
wenzelm@3807
    24
  snd_st     :: "behavior => state"
wenzelm@3807
    25
  
wenzelm@3807
    26
  Init       :: "action => temporal"
wenzelm@3807
    27
                 (* define Box and Dmd for both actions and temporals *)
wenzelm@3807
    28
  Box        :: "('w::world) form => temporal"      ("([](_))" [40] 40)
wenzelm@3807
    29
  Dmd        :: "('w::world) form => temporal"      ("(<>(_))" [40] 40)
wenzelm@3807
    30
  "~>"       :: "[action,action] => temporal"       (infixr 22)
wenzelm@3807
    31
  stable     :: "action => temporal"
wenzelm@3807
    32
  WF         :: "[action,'a stfun] => temporal"    ("(WF'(_')'_(_))" [0,60] 55)
wenzelm@3807
    33
  SF         :: "[action,'a stfun] => temporal"    ("(SF'(_')'_(_))" [0,60] 55)
wenzelm@3807
    34
wenzelm@3807
    35
  (* Quantification over (flexible) state variables *)
wenzelm@3807
    36
  EEx        :: "('a stfun => temporal) => temporal"    (binder "EEX " 10)
wenzelm@3807
    37
  AAll       :: "('a stfun => temporal) => temporal"    (binder "AALL " 10)
wenzelm@3807
    38
wenzelm@3807
    39
translations
wenzelm@3807
    40
  "sigma |= Init(A)"      == "Init A sigma"
wenzelm@3807
    41
  "sigma |= Box(F)"       == "Box F sigma"
wenzelm@3807
    42
  "sigma |= Dmd(F)"       == "Dmd F sigma"
wenzelm@3807
    43
  "sigma |= F ~> G"       == "op ~> F G sigma"
wenzelm@3807
    44
  "sigma |= stable(A)"    == "stable A sigma"
wenzelm@3807
    45
  "sigma |= WF(A)_v"      == "WF A v sigma"
wenzelm@3807
    46
  "sigma |= SF(A)_v"      == "SF A v sigma"
wenzelm@3807
    47
wenzelm@3808
    48
syntax (symbols)
wenzelm@3808
    49
  Box        :: "('w::world) form => temporal"      ("(\\<box>(_))" [40] 40)
wenzelm@3808
    50
  Dmd        :: "('w::world) form => temporal"      ("(\\<diamond>(_))" [40] 40)
wenzelm@3808
    51
wenzelm@3807
    52
rules
wenzelm@3807
    53
  dmd_def    "(<>F) == .~[].~F"
wenzelm@3807
    54
  boxact_def "([](F::action)) == ([] Init F)"
wenzelm@3807
    55
  leadsto    "P ~> Q == [](Init(P) .-> <>Q)"
wenzelm@3807
    56
  stable_def "stable P == [](P .-> P`)"
wenzelm@3807
    57
wenzelm@3807
    58
  WF_def     "WF(A)_v == <>[] $(Enabled(<A>_v)) .-> []<><A>_v"
wenzelm@3807
    59
  SF_def     "SF(A)_v == []<> $(Enabled(<A>_v)) .-> []<><A>_v"
wenzelm@3807
    60
wenzelm@3807
    61
  Init_def   "(sigma |= Init(F)) == ([[fst_st sigma, snd_st sigma]] |= F)"
wenzelm@3807
    62
wenzelm@3807
    63
(* The following axioms are written "polymorphically", not just for temporal formulas. *)
wenzelm@3807
    64
  normalT    "[](F .-> G) .-> ([]F .-> []G)"
wenzelm@3807
    65
  reflT      "[]F .-> F"         (* F::temporal *)
wenzelm@3807
    66
  transT     "[]F .-> [][]F"
wenzelm@3807
    67
  linT       "(<>F) .& (<>G) .-> (<>(F .& <>G)) .| (<>(G .& <>F))"   (* F,G::temporal *)
wenzelm@3807
    68
  discT      "[](F .-> <>(.~F .& <>F)) .-> (F .-> []<>F)"
wenzelm@3807
    69
  primeI     "[]P .-> Init(P`)"
wenzelm@3807
    70
  primeE     "[](Init(P) .-> []F) .-> Init(P`) .-> (F .-> []F)"
wenzelm@3807
    71
  indT       "[](Init(P) .& .~[]F .-> Init(P`) .& F) .-> Init(P) .-> []F"
wenzelm@3807
    72
  allT       "(RALL x. [](F(x))) .= ([](RALL x. F(x)))"
wenzelm@3807
    73
wenzelm@3807
    74
  necT       "F ==> []F"
wenzelm@3807
    75
wenzelm@3807
    76
(* Flexible quantification: refinement mappings, history variables *)
wenzelm@3807
    77
  aall_def      "(AALL x. F(x)) == .~ (EEX x. .~ F(x))"
wenzelm@3807
    78
  eexI          "F x .-> (EEX x. F x)"
wenzelm@3807
    79
  historyI      "[| sigma |= Init(I); sigma |= []N;
wenzelm@3807
    80
                    (!!h s t. (h s = ha s t) & I [[s,t]] --> HI(h)[[s,t]]);
wenzelm@3807
    81
                    (!!h s t. (h t = hc s t (h s)) & N [[s,t]] --> HN(h) [[s,t]])
wenzelm@3807
    82
                 |] ==> sigma |= (EEX h. Init(HI(h)) .& []HN(h))"
wenzelm@3807
    83
  eexE          "[| sigma |= (EEX x. F x);
wenzelm@3807
    84
		    (!!x. [| base_var x; (sigma |= F x) |] ==> (G sigma)::bool) 
wenzelm@3807
    85
		 |] ==> G sigma"
wenzelm@3807
    86
wenzelm@3807
    87
end