(* File: TLA/Inc/Inc.thy ID: $Id: Inc.thy,v 1.5 2005/09/07 18:22:41 wenzelm Exp $ Author: Stephan Merz Copyright: 1997 University of Munich Theory Name: Inc Logic Image: TLA *) header {* Lamport's "increment" example *} theory Inc imports TLA begin (* program counter as an enumeration type *) datatype pcount = a | b | g consts (* program variables *) x :: "nat stfun" y :: "nat stfun" sem :: "nat stfun" pc1 :: "pcount stfun" pc2 :: "pcount stfun" (* names of actions and predicates *) M1 :: action M2 :: action N1 :: action N2 :: action alpha1 :: action alpha2 :: action beta1 :: action beta2 :: action gamma1 :: action gamma2 :: action InitPhi :: stpred InitPsi :: stpred PsiInv :: stpred PsiInv1 :: stpred PsiInv2 :: stpred PsiInv3 :: stpred (* temporal formulas *) Phi :: temporal Psi :: temporal axioms (* the "base" variables, required to compute enabledness predicates *) Inc_base: "basevars (x, y, sem, pc1, pc2)" (* definitions for high-level program *) InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0" M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y" M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x" Phi_def: "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y) & WF(M1)_(x,y) & WF(M2)_(x,y)" (* definitions for low-level program *) InitPsi_def: "InitPsi == PRED pc1 = #a & pc2 = #a & x = # 0 & y = # 0 & sem = # 1" alpha1_def: "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem$> & unchanged(x,y,pc2)" alpha2_def: "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem$> & unchanged(x,y,pc1)" beta1_def: "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x> & unchanged(y,sem,pc2)" beta2_def: "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y> & unchanged(x,sem,pc1)" gamma1_def: "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem> & unchanged(x,y,pc2)" gamma2_def: "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem> & unchanged(x,y,pc1)" N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)" N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)" Psi_def: "Psi == TEMP Init InitPsi & [][N1 | N2]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)" PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a" PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" PsiInv_def: "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)" ML {* use_legacy_bindings (the_context ()) *} end
theorem PsiInv_Init:
|- InitPsi --> PsiInv
theorem PsiInv_alpha1:
|- alpha1 ∧ $PsiInv --> PsiInv$
theorem PsiInv_alpha2:
|- alpha2 ∧ $PsiInv --> PsiInv$
theorem PsiInv_beta1:
|- beta1 ∧ $PsiInv --> PsiInv$
theorem PsiInv_beta2:
|- beta2 ∧ $PsiInv --> PsiInv$
theorem PsiInv_gamma1:
|- gamma1 ∧ $PsiInv --> PsiInv$
theorem PsiInv_gamma2:
|- gamma2 ∧ $PsiInv --> PsiInv$
theorem PsiInv_stutter:
|- unchanged (x, y, sem, pc1, pc2) ∧ $PsiInv --> PsiInv$
theorem PsiInv:
|- Psi --> []PsiInv
theorem Init_sim:
|- Psi --> Init InitPhi
theorem Step_sim:
|- Psi --> [][M1 ∨ M2]_(x, y)
theorem Stuck_at_b:
|- [][(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2) --> stable pc1 = #b
theorem N1_enabled_at_g:
|- pc1 = #g --> Enabled (<N1>_(x, y, sem, pc1, pc2))
theorem g1_leadsto_a1:
|- [][(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2) ∧ SF(N1)_(x, y, sem, pc1, pc2) ∧ []#True --> (pc1 = #g ~> pc1 = #a)
theorem N2_enabled_at_g:
|- pc2 = #g --> Enabled (<N2>_(x, y, sem, pc1, pc2))
theorem g2_leadsto_a2:
|- [][(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2) ∧ SF(N2)_(x, y, sem, pc1, pc2) ∧ []#True --> (pc2 = #g ~> pc2 = #a)
theorem N2_enabled_at_b:
|- pc2 = #b --> Enabled (<N2>_(x, y, sem, pc1, pc2))
theorem b2_leadsto_g2:
|- [][(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2) ∧ SF(N2)_(x, y, sem, pc1, pc2) ∧ []#True --> (pc2 = #b ~> pc2 = #g)
theorem N2_leadsto_a:
|- [][(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2) ∧ SF(N2)_(x, y, sem, pc1, pc2) ∧ []#True --> (pc2 = #a ∨ pc2 = #b ∨ pc2 = #g ~> pc2 = #a)
theorem N2_live:
|- [][(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2) ∧ SF(N2)_(x, y, sem, pc1, pc2) --> <>pc2 = #a
theorem N1_enabled_at_both_a:
|- pc2 = #a ∧ PsiInv ∧ pc1 = #a --> Enabled (<N1>_(x, y, sem, pc1, pc2))
theorem a1_leadsto_b1:
|- []($PsiInv ∧ [(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2)) ∧ SF(N1)_(x, y, sem, pc1, pc2) ∧ []SF(N2)_(x, y, sem, pc1, pc2) --> (pc1 = #a ~> pc1 = #b)
theorem N1_leadsto_b:
|- []($PsiInv ∧ [(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2)) ∧ SF(N1)_(x, y, sem, pc1, pc2) ∧ []SF(N2)_(x, y, sem, pc1, pc2) --> (pc1 = #b ∨ pc1 = #g ∨ pc1 = #a ~> pc1 = #b)
theorem N1_live:
|- []($PsiInv ∧ [(N1 ∨ N2) ∧ ¬ beta1]_(x, y, sem, pc1, pc2)) ∧ SF(N1)_(x, y, sem, pc1, pc2) ∧ []SF(N2)_(x, y, sem, pc1, pc2) --> <>pc1 = #b
theorem N1_enabled_at_b:
|- pc1 = #b --> Enabled (<N1>_(x, y, sem, pc1, pc2))
theorem Fair_M1_lemma:
|- []($PsiInv ∧ [N1 ∨ N2]_(x, y, sem, pc1, pc2)) ∧ SF(N1)_(x, y, sem, pc1, pc2) ∧ []SF(N2)_(x, y, sem, pc1, pc2) --> SF(M1)_(x, y)
theorem Fair_M1:
|- Psi --> WF(M1)_(x, y)