src/HOL/Bali/Term.thy
changeset 35067 af4c18c30593
parent 32960 69916a850301
child 35069 09154b995ed8
--- a/src/HOL/Bali/Term.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Term.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -244,22 +244,23 @@
   "stmt"  <= (type) "Term.stmt"
   "term"  <= (type) "(expr+stmt,var,expr list) sum3"
 
-syntax
-  
-  this    :: expr
-  LAcc    :: "vname \<Rightarrow> expr" ("!!")
-  LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
-  Return  :: "expr \<Rightarrow> stmt"
-  StatRef :: "ref_ty \<Rightarrow> expr"
+abbreviation this :: expr
+  where "this == Acc (LVar This)"
+
+abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!")
+  where "!!v == Acc (LVar (EName (VNam v)))"
 
-translations
-  
- "this"       == "Acc (LVar This)"
- "!!v"        == "Acc (LVar (EName (VNam v)))"
- "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
- "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Jmp Ret" 
-                  --{* \tt Res := e;; Jmp Ret *}
- "StatRef rt" == "Cast (RefT rt) (Lit Null)"
+abbreviation
+  LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
+  where "v:==e == Expr (Ass (LVar (EName (VNam  v))) e)"
+
+abbreviation
+  Return :: "expr \<Rightarrow> stmt"
+  where "Return e == Expr (Ass (LVar (EName Res)) e);; Jmp Ret" --{* \tt Res := e;; Jmp Ret *}
+
+abbreviation
+  StatRef :: "ref_ty \<Rightarrow> expr"
+  where "StatRef rt == Cast (RefT rt) (Lit Null)"
   
 constdefs
 
@@ -275,17 +276,21 @@
   expressions, variables and expression lists into general terms.
 *}
 
-syntax 
-  expr_inj_term:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
-  stmt_inj_term:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
-  var_inj_term::  "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
-  lst_inj_term:: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
+abbreviation (input)
+  expr_inj_term :: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
+  where "\<langle>e\<rangle>\<^sub>e == In1l e"
+
+abbreviation (input)
+  stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
+  where "\<langle>c\<rangle>\<^sub>s == In1r c"
 
-translations 
-  "\<langle>e\<rangle>\<^sub>e" \<rightharpoonup> "In1l e"
-  "\<langle>c\<rangle>\<^sub>s" \<rightharpoonup> "In1r c"
-  "\<langle>v\<rangle>\<^sub>v" \<rightharpoonup> "In2 v"
-  "\<langle>es\<rangle>\<^sub>l" \<rightharpoonup> "In3 es"
+abbreviation (input)
+  var_inj_term :: "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
+  where "\<langle>v\<rangle>\<^sub>v == In2 v"
+
+abbreviation (input)
+  lst_inj_term :: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
+  where "\<langle>es\<rangle>\<^sub>l == In3 es"
 
 text {* It seems to be more elegant to have an overloaded injection like the
 following.
@@ -300,7 +305,7 @@
 @{text AxSem} don't follow this convention right now, but introduce subtle 
 syntactic sugar in the relations themselves to make a distinction on 
 expressions, statements and so on. So unfortunately you will encounter a 
-mixture of dealing with these injections. The translations above are used
+mixture of dealing with these injections. The abbreviations above are used
 as bridge between the different conventions.  
 *}