# HG changeset patch
# User wenzelm
# Date 1452543662 -3600
# Node ID 5b946c81dfbf586806f8008c2e2adf52af61cfc8
# Parent  bdab93ccfaf83d50a6b81f58ef264d996c5b175d
eliminated old defs;

diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/Auth/All_Symmetric.thy
--- a/src/HOL/Auth/All_Symmetric.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Auth/All_Symmetric.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -4,7 +4,10 @@
 
 text \<open>All keys are symmetric\<close>
 
-defs all_symmetric_def: "all_symmetric \<equiv> True"
+overloading all_symmetric \<equiv> all_symmetric
+begin
+  definition "all_symmetric \<equiv> True"
+end
 
 lemma isSym_keys: "K \<in> symKeys"
   by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Bali/Example.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -141,12 +141,16 @@
 lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
 by (simp add: SXcpt_def)
 
+
 subsubsection "classes and interfaces"
 
-defs
-
-  Object_mdecls_def: "Object_mdecls \<equiv> []"
-  SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
+overloading
+  Object_mdecls \<equiv> Object_mdecls
+  SXcpt_mdecls \<equiv> SXcpt_mdecls
+begin
+  definition "Object_mdecls \<equiv> []"
+  definition "SXcpt_mdecls  \<equiv> []"
+end
 
 axiomatization  
   foo    :: mname
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -29,8 +29,10 @@
          THEN Loc Res:==(%s. 1)
          ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
 
-defs
-  bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
+overloading bodies \<equiv> bodies
+begin
+  definition "bodies == [(Even,evn),(Odd,odd)]"
+end
 
 definition
   Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/IMPP/Misc.thy
--- a/src/HOL/IMPP/Misc.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/IMPP/Misc.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -8,13 +8,29 @@
 imports Hoare
 begin
 
-defs
-  newlocs_def: "newlocs       == %x. undefined"
-  setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
-  getlocs_def: "getlocs s     == case s of st g l => l"
-   update_def: "update s vn v == case vn of
-                               Glb gn => (case s of st g l => st (g(gn:=v)) l)
-                             | Loc ln => (case s of st g l => st g (l(ln:=v)))"
+overloading
+  newlocs \<equiv> newlocs
+  setlocs \<equiv> setlocs
+  getlocs \<equiv> getlocs
+  update \<equiv> update
+begin
+
+definition newlocs :: locals
+  where "newlocs == %x. undefined"
+
+definition setlocs :: "state => locals => state"
+  where "setlocs s l' == case s of st g l => st g l'"
+
+definition getlocs :: "state => locals"
+  where "getlocs s == case s of st g l => l"
+
+definition update  :: "state => vname => val => state"
+  where "update s vn v ==
+    case vn of
+      Glb gn => (case s of st g l => st (g(gn:=v)) l)
+    | Loc ln => (case s of st g l => st g (l(ln:=v)))"
+
+end
 
 
 subsection "state access"
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/IOA/Asig.thy
--- a/src/HOL/IOA/Asig.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/IOA/Asig.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -9,41 +9,31 @@
 imports Main
 begin
 
-type_synonym
-  'a signature = "('a set * 'a set * 'a set)"
+type_synonym 'a signature = "('a set * 'a set * 'a set)"
+
+definition "inputs" :: "'action signature => 'action set"
+  where asig_inputs_def: "inputs == fst"
 
-consts
-  "actions" :: "'action signature => 'action set"
-  "inputs" :: "'action signature => 'action set"
-  "outputs" :: "'action signature => 'action set"
-  "internals" :: "'action signature => 'action set"
-  externals :: "'action signature => 'action set"
+definition "outputs" :: "'action signature => 'action set"
+  where asig_outputs_def: "outputs == (fst o snd)"
 
-  is_asig       ::"'action signature => bool"
-  mk_ext_asig   ::"'action signature => 'action signature"
-
-
-defs
+definition "internals" :: "'action signature => 'action set"
+  where asig_internals_def: "internals == (snd o snd)"
 
-asig_inputs_def:    "inputs == fst"
-asig_outputs_def:   "outputs == (fst o snd)"
-asig_internals_def: "internals == (snd o snd)"
+definition "actions" :: "'action signature => 'action set"
+  where actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
 
-actions_def:
-   "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
-
-externals_def:
-   "externals(asig) == (inputs(asig) Un outputs(asig))"
+definition externals :: "'action signature => 'action set"
+  where externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))"
 
-is_asig_def:
-  "is_asig(triple) ==
-      ((inputs(triple) Int outputs(triple) = {})    &
-       (outputs(triple) Int internals(triple) = {}) &
-       (inputs(triple) Int internals(triple) = {}))"
+definition is_asig :: "'action signature => bool"
+  where "is_asig(triple) ==
+    ((inputs(triple) Int outputs(triple) = {})    &
+     (outputs(triple) Int internals(triple) = {}) &
+     (inputs(triple) Int internals(triple) = {}))"
 
-
-mk_ext_asig_def:
-  "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
+definition mk_ext_asig :: "'action signature => 'action signature"
+  where "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
 
 
 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/IOA/IOA.thy
--- a/src/HOL/IOA/IOA.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/IOA/IOA.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -15,183 +15,148 @@
 type_synonym ('a, 's) transition = "('s * 'a * 's)"
 type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
 
-consts
+(* IO automata *)
+
+definition state_trans :: "['action signature, ('action,'state)transition set] => bool"
+  where "state_trans asig R ==
+     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
+     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+
+definition asig_of :: "('action,'state)ioa => 'action signature"
+  where "asig_of == fst"
 
-  (* IO automata *)
-  state_trans::"['action signature, ('action,'state)transition set] => bool"
-  asig_of    ::"('action,'state)ioa => 'action signature"
-  starts_of  ::"('action,'state)ioa => 'state set"
-  trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
-  IOA        ::"('action,'state)ioa => bool"
+definition starts_of :: "('action,'state)ioa => 'state set"
+  where "starts_of == (fst o snd)"
+
+definition trans_of :: "('action,'state)ioa => ('action,'state)transition set"
+  where "trans_of == (snd o snd)"
 
-  (* Executions, schedules, and traces *)
+definition IOA :: "('action,'state)ioa => bool"
+  where "IOA(ioa) == (is_asig(asig_of(ioa)) &
+                (~ starts_of(ioa) = {}) &
+                state_trans (asig_of ioa) (trans_of ioa))"
+
+
+(* Executions, schedules, and traces *)
 
