Theory TLA

Up to index of Isabelle/HOL/TLA

theory TLA
imports Init
uses [TLA.ML]
begin

(*
    File:        TLA/TLA.thy
    ID:          $Id: TLA.thy,v 1.8 2005/09/07 18:22:40 wenzelm Exp $
    Author:      Stephan Merz
    Copyright:   1998 University of Munich

    Theory Name: TLA
    Logic Image: HOL

The temporal level of TLA.
*)

theory TLA
imports Init
begin

consts
  (** abstract syntax **)
  Box        :: "('w::world) form => temporal"
  Dmd        :: "('w::world) form => temporal"
  leadsto    :: "['w::world form, 'v::world form] => temporal"
  Stable     :: "stpred => temporal"
  WF         :: "[action, 'a stfun] => temporal"
  SF         :: "[action, 'a stfun] => temporal"

  (* Quantification over (flexible) state variables *)
  EEx        :: "('a stfun => temporal) => temporal"       (binder "Eex " 10)
  AAll       :: "('a stfun => temporal) => temporal"       (binder "Aall " 10)

  (** concrete syntax **)
syntax
  "_Box"     :: "lift => lift"                        ("([]_)" [40] 40)
  "_Dmd"     :: "lift => lift"                        ("(<>_)" [40] 40)
  "_leadsto" :: "[lift,lift] => lift"                 ("(_ ~> _)" [23,22] 22)
  "_stable"  :: "lift => lift"                        ("(stable/ _)")
  "_WF"      :: "[lift,lift] => lift"                 ("(WF'(_')'_(_))" [0,60] 55)
  "_SF"      :: "[lift,lift] => lift"                 ("(SF'(_')'_(_))" [0,60] 55)

  "_EEx"     :: "[idts, lift] => lift"                ("(3EEX _./ _)" [0,10] 10)
  "_AAll"    :: "[idts, lift] => lift"                ("(3AALL _./ _)" [0,10] 10)

translations
  "_Box"      ==   "Box"
  "_Dmd"      ==   "Dmd"
  "_leadsto"  ==   "leadsto"
  "_stable"   ==   "Stable"
  "_WF"       ==   "WF"
  "_SF"       ==   "SF"
  "_EEx v A"  ==   "Eex v. A"
  "_AAll v A" ==   "Aall v. A"

  "sigma |= []F"         <= "_Box F sigma"
  "sigma |= <>F"         <= "_Dmd F sigma"
  "sigma |= F ~> G"      <= "_leadsto F G sigma"
  "sigma |= stable P"    <= "_stable P sigma"
  "sigma |= WF(A)_v"     <= "_WF A v sigma"
  "sigma |= SF(A)_v"     <= "_SF A v sigma"
  "sigma |= EEX x. F"    <= "_EEx x F sigma"
  "sigma |= AALL x. F"    <= "_AAll x F sigma"

syntax (xsymbols)
  "_Box"     :: "lift => lift"                        ("(\<box>_)" [40] 40)
  "_Dmd"     :: "lift => lift"                        ("(\<diamond>_)" [40] 40)
  "_leadsto" :: "[lift,lift] => lift"                 ("(_ \<leadsto> _)" [23,22] 22)
  "_EEx"     :: "[idts, lift] => lift"                ("(3∃∃ _./ _)" [0,10] 10)
  "_AAll"    :: "[idts, lift] => lift"                ("(3∀∀ _./ _)" [0,10] 10)

syntax (HTML output)
  "_EEx"     :: "[idts, lift] => lift"                ("(3∃∃ _./ _)" [0,10] 10)
  "_AAll"    :: "[idts, lift] => lift"                ("(3∀∀ _./ _)" [0,10] 10)

axioms
  (* Definitions of derived operators *)
  dmd_def:      "TEMP <>F  ==  TEMP ~[]~F"
  boxInit:      "TEMP []F  ==  TEMP []Init F"
  leadsto_def:  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
  stable_def:   "TEMP stable P  ==  TEMP []($P --> P$)"
  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
  aall_def:     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"

(* Base axioms for raw TLA. *)
  normalT:    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
  reflT:      "|- []F --> F"         (* F::temporal *)
  transT:     "|- []F --> [][]F"     (* polymorphic *)
  linT:       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
  discT:      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
  primeI:     "|- []P --> Init P`"
  primeE:     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
  indT:       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
  allT:       "|- (ALL x. [](F x)) = ([](ALL x. F x))"

  necT:       "|- F ==> |- []F"      (* polymorphic *)

(* Flexible quantification: refinement mappings, history variables *)
  eexI:       "|- F x --> (EEX x. F x)"
  eexE:       "[| sigma |= (EEX x. F x); basevars vs;
                 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
              |] ==> G sigma"
  history:    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"

