modernized syntax translations, using mostly abbreviation/notation;
authorwenzelm
Wed Feb 10 00:45:16 2010 +0100 (2010-02-10)
changeset 35067af4c18c30593
parent 35066 894e82be8d05
child 35068 544867142ea4
modernized syntax translations, using mostly abbreviation/notation;
minor tuning;
src/HOL/Bali/AxExample.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/Trans.thy
src/HOL/Bali/Type.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Bali/WellForm.thy
src/HOL/Bali/WellType.thy
     1.1 --- a/src/HOL/Bali/AxExample.thy	Tue Feb 09 16:07:09 2010 +0100
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Wed Feb 10 00:45:16 2010 +0100
     1.3 @@ -166,7 +166,7 @@
     1.4  apply  (tactic "ax_tac 1" (* NewC *))
     1.5  apply  (tactic "ax_tac 1" (* ax_Alloc *))
     1.6       (* just for clarification: *)
     1.7 -apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2)
     1.8 +apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free three \<and>. initd Ext)" in conseq2)
     1.9  prefer 2
    1.10  apply   (simp add: invocation_declclass_def dynmethd_def)
    1.11  apply   (unfold dynlookup_def)
     2.1 --- a/src/HOL/Bali/AxSem.thy	Tue Feb 09 16:07:09 2010 +0100
     2.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Feb 10 00:45:16 2010 +0100
     2.3 @@ -6,7 +6,6 @@
     2.4  header {* Axiomatic semantics of Java expressions and statements 
     2.5            (see also Eval.thy)
     2.6          *}
     2.7 -
     2.8  theory AxSem imports Evaln TypeSafe begin
     2.9  
    2.10  text {*
    2.11 @@ -39,14 +38,15 @@
    2.12  *}
    2.13  
    2.14  types  res = vals --{* result entry *}
    2.15 -syntax
    2.16 -  Val  :: "val      \<Rightarrow> res"
    2.17 -  Var  :: "var      \<Rightarrow> res"
    2.18 -  Vals :: "val list \<Rightarrow> res"
    2.19 -translations
    2.20 -  "Val  x"     => "(In1 x)"
    2.21 -  "Var  x"     => "(In2 x)"
    2.22 -  "Vals x"     => "(In3 x)"
    2.23 +
    2.24 +abbreviation (input)
    2.25 +  Val where "Val x == In1 x"
    2.26 +
    2.27 +abbreviation (input)
    2.28 +  Var where "Var x == In2 x"
    2.29 +
    2.30 +abbreviation (input)
    2.31 +  Vals where "Vals x == In3 x"
    2.32  
    2.33  syntax
    2.34    "_Val"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
    2.35 @@ -54,9 +54,9 @@
    2.36    "_Vals"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
    2.37  
    2.38  translations
    2.39 -  "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> the_In1"
    2.40 -  "\<lambda>Var:v . b"  == "(\<lambda>v. b) \<circ> the_In2"
    2.41 -  "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> the_In3"
    2.42 +  "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> CONST the_In1"
    2.43 +  "\<lambda>Var:v . b"  == "(\<lambda>v. b) \<circ> CONST the_In2"
    2.44 +  "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> CONST the_In3"
    2.45  
    2.46    --{* relation on result values, state and auxiliary variables *}
    2.47  types 'a assn   =        "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
    2.48 @@ -105,10 +105,9 @@
    2.49  apply auto
    2.50  done
    2.51  
    2.52 -syntax
    2.53 -  Normal     :: "'a assn \<Rightarrow> 'a assn"
    2.54 -translations
    2.55 -  "Normal P" == "P \<and>. normal"
    2.56 +abbreviation
    2.57 +  Normal :: "'a assn \<Rightarrow> 'a assn"
    2.58 +  where "Normal P == P \<and>. normal"
    2.59  
    2.60  lemma peek_and_Normal [simp]: "peek_and (Normal P) p = Normal (peek_and P p)"
    2.61  apply (rule ext)
    2.62 @@ -207,9 +206,9 @@
    2.63   "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
    2.64  
    2.65  syntax
    2.66 -"@peek_res"  :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
    2.67 +  "_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
    2.68  translations
    2.69 -  "\<lambda>w:. P"   == "peek_res (\<lambda>w. P)"
    2.70 +  "\<lambda>w:. P"   == "CONST peek_res (\<lambda>w. P)"
    2.71  
    2.72  lemma peek_res_def2 [simp]: "peek_res P Y = P Y Y"
    2.73  apply (unfold peek_res_def)
    2.74 @@ -268,9 +267,9 @@
    2.75   "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
    2.76  
    2.77  syntax
    2.78 -"@peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
    2.79 +  "_peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
    2.80  translations
    2.81 -  "\<lambda>s.. P"   == "peek_st (\<lambda>s. P)"
    2.82 +  "\<lambda>s.. P"   == "CONST peek_st (\<lambda>s. P)"
    2.83  
    2.84  lemma peek_st_def2 [simp]: "(\<lambda>s.. Pf s) Y s = Pf (store s) Y s"
    2.85  apply (unfold peek_st_def)
    2.86 @@ -386,33 +385,31 @@
    2.87                                          ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
    2.88  types    'a triples = "'a triple set"
    2.89  
    2.90 -syntax
    2.91 -
    2.92 +abbreviation
    2.93    var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
    2.94                                           ("{(1_)}/ _=>/ {(1_)}"    [3,80,3] 75)
    2.95 +  where "{P} e=> {Q} == {P} In2  e> {Q}"
    2.96 +
    2.97 +abbreviation
    2.98    expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
    2.99                                           ("{(1_)}/ _->/ {(1_)}"    [3,80,3] 75)
   2.100 +  where "{P} e-> {Q} == {P} In1l e> {Q}"
   2.101 +
   2.102 +abbreviation
   2.103    exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
   2.104                                           ("{(1_)}/ _#>/ {(1_)}"    [3,65,3] 75)
   2.105 +  where "{P} e#> {Q} == {P} In3  e> {Q}"
   2.106 +
   2.107 +abbreviation
   2.108    stmt_triple  :: "['a assn, stmt,        'a assn] \<Rightarrow> 'a triple"
   2.109                                           ("{(1_)}/ ._./ {(1_)}"     [3,65,3] 75)
   2.110 -
   2.111 -syntax (xsymbols)
   2.112 +  where "{P} .c. {Q} == {P} In1r c> {Q}"
   2.113  
   2.114 -  triple       :: "['a assn, term        ,'a assn] \<Rightarrow> 'a triple"
   2.115 -                                         ("{(1_)}/ _\<succ>/ {(1_)}"     [3,65,3] 75)
   2.116 -  var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
   2.117 -                                         ("{(1_)}/ _=\<succ>/ {(1_)}"    [3,80,3] 75)
   2.118 -  expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
   2.119 -                                         ("{(1_)}/ _-\<succ>/ {(1_)}"    [3,80,3] 75)
   2.120 -  exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
   2.121 -                                         ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}"    [3,65,3] 75)
   2.122 -
   2.123 -translations
   2.124 -  "{P} e-\<succ> {Q}" == "{P} In1l e\<succ> {Q}"
   2.125 -  "{P} e=\<succ> {Q}" == "{P} In2  e\<succ> {Q}"
   2.126 -  "{P} e\<doteq>\<succ> {Q}" == "{P} In3  e\<succ> {Q}"
   2.127 -  "{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
   2.128 +notation (xsymbols)
   2.129 +  triple  ("{(1_)}/ _\<succ>/ {(1_)}"     [3,65,3] 75) and
   2.130 +  var_triple  ("{(1_)}/ _=\<succ>/ {(1_)}"    [3,80,3] 75) and
   2.131 +  expr_triple  ("{(1_)}/ _-\<succ>/ {(1_)}"    [3,80,3] 75) and
   2.132 +  exprs_triple  ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}"    [3,65,3] 75)
   2.133  
   2.134  lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
   2.135  apply (rule inj_onI)
   2.136 @@ -436,26 +433,25 @@
   2.137      ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
   2.138                                                  ("_,_|\<Turnstile>_"   [61,58,58] 57)
   2.139  
   2.140 -syntax
   2.141 -
   2.142 +abbreviation
   2.143   triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
   2.144                                                  (  "_||=_:_" [61,0, 58] 57)
   2.145 -     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   2.146 -                                                ( "_,_|=_"   [61,58,58] 57)
   2.147 -
   2.148 -syntax (xsymbols)
   2.149 + where "G||=n:ts == Ball ts (triple_valid G n)"
   2.150  
   2.151 - triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
   2.152 -                                                (  "_|\<Turnstile>_:_" [61,0, 58] 57)
   2.153 -     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   2.154 -                                                ( "_,_\<Turnstile>_"   [61,58,58] 57)
   2.155 +abbreviation
   2.156 + ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   2.157 +                                                ( "_,_|=_"   [61,58,58] 57)
   2.158 + where "G,A |=t == G,A|\<Turnstile>{t}"
   2.159 +
   2.160 +notation (xsymbols)
   2.161 +  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57) and
   2.162 +  ax_valid  ("_,_\<Turnstile>_" [61,58,58] 57)
   2.163  
   2.164  defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
   2.165                            \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
   2.166                            (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
   2.167 -translations         "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
   2.168 -defs   ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
   2.169 -translations         "G,A \<Turnstile>t"  == "G,A|\<Turnstile>{t}"
   2.170 +
   2.171 +defs  ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
   2.172  
   2.173  lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
   2.174   (\<forall>Y s Z. P Y s Z 
     3.1 --- a/src/HOL/Bali/Basis.thy	Tue Feb 09 16:07:09 2010 +0100
     3.2 +++ b/src/HOL/Bali/Basis.thy	Wed Feb 10 00:45:16 2010 +0100
     3.3 @@ -27,12 +27,8 @@
     3.4  apply fast+
     3.5  done
     3.6  
     3.7 -syntax
     3.8 -  "3" :: nat   ("3") 
     3.9 -  "4" :: nat   ("4")
    3.10 -translations
    3.11 - "3" == "Suc 2"
    3.12 - "4" == "Suc 3"
    3.13 +abbreviation nat3 :: nat  ("3") where "3 == Suc 2"
    3.14 +abbreviation nat4 :: nat  ("4") where "4 == Suc 3"
    3.15  
    3.16  (*unused*)
    3.17  lemma range_bool_domain: "range f = {f True, f False}"
    3.18 @@ -182,10 +178,7 @@
    3.19  
    3.20  hide const In0 In1
    3.21  
    3.22 -syntax
    3.23 -  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
    3.24 -translations
    3.25 - "fun_sum" == "CONST sum_case"
    3.26 +notation sum_case  (infixr "'(+')"80)
    3.27  
    3.28  consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
    3.29            the_Inr  :: "'a + 'b \<Rightarrow> 'b"
    3.30 @@ -201,18 +194,17 @@
    3.31  primrec  "the_In2 (In2 b) = b"
    3.32  primrec  "the_In3 (In3 c) = c"
    3.33  
    3.34 -syntax
    3.35 -         In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    3.36 -         In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    3.37 -translations
    3.38 -        "In1l e" == "In1 (CONST Inl e)"
    3.39 -        "In1r c" == "In1 (CONST Inr c)"
    3.40 +abbreviation In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    3.41 +      where "In1l e == In1 (Inl e)"
    3.42 +
    3.43 +abbreviation In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    3.44 +      where "In1r c == In1 (Inr c)"
    3.45  
    3.46 -syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
    3.47 -       the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
    3.48 -translations
    3.49 -   "the_In1l" == "the_Inl \<circ> the_In1"
    3.50 -   "the_In1r" == "the_Inr \<circ> the_In1"
    3.51 +abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
    3.52 +      where "the_In1l == the_Inl \<circ> the_In1"
    3.53 +
    3.54 +abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
    3.55 +      where "the_In1r == the_Inr \<circ> the_In1"
    3.56  
    3.57  ML {*
    3.58  fun sum3_instantiate ctxt thm = map (fn s =>
    3.59 @@ -319,8 +311,8 @@
    3.60  syntax
    3.61    "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
    3.62  translations
    3.63 -  "%y#x#xs. b"  == "lsplit (%y x#xs. b)"
    3.64 -  "%x#xs  . b"  == "lsplit (%x xs  . b)"
    3.65 +  "%y#x#xs. b"  == "CONST lsplit (%y x#xs. b)"
    3.66 +  "%x#xs  . b"  == "CONST lsplit (%x xs  . b)"
    3.67  
    3.68  lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
    3.69  apply (unfold lsplit_def)
     4.1 --- a/src/HOL/Bali/Decl.thy	Tue Feb 09 16:07:09 2010 +0100
     4.2 +++ b/src/HOL/Bali/Decl.thy	Wed Feb 10 00:45:16 2010 +0100
     4.3 @@ -402,17 +402,21 @@
     4.4       "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
     4.5       "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
     4.6  
     4.7 -syntax
     4.8 -  iface     :: "prog  \<Rightarrow> (qtname, iface) table"
     4.9 -  "class"     :: "prog  \<Rightarrow> (qtname, class) table"
    4.10 -  is_iface  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
    4.11 -  is_class  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
    4.12 +abbreviation
    4.13 +  iface :: "prog  \<Rightarrow> (qtname, iface) table"
    4.14 +  where "iface G I == table_of (ifaces G) I"
    4.15 +
    4.16 +abbreviation
    4.17 +  "class" :: "prog  \<Rightarrow> (qtname, class) table"
    4.18 +  where "class G C == table_of (classes G) C"
    4.19  
    4.20 -translations
    4.21 -           "iface G I" == "table_of (ifaces G) I"
    4.22 -           "class G C" == "table_of (classes G) C"
    4.23 -        "is_iface G I" == "iface G I \<noteq> None"
    4.24 -        "is_class G C" == "class G C \<noteq> None"
    4.25 +abbreviation
    4.26 +  is_iface :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
    4.27 +  where "is_iface G I == iface G I \<noteq> None"
    4.28 +
    4.29 +abbreviation
    4.30 +  is_class :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
    4.31 +  where "is_class G C == class G C \<noteq> None"
    4.32  
    4.33  
    4.34  section "is type"
    4.35 @@ -445,21 +449,22 @@
    4.36    subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
    4.37    subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
    4.38  
    4.39 -syntax
    4.40 - "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
    4.41 - "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
    4.42 - "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
    4.43 +abbreviation
    4.44 +  subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
    4.45 +  where "G|-C <:C1 D == (C,D) \<in> subcls1 G"
    4.46 +
    4.47 +abbreviation
    4.48 +  subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
    4.49 +  where "G|-C <=:C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
    4.50  
    4.51 -syntax (xsymbols)
    4.52 -  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
    4.53 -  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
    4.54 -  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
    4.55 +abbreviation
    4.56 +  subcls_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
    4.57 +  where "G|-C <:C D == (C,D) \<in>(subcls1 G)^+"
    4.58  
    4.59 -translations
    4.60 -        "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
    4.61 -        "G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
    4.62 -        "G\<turnstile>C \<prec>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^+"
    4.63 - 
    4.64 +notation (xsymbols)
    4.65 +  subcls1_syntax  ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70) and
    4.66 +  subclseq_syntax  ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70) and
    4.67 +  subcls_syntax  ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
    4.68  
    4.69  lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk> 
    4.70                   \<Longrightarrow> (I,J) \<in> subint1 G" 
     5.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Feb 09 16:07:09 2010 +0100
     5.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Feb 10 00:45:16 2010 +0100
     5.3 @@ -13,8 +13,8 @@
     5.4  "is_public G qn \<equiv> (case class G qn of
     5.5                       None       \<Rightarrow> (case iface G qn of
     5.6                                        None       \<Rightarrow> False
     5.7 -                                    | Some iface \<Rightarrow> access iface = Public)
     5.8 -                   | Some class \<Rightarrow> access class = Public)"
     5.9 +                                    | Some i \<Rightarrow> access i = Public)
    5.10 +                   | Some c \<Rightarrow> access c = Public)"
    5.11  
    5.12  subsection "accessibility of types (cf. 6.6.1)"
    5.13  text {* 
    5.14 @@ -445,21 +445,17 @@
    5.15       | Protected \<Rightarrow> True
    5.16       | Public    \<Rightarrow> True)"
    5.17  
    5.18 -syntax
    5.19 -Method_inheritable_in::
    5.20 +abbreviation
    5.21 +Method_inheritable_in_syntax::
    5.22   "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool"
    5.23                  ("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60)
    5.24 + where "G\<turnstile>Method m inheritable_in p == G\<turnstile>methdMembr m inheritable_in p"
    5.25  
    5.26 -translations
    5.27 -"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p"
    5.28 -
    5.29 -syntax
    5.30 +abbreviation
    5.31  Methd_inheritable_in::
    5.32   "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"
    5.33                  ("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
    5.34 -
    5.35 -translations
    5.36 -"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p"
    5.37 + where "G\<turnstile>Methd s m inheritable_in p == G\<turnstile>(method s m) inheritable_in p"
    5.38  
    5.39  subsubsection "declared-in/undeclared-in"
    5.40  
    5.41 @@ -486,17 +482,15 @@
    5.42                          fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
    5.43                        | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
    5.44  
    5.45 -syntax
    5.46 +abbreviation
    5.47  method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    5.48                                   ("_\<turnstile>Method _ declared'_in _" [61,61,61] 60)
    5.49 -translations
    5.50 -"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C"
    5.51 + where "G\<turnstile>Method m declared_in C == G\<turnstile>mdecl (mthd m) declared_in C"
    5.52  
    5.53 -syntax
    5.54 +abbreviation
    5.55  methd_declared_in:: "prog  \<Rightarrow> sig  \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
    5.56                                 ("_\<turnstile>Methd _  _ declared'_in _" [61,61,61,61] 60)
    5.57 -translations
    5.58 -"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C"
    5.59 + where "G\<turnstile>Methd s m declared_in C == G\<turnstile>mdecl (s,mthd m) declared_in C"
    5.60  
    5.61  lemma declared_in_classD:
    5.62   "G\<turnstile>m declared_in C \<Longrightarrow> is_class G C"
    5.63 @@ -538,26 +532,20 @@
    5.64  of S will not inherit the member, regardless if they are in the same
    5.65  package as A or not.*}
    5.66  
    5.67 -syntax
    5.68 +abbreviation
    5.69  method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    5.70                             ("_ \<turnstile>Method _ member'_of _" [61,61,61] 60)
    5.71 + where "G\<turnstile>Method m member_of C == G\<turnstile>(methdMembr m) member_of C"
    5.72  
    5.73 -translations
    5.74 - "G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C" 
    5.75 -
    5.76 -syntax
    5.77 +abbreviation
    5.78  methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
    5.79                             ("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)
    5.80 + where "G\<turnstile>Methd s m member_of C == G\<turnstile>(method s m) member_of C" 
    5.81  
    5.82 -translations
    5.83 - "G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C" 
    5.84 -
    5.85 -syntax
    5.86 +abbreviation
    5.87  fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool"
    5.88                             ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
    5.89 -
    5.90 -translations
    5.91 - "G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C" 
    5.92 + where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
    5.93  
    5.94  constdefs
    5.95  inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"
    5.96 @@ -578,19 +566,15 @@
    5.97  is necessary since not all members are inherited to subclasses. So such
    5.98  members are not member-of the subclass but member-in the subclass.*}
    5.99  
   5.100 -syntax
   5.101 +abbreviation
   5.102  method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   5.103                             ("_ \<turnstile>Method _ member'_in _" [61,61,61] 60)
   5.104 + where "G\<turnstile>Method m member_in C == G\<turnstile>(methdMembr m) member_in C"
   5.105  
   5.106 -translations
   5.107 - "G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C" 
   5.108 -
   5.109 -syntax
   5.110 +abbreviation
   5.111  methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
   5.112                             ("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60)
   5.113 -
   5.114 -translations
   5.115 - "G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" 
   5.116 + where "G\<turnstile>Methd s m member_in C == G\<turnstile>(method s m) member_in C"
   5.117  
   5.118  lemma member_inD: "G\<turnstile>m member_in C 
   5.119   \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
   5.120 @@ -649,18 +633,16 @@
   5.121  | Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
   5.122              \<Longrightarrow> G\<turnstile>new overrides old"
   5.123  
   5.124 -syntax
   5.125 +abbreviation (input)
   5.126  sig_stat_overrides:: 
   5.127   "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   5.128                                    ("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60)
   5.129 -translations
   5.130 - "G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
   5.131 + where "G,s\<turnstile>new overrides\<^sub>S old == G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
   5.132  
   5.133 -syntax
   5.134 +abbreviation (input)
   5.135  sig_overrides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   5.136                                    ("_,_\<turnstile> _ overrides _" [61,61,61,61] 60)
   5.137 -translations
   5.138 - "G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" 
   5.139 + where "G,s\<turnstile>new overrides old == G\<turnstile>(qmdecl s new) overrides (qmdecl s old)"
   5.140  
   5.141  subsubsection "Hiding"
   5.142  
   5.143 @@ -674,11 +656,10 @@
   5.144      G\<turnstile>Method old declared_in (declclass old) \<and> 
   5.145      G\<turnstile>Method old inheritable_in pid (declclass new)"
   5.146  
   5.147 -syntax
   5.148 -sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
   5.149 +abbreviation
   5.150 +sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   5.151                                    ("_,_\<turnstile> _ hides _" [61,61,61,61] 60)
   5.152 -translations
   5.153 - "G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)" 
   5.154 + where "G,s\<turnstile>new hides old == G\<turnstile>(qmdecl s new) hides (qmdecl s old)"
   5.155  
   5.156  lemma hidesI:
   5.157  "\<lbrakk>is_static new; msig new = msig old;
   5.158 @@ -731,14 +712,14 @@
   5.159   "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   5.160                     ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
   5.161  
   5.162 -"G\<turnstile>membr in class permits_acc_from accclass 
   5.163 +"G\<turnstile>membr in cls permits_acc_from accclass 
   5.164    \<equiv> (case (accmodi membr) of
   5.165         Private   \<Rightarrow> (declclass membr = accclass)
   5.166       | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
   5.167       | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
   5.168                      \<or>
   5.169                      (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
   5.170 -                     \<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr)) 
   5.171 +                     \<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr)) 
   5.172       | Public    \<Rightarrow> True)"
   5.173  text {*
   5.174  The subcondition of the @{term "Protected"} case: 
   5.175 @@ -774,12 +755,14 @@
   5.176  
   5.177  | "G\<turnstile>Method m of cls accessible_from accclass \<equiv> accessible_fromR G accclass (methdMembr m) cls"
   5.178  
   5.179 -| Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
   5.180 +| Immediate:  "!!membr class.
   5.181 +               \<lbrakk>G\<turnstile>membr member_of class;
   5.182                  G\<turnstile>(Class class) accessible_in (pid accclass);
   5.183                  G\<turnstile>membr in class permits_acc_from accclass 
   5.184                 \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   5.185  
   5.186 -| Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
   5.187 +| Overriding: "!!membr class C new old supr.
   5.188 +               \<lbrakk>G\<turnstile>membr member_of class;
   5.189                  G\<turnstile>(Class class) accessible_in (pid accclass);
   5.190                  membr=(C,mdecl new);
   5.191                  G\<turnstile>(C,new) overrides\<^sub>S old; 
   5.192 @@ -787,23 +770,21 @@
   5.193                  G\<turnstile>Method old of supr accessible_from accclass
   5.194                 \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   5.195  
   5.196 -syntax 
   5.197 +abbreviation
   5.198  methd_accessible_from:: 
   5.199   "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   5.200                   ("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
   5.201 + where
   5.202 + "G\<turnstile>Methd s m of cls accessible_from accclass ==
   5.203 +   G\<turnstile>(method s m) of cls accessible_from accclass"
   5.204  
   5.205 -translations
   5.206 -"G\<turnstile>Methd s m of cls accessible_from accclass"  
   5.207 - \<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass"  
   5.208 -
   5.209 -syntax 
   5.210 +abbreviation
   5.211  field_accessible_from:: 
   5.212   "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   5.213                   ("_ \<turnstile>Field _  _ of _ accessible'_from _" [61,61,61,61,61] 60)
   5.214 -
   5.215 -translations
   5.216 -"G\<turnstile>Field fn f of C accessible_from accclass"  
   5.217 - \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
   5.218 + where
   5.219 + "G\<turnstile>Field fn f of C accessible_from accclass ==
   5.220 +  G\<turnstile>(fieldm fn f) of C accessible_from accclass"
   5.221  
   5.222  inductive
   5.223    dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   5.224 @@ -817,34 +798,32 @@
   5.225  
   5.226  | "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC (methdMembr m) C"
   5.227  
   5.228 -| Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
   5.229 +| Immediate:  "!!class. \<lbrakk>G\<turnstile>membr member_in class;
   5.230                  G\<turnstile>membr in class permits_acc_from accclass 
   5.231                 \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   5.232  
   5.233 -| Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
   5.234 +| Overriding: "!!class. \<lbrakk>G\<turnstile>membr member_in class;
   5.235                  membr=(C,mdecl new);
   5.236                  G\<turnstile>(C,new) overrides old; 
   5.237                  G\<turnstile>class \<prec>\<^sub>C supr;
   5.238                  G\<turnstile>Method old in supr dyn_accessible_from accclass
   5.239                 \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   5.240  
   5.241 -syntax 
   5.242 +abbreviation
   5.243  methd_dyn_accessible_from:: 
   5.244   "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   5.245               ("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
   5.246 + where
   5.247 + "G\<turnstile>Methd s m in C dyn_accessible_from accC ==
   5.248 +  G\<turnstile>(method s m) in C dyn_accessible_from accC"  
   5.249  
   5.250 -translations
   5.251 -"G\<turnstile>Methd s m in C dyn_accessible_from accC"  
   5.252 - \<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC"  
   5.253 -
   5.254 -syntax 
   5.255 +abbreviation
   5.256  field_dyn_accessible_from:: 
   5.257   "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   5.258           ("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
   5.259 -
   5.260 -translations
   5.261 -"G\<turnstile>Field fn f in dynC dyn_accessible_from accC"  
   5.262 - \<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
   5.263 + where
   5.264 + "G\<turnstile>Field fn f in dynC dyn_accessible_from accC ==
   5.265 +  G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
   5.266  
   5.267  
   5.268  lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S
     6.1 --- a/src/HOL/Bali/Eval.thy	Tue Feb 09 16:07:09 2010 +0100
     6.2 +++ b/src/HOL/Bali/Eval.thy	Wed Feb 10 00:45:16 2010 +0100
     6.3 @@ -125,20 +125,21 @@
     6.4   assignment. 
     6.5  *}
     6.6  
     6.7 -syntax (xsymbols)
     6.8 +abbreviation (xsymbols)
     6.9    dummy_res :: "vals" ("\<diamondsuit>")
    6.10 -translations
    6.11 -  "\<diamondsuit>" == "In1 Unit"
    6.12 +  where "\<diamondsuit> == In1 Unit"
    6.13 +
    6.14 +abbreviation (input)
    6.15 +  val_inj_vals ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
    6.16 +  where "\<lfloor>e\<rfloor>\<^sub>e == In1 e"
    6.17  
    6.18 -syntax 
    6.19 -  val_inj_vals:: "expr \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
    6.20 -  var_inj_vals::  "var \<Rightarrow> term"  ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
    6.21 -  lst_inj_vals:: "expr list \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
    6.22 +abbreviation (input)
    6.23 +  var_inj_vals  ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
    6.24 +  where "\<lfloor>v\<rfloor>\<^sub>v == In2 v"
    6.25  
    6.26 -translations 
    6.27 -  "\<lfloor>e\<rfloor>\<^sub>e" \<rightharpoonup> "In1 e"
    6.28 -  "\<lfloor>v\<rfloor>\<^sub>v" \<rightharpoonup> "In2 v"
    6.29 -  "\<lfloor>es\<rfloor>\<^sub>l" \<rightharpoonup> "In3 es"
    6.30 +abbreviation (input)
    6.31 +  lst_inj_vals  ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
    6.32 +  where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
    6.33  
    6.34  constdefs
    6.35    undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
     7.1 --- a/src/HOL/Bali/Example.thy	Tue Feb 09 16:07:09 2010 +0100
     7.2 +++ b/src/HOL/Bali/Example.thy	Wed Feb 10 00:45:16 2010 +0100
     7.3 @@ -1202,74 +1202,52 @@
     7.4  
     7.5  abbreviation "one == Suc 0"
     7.6  abbreviation "two == Suc one"
     7.7 -abbreviation "tree == Suc two"
     7.8 -abbreviation "four == Suc tree"
     7.9 +abbreviation "three == Suc two"
    7.10 +abbreviation "four == Suc three"
    7.11 +
    7.12 +abbreviation
    7.13 +  "obj_a == \<lparr>tag=Arr (PrimT Boolean) 2
    7.14 +                ,values= empty(Inr 0\<mapsto>Bool False)(Inr 1\<mapsto>Bool False)\<rparr>"
    7.15  
    7.16 -syntax
    7.17 -  obj_a :: obj
    7.18 -  obj_b :: obj
    7.19 -  obj_c :: obj
    7.20 -  arr_N :: "(vn, val) table"
    7.21 -  arr_a :: "(vn, val) table"
    7.22 -  globs1 :: globs
    7.23 -  globs2 :: globs
    7.24 -  globs3 :: globs
    7.25 -  globs8 :: globs
    7.26 -  locs3 :: locals
    7.27 -  locs4 :: locals
    7.28 -  locs8 :: locals
    7.29 -  s0  :: state
    7.30 -  s0' :: state
    7.31 -  s9' :: state
    7.32 -  s1  :: state
    7.33 -  s1' :: state
    7.34 -  s2  :: state
    7.35 -  s2' :: state
    7.36 -  s3  :: state
    7.37 -  s3' :: state
    7.38 -  s4  :: state
    7.39 -  s4' :: state
    7.40 -  s6' :: state
    7.41 -  s7' :: state
    7.42 -  s8  :: state
    7.43 -  s8' :: state
    7.44 +abbreviation
    7.45 +  "obj_b == \<lparr>tag=CInst Ext
    7.46 +                ,values=(empty(Inl (vee, Base)\<mapsto>Null   )
    7.47 +                              (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
    7.48 +
    7.49 +abbreviation
    7.50 +  "obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
    7.51 +
    7.52 +abbreviation "arr_N == empty(Inl (arr, Base)\<mapsto>Null)"
    7.53 +abbreviation "arr_a == empty(Inl (arr, Base)\<mapsto>Addr a)"
    7.54 +
    7.55 +abbreviation
    7.56 +  "globs1 == empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
    7.57 +                     (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>)
    7.58 +                     (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)"
    7.59  
    7.60 -translations
    7.61 -  "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two)
    7.62 -                ,values=CONST empty(CONST Inr 0\<mapsto>Bool False)(CONST Inr (CONST one)\<mapsto>Bool False)\<rparr>"
    7.63 -  "obj_b"   <= "\<lparr>tag=CInst (CONST Ext)
    7.64 -                ,values=(CONST empty(CONST Inl (CONST vee, CONST Base)\<mapsto>Null   ) 
    7.65 -                              (CONST Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
    7.66 -  "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
    7.67 -  "arr_N"   == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Null)"
    7.68 -  "arr_a"   == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
    7.69 -  "globs1"  == "CONST empty(CONST Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    7.70 -                     (CONST Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
    7.71 -                     (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
    7.72 -  "globs2"  == "CONST empty(CONST Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    7.73 -                     (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    7.74 -                     (CONST Inl a\<mapsto>obj_a)
    7.75 -                     (CONST Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
    7.76 -  "globs3"  == "globs2(CONST Inl b\<mapsto>obj_b)"
    7.77 -  "globs8"  == "globs3(CONST Inl c\<mapsto>obj_c)"
    7.78 -  "locs3"   == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
    7.79 -  "locs4"   == "CONST empty(VName (CONST z)\<mapsto>Null)(CONST Inr()\<mapsto>Addr b)"
    7.80 -  "locs8"   == "locs3(VName (CONST z)\<mapsto>Addr c)"
    7.81 -  "s0"  == "       st (CONST empty) (CONST empty)"
    7.82 -  "s0'" == " Norm  s0"
    7.83 -  "s1"  == "       st globs1 (CONST empty)"
    7.84 -  "s1'" == " Norm  s1"
    7.85 -  "s2"  == "       st globs2 (CONST empty)"
    7.86 -  "s2'" == " Norm  s2"
    7.87 -  "s3"  == "       st globs3 locs3 "
    7.88 -  "s3'" == " Norm  s3"
    7.89 -  "s4"  == "       st globs3 locs4"
    7.90 -  "s4'" == " Norm  s4"
    7.91 -  "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
    7.92 -  "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
    7.93 -  "s8"  == "       st globs8 locs8"
    7.94 -  "s8'" == " Norm  s8"
    7.95 -  "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
    7.96 +abbreviation
    7.97 +  "globs2 == empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
    7.98 +                     (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
    7.99 +                     (Inl a\<mapsto>obj_a)
   7.100 +                     (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
   7.101 +
   7.102 +abbreviation "globs3 == globs2(Inl b\<mapsto>obj_b)"
   7.103 +abbreviation "globs8 == globs3(Inl c\<mapsto>obj_c)"
   7.104 +abbreviation "locs3 == empty(VName e\<mapsto>Addr b)"
   7.105 +abbreviation "locs8 == locs3(VName z\<mapsto>Addr c)"
   7.106 +
   7.107 +abbreviation "s0 == st empty empty"
   7.108 +abbreviation "s0' == Norm  s0"
   7.109 +abbreviation "s1 == st globs1 empty"
   7.110 +abbreviation "s1' == Norm s1"
   7.111 +abbreviation "s2 == st globs2 empty"
   7.112 +abbreviation "s2' == Norm s2"
   7.113 +abbreviation "s3 == st globs3 locs3"
   7.114 +abbreviation "s3' == Norm s3"
   7.115 +abbreviation "s7' == (Some (Xcpt (Std NullPointer)), s3)"
   7.116 +abbreviation "s8 == st globs8 locs8"
   7.117 +abbreviation "s8' == Norm s8"
   7.118 +abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
   7.119  
   7.120  
   7.121  declare Pair_eq [simp del]
   7.122 @@ -1293,7 +1271,7 @@
   7.123  apply  (rule eval_Is (* NewC *))
   7.124        (* begin init Ext *)
   7.125  apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
   7.126 -apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
   7.127 +apply   (erule_tac V = "atleast_free ?h three" in thin_rl)
   7.128  apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
   7.129  apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
   7.130  apply   (rule eval_Is (* Init Ext *))
   7.131 @@ -1336,7 +1314,7 @@
   7.132  apply (drule alloc_one)
   7.133  apply  (simp (no_asm_simp))
   7.134  apply clarsimp
   7.135 -apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
   7.136 +apply (erule_tac V = "atleast_free ?h three" in thin_rl)
   7.137  apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
   7.138  apply (simp (no_asm_use))
   7.139  apply (rule eval_Is (* Try *))
     8.1 --- a/src/HOL/Bali/Name.thy	Tue Feb 09 16:07:09 2010 +0100
     8.2 +++ b/src/HOL/Bali/Name.thy	Wed Feb 10 00:45:16 2010 +0100
     8.3 @@ -20,13 +20,11 @@
     8.4  datatype lname        --{* names for local variables and the This pointer *}
     8.5          = EName ename 
     8.6          | This
     8.7 -syntax   
     8.8 -  VName  :: "vname \<Rightarrow> lname"
     8.9 -  Result :: lname
    8.10 +abbreviation VName   :: "vname \<Rightarrow> lname"
    8.11 +      where "VName n == EName (VNam n)"
    8.12  
    8.13 -translations
    8.14 -  "VName n" == "EName (VNam n)"
    8.15 -  "Result"  == "EName Res"
    8.16 +abbreviation Result :: lname
    8.17 +      where "Result == EName Res"
    8.18  
    8.19  datatype xname          --{* names of standard exceptions *}
    8.20          = Throwable
     9.1 --- a/src/HOL/Bali/State.thy	Tue Feb 09 16:07:09 2010 +0100
     9.2 +++ b/src/HOL/Bali/State.thy	Wed Feb 10 00:45:16 2010 +0100
     9.3 @@ -254,13 +254,11 @@
     9.4  by (simp add: heap_def)
     9.5  
     9.6  
     9.7 -syntax
     9.8 -  val_this     :: "st \<Rightarrow> val"
     9.9 -  lookup_obj   :: "st \<Rightarrow> val \<Rightarrow> obj"
    9.10 +abbreviation val_this :: "st \<Rightarrow> val"
    9.11 +  where "val_this s == the (locals s This)"
    9.12  
    9.13 -translations
    9.14 - "val_this s"       == "CONST the (locals s This)" 
    9.15 - "lookup_obj s a'"  == "CONST the (heap s (the_Addr a'))"
    9.16 +abbreviation lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj"
    9.17 +  where "lookup_obj s a' == the (heap s (the_Addr a'))"
    9.18  
    9.19  subsection "memory allocation"
    9.20  
    9.21 @@ -286,12 +284,8 @@
    9.22  
    9.23  subsection "initialization"
    9.24  
    9.25 -syntax
    9.26 -
    9.27 -  init_vals     :: "('a, ty) table \<Rightarrow> ('a, val) table"
    9.28 -
    9.29 -translations
    9.30 - "init_vals vs"    == "CONST Option.map default_val \<circ> vs"
    9.31 +abbreviation init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
    9.32 +  where "init_vals vs == Option.map default_val \<circ> vs"
    9.33  
    9.34  lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
    9.35  apply (unfold arr_comps_def in_bounds_def)
    9.36 @@ -325,11 +319,9 @@
    9.37    init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
    9.38   "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
    9.39  
    9.40 -syntax
    9.41 +abbreviation
    9.42    init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
    9.43 -
    9.44 -translations
    9.45 - "init_class_obj G C" == "init_obj G CONST undefined (CONST Inr C)"
    9.46 +  where "init_class_obj G C == init_obj G undefined (Inr C)"
    9.47  
    9.48  lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
    9.49  apply (unfold gupd_def)
    9.50 @@ -513,19 +505,17 @@
    9.51  apply auto
    9.52  done
    9.53  
    9.54 -syntax
    9.55 +abbreviation raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
    9.56 +  where "raise_if c xn == abrupt_if c (Some (Xcpt (Std xn)))"
    9.57 +
    9.58 +abbreviation np :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
    9.59 +  where "np v == raise_if (v = Null) NullPointer"
    9.60  
    9.61 -  raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
    9.62 -  np       :: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
    9.63 -  check_neg:: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
    9.64 -  error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
    9.65 -  
    9.66 -translations
    9.67 +abbreviation check_neg :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
    9.68 +  where "check_neg i' == raise_if (the_Intg i'<0) NegArrSize"
    9.69  
    9.70 - "raise_if c xn" == "abrupt_if c (Some (Xcpt (Std xn)))"
    9.71 - "np v"          == "raise_if (v = Null)      NullPointer"
    9.72 - "check_neg i'"  == "raise_if (the_Intg i'<0) NegArrSize"
    9.73 - "error_if c e"  == "abrupt_if c (Some (Error e))"
    9.74 +abbreviation error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
    9.75 +  where "error_if c e == abrupt_if c (Some (Error e))"
    9.76  
    9.77  lemma raise_if_None [simp]: "(raise_if c x y = None) = (\<not>c \<and> y = None)"
    9.78  apply (simp add: abrupt_if_def)
    9.79 @@ -592,22 +582,23 @@
    9.80  types
    9.81    state = "abopt \<times> st"          --{* state including abruption information *}
    9.82  
    9.83 -syntax 
    9.84 -  Norm   :: "st \<Rightarrow> state"
    9.85 -  abrupt :: "state \<Rightarrow> abopt"
    9.86 -  store  :: "state \<Rightarrow> st"
    9.87 -
    9.88  translations
    9.89 -   
    9.90 -  "Norm s"     == "(None,s)" 
    9.91 -  "abrupt"     => "fst"
    9.92 -  "store"      => "snd"
    9.93    "abopt"       <= (type) "State.abrupt option"
    9.94    "abopt"       <= (type) "abrupt option"
    9.95    "state"      <= (type) "abopt \<times> State.st"
    9.96    "state"      <= (type) "abopt \<times> st"
    9.97  
    9.98 +abbreviation
    9.99 +  Norm :: "st \<Rightarrow> state"
   9.100 +  where "Norm s == (None, s)"
   9.101  
   9.102 +abbreviation (input)
   9.103 +  abrupt :: "state \<Rightarrow> abopt"
   9.104 +  where "abrupt == fst"
   9.105 +
   9.106 +abbreviation (input)
   9.107 +  store :: "state \<Rightarrow> st"
   9.108 +  where "store == snd"
   9.109  
   9.110  lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
   9.111  apply (erule_tac x = "(Some k,y)" in all_dupE)
   9.112 @@ -683,15 +674,11 @@
   9.113  lemma supd_abrupt_invariant [simp]: "abrupt (supd f s) = abrupt s"
   9.114    by (cases s) simp
   9.115  
   9.116 -syntax
   9.117 +abbreviation set_lvars :: "locals \<Rightarrow> state \<Rightarrow> state"
   9.118 +  where "set_lvars l == supd (set_locals l)"
   9.119  
   9.120 -  set_lvars     :: "locals \<Rightarrow> state \<Rightarrow> state"
   9.121 -  restore_lvars :: "state  \<Rightarrow> state \<Rightarrow> state"
   9.122 -  
   9.123 -translations
   9.124 -
   9.125 - "set_lvars l" == "supd (set_locals l)"
   9.126 - "restore_lvars s' s" == "set_lvars (locals (store s')) s"
   9.127 +abbreviation restore_lvars :: "state  \<Rightarrow> state \<Rightarrow> state"
   9.128 +  where "restore_lvars s' s == set_lvars (locals (store s')) s"
   9.129  
   9.130  lemma set_set_lvars [simp]: "\<And> s. set_lvars l (set_lvars l' s) = set_lvars l s"
   9.131  apply (simp (no_asm_simp) only: split_tupled_all)
    10.1 --- a/src/HOL/Bali/Term.thy	Tue Feb 09 16:07:09 2010 +0100
    10.2 +++ b/src/HOL/Bali/Term.thy	Wed Feb 10 00:45:16 2010 +0100
    10.3 @@ -244,22 +244,23 @@
    10.4    "stmt"  <= (type) "Term.stmt"
    10.5    "term"  <= (type) "(expr+stmt,var,expr list) sum3"
    10.6  
    10.7 -syntax
    10.8 -  
    10.9 -  this    :: expr
   10.10 -  LAcc    :: "vname \<Rightarrow> expr" ("!!")
   10.11 -  LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   10.12 -  Return  :: "expr \<Rightarrow> stmt"
   10.13 -  StatRef :: "ref_ty \<Rightarrow> expr"
   10.14 +abbreviation this :: expr
   10.15 +  where "this == Acc (LVar This)"
   10.16 +
   10.17 +abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!")
   10.18 +  where "!!v == Acc (LVar (EName (VNam v)))"
   10.19  
   10.20 -translations
   10.21 -  
   10.22 - "this"       == "Acc (LVar This)"
   10.23 - "!!v"        == "Acc (LVar (EName (VNam v)))"
   10.24 - "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
   10.25 - "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Jmp Ret" 
   10.26 -                  --{* \tt Res := e;; Jmp Ret *}
   10.27 - "StatRef rt" == "Cast (RefT rt) (Lit Null)"
   10.28 +abbreviation
   10.29 +  LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   10.30 +  where "v:==e == Expr (Ass (LVar (EName (VNam  v))) e)"
   10.31 +
   10.32 +abbreviation
   10.33 +  Return :: "expr \<Rightarrow> stmt"
   10.34 +  where "Return e == Expr (Ass (LVar (EName Res)) e);; Jmp Ret" --{* \tt Res := e;; Jmp Ret *}
   10.35 +
   10.36 +abbreviation
   10.37 +  StatRef :: "ref_ty \<Rightarrow> expr"
   10.38 +  where "StatRef rt == Cast (RefT rt) (Lit Null)"
   10.39    
   10.40  constdefs
   10.41  
   10.42 @@ -275,17 +276,21 @@
   10.43    expressions, variables and expression lists into general terms.
   10.44  *}
   10.45  
   10.46 -syntax 
   10.47 -  expr_inj_term:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
   10.48 -  stmt_inj_term:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
   10.49 -  var_inj_term::  "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
   10.50 -  lst_inj_term:: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
   10.51 +abbreviation (input)
   10.52 +  expr_inj_term :: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
   10.53 +  where "\<langle>e\<rangle>\<^sub>e == In1l e"
   10.54 +
   10.55 +abbreviation (input)
   10.56 +  stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
   10.57 +  where "\<langle>c\<rangle>\<^sub>s == In1r c"
   10.58  
   10.59 -translations 
   10.60 -  "\<langle>e\<rangle>\<^sub>e" \<rightharpoonup> "In1l e"
   10.61 -  "\<langle>c\<rangle>\<^sub>s" \<rightharpoonup> "In1r c"
   10.62 -  "\<langle>v\<rangle>\<^sub>v" \<rightharpoonup> "In2 v"
   10.63 -  "\<langle>es\<rangle>\<^sub>l" \<rightharpoonup> "In3 es"
   10.64 +abbreviation (input)
   10.65 +  var_inj_term :: "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
   10.66 +  where "\<langle>v\<rangle>\<^sub>v == In2 v"
   10.67 +
   10.68 +abbreviation (input)
   10.69 +  lst_inj_term :: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
   10.70 +  where "\<langle>es\<rangle>\<^sub>l == In3 es"
   10.71  
   10.72  text {* It seems to be more elegant to have an overloaded injection like the
   10.73  following.
   10.74 @@ -300,7 +305,7 @@
   10.75  @{text AxSem} don't follow this convention right now, but introduce subtle 
   10.76  syntactic sugar in the relations themselves to make a distinction on 
   10.77  expressions, statements and so on. So unfortunately you will encounter a 
   10.78 -mixture of dealing with these injections. The translations above are used
   10.79 +mixture of dealing with these injections. The abbreviations above are used
   10.80  as bridge between the different conventions.  
   10.81  *}
   10.82  
    11.1 --- a/src/HOL/Bali/Trans.thy	Tue Feb 09 16:07:09 2010 +0100
    11.2 +++ b/src/HOL/Bali/Trans.thy	Wed Feb 10 00:45:16 2010 +0100
    11.3 @@ -60,13 +60,13 @@
    11.4  by (simp)
    11.5  declare the_var_AVar_def [simp del]
    11.6  
    11.7 -syntax (xsymbols)
    11.8 -  Ref  :: "loc \<Rightarrow> expr"
    11.9 -  SKIP :: "expr"
   11.10 +abbreviation
   11.11 +  Ref :: "loc \<Rightarrow> expr"
   11.12 +  where "Ref a == Lit (Addr a)"
   11.13  
   11.14 -translations
   11.15 -  "Ref a" == "Lit (Addr a)"
   11.16 -  "SKIP"  == "Lit Unit"
   11.17 +abbreviation
   11.18 +  SKIP :: "expr"
   11.19 +  where "SKIP == Lit Unit"
   11.20  
   11.21  inductive
   11.22    step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
    12.1 --- a/src/HOL/Bali/Type.thy	Tue Feb 09 16:07:09 2010 +0100
    12.2 +++ b/src/HOL/Bali/Type.thy	Wed Feb 10 00:45:16 2010 +0100
    12.3 @@ -36,17 +36,11 @@
    12.4    "ref_ty"  <= (type) "Type.ref_ty"
    12.5    "ty"      <= (type) "Type.ty"
    12.6  
    12.7 -syntax
    12.8 -         NT     :: "       \<spacespace> ty"
    12.9 -         Iface  :: "qtname  \<Rightarrow> ty"
   12.10 -         Class  :: "qtname  \<Rightarrow> ty"
   12.11 -         Array  :: "ty     \<Rightarrow> ty"    ("_.[]" [90] 90)
   12.12 -
   12.13 -translations
   12.14 -        "NT"      == "RefT   NullT"
   12.15 -        "Iface I" == "RefT (IfaceT I)"
   12.16 -        "Class C" == "RefT (ClassT C)"
   12.17 -        "T.[]"    == "RefT (ArrayT T)"
   12.18 +abbreviation "NT == RefT NullT"
   12.19 +abbreviation "Iface I == RefT (IfaceT I)"
   12.20 +abbreviation "Class C == RefT (ClassT C)"
   12.21 +abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
   12.22 +  where "T.[] == RefT (ArrayT T)"
   12.23  
   12.24  constdefs
   12.25    the_Class :: "ty \<Rightarrow> qtname"
    13.1 --- a/src/HOL/Bali/TypeRel.thy	Tue Feb 09 16:07:09 2010 +0100
    13.2 +++ b/src/HOL/Bali/TypeRel.thy	Wed Feb 10 00:45:16 2010 +0100
    13.3 @@ -35,37 +35,22 @@
    13.4  (*subclseq, by translation*)                 (* subclass + identity       *)
    13.5    implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
    13.6  
    13.7 -syntax
    13.8 +abbreviation
    13.9 +  subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
   13.10 +  where "G|-I <:I1 J == (I,J) \<in> subint1 G"
   13.11  
   13.12 - "_subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
   13.13 - "_subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
   13.14 - (* Defined in Decl.thy:
   13.15 - "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
   13.16 - "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
   13.17 - "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
   13.18 - *)
   13.19 - "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
   13.20 -
   13.21 -syntax (xsymbols)
   13.22 +abbreviation
   13.23 +  subint_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
   13.24 +  where "G|-I <=:I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
   13.25  
   13.26 -  "_subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
   13.27 -  "_subint"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
   13.28 -  (* Defined in Decl.thy:
   13.29 -\  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
   13.30 -  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
   13.31 -  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
   13.32 -  *)
   13.33 -  "_implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
   13.34 +abbreviation
   13.35 +  implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
   13.36 +  where "G|-C ~>1 I == (C,I) \<in> implmt1 G"
   13.37  
   13.38 -translations
   13.39 -
   13.40 -        "G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"
   13.41 -        "G\<turnstile>I \<preceq>I  J" == "(I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
   13.42 -        (* Defined in Decl.thy:
   13.43 -        "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
   13.44 -        "G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" 
   13.45 -        *)
   13.46 -        "G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G"
   13.47 +notation (xsymbols)
   13.48 +  subint1_syntax  ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70) and
   13.49 +  subint_syntax  ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70) and
   13.50 +  implmt1_syntax   ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
   13.51  
   13.52  
   13.53  section "subclass and subinterface relations"
    14.1 --- a/src/HOL/Bali/WellForm.thy	Tue Feb 09 16:07:09 2010 +0100
    14.2 +++ b/src/HOL/Bali/WellForm.thy	Wed Feb 10 00:45:16 2010 +0100
    14.3 @@ -2925,7 +2925,7 @@
    14.4      then show "?P m"
    14.5        by (auto simp add: permits_acc_def)
    14.6    next
    14.7 -    case (Overriding new C declC newm old Sup)
    14.8 +    case (Overriding new declC newm old Sup C)
    14.9      assume member_new: "G \<turnstile> new member_in C" and
   14.10                    new: "new = (declC, mdecl newm)" and
   14.11               override: "G \<turnstile> (declC, newm) overrides old" and
    15.1 --- a/src/HOL/Bali/WellType.thy	Tue Feb 09 16:07:09 2010 +0100
    15.2 +++ b/src/HOL/Bali/WellType.thy	Wed Feb 10 00:45:16 2010 +0100
    15.3 @@ -43,11 +43,9 @@
    15.4    "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
    15.5  
    15.6  
    15.7 -
    15.8 -syntax
    15.9 +abbreviation
   15.10    pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
   15.11 -translations 
   15.12 -  "pkg e" == "pid (cls e)"
   15.13 +  where "pkg e == pid (cls e)"
   15.14  
   15.15  section "Static overloading: maximally specific methods "
   15.16  
   15.17 @@ -426,29 +424,33 @@
   15.18                                           E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   15.19  
   15.20  
   15.21 -syntax (* for purely static typing *)
   15.22 -  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   15.23 -  "_wt_stmt" :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   15.24 -  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   15.25 -  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   15.26 -  "_ty_exprs":: "env \<Rightarrow> [expr list,
   15.27 -                     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   15.28 +(* for purely static typing *)
   15.29 +abbreviation
   15.30 +  wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   15.31 +  where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
   15.32 +
   15.33 +abbreviation
   15.34 +  wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   15.35 +  where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
   15.36 +
   15.37 +abbreviation
   15.38 +  ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   15.39 +  where "E|-e:-T == E|-In1l e :: Inl T"
   15.40  
   15.41 -syntax (xsymbols)
   15.42 -  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   15.43 -  "_wt_stmt" ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   15.44 -  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
   15.45 -  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   15.46 -  "_ty_exprs" :: "env \<Rightarrow> [expr list,
   15.47 -                    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   15.48 +abbreviation
   15.49 +  ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   15.50 +  where "E|-e:=T == E|-In2 e :: Inl T"
   15.51  
   15.52 -translations
   15.53 -        "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
   15.54 -        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
   15.55 -        "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
   15.56 -        "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>CONST Inl T"
   15.57 -        "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>CONST Inr T"
   15.58 +abbreviation
   15.59 +  ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   15.60 +  where "E|-e:#T == E|-In3 e :: Inr T"
   15.61  
   15.62 +notation (xsymbols)
   15.63 +  wt_syntax  ("_\<turnstile>_\<Colon>_"  [51,51,51] 50) and
   15.64 +  wt_stmt_syntax  ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50) and
   15.65 +  ty_expr_syntax  ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
   15.66 +  ty_var_syntax  ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
   15.67 +  ty_exprs_syntax  ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   15.68  
   15.69  declare not_None_eq [simp del] 
   15.70  declare split_if [split del] split_if_asm [split del]