-  is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool"
-  has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
-  executions    :: "('action,'state)ioa => ('action,'state)execution set"
-  mk_trace  :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
-  reachable     :: "[('action,'state)ioa, 'state] => bool"
-  invariant     :: "[('action,'state)ioa, 'state=>bool] => bool"
-  has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
-  traces    :: "('action,'state)ioa => 'action oseq set"
-  NF            :: "'a oseq => 'a oseq"
+(* An execution fragment is modelled with a pair of sequences:
+   the first is the action options, the second the state sequence.
+   Finite executions have None actions from some point on. *)
+definition is_execution_fragment :: "[('action,'state)ioa, ('action,'state)execution] => bool"
+  where "is_execution_fragment A ex ==
+     let act = fst(ex); state = snd(ex)
+     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
+              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
+
+definition executions :: "('action,'state)ioa => ('action,'state)execution set"
+  where "executions(ioa) == {e. snd e 0:starts_of(ioa) & is_execution_fragment ioa e}"
 
-  (* Composition of action signatures and automata *)
+
+definition reachable :: "[('action,'state)ioa, 'state] => bool"
+  where "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
+
+definition invariant :: "[('action,'state)ioa, 'state=>bool] => bool"
+  where "invariant A P == (!s. reachable A s --> P(s))"
+
+
+(* Composition of action signatures and automata *)
+
+consts
   compatible_asigs ::"('a => 'action signature) => bool"
   asig_composition ::"('a => 'action signature) => 'action signature"
   compatible_ioas  ::"('a => ('action,'state)ioa) => bool"
   ioa_composition  ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"
 
-  (* binary composition of action signatures and automata *)
-  compat_asigs ::"['action signature, 'action signature] => bool"
-  asig_comp    ::"['action signature, 'action signature] => 'action signature"
-  compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
-  par         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
+
+(* binary composition of action signatures and automata *)
 
-  (* Filtering and hiding *)
-  filter_oseq  :: "('a => bool) => 'a oseq => 'a oseq"
+definition compat_asigs ::"['action signature, 'action signature] => bool"
+  where "compat_asigs a1 a2 ==
+   (((outputs(a1) Int outputs(a2)) = {}) &
+    ((internals(a1) Int actions(a2)) = {}) &
+    ((internals(a2) Int actions(a1)) = {}))"
 
-  restrict_asig :: "['a signature, 'a set] => 'a signature"
-  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+definition compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
+  where "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
 
-  (* Notions of correctness *)
-  ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
-
-  (* Instantiation of abstract IOA by concrete actions *)
-  rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+definition asig_comp :: "['action signature, 'action signature] => 'action signature"
+  where "asig_comp a1 a2 ==
+      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
+        (outputs(a1) Un outputs(a2)),
+        (internals(a1) Un internals(a2))))"
 
-defs
-
-state_trans_def:
-  "state_trans asig R ==
-     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
-     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+definition par :: "[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
+  where "(ioa1 || ioa2) ==
+     (asig_comp (asig_of ioa1) (asig_of ioa2),
+      {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
+      {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+           in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
+              (if a:actions(asig_of(ioa1)) then
+                 (fst(s),a,fst(t)):trans_of(ioa1)
+               else fst(t) = fst(s))
+              &
+              (if a:actions(asig_of(ioa2)) then
+                 (snd(s),a,snd(t)):trans_of(ioa2)
+               else snd(t) = snd(s))})"
 
 
-asig_of_def:   "asig_of == fst"
-starts_of_def: "starts_of == (fst o snd)"
-trans_of_def:  "trans_of == (snd o snd)"
-
-ioa_def:
-  "IOA(ioa) == (is_asig(asig_of(ioa))      &
-                (~ starts_of(ioa) = {})    &
-                state_trans (asig_of ioa) (trans_of ioa))"
-
-
-(* An execution fragment is modelled with a pair of sequences:
- * the first is the action options, the second the state sequence.
- * Finite executions have None actions from some point on.
- *******)
-is_execution_fragment_def:
-  "is_execution_fragment A ex ==
-     let act = fst(ex); state = snd(ex)
-     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
-              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
-
-
-executions_def:
-  "executions(ioa) == {e. snd e 0:starts_of(ioa) &
-                        is_execution_fragment ioa e}"
-
-
-reachable_def:
-  "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
-
-
-invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
-
+(* Filtering and hiding *)
 
 (* Restrict the trace to those members of the set s *)
-filter_oseq_def:
-  "filter_oseq p s ==
+definition filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
+  where "filter_oseq p s ==
    (%i. case s(i)
          of None => None
           | Some(x) => if p x then Some x else None)"
 
-
-mk_trace_def:
-  "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
-
+definition mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
+  where "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
 
 (* Does an ioa have an execution with the given trace *)
-has_trace_def:
-  "has_trace ioa b ==
-     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
+definition has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
+  where "has_trace ioa b == (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
 
-normal_form_def:
-  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
+definition NF :: "'a oseq => 'a oseq"
+  where "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
                     (!j. j ~: range(f) --> nf(j)= None) &
-                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
+                    (!i. nf(i)=None --> (nf (Suc i)) = None)"
 
 (* All the traces of an ioa *)
-
-  traces_def:
-  "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
-
-(*
-  traces_def:
-  "traces(ioa) == {tr. has_trace ioa tr}"
-*)
-
-compat_asigs_def:
-  "compat_asigs a1 a2 ==
-   (((outputs(a1) Int outputs(a2)) = {}) &
-    ((internals(a1) Int actions(a2)) = {}) &
-    ((internals(a2) Int actions(a1)) = {}))"
-
-
-compat_ioas_def:
-  "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
+definition traces :: "('action,'state)ioa => 'action oseq set"
+  where "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
 
 
-asig_comp_def:
-  "asig_comp a1 a2 ==
-      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
-        (outputs(a1) Un outputs(a2)),
-        (internals(a1) Un internals(a2))))"
-
-
-par_def:
-  "(ioa1 || ioa2) ==
-       (asig_comp (asig_of ioa1) (asig_of ioa2),
-        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
-        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
-             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
-                (if a:actions(asig_of(ioa1)) then
-                   (fst(s),a,fst(t)):trans_of(ioa1)
-                 else fst(t) = fst(s))
-                &
-                (if a:actions(asig_of(ioa2)) then
-                   (snd(s),a,snd(t)):trans_of(ioa2)
-                 else snd(t) = snd(s))})"
-
-
-restrict_asig_def:
-  "restrict_asig asig actns ==
+definition restrict_asig :: "['a signature, 'a set] => 'a signature"
+  where "restrict_asig asig actns ==
     (inputs(asig) Int actns, outputs(asig) Int actns,
      internals(asig) Un (externals(asig) - actns))"
 