ML {* use_legacy_bindings (the_context ()) *}

end

theorem tempI:

  (!!sigma. F sigma) ==> |- F

theorem tempD:

  |- F ==> F sigma

Simple temporal logic

theorem boxNotInit:

  []¬ F == []¬ Init F

theorem dmdInit:

  <>F == <>Init F

theorem dmdNotInit:

  <>¬ F == <>¬ Init F

theorem boxInit_stp:

  []F == []Init F

theorem boxInit_act:

  []F == []Init F

theorem dmdInit_stp:

  <>F == <>Init F

theorem dmdInit_act:

  <>F == <>Init F

theorem boxInitD:

  []Init F == []F

theorem dmdInitD:

  <>Init F == <>F

theorem boxNotInitD:

  []¬ Init F == []¬ F

theorem dmdNotInitD:

  <>¬ Init F == <>¬ F

theorem STL2:

  |- []F --> F

theorem STL2_gen:

  |- []F --> Init F

theorem InitDmd:

  |- F --> <>F

theorem InitDmd_gen:

  |- Init F --> <>F

theorem STL3:

  |- ([][]F) = ([]F)

theorem dup_boxE:

  [| sigma |= []F; sigma |= [][]F ==> PROP W |] ==> PROP W

theorem dup_boxD:

  sigma |= [][]F ==> sigma |= []F

theorem DmdDmd:

  |- (<><>F) = (<>F)

theorem dup_dmdE:

  [| sigma |= <>F; sigma |= <><>F ==> PROP W |] ==> PROP W

theorem dup_dmdD:

  sigma |= <><>F ==> sigma |= <>F

theorem STL4:

  |- F --> G ==> |- []F --> []G

theorem STL4E:

  [| sigma |= []F; |- F --> G |] ==> sigma |= []G

theorem STL4_gen:

  |- Init F --> Init G ==> |- []F --> []G

