src/HOL/TLA/Memory/ProcedureInterface.thy
changeset 62145 5b946c81dfbf
parent 60592 c9bd1d902f04
child 62146 324bc1ffba12
     1.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -16,65 +16,78 @@
     1.4    *)
     1.5  type_synonym ('a,'r) channel =" (PrIds \<Rightarrow> ('a,'r) chan) stfun"
     1.6  
     1.7 +
     1.8 +(* data-level functions *)
     1.9 +
    1.10  consts
    1.11 -  (* data-level functions *)
    1.12    cbit          :: "('a,'r) chan \<Rightarrow> bit"
    1.13    rbit          :: "('a,'r) chan \<Rightarrow> bit"
    1.14    arg           :: "('a,'r) chan \<Rightarrow> 'a"
    1.15    res           :: "('a,'r) chan \<Rightarrow> 'r"
    1.16  
    1.17 -  (* state functions *)
    1.18 -  caller        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
    1.19 -  rtrner        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
    1.20 +
    1.21 +(* state functions *)
    1.22  
    1.23 -  (* state predicates *)
    1.24 -  Calling   :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
    1.25 +definition caller :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
    1.26 +  where "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
    1.27  
    1.28 -  (* actions *)
    1.29 -  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
    1.30 -  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
    1.31 +definition rtrner :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
    1.32 +  where "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))"
    1.33 +
    1.34  
    1.35 -  (* temporal formulas *)
    1.36 -  PLegalCaller      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
    1.37 -  LegalCaller       :: "('a,'r) channel \<Rightarrow> temporal"
    1.38 -  PLegalReturner    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
    1.39 -  LegalReturner     :: "('a,'r) channel \<Rightarrow> temporal"
    1.40 +(* slice through array-valued state function *)
    1.41  
    1.42 -  (* slice through array-valued state function *)
    1.43 +consts
    1.44    slice        :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
    1.45 -
    1.46  syntax
    1.47    "_slice"    :: "[lift, 'a] \<Rightarrow> lift"      ("(_!_)" [70,70] 70)
    1.48 -
    1.49 -  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
    1.50 -  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
    1.51 -
    1.52  translations
    1.53    "_slice"  ==  "CONST slice"
    1.54 -
    1.55 -  "_Call"   ==  "CONST ACall"
    1.56 -  "_Return" ==  "CONST AReturn"
    1.57 -
    1.58  defs
    1.59    slice_def:     "(PRED (x!i)) s == x s i"
    1.60  
    1.61 -  caller_def:    "caller ch   == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
    1.62 -  rtrner_def:    "rtrner ch   == \<lambda>s p. (rbit (ch s p), res (ch s p))"
    1.63 +
    1.64 +(* state predicates *)
    1.65 +
    1.66 +definition Calling :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
    1.67 +  where "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
    1.68 +
    1.69 +
    1.70 +(* actions *)
    1.71  
    1.72 -  Calling_def:   "Calling ch p  == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
    1.73 +consts
    1.74 +  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
    1.75 +  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
    1.76 +syntax
    1.77 +  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
    1.78 +  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
    1.79 +translations
    1.80 +  "_Call"   ==  "CONST ACall"
    1.81 +  "_Return" ==  "CONST AReturn"
    1.82 +defs
    1.83    Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
    1.84                                       \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
    1.85                                       \<and> (arg<ch!p>$ = $v)"
    1.86    Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
    1.87                                       \<and> (rbit<ch!p>$ = $cbit<ch!p>)
    1.88                                       \<and> (res<ch!p>$ = $v)"
    1.89 -  PLegalCaller_def:      "PLegalCaller ch p == TEMP
    1.90 -                             Init(\<not> Calling ch p)
    1.91 -                             \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
    1.92 -  LegalCaller_def:       "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
    1.93 -  PLegalReturner_def:    "PLegalReturner ch p == TEMP
    1.94 -                                \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
    1.95 -  LegalReturner_def:     "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
    1.96 +
    1.97 +
    1.98 +(* temporal formulas *)
    1.99 +
   1.100 +definition PLegalCaller :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
   1.101 +  where "PLegalCaller ch p == TEMP
   1.102 +     Init(\<not> Calling ch p)
   1.103 +     \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
   1.104 +
   1.105 +definition LegalCaller :: "('a,'r) channel \<Rightarrow> temporal"
   1.106 +  where "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
   1.107 +
   1.108 +definition PLegalReturner :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
   1.109 +  where "PLegalReturner ch p == TEMP \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
   1.110 +
   1.111 +definition LegalReturner :: "('a,'r) channel \<Rightarrow> temporal"
   1.112 +  where "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
   1.113  
   1.114  declare slice_def [simp]
   1.115