-
-restrict_def:
-  "restrict ioa actns ==
+definition restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+  where "restrict ioa actns ==
     (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
 
 
-ioa_implements_def:
-  "ioa_implements ioa1 ioa2 ==
+
+(* Notions of correctness *)
+
+definition ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
+  where "ioa_implements ioa1 ioa2 ==
   ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
      (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
       traces(ioa1) <= traces(ioa2))"
 
-rename_def:
-"rename ioa ren ==
-  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
-    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
-    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
-              starts_of(ioa)   ,
-   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
-        in
-        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
+
+(* Instantiation of abstract IOA by concrete actions *)
+
+definition rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+  where "rename ioa ren ==
+    (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
+      {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
+      {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
+                starts_of(ioa)   ,
+     {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
+          in
+          ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
 
 
 declare Let_def [simp]
@@ -206,7 +171,7 @@
 
 lemma trans_in_actions:
   "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"
-  apply (unfold ioa_def state_trans_def actions_def is_asig_def)
+  apply (unfold IOA_def state_trans_def actions_def is_asig_def)
   apply (erule conjE)+
   apply (erule allE, erule impE, assumption)
   apply simp
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -26,80 +26,67 @@
 type_synonym 'a item        = "('a, unit) node set"
 type_synonym ('a, 'b) dtree = "('a, 'b) node set"
 
-consts
-  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
-
-  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
-  ndepth    :: "('a, 'b) node => nat"
+definition Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
+  (*crude "lists" of nats -- needed for the constructions*)
+  where "Push == (%b h. case_nat b h)"
 
-  Atom      :: "('a + nat) => ('a, 'b) dtree"
-  Leaf      :: "'a => ('a, 'b) dtree"
-  Numb      :: "nat => ('a, 'b) dtree"
-  Scons     :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
-  In0       :: "('a, 'b) dtree => ('a, 'b) dtree"
-  In1       :: "('a, 'b) dtree => ('a, 'b) dtree"
-  Lim       :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
-
-  ntrunc    :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
-
-  uprod     :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
-  usum      :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
-
-  Split     :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
-  Case      :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
-
-  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
-                => (('a, 'b) dtree * ('a, 'b) dtree)set"
-  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
-                => (('a, 'b) dtree * ('a, 'b) dtree)set"
+definition Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
+  where "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
 
 
-defs
+(** operations on S-expressions -- sets of nodes **)
 
-  Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
-
-  (*crude "lists" of nats -- needed for the constructions*)
-  Push_def:   "Push == (%b h. case_nat b h)"
+(*S-expression constructors*)
+definition Atom :: "('a + nat) => ('a, 'b) dtree"
+  where "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
+definition Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
+  where "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
 
-  (** operations on S-expressions -- sets of nodes **)
+(*Leaf nodes, with arbitrary or nat labels*)
+definition Leaf :: "'a => ('a, 'b) dtree"
+  where "Leaf == Atom o Inl"
+definition Numb :: "nat => ('a, 'b) dtree"
+  where "Numb == Atom o Inr"
 
-  (*S-expression constructors*)
-  Atom_def:   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
-  Scons_def:  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
-
-  (*Leaf nodes, with arbitrary or nat labels*)
-  Leaf_def:   "Leaf == Atom o Inl"
-  Numb_def:   "Numb == Atom o Inr"
+(*Injections of the "disjoint sum"*)
+definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
+  where "In0(M) == Scons (Numb 0) M"
+definition In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
+  where "In1(M) == Scons (Numb 1) M"
 
-  (*Injections of the "disjoint sum"*)
-  In0_def:    "In0(M) == Scons (Numb 0) M"
-  In1_def:    "In1(M) == Scons (Numb 1) M"
+(*Function spaces*)
+definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
+  where "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
 
-  (*Function spaces*)
-  Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
+(*the set of nodes with depth less than k*)
+definition ndepth :: "('a, 'b) node => nat"
+  where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
+definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
+  where "ntrunc k N == {n. n:N & ndepth(n)<k}"
 
-  (*the set of nodes with depth less than k*)
-  ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
-  ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
+(*products and sums for the "universe"*)
+definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
+  where "uprod A B == UN x:A. UN y:B. { Scons x y }"
+definition usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
+  where "usum A B == In0`A Un In1`B"
 
-  (*products and sums for the "universe"*)
-  uprod_def:  "uprod A B == UN x:A. UN y:B. { Scons x y }"
-  usum_def:   "usum A B == In0`A Un In1`B"
+(*the corresponding eliminators*)
+definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
+  where "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
 
-  (*the corresponding eliminators*)
-  Split_def:  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
-
-  Case_def:   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x))
-                                  | (EX y . M = In1(y) & u = d(y))"
+definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
+  where "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) | (EX y . M = In1(y) & u = d(y))"
 
 
-  (** equality for the "universe" **)
-
-  dprod_def:  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
+(** equality for the "universe" **)
 
-  dsum_def:   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
-                          (UN (y,y'):s. {(In1(y),In1(y'))})"
+definition dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
+      => (('a, 'b) dtree * ('a, 'b) dtree)set"
+  where "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
 
+definition dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
+      => (('a, 'b) dtree * ('a, 'b) dtree)set"
+  where "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un (UN (y,y'):s. {(In1(y),In1(y'))})"
 
 
 lemma apfst_convE: 
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -15,23 +15,26 @@
 type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
 
-consts
-  "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
-  "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
-  "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" 
-(*<*)
+definition lesub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
+  where "lesub x r y \<longleftrightarrow> r x y"
+
+definition lesssub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
+  where "lesssub x r y \<longleftrightarrow> lesub x r y \<and> x \<noteq> y"
+
+definition plussub :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
+  where "plussub x f y = f x y"
+
 notation (ASCII)
   "lesub"  ("(_ /<='__ _)" [50, 1000, 51] 50) and
   "lesssub"  ("(_ /<'__ _)" [50, 1000, 51] 50) and
   "plussub"  ("(_ /+'__ _)" [65, 1000, 66] 65)
