modernized translations;
authorwenzelm
Wed Feb 10 23:53:46 2010 +0100 (2010-02-10)
changeset 351016ce9177d6b38
parent 35100 53754ec7360b
child 35102 cc7a0b9f938c
modernized translations;
src/HOL/Hoare/HeapSyntax.thy
src/HOL/Hoare/HeapSyntaxAbort.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/Pointers0.thy
src/HOL/Hoare/Separation.thy
src/HOL/SET_Protocol/Event_SET.thy
     1.1 --- a/src/HOL/Hoare/HeapSyntax.thy	Wed Feb 10 19:37:34 2010 +0100
     1.2 +++ b/src/HOL/Hoare/HeapSyntax.thy	Wed Feb 10 23:53:46 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Hoare/HeapSyntax.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7      Copyright   2002 TUM
     1.8  *)
     1.9 @@ -9,16 +8,16 @@
    1.10  subsection "Field access and update"
    1.11  
    1.12  syntax
    1.13 -  "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    1.14 +  "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    1.15     ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
    1.16 -  "@fassign"  :: "'a ref => id => 'v => 's com"
    1.17 +  "_fassign"  :: "'a ref => id => 'v => 's com"
    1.18     ("(2_^._ :=/ _)" [70,1000,65] 61)
    1.19 -  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    1.20 +  "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    1.21     ("_^._" [65,1000] 65)
    1.22  translations
    1.23 -  "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
    1.24 +  "f(r \<rightarrow> v)"  ==  "f(CONST addr r := v)"
    1.25    "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
    1.26 -  "p^.f"       =>  "f(addr p)"
    1.27 +  "p^.f"       =>  "f(CONST addr p)"
    1.28  
    1.29  
    1.30  declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
     2.1 --- a/src/HOL/Hoare/HeapSyntaxAbort.thy	Wed Feb 10 19:37:34 2010 +0100
     2.2 +++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Wed Feb 10 23:53:46 2010 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Hoare/HeapSyntax.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Tobias Nipkow
     2.7      Copyright   2002 TUM
     2.8  *)
     2.9 @@ -17,16 +16,16 @@
    2.10  reason about storage allocation/deallocation. *}
    2.11  
    2.12  syntax
    2.13 -  "refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    2.14 +  "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    2.15     ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
    2.16 -  "@fassign"  :: "'a ref => id => 'v => 's com"
    2.17 +  "_fassign"  :: "'a ref => id => 'v => 's com"
    2.18     ("(2_^._ :=/ _)" [70,1000,65] 61)
    2.19 -  "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    2.20 +  "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    2.21     ("_^._" [65,1000] 65)
    2.22  translations
    2.23 -  "refupdate f r v"  ==  "f(addr r := v)"
    2.24 -  "p^.f := e"  =>  "(p \<noteq> Null) \<rightarrow> (f := refupdate f p e)"
    2.25 -  "p^.f"       =>  "f(addr p)"
    2.26 +  "_refupdate f r v"  ==  "f(CONST addr r := v)"
    2.27 +  "p^.f := e"  =>  "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
    2.28 +  "p^.f"       =>  "f(CONST addr p)"
    2.29  
    2.30  
    2.31  declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
     3.1 --- a/src/HOL/Hoare/HoareAbort.thy	Wed Feb 10 19:37:34 2010 +0100
     3.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Wed Feb 10 23:53:46 2010 +0100
     3.3 @@ -257,7 +257,7 @@
     3.4    guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
     3.5    array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
     3.6  translations
     3.7 -  "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
     3.8 +  "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
     3.9    "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
    3.10    (* reverse translation not possible because of duplicate "a" *)
    3.11  
     4.1 --- a/src/HOL/Hoare/Pointers0.thy	Wed Feb 10 19:37:34 2010 +0100
     4.2 +++ b/src/HOL/Hoare/Pointers0.thy	Wed Feb 10 23:53:46 2010 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Hoare/Pointers.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Tobias Nipkow
     4.7      Copyright   2002 TUM
     4.8  
     4.9 @@ -20,12 +19,12 @@
    4.10  subsection "Field access and update"
    4.11  
    4.12  syntax
    4.13 -  "@fassign"  :: "'a::ref => id => 'v => 's com"
    4.14 +  "_fassign"  :: "'a::ref => id => 'v => 's com"
    4.15     ("(2_^._ :=/ _)" [70,1000,65] 61)
    4.16 -  "@faccess"  :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
    4.17 +  "_faccess"  :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
    4.18     ("_^._" [65,1000] 65)
    4.19  translations
    4.20 -  "p^.f := e"  =>  "f := fun_upd f p e"
    4.21 +  "p^.f := e"  =>  "f := CONST fun_upd f p e"
    4.22    "p^.f"       =>  "f p"
    4.23  
    4.24  
     5.1 --- a/src/HOL/Hoare/Separation.thy	Wed Feb 10 19:37:34 2010 +0100
     5.2 +++ b/src/HOL/Hoare/Separation.thy	Wed Feb 10 23:53:46 2010 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Hoare/Separation.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Tobias Nipkow
     5.7      Copyright   2003 TUM
     5.8  
     5.9 @@ -50,10 +49,10 @@
    5.10  bound Hs - otherwise they may bind the implicit H. *}
    5.11  
    5.12  syntax
    5.13 - "@emp" :: "bool" ("emp")
    5.14 - "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
    5.15 - "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
    5.16 - "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
    5.17 + "_emp" :: "bool" ("emp")
    5.18 + "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
    5.19 + "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
    5.20 + "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
    5.21  
    5.22  (* FIXME does not handle "_idtdummy" *)
    5.23  ML{*
    5.24 @@ -79,8 +78,8 @@
    5.25  *}
    5.26  
    5.27  parse_translation
    5.28 - {* [("@emp", emp_tr), ("@singl", singl_tr),
    5.29 -     ("@star", star_tr), ("@wand", wand_tr)] *}
    5.30 + {* [("_emp", emp_tr), ("_singl", singl_tr),
    5.31 +     ("_star", star_tr), ("_wand", wand_tr)] *}
    5.32  
    5.33  text{* Now it looks much better: *}
    5.34  
    5.35 @@ -121,13 +120,13 @@
    5.36  *)
    5.37    | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
    5.38    | strip (Abs(_,_,P)) = P
    5.39 -  | strip (Const("is_empty",_)) = Syntax.const "@emp"
    5.40 +  | strip (Const("is_empty",_)) = Syntax.const "_emp"
    5.41    | strip t = t;
    5.42  in
    5.43 -fun is_empty_tr' [_] = Syntax.const "@emp"
    5.44 -fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q
    5.45 -fun star_tr' [P,Q,_] = Syntax.const "@star" $ strip P $ strip Q
    5.46 -fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q
    5.47 +fun is_empty_tr' [_] = Syntax.const "_emp"
    5.48 +fun singl_tr' [_,p,q] = Syntax.const "_singl" $ p $ q
    5.49 +fun star_tr' [P,Q,_] = Syntax.const "_star" $ strip P $ strip Q
    5.50 +fun wand_tr' [P,Q,_] = Syntax.const "_wand" $ strip P $ strip Q
    5.51  end
    5.52  *}
    5.53  
     6.1 --- a/src/HOL/SET_Protocol/Event_SET.thy	Wed Feb 10 19:37:34 2010 +0100
     6.2 +++ b/src/HOL/SET_Protocol/Event_SET.thy	Wed Feb 10 23:53:46 2010 +0100
     6.3 @@ -11,8 +11,7 @@
     6.4  begin
     6.5  
     6.6  text{*The Root Certification Authority*}
     6.7 -syntax        RCA :: agent
     6.8 -translations "RCA" == "CA 0"
     6.9 +abbreviation "RCA == CA 0"
    6.10  
    6.11  
    6.12  text{*Message events*}