src/HOL/TLA/TLA.thy
changeset 3807 82a99b090d9d
child 3808 8489375c6198
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TLA/TLA.thy	Wed Oct 08 11:50:33 1997 +0200
     1.3 @@ -0,0 +1,85 @@
     1.4 +(* 
     1.5 +    File:        TLA/TLA.thy
     1.6 +    Author:      Stephan Merz
     1.7 +    Copyright:   1997 University of Munich
     1.8 +
     1.9 +    Theory Name: TLA
    1.10 +    Logic Image: HOL
    1.11 +
    1.12 +The temporal level of TLA.
    1.13 +*)
    1.14 +
    1.15 +TLA  =  Action + WF_Rel +
    1.16 +
    1.17 +types
    1.18 +    behavior
    1.19 +    temporal = "behavior form"
    1.20 +
    1.21 +arities
    1.22 +    behavior :: world
    1.23 +
    1.24 +consts
    1.25 +  (* get first 2 states of behavior *)
    1.26 +  fst_st     :: "behavior => state"
    1.27 +  snd_st     :: "behavior => state"
    1.28 +  
    1.29 +  Init       :: "action => temporal"
    1.30 +                 (* define Box and Dmd for both actions and temporals *)
    1.31 +  Box        :: "('w::world) form => temporal"      ("([](_))" [40] 40)
    1.32 +  Dmd        :: "('w::world) form => temporal"      ("(<>(_))" [40] 40)
    1.33 +  "~>"       :: "[action,action] => temporal"       (infixr 22)
    1.34 +  stable     :: "action => temporal"
    1.35 +  WF         :: "[action,'a stfun] => temporal"    ("(WF'(_')'_(_))" [0,60] 55)
    1.36 +  SF         :: "[action,'a stfun] => temporal"    ("(SF'(_')'_(_))" [0,60] 55)
    1.37 +
    1.38 +  (* Quantification over (flexible) state variables *)
    1.39 +  EEx        :: "('a stfun => temporal) => temporal"    (binder "EEX " 10)
    1.40 +  AAll       :: "('a stfun => temporal) => temporal"    (binder "AALL " 10)
    1.41 +
    1.42 +translations
    1.43 +  "sigma |= Init(A)"      == "Init A sigma"
    1.44 +  "sigma |= Box(F)"       == "Box F sigma"
    1.45 +  "sigma |= Dmd(F)"       == "Dmd F sigma"
    1.46 +  "sigma |= F ~> G"       == "op ~> F G sigma"
    1.47 +  "sigma |= stable(A)"    == "stable A sigma"
    1.48 +  "sigma |= WF(A)_v"      == "WF A v sigma"
    1.49 +  "sigma |= SF(A)_v"      == "SF A v sigma"
    1.50 +
    1.51 +rules
    1.52 +  dmd_def    "(<>F) == .~[].~F"
    1.53 +  boxact_def "([](F::action)) == ([] Init F)"
    1.54 +  leadsto    "P ~> Q == [](Init(P) .-> <>Q)"
    1.55 +  stable_def "stable P == [](P .-> P`)"
    1.56 +
    1.57 +  WF_def     "WF(A)_v == <>[] $(Enabled(<A>_v)) .-> []<><A>_v"
    1.58 +  SF_def     "SF(A)_v == []<> $(Enabled(<A>_v)) .-> []<><A>_v"
    1.59 +
    1.60 +  Init_def   "(sigma |= Init(F)) == ([[fst_st sigma, snd_st sigma]] |= F)"
    1.61 +
    1.62 +(* The following axioms are written "polymorphically", not just for temporal formulas. *)
    1.63 +  normalT    "[](F .-> G) .-> ([]F .-> []G)"
    1.64 +  reflT      "[]F .-> F"         (* F::temporal *)
    1.65 +  transT     "[]F .-> [][]F"
    1.66 +  linT       "(<>F) .& (<>G) .-> (<>(F .& <>G)) .| (<>(G .& <>F))"   (* F,G::temporal *)
    1.67 +  discT      "[](F .-> <>(.~F .& <>F)) .-> (F .-> []<>F)"
    1.68 +  primeI     "[]P .-> Init(P`)"
    1.69 +  primeE     "[](Init(P) .-> []F) .-> Init(P`) .-> (F .-> []F)"
    1.70 +  indT       "[](Init(P) .& .~[]F .-> Init(P`) .& F) .-> Init(P) .-> []F"
    1.71 +  allT       "(RALL x. [](F(x))) .= ([](RALL x. F(x)))"
    1.72 +
    1.73 +  necT       "F ==> []F"
    1.74 +
    1.75 +(* Flexible quantification: refinement mappings, history variables *)
    1.76 +  aall_def      "(AALL x. F(x)) == .~ (EEX x. .~ F(x))"
    1.77 +  eexI          "F x .-> (EEX x. F x)"
    1.78 +  historyI      "[| sigma |= Init(I); sigma |= []N;
    1.79 +                    (!!h s t. (h s = ha s t) & I [[s,t]] --> HI(h)[[s,t]]);
    1.80 +                    (!!h s t. (h t = hc s t (h s)) & N [[s,t]] --> HN(h) [[s,t]])
    1.81 +                 |] ==> sigma |= (EEX h. Init(HI(h)) .& []HN(h))"
    1.82 +  eexE          "[| sigma |= (EEX x. F x);
    1.83 +		    (!!x. [| base_var x; (sigma |= F x) |] ==> (G sigma)::bool) 
    1.84 +		 |] ==> G sigma"
    1.85 +
    1.86 +end
    1.87 +
    1.88 +ML