-(*>*)
+
 notation
   "lesub"  ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
   "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
   "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
-(*<*)
+
 (* allow \<sub> instead of \<bsub>..\<esub> *)
-
 abbreviation (input)
   lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
   where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
@@ -43,12 +46,6 @@
 abbreviation (input)
   plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
   where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
-(*>*)
-
-defs
-  lesub_def:   "x \<sqsubseteq>\<^sub>r y \<equiv> r x y"
-  lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y"
-  plussub_def: "x \<squnion>\<^sub>f y \<equiv> f x y"
 
 definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where
   "ord r \<equiv> \<lambda>x y. (x,y) \<in> r"
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -82,31 +82,33 @@
 declare Base_not_Xcpt [symmetric, simp]
 declare Ext_not_Xcpt  [symmetric, simp]
 
-consts
-  foo_Base::  java_mb
-  foo_Ext ::  java_mb
-  BaseC   :: "java_mb cdecl"
-  ExtC    :: "java_mb cdecl"
-  test    ::  stmt
-  foo   ::  mname
-  a   ::  loc
-  b       ::  loc
+definition foo_Base :: java_mb
+  where "foo_Base == ([x],[],Skip,LAcc x)"
 
-defs
-  foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
-  BaseC_def:"BaseC == (Base, (Object, 
+definition foo_Ext :: java_mb
+  where "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
+               (LAcc x)..vee:=Lit (Intg Numeral1)),
+           Lit Null)"
+
+consts foo ::  mname
+
+definition BaseC :: "java_mb cdecl"
+  where "BaseC == (Base, (Object, 
            [(vee, PrimT Boolean)], 
            [((foo,[Class Base]),Class Base,foo_Base)]))"
