--- a/src/HOL/Bali/WellType.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/WellType.thy Wed Feb 10 00:45:16 2010 +0100
@@ -43,11 +43,9 @@
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
-
-syntax
+abbreviation
pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
-translations
- "pkg e" == "pid (cls e)"
+ where "pkg e == pid (cls e)"
section "Static overloading: maximally specific methods "
@@ -426,29 +424,33 @@
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
-syntax (* for purely static typing *)
- "_wt" :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
- "_wt_stmt" :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
- "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
- "_ty_var" :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
- "_ty_exprs":: "env \<Rightarrow> [expr list,
- \<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
+(* for purely static typing *)
+abbreviation
+ wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
+ where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
+
+abbreviation
+ wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
+ where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
+
+abbreviation
+ ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
+ where "E|-e:-T == E|-In1l e :: Inl T"
-syntax (xsymbols)
- "_wt" :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
- "_wt_stmt" :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
- "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
- "_ty_var" :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
- "_ty_exprs" :: "env \<Rightarrow> [expr list,
- \<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
+abbreviation
+ ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
+ where "E|-e:=T == E|-In2 e :: Inl T"
-translations
- "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
- "E\<turnstile>s\<Colon>\<surd>" == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
- "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
- "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2 e\<Colon>CONST Inl T"
- "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3 e\<Colon>CONST Inr T"
+abbreviation
+ ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
+ where "E|-e:#T == E|-In3 e :: Inr T"
+notation (xsymbols)
+ wt_syntax ("_\<turnstile>_\<Colon>_" [51,51,51] 50) and
+ wt_stmt_syntax ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) and
+ ty_expr_syntax ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
+ ty_var_syntax ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
+ ty_exprs_syntax ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
declare not_None_eq [simp del]
declare split_if [split del] split_if_asm [split del]