(* 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
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) = ([](F ∧ G))
theorem split_box_conj:
(sigma |= [](F ∧ G)) = ((sigma |= []F) ∧ (sigma |= []G))
theorem box_conjE:
[| sigma |= []F; sigma |= []G; sigma |= [](F ∧ G) ==> PROP R |] ==> PROP R
theorem box_conjE_temp:
[| sigma |= []F; sigma |= []G; sigma |= [](F ∧ G) ==> PROP R |] ==> PROP R
theorem box_conjE_stp:
[| sigma |= []F; sigma |= []G; sigma |= [](F ∧ G) ==> PROP R |] ==> PROP R
theorem box_conjE_act:
[| sigma |= []F; sigma |= []G; sigma |= [](F ∧ G) ==> PROP R |] ==> PROP R
theorem all_box:
(sigma |= []RAll F) = (∀x. sigma |= []F x)
theorem DmdOr:
|- (<>(F ∨ G)) = (<>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; |- F ∧ G --> H |] ==> sigma |= []<>H
theorem BoxDmd:
|- []F ∧ <>G --> <>([]F ∧ G)
theorem BoxDmd_simple:
|- []F ∧ <>G --> <>(F ∧ G)
theorem BoxDmd2_simple:
|- []F ∧ <>G --> <>(G ∧ F)
theorem DmdImpldup:
[| sigma |= []A; sigma |= <>F; |- []A ∧ F --> G |] ==> sigma |= <>G
theorem STL6:
|- <>[]F ∧ <>[]G --> <>[](F ∧ G)
theorem BoxConst:
|- ([]#P) = #P
theorem DmdConst:
|- (<>#P) = #P
theorem NotBox:
|- (¬ []F) = (<>¬ F)
theorem NotDmd:
|- (¬ <>F) = ([]¬ F)
theorem BoxDmdBox:
|- ([]<>[]F) = (<>[]F)
theorem DmdBoxDmd:
|- (<>[]<>F) = ([]<>F)
theorem BoxOr:
sigma |= []F ∨ []G ==> sigma |= [](F ∨ G)
theorem DBImplBD:
|- <>[]F --> []<>F
theorem BoxDmdDmdBox:
|- []<>F ∧ <>[]G --> []<>(F ∧ G)
theorem STL2_pr:
|- []P --> Init P ∧ Init P$
theorem BoxPrime:
|- []P --> []($P ∧ P$)
theorem TLA2:
|- $P ∧ P$ --> A ==> |- []P --> []A
theorem TLA2E:
[| sigma |= []P; |- $P ∧ P$ --> A |] ==> sigma |= []A
theorem DmdPrime:
|- <>P$ --> <>P
theorem PrimeDmd:
sigma |= Init P$ ==> sigma |= <>P
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:
|- $P ∧ A --> P$ ==> |- []A --> stable P
theorem Stable:
[| sigma |= []A; |- $P ∧ A --> 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
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; |- A ∧ N --> P$ |] ==> sigma |= []<>P
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 ∧ (P ∧ I ~> 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:
[| |- $P ∧ N --> P$ ∨ Q$; |- ($P ∧ N) ∧ A --> Q$ |] ==> |- []N ∧ []([]P --> <>A) --> (P ~> Q)
theorem ensures_simple:
[| |- $P ∧ N --> P$ ∨ Q$; |- ($P ∧ N) ∧ A --> Q$ |] ==> |- []N ∧ []<>A --> (P ~> Q)
theorem EnsuresInfinite:
[| sigma |= []<>P; sigma |= []A; |- A ∧ $P --> Q$ |] ==> sigma |= []<>Q
theorem LatticeReflexivity:
|- F ~> F
theorem LatticeTransitivity:
|- (G ~> H) ∧ (F ~> G) --> (F ~> H)
theorem LatticeDisjunctionElim1:
|- (F ∨ G ~> H) --> (F ~> H)
theorem LatticeDisjunctionElim2:
|- (F ∨ G ~> H) --> (G ~> H)
theorem LatticeDisjunctionIntro:
|- (F ~> H) ∧ (G ~> H) --> (F ∨ G ~> H)
theorem LatticeDisjunction:
|- (F ∨ G ~> H) = ((F ~> H) ∧ (G ~> H))
theorem LatticeDiamond:
|- (A ~> B ∨ C) ∧ (B ~> D) ∧ (C ~> D) --> (A ~> D)
theorem LatticeTriangle:
|- (A ~> D ∨ B) ∧ (B ~> D) --> (A ~> D)
theorem LatticeTriangle2:
|- (A ~> B ∨ D) ∧ (B ~> D) --> (A ~> D)
theorem WF1:
[| |- $P ∧ N --> P$ ∨ Q$; |- ($P ∧ N) ∧ <A>_v --> Q$; |- $P ∧ N --> $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:
[| |- $P ∧ N --> P$ ∨ Q$; |- ($P ∧ N) ∧ <A>_v --> Q$; |- []P ∧ []N ∧ []F --> <>Enabled (<A>_v) |] ==> |- []N ∧ SF(A)_v ∧ []F --> (P ~> Q)
theorem WF2:
[| |- N ∧ <B>_f --> <M>_g; |- $P ∧ P$ ∧ <N ∧ A>_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; |- $P ∧ P$ ∧ <N ∧ A>_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
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$
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) ==> |- I ∧ h = 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