-  foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
-               (LAcc x)..vee:=Lit (Intg Numeral1)),
-           Lit Null)"
-  ExtC_def: "ExtC  == (Ext,  (Base  , 
+
+definition ExtC :: "java_mb cdecl"
+  where "ExtC  == (Ext,  (Base  ,
            [(vee, PrimT Integer)], 
            [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
-  test_def:"test == Expr(e::=NewC Ext);; 
+definition test ::  stmt
+  where "test == Expr(e::=NewC Ext);;
                     Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
 
+consts
+  a :: loc
+  b :: loc
 
 abbreviation
   NP  :: xcpt where
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -176,14 +176,18 @@
     by(rule finite_acyclic_wf_converse[OF finite_subcls1])
 qed
 
-consts
-  "method" :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
-  field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
-  fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
+definition "method" :: "'c prog \<times> cname => (sig \<rightharpoonup> cname \<times> ty \<times> 'c)"
+  \<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
+  where [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
+                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
 
-\<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
-defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
-                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
+definition fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list"
+  \<comment> "list of fields of a class, including inherited and hidden ones"
+  where [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
+                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
+
+definition field :: "'c prog \<times> cname => (vname \<rightharpoonup> cname \<times> ty)"
+  where [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
 
 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   method (G,C) = (if C = Object then empty else method (G,D)) ++  
@@ -194,11 +198,6 @@
 apply auto
 done
 
-
-\<comment> "list of fields of a class, including inherited and hidden ones"
-defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
-                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
-
 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
  fields (G,C) = 
   map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
@@ -208,9 +207,6 @@
 apply auto
 done
 
-
-defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
-
 lemma field_fields: 
 "field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
 apply (unfold field_def)
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -33,24 +33,20 @@
   localT :: "'c env => (vname \<rightharpoonup> ty)"
   where "localT == snd"
 
-consts
-  more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
-                (ty \<times> 'x) \<times> ty list => bool"
-  appl_methds :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
-  max_spec :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
+definition more_spec :: "'c prog \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> bool"
+  where "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
+                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
 
-defs
-  more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
-                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
-  
+definition appl_methds :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
   \<comment> "applicable methods, cf. 15.11.2.1"
-  appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
+  where "appl_methds G C == \<lambda>(mn, pTs).
                      {((Class md,rT),pTs') |md rT mb pTs'.
                       method (G,C)  (mn, pTs') = Some (md,rT,mb) \<and>
                       list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
 
+definition max_spec :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
   \<comment> "maximally specific methods, cf. 15.11.2.2"
-  max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
+  where "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
                                        (\<forall>m'\<in>appl_methds G C sig.
                                          more_spec G m' m --> m' = m)}"
 
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -1273,10 +1273,20 @@
 
 consts inverse :: "'a \<Rightarrow> 'a"
 
-defs (overloaded)
-inverse_bool: "inverse (b::bool) \<equiv> \<not> b"
-inverse_set: "inverse (S::'a set) \<equiv> -S"
-inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
+overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
+begin
+  definition "inverse (b::bool) \<equiv> \<not> b"
+end
+
+overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
+begin
+  definition "inverse (S::'a set) \<equiv> -S"
+end
+
+overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
+begin
+  definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
+end
 
 lemma "inverse b"
 nitpick [expect = genuine]
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -2416,11 +2416,15 @@
 consts
   fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
 
-defs (overloaded)
-  fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
-
-defs (overloaded)
-  fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
+overloading fresh_star_set \<equiv> "fresh_star :: 'b set \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+  definition fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>xs. x\<sharp>(c::'a)"
+end
+
+overloading frsh_star_list \<equiv> "fresh_star :: 'b list \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+  definition fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>set xs. x\<sharp>(c::'a)"
+end
 
 lemmas fresh_star_def = fresh_star_list fresh_star_set
 
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/TLA/Buffer/Buffer.thy
--- a/src/HOL/TLA/Buffer/Buffer.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -8,31 +8,35 @@
 imports "../TLA"
 begin
 
-consts
-  (* actions *)
-  BInit     :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
-  Enq       :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
-  Deq       :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
-  Next      :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+(* actions *)
+
+definition BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
+  where "BInit ic q oc == PRED q = #[]"
 
-  (* temporal formulas *)
-  IBuffer   :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
-  Buffer    :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+definition Enq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+  where "Enq ic q oc == ACT (ic$ \<noteq> $ic)
+                         \<and> (q$ = $q @ [ ic$ ])
+                         \<and> (oc$ = $oc)"
 
-defs
-  BInit_def:   "BInit ic q oc    == PRED q = #[]"
-  Enq_def:     "Enq ic q oc      == ACT (ic$ \<noteq> $ic)
-                                     \<and> (q$ = $q @ [ ic$ ])
-                                     \<and> (oc$ = $oc)"
-  Deq_def:     "Deq ic q oc      == ACT ($q \<noteq> #[])
-                                     \<and> (oc$ = hd< $q >)
-                                     \<and> (q$ = tl< $q >)
-                                     \<and> (ic$ = $ic)"
-  Next_def:    "Next ic q oc     == ACT (Enq ic q oc \<or> Deq ic q oc)"
-  IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
-                                      \<and> \<box>[Next ic q oc]_(ic,q,oc)
-                                      \<and> WF(Deq ic q oc)_(ic,q,oc)"
-  Buffer_def:  "Buffer ic oc     == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
+definition Deq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+  where "Deq ic q oc == ACT ($q \<noteq> #[])
+                         \<and> (oc$ = hd< $q >)
+                         \<and> (q$ = tl< $q >)
+                         \<and> (ic$ = $ic)"
+
+definition Next :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+  where "Next ic q oc == ACT (Enq ic q oc \<or> Deq ic q oc)"
+
+
+(* temporal formulas *)
+
+definition IBuffer :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+  where "IBuffer ic q oc == TEMP Init (BInit ic q oc)
+                                  \<and> \<box>[Next ic q oc]_(ic,q,oc)
+                                  \<and> WF(Deq ic q oc)_(ic,q,oc)"
+
+definition Buffer :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+  where "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
 
 
 (* ---------------------------- Data lemmas ---------------------------- *)
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Init.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -35,10 +35,17 @@
 defs
   Init_def:    "sigma \<Turnstile> Init F  ==  (first_world sigma) \<Turnstile> F"
 
-defs (overloaded)
-  fw_temp_def: "first_world == \<lambda>sigma. sigma"
-  fw_stp_def:  "first_world == st1"
-  fw_act_def:  "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
+overloading
+  fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
+  fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
+  fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> state"
+begin
+
+definition "first_world == \<lambda>sigma. sigma"
+definition "first_world == st1"
+definition "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
+
+end
 
 lemma const_simps [int_rewrite, simp]:
   "\<turnstile> (Init #True) = #True"
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -12,122 +12,135 @@
 type_synonym memType = "(Locs \<Rightarrow> Vals) stfun"  (* intention: MemLocs \<Rightarrow> MemVals *)
 type_synonym resType = "(PrIds \<Rightarrow> Vals) stfun"
 
-consts
-  (* state predicates *)
-  MInit      :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
-  PInit      :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
-  (* auxiliary predicates: is there a pending read/write request for
-     some process id and location/value? *)
-  RdRequest  :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
-  WrRequest  :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
+
+(* state predicates *)
+
+definition MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+  where "MInit mm l == PRED mm!l = #InitVal"
+
+definition PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
+  where "PInit rs p == PRED rs!p = #NotAResult"
+
+
+(* auxiliary predicates: is there a pending read/write request for
+   some process id and location/value? *)
+
+definition RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
+  where "RdRequest ch p l == PRED Calling ch p \<and> (arg<ch!p> = #(read l))"
+
+definition WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
+  where "WrRequest ch p l v == PRED Calling ch p \<and> (arg<ch!p> = #(write l v))"
+
+
+(* actions *)
+
+(* a read that doesn't raise BadArg *)
+definition GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+  where "GoodRead mm rs p l == ACT #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
+
+(* a read that raises BadArg *)
+definition BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+  where "BadRead mm rs p l == ACT #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
 
-  (* actions *)
-  GoodRead   :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
-  BadRead    :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
-  ReadInner  :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
-  Read       :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
-  GoodWrite  :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
-  BadWrite   :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
-  WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
-  Write      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
-  MemReturn  :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
-  MemFail    :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
-  RNext      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
-  UNext      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+(* the read action with l visible *)
+definition ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+  where "ReadInner ch mm rs p l == ACT
+    $(RdRequest ch p l)
+    \<and> (GoodRead mm rs p l  \<or>  BadRead mm rs p l)
+    \<and> unchanged (rtrner ch ! p)"
+
+(* the read action with l quantified *)
+definition Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
 
-  (* temporal formulas *)
-  RPSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
-  UPSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
-  MSpec      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
-  IRSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
-  IUSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+(* similar definitions for the write action *)
+definition GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+  where "GoodWrite mm rs p l v ==
+    ACT #l \<in> #MemLoc \<and> #v \<in> #MemVal
+      \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
 
-  RSpec      :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
-  USpec      :: "memChType \<Rightarrow> temporal"
+definition BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+  where "BadWrite mm rs p l v == ACT
+    \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
+    \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
 
-  (* memory invariant: in the paper, the invariant is hidden in the definition of
-     the predicate S used in the implementation proof, but it is easier to verify
-     at this level. *)
-  MemInv    :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+definition WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+  where "WriteInner ch mm rs p l v == ACT
+    $(WrRequest ch p l v)
+    \<and> (GoodWrite mm rs p l v  \<or>  BadWrite mm rs p l v)
+    \<and> unchanged (rtrner ch ! p)"
 
-defs
-  MInit_def:         "MInit mm l == PRED mm!l = #InitVal"
-  PInit_def:         "PInit rs p == PRED rs!p = #NotAResult"
+definition Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+  where "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
+
 
-  RdRequest_def:     "RdRequest ch p l == PRED
-                         Calling ch p \<and> (arg<ch!p> = #(read l))"
-  WrRequest_def:     "WrRequest ch p l v == PRED
-                         Calling ch p \<and> (arg<ch!p> = #(write l v))"
-  (* a read that doesn't raise BadArg *)
-  GoodRead_def:      "GoodRead mm rs p l == ACT
-                        #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
-  (* a read that raises BadArg *)
-  BadRead_def:       "BadRead mm rs p l == ACT
-                        #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
-  (* the read action with l visible *)
-  ReadInner_def:     "ReadInner ch mm rs p l == ACT
-                         $(RdRequest ch p l)
-                         \<and> (GoodRead mm rs p l  \<or>  BadRead mm rs p l)
-                         \<and> unchanged (rtrner ch ! p)"
-  (* the read action with l quantified *)
-  Read_def:          "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
+(* the return action *)
+definition MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "MemReturn ch rs p == ACT
+   (   ($(rs!p) \<noteq> #NotAResult)
+    \<and> ((rs!p)$ = #NotAResult)
+    \<and> Return ch p (rs!p))"
+
+(* the failure action of the unreliable memory *)
+definition MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "MemFail ch rs p == ACT
+    $(Calling ch p)
+    \<and> ((rs!p)$ = #MemFailure)
+    \<and> unchanged (rtrner ch ! p)"
 
-  (* similar definitions for the write action *)
-  GoodWrite_def:     "GoodWrite mm rs p l v == ACT
-                        #l \<in> #MemLoc \<and> #v \<in> #MemVal
-                        \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
-  BadWrite_def:      "BadWrite mm rs p l v == ACT
-                        \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
-                        \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
-  WriteInner_def:    "WriteInner ch mm rs p l v == ACT
-                        $(WrRequest ch p l v)
-                        \<and> (GoodWrite mm rs p l v  \<or>  BadWrite mm rs p l v)
-                        \<and> unchanged (rtrner ch ! p)"
-  Write_def:         "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
+(* next-state relations for reliable / unreliable memory *)
+definition RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RNext ch mm rs p == ACT
+   (  Read ch mm rs p
+    \<or> (\<exists>l. Write ch mm rs p l)
+    \<or> MemReturn ch rs p)"
+
+definition UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "UNext ch mm rs p == ACT (RNext ch mm rs p \<or> MemFail ch rs p)"
 
-  (* the return action *)
-  MemReturn_def:     "MemReturn ch rs p == ACT
-                       (   ($(rs!p) \<noteq> #NotAResult)
-                        \<and> ((rs!p)$ = #NotAResult)
-                        \<and> Return ch p (rs!p))"
+
+(* temporal formulas *)
+
+definition RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "RPSpec ch mm rs p == TEMP
+    Init(PInit rs p)
+    \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+    \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+    \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
 
-  (* the failure action of the unreliable memory *)
-  MemFail_def:       "MemFail ch rs p == ACT
-                        $(Calling ch p)
-                        \<and> ((rs!p)$ = #MemFailure)
-                        \<and> unchanged (rtrner ch ! p)"
-  (* next-state relations for reliable / unreliable memory *)
-  RNext_def:         "RNext ch mm rs p == ACT
-                       (  Read ch mm rs p
-                        \<or> (\<exists>l. Write ch mm rs p l)
-                        \<or> MemReturn ch rs p)"
-  UNext_def:         "UNext ch mm rs p == ACT
-                        (RNext ch mm rs p \<or> MemFail ch rs p)"
+definition UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "UPSpec ch mm rs p == TEMP
+    Init(PInit rs p)
+    \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+    \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+    \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
+
+definition MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
+  where "MSpec ch mm rs l == TEMP
+    Init(MInit mm l)
+    \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
+
+definition IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+  where "IRSpec ch mm rs == TEMP
+    (\<forall>p. RPSpec ch mm rs p)
+    \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
 
-  RPSpec_def:        "RPSpec ch mm rs p == TEMP
-                        Init(PInit rs p)
-                        \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
-                        \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
-                        \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
-  UPSpec_def:        "UPSpec ch mm rs p == TEMP
-                        Init(PInit rs p)
-                        \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
-                        \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
-                        \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
-  MSpec_def:         "MSpec ch mm rs l == TEMP
-                        Init(MInit mm l)
-                        \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
-  IRSpec_def:        "IRSpec ch mm rs == TEMP
-                        (\<forall>p. RPSpec ch mm rs p)
-                        \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
-  IUSpec_def:        "IUSpec ch mm rs == TEMP
-                        (\<forall>p. UPSpec ch mm rs p)
-                        \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+definition IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+  where "IUSpec ch mm rs == TEMP
+    (\<forall>p. UPSpec ch mm rs p)
+    \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+
+definition RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
+  where "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
 
-  RSpec_def:         "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
-  USpec_def:         "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
+definition USpec :: "memChType \<Rightarrow> temporal"
+  where "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
 
-  MemInv_def:        "MemInv mm l == PRED  #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
+(* memory invariant: in the paper, the invariant is hidden in the definition of
+   the predicate S used in the implementation proof, but it is easier to verify
+   at this level. *)
+definition MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+  where "MemInv mm l == PRED  #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
 
 lemmas RM_action_defs =
   MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -16,65 +16,78 @@
   *)
 type_synonym ('a,'r) channel =" (PrIds \<Rightarrow> ('a,'r) chan) stfun"
 
+
+(* data-level functions *)
+
 consts
-  (* data-level functions *)
   cbit          :: "('a,'r) chan \<Rightarrow> bit"
   rbit          :: "('a,'r) chan \<Rightarrow> bit"
   arg           :: "('a,'r) chan \<Rightarrow> 'a"
   res           :: "('a,'r) chan \<Rightarrow> 'r"
 
-  (* state functions *)
-  caller        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
-  rtrner        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
+
+(* state functions *)
 
-  (* state predicates *)
-  Calling   :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
+definition caller :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
+  where "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
 
-  (* actions *)
-  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
-  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+definition rtrner :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
+  where "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))"
+
 
-  (* temporal formulas *)
-  PLegalCaller      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
-  LegalCaller       :: "('a,'r) channel \<Rightarrow> temporal"
-  PLegalReturner    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
-  LegalReturner     :: "('a,'r) channel \<Rightarrow> temporal"
+(* slice through array-valued state function *)
 
-  (* slice through array-valued state function *)
+consts
   slice        :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
-
 syntax
   "_slice"    :: "[lift, 'a] \<Rightarrow> lift"      ("(_!_)" [70,70] 70)
-
-  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
-  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
-
 translations
   "_slice"  ==  "CONST slice"
-
-  "_Call"   ==  "CONST ACall"
-  "_Return" ==  "CONST AReturn"
-
 defs
   slice_def:     "(PRED (x!i)) s == x s i"
 
-  caller_def:    "caller ch   == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
-  rtrner_def:    "rtrner ch   == \<lambda>s p. (rbit (ch s p), res (ch s p))"
+
+(* state predicates *)
+
+definition Calling :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
+  where "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
+
+
+(* actions *)
 
-  Calling_def:   "Calling ch p  == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
+consts
+  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
+  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+syntax
+  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
+  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
+translations
+  "_Call"   ==  "CONST ACall"
+  "_Return" ==  "CONST AReturn"
+defs
   Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
                                      \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
                                      \<and> (arg<ch!p>$ = $v)"
   Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
                                      \<and> (rbit<ch!p>$ = $cbit<ch!p>)
                                      \<and> (res<ch!p>$ = $v)"
-  PLegalCaller_def:      "PLegalCaller ch p == TEMP
-                             Init(\<not> Calling ch p)
-                             \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
-  LegalCaller_def:       "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
-  PLegalReturner_def:    "PLegalReturner ch p == TEMP
-                                \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
-  LegalReturner_def:     "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
+
+
+(* temporal formulas *)
+
+definition PLegalCaller :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "PLegalCaller ch p == TEMP
+     Init(\<not> Calling ch p)
+     \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
+
+definition LegalCaller :: "('a,'r) channel \<Rightarrow> temporal"
+  where "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
+
+definition PLegalReturner :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "PLegalReturner ch p == TEMP \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
+
+definition LegalReturner :: "('a,'r) channel \<Rightarrow> temporal"
+  where "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
 
 declare slice_def [simp]
 
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -12,63 +12,64 @@
 type_synonym rpcRcvChType = "memChType"
 type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun"
 
-consts
-  (* state predicates *)
-  RPCInit      :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
+
+(* state predicates *)
 
-  (* actions *)
-  RPCFwd     :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
-  RPCReject  :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
-  RPCFail    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
-  RPCReply   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
-  RPCNext    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+definition RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
+  where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
+
+
+(* actions *)
 
-  (* temporal *)
-  RPCIPSpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
-  RPCISpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
-
-defs
-  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
+definition RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCFwd send rcv rst p == ACT
+      $(Calling send p)
+    \<and> $(rst!p) = # rpcA
+    \<and> IsLegalRcvArg<arg<$(send!p)>>
+    \<and> Call rcv p RPCRelayArg<arg<send!p>>
+    \<and> (rst!p)$ = # rpcB
+    \<and> unchanged (rtrner send!p)"
 
-  RPCFwd_def:        "RPCFwd send rcv rst p == ACT
-                         $(Calling send p)
-                         \<and> $(rst!p) = # rpcA
-                         \<and> IsLegalRcvArg<arg<$(send!p)>>
-                         \<and> Call rcv p RPCRelayArg<arg<send!p>>
-                         \<and> (rst!p)$ = # rpcB
-                         \<and> unchanged (rtrner send!p)"
+definition RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCReject send rcv rst p == ACT
+      $(rst!p) = # rpcA
+    \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
+    \<and> Return send p #BadCall
+    \<and> unchanged ((rst!p), (caller rcv!p))"
 
-  RPCReject_def:     "RPCReject send rcv rst p == ACT
-                           $(rst!p) = # rpcA
-                         \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
-                         \<and> Return send p #BadCall
-                         \<and> unchanged ((rst!p), (caller rcv!p))"
+definition RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCFail send rcv rst p == ACT
+      \<not>$(Calling rcv p)
+    \<and> Return send p #RPCFailure
+    \<and> (rst!p)$ = #rpcA
+    \<and> unchanged (caller rcv!p)"
 
-  RPCFail_def:       "RPCFail send rcv rst p == ACT
-                           \<not>$(Calling rcv p)
-                         \<and> Return send p #RPCFailure
-                         \<and> (rst!p)$ = #rpcA
-                         \<and> unchanged (caller rcv!p)"
+definition RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCReply send rcv rst p == ACT
+      \<not>$(Calling rcv p)
+    \<and> $(rst!p) = #rpcB
+    \<and> Return send p res<rcv!p>
+    \<and> (rst!p)$ = #rpcA
+    \<and> unchanged (caller rcv!p)"
 
-  RPCReply_def:      "RPCReply send rcv rst p == ACT
-                           \<not>$(Calling rcv p)
-                         \<and> $(rst!p) = #rpcB
-                         \<and> Return send p res<rcv!p>
-                         \<and> (rst!p)$ = #rpcA
-                         \<and> unchanged (caller rcv!p)"
+definition RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCNext send rcv rst p == ACT
+    (  RPCFwd send rcv rst p
+     \<or> RPCReject send rcv rst p
+     \<or> RPCFail send rcv rst p
+     \<or> RPCReply send rcv rst p)"
+
 
-  RPCNext_def:       "RPCNext send rcv rst p == ACT
-                        (  RPCFwd send rcv rst p
-                         \<or> RPCReject send rcv rst p
-                         \<or> RPCFail send rcv rst p
-                         \<or> RPCReply send rcv rst p)"
+(* temporal *)
 
-  RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
-                           Init RPCInit rcv rst p
-                         \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
-                         \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
+definition RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "RPCIPSpec send rcv rst p == TEMP
+     Init RPCInit rcv rst p
+   \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
+   \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
 
-  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
+definition RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
+  where "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
 
 
 lemmas RPC_action_defs =
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/TLA/Memory/RPCParameters.thy
--- a/src/HOL/TLA/Memory/RPCParameters.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/RPCParameters.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -16,32 +16,28 @@
 datatype rpcOp = memcall memOp | othercall Vals
 datatype rpcState = rpcA | rpcB
 
-consts
-  (* some particular return values *)
-  RPCFailure     :: Vals
-  BadCall        :: Vals
-  
-  (* Translate an rpc call to a memory call and test if the current argument
-     is legal for the receiver (i.e., the memory). This can now be a little
-     simpler than for the generic RPC component. RelayArg returns an arbitrary
-     memory call for illegal arguments. *)
-  IsLegalRcvArg  :: "rpcOp \<Rightarrow> bool"
-  RPCRelayArg    :: "rpcOp \<Rightarrow> memOp"
-
-axiomatization where
+axiomatization RPCFailure :: Vals and BadCall :: Vals
+where
   (* RPCFailure is different from MemVals and exceptions *)
   RFNoMemVal:        "RPCFailure \<notin> MemVal" and
   NotAResultNotRF:   "NotAResult \<noteq> RPCFailure" and
   OKNotRF:           "OK \<noteq> RPCFailure" and
   BANotRF:           "BadArg \<noteq> RPCFailure"
 
-defs
-  IsLegalRcvArg_def: "IsLegalRcvArg ra ==
-                         case ra of (memcall m) \<Rightarrow> True
-                                  | (othercall v) \<Rightarrow> False"
-  RPCRelayArg_def:   "RPCRelayArg ra ==
-                         case ra of (memcall m) \<Rightarrow> m
-                                  | (othercall v) \<Rightarrow> undefined"
+(* Translate an rpc call to a memory call and test if the current argument
+   is legal for the receiver (i.e., the memory). This can now be a little
+   simpler than for the generic RPC component. RelayArg returns an arbitrary
+   memory call for illegal arguments. *)
+
+definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
+  where "IsLegalRcvArg ra ==
+    case ra of (memcall m) \<Rightarrow> True
+             | (othercall v) \<Rightarrow> False"
+
+definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
+  where "RPCRelayArg ra ==
+    case ra of (memcall m) \<Rightarrow> m
+             | (othercall v) \<Rightarrow> undefined"
 
 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
   NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Stfun.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -40,15 +40,17 @@
   "PRED P"   =>  "(P::state \<Rightarrow> _)"
   "_stvars"  ==  "CONST stvars"
 
-defs
-  (* Base variables may be assigned arbitrary (type-correct) values.
-     Note that vs may be a tuple of variables. The correct identification
-     of base variables is up to the user who must take care not to
-     introduce an inconsistency. For example, "basevars (x,x)" would
-     definitely be inconsistent.
-  *)
-  basevars_def:  "stvars vs == range vs = UNIV"
-
+(* Base variables may be assigned arbitrary (type-correct) values.
+   Note that vs may be a tuple of variables. The correct identification
+   of base variables is up to the user who must take care not to
+   introduce an inconsistency. For example, "basevars (x,x)" would
+   definitely be inconsistent.
+*)
+overloading stvars \<equiv> stvars
+begin
+  definition stvars :: "(state \<Rightarrow> 'a) \<Rightarrow> bool"
+    where basevars_def: "stvars vs == range vs = UNIV"
+end
 
 lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>u. vs u = c"
   apply (unfold basevars_def)
diff -r bdab93ccfaf8 -r 5b946c81dfbf src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/ex/MT.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -60,21 +60,7 @@
   te_app :: "[TyEnv, ExVar] => Ty"
   te_dom :: "TyEnv => ExVar set"
 
-  eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
-  eval_rel :: "((ValEnv * Ex) * Val) set"
-  eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
-
-  elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
-  elab_rel :: "((TyEnv * Ex) * Ty) set"
-  elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
-
   isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
-  isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
-
-  hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
-  hasty_rel :: "(Val * Ty) set"
-  hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
-  hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
 
 (*
   Expression constructors must be injective, distinct and it must be possible
@@ -185,9 +171,8 @@
 derived.
 *)
 
-defs
-  eval_fun_def:
-    " eval_fun(s) ==
+definition eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
+  where "eval_fun(s) ==
      { pp.
        (? ve c. pp=((ve,e_const(c)),v_const(c))) |
        (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
@@ -208,51 +193,56 @@
        )
      }"
 
-  eval_rel_def: "eval_rel == lfp(eval_fun)"
-  eval_def: "ve |- e ---> v == ((ve,e),v):eval_rel"
+definition eval_rel :: "((ValEnv * Ex) * Val) set"
+  where "eval_rel == lfp(eval_fun)"
+
+definition eval :: "[ValEnv, Ex, Val] => bool"  ("_ |- _ ---> _" [36,0,36] 50)
+  where "ve |- e ---> v == ((ve,e),v) \<in> eval_rel"
 
 (* The static semantics is defined in the same way as the dynamic
 semantics.  The relation te |- e ===> t express the expression e has the
 type t in the type environment te.
 *)
 
-  elab_fun_def:
-  "elab_fun(s) ==
-  { pp.
-    (? te c t. pp=((te,e_const(c)),t) & c isof t) |
-    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
-    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
-    (? te f x e t1 t2.
-       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
-    ) |
-    (? te e1 e2 t1 t2.
-       pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
-    )
-  }"
+definition elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
+  where "elab_fun(s) ==
+    { pp.
+      (? te c t. pp=((te,e_const(c)),t) & c isof t) |
+      (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
+      (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
+      (? te f x e t1 t2.
+         pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
+      ) |
+      (? te e1 e2 t1 t2.
+         pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
+      )
+    }"
 
-  elab_rel_def: "elab_rel == lfp(elab_fun)"
-  elab_def: "te |- e ===> t == ((te,e),t):elab_rel"
+definition elab_rel :: "((TyEnv * Ex) * Ty) set"
+  where "elab_rel == lfp(elab_fun)"
+
+definition elab :: "[TyEnv, Ex, Ty] => bool"  ("_ |- _ ===> _" [36,0,36] 50)
+  where "te |- e ===> t == ((te,e),t):elab_rel"
+
 
 (* The original correspondence relation *)
 
-  isof_env_def:
-    " ve isofenv te ==
-     ve_dom(ve) = te_dom(te) &
-     ( ! x.
+definition isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
+  where "ve isofenv te ==
+    ve_dom(ve) = te_dom(te) &
+     (! x.
          x:ve_dom(ve) -->
-         (? c. ve_app ve x = v_const(c) & c isof te_app te x)
-     )
-   "
+         (? c. ve_app ve x = v_const(c) & c isof te_app te x))"
 
 axiomatization where
   isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
 
-defs
+
 (* The extented correspondence relation *)
 
-  hasty_fun_def:
-    " hasty_fun(r) ==
-     { p.
+definition hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
+  where "hasty_fun(r) ==
+    { p.
        ( ? c t. p = (v_const(c),t) & c isof t) |
        ( ? ev e ve t te.
            p = (v_clos(<|ev,e,ve|>),t) &
@@ -260,15 +250,18 @@
            ve_dom(ve) = te_dom(te) &
            (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
        )
-     }
-   "
+    }"
+
+definition hasty_rel :: "(Val * Ty) set"
+  where "hasty_rel == gfp(hasty_fun)"
 
-  hasty_rel_def: "hasty_rel == gfp(hasty_fun)"
-  hasty_def: "v hasty t == (v,t) : hasty_rel"
-  hasty_env_def:
-    " ve hastyenv te ==
-     ve_dom(ve) = te_dom(te) &
-     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
+definition hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
+  where "v hasty t == (v,t) : hasty_rel"
+
+definition hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
+  where "ve hastyenv te ==
+    ve_dom(ve) = te_dom(te) &
+      (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
 
 
 (* ############################################################ *)