--- a/src/HOL/TLA/Inc/Inc.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,69 +1,90 @@
-(*
+(*
File: TLA/Inc/Inc.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
Theory Name: Inc
- Logic Image: TLA
-
- Lamport's "increment" example.
+ Logic Image: TLA
*)
-Inc = 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,y,sem :: nat stfun
- pc1,pc2 :: pcount stfun
+ x :: "nat stfun"
+ y :: "nat stfun"
+ sem :: "nat stfun"
+ pc1 :: "pcount stfun"
+ pc2 :: "pcount stfun"
(* names of actions and predicates *)
- M1,M2,N1,N2 :: action
- alpha1,alpha2,beta1,beta2,gamma1,gamma2 :: action
- InitPhi, InitPsi :: stpred
- PsiInv,PsiInv1,PsiInv2,PsiInv3 :: stpred
+ 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, Psi :: temporal
-
-rules
+ Phi :: temporal
+ Psi :: temporal
+
+axioms
(* the "base" variables, required to compute enabledness predicates *)
- Inc_base "basevars (x, y, sem, pc1, pc2)"
+ 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)
+ 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
+ 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$>
+ 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$>
+ 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>
+ 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>
+ 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>
+ 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>
+ 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_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)"
-
+ 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