--- a/src/HOL/MicroJava/BV/BVExample.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Feb 11 00:45:02 2010 +0100
@@ -296,12 +296,10 @@
done
text {* Some abbreviations for readability *}
-syntax
- Clist :: ty
- Ctest :: ty
-translations
- "Clist" == "Class list_name"
- "Ctest" == "Class test_name"
+abbreviation Clist :: ty
+ where "Clist == Class list_name"
+abbreviation Ctest :: ty
+ where "Ctest == Class test_name"
constdefs
phi_makelist :: method_type ("\<phi>\<^sub>m")
--- a/src/HOL/MicroJava/BV/JType.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Thu Feb 11 00:45:02 2010 +0100
@@ -37,9 +37,7 @@
"is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow>
(case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C, Object) \<in> (subcls1 G)^*)"
-
-translations
- "types G" == "Collect (is_type G)"
+abbreviation "types G == Collect (is_type G)"
constdefs
esl :: "'c prog \<Rightarrow> ty esl"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Feb 11 00:45:02 2010 +0100
@@ -584,10 +584,9 @@
(* Currently: empty exception_table *)
-syntax
+abbreviation (input)
empty_et :: exception_table
-translations
- "empty_et" => "[]"
+ where "empty_et == []"
@@ -860,12 +859,13 @@
section "Correspondence bytecode - method types"
(* ********************************************************************** *)
-syntax
+abbreviation (input)
ST_of :: "state_type \<Rightarrow> opstack_type"
+ where "ST_of == fst"
+
+abbreviation (input)
LT_of :: "state_type \<Rightarrow> locvars_type"
-translations
- "ST_of" => "fst"
- "LT_of" => "snd"
+ where "LT_of == snd"
lemma states_lower:
"\<lbrakk> OK (Some (ST, LT)) \<in> states cG mxs mxr; length ST \<le> mxs\<rbrakk>
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Feb 11 00:45:02 2010 +0100
@@ -262,10 +262,8 @@
done
-syntax
- mtd_mb :: "cname \<times> ty \<times> 'c \<Rightarrow> 'c"
-translations
- "mtd_mb" => "Fun.comp snd snd"
+abbreviation (input)
+ "mtd_mb == snd o snd"
lemma map_of_map_fst: "\<lbrakk> inj f;
\<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Thu Feb 11 00:45:02 2010 +0100
@@ -41,13 +41,13 @@
(**********************************************************************)
-syntax
- mt_of :: "method_type \<times> state_type \<Rightarrow> method_type"
- sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
+abbreviation (input)
+ mt_of :: "method_type \<times> state_type \<Rightarrow> method_type"
+ where "mt_of == fst"
-translations
- "mt_of" => "fst"
- "sttp_of" => "snd"
+abbreviation (input)
+ sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
+ where "sttp_of == snd"
consts
compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr
@@ -189,4 +189,3 @@
end
-
--- a/src/HOL/MicroJava/DFA/Err.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy Thu Feb 11 00:45:02 2010 +0100
@@ -45,10 +45,9 @@
sl :: "'a esl \<Rightarrow> 'a err sl"
"sl == %(A,r,f). (err A, le r, lift2 f)"
-syntax
- err_semilat :: "'a esl \<Rightarrow> bool"
-translations
-"err_semilat L" == "semilat(Err.sl L)"
+abbreviation
+ err_semilat :: "'a esl \<Rightarrow> bool"
+ where "err_semilat L == semilat(Err.sl L)"
consts
--- a/src/HOL/MicroJava/DFA/Listn.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy Thu Feb 11 00:45:02 2010 +0100
@@ -17,21 +17,24 @@
le :: "'a ord \<Rightarrow> ('a list)ord"
"le r == list_all2 (%x y. x <=_r y)"
-syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
+abbreviation
+ lesublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
("(_ /<=[_] _)" [50, 0, 51] 50)
-syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "x <=[r] y == x <=_(le r) y"
+
+abbreviation
+ lesssublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
("(_ /<[_] _)" [50, 0, 51] 50)
-translations
- "x <=[r] y" == "x <=_(Listn.le r) y"
- "x <[r] y" == "x <_(Listn.le r) y"
+ where "x <[r] y == x <_(le r) y"
constdefs
map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
"map2 f == (%xs ys. map (split f) (zip xs ys))"
-syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
+abbreviation
+ plussublist_syntax :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
("(_ /+[_] _)" [65, 0, 66] 65)
-translations "x +[f] y" == "x +_(map2 f) y"
+ where "x +[f] y == x +_(map2 f) y"
consts coalesce :: "'a err list \<Rightarrow> 'a list err"
primrec
--- a/src/HOL/MicroJava/J/Example.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/Example.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -55,19 +54,16 @@
declare inj_cnam' [simp] inj_vnam' [simp]
-syntax
- Base :: cname
- Ext :: cname
- vee :: vname
- x :: vname
- e :: vname
-
-translations
- "Base" == "cnam' Base'"
- "Ext" == "cnam' Ext'"
- "vee" == "VName (vnam' vee')"
- "x" == "VName (vnam' x')"
- "e" == "VName (vnam' e')"
+abbreviation Base :: cname
+ where "Base == cnam' Base'"
+abbreviation Ext :: cname
+ where "Ext == cnam' Ext'"
+abbreviation vee :: vname
+ where "vee == VName (vnam' vee')"
+abbreviation x :: vname
+ where "x == VName (vnam' x')"
+abbreviation e :: vname
+ where "e == VName (vnam' e')"
axioms
Base_not_Object: "Base \<noteq> Object"
--- a/src/HOL/MicroJava/J/Exceptions.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/Exceptions.thy Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/Exceptions.thy
- ID: $Id$
Author: Gerwin Klein, Martin Strecker
Copyright 2002 Technische Universitaet Muenchen
*)
@@ -17,11 +16,9 @@
(XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
-consts
+abbreviation
cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
-
-translations
- "cname_of hp v" == "fst (CONST the (hp (the_Addr v)))"
+ where "cname_of hp v == fst (the (hp (the_Addr v)))"
constdefs
--- a/src/HOL/MicroJava/J/State.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/State.thy Thu Feb 11 00:45:02 2010 +0100
@@ -27,21 +27,27 @@
state = "aheap \<times> locals" -- "heap, local parameter including This"
xstate = "val option \<times> state" -- "state including exception information"
-syntax
- heap :: "state => aheap"
- locals :: "state => locals"
- Norm :: "state => xstate"
- abrupt :: "xstate \<Rightarrow> val option"
- store :: "xstate \<Rightarrow> state"
- lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
+abbreviation (input)
+ heap :: "state => aheap"
+ where "heap == fst"
+
+abbreviation (input)
+ locals :: "state => locals"
+ where "locals == snd"
+
+abbreviation "Norm s == (None, s)"
-translations
- "heap" => "fst"
- "locals" => "snd"
- "Norm s" == "(None,s)"
- "abrupt" => "fst"
- "store" => "snd"
- "lookup_obj s a'" == "CONST the (heap s (the_Addr a'))"
+abbreviation (input)
+ abrupt :: "xstate \<Rightarrow> val option"
+ where "abrupt == fst"
+
+abbreviation (input)
+ store :: "xstate \<Rightarrow> state"
+ where "store == snd"
+
+abbreviation
+ lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
+ where "lookup_obj s a' == the (heap s (the_Addr a'))"
constdefs
--- a/src/HOL/MicroJava/J/Type.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/Type.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -47,12 +46,10 @@
= PrimT prim_ty -- "primitive type"
| RefT ref_ty -- "reference type"
-syntax
- NT :: "ty"
- Class :: "cname => ty"
+abbreviation NT :: ty
+ where "NT == RefT NullT"
-translations
- "NT" == "RefT NullT"
- "Class C" == "RefT (ClassT C)"
+abbreviation Class :: "cname => ty"
+ where "Class C == RefT (ClassT C)"
end
--- a/src/HOL/MicroJava/J/WellType.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/WellType.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -27,13 +26,13 @@
lenv = "vname \<rightharpoonup> ty"
'c env = "'c prog \<times> lenv"
-syntax
- prg :: "'c env => 'c prog"
- localT :: "'c env => (vname \<rightharpoonup> ty)"
+abbreviation (input)
+ prg :: "'c env => 'c prog"
+ where "prg == fst"
-translations
- "prg" => "fst"
- "localT" => "snd"
+abbreviation (input)
+ localT :: "'c env => (vname \<rightharpoonup> ty)"
+ where "localT == snd"
consts
more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
@@ -207,10 +206,7 @@
(let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
-syntax
- wf_java_prog :: "'c prog => bool"
-translations
- "wf_java_prog" == "wf_prog wf_java_mdecl"
+abbreviation "wf_java_prog == wf_prog wf_java_mdecl"
lemma wf_java_prog_wf_java_mdecl: "\<lbrakk>
wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths \<rbrakk>
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/JVM/JVMDefensive.thy
- ID: $Id$
Author: Gerwin Klein
*)
@@ -13,9 +12,9 @@
datatype 'a type_error = TypeError | Normal 'a
-syntax "fifth" :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
-translations
- "fifth x" == "fst(snd(snd(snd(snd x))))"
+abbreviation
+ fifth :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
+ where "fifth x == fst(snd(snd(snd(snd x))))"
consts isAddr :: "val \<Rightarrow> bool"
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/JVM/JVMExceptions.thy
- ID: $Id$
Author: Gerwin Klein, Martin Strecker
Copyright 2001 Technische Universitaet Muenchen
*)
@@ -24,10 +23,9 @@
then Some (fst (snd (snd e)))
else match_exception_table G cn pc es)"
-consts
+abbreviation
ex_table_of :: "jvm_method \<Rightarrow> exception_table"
-translations
- "ex_table_of m" == "snd (snd (snd m))"
+ where "ex_table_of m == snd (snd (snd m))"
consts
--- a/src/HOL/NanoJava/Example.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/NanoJava/Example.thy Thu Feb 11 00:45:02 2010 +0100
@@ -50,11 +50,14 @@
consts suc :: mname
add :: mname
consts any :: vname
-syntax dummy:: expr ("<>")
- one :: expr
-translations
- "<>" == "LAcc any"
- "one" == "{Nat}new Nat..suc(<>)"
+
+abbreviation
+ dummy :: expr ("<>")
+ where "<> == LAcc any"
+
+abbreviation
+ one :: expr
+ where "one == {Nat}new Nat..suc(<>)"
text {* The following properties could be derived from a more complete
program model, which we leave out for laziness. *}
--- a/src/HOL/NanoJava/TypeRel.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Thu Feb 11 00:45:02 2010 +0100
@@ -11,16 +11,16 @@
consts
subcls1 :: "(cname \<times> cname) set" --{* subclass *}
-syntax (xsymbols)
- subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70)
- subcls :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70)
-syntax
- subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
- subcls :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70)
+abbreviation
+ subcls1_syntax :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
+ where "C <=C1 D == (C,D) \<in> subcls1"
+abbreviation
+ subcls_syntax :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70)
+ where "C <=C D == (C,D) \<in> subcls1^*"
-translations
- "C \<prec>C1 D" == "(C,D) \<in> subcls1"
- "C \<preceq>C D" == "(C,D) \<in> subcls1^*"
+notation (xsymbols)
+ subcls1_syntax ("_ \<prec>C1 _" [71,71] 70) and
+ subcls_syntax ("_ \<preceq>C _" [71,71] 70)
consts
method :: "cname => (mname \<rightharpoonup> methd)"