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