theorem STL4E_gen:

  [| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G

theorem DmdImpl:

  |- F --> G ==> |- <>F --> <>G

theorem DmdImplE:

  [| sigma |= <>F; |- F --> G |] ==> sigma |= <>G

theorem STL5:

  |- ([]F ∧ []G) = ([](FG))

theorem split_box_conj:

  (sigma |= [](FG)) = ((sigma |= []F) ∧ (sigma |= []G))

theorem box_conjE:

  [| sigma |= []F; sigma |= []G; sigma |= [](FG) ==> PROP R |] ==> PROP R

theorem box_conjE_temp:

  [| sigma |= []F; sigma |= []G; sigma |= [](FG) ==> PROP R |] ==> PROP R

theorem box_conjE_stp:

  [| sigma |= []F; sigma |= []G; sigma |= [](FG) ==> PROP R |] ==> PROP R

theorem box_conjE_act:

  [| sigma |= []F; sigma |= []G; sigma |= [](FG) ==> PROP R |] ==> PROP R

theorem all_box:

  (sigma |= []RAll F) = (∀x. sigma |= []F x)

theorem DmdOr:

  |- (<>(FG)) = (<>F ∨ <>G)

theorem exT:

  |- (∃x. <>F x) = (<>(∃x. F x))

theorem ex_dmd:

  (sigma |= <>REx F) = (∃x. sigma |= <>F x)

theorem STL4Edup:

  [| sigma |= []A; sigma |= []F; |- F ∧ []A --> G |] ==> sigma |= []G

theorem DmdImpl2:

  [| sigma |= <>F; sigma |= [](F --> G) |] ==> sigma |= <>G

theorem InfImpl:

  [| sigma |= []<>F; sigma |= []G; |- FG --> H |] ==> sigma |= []<>H

theorem BoxDmd:

  |- []F ∧ <>G --> <>([]FG)

theorem BoxDmd_simple:

  |- []F ∧ <>G --> <>(FG)

theorem BoxDmd2_simple:

  |- []F ∧ <>G --> <>(GF)

theorem DmdImpldup:

  [| sigma |= []A; sigma |= <>F; |- []AF --> G |] ==> sigma |= <>G

theorem STL6:

  |- <>[]F ∧ <>[]G --> <>[](FG)

Simplification of constants

theorem BoxConst:

  |- ([]#P) = #P

theorem DmdConst:

  |- (<>#P) = #P

Further rewrites

theorem NotBox:

  |- (¬ []F) = (<>¬ F)

theorem NotDmd:

  |- (¬ <>F) = ([]¬ F)

theorem BoxDmdBox:

  |- ([]<>[]F) = (<>[]F)

theorem DmdBoxDmd:

  |- (<>[]<>F) = ([]<>F)

theorem BoxOr:

  sigma |= []F ∨ []G ==> sigma |= [](FG)

theorem DBImplBD:

  |- <>[]F --> []<>F

theorem BoxDmdDmdBox:

  |- []<>F ∧ <>[]G --> []<>(FG)

priming

theorem STL2_pr:

  |- []P --> Init P ∧ Init P$

theorem BoxPrime:

  |- []P --> []($PP$)

theorem TLA2:

  |- $PP$ --> A ==> |- []P --> []A

theorem TLA2E:

  [| sigma |= []P; |- $PP$ --> A |] ==> sigma |= []A

theorem DmdPrime:

  |- <>P$ --> <>P

theorem PrimeDmd:

  sigma |= Init P$ ==> sigma |= <>P

stable, invariant

theorem ind_rule:

  [| sigma |= []H; sigma |= Init P; |- H --> Init P ∧ ¬ []F --> Init P$ ∧ F |]
  ==> sigma |= []F

theorem box_stp_act:

  |- ([]$P) = ([]P)

theorem box_stp_actI:

  sigma |= []P ==> sigma |= []$P

theorem box_stp_actD:

  sigma |= []$P ==> sigma |= []P

theorem INV1:

  |- Init P --> stable P --> []P

theorem StableT:

  |- $PA --> P$ ==> |- []A --> stable P

theorem Stable:

  [| sigma |= []A; |- $PA --> P$ |] ==> sigma |= stable P

theorem StableBox:

  |- stable P --> [](Init P --> []P)

theorem DmdStable:

  |- stable P ∧ <>P --> <>[]P

theorem unless:

  |- []($P --> P$ ∨ Q$) --> stable P ∨ <>Q

recursive expansions

theorem BoxRec:

  |- ([]P) = (Init P ∧ []P$)

theorem DmdRec:

  |- (<>P) = (Init P ∨ <>P$)

theorem DmdRec2:

  [| sigma |= <>P; sigma |= []¬ P$ |] ==> sigma |= Init P

theorem InfinitePrime:

  |- ([]<>P) = ([]<>P$)

theorem InfiniteEnsures:

  [| sigma |= []N; sigma |= []<>A; |- AN --> P$ |] ==> sigma |= []<>P

fairness

theorem WF_alt:

  |- WF(A)_v = ([]<>¬ Enabled (<A>_v) ∨ []<><A>_v)

theorem SF_alt:

  |- SF(A)_v = (<>[]¬ Enabled (<A>_v) ∨ []<><A>_v)

theorem BoxWFI:

  |- WF(A)_v --> []WF(A)_v

theorem WF_Box:

  |- ([]WF(A)_v) = WF(A)_v

theorem BoxSFI:

  |- SF(A)_v --> []SF(A)_v

theorem SF_Box:

  |- ([]SF(A)_v) = SF(A)_v

theorem SFImplWF:

  |- SF(A)_v --> WF(A)_v

~>

theorem leadsto_init:

  |- Init F ∧ (F ~> G) --> <>G

theorem leadsto_init_temp:

  |- F ∧ (F ~> G) --> <>G

theorem streett_leadsto:

  |- ([]<>Init F --> []<>G) = (<>(F ~> G))

theorem leadsto_infinite:

  |- []<>F ∧ (F ~> G) --> []<>G

theorem leadsto_SF:

  |- (Enabled (<A>_v) ~> <A>_v) --> SF(A)_v

theorem leadsto_WF:

  |- (Enabled (<A>_v) ~> <A>_v) --> WF(A)_v

theorem INV_leadsto:

  |- []I ∧ (PI ~> Q) --> (P ~> Q)

theorem leadsto_classical:

  |- (Init F ∧ []¬ G ~> G) --> (F ~> G)

theorem leadsto_false:

  |- (F ~> #False) = ([]¬ F)

theorem leadsto_exists:

  |- ((∃x. F x) ~> G) = (∀x. F x ~> G)

theorem ImplLeadsto_gen:

  |- [](Init F --> Init G) --> (F ~> G)

theorem ImplLeadsto:

  |- [](F --> G) --> (F ~> G)

theorem ImplLeadsto_simple:

  |- F --> G ==> |- F ~> G

theorem EnsuresLeadsto:

  |- A ∧ $P --> Q$ ==> |- []A --> (P ~> Q)

theorem EnsuresLeadsto2:

  |- []($P --> Q$) --> (P ~> Q)

theorem ensures:

  [| |- $PN --> P$ ∨ Q$; |- ($PN) ∧ A --> Q$ |]
  ==> |- []N ∧ []([]P --> <>A) --> (P ~> Q)

theorem ensures_simple:

  [| |- $PN --> P$ ∨ Q$; |- ($PN) ∧ A --> Q$ |]
  ==> |- []N ∧ []<>A --> (P ~> Q)

theorem EnsuresInfinite:

  [| sigma |= []<>P; sigma |= []A; |- A ∧ $P --> Q$ |] ==> sigma |= []<>Q

Lattice rules

theorem LatticeReflexivity:

  |- F ~> F

theorem LatticeTransitivity:

  |- (G ~> H) ∧ (F ~> G) --> (F ~> H)

theorem LatticeDisjunctionElim1:

  |- (FG ~> H) --> (F ~> H)

theorem LatticeDisjunctionElim2:

  |- (FG ~> H) --> (G ~> H)

theorem LatticeDisjunctionIntro:

  |- (F ~> H) ∧ (G ~> H) --> (FG ~> H)

theorem LatticeDisjunction:

  |- (FG ~> H) = ((F ~> H) ∧ (G ~> H))

theorem LatticeDiamond:

  |- (A ~> BC) ∧ (B ~> D) ∧ (C ~> D) --> (A ~> D)

theorem LatticeTriangle:

  |- (A ~> DB) ∧ (B ~> D) --> (A ~> D)

theorem LatticeTriangle2:

  |- (A ~> BD) ∧ (B ~> D) --> (A ~> D)

Fairness rules

theorem WF1:

  [| |- $PN --> P$ ∨ Q$; |- ($PN) ∧ <A>_v --> Q$;
     |- $PN --> $Enabled (<A>_v) |]
  ==> |- []N ∧ WF(A)_v --> (P ~> Q)

theorem WF_leadsto:

  [| |- N ∧ $P --> $Enabled (<A>_v); |- N ∧ <A>_v --> B;
     |- [](N ∧ [¬ A]_v) --> stable P |]
  ==> |- []N ∧ WF(A)_v --> (P ~> B)

theorem SF1:

  [| |- $PN --> P$ ∨ Q$; |- ($PN) ∧ <A>_v --> Q$;
     |- []P ∧ []N ∧ []F --> <>Enabled (<A>_v) |]
  ==> |- []N ∧ SF(A)_v ∧ []F --> (P ~> Q)

theorem WF2:

  [| |- N ∧ <B>_f --> <M>_g; |- $PP$ ∧ <NA>_f --> B;
     |- P ∧ Enabled (<M>_g) --> Enabled (<A>_f);
     |- [](N ∧ [¬ B]_f) ∧ WF(A)_f ∧ []F ∧ <>[]Enabled (<M>_g) --> <>[]P |]
  ==> |- []N ∧ WF(A)_f ∧ []F --> WF(M)_g

theorem SF2:

  [| |- N ∧ <B>_f --> <M>_g; |- $PP$ ∧ <NA>_f --> B;
     |- P ∧ Enabled (<M>_g) --> Enabled (<A>_f);
     |- [](N ∧ [¬ B]_f) ∧ SF(A)_f ∧ []F ∧ []<>Enabled (<M>_g) --> <>[]P |]
  ==> |- []N ∧ SF(A)_f ∧ []F --> SF(M)_g

Well-founded orderings

theorem wf_leadsto:

  [| wf r; !!x. sigma |= F x ~> G ∨ (∃y. #((y, x) ∈ r) ∧ F y) |]
  ==> sigma |= F x ~> G

theorem wf_not_box_decrease:

  wf r ==> |- [][(v$, $v) ∈ #r]_v --> <>[][#False]_v

theorem wf_not_dmd_box_decrease:

  wf r ==> |- <>[][(v$, $v) ∈ #r]_v --> <>[][#False]_v

theorem wf_box_dmd_decrease:

  wf r ==> |- []<>(v$, $v) ∈ #r --> []<><(v$, $v) ∉ #r>_v

theorem nat_box_dmd_decrease:

  |- []<>n$ < $n --> []<>$n < n$

Flexible quantification

theorem aallI:

  [| basevars vs; !!x. basevars (x, vs) ==> F x sigma |] ==> (∀∀ x. F x) sigma

theorem aallE:

  |- (∀∀ x. F x) --> F x

theorem eex_mono:

  [| (∃∃ x. F x) sigma; !!x. sigma |= F x --> G x |] ==> (∃∃ x. G x) sigma

theorem aall_mono:

  [| (∀∀ x. F x) sigma; !!x. sigma |= F x --> G x |] ==> (∀∀ x. G x) sigma

theorem historyI:

  [| sigma |= Init I; sigma |= []N; basevars vs;
     !!h. basevars (h, vs) ==> |- Ih = ha --> HI h;
     !!h s t.
        [| basevars (h, vs); N (s, t); h t = hb (h s) (s, t) |] ==> HN h (s, t) |]
  ==> (∃∃ h. Init HI h ∧ []HN h) sigma