wenzelm@41589: (*  Title:      HOL/TLA/Inc/Inc.thy
wenzelm@41589:     Author:     Stephan Merz, University of Munich
wenzelm@3807: *)
wenzelm@3807: 
wenzelm@58889: section {* Lamport's "increment" example *}
wenzelm@17309: 
wenzelm@17309: theory Inc
wenzelm@17309: imports TLA
wenzelm@17309: begin
wenzelm@6255: 
wenzelm@6255: (* program counter as an enumeration type *)
blanchet@58310: datatype pcount = a | b | g
wenzelm@3807: 
wenzelm@47968: axiomatization
wenzelm@3807:   (* program variables *)
wenzelm@47968:   x :: "nat stfun" and
wenzelm@47968:   y :: "nat stfun" and
wenzelm@47968:   sem :: "nat stfun" and
wenzelm@47968:   pc1 :: "pcount stfun" and
wenzelm@47968:   pc2 :: "pcount stfun" and
wenzelm@3807: 
wenzelm@3807:   (* names of actions and predicates *)
wenzelm@47968:   M1 :: action and
wenzelm@47968:   M2 :: action and
wenzelm@47968:   N1 :: action and
wenzelm@47968:   N2 :: action and
wenzelm@47968:   alpha1 :: action and
wenzelm@47968:   alpha2 :: action and
wenzelm@47968:   beta1 :: action and
wenzelm@47968:   beta2 :: action and
wenzelm@47968:   gamma1 :: action and
wenzelm@47968:   gamma2 :: action and
wenzelm@47968:   InitPhi :: stpred and
wenzelm@47968:   InitPsi :: stpred and
wenzelm@47968:   PsiInv :: stpred and
wenzelm@47968:   PsiInv1 :: stpred and
wenzelm@47968:   PsiInv2 :: stpred and
wenzelm@47968:   PsiInv3 :: stpred and
wenzelm@3807: 
wenzelm@3807:   (* temporal formulas *)
wenzelm@47968:   Phi :: temporal and
wenzelm@17309:   Psi :: temporal
wenzelm@47968: where
wenzelm@3807:   (* the "base" variables, required to compute enabledness predicates *)
wenzelm@47968:   Inc_base:      "basevars (x, y, sem, pc1, pc2)" and
wenzelm@3807: 
wenzelm@3807:   (* definitions for high-level program *)
wenzelm@47968:   InitPhi_def:   "InitPhi == PRED x = # 0 & y = # 0" and
wenzelm@47968:   M1_def:        "M1      == ACT  x$ = Suc<$x> & y$ = $y" and
wenzelm@47968:   M2_def:        "M2      == ACT  y$ = Suc<$y> & x$ = $x" and
wenzelm@17309:   Phi_def:       "Phi     == TEMP Init InitPhi & [][M1 | M2]_(x,y)
wenzelm@47968:                                  & WF(M1)_(x,y) & WF(M2)_(x,y)" and
wenzelm@3807: 
wenzelm@3807:   (* definitions for low-level program *)
wenzelm@17309:   InitPsi_def:   "InitPsi == PRED pc1 = #a & pc2 = #a
wenzelm@47968:                                  & x = # 0 & y = # 0 & sem = # 1" and
wenzelm@17309:   alpha1_def:    "alpha1  == ACT  $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
wenzelm@47968:                                  & unchanged(x,y,pc2)" and
wenzelm@17309:   alpha2_def:    "alpha2  == ACT  $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
wenzelm@47968:                                  & unchanged(x,y,pc1)" and
wenzelm@17309:   beta1_def:     "beta1   == ACT  $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
wenzelm@47968:                                  & unchanged(y,sem,pc2)" and
wenzelm@17309:   beta2_def:     "beta2   == ACT  $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
wenzelm@47968:                                  & unchanged(x,sem,pc1)" and
wenzelm@17309:   gamma1_def:    "gamma1  == ACT  $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
wenzelm@47968:                                  & unchanged(x,y,pc2)" and
wenzelm@17309:   gamma2_def:    "gamma2  == ACT  $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
wenzelm@47968:                                  & unchanged(x,y,pc1)" and
wenzelm@47968:   N1_def:        "N1      == ACT  (alpha1 | beta1 | gamma1)" and
wenzelm@47968:   N2_def:        "N2      == ACT  (alpha2 | beta2 | gamma2)" and
wenzelm@17309:   Psi_def:       "Psi     == TEMP Init InitPsi
wenzelm@6255:                                & [][N1 | N2]_(x,y,sem,pc1,pc2)
wenzelm@6255:                                & SF(N1)_(x,y,sem,pc1,pc2)
wenzelm@47968:                                & SF(N2)_(x,y,sem,pc1,pc2)" and
wenzelm@3807: 
wenzelm@47968:   PsiInv1_def:  "PsiInv1  == PRED sem = # 1 & pc1 = #a & pc2 = #a" and
wenzelm@47968:   PsiInv2_def:  "PsiInv2  == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" and
wenzelm@47968:   PsiInv3_def:  "PsiInv3  == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" and
wenzelm@17309:   PsiInv_def:   "PsiInv   == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
wenzelm@17309: 
wenzelm@21624: 
wenzelm@21624: lemmas PsiInv_defs = PsiInv_def PsiInv1_def PsiInv2_def PsiInv3_def
wenzelm@21624: lemmas Psi_defs = Psi_def InitPsi_def N1_def N2_def alpha1_def alpha2_def
wenzelm@21624:   beta1_def beta2_def gamma1_def gamma2_def
wenzelm@21624: 
wenzelm@21624: 
wenzelm@21624: (*** Invariant proof for Psi: "manual" proof proves individual lemmas ***)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv_Init: "|- InitPsi --> PsiInv"
wenzelm@21624:   by (auto simp: InitPsi_def PsiInv_defs)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv_alpha1: "|- alpha1 & $PsiInv --> PsiInv$"
wenzelm@21624:   by (auto simp: alpha1_def PsiInv_defs)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv_alpha2: "|- alpha2 & $PsiInv --> PsiInv$"
wenzelm@21624:   by (auto simp: alpha2_def PsiInv_defs)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv_beta1: "|- beta1 & $PsiInv --> PsiInv$"
wenzelm@21624:   by (auto simp: beta1_def PsiInv_defs)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv_beta2: "|- beta2 & $PsiInv --> PsiInv$"
wenzelm@21624:   by (auto simp: beta2_def PsiInv_defs)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv_gamma1: "|- gamma1 & $PsiInv --> PsiInv$"
wenzelm@21624:   by (auto simp: gamma1_def PsiInv_defs)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv_gamma2: "|- gamma2 & $PsiInv --> PsiInv$"
wenzelm@21624:   by (auto simp: gamma2_def PsiInv_defs)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv_stutter: "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv$"
wenzelm@21624:   by (auto simp: PsiInv_defs)
wenzelm@21624: 
wenzelm@21624: lemma PsiInv: "|- Psi --> []PsiInv"
wenzelm@42769:   apply (invariant simp: Psi_def)
wenzelm@21624:    apply (force simp: PsiInv_Init [try_rewrite] Init_def)
wenzelm@21624:   apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
wenzelm@21624:     PsiInv_beta1 [try_rewrite] PsiInv_beta2 [try_rewrite] PsiInv_gamma1 [try_rewrite]
wenzelm@21624:     PsiInv_gamma2 [try_rewrite] PsiInv_stutter [try_rewrite]
wenzelm@21624:     simp add: square_def N1_def N2_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: (* Automatic proof works too, but it make take a while on a slow machine.
wenzelm@21624:    More realistic examples require user guidance anyway.
wenzelm@21624: *)
wenzelm@21624: 
wenzelm@21624: lemma "|- Psi --> []PsiInv"
wenzelm@42769:   by (auto_invariant simp: PsiInv_defs Psi_defs)
wenzelm@21624: 
wenzelm@21624: 
wenzelm@21624: (**** Step simulation ****)
wenzelm@21624: 
wenzelm@21624: lemma Init_sim: "|- Psi --> Init InitPhi"
wenzelm@21624:   by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def)
wenzelm@21624: 
wenzelm@21624: lemma Step_sim: "|- Psi --> [][M1 | M2]_(x,y)"
wenzelm@21624:   by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use])
wenzelm@21624: 
wenzelm@21624: 
wenzelm@21624: (**** Proof of fairness ****)
wenzelm@21624: 
wenzelm@21624: (*
wenzelm@21624:    The goal is to prove Fair_M1 far below, which asserts
wenzelm@21624:          |- Psi --> WF(M1)_(x,y)
wenzelm@21624:    (the other fairness condition is symmetrical).
wenzelm@21624: 
wenzelm@21624:    The strategy is to use WF2 (with beta1 as the helpful action). Proving its
wenzelm@21624:    temporal premise needs two auxiliary lemmas:
wenzelm@21624:    1. Stuck_at_b: control can only proceed at pc1 = b by executing beta1
wenzelm@21624:    2. N1_live: the first component will eventually reach b
wenzelm@21624: 
wenzelm@21624:    Lemma 1 is easy, lemma 2 relies on the invariant, the strong fairness
wenzelm@21624:    of the semaphore, and needs auxiliary lemmas that ensure that the second
wenzelm@21624:    component will eventually release the semaphore. Most of the proofs of
wenzelm@21624:    the auxiliary lemmas are very similar.
wenzelm@21624: *)
wenzelm@21624: 
wenzelm@21624: lemma Stuck_at_b: "|- [][(N1 | N2) & ~ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)"
wenzelm@21624:   by (auto elim!: Stable squareE simp: Psi_defs)
wenzelm@21624: 
wenzelm@21624: lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
wenzelm@21624:   apply clarsimp
wenzelm@21624:   apply (rule_tac F = gamma1 in enabled_mono)
wenzelm@42785:    apply (enabled Inc_base)
wenzelm@21624:   apply (force simp: gamma1_def)
wenzelm@21624:   apply (force simp: angle_def gamma1_def N1_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: lemma g1_leadsto_a1:
wenzelm@21624:   "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & []#True  
wenzelm@21624:     --> (pc1 = #g ~> pc1 = #a)"
wenzelm@21624:   apply (rule SF1)
wenzelm@21624:     apply (tactic
wenzelm@51717:       {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
wenzelm@21624:    apply (tactic
wenzelm@51717:       {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
wenzelm@21624:   (* reduce |- []A --> <>Enabled B  to  |- A --> Enabled B *)
wenzelm@21624:   apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
wenzelm@21624:     dest!: STL2_gen [temp_use] simp: Init_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: (* symmetrical for N2, and similar for beta2 *)
wenzelm@21624: lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
wenzelm@21624:   apply clarsimp
wenzelm@21624:   apply (rule_tac F = gamma2 in enabled_mono)
wenzelm@42785:   apply (enabled Inc_base)
wenzelm@21624:    apply (force simp: gamma2_def)
wenzelm@21624:   apply (force simp: angle_def gamma2_def N2_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: lemma g2_leadsto_a2:
wenzelm@21624:   "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
wenzelm@21624:     --> (pc2 = #g ~> pc2 = #a)"
wenzelm@21624:   apply (rule SF1)
wenzelm@51717:   apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
wenzelm@51717:   apply (tactic {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs})
wenzelm@21624:     [] [] 1 *})
wenzelm@21624:   apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_g [temp_use]
wenzelm@21624:     dest!: STL2_gen [temp_use] simp add: Init_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
wenzelm@21624:   apply clarsimp
wenzelm@21624:   apply (rule_tac F = beta2 in enabled_mono)
wenzelm@42785:    apply (enabled Inc_base)
wenzelm@21624:    apply (force simp: beta2_def)
wenzelm@21624:   apply (force simp: angle_def beta2_def N2_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: lemma b2_leadsto_g2:
wenzelm@21624:   "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
wenzelm@21624:     --> (pc2 = #b ~> pc2 = #g)"
wenzelm@21624:   apply (rule SF1)
wenzelm@21624:     apply (tactic
wenzelm@51717:       {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
wenzelm@21624:    apply (tactic
wenzelm@51717:      {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
wenzelm@21624:   apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_b [temp_use]
wenzelm@21624:     dest!: STL2_gen [temp_use] simp: Init_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: (* Combine above lemmas: the second component will eventually reach pc2 = a *)
wenzelm@21624: lemma N2_leadsto_a:
wenzelm@21624:   "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
wenzelm@21624:     --> (pc2 = #a | pc2 = #b | pc2 = #g ~> pc2 = #a)"
wenzelm@21624:   apply (auto intro!: LatticeDisjunctionIntro [temp_use])
wenzelm@21624:     apply (rule LatticeReflexivity [temp_use])
wenzelm@21624:    apply (rule LatticeTransitivity [temp_use])
wenzelm@21624:   apply (auto intro!: b2_leadsto_g2 [temp_use] g2_leadsto_a2 [temp_use])
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: (* Get rid of disjunction on the left-hand side of ~> above. *)
wenzelm@21624: lemma N2_live:
wenzelm@21624:   "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)  
wenzelm@21624:     --> <>(pc2 = #a)"
wenzelm@21624:   apply (auto simp: Init_defs intro!: N2_leadsto_a [temp_use, THEN [2] leadsto_init [temp_use]])
wenzelm@21624:   apply (case_tac "pc2 (st1 sigma)")
wenzelm@21624:     apply auto
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: (* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
wenzelm@21624: 
wenzelm@21624: lemma N1_enabled_at_both_a:
wenzelm@21624:   "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
wenzelm@21624:   apply clarsimp
wenzelm@21624:   apply (rule_tac F = alpha1 in enabled_mono)
wenzelm@42785:   apply (enabled Inc_base)
wenzelm@21624:    apply (force simp: alpha1_def PsiInv_defs)
wenzelm@21624:   apply (force simp: angle_def alpha1_def N1_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: lemma a1_leadsto_b1:
wenzelm@21624:   "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))       
wenzelm@21624:          & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
wenzelm@21624:          --> (pc1 = #a ~> pc1 = #b)"
wenzelm@21624:   apply (rule SF1)
wenzelm@51717:   apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
wenzelm@21624:   apply (tactic
wenzelm@51717:     {* action_simp_tac (@{context} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
wenzelm@21624:   apply (clarsimp intro!: N1_enabled_at_both_a [THEN DmdImpl [temp_use]])
wenzelm@21624:   apply (auto intro!: BoxDmd2_simple [temp_use] N2_live [temp_use]
wenzelm@21624:     simp: split_box_conj more_temp_simps)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: (* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
wenzelm@21624: 
wenzelm@21624: lemma N1_leadsto_b: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))              
wenzelm@21624:          & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
wenzelm@21624:          --> (pc1 = #b | pc1 = #g | pc1 = #a ~> pc1 = #b)"
wenzelm@21624:   apply (auto intro!: LatticeDisjunctionIntro [temp_use])
wenzelm@21624:     apply (rule LatticeReflexivity [temp_use])
wenzelm@21624:    apply (rule LatticeTransitivity [temp_use])
wenzelm@21624:     apply (auto intro!: a1_leadsto_b1 [temp_use] g1_leadsto_a1 [temp_use]
wenzelm@21624:       simp: split_box_conj)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: lemma N1_live: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))              
wenzelm@21624:          & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
wenzelm@21624:          --> <>(pc1 = #b)"
wenzelm@21624:   apply (auto simp: Init_defs intro!: N1_leadsto_b [temp_use, THEN [2] leadsto_init [temp_use]])
wenzelm@21624:   apply (case_tac "pc1 (st1 sigma)")
wenzelm@21624:     apply auto
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
wenzelm@21624:   apply clarsimp
wenzelm@21624:   apply (rule_tac F = beta1 in enabled_mono)
wenzelm@42785:    apply (enabled Inc_base)
wenzelm@21624:    apply (force simp: beta1_def)
wenzelm@21624:   apply (force simp: angle_def beta1_def N1_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: (* Now assemble the bits and pieces to prove that Psi is fair. *)
wenzelm@21624: 
wenzelm@21624: lemma Fair_M1_lemma: "|- []($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))    
wenzelm@21624:          & SF(N1)_(x,y,sem,pc1,pc2) & []SF(N2)_(x,y,sem,pc1,pc2)   
wenzelm@21624:          --> SF(M1)_(x,y)"
wenzelm@21624:   apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2)
wenzelm@21624:    (* action premises *)
wenzelm@21624:      apply (force simp: angle_def M1_def beta1_def)
wenzelm@21624:   apply (force simp: angle_def Psi_defs)
wenzelm@21624:   apply (force elim!: N1_enabled_at_b [temp_use])
wenzelm@21624:     (* temporal premise: use previous lemmas and simple TL *)
wenzelm@21624:   apply (force intro!: DmdStable [temp_use] N1_live [temp_use] Stuck_at_b [temp_use]
wenzelm@21624:     elim: STL4E [temp_use] simp: square_def)
wenzelm@21624:   done
wenzelm@21624: 
wenzelm@21624: lemma Fair_M1: "|- Psi --> WF(M1)_(x,y)"
wenzelm@21624:   by (auto intro!: SFImplWF [temp_use] Fair_M1_lemma [temp_use] PsiInv [temp_use]
wenzelm@21624:     simp: Psi_def split_box_conj [temp_use] more_temp_simps)
wenzelm@17309: 
wenzelm@3807: end