eliminated old defs;
authorwenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 621455b946c81dfbf
parent 62144 bdab93ccfaf8
child 62146 324bc1ffba12
eliminated old defs;
src/HOL/Auth/All_Symmetric.thy
src/HOL/Bali/Example.thy
src/HOL/IMPP/EvenOdd.thy
src/HOL/IMPP/Misc.thy
src/HOL/IOA/Asig.thy
src/HOL/IOA/IOA.thy
src/HOL/Library/Old_Datatype.thy
src/HOL/MicroJava/DFA/Semilat.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Nominal/Nominal.thy
src/HOL/TLA/Buffer/Buffer.thy
src/HOL/TLA/Init.thy
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/Memory/RPC.thy
src/HOL/TLA/Memory/RPCParameters.thy
src/HOL/TLA/Stfun.thy
src/HOL/ex/MT.thy
     1.1 --- a/src/HOL/Auth/All_Symmetric.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/Auth/All_Symmetric.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -4,7 +4,10 @@
     1.4  
     1.5  text \<open>All keys are symmetric\<close>
     1.6  
     1.7 -defs all_symmetric_def: "all_symmetric \<equiv> True"
     1.8 +overloading all_symmetric \<equiv> all_symmetric
     1.9 +begin
    1.10 +  definition "all_symmetric \<equiv> True"
    1.11 +end
    1.12  
    1.13  lemma isSym_keys: "K \<in> symKeys"
    1.14    by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
     2.1 --- a/src/HOL/Bali/Example.thy	Mon Jan 11 21:20:44 2016 +0100
     2.2 +++ b/src/HOL/Bali/Example.thy	Mon Jan 11 21:21:02 2016 +0100
     2.3 @@ -141,12 +141,16 @@
     2.4  lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
     2.5  by (simp add: SXcpt_def)
     2.6  
     2.7 +
     2.8  subsubsection "classes and interfaces"
     2.9  
    2.10 -defs
    2.11 -
    2.12 -  Object_mdecls_def: "Object_mdecls \<equiv> []"
    2.13 -  SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
    2.14 +overloading
    2.15 +  Object_mdecls \<equiv> Object_mdecls
    2.16 +  SXcpt_mdecls \<equiv> SXcpt_mdecls
    2.17 +begin
    2.18 +  definition "Object_mdecls \<equiv> []"
    2.19 +  definition "SXcpt_mdecls  \<equiv> []"
    2.20 +end
    2.21  
    2.22  axiomatization  
    2.23    foo    :: mname
     3.1 --- a/src/HOL/IMPP/EvenOdd.thy	Mon Jan 11 21:20:44 2016 +0100
     3.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Mon Jan 11 21:21:02 2016 +0100
     3.3 @@ -29,8 +29,10 @@
     3.4           THEN Loc Res:==(%s. 1)
     3.5           ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
     3.6  
     3.7 -defs
     3.8 -  bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
     3.9 +overloading bodies \<equiv> bodies
    3.10 +begin
    3.11 +  definition "bodies == [(Even,evn),(Odd,odd)]"
    3.12 +end
    3.13  
    3.14  definition
    3.15    Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
     4.1 --- a/src/HOL/IMPP/Misc.thy	Mon Jan 11 21:20:44 2016 +0100
     4.2 +++ b/src/HOL/IMPP/Misc.thy	Mon Jan 11 21:21:02 2016 +0100
     4.3 @@ -8,13 +8,29 @@
     4.4  imports Hoare
     4.5  begin
     4.6  
     4.7 -defs
     4.8 -  newlocs_def: "newlocs       == %x. undefined"
     4.9 -  setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
    4.10 -  getlocs_def: "getlocs s     == case s of st g l => l"
    4.11 -   update_def: "update s vn v == case vn of
    4.12 -                               Glb gn => (case s of st g l => st (g(gn:=v)) l)
    4.13 -                             | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    4.14 +overloading
    4.15 +  newlocs \<equiv> newlocs
    4.16 +  setlocs \<equiv> setlocs
    4.17 +  getlocs \<equiv> getlocs
    4.18 +  update \<equiv> update
    4.19 +begin
    4.20 +
    4.21 +definition newlocs :: locals
    4.22 +  where "newlocs == %x. undefined"
    4.23 +
    4.24 +definition setlocs :: "state => locals => state"
    4.25 +  where "setlocs s l' == case s of st g l => st g l'"
    4.26 +
    4.27 +definition getlocs :: "state => locals"
    4.28 +  where "getlocs s == case s of st g l => l"
    4.29 +
    4.30 +definition update  :: "state => vname => val => state"
    4.31 +  where "update s vn v ==
    4.32 +    case vn of
    4.33 +      Glb gn => (case s of st g l => st (g(gn:=v)) l)
    4.34 +    | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    4.35 +
    4.36 +end
    4.37  
    4.38  
    4.39  subsection "state access"
     5.1 --- a/src/HOL/IOA/Asig.thy	Mon Jan 11 21:20:44 2016 +0100
     5.2 +++ b/src/HOL/IOA/Asig.thy	Mon Jan 11 21:21:02 2016 +0100
     5.3 @@ -9,41 +9,31 @@
     5.4  imports Main
     5.5  begin
     5.6  
     5.7 -type_synonym
     5.8 -  'a signature = "('a set * 'a set * 'a set)"
     5.9 +type_synonym 'a signature = "('a set * 'a set * 'a set)"
    5.10 +
    5.11 +definition "inputs" :: "'action signature => 'action set"
    5.12 +  where asig_inputs_def: "inputs == fst"
    5.13  
    5.14 -consts
    5.15 -  "actions" :: "'action signature => 'action set"
    5.16 -  "inputs" :: "'action signature => 'action set"
    5.17 -  "outputs" :: "'action signature => 'action set"
    5.18 -  "internals" :: "'action signature => 'action set"
    5.19 -  externals :: "'action signature => 'action set"
    5.20 +definition "outputs" :: "'action signature => 'action set"
    5.21 +  where asig_outputs_def: "outputs == (fst o snd)"
    5.22  
    5.23 -  is_asig       ::"'action signature => bool"
    5.24 -  mk_ext_asig   ::"'action signature => 'action signature"
    5.25 -
    5.26 -
    5.27 -defs
    5.28 +definition "internals" :: "'action signature => 'action set"
    5.29 +  where asig_internals_def: "internals == (snd o snd)"
    5.30  
    5.31 -asig_inputs_def:    "inputs == fst"
    5.32 -asig_outputs_def:   "outputs == (fst o snd)"
    5.33 -asig_internals_def: "internals == (snd o snd)"
    5.34 +definition "actions" :: "'action signature => 'action set"
    5.35 +  where actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    5.36  
    5.37 -actions_def:
    5.38 -   "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    5.39 -
    5.40 -externals_def:
    5.41 -   "externals(asig) == (inputs(asig) Un outputs(asig))"
    5.42 +definition externals :: "'action signature => 'action set"
    5.43 +  where externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))"
    5.44  
    5.45 -is_asig_def:
    5.46 -  "is_asig(triple) ==
    5.47 -      ((inputs(triple) Int outputs(triple) = {})    &
    5.48 -       (outputs(triple) Int internals(triple) = {}) &
    5.49 -       (inputs(triple) Int internals(triple) = {}))"
    5.50 +definition is_asig :: "'action signature => bool"
    5.51 +  where "is_asig(triple) ==
    5.52 +    ((inputs(triple) Int outputs(triple) = {})    &
    5.53 +     (outputs(triple) Int internals(triple) = {}) &
    5.54 +     (inputs(triple) Int internals(triple) = {}))"
    5.55  
    5.56 -
    5.57 -mk_ext_asig_def:
    5.58 -  "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    5.59 +definition mk_ext_asig :: "'action signature => 'action signature"
    5.60 +  where "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    5.61  
    5.62  
    5.63  lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
     6.1 --- a/src/HOL/IOA/IOA.thy	Mon Jan 11 21:20:44 2016 +0100
     6.2 +++ b/src/HOL/IOA/IOA.thy	Mon Jan 11 21:21:02 2016 +0100
     6.3 @@ -15,183 +15,148 @@
     6.4  type_synonym ('a, 's) transition = "('s * 'a * 's)"
     6.5  type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
     6.6  
     6.7 -consts
     6.8 +(* IO automata *)
     6.9 +
    6.10 +definition state_trans :: "['action signature, ('action,'state)transition set] => bool"
    6.11 +  where "state_trans asig R ==
    6.12 +     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
    6.13 +     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
    6.14 +
    6.15 +definition asig_of :: "('action,'state)ioa => 'action signature"
    6.16 +  where "asig_of == fst"
    6.17  
    6.18 -  (* IO automata *)
    6.19 -  state_trans::"['action signature, ('action,'state)transition set] => bool"
    6.20 -  asig_of    ::"('action,'state)ioa => 'action signature"
    6.21 -  starts_of  ::"('action,'state)ioa => 'state set"
    6.22 -  trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
    6.23 -  IOA        ::"('action,'state)ioa => bool"
    6.24 +definition starts_of :: "('action,'state)ioa => 'state set"
    6.25 +  where "starts_of == (fst o snd)"
    6.26 +
    6.27 +definition trans_of :: "('action,'state)ioa => ('action,'state)transition set"
    6.28 +  where "trans_of == (snd o snd)"
    6.29  
    6.30 -  (* Executions, schedules, and traces *)
    6.31 +definition IOA :: "('action,'state)ioa => bool"
    6.32 +  where "IOA(ioa) == (is_asig(asig_of(ioa)) &
    6.33 +                (~ starts_of(ioa) = {}) &
    6.34 +                state_trans (asig_of ioa) (trans_of ioa))"
    6.35 +
    6.36 +
    6.37 +(* Executions, schedules, and traces *)
    6.38  
    6.39 -  is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool"
    6.40 -  has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
    6.41 -  executions    :: "('action,'state)ioa => ('action,'state)execution set"
    6.42 -  mk_trace  :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
    6.43 -  reachable     :: "[('action,'state)ioa, 'state] => bool"
    6.44 -  invariant     :: "[('action,'state)ioa, 'state=>bool] => bool"
    6.45 -  has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
    6.46 -  traces    :: "('action,'state)ioa => 'action oseq set"
    6.47 -  NF            :: "'a oseq => 'a oseq"
    6.48 +(* An execution fragment is modelled with a pair of sequences:
    6.49 +   the first is the action options, the second the state sequence.
    6.50 +   Finite executions have None actions from some point on. *)
    6.51 +definition is_execution_fragment :: "[('action,'state)ioa, ('action,'state)execution] => bool"
    6.52 +  where "is_execution_fragment A ex ==
    6.53 +     let act = fst(ex); state = snd(ex)
    6.54 +     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
    6.55 +              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
    6.56 +
    6.57 +definition executions :: "('action,'state)ioa => ('action,'state)execution set"
    6.58 +  where "executions(ioa) == {e. snd e 0:starts_of(ioa) & is_execution_fragment ioa e}"
    6.59  
    6.60 -  (* Composition of action signatures and automata *)
    6.61 +
    6.62 +definition reachable :: "[('action,'state)ioa, 'state] => bool"
    6.63 +  where "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
    6.64 +
    6.65 +definition invariant :: "[('action,'state)ioa, 'state=>bool] => bool"
    6.66 +  where "invariant A P == (!s. reachable A s --> P(s))"
    6.67 +
    6.68 +
    6.69 +(* Composition of action signatures and automata *)
    6.70 +
    6.71 +consts
    6.72    compatible_asigs ::"('a => 'action signature) => bool"
    6.73    asig_composition ::"('a => 'action signature) => 'action signature"
    6.74    compatible_ioas  ::"('a => ('action,'state)ioa) => bool"
    6.75    ioa_composition  ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"
    6.76  
    6.77 -  (* binary composition of action signatures and automata *)
    6.78 -  compat_asigs ::"['action signature, 'action signature] => bool"
    6.79 -  asig_comp    ::"['action signature, 'action signature] => 'action signature"
    6.80 -  compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
    6.81 -  par         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
    6.82 +
    6.83 +(* binary composition of action signatures and automata *)
    6.84  
    6.85 -  (* Filtering and hiding *)
    6.86 -  filter_oseq  :: "('a => bool) => 'a oseq => 'a oseq"
    6.87 +definition compat_asigs ::"['action signature, 'action signature] => bool"
    6.88 +  where "compat_asigs a1 a2 ==
    6.89 +   (((outputs(a1) Int outputs(a2)) = {}) &
    6.90 +    ((internals(a1) Int actions(a2)) = {}) &
    6.91 +    ((internals(a2) Int actions(a1)) = {}))"
    6.92  
    6.93 -  restrict_asig :: "['a signature, 'a set] => 'a signature"
    6.94 -  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
    6.95 +definition compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
    6.96 +  where "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
    6.97  
    6.98 -  (* Notions of correctness *)
    6.99 -  ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
   6.100 -
   6.101 -  (* Instantiation of abstract IOA by concrete actions *)
   6.102 -  rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
   6.103 +definition asig_comp :: "['action signature, 'action signature] => 'action signature"
   6.104 +  where "asig_comp a1 a2 ==
   6.105 +      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
   6.106 +        (outputs(a1) Un outputs(a2)),
   6.107 +        (internals(a1) Un internals(a2))))"
   6.108  
   6.109 -defs
   6.110 -
   6.111 -state_trans_def:
   6.112 -  "state_trans asig R ==
   6.113 -     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
   6.114 -     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
   6.115 +definition par :: "[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
   6.116 +  where "(ioa1 || ioa2) ==
   6.117 +     (asig_comp (asig_of ioa1) (asig_of ioa2),
   6.118 +      {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
   6.119 +      {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
   6.120 +           in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
   6.121 +              (if a:actions(asig_of(ioa1)) then
   6.122 +                 (fst(s),a,fst(t)):trans_of(ioa1)
   6.123 +               else fst(t) = fst(s))
   6.124 +              &
   6.125 +              (if a:actions(asig_of(ioa2)) then
   6.126 +                 (snd(s),a,snd(t)):trans_of(ioa2)
   6.127 +               else snd(t) = snd(s))})"
   6.128  
   6.129  
   6.130 -asig_of_def:   "asig_of == fst"
   6.131 -starts_of_def: "starts_of == (fst o snd)"
   6.132 -trans_of_def:  "trans_of == (snd o snd)"
   6.133 -
   6.134 -ioa_def:
   6.135 -  "IOA(ioa) == (is_asig(asig_of(ioa))      &
   6.136 -                (~ starts_of(ioa) = {})    &
   6.137 -                state_trans (asig_of ioa) (trans_of ioa))"
   6.138 -
   6.139 -
   6.140 -(* An execution fragment is modelled with a pair of sequences:
   6.141 - * the first is the action options, the second the state sequence.
   6.142 - * Finite executions have None actions from some point on.
   6.143 - *******)
   6.144 -is_execution_fragment_def:
   6.145 -  "is_execution_fragment A ex ==
   6.146 -     let act = fst(ex); state = snd(ex)
   6.147 -     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
   6.148 -              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
   6.149 -
   6.150 -
   6.151 -executions_def:
   6.152 -  "executions(ioa) == {e. snd e 0:starts_of(ioa) &
   6.153 -                        is_execution_fragment ioa e}"
   6.154 -
   6.155 -
   6.156 -reachable_def:
   6.157 -  "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
   6.158 -
   6.159 -
   6.160 -invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
   6.161 -
   6.162 +(* Filtering and hiding *)
   6.163  
   6.164  (* Restrict the trace to those members of the set s *)
   6.165 -filter_oseq_def:
   6.166 -  "filter_oseq p s ==
   6.167 +definition filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
   6.168 +  where "filter_oseq p s ==
   6.169     (%i. case s(i)
   6.170           of None => None
   6.171            | Some(x) => if p x then Some x else None)"
   6.172  
   6.173 -
   6.174 -mk_trace_def:
   6.175 -  "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
   6.176 -
   6.177 +definition mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
   6.178 +  where "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
   6.179  
   6.180  (* Does an ioa have an execution with the given trace *)
   6.181 -has_trace_def:
   6.182 -  "has_trace ioa b ==
   6.183 -     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
   6.184 +definition has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
   6.185 +  where "has_trace ioa b == (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
   6.186  
   6.187 -normal_form_def:
   6.188 -  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
   6.189 +definition NF :: "'a oseq => 'a oseq"
   6.190 +  where "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
   6.191                      (!j. j ~: range(f) --> nf(j)= None) &
   6.192 -                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
   6.193 +                    (!i. nf(i)=None --> (nf (Suc i)) = None)"
   6.194  
   6.195  (* All the traces of an ioa *)
   6.196 -
   6.197 -  traces_def:
   6.198 -  "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
   6.199 -
   6.200 -(*
   6.201 -  traces_def:
   6.202 -  "traces(ioa) == {tr. has_trace ioa tr}"
   6.203 -*)
   6.204 -
   6.205 -compat_asigs_def:
   6.206 -  "compat_asigs a1 a2 ==
   6.207 -   (((outputs(a1) Int outputs(a2)) = {}) &
   6.208 -    ((internals(a1) Int actions(a2)) = {}) &
   6.209 -    ((internals(a2) Int actions(a1)) = {}))"
   6.210 -
   6.211 -
   6.212 -compat_ioas_def:
   6.213 -  "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
   6.214 +definition traces :: "('action,'state)ioa => 'action oseq set"
   6.215 +  where "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
   6.216  
   6.217  
   6.218 -asig_comp_def:
   6.219 -  "asig_comp a1 a2 ==
   6.220 -      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
   6.221 -        (outputs(a1) Un outputs(a2)),
   6.222 -        (internals(a1) Un internals(a2))))"
   6.223 -
   6.224 -
   6.225 -par_def:
   6.226 -  "(ioa1 || ioa2) ==
   6.227 -       (asig_comp (asig_of ioa1) (asig_of ioa2),
   6.228 -        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
   6.229 -        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
   6.230 -             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
   6.231 -                (if a:actions(asig_of(ioa1)) then
   6.232 -                   (fst(s),a,fst(t)):trans_of(ioa1)
   6.233 -                 else fst(t) = fst(s))
   6.234 -                &
   6.235 -                (if a:actions(asig_of(ioa2)) then
   6.236 -                   (snd(s),a,snd(t)):trans_of(ioa2)
   6.237 -                 else snd(t) = snd(s))})"
   6.238 -
   6.239 -
   6.240 -restrict_asig_def:
   6.241 -  "restrict_asig asig actns ==
   6.242 +definition restrict_asig :: "['a signature, 'a set] => 'a signature"
   6.243 +  where "restrict_asig asig actns ==
   6.244      (inputs(asig) Int actns, outputs(asig) Int actns,
   6.245       internals(asig) Un (externals(asig) - actns))"
   6.246  
   6.247 -
   6.248 -restrict_def:
   6.249 -  "restrict ioa actns ==
   6.250 +definition restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
   6.251 +  where "restrict ioa actns ==
   6.252      (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
   6.253  
   6.254  
   6.255 -ioa_implements_def:
   6.256 -  "ioa_implements ioa1 ioa2 ==
   6.257 +
   6.258 +(* Notions of correctness *)
   6.259 +
   6.260 +definition ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
   6.261 +  where "ioa_implements ioa1 ioa2 ==
   6.262    ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
   6.263       (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
   6.264        traces(ioa1) <= traces(ioa2))"
   6.265  
   6.266 -rename_def:
   6.267 -"rename ioa ren ==
   6.268 -  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
   6.269 -    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
   6.270 -    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
   6.271 -              starts_of(ioa)   ,
   6.272 -   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
   6.273 -        in
   6.274 -        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
   6.275 +
   6.276 +(* Instantiation of abstract IOA by concrete actions *)
   6.277 +
   6.278 +definition rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
   6.279 +  where "rename ioa ren ==
   6.280 +    (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
   6.281 +      {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
   6.282 +      {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
   6.283 +                starts_of(ioa)   ,
   6.284 +     {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
   6.285 +          in
   6.286 +          ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
   6.287  
   6.288  
   6.289  declare Let_def [simp]
   6.290 @@ -206,7 +171,7 @@
   6.291  
   6.292  lemma trans_in_actions:
   6.293    "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"
   6.294 -  apply (unfold ioa_def state_trans_def actions_def is_asig_def)
   6.295 +  apply (unfold IOA_def state_trans_def actions_def is_asig_def)
   6.296    apply (erule conjE)+
   6.297    apply (erule allE, erule impE, assumption)
   6.298    apply simp
     7.1 --- a/src/HOL/Library/Old_Datatype.thy	Mon Jan 11 21:20:44 2016 +0100
     7.2 +++ b/src/HOL/Library/Old_Datatype.thy	Mon Jan 11 21:21:02 2016 +0100
     7.3 @@ -26,80 +26,67 @@
     7.4  type_synonym 'a item        = "('a, unit) node set"
     7.5  type_synonym ('a, 'b) dtree = "('a, 'b) node set"
     7.6  
     7.7 -consts
     7.8 -  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
     7.9 -
    7.10 -  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    7.11 -  ndepth    :: "('a, 'b) node => nat"
    7.12 +definition Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
    7.13 +  (*crude "lists" of nats -- needed for the constructions*)
    7.14 +  where "Push == (%b h. case_nat b h)"
    7.15  
    7.16 -  Atom      :: "('a + nat) => ('a, 'b) dtree"
    7.17 -  Leaf      :: "'a => ('a, 'b) dtree"
    7.18 -  Numb      :: "nat => ('a, 'b) dtree"
    7.19 -  Scons     :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
    7.20 -  In0       :: "('a, 'b) dtree => ('a, 'b) dtree"
    7.21 -  In1       :: "('a, 'b) dtree => ('a, 'b) dtree"
    7.22 -  Lim       :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
    7.23 -
    7.24 -  ntrunc    :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
    7.25 -
    7.26 -  uprod     :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    7.27 -  usum      :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    7.28 -
    7.29 -  Split     :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
    7.30 -  Case      :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
    7.31 -
    7.32 -  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
    7.33 -                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    7.34 -  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
    7.35 -                => (('a, 'b) dtree * ('a, 'b) dtree)set"
    7.36 +definition Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    7.37 +  where "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    7.38  
    7.39  
    7.40 -defs
    7.41 +(** operations on S-expressions -- sets of nodes **)
    7.42  
    7.43 -  Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    7.44 -
    7.45 -  (*crude "lists" of nats -- needed for the constructions*)
    7.46 -  Push_def:   "Push == (%b h. case_nat b h)"
    7.47 +(*S-expression constructors*)
    7.48 +definition Atom :: "('a + nat) => ('a, 'b) dtree"
    7.49 +  where "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
    7.50 +definition Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
    7.51 +  where "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
    7.52  
    7.53 -  (** operations on S-expressions -- sets of nodes **)
    7.54 +(*Leaf nodes, with arbitrary or nat labels*)
    7.55 +definition Leaf :: "'a => ('a, 'b) dtree"
    7.56 +  where "Leaf == Atom o Inl"
    7.57 +definition Numb :: "nat => ('a, 'b) dtree"
    7.58 +  where "Numb == Atom o Inr"
    7.59  
    7.60 -  (*S-expression constructors*)
    7.61 -  Atom_def:   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
    7.62 -  Scons_def:  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
    7.63 -
    7.64 -  (*Leaf nodes, with arbitrary or nat labels*)
    7.65 -  Leaf_def:   "Leaf == Atom o Inl"
    7.66 -  Numb_def:   "Numb == Atom o Inr"
    7.67 +(*Injections of the "disjoint sum"*)
    7.68 +definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
    7.69 +  where "In0(M) == Scons (Numb 0) M"
    7.70 +definition In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
    7.71 +  where "In1(M) == Scons (Numb 1) M"
    7.72  
    7.73 -  (*Injections of the "disjoint sum"*)
    7.74 -  In0_def:    "In0(M) == Scons (Numb 0) M"
    7.75 -  In1_def:    "In1(M) == Scons (Numb 1) M"
    7.76 +(*Function spaces*)
    7.77 +definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
    7.78 +  where "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
    7.79  
    7.80 -  (*Function spaces*)
    7.81 -  Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
    7.82 +(*the set of nodes with depth less than k*)
    7.83 +definition ndepth :: "('a, 'b) node => nat"
    7.84 +  where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
    7.85 +definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
    7.86 +  where "ntrunc k N == {n. n:N & ndepth(n)<k}"
    7.87  
    7.88 -  (*the set of nodes with depth less than k*)
    7.89 -  ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
    7.90 -  ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
    7.91 +(*products and sums for the "universe"*)
    7.92 +definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    7.93 +  where "uprod A B == UN x:A. UN y:B. { Scons x y }"
    7.94 +definition usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    7.95 +  where "usum A B == In0`A Un In1`B"
    7.96  
    7.97 -  (*products and sums for the "universe"*)
    7.98 -  uprod_def:  "uprod A B == UN x:A. UN y:B. { Scons x y }"
    7.99 -  usum_def:   "usum A B == In0`A Un In1`B"
   7.100 +(*the corresponding eliminators*)
   7.101 +definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
   7.102 +  where "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
   7.103  
   7.104 -  (*the corresponding eliminators*)
   7.105 -  Split_def:  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
   7.106 -
   7.107 -  Case_def:   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x))
   7.108 -                                  | (EX y . M = In1(y) & u = d(y))"
   7.109 +definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
   7.110 +  where "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) | (EX y . M = In1(y) & u = d(y))"
   7.111  
   7.112  
   7.113 -  (** equality for the "universe" **)
   7.114 -
   7.115 -  dprod_def:  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
   7.116 +(** equality for the "universe" **)
   7.117  
   7.118 -  dsum_def:   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
   7.119 -                          (UN (y,y'):s. {(In1(y),In1(y'))})"
   7.120 +definition dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
   7.121 +      => (('a, 'b) dtree * ('a, 'b) dtree)set"
   7.122 +  where "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
   7.123  
   7.124 +definition dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
   7.125 +      => (('a, 'b) dtree * ('a, 'b) dtree)set"
   7.126 +  where "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un (UN (y,y'):s. {(In1(y),In1(y'))})"
   7.127  
   7.128  
   7.129  lemma apfst_convE: 
     8.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Mon Jan 11 21:20:44 2016 +0100
     8.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Mon Jan 11 21:21:02 2016 +0100
     8.3 @@ -15,23 +15,26 @@
     8.4  type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     8.5  type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
     8.6  
     8.7 -consts
     8.8 -  "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
     8.9 -  "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    8.10 -  "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" 
    8.11 -(*<*)
    8.12 +definition lesub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    8.13 +  where "lesub x r y \<longleftrightarrow> r x y"
    8.14 +
    8.15 +definition lesssub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    8.16 +  where "lesssub x r y \<longleftrightarrow> lesub x r y \<and> x \<noteq> y"
    8.17 +
    8.18 +definition plussub :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
    8.19 +  where "plussub x f y = f x y"
    8.20 +
    8.21  notation (ASCII)
    8.22    "lesub"  ("(_ /<='__ _)" [50, 1000, 51] 50) and
    8.23    "lesssub"  ("(_ /<'__ _)" [50, 1000, 51] 50) and
    8.24    "plussub"  ("(_ /+'__ _)" [65, 1000, 66] 65)
    8.25 -(*>*)
    8.26 +
    8.27  notation
    8.28    "lesub"  ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
    8.29    "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
    8.30    "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
    8.31 -(*<*)
    8.32 +
    8.33  (* allow \<sub> instead of \<bsub>..\<esub> *)
    8.34 -
    8.35  abbreviation (input)
    8.36    lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
    8.37    where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
    8.38 @@ -43,12 +46,6 @@
    8.39  abbreviation (input)
    8.40    plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
    8.41    where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
    8.42 -(*>*)
    8.43 -
    8.44 -defs
    8.45 -  lesub_def:   "x \<sqsubseteq>\<^sub>r y \<equiv> r x y"
    8.46 -  lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y"
    8.47 -  plussub_def: "x \<squnion>\<^sub>f y \<equiv> f x y"
    8.48  
    8.49  definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where
    8.50    "ord r \<equiv> \<lambda>x y. (x,y) \<in> r"
     9.1 --- a/src/HOL/MicroJava/J/Example.thy	Mon Jan 11 21:20:44 2016 +0100
     9.2 +++ b/src/HOL/MicroJava/J/Example.thy	Mon Jan 11 21:21:02 2016 +0100
     9.3 @@ -82,31 +82,33 @@
     9.4  declare Base_not_Xcpt [symmetric, simp]
     9.5  declare Ext_not_Xcpt  [symmetric, simp]
     9.6  
     9.7 -consts
     9.8 -  foo_Base::  java_mb
     9.9 -  foo_Ext ::  java_mb
    9.10 -  BaseC   :: "java_mb cdecl"
    9.11 -  ExtC    :: "java_mb cdecl"
    9.12 -  test    ::  stmt
    9.13 -  foo   ::  mname
    9.14 -  a   ::  loc
    9.15 -  b       ::  loc
    9.16 +definition foo_Base :: java_mb
    9.17 +  where "foo_Base == ([x],[],Skip,LAcc x)"
    9.18  
    9.19 -defs
    9.20 -  foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
    9.21 -  BaseC_def:"BaseC == (Base, (Object, 
    9.22 +definition foo_Ext :: java_mb
    9.23 +  where "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
    9.24 +               (LAcc x)..vee:=Lit (Intg Numeral1)),
    9.25 +           Lit Null)"
    9.26 +
    9.27 +consts foo ::  mname
    9.28 +
    9.29 +definition BaseC :: "java_mb cdecl"
    9.30 +  where "BaseC == (Base, (Object, 
    9.31             [(vee, PrimT Boolean)], 
    9.32             [((foo,[Class Base]),Class Base,foo_Base)]))"
    9.33 -  foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
    9.34 -               (LAcc x)..vee:=Lit (Intg Numeral1)),
    9.35 -           Lit Null)"
    9.36 -  ExtC_def: "ExtC  == (Ext,  (Base  , 
    9.37 +
    9.38 +definition ExtC :: "java_mb cdecl"
    9.39 +  where "ExtC  == (Ext,  (Base  ,
    9.40             [(vee, PrimT Integer)], 
    9.41             [((foo,[Class Base]),Class Ext,foo_Ext)]))"
    9.42  
    9.43 -  test_def:"test == Expr(e::=NewC Ext);; 
    9.44 +definition test ::  stmt
    9.45 +  where "test == Expr(e::=NewC Ext);;
    9.46                      Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
    9.47  
    9.48 +consts
    9.49 +  a :: loc
    9.50 +  b :: loc
    9.51  
    9.52  abbreviation
    9.53    NP  :: xcpt where
    10.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 11 21:20:44 2016 +0100
    10.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 11 21:21:02 2016 +0100
    10.3 @@ -176,14 +176,18 @@
    10.4      by(rule finite_acyclic_wf_converse[OF finite_subcls1])
    10.5  qed
    10.6  
    10.7 -consts
    10.8 -  "method" :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
    10.9 -  field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
   10.10 -  fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
   10.11 +definition "method" :: "'c prog \<times> cname => (sig \<rightharpoonup> cname \<times> ty \<times> 'c)"
   10.12 +  \<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
   10.13 +  where [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
   10.14 +                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
   10.15  
   10.16 -\<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
   10.17 -defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
   10.18 -                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
   10.19 +definition fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list"
   10.20 +  \<comment> "list of fields of a class, including inherited and hidden ones"
   10.21 +  where [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
   10.22 +                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
   10.23 +
   10.24 +definition field :: "'c prog \<times> cname => (vname \<rightharpoonup> cname \<times> ty)"
   10.25 +  where [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
   10.26  
   10.27  lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   10.28    method (G,C) = (if C = Object then empty else method (G,D)) ++  
   10.29 @@ -194,11 +198,6 @@
   10.30  apply auto
   10.31  done
   10.32  
   10.33 -
   10.34 -\<comment> "list of fields of a class, including inherited and hidden ones"
   10.35 -defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
   10.36 -                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
   10.37 -
   10.38  lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   10.39   fields (G,C) = 
   10.40    map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
   10.41 @@ -208,9 +207,6 @@
   10.42  apply auto
   10.43  done
   10.44  
   10.45 -
   10.46 -defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
   10.47 -
   10.48  lemma field_fields: 
   10.49  "field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
   10.50  apply (unfold field_def)
    11.1 --- a/src/HOL/MicroJava/J/WellType.thy	Mon Jan 11 21:20:44 2016 +0100
    11.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Mon Jan 11 21:21:02 2016 +0100
    11.3 @@ -33,24 +33,20 @@
    11.4    localT :: "'c env => (vname \<rightharpoonup> ty)"
    11.5    where "localT == snd"
    11.6  
    11.7 -consts
    11.8 -  more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
    11.9 -                (ty \<times> 'x) \<times> ty list => bool"
   11.10 -  appl_methds :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
   11.11 -  max_spec :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
   11.12 +definition more_spec :: "'c prog \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> bool"
   11.13 +  where "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
   11.14 +                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
   11.15  
   11.16 -defs
   11.17 -  more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
   11.18 -                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
   11.19 -  
   11.20 +definition appl_methds :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
   11.21    \<comment> "applicable methods, cf. 15.11.2.1"
   11.22 -  appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
   11.23 +  where "appl_methds G C == \<lambda>(mn, pTs).
   11.24                       {((Class md,rT),pTs') |md rT mb pTs'.
   11.25                        method (G,C)  (mn, pTs') = Some (md,rT,mb) \<and>
   11.26                        list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
   11.27  
   11.28 +definition max_spec :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
   11.29    \<comment> "maximally specific methods, cf. 15.11.2.2"
   11.30 -  max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
   11.31 +  where "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
   11.32                                         (\<forall>m'\<in>appl_methds G C sig.
   11.33                                           more_spec G m' m --> m' = m)}"
   11.34  
    12.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Jan 11 21:20:44 2016 +0100
    12.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Jan 11 21:21:02 2016 +0100
    12.3 @@ -1273,10 +1273,20 @@
    12.4  
    12.5  consts inverse :: "'a \<Rightarrow> 'a"
    12.6  
    12.7 -defs (overloaded)
    12.8 -inverse_bool: "inverse (b::bool) \<equiv> \<not> b"
    12.9 -inverse_set: "inverse (S::'a set) \<equiv> -S"
   12.10 -inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
   12.11 +overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
   12.12 +begin
   12.13 +  definition "inverse (b::bool) \<equiv> \<not> b"
   12.14 +end
   12.15 +
   12.16 +overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
   12.17 +begin
   12.18 +  definition "inverse (S::'a set) \<equiv> -S"
   12.19 +end
   12.20 +
   12.21 +overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
   12.22 +begin
   12.23 +  definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
   12.24 +end
   12.25  
   12.26  lemma "inverse b"
   12.27  nitpick [expect = genuine]
    13.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Jan 11 21:20:44 2016 +0100
    13.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Jan 11 21:21:02 2016 +0100
    13.3 @@ -2416,11 +2416,15 @@
    13.4  consts
    13.5    fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
    13.6  
    13.7 -defs (overloaded)
    13.8 -  fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
    13.9 -
   13.10 -defs (overloaded)
   13.11 -  fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
   13.12 +overloading fresh_star_set \<equiv> "fresh_star :: 'b set \<Rightarrow> 'a \<Rightarrow> bool"
   13.13 +begin
   13.14 +  definition fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>xs. x\<sharp>(c::'a)"
   13.15 +end
   13.16 +
   13.17 +overloading frsh_star_list \<equiv> "fresh_star :: 'b list \<Rightarrow> 'a \<Rightarrow> bool"
   13.18 +begin
   13.19 +  definition fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>set xs. x\<sharp>(c::'a)"
   13.20 +end
   13.21  
   13.22  lemmas fresh_star_def = fresh_star_list fresh_star_set
   13.23  
    14.1 --- a/src/HOL/TLA/Buffer/Buffer.thy	Mon Jan 11 21:20:44 2016 +0100
    14.2 +++ b/src/HOL/TLA/Buffer/Buffer.thy	Mon Jan 11 21:21:02 2016 +0100
    14.3 @@ -8,31 +8,35 @@
    14.4  imports "../TLA"
    14.5  begin
    14.6  
    14.7 -consts
    14.8 -  (* actions *)
    14.9 -  BInit     :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
   14.10 -  Enq       :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
   14.11 -  Deq       :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
   14.12 -  Next      :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
   14.13 +(* actions *)
   14.14 +
   14.15 +definition BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
   14.16 +  where "BInit ic q oc == PRED q = #[]"
   14.17  
   14.18 -  (* temporal formulas *)
   14.19 -  IBuffer   :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
   14.20 -  Buffer    :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
   14.21 +definition Enq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
   14.22 +  where "Enq ic q oc == ACT (ic$ \<noteq> $ic)
   14.23 +                         \<and> (q$ = $q @ [ ic$ ])
   14.24 +                         \<and> (oc$ = $oc)"
   14.25  
   14.26 -defs
   14.27 -  BInit_def:   "BInit ic q oc    == PRED q = #[]"
   14.28 -  Enq_def:     "Enq ic q oc      == ACT (ic$ \<noteq> $ic)
   14.29 -                                     \<and> (q$ = $q @ [ ic$ ])
   14.30 -                                     \<and> (oc$ = $oc)"
   14.31 -  Deq_def:     "Deq ic q oc      == ACT ($q \<noteq> #[])
   14.32 -                                     \<and> (oc$ = hd< $q >)
   14.33 -                                     \<and> (q$ = tl< $q >)
   14.34 -                                     \<and> (ic$ = $ic)"
   14.35 -  Next_def:    "Next ic q oc     == ACT (Enq ic q oc \<or> Deq ic q oc)"
   14.36 -  IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
   14.37 -                                      \<and> \<box>[Next ic q oc]_(ic,q,oc)
   14.38 -                                      \<and> WF(Deq ic q oc)_(ic,q,oc)"
   14.39 -  Buffer_def:  "Buffer ic oc     == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
   14.40 +definition Deq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
   14.41 +  where "Deq ic q oc == ACT ($q \<noteq> #[])
   14.42 +                         \<and> (oc$ = hd< $q >)
   14.43 +                         \<and> (q$ = tl< $q >)
   14.44 +                         \<and> (ic$ = $ic)"
   14.45 +
   14.46 +definition Next :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
   14.47 +  where "Next ic q oc == ACT (Enq ic q oc \<or> Deq ic q oc)"
   14.48 +
   14.49 +
   14.50 +(* temporal formulas *)
   14.51 +
   14.52 +definition IBuffer :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
   14.53 +  where "IBuffer ic q oc == TEMP Init (BInit ic q oc)
   14.54 +                                  \<and> \<box>[Next ic q oc]_(ic,q,oc)
   14.55 +                                  \<and> WF(Deq ic q oc)_(ic,q,oc)"
   14.56 +
   14.57 +definition Buffer :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
   14.58 +  where "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
   14.59  
   14.60  
   14.61  (* ---------------------------- Data lemmas ---------------------------- *)
    15.1 --- a/src/HOL/TLA/Init.thy	Mon Jan 11 21:20:44 2016 +0100
    15.2 +++ b/src/HOL/TLA/Init.thy	Mon Jan 11 21:21:02 2016 +0100
    15.3 @@ -35,10 +35,17 @@
    15.4  defs
    15.5    Init_def:    "sigma \<Turnstile> Init F  ==  (first_world sigma) \<Turnstile> F"
    15.6  
    15.7 -defs (overloaded)
    15.8 -  fw_temp_def: "first_world == \<lambda>sigma. sigma"
    15.9 -  fw_stp_def:  "first_world == st1"
   15.10 -  fw_act_def:  "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
   15.11 +overloading
   15.12 +  fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
   15.13 +  fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
   15.14 +  fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> state"
   15.15 +begin
   15.16 +
   15.17 +definition "first_world == \<lambda>sigma. sigma"
   15.18 +definition "first_world == st1"
   15.19 +definition "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
   15.20 +
   15.21 +end
   15.22  
   15.23  lemma const_simps [int_rewrite, simp]:
   15.24    "\<turnstile> (Init #True) = #True"
    16.1 --- a/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 21:20:44 2016 +0100
    16.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 21:21:02 2016 +0100
    16.3 @@ -12,122 +12,135 @@
    16.4  type_synonym memType = "(Locs \<Rightarrow> Vals) stfun"  (* intention: MemLocs \<Rightarrow> MemVals *)
    16.5  type_synonym resType = "(PrIds \<Rightarrow> Vals) stfun"
    16.6  
    16.7 -consts
    16.8 -  (* state predicates *)
    16.9 -  MInit      :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
   16.10 -  PInit      :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
   16.11 -  (* auxiliary predicates: is there a pending read/write request for
   16.12 -     some process id and location/value? *)
   16.13 -  RdRequest  :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
   16.14 -  WrRequest  :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
   16.15 +
   16.16 +(* state predicates *)
   16.17 +
   16.18 +definition MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
   16.19 +  where "MInit mm l == PRED mm!l = #InitVal"
   16.20 +
   16.21 +definition PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
   16.22 +  where "PInit rs p == PRED rs!p = #NotAResult"
   16.23 +
   16.24 +
   16.25 +(* auxiliary predicates: is there a pending read/write request for
   16.26 +   some process id and location/value? *)
   16.27 +
   16.28 +definition RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
   16.29 +  where "RdRequest ch p l == PRED Calling ch p \<and> (arg<ch!p> = #(read l))"
   16.30 +
   16.31 +definition WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
   16.32 +  where "WrRequest ch p l v == PRED Calling ch p \<and> (arg<ch!p> = #(write l v))"
   16.33 +
   16.34 +
   16.35 +(* actions *)
   16.36 +
   16.37 +(* a read that doesn't raise BadArg *)
   16.38 +definition GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
   16.39 +  where "GoodRead mm rs p l == ACT #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
   16.40 +
   16.41 +(* a read that raises BadArg *)
   16.42 +definition BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
   16.43 +  where "BadRead mm rs p l == ACT #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
   16.44  
   16.45 -  (* actions *)
   16.46 -  GoodRead   :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
   16.47 -  BadRead    :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
   16.48 -  ReadInner  :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
   16.49 -  Read       :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
   16.50 -  GoodWrite  :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
   16.51 -  BadWrite   :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
   16.52 -  WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
   16.53 -  Write      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
   16.54 -  MemReturn  :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
   16.55 -  MemFail    :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
   16.56 -  RNext      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
   16.57 -  UNext      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
   16.58 +(* the read action with l visible *)
   16.59 +definition ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
   16.60 +  where "ReadInner ch mm rs p l == ACT
   16.61 +    $(RdRequest ch p l)
   16.62 +    \<and> (GoodRead mm rs p l  \<or>  BadRead mm rs p l)
   16.63 +    \<and> unchanged (rtrner ch ! p)"
   16.64 +
   16.65 +(* the read action with l quantified *)
   16.66 +definition Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
   16.67 +  where "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
   16.68  
   16.69 -  (* temporal formulas *)
   16.70 -  RPSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
   16.71 -  UPSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
   16.72 -  MSpec      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
   16.73 -  IRSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
   16.74 -  IUSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
   16.75 +(* similar definitions for the write action *)
   16.76 +definition GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
   16.77 +  where "GoodWrite mm rs p l v ==
   16.78 +    ACT #l \<in> #MemLoc \<and> #v \<in> #MemVal
   16.79 +      \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
   16.80  
   16.81 -  RSpec      :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
   16.82 -  USpec      :: "memChType \<Rightarrow> temporal"
   16.83 +definition BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
   16.84 +  where "BadWrite mm rs p l v == ACT
   16.85 +    \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
   16.86 +    \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
   16.87  
   16.88 -  (* memory invariant: in the paper, the invariant is hidden in the definition of
   16.89 -     the predicate S used in the implementation proof, but it is easier to verify
   16.90 -     at this level. *)
   16.91 -  MemInv    :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
   16.92 +definition WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
   16.93 +  where "WriteInner ch mm rs p l v == ACT
   16.94 +    $(WrRequest ch p l v)
   16.95 +    \<and> (GoodWrite mm rs p l v  \<or>  BadWrite mm rs p l v)
   16.96 +    \<and> unchanged (rtrner ch ! p)"
   16.97  
   16.98 -defs
   16.99 -  MInit_def:         "MInit mm l == PRED mm!l = #InitVal"
  16.100 -  PInit_def:         "PInit rs p == PRED rs!p = #NotAResult"
  16.101 +definition Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
  16.102 +  where "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
  16.103 +
  16.104  
  16.105 -  RdRequest_def:     "RdRequest ch p l == PRED
  16.106 -                         Calling ch p \<and> (arg<ch!p> = #(read l))"
  16.107 -  WrRequest_def:     "WrRequest ch p l v == PRED
  16.108 -                         Calling ch p \<and> (arg<ch!p> = #(write l v))"
  16.109 -  (* a read that doesn't raise BadArg *)
  16.110 -  GoodRead_def:      "GoodRead mm rs p l == ACT
  16.111 -                        #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
  16.112 -  (* a read that raises BadArg *)
  16.113 -  BadRead_def:       "BadRead mm rs p l == ACT
  16.114 -                        #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
  16.115 -  (* the read action with l visible *)
  16.116 -  ReadInner_def:     "ReadInner ch mm rs p l == ACT
  16.117 -                         $(RdRequest ch p l)
  16.118 -                         \<and> (GoodRead mm rs p l  \<or>  BadRead mm rs p l)
  16.119 -                         \<and> unchanged (rtrner ch ! p)"
  16.120 -  (* the read action with l quantified *)
  16.121 -  Read_def:          "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
  16.122 +(* the return action *)
  16.123 +definition MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
  16.124 +  where "MemReturn ch rs p == ACT
  16.125 +   (   ($(rs!p) \<noteq> #NotAResult)
  16.126 +    \<and> ((rs!p)$ = #NotAResult)
  16.127 +    \<and> Return ch p (rs!p))"
  16.128 +
  16.129 +(* the failure action of the unreliable memory *)
  16.130 +definition MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
  16.131 +  where "MemFail ch rs p == ACT
  16.132 +    $(Calling ch p)
  16.133 +    \<and> ((rs!p)$ = #MemFailure)
  16.134 +    \<and> unchanged (rtrner ch ! p)"
  16.135  
  16.136 -  (* similar definitions for the write action *)
  16.137 -  GoodWrite_def:     "GoodWrite mm rs p l v == ACT
  16.138 -                        #l \<in> #MemLoc \<and> #v \<in> #MemVal
  16.139 -                        \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
  16.140 -  BadWrite_def:      "BadWrite mm rs p l v == ACT
  16.141 -                        \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
  16.142 -                        \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
  16.143 -  WriteInner_def:    "WriteInner ch mm rs p l v == ACT
  16.144 -                        $(WrRequest ch p l v)
  16.145 -                        \<and> (GoodWrite mm rs p l v  \<or>  BadWrite mm rs p l v)
  16.146 -                        \<and> unchanged (rtrner ch ! p)"
  16.147 -  Write_def:         "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
  16.148 +(* next-state relations for reliable / unreliable memory *)
  16.149 +definition RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
  16.150 +  where "RNext ch mm rs p == ACT
  16.151 +   (  Read ch mm rs p
  16.152 +    \<or> (\<exists>l. Write ch mm rs p l)
  16.153 +    \<or> MemReturn ch rs p)"
  16.154 +
  16.155 +definition UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
  16.156 +  where "UNext ch mm rs p == ACT (RNext ch mm rs p \<or> MemFail ch rs p)"
  16.157  
  16.158 -  (* the return action *)
  16.159 -  MemReturn_def:     "MemReturn ch rs p == ACT
  16.160 -                       (   ($(rs!p) \<noteq> #NotAResult)
  16.161 -                        \<and> ((rs!p)$ = #NotAResult)
  16.162 -                        \<and> Return ch p (rs!p))"
  16.163 +
  16.164 +(* temporal formulas *)
  16.165 +
  16.166 +definition RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
  16.167 +  where "RPSpec ch mm rs p == TEMP
  16.168 +    Init(PInit rs p)
  16.169 +    \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
  16.170 +    \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
  16.171 +    \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
  16.172  
  16.173 -  (* the failure action of the unreliable memory *)
  16.174 -  MemFail_def:       "MemFail ch rs p == ACT
  16.175 -                        $(Calling ch p)
  16.176 -                        \<and> ((rs!p)$ = #MemFailure)
  16.177 -                        \<and> unchanged (rtrner ch ! p)"
  16.178 -  (* next-state relations for reliable / unreliable memory *)
  16.179 -  RNext_def:         "RNext ch mm rs p == ACT
  16.180 -                       (  Read ch mm rs p
  16.181 -                        \<or> (\<exists>l. Write ch mm rs p l)
  16.182 -                        \<or> MemReturn ch rs p)"
  16.183 -  UNext_def:         "UNext ch mm rs p == ACT
  16.184 -                        (RNext ch mm rs p \<or> MemFail ch rs p)"
  16.185 +definition UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
  16.186 +  where "UPSpec ch mm rs p == TEMP
  16.187 +    Init(PInit rs p)
  16.188 +    \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
  16.189 +    \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
  16.190 +    \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
  16.191 +
  16.192 +definition MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
  16.193 +  where "MSpec ch mm rs l == TEMP
  16.194 +    Init(MInit mm l)
  16.195 +    \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
  16.196 +
  16.197 +definition IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
  16.198 +  where "IRSpec ch mm rs == TEMP
  16.199 +    (\<forall>p. RPSpec ch mm rs p)
  16.200 +    \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
  16.201  
  16.202 -  RPSpec_def:        "RPSpec ch mm rs p == TEMP
  16.203 -                        Init(PInit rs p)
  16.204 -                        \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
  16.205 -                        \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
  16.206 -                        \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
  16.207 -  UPSpec_def:        "UPSpec ch mm rs p == TEMP
  16.208 -                        Init(PInit rs p)
  16.209 -                        \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
  16.210 -                        \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
  16.211 -                        \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
  16.212 -  MSpec_def:         "MSpec ch mm rs l == TEMP
  16.213 -                        Init(MInit mm l)
  16.214 -                        \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
  16.215 -  IRSpec_def:        "IRSpec ch mm rs == TEMP
  16.216 -                        (\<forall>p. RPSpec ch mm rs p)
  16.217 -                        \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
  16.218 -  IUSpec_def:        "IUSpec ch mm rs == TEMP
  16.219 -                        (\<forall>p. UPSpec ch mm rs p)
  16.220 -                        \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
  16.221 +definition IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
  16.222 +  where "IUSpec ch mm rs == TEMP
  16.223 +    (\<forall>p. UPSpec ch mm rs p)
  16.224 +    \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
  16.225 +
  16.226 +definition RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
  16.227 +  where "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
  16.228  
  16.229 -  RSpec_def:         "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
  16.230 -  USpec_def:         "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
  16.231 +definition USpec :: "memChType \<Rightarrow> temporal"
  16.232 +  where "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
  16.233  
  16.234 -  MemInv_def:        "MemInv mm l == PRED  #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
  16.235 +(* memory invariant: in the paper, the invariant is hidden in the definition of
  16.236 +   the predicate S used in the implementation proof, but it is easier to verify
  16.237 +   at this level. *)
  16.238 +definition MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
  16.239 +  where "MemInv mm l == PRED  #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
  16.240  
  16.241  lemmas RM_action_defs =
  16.242    MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
    17.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 21:20:44 2016 +0100
    17.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 21:21:02 2016 +0100
    17.3 @@ -16,65 +16,78 @@
    17.4    *)
    17.5  type_synonym ('a,'r) channel =" (PrIds \<Rightarrow> ('a,'r) chan) stfun"
    17.6  
    17.7 +
    17.8 +(* data-level functions *)
    17.9 +
   17.10  consts
   17.11 -  (* data-level functions *)
   17.12    cbit          :: "('a,'r) chan \<Rightarrow> bit"
   17.13    rbit          :: "('a,'r) chan \<Rightarrow> bit"
   17.14    arg           :: "('a,'r) chan \<Rightarrow> 'a"
   17.15    res           :: "('a,'r) chan \<Rightarrow> 'r"
   17.16  
   17.17 -  (* state functions *)
   17.18 -  caller        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
   17.19 -  rtrner        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
   17.20 +
   17.21 +(* state functions *)
   17.22  
   17.23 -  (* state predicates *)
   17.24 -  Calling   :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
   17.25 +definition caller :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
   17.26 +  where "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
   17.27  
   17.28 -  (* actions *)
   17.29 -  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
   17.30 -  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
   17.31 +definition rtrner :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
   17.32 +  where "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))"
   17.33 +
   17.34  
   17.35 -  (* temporal formulas *)
   17.36 -  PLegalCaller      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
   17.37 -  LegalCaller       :: "('a,'r) channel \<Rightarrow> temporal"
   17.38 -  PLegalReturner    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
   17.39 -  LegalReturner     :: "('a,'r) channel \<Rightarrow> temporal"
   17.40 +(* slice through array-valued state function *)
   17.41  
   17.42 -  (* slice through array-valued state function *)
   17.43 +consts
   17.44    slice        :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
   17.45 -
   17.46  syntax
   17.47    "_slice"    :: "[lift, 'a] \<Rightarrow> lift"      ("(_!_)" [70,70] 70)
   17.48 -
   17.49 -  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
   17.50 -  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
   17.51 -
   17.52  translations
   17.53    "_slice"  ==  "CONST slice"
   17.54 -
   17.55 -  "_Call"   ==  "CONST ACall"
   17.56 -  "_Return" ==  "CONST AReturn"
   17.57 -
   17.58  defs
   17.59    slice_def:     "(PRED (x!i)) s == x s i"
   17.60  
   17.61 -  caller_def:    "caller ch   == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
   17.62 -  rtrner_def:    "rtrner ch   == \<lambda>s p. (rbit (ch s p), res (ch s p))"
   17.63 +
   17.64 +(* state predicates *)
   17.65 +
   17.66 +definition Calling :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
   17.67 +  where "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
   17.68 +
   17.69 +
   17.70 +(* actions *)
   17.71  
   17.72 -  Calling_def:   "Calling ch p  == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
   17.73 +consts
   17.74 +  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
   17.75 +  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
   17.76 +syntax
   17.77 +  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
   17.78 +  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
   17.79 +translations
   17.80 +  "_Call"   ==  "CONST ACall"
   17.81 +  "_Return" ==  "CONST AReturn"
   17.82 +defs
   17.83    Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
   17.84                                       \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
   17.85                                       \<and> (arg<ch!p>$ = $v)"
   17.86    Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
   17.87                                       \<and> (rbit<ch!p>$ = $cbit<ch!p>)
   17.88                                       \<and> (res<ch!p>$ = $v)"
   17.89 -  PLegalCaller_def:      "PLegalCaller ch p == TEMP
   17.90 -                             Init(\<not> Calling ch p)
   17.91 -                             \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
   17.92 -  LegalCaller_def:       "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
   17.93 -  PLegalReturner_def:    "PLegalReturner ch p == TEMP
   17.94 -                                \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
   17.95 -  LegalReturner_def:     "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
   17.96 +
   17.97 +
   17.98 +(* temporal formulas *)
   17.99 +
  17.100 +definition PLegalCaller :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
  17.101 +  where "PLegalCaller ch p == TEMP
  17.102 +     Init(\<not> Calling ch p)
  17.103 +     \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
  17.104 +
  17.105 +definition LegalCaller :: "('a,'r) channel \<Rightarrow> temporal"
  17.106 +  where "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
  17.107 +
  17.108 +definition PLegalReturner :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
  17.109 +  where "PLegalReturner ch p == TEMP \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
  17.110 +
  17.111 +definition LegalReturner :: "('a,'r) channel \<Rightarrow> temporal"
  17.112 +  where "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
  17.113  
  17.114  declare slice_def [simp]
  17.115  
    18.1 --- a/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 21:20:44 2016 +0100
    18.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 21:21:02 2016 +0100
    18.3 @@ -12,63 +12,64 @@
    18.4  type_synonym rpcRcvChType = "memChType"
    18.5  type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun"
    18.6  
    18.7 -consts
    18.8 -  (* state predicates *)
    18.9 -  RPCInit      :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
   18.10 +
   18.11 +(* state predicates *)
   18.12  
   18.13 -  (* actions *)
   18.14 -  RPCFwd     :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.15 -  RPCReject  :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.16 -  RPCFail    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.17 -  RPCReply   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.18 -  RPCNext    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.19 +definition RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
   18.20 +  where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
   18.21 +
   18.22 +
   18.23 +(* actions *)
   18.24  
   18.25 -  (* temporal *)
   18.26 -  RPCIPSpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
   18.27 -  RPCISpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
   18.28 -
   18.29 -defs
   18.30 -  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
   18.31 +definition RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.32 +  where "RPCFwd send rcv rst p == ACT
   18.33 +      $(Calling send p)
   18.34 +    \<and> $(rst!p) = # rpcA
   18.35 +    \<and> IsLegalRcvArg<arg<$(send!p)>>
   18.36 +    \<and> Call rcv p RPCRelayArg<arg<send!p>>
   18.37 +    \<and> (rst!p)$ = # rpcB
   18.38 +    \<and> unchanged (rtrner send!p)"
   18.39  
   18.40 -  RPCFwd_def:        "RPCFwd send rcv rst p == ACT
   18.41 -                         $(Calling send p)
   18.42 -                         \<and> $(rst!p) = # rpcA
   18.43 -                         \<and> IsLegalRcvArg<arg<$(send!p)>>
   18.44 -                         \<and> Call rcv p RPCRelayArg<arg<send!p>>
   18.45 -                         \<and> (rst!p)$ = # rpcB
   18.46 -                         \<and> unchanged (rtrner send!p)"
   18.47 +definition RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.48 +  where "RPCReject send rcv rst p == ACT
   18.49 +      $(rst!p) = # rpcA
   18.50 +    \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
   18.51 +    \<and> Return send p #BadCall
   18.52 +    \<and> unchanged ((rst!p), (caller rcv!p))"
   18.53  
   18.54 -  RPCReject_def:     "RPCReject send rcv rst p == ACT
   18.55 -                           $(rst!p) = # rpcA
   18.56 -                         \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
   18.57 -                         \<and> Return send p #BadCall
   18.58 -                         \<and> unchanged ((rst!p), (caller rcv!p))"
   18.59 +definition RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.60 +  where "RPCFail send rcv rst p == ACT
   18.61 +      \<not>$(Calling rcv p)
   18.62 +    \<and> Return send p #RPCFailure
   18.63 +    \<and> (rst!p)$ = #rpcA
   18.64 +    \<and> unchanged (caller rcv!p)"
   18.65  
   18.66 -  RPCFail_def:       "RPCFail send rcv rst p == ACT
   18.67 -                           \<not>$(Calling rcv p)
   18.68 -                         \<and> Return send p #RPCFailure
   18.69 -                         \<and> (rst!p)$ = #rpcA
   18.70 -                         \<and> unchanged (caller rcv!p)"
   18.71 +definition RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.72 +  where "RPCReply send rcv rst p == ACT
   18.73 +      \<not>$(Calling rcv p)
   18.74 +    \<and> $(rst!p) = #rpcB
   18.75 +    \<and> Return send p res<rcv!p>
   18.76 +    \<and> (rst!p)$ = #rpcA
   18.77 +    \<and> unchanged (caller rcv!p)"
   18.78  
   18.79 -  RPCReply_def:      "RPCReply send rcv rst p == ACT
   18.80 -                           \<not>$(Calling rcv p)
   18.81 -                         \<and> $(rst!p) = #rpcB
   18.82 -                         \<and> Return send p res<rcv!p>
   18.83 -                         \<and> (rst!p)$ = #rpcA
   18.84 -                         \<and> unchanged (caller rcv!p)"
   18.85 +definition RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
   18.86 +  where "RPCNext send rcv rst p == ACT
   18.87 +    (  RPCFwd send rcv rst p
   18.88 +     \<or> RPCReject send rcv rst p
   18.89 +     \<or> RPCFail send rcv rst p
   18.90 +     \<or> RPCReply send rcv rst p)"
   18.91 +
   18.92  
   18.93 -  RPCNext_def:       "RPCNext send rcv rst p == ACT
   18.94 -                        (  RPCFwd send rcv rst p
   18.95 -                         \<or> RPCReject send rcv rst p
   18.96 -                         \<or> RPCFail send rcv rst p
   18.97 -                         \<or> RPCReply send rcv rst p)"
   18.98 +(* temporal *)
   18.99  
  18.100 -  RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
  18.101 -                           Init RPCInit rcv rst p
  18.102 -                         \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
  18.103 -                         \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
  18.104 +definition RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
  18.105 +  where "RPCIPSpec send rcv rst p == TEMP
  18.106 +     Init RPCInit rcv rst p
  18.107 +   \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
  18.108 +   \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
  18.109  
  18.110 -  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
  18.111 +definition RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
  18.112 +  where "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
  18.113  
  18.114  
  18.115  lemmas RPC_action_defs =
    19.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Mon Jan 11 21:20:44 2016 +0100
    19.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Mon Jan 11 21:21:02 2016 +0100
    19.3 @@ -16,32 +16,28 @@
    19.4  datatype rpcOp = memcall memOp | othercall Vals
    19.5  datatype rpcState = rpcA | rpcB
    19.6  
    19.7 -consts
    19.8 -  (* some particular return values *)
    19.9 -  RPCFailure     :: Vals
   19.10 -  BadCall        :: Vals
   19.11 -  
   19.12 -  (* Translate an rpc call to a memory call and test if the current argument
   19.13 -     is legal for the receiver (i.e., the memory). This can now be a little
   19.14 -     simpler than for the generic RPC component. RelayArg returns an arbitrary
   19.15 -     memory call for illegal arguments. *)
   19.16 -  IsLegalRcvArg  :: "rpcOp \<Rightarrow> bool"
   19.17 -  RPCRelayArg    :: "rpcOp \<Rightarrow> memOp"
   19.18 -
   19.19 -axiomatization where
   19.20 +axiomatization RPCFailure :: Vals and BadCall :: Vals
   19.21 +where
   19.22    (* RPCFailure is different from MemVals and exceptions *)
   19.23    RFNoMemVal:        "RPCFailure \<notin> MemVal" and
   19.24    NotAResultNotRF:   "NotAResult \<noteq> RPCFailure" and
   19.25    OKNotRF:           "OK \<noteq> RPCFailure" and
   19.26    BANotRF:           "BadArg \<noteq> RPCFailure"
   19.27  
   19.28 -defs
   19.29 -  IsLegalRcvArg_def: "IsLegalRcvArg ra ==
   19.30 -                         case ra of (memcall m) \<Rightarrow> True
   19.31 -                                  | (othercall v) \<Rightarrow> False"
   19.32 -  RPCRelayArg_def:   "RPCRelayArg ra ==
   19.33 -                         case ra of (memcall m) \<Rightarrow> m
   19.34 -                                  | (othercall v) \<Rightarrow> undefined"
   19.35 +(* Translate an rpc call to a memory call and test if the current argument
   19.36 +   is legal for the receiver (i.e., the memory). This can now be a little
   19.37 +   simpler than for the generic RPC component. RelayArg returns an arbitrary
   19.38 +   memory call for illegal arguments. *)
   19.39 +
   19.40 +definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
   19.41 +  where "IsLegalRcvArg ra ==
   19.42 +    case ra of (memcall m) \<Rightarrow> True
   19.43 +             | (othercall v) \<Rightarrow> False"
   19.44 +
   19.45 +definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
   19.46 +  where "RPCRelayArg ra ==
   19.47 +    case ra of (memcall m) \<Rightarrow> m
   19.48 +             | (othercall v) \<Rightarrow> undefined"
   19.49  
   19.50  lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
   19.51    NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
    20.1 --- a/src/HOL/TLA/Stfun.thy	Mon Jan 11 21:20:44 2016 +0100
    20.2 +++ b/src/HOL/TLA/Stfun.thy	Mon Jan 11 21:21:02 2016 +0100
    20.3 @@ -40,15 +40,17 @@
    20.4    "PRED P"   =>  "(P::state \<Rightarrow> _)"
    20.5    "_stvars"  ==  "CONST stvars"
    20.6  
    20.7 -defs
    20.8 -  (* Base variables may be assigned arbitrary (type-correct) values.
    20.9 -     Note that vs may be a tuple of variables. The correct identification
   20.10 -     of base variables is up to the user who must take care not to
   20.11 -     introduce an inconsistency. For example, "basevars (x,x)" would
   20.12 -     definitely be inconsistent.
   20.13 -  *)
   20.14 -  basevars_def:  "stvars vs == range vs = UNIV"
   20.15 -
   20.16 +(* Base variables may be assigned arbitrary (type-correct) values.
   20.17 +   Note that vs may be a tuple of variables. The correct identification
   20.18 +   of base variables is up to the user who must take care not to
   20.19 +   introduce an inconsistency. For example, "basevars (x,x)" would
   20.20 +   definitely be inconsistent.
   20.21 +*)
   20.22 +overloading stvars \<equiv> stvars
   20.23 +begin
   20.24 +  definition stvars :: "(state \<Rightarrow> 'a) \<Rightarrow> bool"
   20.25 +    where basevars_def: "stvars vs == range vs = UNIV"
   20.26 +end
   20.27  
   20.28  lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>u. vs u = c"
   20.29    apply (unfold basevars_def)
    21.1 --- a/src/HOL/ex/MT.thy	Mon Jan 11 21:20:44 2016 +0100
    21.2 +++ b/src/HOL/ex/MT.thy	Mon Jan 11 21:21:02 2016 +0100
    21.3 @@ -60,21 +60,7 @@
    21.4    te_app :: "[TyEnv, ExVar] => Ty"
    21.5    te_dom :: "TyEnv => ExVar set"
    21.6  
    21.7 -  eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
    21.8 -  eval_rel :: "((ValEnv * Ex) * Val) set"
    21.9 -  eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
   21.10 -
   21.11 -  elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
   21.12 -  elab_rel :: "((TyEnv * Ex) * Ty) set"
   21.13 -  elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
   21.14 -
   21.15    isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
   21.16 -  isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
   21.17 -
   21.18 -  hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
   21.19 -  hasty_rel :: "(Val * Ty) set"
   21.20 -  hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
   21.21 -  hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
   21.22  
   21.23  (*
   21.24    Expression constructors must be injective, distinct and it must be possible
   21.25 @@ -185,9 +171,8 @@
   21.26  derived.
   21.27  *)
   21.28  
   21.29 -defs
   21.30 -  eval_fun_def:
   21.31 -    " eval_fun(s) ==
   21.32 +definition eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
   21.33 +  where "eval_fun(s) ==
   21.34       { pp.
   21.35         (? ve c. pp=((ve,e_const(c)),v_const(c))) |
   21.36         (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
   21.37 @@ -208,51 +193,56 @@
   21.38         )
   21.39       }"
   21.40  
   21.41 -  eval_rel_def: "eval_rel == lfp(eval_fun)"
   21.42 -  eval_def: "ve |- e ---> v == ((ve,e),v):eval_rel"
   21.43 +definition eval_rel :: "((ValEnv * Ex) * Val) set"
   21.44 +  where "eval_rel == lfp(eval_fun)"
   21.45 +
   21.46 +definition eval :: "[ValEnv, Ex, Val] => bool"  ("_ |- _ ---> _" [36,0,36] 50)
   21.47 +  where "ve |- e ---> v == ((ve,e),v) \<in> eval_rel"
   21.48  
   21.49  (* The static semantics is defined in the same way as the dynamic
   21.50  semantics.  The relation te |- e ===> t express the expression e has the
   21.51  type t in the type environment te.
   21.52  *)
   21.53  
   21.54 -  elab_fun_def:
   21.55 -  "elab_fun(s) ==
   21.56 -  { pp.
   21.57 -    (? te c t. pp=((te,e_const(c)),t) & c isof t) |
   21.58 -    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
   21.59 -    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
   21.60 -    (? te f x e t1 t2.
   21.61 -       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
   21.62 -    ) |
   21.63 -    (? te e1 e2 t1 t2.
   21.64 -       pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
   21.65 -    )
   21.66 -  }"
   21.67 +definition elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
   21.68 +  where "elab_fun(s) ==
   21.69 +    { pp.
   21.70 +      (? te c t. pp=((te,e_const(c)),t) & c isof t) |
   21.71 +      (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
   21.72 +      (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
   21.73 +      (? te f x e t1 t2.
   21.74 +         pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
   21.75 +      ) |
   21.76 +      (? te e1 e2 t1 t2.
   21.77 +         pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
   21.78 +      )
   21.79 +    }"
   21.80  
   21.81 -  elab_rel_def: "elab_rel == lfp(elab_fun)"
   21.82 -  elab_def: "te |- e ===> t == ((te,e),t):elab_rel"
   21.83 +definition elab_rel :: "((TyEnv * Ex) * Ty) set"
   21.84 +  where "elab_rel == lfp(elab_fun)"
   21.85 +
   21.86 +definition elab :: "[TyEnv, Ex, Ty] => bool"  ("_ |- _ ===> _" [36,0,36] 50)
   21.87 +  where "te |- e ===> t == ((te,e),t):elab_rel"
   21.88 +
   21.89  
   21.90  (* The original correspondence relation *)
   21.91  
   21.92 -  isof_env_def:
   21.93 -    " ve isofenv te ==
   21.94 -     ve_dom(ve) = te_dom(te) &
   21.95 -     ( ! x.
   21.96 +definition isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
   21.97 +  where "ve isofenv te ==
   21.98 +    ve_dom(ve) = te_dom(te) &
   21.99 +     (! x.
  21.100           x:ve_dom(ve) -->
  21.101 -         (? c. ve_app ve x = v_const(c) & c isof te_app te x)
  21.102 -     )
  21.103 -   "
  21.104 +         (? c. ve_app ve x = v_const(c) & c isof te_app te x))"
  21.105  
  21.106  axiomatization where
  21.107    isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
  21.108  
  21.109 -defs
  21.110 +
  21.111  (* The extented correspondence relation *)
  21.112  
  21.113 -  hasty_fun_def:
  21.114 -    " hasty_fun(r) ==
  21.115 -     { p.
  21.116 +definition hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
  21.117 +  where "hasty_fun(r) ==
  21.118 +    { p.
  21.119         ( ? c t. p = (v_const(c),t) & c isof t) |
  21.120         ( ? ev e ve t te.
  21.121             p = (v_clos(<|ev,e,ve|>),t) &
  21.122 @@ -260,15 +250,18 @@
  21.123             ve_dom(ve) = te_dom(te) &
  21.124             (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
  21.125         )
  21.126 -     }
  21.127 -   "
  21.128 +    }"
  21.129 +
  21.130 +definition hasty_rel :: "(Val * Ty) set"
  21.131 +  where "hasty_rel == gfp(hasty_fun)"
  21.132  
  21.133 -  hasty_rel_def: "hasty_rel == gfp(hasty_fun)"
  21.134 -  hasty_def: "v hasty t == (v,t) : hasty_rel"
  21.135 -  hasty_env_def:
  21.136 -    " ve hastyenv te ==
  21.137 -     ve_dom(ve) = te_dom(te) &
  21.138 -     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
  21.139 +definition hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
  21.140 +  where "v hasty t == (v,t) : hasty_rel"
  21.141 +
  21.142 +definition hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
  21.143 +  where "ve hastyenv te ==
  21.144 +    ve_dom(ve) = te_dom(te) &
  21.145 +      (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
  21.146  
  21.147  
  21.148  (* ############################################################ *)