eliminated old 'axioms';
authorwenzelm
Wed May 23 16:53:12 2012 +0200 (2012-05-23)
changeset 479683119ad2b5ad3
parent 47967 c422128d3889
child 47969 ce4345b06408
eliminated old 'axioms';
src/HOL/TLA/Action.thy
src/HOL/TLA/Buffer/DBuffer.thy
src/HOL/TLA/Inc/Inc.thy
src/HOL/TLA/Memory/MemoryParameters.thy
src/HOL/TLA/Memory/RPCParameters.thy
src/HOL/TLA/TLA.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Wed May 23 16:22:27 2012 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Wed May 23 16:53:12 2012 +0200
     1.3 @@ -58,11 +58,13 @@
     1.4    "s |= Enabled A"   <=   "_Enabled A s"
     1.5    "w |= unchanged f" <=   "_unchanged f w"
     1.6  
     1.7 -axioms
     1.8 -  unl_before:    "(ACT $v) (s,t) == v s"
     1.9 -  unl_after:     "(ACT v$) (s,t) == v t"
    1.10 +axiomatization where
    1.11 +  unl_before:    "(ACT $v) (s,t) == v s" and
    1.12 +  unl_after:     "(ACT v$) (s,t) == v t" and
    1.13  
    1.14    unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
    1.15 +
    1.16 +defs
    1.17    square_def:    "ACT [A]_v == ACT (A | unchanged v)"
    1.18    angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"
    1.19  
     2.1 --- a/src/HOL/TLA/Buffer/DBuffer.thy	Wed May 23 16:22:27 2012 +0200
     2.2 +++ b/src/HOL/TLA/Buffer/DBuffer.thy	Wed May 23 16:53:12 2012 +0200
     2.3 @@ -8,35 +8,34 @@
     2.4  imports Buffer
     2.5  begin
     2.6  
     2.7 -consts
     2.8 +axiomatization
     2.9    (* implementation variables *)
    2.10 -  inp  :: "nat stfun"
    2.11 -  mid  :: "nat stfun"
    2.12 -  out  :: "nat stfun"
    2.13 -  q1   :: "nat list stfun"
    2.14 -  q2   :: "nat list stfun"
    2.15 -  qc   :: "nat list stfun"
    2.16 +  inp  :: "nat stfun" and
    2.17 +  mid  :: "nat stfun" and
    2.18 +  out  :: "nat stfun" and
    2.19 +  q1   :: "nat list stfun" and
    2.20 +  q2   :: "nat list stfun" and
    2.21 +  qc   :: "nat list stfun" and
    2.22  
    2.23 -  DBInit :: stpred
    2.24 -  DBEnq :: action
    2.25 -  DBDeq :: action
    2.26 -  DBPass :: action
    2.27 -  DBNext :: action
    2.28 +  DBInit :: stpred and
    2.29 +  DBEnq :: action and
    2.30 +  DBDeq :: action and
    2.31 +  DBPass :: action and
    2.32 +  DBNext :: action and
    2.33    DBuffer :: temporal
    2.34 -
    2.35 -axioms
    2.36 -  DB_base:        "basevars (inp,mid,out,q1,q2)"
    2.37 +where
    2.38 +  DB_base:        "basevars (inp,mid,out,q1,q2)" and
    2.39  
    2.40    (* the concatenation of the two buffers *)
    2.41 -  qc_def:         "PRED qc == PRED (q2 @ q1)"
    2.42 +  qc_def:         "PRED qc == PRED (q2 @ q1)" and
    2.43  
    2.44 -  DBInit_def:     "DBInit   == PRED (BInit inp q1 mid  &  BInit mid q2 out)"
    2.45 -  DBEnq_def:      "DBEnq    == ACT  Enq inp q1 mid  &  unchanged (q2,out)"
    2.46 -  DBDeq_def:      "DBDeq    == ACT  Deq mid q2 out  &  unchanged (inp,q1)"
    2.47 +  DBInit_def:     "DBInit   == PRED (BInit inp q1 mid  &  BInit mid q2 out)" and
    2.48 +  DBEnq_def:      "DBEnq    == ACT  Enq inp q1 mid  &  unchanged (q2,out)" and
    2.49 +  DBDeq_def:      "DBDeq    == ACT  Deq mid q2 out  &  unchanged (inp,q1)" and
    2.50    DBPass_def:     "DBPass   == ACT  Deq inp q1 mid
    2.51                                   & (q2$ = $q2 @ [ mid$ ])
    2.52 -                                 & (out$ = $out)"
    2.53 -  DBNext_def:     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)"
    2.54 +                                 & (out$ = $out)" and
    2.55 +  DBNext_def:     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)" and
    2.56    DBuffer_def:    "DBuffer  == TEMP Init DBInit
    2.57                                   & [][DBNext]_(inp,mid,out,q1,q2)
    2.58                                   & WF(DBDeq)_(inp,mid,out,q1,q2)
     3.1 --- a/src/HOL/TLA/Inc/Inc.thy	Wed May 23 16:22:27 2012 +0200
     3.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Wed May 23 16:53:12 2012 +0200
     3.3 @@ -11,72 +11,71 @@
     3.4  (* program counter as an enumeration type *)
     3.5  datatype pcount = a | b | g
     3.6  
     3.7 -consts
     3.8 +axiomatization
     3.9    (* program variables *)
    3.10 -  x :: "nat stfun"
    3.11 -  y :: "nat stfun"
    3.12 -  sem :: "nat stfun"
    3.13 -  pc1 :: "pcount stfun"
    3.14 -  pc2 :: "pcount stfun"
    3.15 +  x :: "nat stfun" and
    3.16 +  y :: "nat stfun" and
    3.17 +  sem :: "nat stfun" and
    3.18 +  pc1 :: "pcount stfun" and
    3.19 +  pc2 :: "pcount stfun" and
    3.20  
    3.21    (* names of actions and predicates *)
    3.22 -  M1 :: action
    3.23 -  M2 :: action
    3.24 -  N1 :: action
    3.25 -  N2 :: action
    3.26 -  alpha1 :: action
    3.27 -  alpha2 :: action
    3.28 -  beta1 :: action
    3.29 -  beta2 :: action
    3.30 -  gamma1 :: action
    3.31 -  gamma2 :: action
    3.32 -  InitPhi :: stpred
    3.33 -  InitPsi :: stpred
    3.34 -  PsiInv :: stpred
    3.35 -  PsiInv1 :: stpred
    3.36 -  PsiInv2 :: stpred
    3.37 -  PsiInv3 :: stpred
    3.38 +  M1 :: action and
    3.39 +  M2 :: action and
    3.40 +  N1 :: action and
    3.41 +  N2 :: action and
    3.42 +  alpha1 :: action and
    3.43 +  alpha2 :: action and
    3.44 +  beta1 :: action and
    3.45 +  beta2 :: action and
    3.46 +  gamma1 :: action and
    3.47 +  gamma2 :: action and
    3.48 +  InitPhi :: stpred and
    3.49 +  InitPsi :: stpred and
    3.50 +  PsiInv :: stpred and
    3.51 +  PsiInv1 :: stpred and
    3.52 +  PsiInv2 :: stpred and
    3.53 +  PsiInv3 :: stpred and
    3.54  
    3.55    (* temporal formulas *)
    3.56 -  Phi :: temporal
    3.57 +  Phi :: temporal and
    3.58    Psi :: temporal
    3.59 -
    3.60 -axioms
    3.61 +where
    3.62    (* the "base" variables, required to compute enabledness predicates *)
    3.63 -  Inc_base:      "basevars (x, y, sem, pc1, pc2)"
    3.64 +  Inc_base:      "basevars (x, y, sem, pc1, pc2)" and
    3.65  
    3.66    (* definitions for high-level program *)
    3.67 -  InitPhi_def:   "InitPhi == PRED x = # 0 & y = # 0"
    3.68 -  M1_def:        "M1      == ACT  x$ = Suc<$x> & y$ = $y"
    3.69 -  M2_def:        "M2      == ACT  y$ = Suc<$y> & x$ = $x"
    3.70 +  InitPhi_def:   "InitPhi == PRED x = # 0 & y = # 0" and
    3.71 +  M1_def:        "M1      == ACT  x$ = Suc<$x> & y$ = $y" and
    3.72 +  M2_def:        "M2      == ACT  y$ = Suc<$y> & x$ = $x" and
    3.73    Phi_def:       "Phi     == TEMP Init InitPhi & [][M1 | M2]_(x,y)
    3.74 -                                 & WF(M1)_(x,y) & WF(M2)_(x,y)"
    3.75 +                                 & WF(M1)_(x,y) & WF(M2)_(x,y)" and
    3.76  
    3.77    (* definitions for low-level program *)
    3.78    InitPsi_def:   "InitPsi == PRED pc1 = #a & pc2 = #a
    3.79 -                                 & x = # 0 & y = # 0 & sem = # 1"
    3.80 +                                 & x = # 0 & y = # 0 & sem = # 1" and
    3.81    alpha1_def:    "alpha1  == ACT  $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
    3.82 -                                 & unchanged(x,y,pc2)"
    3.83 +                                 & unchanged(x,y,pc2)" and
    3.84    alpha2_def:    "alpha2  == ACT  $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
    3.85 -                                 & unchanged(x,y,pc1)"
    3.86 +                                 & unchanged(x,y,pc1)" and
    3.87    beta1_def:     "beta1   == ACT  $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
    3.88 -                                 & unchanged(y,sem,pc2)"
    3.89 +                                 & unchanged(y,sem,pc2)" and
    3.90    beta2_def:     "beta2   == ACT  $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
    3.91 -                                 & unchanged(x,sem,pc1)"
    3.92 +                                 & unchanged(x,sem,pc1)" and
    3.93    gamma1_def:    "gamma1  == ACT  $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
    3.94 -                                 & unchanged(x,y,pc2)"
    3.95 +                                 & unchanged(x,y,pc2)" and
    3.96    gamma2_def:    "gamma2  == ACT  $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
    3.97 -                                 & unchanged(x,y,pc1)"
    3.98 -  N1_def:        "N1      == ACT  (alpha1 | beta1 | gamma1)"
    3.99 -  N2_def:        "N2      == ACT  (alpha2 | beta2 | gamma2)"
   3.100 +                                 & unchanged(x,y,pc1)" and
   3.101 +  N1_def:        "N1      == ACT  (alpha1 | beta1 | gamma1)" and
   3.102 +  N2_def:        "N2      == ACT  (alpha2 | beta2 | gamma2)" and
   3.103    Psi_def:       "Psi     == TEMP Init InitPsi
   3.104                                 & [][N1 | N2]_(x,y,sem,pc1,pc2)
   3.105                                 & SF(N1)_(x,y,sem,pc1,pc2)
   3.106 -                               & SF(N2)_(x,y,sem,pc1,pc2)"
   3.107 +                               & SF(N2)_(x,y,sem,pc1,pc2)" and
   3.108  
   3.109 -  PsiInv1_def:  "PsiInv1  == PRED sem = # 1 & pc1 = #a & pc2 = #a"
   3.110 -  PsiInv2_def:  "PsiInv2  == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
   3.111 -  PsiInv3_def:  "PsiInv3  == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
   3.112 +  PsiInv1_def:  "PsiInv1  == PRED sem = # 1 & pc1 = #a & pc2 = #a" and
   3.113 +  PsiInv2_def:  "PsiInv2  == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" and
   3.114 +  PsiInv3_def:  "PsiInv3  == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" and
   3.115    PsiInv_def:   "PsiInv   == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
   3.116  
   3.117  
     4.1 --- a/src/HOL/TLA/Memory/MemoryParameters.thy	Wed May 23 16:22:27 2012 +0200
     4.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Wed May 23 16:53:12 2012 +0200
     4.3 @@ -25,14 +25,14 @@
     4.4    (* the initial value stored in each memory cell *)
     4.5    InitVal        :: "Vals"
     4.6  
     4.7 -axioms
     4.8 +axiomatization where
     4.9    (* basic assumptions about the above constants and predicates *)
    4.10 -  BadArgNoMemVal:    "BadArg ~: MemVal"
    4.11 -  MemFailNoMemVal:   "MemFailure ~: MemVal"
    4.12 -  InitValMemVal:     "InitVal : MemVal"
    4.13 -  NotAResultNotVal:  "NotAResult ~: MemVal"
    4.14 -  NotAResultNotOK:   "NotAResult ~= OK"
    4.15 -  NotAResultNotBA:   "NotAResult ~= BadArg"
    4.16 +  BadArgNoMemVal:    "BadArg ~: MemVal" and
    4.17 +  MemFailNoMemVal:   "MemFailure ~: MemVal" and
    4.18 +  InitValMemVal:     "InitVal : MemVal" and
    4.19 +  NotAResultNotVal:  "NotAResult ~: MemVal" and
    4.20 +  NotAResultNotOK:   "NotAResult ~= OK" and
    4.21 +  NotAResultNotBA:   "NotAResult ~= BadArg" and
    4.22    NotAResultNotMF:   "NotAResult ~= MemFailure"
    4.23  
    4.24  lemmas [simp] =
     5.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Wed May 23 16:22:27 2012 +0200
     5.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Wed May 23 16:53:12 2012 +0200
     5.3 @@ -28,11 +28,11 @@
     5.4    IsLegalRcvArg  :: "rpcOp => bool"
     5.5    RPCRelayArg    :: "rpcOp => memOp"
     5.6  
     5.7 -axioms
     5.8 +axiomatization where
     5.9    (* RPCFailure is different from MemVals and exceptions *)
    5.10 -  RFNoMemVal:        "RPCFailure ~: MemVal"
    5.11 -  NotAResultNotRF:   "NotAResult ~= RPCFailure"
    5.12 -  OKNotRF:           "OK ~= RPCFailure"
    5.13 +  RFNoMemVal:        "RPCFailure ~: MemVal" and
    5.14 +  NotAResultNotRF:   "NotAResult ~= RPCFailure" and
    5.15 +  OKNotRF:           "OK ~= RPCFailure" and
    5.16    BANotRF:           "BadArg ~= RPCFailure"
    5.17  
    5.18  defs
     6.1 --- a/src/HOL/TLA/TLA.thy	Wed May 23 16:22:27 2012 +0200
     6.2 +++ b/src/HOL/TLA/TLA.thy	Wed May 23 16:53:12 2012 +0200
     6.3 @@ -64,34 +64,39 @@
     6.4    "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
     6.5    "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
     6.6  
     6.7 -axioms
     6.8 +axiomatization where
     6.9    (* Definitions of derived operators *)
    6.10 -  dmd_def:      "TEMP <>F  ==  TEMP ~[]~F"
    6.11 -  boxInit:      "TEMP []F  ==  TEMP []Init F"
    6.12 -  leadsto_def:  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
    6.13 -  stable_def:   "TEMP stable P  ==  TEMP []($P --> P$)"
    6.14 -  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
    6.15 -  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
    6.16 +  dmd_def:      "\<And>F. TEMP <>F  ==  TEMP ~[]~F"
    6.17 +
    6.18 +axiomatization where
    6.19 +  boxInit:      "\<And>F. TEMP []F  ==  TEMP []Init F" and
    6.20 +  leadsto_def:  "\<And>F G. TEMP F ~> G  ==  TEMP [](Init F --> <>G)" and
    6.21 +  stable_def:   "\<And>P. TEMP stable P  ==  TEMP []($P --> P$)" and
    6.22 +  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v" and
    6.23 +  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v" and
    6.24    aall_def:     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
    6.25  
    6.26 +axiomatization where
    6.27  (* Base axioms for raw TLA. *)
    6.28 -  normalT:    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
    6.29 -  reflT:      "|- []F --> F"         (* F::temporal *)
    6.30 -  transT:     "|- []F --> [][]F"     (* polymorphic *)
    6.31 -  linT:       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
    6.32 -  discT:      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
    6.33 -  primeI:     "|- []P --> Init P`"
    6.34 -  primeE:     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
    6.35 -  indT:       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
    6.36 -  allT:       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
    6.37 +  normalT:    "\<And>F G. |- [](F --> G) --> ([]F --> []G)" and    (* polymorphic *)
    6.38 +  reflT:      "\<And>F. |- []F --> F" and         (* F::temporal *)
    6.39 +  transT:     "\<And>F. |- []F --> [][]F" and     (* polymorphic *)
    6.40 +  linT:       "\<And>F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and
    6.41 +  discT:      "\<And>F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and
    6.42 +  primeI:     "\<And>P. |- []P --> Init P`" and
    6.43 +  primeE:     "\<And>P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and
    6.44 +  indT:       "\<And>P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and
    6.45 +  allT:       "\<And>F. |- (ALL x. [](F x)) = ([](ALL x. F x))"
    6.46  
    6.47 -  necT:       "|- F ==> |- []F"      (* polymorphic *)
    6.48 +axiomatization where
    6.49 +  necT:       "\<And>F. |- F ==> |- []F"      (* polymorphic *)
    6.50  
    6.51 +axiomatization where
    6.52  (* Flexible quantification: refinement mappings, history variables *)
    6.53 -  eexI:       "|- F x --> (EEX x. F x)"
    6.54 +  eexI:       "|- F x --> (EEX x. F x)" and
    6.55    eexE:       "[| sigma |= (EEX x. F x); basevars vs;
    6.56                   (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
    6.57 -              |] ==> G sigma"
    6.58 +              |] ==> G sigma" and
    6.59    history:    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
    6.60  
    6.61