# Theory Inc

Up to index of Isabelle/HOL/TLA/Inc

theory Inc
imports TLA
uses [Inc.ML]
begin

    (*
        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)