# HG changeset patch
# User wenzelm
# Date 1280158886 -7200
# Node ID ee939247b2fb180c9c0f4693cf925b6f7ebf94b1
# Parent  f87d1105e181580667995416b3aa5f35c46ab21d
modernized/unified some specifications;

diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -20,8 +20,9 @@
            
 section "set of not yet initialzed classes"
 
-definition nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set" where
- "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
+definition
+  nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
+  where "nyinitcls G s = {C. is_class G C \<and> \<not> initd C s}"
 
 lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
 apply (unfold nyinitcls_def)
@@ -113,8 +114,9 @@
 
 section "init-le"
 
-definition init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_"  [51,51] 50) where
- "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
+definition
+  init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_"  [51,51] 50)
+  where "G\<turnstile>init\<le>n = (\<lambda>s. card (nyinitcls G s) \<le> n)"
   
 lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
 apply (unfold init_le_def)
@@ -132,27 +134,22 @@
 
 section "Most General Triples and Formulas"
 
-definition remember_init_state :: "state assn" ("\<doteq>") where
-  "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
+definition
+  remember_init_state :: "state assn" ("\<doteq>")
+  where "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
 
 lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
 apply (unfold remember_init_state_def)
 apply (simp (no_asm))
 done
 
-consts
-  
+definition
   MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
-  MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
+  where "{P} t\<succ> {G\<rightarrow>} = {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
 
-defs
-  
-
-  MGF_def:
-  "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
-
-  MGFn_def:
-  "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
+definition
+  MGFn :: "[nat, term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
+  where "{=:n} t\<succ> {G\<rightarrow>} = {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
 
 (* unused *)
 lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
@@ -574,9 +571,9 @@
 unroll the loop in iterated evaluations of the expression and evaluations of
 the loop body. *}
 
-definition unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set" where
-
- "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2.
+definition
+  unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set" where
+  "unroll G l e c = {(s,t). \<exists> v s1 s2.
                              G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and>
                              G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}"
 
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/AxExample.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -8,10 +8,11 @@
 imports AxSem Example
 begin
 
-definition arr_inv :: "st \<Rightarrow> bool" where
- "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
+definition
+  arr_inv :: "st \<Rightarrow> bool" where
+ "arr_inv = (\<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
                               values obj (Inl (arr, Base)) = Some (Addr a) \<and>
-                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"
+                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)"
 
 lemma arr_inv_new_obj: 
 "\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/AxSem.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -62,8 +62,9 @@
 translations
   (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
 
-definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
- "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
+definition
+  assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25)
+  where "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
   
 lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
 apply (unfold assn_imp_def)
@@ -75,8 +76,9 @@
 
 subsection "peek-and"
 
-definition peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13) where
- "P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"
+definition
+  peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
+  where "(P \<and>. p) = (\<lambda>Y s Z. P Y s Z \<and> p s)"
 
 lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"
 apply (unfold peek_and_def)
@@ -114,8 +116,9 @@
 
 subsection "assn-supd"
 
-definition assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13) where
- "P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"
+definition
+  assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
+  where "(P ;. f) = (\<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s)"
 
 lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"
 apply (unfold assn_supd_def)
@@ -124,8 +127,9 @@
 
 subsection "supd-assn"
 
-definition supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13) where
- "f .; P \<equiv> \<lambda>Y s. P Y (f s)"
+definition
+  supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
+  where "(f .; P) = (\<lambda>Y s. P Y (f s))"
 
 
 lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"
@@ -143,8 +147,9 @@
 
 subsection "subst-res"
 
-definition subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_"  [60,61] 60) where
- "P\<leftarrow>w \<equiv> \<lambda>Y. P w"
+definition
+  subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_"  [60,61] 60)
+  where "P\<leftarrow>w = (\<lambda>Y. P w)"
 
 lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"
 apply (unfold subst_res_def)
@@ -178,8 +183,9 @@
 
 subsection "subst-Bool"
 
-definition subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60) where
- "P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
+definition
+  subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60)
+  where "P\<leftarrow>=b = (\<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
 
 lemma subst_Bool_def2 [simp]: 
 "(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
@@ -193,8 +199,9 @@
 
 subsection "peek-res"
 
-definition peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
- "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
+definition
+  peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
+  where "peek_res Pf = (\<lambda>Y. Pf Y Y)"
 
 syntax
   "_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
@@ -221,8 +228,9 @@
 
 subsection "ign-res"
 
-definition ign_res :: "        'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000) where
-  "P\<down>        \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
+definition
+  ign_res :: "'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000)
+  where "P\<down> = (\<lambda>Y s Z. \<exists>Y. P Y s Z)"
 
 lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"
 apply (unfold ign_res_def)
@@ -252,8 +260,9 @@
 
 subsection "peek-st"
 
-definition peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
- "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
+definition
+  peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
+  where "peek_st P = (\<lambda>Y s. P (store s) Y s)"
 
 syntax
   "_peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
@@ -296,8 +305,9 @@
 
 subsection "ign-res-eq"
 
-definition ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_"  [60,61] 60) where
- "P\<down>=w       \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
+definition
+  ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_"  [60,61] 60)
+  where "P\<down>=w \<equiv> (\<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w))"
 
 lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"
 apply (unfold ign_res_eq_def)
@@ -326,8 +336,9 @@
 
 subsection "RefVar"
 
-definition RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13) where
- "vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"
+definition
+  RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13)
+  where "(vf ..; P) = (\<lambda>Y s. let (v,s') = vf s in P (Var v) s')"
  
 lemma RefVar_def2 [simp]: "(vf ..; P) Y s =  
   P (Var (fst (vf s))) (snd (vf s))"
@@ -337,12 +348,13 @@
 
 subsection "allocation"
 
-definition Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
- "Alloc G otag P \<equiv> \<lambda>Y s Z.
-                   \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"
+definition
+  Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+  where "Alloc G otag P = (\<lambda>Y s Z. \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)"
 
-definition SXAlloc     :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
- "SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"
+definition
+  SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+  where "SXAlloc G P = (\<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"
 
 
 lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =  
@@ -359,11 +371,12 @@
 
 section "validity"
 
-definition type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
- "type_ok G t s \<equiv> 
-    \<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
-                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
-              \<and> s\<Colon>\<preceq>(G,L)"
+definition
+  type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
+  "type_ok G t s =
+    (\<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
+                             \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
+               \<and> s\<Colon>\<preceq>(G,L))"
 
 datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
 something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
@@ -407,34 +420,35 @@
 
 definition mtriples :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 
                 ('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times>  'sig) set \<Rightarrow> 'a triples" ("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75) where
- "{{P} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
+ "{{P} tf-\<succ> {Q} | ms} = (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
   
-consts
-
- triple_valid :: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
-                                                (   "_\<Turnstile>_:_" [61,0, 58] 57)
-    ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
-                                                ("_,_|\<Turnstile>_"   [61,58,58] 57)
+definition
+  triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple  \<Rightarrow> bool"  ("_\<Turnstile>_:_" [61,0, 58] 57)
+  where
+    "G\<Turnstile>n:t =
+      (case t of {P} t\<succ> {Q} \<Rightarrow>
+        \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
+        (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z))"
 
 abbreviation
- triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
-                                                (  "_||=_:_" [61,0, 58] 57)
- where "G||=n:ts == Ball ts (triple_valid G n)"
+  triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"  (  "_||=_:_" [61,0, 58] 57)
+  where "G||=n:ts == Ball ts (triple_valid G n)"
+
+notation (xsymbols)
+  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57)
+
+
+definition
+  ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"  ("_,_|\<Turnstile>_" [61,58,58] 57)
+  where "(G,A|\<Turnstile>ts) = (\<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts)"
 
 abbreviation
- ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
-                                                ( "_,_|=_"   [61,58,58] 57)
- where "G,A |=t == G,A|\<Turnstile>{t}"
+  ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"  ( "_,_|=_"   [61,58,58] 57)
+  where "G,A |=t == G,A|\<Turnstile>{t}"
 
 notation (xsymbols)
-  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57) and
   ax_valid  ("_,_\<Turnstile>_" [61,58,58] 57)
 
-defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
-                          \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
-                          (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
-
-defs  ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
 
 lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
  (\<forall>Y s Z. P Y s Z 
@@ -625,8 +639,9 @@
 axioms 
 *)
 
-definition adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
-"adapt_pre P Q Q'\<equiv>\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z)"
+definition
+  adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+  where "adapt_pre P Q Q' = (\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z))"
 
 
 section "rules derived by induction"
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/AxSound.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -9,18 +9,15 @@
 
 section "validity"
 
-consts
-
- triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
-                                                (   "_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
-    ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
-                                                ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
-
-defs  triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
- \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) 
- \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
-                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
- (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L))))"
+definition
+  triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool"  ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
+  where
+    "G\<Turnstile>n\<Colon>t =
+      (case t of {P} t\<succ> {Q} \<Rightarrow>
+        \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L)
+          \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and>
+            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
+             (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))"
 
 text {* This definition differs from the ordinary  @{text triple_valid_def} 
 manly in the conclusion: We also ensures conformance of the result state. So
@@ -29,8 +26,10 @@
 proof of the axiomatic semantics, in the end we will conclude to 
 the ordinary definition.
 *}
- 
-defs  ax_valids2_def:    "G,A|\<Turnstile>\<Colon>ts \<equiv>  \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)"
+
+definition
+  ax_valids2 :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"  ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
+  where "G,A|\<Turnstile>\<Colon>ts = (\<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t))"
 
 lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} =  
  (\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow>  
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Basis.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -180,31 +180,34 @@
 
 notation sum_case  (infixr "'(+')"80)
 
-consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
-          the_Inr  :: "'a + 'b \<Rightarrow> 'b"
-primrec  "the_Inl (Inl a) = a"
-primrec  "the_Inr (Inr b) = b"
+primrec the_Inl  :: "'a + 'b \<Rightarrow> 'a"
+  where "the_Inl (Inl a) = a"
+
+primrec the_Inr  :: "'a + 'b \<Rightarrow> 'b"
+  where "the_Inr (Inr b) = b"
 
 datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
 
-consts    the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
-          the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
-          the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
-primrec  "the_In1 (In1 a) = a"
-primrec  "the_In2 (In2 b) = b"
-primrec  "the_In3 (In3 c) = c"
+primrec the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
+  where "the_In1 (In1 a) = a"
+
+primrec the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
+  where "the_In2 (In2 b) = b"
+
+primrec the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
+  where "the_In3 (In3 c) = c"
 
 abbreviation In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
-      where "In1l e == In1 (Inl e)"
+  where "In1l e == In1 (Inl e)"
 
 abbreviation In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
-      where "In1r c == In1 (Inr c)"
+  where "In1r c == In1 (Inr c)"
 
 abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
-      where "the_In1l == the_Inl \<circ> the_In1"
+  where "the_In1l == the_Inl \<circ> the_In1"
 
 abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
-      where "the_In1r == the_Inr \<circ> the_In1"
+  where "the_In1r == the_Inr \<circ> the_In1"
 
 ML {*
 fun sum3_instantiate ctxt thm = map (fn s =>
@@ -232,8 +235,9 @@
 
 text{* Deemed too special for theory Map. *}
 
-definition chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" where
- "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
+definition
+  chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
+  where "chg_map f a m = (case m a of None => m | Some b => m(a|->f b))"
 
 lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
 by (unfold chg_map_def, auto)
@@ -247,8 +251,9 @@
 
 section "unique association lists"
 
-definition unique :: "('a \<times> 'b) list \<Rightarrow> bool" where
- "unique \<equiv> distinct \<circ> map fst"
+definition
+  unique :: "('a \<times> 'b) list \<Rightarrow> bool"
+  where "unique = distinct \<circ> map fst"
 
 lemma uniqueD [rule_format (no_asm)]: 
 "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
@@ -296,11 +301,11 @@
 
 section "list patterns"
 
-consts
-  lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
-defs
-  lsplit_def:    "lsplit == %f l. f (hd l) (tl l)"
-(*  list patterns -- extends pre-defined type "pttrn" used in abstractions *)
+definition
+  lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b" where
+  "lsplit = (\<lambda>f l. f (hd l) (tl l))"
+
+text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *}
 syntax
   "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
 translations
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Conform.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -96,8 +96,8 @@
 
 section "value conformance"
 
-definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70) where
-           "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
+definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
+  where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
 
 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
 by (auto simp: conf_def)
@@ -177,8 +177,9 @@
 
 section "value list conformance"
 
-definition lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) where
-           "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
+definition
+  lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
+  where "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
 
 lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T"
 by (force simp: lconf_def)
@@ -260,8 +261,9 @@
 *}
 
   
-definition wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70) where
-           "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
+definition
+  wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
+  where "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
 
 lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
 by (auto simp: wlconf_def)
@@ -338,11 +340,12 @@
 
 section "object conformance"
 
-definition oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
-           "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
+definition
+  oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
+  "(G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r) = (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
                            (case r of 
                               Heap a \<Rightarrow> is_type G (obj_ty obj) 
-                            | Stat C \<Rightarrow> True)"
+                            | Stat C \<Rightarrow> True))"
 
 
 lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
@@ -373,12 +376,14 @@
 
 section "state conformance"
 
-definition conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"   ("_\<Colon>\<preceq>_"   [71,71]      70)  where
-   "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
-    (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
-                \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
-    (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
-         (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)"
+definition
+  conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"  ("_\<Colon>\<preceq>_" [71,71] 70)  where
+   "xs\<Colon>\<preceq>E =
+      (let (G, L) = E; s = snd xs; l = locals s in
+        (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
+                    \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
+        (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
+             (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
 
 section "conforms"
 
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Decl.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -206,8 +206,9 @@
   (type) "mdecl" <= (type) "sig \<times> methd"
 
 
-definition mhead :: "methd \<Rightarrow> mhead" where
-  "mhead m \<equiv> \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
+definition
+  mhead :: "methd \<Rightarrow> mhead"
+  where "mhead m = \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
 
 lemma access_mhead [simp]:"access (mhead m) = access m"
 by (simp add: mhead_def)
@@ -237,7 +238,7 @@
 
 definition
 memberdecl_memberid_def:
-  "memberid m \<equiv> (case m of
+  "memberid m = (case m of
                     fdecl (vn,f)  \<Rightarrow> fid vn
                   | mdecl (sig,m) \<Rightarrow> mid sig)"
 
@@ -262,7 +263,7 @@
 
 definition
 pair_memberid_def:
-  "memberid p \<equiv> memberid (snd p)"
+  "memberid p = memberid (snd p)"
 
 instance ..
 
@@ -274,8 +275,9 @@
 lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
 by (simp add: pair_memberid_def)
 
-definition is_field :: "qtname \<times> memberdecl \<Rightarrow> bool" where
-"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)"
+definition
+  is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
+  where "is_field m = (\<exists> declC f. m=(declC,fdecl f))"
   
 lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
 by (simp add: is_field_def)
@@ -283,8 +285,9 @@
 lemma is_fieldI: "is_field (C,fdecl f)"
 by (simp add: is_field_def)
 
-definition is_method :: "qtname \<times> memberdecl \<Rightarrow> bool" where
-"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)"
+definition
+  is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
+  where "is_method membr = (\<exists>declC m. membr=(declC,mdecl m))"
   
 lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
 by (simp add: is_method_def)
@@ -314,8 +317,9 @@
                       isuperIfs::qtname list,\<dots>::'a\<rparr>"
   (type) "idecl" <= (type) "qtname \<times> iface"
 
-definition ibody :: "iface \<Rightarrow> ibody" where
-  "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
+definition
+  ibody :: "iface \<Rightarrow> ibody"
+  where "ibody i = \<lparr>access=access i,imethods=imethods i\<rparr>"
 
 lemma access_ibody [simp]: "(access (ibody i)) = access i"
 by (simp add: ibody_def)
@@ -349,8 +353,9 @@
                       super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
   (type) "cdecl" <= (type) "qtname \<times> class"
 
-definition cbody :: "class \<Rightarrow> cbody" where
-  "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
+definition
+  cbody :: "class \<Rightarrow> cbody"
+  where "cbody c = \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
 
 lemma access_cbody [simp]:"access (cbody c) = access c"
 by (simp add: cbody_def)
@@ -368,18 +373,17 @@
 section "standard classes"
 
 consts
-
   Object_mdecls  ::  "mdecl list" --{* methods of Object *}
   SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
-  ObjectC ::         "cdecl"      --{* declaration  of root      class   *}
-  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *}
-
-defs 
 
+definition
+  ObjectC ::         "cdecl"      --{* declaration  of root      class   *} where
+  "ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
+                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
 
-ObjectC_def:"ObjectC  \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
-                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
-SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
+definition
+  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *} where
+  "SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
                                    init=Skip,
                                    super=if xn = Throwable then Object 
                                                            else SXcpt Throwable,
@@ -391,8 +395,9 @@
 lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
 by (simp add: SXcptC_def)
 
-definition standard_classes :: "cdecl list" where
-         "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
+definition
+  standard_classes :: "cdecl list" where
+  "standard_classes = [ObjectC, SXcptC Throwable,
                 SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
                 SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
 
@@ -426,16 +431,15 @@
 
 section "is type"
 
-consts
-  is_type :: "prog \<Rightarrow>     ty \<Rightarrow> bool"
-  isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
-
-primrec "is_type G (PrimT pt)  = True"
-        "is_type G (RefT  rt)  = isrtype G rt"
-        "isrtype G (NullT    ) = True"
-        "isrtype G (IfaceT tn) = is_iface G tn"
-        "isrtype G (ClassT tn) = is_class G tn"
-        "isrtype G (ArrayT T ) = is_type  G T"
+primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
+  and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
+where
+  "is_type G (PrimT pt)  = True"
+| "is_type G (RefT  rt)  = isrtype G rt"
+| "isrtype G (NullT) = True"
+| "isrtype G (IfaceT tn) = is_iface G tn"
+| "isrtype G (ClassT tn) = is_class G tn"
+| "isrtype G (ArrayT T ) = is_type  G T"
 
 lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
 by auto
@@ -446,13 +450,13 @@
 
 section "subinterface and subclass relation, in anticipation of TypeRel.thy"
 
-consts 
+definition
   subint1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
-  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass     *}
+  where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
 
-defs
-  subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
-  subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
+definition
+  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass *}
+  where "subcls1 G = {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
 
 abbreviation
   subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
@@ -517,15 +521,18 @@
 
 section "well-structured programs"
 
-definition ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool" where
- "ws_idecl G I si \<equiv> \<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+"
+definition
+  ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
+  where "ws_idecl G I si = (\<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+)"
   
-definition ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" where
- "ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
+definition
+  ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
+  where "ws_cdecl G C sc = (C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+)"
   
-definition ws_prog  :: "prog \<Rightarrow> bool" where
- "ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
-              (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))"
+definition
+  ws_prog  :: "prog \<Rightarrow> bool" where
+  "ws_prog G = ((\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
+                 (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c)))"
 
 
 lemma ws_progI: 
@@ -810,10 +817,10 @@
 apply simp
 done
 
-definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+definition
+  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
-"imethds G I 
-  \<equiv> iface_rec G I  
+  "imethds G I = iface_rec G I
               (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
                         (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
         
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -9,7 +9,7 @@
 section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
 
 definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where
-"is_public G qn \<equiv> (case class G qn of
+"is_public G qn = (case class G qn of
                      None       \<Rightarrow> (case iface G qn of
                                       None       \<Rightarrow> False
                                     | Some i \<Rightarrow> access i = Public)
@@ -21,33 +21,35 @@
 in their package or if they are defined public, an array type is accessible if
 its element type is accessible *}
  
-consts accessible_in   :: "prog \<Rightarrow> ty     \<Rightarrow> pname \<Rightarrow> bool"  
-                                      ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60)
-       rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" 
-                                      ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) 
 primrec
-"G\<turnstile>(PrimT p)   accessible_in pack  = True"
-accessible_in_RefT_simp: 
-"G\<turnstile>(RefT  r)   accessible_in pack  = G\<turnstile>r accessible_in' pack"
-
-"G\<turnstile>(NullT)     accessible_in' pack = True"
-"G\<turnstile>(IfaceT I)  accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
-"G\<turnstile>(ClassT C)  accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
-"G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
+  accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool"  ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and
+  rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool"  ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)
+where
+  "G\<turnstile>(PrimT p) accessible_in pack = True"
+| accessible_in_RefT_simp:
+  "G\<turnstile>(RefT  r) accessible_in pack = G\<turnstile>r accessible_in' pack"
+| "G\<turnstile>(NullT) accessible_in' pack = True"
+| "G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
+| "G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
+| "G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
 
 declare accessible_in_RefT_simp [simp del]
 
-definition is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
-    "is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
+definition
+  is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
+  where "is_acc_class G P C = (is_class G C \<and> G\<turnstile>(Class C) accessible_in P)"
 
-definition is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
-    "is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
+definition
+  is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
+  where "is_acc_iface G P I = (is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P)"
 
-definition is_acc_type  :: "prog \<Rightarrow> pname \<Rightarrow> ty     \<Rightarrow> bool" where
-    "is_acc_type  G P T \<equiv> is_type G T  \<and> G\<turnstile>T accessible_in P"
+definition
+  is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool"
+  where "is_acc_type  G P T = (is_type G T  \<and> G\<turnstile>T accessible_in P)"
 
-definition is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool" where
-  "is_acc_reftype  G P T \<equiv> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
+definition
+  is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
+  where "is_acc_reftype G P T = (isrtype G T  \<and> G\<turnstile>T accessible_in' P)"
 
 lemma is_acc_classD:
  "is_acc_class G P C \<Longrightarrow>  is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
@@ -87,7 +89,7 @@
 begin
 
 definition
-  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
+  acc_modi_accmodi_def: "accmodi (a::acc_modi) = a"
 
 instance ..
 
@@ -100,7 +102,7 @@
 begin
 
 definition
-  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
+  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) = access d"
 
 instance ..
 
@@ -113,7 +115,7 @@
 begin
 
 definition
-  pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
+  pair_acc_modi_def: "accmodi p = accmodi (snd p)"
 
 instance ..
 
@@ -126,7 +128,7 @@
 begin
 
 definition
-  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
+  memberdecl_acc_modi_def: "accmodi m = (case m of
                                           fdecl f \<Rightarrow> accmodi f
                                         | mdecl m \<Rightarrow> accmodi m)"
 
@@ -152,7 +154,7 @@
 begin
 
 definition
-  "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
+  "declclass q = \<lparr> pid = pid q, tid = tid q \<rparr>"
 
 instance ..
 
@@ -169,7 +171,7 @@
 begin
 
 definition
-  pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
+  pair_declclass_def: "declclass p = declclass (fst p)"
 
 instance ..
 
@@ -208,7 +210,7 @@
 begin
 
 definition
-  pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
+  pair_is_static_def: "is_static p = is_static (snd p)"
 
 instance ..
 
@@ -225,7 +227,7 @@
 
 definition
 memberdecl_is_static_def: 
- "is_static m \<equiv> (case m of
+ "is_static m = (case m of
                     fdecl f \<Rightarrow> is_static f
                   | mdecl m \<Rightarrow> is_static m)"
 
@@ -246,28 +248,34 @@
 
 -- {* some mnemotic selectors for various pairs *} 
 
-definition decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
+definition
+  decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
   "decliface = fst"          --{* get the interface component *}
 
-definition mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
+definition
+  mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
   "mbr = snd"            --{* get the memberdecl component *}
 
-definition mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
+definition
+  mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
   "mthd = snd"              --{* get the method component *}
     --{* also used for mdecl, mhead *}
 
-definition fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
+definition
+  fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
   "fld = snd"               --{* get the field component *}
     --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
 
 -- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
 
-definition fname:: "vname \<times> 'a \<Rightarrow> vname" where 
-  "fname = fst"
+definition
+  fname:: "vname \<times> 'a \<Rightarrow> vname"
+  where "fname = fst"
     --{* also used for fdecl *}
 
-definition declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" where
-  "declclassf = snd"
+definition
+  declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
+  where "declclassf = snd"
 
 
 lemma decliface_simp[simp]: "decliface (I,m) = I"
@@ -320,11 +328,13 @@
 
   --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
 
-definition fldname :: "vname \<times> qtname \<Rightarrow> vname"  where
-  "fldname = fst"
+definition
+  fldname :: "vname \<times> qtname \<Rightarrow> vname"
+  where "fldname = fst"
 
-definition fldclass :: "vname \<times> qtname \<Rightarrow> qtname" where
-  "fldclass = snd"
+definition
+  fldclass :: "vname \<times> qtname \<Rightarrow> qtname"
+  where "fldclass = snd"
 
 lemma fldname_simp[simp]: "fldname (n,c) = n"
 by (simp add: fldname_def)
@@ -338,8 +348,9 @@
 text {* Convert a qualified method declaration (qualified with its declaring 
 class) to a qualified member declaration:  @{text methdMembr}  *}
 
-definition methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" where
- "methdMembr m = (fst m, mdecl (snd m))"
+definition
+  methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl"
+  where "methdMembr m = (fst m, mdecl (snd m))"
 
 lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
 by (simp add: methdMembr_def)
@@ -356,8 +367,9 @@
 text {* Convert a qualified method (qualified with its declaring 
 class) to a qualified member declaration:  @{text method}  *}
 
-definition method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" where 
-"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"
+definition
+  method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
+  where "method sig m = (declclass m, mdecl (sig, mthd m))"
 
 lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
 by (simp add: method_def)
@@ -377,8 +389,9 @@
 lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
   by (simp add: method_def) 
 
-definition fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" where 
-"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"
+definition
+  fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)"
+  where "fieldm n f = (declclass f, fdecl (n, fld f))"
 
 lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
 by (simp add: fieldm_def)
@@ -401,8 +414,9 @@
 text {* Select the signature out of a qualified method declaration:
  @{text msig} *}
 
-definition msig :: "(qtname \<times> mdecl) \<Rightarrow> sig" where
-"msig m \<equiv> fst (snd m)"
+definition
+  msig :: "(qtname \<times> mdecl) \<Rightarrow> sig"
+  where "msig m = fst (snd m)"
 
 lemma msig_simp[simp]: "msig (c,(s,m)) = s"
 by (simp add: msig_def)
@@ -410,8 +424,9 @@
 text {* Convert a qualified method (qualified with its declaring 
 class) to a qualified method declaration:  @{text qmdecl}  *}
 
-definition qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)" where
-"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"
+definition
+  qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
+  where "qmdecl sig m = (declclass m, (sig,mthd m))"
 
 lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
 by (simp add: qmdecl_def)
@@ -476,7 +491,7 @@
 begin
 
 definition
-  pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
+  pair_resTy_def: "resTy p = resTy (snd p)"
 
 instance ..
 
@@ -503,14 +518,15 @@
       it is not accessible for inheritance at all.
 \end{itemize}
 *}
-definition inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60) where
-                  
-"G\<turnstile>membr inheritable_in pack 
-  \<equiv> (case (accmodi membr) of
-       Private   \<Rightarrow> False
-     | Package   \<Rightarrow> (pid (declclass membr)) = pack
-     | Protected \<Rightarrow> True
-     | Public    \<Rightarrow> True)"
+definition
+  inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
+where
+"G\<turnstile>membr inheritable_in pack =
+  (case (accmodi membr) of
+     Private   \<Rightarrow> False
+   | Package   \<Rightarrow> (pid (declclass membr)) = pack
+   | Protected \<Rightarrow> True
+   | Public    \<Rightarrow> True)"
 
 abbreviation
 Method_inheritable_in_syntax::
@@ -526,24 +542,26 @@
 
 subsubsection "declared-in/undeclared-in"
 
-definition cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
-"cdeclaredmethd G C 
-  \<equiv> (case class G C of
+definition
+  cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
+  "cdeclaredmethd G C =
+    (case class G C of
        None \<Rightarrow> \<lambda> sig. None
-     | Some c \<Rightarrow> table_of (methods c)
-    )"
+     | Some c \<Rightarrow> table_of (methods c))"
 
-definition cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
-"cdeclaredfield G C 
-  \<equiv> (case class G C of
-       None \<Rightarrow> \<lambda> sig. None
-     | Some c \<Rightarrow> table_of (cfields c)
-    )"
+definition
+  cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
+  "cdeclaredfield G C =
+    (case class G C of
+      None \<Rightarrow> \<lambda> sig. None
+    | Some c \<Rightarrow> table_of (cfields c))"
 
-definition declared_in :: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60) where
-"G\<turnstile>m declared_in C \<equiv> (case m of
-                        fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
-                      | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
+definition
+  declared_in :: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
+where
+  "G\<turnstile>m declared_in C = (case m of
+                          fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
+                        | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
 
 abbreviation
 method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
@@ -560,10 +578,12 @@
 by (cases m) 
    (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
 
-definition undeclared_in :: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60) where
-"G\<turnstile>m undeclared_in C \<equiv> (case m of
-                            fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
-                          | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
+definition
+  undeclared_in :: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
+where
+  "G\<turnstile>m undeclared_in C = (case m of
+                           fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
+                         | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
 
 
 subsubsection "members"
@@ -607,17 +627,20 @@
                            ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
  where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
 
-definition inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60) where
-"G\<turnstile>C inherits m 
-  \<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
-    (\<exists> S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)"
+definition
+  inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60)
+where
+  "G\<turnstile>C inherits m =
+    (G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
+      (\<exists>S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S))"
 
 lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
 by (auto simp add: inherits_def intro: members.Inherited)
 
 
-definition member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60) where
-"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
+definition
+  member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
+  where "G\<turnstile>m member_in C = (\<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC)"
 text {* A member is in a class if it is member of the class or a superclass.
 If a member is in a class we can select this member. This additional notion
 is necessary since not all members are inherited to subclasses. So such
@@ -703,13 +726,15 @@
 
 subsubsection "Hiding"
 
-definition hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60) where 
-"G\<turnstile>new hides old
-  \<equiv> is_static new \<and> msig new = msig old \<and>
-    G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
-    G\<turnstile>Method new declared_in (declclass new) \<and>
-    G\<turnstile>Method old declared_in (declclass old) \<and> 
-    G\<turnstile>Method old inheritable_in pid (declclass new)"
+definition
+  hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60)
+where 
+  "G\<turnstile>new hides old =
+    (is_static new \<and> msig new = msig old \<and>
+      G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
+      G\<turnstile>Method new declared_in (declclass new) \<and>
+      G\<turnstile>Method old declared_in (declclass old) \<and> 
+      G\<turnstile>Method old inheritable_in pid (declclass new))"
 
 abbreviation
 sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
@@ -762,16 +787,18 @@
 by (auto simp add: hides_def)
 
 subsubsection "permits access" 
-definition permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60) where
-"G\<turnstile>membr in cls permits_acc_from accclass 
-  \<equiv> (case (accmodi membr) of
-       Private   \<Rightarrow> (declclass membr = accclass)
-     | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
-     | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
+definition
+  permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
+where
+  "G\<turnstile>membr in cls permits_acc_from accclass =
+    (case (accmodi membr) of
+      Private   \<Rightarrow> (declclass membr = accclass)
+    | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
+    | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
                     \<or>
                     (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
                      \<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr)) 
-     | Public    \<Rightarrow> True)"
+    | Public    \<Rightarrow> True)"
 text {*
 The subcondition of the @{term "Protected"} case: 
 @{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
@@ -1380,24 +1407,25 @@
 translations 
   (type) "fspec" <= (type) "vname \<times> qtname" 
 
-definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
-"imethds G I 
-  \<equiv> iface_rec G I  
-              (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
+definition
+  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+  "imethds G I =
+    iface_rec G I  (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
                         (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
 text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
 
-definition accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
-"accimethds G pack I
-  \<equiv> if G\<turnstile>Iface I accessible_in pack 
-       then imethds G I
-       else (\<lambda> k. {})"
+definition
+  accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+  "accimethds G pack I =
+    (if G\<turnstile>Iface I accessible_in pack 
+     then imethds G I
+     else (\<lambda> k. {}))"
 text {* only returns imethds if the interface is accessible *}
 
-definition methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
-
-"methd G C 
- \<equiv> class_rec G C empty
+definition
+  methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "methd G C =
+    class_rec G C empty
              (\<lambda>C c subcls_mthds. 
                filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
                           subcls_mthds 
@@ -1409,10 +1437,10 @@
      Every new method with the same signature coalesces the
      method of a superclass. *}
 
-definition accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
-"accmethd G S C 
- \<equiv> filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) 
-              (methd G C)"
+definition
+  accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "accmethd G S C =
+    filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) (methd G C)"
 text {* @{term "accmethd G S C"}: only those methods of @{term "methd G C"}, 
         accessible from S *}
 
@@ -1423,23 +1451,24 @@
     So we must test accessibility of method @{term m} of class @{term C} 
     (not @{term "declclass m"}) *}
 
-definition dynmethd :: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynmethd G statC dynC  
-  \<equiv> \<lambda> sig. 
-     (if G\<turnstile>dynC \<preceq>\<^sub>C statC
-        then (case methd G statC sig of
-                None \<Rightarrow> None
-              | Some statM 
-                  \<Rightarrow> (class_rec G dynC empty
-                       (\<lambda>C c subcls_mthds. 
-                          subcls_mthds
-                          ++
-                          (filter_tab 
-                            (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
-                            (methd G C) ))
-                      ) sig
-              )
-        else None)"
+definition
+  dynmethd :: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "dynmethd G statC dynC =
+    (\<lambda>sig.
+       (if G\<turnstile>dynC \<preceq>\<^sub>C statC
+          then (case methd G statC sig of
+                  None \<Rightarrow> None
+                | Some statM 
+                    \<Rightarrow> (class_rec G dynC empty
+                         (\<lambda>C c subcls_mthds. 
+                            subcls_mthds
+                            ++
+                            (filter_tab 
+                              (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
+                              (methd G C) ))
+                        ) sig
+                )
+          else None))"
 
 text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference 
         with dynamic class @{term dynC} and static class @{term statC} *}
@@ -1449,11 +1478,12 @@
         filters the new methods (to get only those methods which actually
         override the methods of the static class) *}
 
-definition dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynimethd G I dynC 
-  \<equiv> \<lambda> sig. if imethds G I sig \<noteq> {}
-               then methd G dynC sig
-               else dynmethd G Object dynC sig"
+definition
+  dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "dynimethd G I dynC =
+    (\<lambda>sig. if imethds G I sig \<noteq> {}
+           then methd G dynC sig
+           else dynmethd G Object dynC sig)"
 text {* @{term "dynimethd G I dynC"}: dynamic method lookup of a reference with 
         dynamic class dynC and static interface type I *}
 text {* 
@@ -1468,31 +1498,34 @@
    down to the actual dynamic class.
  *}
 
-definition dynlookup :: "prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynlookup G statT dynC
-  \<equiv> (case statT of
-       NullT        \<Rightarrow> empty
-     | IfaceT I     \<Rightarrow> dynimethd G I      dynC
-     | ClassT statC \<Rightarrow> dynmethd  G statC  dynC
-     | ArrayT ty    \<Rightarrow> dynmethd  G Object dynC)"
+definition
+  dynlookup :: "prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+  "dynlookup G statT dynC =
+    (case statT of
+      NullT        \<Rightarrow> empty
+    | IfaceT I     \<Rightarrow> dynimethd G I      dynC
+    | ClassT statC \<Rightarrow> dynmethd  G statC  dynC
+    | ArrayT ty    \<Rightarrow> dynmethd  G Object dynC)"
 text {* @{term "dynlookup G statT dynC"}: dynamic lookup of a method within the 
     static reference type statT and the dynamic class dynC. 
     In a wellformd context statT will not be NullT and in case
     statT is an array type, dynC=Object *}
 
-definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
-"fields G C 
-  \<equiv> class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
+definition
+  fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
+  "fields G C =
+    class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
 text {* @{term "fields G C"} 
      list of fields of a class, including all the fields of the superclasses
      (private, inherited and hidden ones) not only the accessible ones
      (an instance of a object allocates all these fields *}
 
-definition accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table" where
-"accfield G S C
-  \<equiv> let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
-    in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
-                  field_tab"
+definition
+  accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table" where
+  "accfield G S C =
+    (let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
+      in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
+                    field_tab)"
 text  {* @{term "accfield G C S"}: fields of a class @{term C} which are 
          accessible from scope of class
          @{term S} with inheritance and hiding, cf. 8.3 *}
@@ -1503,11 +1536,13 @@
    inheritance, too. So we must test accessibility of field @{term f} of class 
    @{term C} (not @{term "declclass f"}) *} 
 
-definition is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool" where
- "is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None"
+definition
+  is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool"
+  where "is_methd G = (\<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None)"
 
-definition efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)" where
-"efname \<equiv> fst"
+definition
+  efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)"
+  where "efname = fst"
 
 lemma efname_simp[simp]:"efname (n,f) = n"
 by (simp add: efname_def) 
@@ -2270,8 +2305,9 @@
 
 section "calculation of the superclasses of a class"
 
-definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
- "superclasses G C \<equiv> class_rec G C {} 
+definition
+  superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
+ "superclasses G C = class_rec G C {} 
                        (\<lambda> C c superclss. (if C=Object 
                                             then {} 
                                             else insert (super c) superclss))"
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -49,33 +49,33 @@
 with a jump, since no breaks, continues or returns are allowed in an 
 expression. *}
 
-consts jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
-primrec
-"jumpNestingOkS jmps (Skip)   = True"
-"jumpNestingOkS jmps (Expr e) = True"
-"jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
-"jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
-                                 jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
-                                           jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
+primrec jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
+where
+  "jumpNestingOkS jmps (Skip)   = True"
+| "jumpNestingOkS jmps (Expr e) = True"
+| "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
+| "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
+                                   jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
+                                             jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
 --{* The label of the while loop only handles continue jumps. Breaks are only
      handled by @{term Lab} *}
-"jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
-"jumpNestingOkS jmps (Throw e) = True"
-"jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
-                                                jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
-                                        jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (Init C) = True" 
+| "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
+| "jumpNestingOkS jmps (Throw e) = True"
+| "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
+                                                  jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
+                                          jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (Init C) = True" 
  --{* wellformedness of the program must enshure that for all initializers 
       jumpNestingOkS {} holds *} 
 --{* Dummy analysis for intermediate smallstep term @{term  FinA} *}
-"jumpNestingOkS jmps (FinA a c) = False"
+| "jumpNestingOkS jmps (FinA a c) = False"
 
 
 definition jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool" where
-"jumpNestingOk jmps t \<equiv> (case t of
+"jumpNestingOk jmps t = (case t of
                       In1 se \<Rightarrow> (case se of
                                    Inl e \<Rightarrow> True
                                  | Inr s \<Rightarrow> jumpNestingOkS jmps s)
@@ -116,48 +116,46 @@
 
 subsection {* Very restricted calculation fallback calculation *}
 
-consts the_LVar_name:: "var \<Rightarrow> lname"
-primrec 
-"the_LVar_name (LVar n) = n"
+primrec the_LVar_name :: "var \<Rightarrow> lname"
+  where "the_LVar_name (LVar n) = n"
 
-consts assignsE :: "expr      \<Rightarrow> lname set" 
-       assignsV :: "var       \<Rightarrow> lname set"
-       assignsEs:: "expr list \<Rightarrow> lname set"
-text {* *}
-primrec
-"assignsE (NewC c)            = {}" 
-"assignsE (NewA t e)          = assignsE e"
-"assignsE (Cast t e)          = assignsE e"
-"assignsE (e InstOf r)        = assignsE e"
-"assignsE (Lit val)           = {}"
-"assignsE (UnOp unop e)       = assignsE e"
-"assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
-                                     then (assignsE e1)
-                                     else (assignsE e1) \<union> (assignsE e2))" 
-"assignsE (Super)             = {}"
-"assignsE (Acc v)             = assignsV v"
-"assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
-                                 (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
-                                                     else {})"
-"assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
-"assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
-                          = (assignsE objRef) \<union> (assignsEs args)"
+primrec assignsE :: "expr \<Rightarrow> lname set" 
+  and assignsV :: "var \<Rightarrow> lname set"
+  and assignsEs:: "expr list \<Rightarrow> lname set"
+where
+  "assignsE (NewC c)            = {}" 
+| "assignsE (NewA t e)          = assignsE e"
+| "assignsE (Cast t e)          = assignsE e"
+| "assignsE (e InstOf r)        = assignsE e"
+| "assignsE (Lit val)           = {}"
+| "assignsE (UnOp unop e)       = assignsE e"
+| "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
+                                       then (assignsE e1)
+                                       else (assignsE e1) \<union> (assignsE e2))" 
+| "assignsE (Super)             = {}"
+| "assignsE (Acc v)             = assignsV v"
+| "assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
+                                   (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
+                                                       else {})"
+| "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
+| "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
+                            = (assignsE objRef) \<union> (assignsEs args)"
 -- {* Only dummy analysis for intermediate expressions  
       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
-"assignsE (Methd C sig)   = {}" 
-"assignsE (Body  C s)     = {}"   
-"assignsE (InsInitE s e)  = {}"  
-"assignsE (Callee l e)    = {}" 
+| "assignsE (Methd C sig)   = {}" 
+| "assignsE (Body  C s)     = {}"   
+| "assignsE (InsInitE s e)  = {}"  
+| "assignsE (Callee l e)    = {}" 
 
-"assignsV (LVar n)       = {}"
-"assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
-"assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
+| "assignsV (LVar n)       = {}"
+| "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
+| "assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
 
-"assignsEs     [] = {}"
-"assignsEs (e#es) = assignsE e \<union> assignsEs es"
+| "assignsEs     [] = {}"
+| "assignsEs (e#es) = assignsE e \<union> assignsEs es"
 
 definition assigns :: "term \<Rightarrow> lname set" where
-"assigns t \<equiv> (case t of
+"assigns t = (case t of
                 In1 se \<Rightarrow> (case se of
                              Inl e \<Rightarrow> assignsE e
                            | Inr s \<Rightarrow> {})
@@ -190,42 +188,42 @@
 
 subsection "Analysis of constant expressions"
 
-consts constVal :: "expr \<Rightarrow> val option"
-primrec 
-"constVal (NewC c)      = None"
-"constVal (NewA t e)    = None"
-"constVal (Cast t e)    = None"
-"constVal (Inst e r)    = None"
-"constVal (Lit val)     = Some val"
-"constVal (UnOp unop e) = (case (constVal e) of
-                             None   \<Rightarrow> None
-                           | Some v \<Rightarrow> Some (eval_unop unop v))" 
-"constVal (BinOp binop e1 e2) = (case (constVal e1) of
-                                   None    \<Rightarrow> None
-                                 | Some v1 \<Rightarrow> (case (constVal e2) of 
-                                                None    \<Rightarrow> None
-                                              | Some v2 \<Rightarrow> Some (eval_binop 
-                                                                 binop v1 v2)))"
-"constVal (Super)         = None"
-"constVal (Acc v)         = None"
-"constVal (Ass v e)       = None"
-"constVal (Cond b e1 e2)  = (case (constVal b) of
+primrec constVal :: "expr \<Rightarrow> val option"
+where
+  "constVal (NewC c)      = None"
+| "constVal (NewA t e)    = None"
+| "constVal (Cast t e)    = None"
+| "constVal (Inst e r)    = None"
+| "constVal (Lit val)     = Some val"
+| "constVal (UnOp unop e) = (case (constVal e) of
                                None   \<Rightarrow> None
-                             | Some bv\<Rightarrow> (case the_Bool bv of
-                                            True \<Rightarrow> (case (constVal e2) of
-                                                       None   \<Rightarrow> None
-                                                     | Some v \<Rightarrow> constVal e1)
-                                          | False\<Rightarrow> (case (constVal e1) of
-                                                       None   \<Rightarrow> None
-                                                     | Some v \<Rightarrow> constVal e2)))"
+                             | Some v \<Rightarrow> Some (eval_unop unop v))" 
+| "constVal (BinOp binop e1 e2) = (case (constVal e1) of
+                                     None    \<Rightarrow> None
+                                   | Some v1 \<Rightarrow> (case (constVal e2) of 
+                                                  None    \<Rightarrow> None
+                                                | Some v2 \<Rightarrow> Some (eval_binop 
+                                                                   binop v1 v2)))"
+| "constVal (Super)         = None"
+| "constVal (Acc v)         = None"
+| "constVal (Ass v e)       = None"
+| "constVal (Cond b e1 e2)  = (case (constVal b) of
+                                 None   \<Rightarrow> None
+                               | Some bv\<Rightarrow> (case the_Bool bv of
+                                              True \<Rightarrow> (case (constVal e2) of
+                                                         None   \<Rightarrow> None
+                                                       | Some v \<Rightarrow> constVal e1)
+                                            | False\<Rightarrow> (case (constVal e1) of
+                                                         None   \<Rightarrow> None
+                                                       | Some v \<Rightarrow> constVal e2)))"
 --{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be.
      It requires that all tree expressions are constant even if we can decide
      which branch to choose, provided the constant value of @{term b} *}
-"constVal (Call accC statT mode objRef mn pTs args) = None"
-"constVal (Methd C sig)   = None" 
-"constVal (Body  C s)     = None"   
-"constVal (InsInitE s e)  = None"  
-"constVal (Callee l e)    = None" 
+| "constVal (Call accC statT mode objRef mn pTs args) = None"
+| "constVal (Methd C sig)   = None" 
+| "constVal (Body  C s)     = None"   
+| "constVal (InsInitE s e)  = None"  
+| "constVal (Callee l e)    = None" 
 
 lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]: 
   assumes const: "constVal e = Some v" and
@@ -282,55 +280,55 @@
 to a specific boolean value. If the expression cannot evaluate to a 
 @{term Boolean} value UNIV is returned. If we expect true/false the opposite 
 constant false/true will also lead to UNIV. *}
-consts assigns_if:: "bool \<Rightarrow> expr \<Rightarrow> lname set" 
-primrec
-"assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
-"assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (Cast t e)          = assigns_if b e" 
-"assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
-                                                     e is a reference type*}
-"assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
-"assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
-                                         None   \<Rightarrow> (if unop = UNot 
-                                                       then assigns_if (\<not>b) e
-                                                       else UNIV)
-                                       | Some v \<Rightarrow> (if v=Bool b 
-                                                       then {} 
-                                                       else UNIV))"
-"assigns_if b (BinOp binop e1 e2) 
-  = (case constVal (BinOp binop e1 e2) of
-       None \<Rightarrow> (if binop=CondAnd then
-                   (case b of 
-                       True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
-                    |  False \<Rightarrow> assigns_if False e1 \<inter> 
-                                (assigns_if True e1 \<union> assigns_if False e2))
-                else
-               (if binop=CondOr then
-                   (case b of 
-                       True  \<Rightarrow> assigns_if True e1 \<inter> 
-                                (assigns_if False e1 \<union> assigns_if True e2)
-                    |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
-                else assignsE e1 \<union> assignsE e2))
-     | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
+primrec assigns_if :: "bool \<Rightarrow> expr \<Rightarrow> lname set"
+where
+  "assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
+| "assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Cast t e)          = assigns_if b e" 
+| "assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
+                                                       e is a reference type*}
+| "assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
+| "assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
+                                           None   \<Rightarrow> (if unop = UNot 
+                                                         then assigns_if (\<not>b) e
+                                                         else UNIV)
+                                         | Some v \<Rightarrow> (if v=Bool b 
+                                                         then {} 
+                                                         else UNIV))"
+| "assigns_if b (BinOp binop e1 e2) 
+    = (case constVal (BinOp binop e1 e2) of
+         None \<Rightarrow> (if binop=CondAnd then
+                     (case b of 
+                         True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
+                      |  False \<Rightarrow> assigns_if False e1 \<inter> 
+                                  (assigns_if True e1 \<union> assigns_if False e2))
+                  else
+                 (if binop=CondOr then
+                     (case b of 
+                         True  \<Rightarrow> assigns_if True e1 \<inter> 
+                                  (assigns_if False e1 \<union> assigns_if True e2)
+                      |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
+                  else assignsE e1 \<union> assignsE e2))
+       | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
 
-"assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (Acc v)      = (assignsV v)"
-"assigns_if b (v := e)     = (assignsE (Ass v e))"
-"assigns_if b (c? e1 : e2) = (assignsE c) \<union>
-                               (case (constVal c) of
-                                  None    \<Rightarrow> (assigns_if b e1) \<inter> 
-                                             (assigns_if b e2)
-                                | Some bv \<Rightarrow> (case the_Bool bv of
-                                                True  \<Rightarrow> assigns_if b e1
-                                              | False \<Rightarrow> assigns_if b e2))"
-"assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
-          = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
+| "assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Acc v)      = (assignsV v)"
+| "assigns_if b (v := e)     = (assignsE (Ass v e))"
+| "assigns_if b (c? e1 : e2) = (assignsE c) \<union>
+                                 (case (constVal c) of
+                                    None    \<Rightarrow> (assigns_if b e1) \<inter> 
+                                               (assigns_if b e2)
+                                  | Some bv \<Rightarrow> (case the_Bool bv of
+                                                  True  \<Rightarrow> assigns_if b e1
+                                                | False \<Rightarrow> assigns_if b e2))"
+| "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
+            = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
 -- {* Only dummy analysis for intermediate expressions  
       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
-"assigns_if b (Methd C sig)   = {}" 
-"assigns_if b (Body  C s)     = {}"   
-"assigns_if b (InsInitE s e)  = {}"  
-"assigns_if b (Callee l e)    = {}" 
+| "assigns_if b (Methd C sig)   = {}" 
+| "assigns_if b (Body  C s)     = {}"   
+| "assigns_if b (InsInitE s e)  = {}"  
+| "assigns_if b (Callee l e)    = {}" 
 
 lemma assigns_if_const_b_simp:
   assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
@@ -429,14 +427,17 @@
 
 subsection {* Lifting set operations to range of tables (map to a set) *}
 
-definition union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65) where
- "A \<Rightarrow>\<union> B \<equiv> \<lambda> k. A k \<union> B k"
+definition
+  union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65)
+  where "A \<Rightarrow>\<union> B = (\<lambda> k. A k \<union> B k)"
 
-definition intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71) where
- "A \<Rightarrow>\<inter>  B \<equiv> \<lambda> k. A k \<inter> B k"
+definition
+  intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71)
+  where "A \<Rightarrow>\<inter>  B = (\<lambda>k. A k \<inter> B k)"
 
-definition all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40) where 
- "A \<Rightarrow>\<union>\<^sub>\<forall> B \<equiv> \<lambda> k. A k \<union> B"
+definition
+  all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)
+  where "(A \<Rightarrow>\<union>\<^sub>\<forall> B) = (\<lambda> k. A k \<union> B)"
   
 subsubsection {* Binary union of tables *}
 
@@ -507,16 +508,19 @@
          brk :: "breakass" --{* Definetly assigned variables for 
                                 abrupt completion with a break *}
 
-definition rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" where
-"rmlab k A \<equiv> \<lambda> x. if x=k then UNIV else A x"
+definition
+  rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
+  where "rmlab k A = (\<lambda>x. if x=k then UNIV else A x)"
  
 (*
-definition setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
-"setbrk b A \<equiv> {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
+definition
+  setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
+  "setbrk b A = {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
 *)
 
-definition range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80) where 
- "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}"
+definition
+  range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
+  where "\<Rightarrow>\<Inter>A = {x |x. \<forall> k. x \<in> A k}"
 
 text {*
 In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"},
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Eval.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -141,7 +141,7 @@
   where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
 
 definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
- "undefined3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
+ "undefined3 = sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
                      (\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
 
 lemma [simp]: "undefined3 (In1l x) = In1 undefined"
@@ -159,8 +159,9 @@
 
 section "exception throwing and catching"
 
-definition throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
- "throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
+definition
+  throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
+  "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
 
 lemma throw_def2: 
  "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
@@ -168,8 +169,9 @@
 apply (simp (no_asm))
 done
 
-definition fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60) where
- "G,s\<turnstile>a' fits T  \<equiv> (\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T"
+definition
+  fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
+  where "G,s\<turnstile>a' fits T = ((\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T)"
 
 lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
 by (simp add: fits_def)
@@ -192,9 +194,10 @@
 apply iprover
 done
 
-definition catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
- "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
-                    G,store s\<turnstile>Addr (the_Loc xc) fits Class C"
+definition
+  catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
+  "G,s\<turnstile>catch C = (\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
+                        G,store s\<turnstile>Addr (the_Loc xc) fits Class C)"
 
 lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
 apply (unfold catch_def)
@@ -217,9 +220,9 @@
 apply (simp (no_asm))
 done
 
-definition new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
- "new_xcpt_var vn \<equiv> 
-     \<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
+definition
+  new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
+  "new_xcpt_var vn = (\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s))"
 
 lemma new_xcpt_var_def2 [simp]: 
  "new_xcpt_var vn (x,s) = 
@@ -232,9 +235,10 @@
 
 section "misc"
 
-definition assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
- "assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
-                   in  (x',if x' = None then s' else s)"
+definition
+  assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
+ "assign f v = (\<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
+                        in  (x',if x' = None then s' else s))"
 
 (*
 lemma assign_Norm_Norm [simp]: 
@@ -293,26 +297,29 @@
 done
 *)
 
-definition init_comp_ty :: "ty \<Rightarrow> stmt" where
- "init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip"
+definition
+  init_comp_ty :: "ty \<Rightarrow> stmt"
+  where "init_comp_ty T = (if (\<exists>C. T = Class C) then Init (the_Class T) else Skip)"
 
 lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
 apply (unfold init_comp_ty_def)
 apply (simp (no_asm))
 done
 
-definition invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
- "invocation_class m s a' statT 
-    \<equiv> (case m of
-         Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
-                      then the_Class (RefT statT) 
-                      else Object
-       | SuperM \<Rightarrow> the_Class (RefT statT)
-       | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
+definition
+  invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
+ "invocation_class m s a' statT =
+    (case m of
+       Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
+                    then the_Class (RefT statT) 
+                    else Object
+     | SuperM \<Rightarrow> the_Class (RefT statT)
+     | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
 
-definition invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
-"invocation_declclass G m s a' statT sig 
-   \<equiv> declclass (the (dynlookup G statT 
+definition
+  invocation_declclass :: "prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
+  "invocation_declclass G m s a' statT sig =
+    declclass (the (dynlookup G statT
                                 (invocation_class m s a' statT)
                                 sig))" 
   
@@ -330,10 +337,11 @@
                                             else Object)"
 by (simp add: invocation_class_def)
 
-definition init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
-                   state \<Rightarrow> state" where
- "init_lvars G C sig mode a' pvs 
-   \<equiv> \<lambda> (x,s). 
+definition
+  init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> state \<Rightarrow> state"
+where
+  "init_lvars G C sig mode a' pvs =
+    (\<lambda>(x,s). 
       let m = mthd (the (methd G C sig));
           l = \<lambda> k. 
               (case k of
@@ -343,7 +351,7 @@
                        | Res    \<Rightarrow> None)
                | This 
                    \<Rightarrow> (if mode=Static then None else Some a'))
-      in set_lvars l (if mode = Static then x else np a' x,s)"
+      in set_lvars l (if mode = Static then x else np a' x,s))"
 
 
 
@@ -364,9 +372,11 @@
 apply (simp (no_asm) add: Let_def)
 done
 
-definition body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
- "body G C sig \<equiv> let m = the (methd G C sig) 
-                 in Body (declclass m) (stmt (mbody (mthd m)))"
+definition
+  body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
+ "body G C sig =
+    (let m = the (methd G C sig) 
+     in Body (declclass m) (stmt (mbody (mthd m))))"
 
 lemma body_def2: --{* better suited for simplification *} 
 "body G C sig = Body  (declclass (the (methd G C sig))) 
@@ -377,28 +387,30 @@
 
 section "variables"
 
-definition lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar" where
- "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
+definition
+  lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
+  where "lvar vn s = (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
 
-definition fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
- "fvar C stat fn a' s 
-    \<equiv> let (oref,xf) = if stat then (Stat C,id)
-                              else (Heap (the_Addr a'),np a');
+definition
+  fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
+ "fvar C stat fn a' s =
+   (let (oref,xf) = if stat then (Stat C,id)
+                            else (Heap (the_Addr a'),np a');
                   n = Inl (fn,C); 
                   f = (\<lambda>v. supd (upd_gobj oref n v)) 
-      in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
+    in ((the (values (the (globs (store s) oref)) n),f),abupd xf s))"
 
-definition avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
- "avar G i' a' s 
-    \<equiv> let   oref = Heap (the_Addr a'); 
-               i = the_Intg i'; 
-               n = Inr i;
-        (T,k,cs) = the_Arr (globs (store s) oref); 
-               f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
+definition
+  avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
+  "avar G i' a' s =
+    (let   oref = Heap (the_Addr a'); 
+              i = the_Intg i'; 
+              n = Inr i;
+       (T,k,cs) = the_Arr (globs (store s) oref); 
+              f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
                                            ArrStore x
                               ,upd_gobj oref n v s)) 
-      in ((the (cs n),f)
-         ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
+     in ((the (cs n),f),abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s))"
 
 lemma fvar_def2: --{* better suited for simplification *} 
 "fvar C stat fn a' s =  
@@ -431,27 +443,29 @@
 apply (simp (no_asm) add: Let_def split_beta)
 done
 
-definition check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
-"check_field_access G accC statDeclC fn stat a' s
- \<equiv> let oref = if stat then Stat statDeclC
-                      else Heap (the_Addr a');
-       dynC = case oref of
+definition
+  check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
+  "check_field_access G accC statDeclC fn stat a' s =
+    (let oref = if stat then Stat statDeclC
+                else Heap (the_Addr a');
+         dynC = case oref of
                    Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
                  | Stat C \<Rightarrow> C;
-       f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
-   in abupd 
+         f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
+     in abupd 
         (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
                   AccessViolation)
-        s"
+        s)"
 
-definition check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
-"check_method_access G accC statT mode sig  a' s
- \<equiv> let invC = invocation_class mode (store s) a' statT;
+definition
+  check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
+  "check_method_access G accC statT mode sig  a' s =
+    (let invC = invocation_class mode (store s) a' statT;
        dynM = the (dynlookup G statT invC sig)
-   in abupd 
+     in abupd 
         (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
                   AccessViolation)
-        s"
+        s)"
        
 section "evaluation judgments"
 
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Example.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -70,22 +70,21 @@
 datatype vnam'  = arr' | vee' | z' | e'
 datatype label' = lab1'
 
-consts
-
-  tnam' :: "tnam'  \<Rightarrow> tnam"
-  vnam' :: "vnam'  \<Rightarrow> vname"
+axiomatization
+  tnam' :: "tnam'  \<Rightarrow> tnam" and
+  vnam' :: "vnam'  \<Rightarrow> vname" and
   label':: "label' \<Rightarrow> label"
-axioms  (** tnam', vnam' and label are intended to be isomorphic 
+where
+  (** tnam', vnam' and label are intended to be isomorphic 
             to tnam, vname and label **)
 
-  inj_tnam'  [simp]: "(tnam'  x = tnam'  y) = (x = y)"
-  inj_vnam'  [simp]: "(vnam'  x = vnam'  y) = (x = y)"
-  inj_label' [simp]: "(label' x = label' y) = (x = y)"
-  
-  
-  surj_tnam':  "\<exists>m. n = tnam'  m"
-  surj_vnam':  "\<exists>m. n = vnam'  m"
-  surj_label':" \<exists>m. n = label' m"
+  inj_tnam'  [simp]: "\<And>x y. (tnam'  x = tnam'  y) = (x = y)" and
+  inj_vnam'  [simp]: "\<And>x y. (vnam'  x = vnam'  y) = (x = y)" and
+  inj_label' [simp]: "\<And>x y. (label' x = label' y) = (x = y)" and
+    
+  surj_tnam':  "\<And>n. \<exists>m. n = tnam'  m" and
+  surj_vnam':  "\<And>n. \<exists>m. n = vnam'  m" and
+  surj_label':" \<And>n. \<exists>m. n = label' m"
 
 abbreviation
   HasFoo :: qtname where
@@ -149,22 +148,24 @@
   Object_mdecls_def: "Object_mdecls \<equiv> []"
   SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
 
-consts
-  
+axiomatization  
   foo    :: mname
 
-definition foo_sig :: sig
- where "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
+definition
+  foo_sig :: sig
+  where "foo_sig = \<lparr>name=foo,parTs=[Class Base]\<rparr>"
   
-definition foo_mhead :: mhead
- where "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
+definition
+  foo_mhead :: mhead
+  where "foo_mhead = \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
 
-definition Base_foo :: mdecl
- where "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
+definition
+  Base_foo :: mdecl
+  where "Base_foo = (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
                         mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
 
 definition Ext_foo :: mdecl
- where "Ext_foo  \<equiv> (foo_sig, 
+  where "Ext_foo = (foo_sig, 
               \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
                mbody=\<lparr>lcls=[]
                      ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
@@ -172,11 +173,13 @@
                                 Return (Lit Null)\<rparr>
               \<rparr>)"
 
-definition arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var" where
-"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
+definition
+  arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
+  where "arr_viewed_from accC C = {accC,Base,True}StatRef (ClassT C)..arr"
 
-definition BaseCl :: "class" where
-"BaseCl \<equiv> \<lparr>access=Public,
+definition
+  BaseCl :: "class" where
+  "BaseCl = \<lparr>access=Public,
            cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
                     (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
            methods=[Base_foo],
@@ -185,16 +188,18 @@
            super=Object,
            superIfs=[HasFoo]\<rparr>"
   
-definition ExtCl  :: "class" where
-"ExtCl  \<equiv> \<lparr>access=Public,
+definition
+  ExtCl  :: "class" where
+  "ExtCl = \<lparr>access=Public,
            cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
            methods=[Ext_foo],
            init=Skip,
            super=Base,
            superIfs=[]\<rparr>"
 
-definition MainCl :: "class" where
-"MainCl \<equiv> \<lparr>access=Public,
+definition
+  MainCl :: "class" where
+  "MainCl = \<lparr>access=Public,
            cfields=[], 
            methods=[], 
            init=Skip,
@@ -202,14 +207,17 @@
            superIfs=[]\<rparr>"
 (* The "main" method is modeled seperately (see tprg) *)
 
-definition HasFooInt :: iface
- where "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
+definition
+  HasFooInt :: iface
+  where "HasFooInt = \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
 
-definition Ifaces ::"idecl list"
- where "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
+definition
+  Ifaces ::"idecl list"
+  where "Ifaces = [(HasFoo,HasFooInt)]"
 
-definition "Classes" ::"cdecl list"
- where "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
+definition
+  "Classes" ::"cdecl list"
+  where "Classes = [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
 
 lemmas table_classes_defs = 
      Classes_def standard_classes_def ObjectC_def SXcptC_def
@@ -264,12 +272,13 @@
   tprg :: prog where
   "tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
 
-definition test :: "(ty)list \<Rightarrow> stmt" where
- "test pTs \<equiv> e:==NewC Ext;; 
+definition
+  test :: "(ty)list \<Rightarrow> stmt" where
+  "test pTs = (e:==NewC Ext;; 
            \<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
            \<spacespace> Catch((SXcpt NullPointer) z)
            (lab1\<bullet> While(Acc 
-                        (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)"
+                        (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip))"
 
 
 section "well-structuredness"
@@ -1185,9 +1194,9 @@
          rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
 
-consts
-  a :: loc
-  b :: loc
+axiomatization
+  a :: loc and
+  b :: loc and
   c :: loc
 
 abbreviation "one == Suc 0"
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Name.thy
--- a/src/HOL/Bali/Name.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Name.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -68,14 +68,14 @@
 begin
 
 definition
-  tname_tname_def: "tname (t::tname) \<equiv> t"
+  tname_tname_def: "tname (t::tname) = t"
 
 instance ..
 
 end
 
 definition
-  qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
+  qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
 
 translations
   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
@@ -84,16 +84,17 @@
 
 axiomatization java_lang::pname --{* package java.lang *}
 
-consts 
+definition
   Object :: qtname
-  SXcpt  :: "xname \<Rightarrow> qtname"
-defs
-  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
-  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
+  where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>"
+
+definition SXcpt :: "xname \<Rightarrow> qtname"
+  where "SXcpt = (\<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)"
 
 lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
 by (simp add: Object_def SXcpt_def)
 
 lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
 by (simp add: SXcpt_def)
+
 end
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/State.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -38,8 +38,9 @@
   (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
   (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
 
-definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
- "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
+definition
+  the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table"
+  where "the_Arr obj = (SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>)"
 
 lemma the_Arr_Arr [simp]: "the_Arr (Some \<lparr>tag=Arr T k,values=cs\<rparr>) = (T,k,cs)"
 apply (auto simp: the_Arr_def)
@@ -50,18 +51,20 @@
 apply (auto simp add: the_Arr_def)
 done
 
-definition upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj" where 
- "upd_obj n v \<equiv> \<lambda> obj . obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>"
+definition
+  upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj"
+  where "upd_obj n v = (\<lambda>obj. obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>)"
 
 lemma upd_obj_def2 [simp]: 
   "upd_obj n v obj = obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>" 
 apply (auto simp: upd_obj_def)
 done
 
-definition obj_ty :: "obj \<Rightarrow> ty" where
- "obj_ty obj    \<equiv> case tag obj of 
-                    CInst C \<Rightarrow> Class C 
-                  | Arr T k \<Rightarrow> T.[]"
+definition
+  obj_ty :: "obj \<Rightarrow> ty" where
+  "obj_ty obj = (case tag obj of 
+                  CInst C \<Rightarrow> Class C 
+                | Arr T k \<Rightarrow> T.[])"
 
 lemma obj_ty_eq [intro!]: "obj_ty \<lparr>tag=oi,values=x\<rparr> = obj_ty \<lparr>tag=oi,values=y\<rparr>" 
 by (simp add: obj_ty_def)
@@ -97,10 +100,11 @@
 apply (auto split add: obj_tag.split_asm)
 done
 
-definition obj_class :: "obj \<Rightarrow> qtname" where
- "obj_class obj \<equiv> case tag obj of 
-                    CInst C \<Rightarrow> C 
-                  | Arr T k \<Rightarrow> Object"
+definition
+  obj_class :: "obj \<Rightarrow> qtname" where
+  "obj_class obj = (case tag obj of 
+                     CInst C \<Rightarrow> C 
+                   | Arr T k \<Rightarrow> Object)"
 
 
 lemma obj_class_CInst [simp]: "obj_class \<lparr>tag=CInst C,values=vs\<rparr> = C" 
@@ -136,9 +140,10 @@
   "Stat" => "CONST Inr"
   (type) "oref" <= (type) "loc + qtname"
 
-definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
- "fields_table G C P 
-    \<equiv> Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
+definition
+  fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
+  "fields_table G C P =
+    Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
 
 lemma fields_table_SomeI: 
 "\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 
@@ -173,20 +178,23 @@
 apply simp
 done
 
-definition in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50) where
- "i in_bounds k \<equiv> 0 \<le> i \<and> i < k"
+definition
+  in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50)
+  where "i in_bounds k = (0 \<le> i \<and> i < k)"
 
-definition arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option" where
- "arr_comps T k \<equiv> \<lambda>i. if i in_bounds k then Some T else None"
+definition
+  arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option"
+  where "arr_comps T k = (\<lambda>i. if i in_bounds k then Some T else None)"
   
-definition var_tys       :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where
-"var_tys G oi r 
-  \<equiv> case r of 
+definition
+  var_tys :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where
+  "var_tys G oi r =
+    (case r of 
       Heap a \<Rightarrow> (case oi of 
                    CInst C \<Rightarrow> fields_table G C (\<lambda>n f. \<not>static f) (+) empty
                  | Arr T k \<Rightarrow> empty (+) arr_comps T k)
     | Stat C \<Rightarrow> fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) 
-                (+) empty"
+                (+) empty)"
 
 lemma var_tys_Some_eq: 
  "var_tys G oi r n = Some T 
@@ -222,14 +230,16 @@
 
 subsection "access"
 
-definition globs :: "st \<Rightarrow> globs" where
- "globs  \<equiv> st_case (\<lambda>g l. g)"
+definition
+  globs :: "st \<Rightarrow> globs"
+  where "globs = st_case (\<lambda>g l. g)"
   
-definition locals :: "st \<Rightarrow> locals" where
- "locals \<equiv> st_case (\<lambda>g l. l)"
+definition
+  locals :: "st \<Rightarrow> locals"
+  where "locals = st_case (\<lambda>g l. l)"
 
-definition heap   :: "st \<Rightarrow> heap" where
- "heap s \<equiv> globs s \<circ> Heap"
+definition heap :: "st \<Rightarrow> heap" where
+ "heap s = globs s \<circ> Heap"
 
 
 lemma globs_def2 [simp]: " globs (st g l) = g"
@@ -250,8 +260,9 @@
 
 subsection "memory allocation"
 
-definition new_Addr :: "heap \<Rightarrow> loc option" where
- "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)"
+definition
+  new_Addr :: "heap \<Rightarrow> loc option" where
+  "new_Addr h = (if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None))"
 
 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
 apply (auto simp add: new_Addr_def)
@@ -290,20 +301,25 @@
 
 subsection "update"
 
-definition gupd :: "oref  \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')"[10,10]1000) where
- "gupd r obj  \<equiv> st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
+definition
+  gupd :: "oref  \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')" [10, 10] 1000)
+  where "gupd r obj = st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
 
-definition lupd       :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')"[10,10]1000) where
- "lupd vn v   \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
+definition
+  lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')" [10, 10] 1000)
+  where "lupd vn v = st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
 
-definition upd_gobj   :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" where
- "upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
+definition
+  upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
+  where "upd_gobj r n v = st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
 
-definition set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st" where
- "set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
+definition
+  set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st"
+  where "set_locals l = st_case (\<lambda>g l'. st g l)"
 
-definition init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st" where
- "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
+definition
+  init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
+  where "init_obj G oi r = gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
 
 abbreviation
   init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
@@ -447,23 +463,22 @@
 
 
 
-consts
+primrec the_Xcpt :: "abrupt \<Rightarrow> xcpt"
+  where "the_Xcpt (Xcpt x) = x"
 
-  the_Xcpt :: "abrupt \<Rightarrow> xcpt"
-  the_Jump :: "abrupt => jump"
-  the_Loc  :: "xcpt \<Rightarrow> loc"
-  the_Std  :: "xcpt \<Rightarrow> xname"
+primrec the_Jump :: "abrupt => jump"
+  where "the_Jump (Jump j) = j"
 
-primrec "the_Xcpt (Xcpt x) = x"
-primrec "the_Jump (Jump j) = j"
-primrec "the_Loc (Loc a) = a"
-primrec "the_Std (Std x) = x"
+primrec the_Loc :: "xcpt \<Rightarrow> loc"
+  where "the_Loc (Loc a) = a"
 
-
+primrec the_Std :: "xcpt \<Rightarrow> xname"
+  where "the_Std (Std x) = x"
         
 
-definition abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt" where
- "abrupt_if c x' x \<equiv> if c \<and> (x = None) then x' else x"
+definition
+  abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt"
+  where "abrupt_if c x' x = (if c \<and> (x = None) then x' else x)"
 
 lemma abrupt_if_True_None [simp]: "abrupt_if True x None = x"
 by (simp add: abrupt_if_def)
@@ -542,8 +557,9 @@
 apply auto
 done
 
-definition absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt" where
-  "absorb j a \<equiv> if a=Some (Jump j) then None else a"
+definition
+  absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt"
+  where "absorb j a = (if a=Some (Jump j) then None else a)"
 
 lemma absorb_SomeD [dest!]: "absorb j a = Some x \<Longrightarrow> a = Some x"
 by (auto simp add: absorb_def)
@@ -593,16 +609,18 @@
 apply clarsimp
 done
 
-definition normal :: "state \<Rightarrow> bool" where
- "normal \<equiv> \<lambda>s. abrupt s = None"
+definition
+  normal :: "state \<Rightarrow> bool"
+  where "normal = (\<lambda>s. abrupt s = None)"
 
 lemma normal_def2 [simp]: "normal s = (abrupt s = None)"
 apply (unfold normal_def)
 apply (simp (no_asm))
 done
 
-definition heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool" where
- "heap_free n \<equiv> \<lambda>s. atleast_free (heap (store s)) n"
+definition
+  heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool"
+  where "heap_free n = (\<lambda>s. atleast_free (heap (store s)) n)"
 
 lemma heap_free_def2 [simp]: "heap_free n s = atleast_free (heap (store s)) n"
 apply (unfold heap_free_def)
@@ -611,11 +629,13 @@
 
 subsection "update"
 
-definition abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state" where
- "abupd f \<equiv> prod_fun f id"
+definition
+  abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
+  where "abupd f = prod_fun f id"
 
-definition supd     :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state" where
- "supd \<equiv> prod_fun id"
+definition
+  supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
+  where "supd = prod_fun id"
   
 lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
 by (simp add: abupd_def)
@@ -669,11 +689,13 @@
 
 section "initialisation test"
 
-definition inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool" where
- "inited C g \<equiv> g (Stat C) \<noteq> None"
+definition
+  inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool"
+  where "inited C g = (g (Stat C) \<noteq> None)"
 
-definition initd    :: "qtname \<Rightarrow> state \<Rightarrow> bool" where
- "initd C \<equiv> inited C \<circ> globs \<circ> store"
+definition
+  initd :: "qtname \<Rightarrow> state \<Rightarrow> bool"
+  where "initd C = inited C \<circ> globs \<circ> store"
 
 lemma not_inited_empty [simp]: "\<not>inited C empty"
 apply (unfold inited_def)
@@ -706,8 +728,10 @@
 done
 
 section {* @{text error_free} *}
-definition error_free :: "state \<Rightarrow> bool" where
-"error_free s \<equiv> \<not> (\<exists> err. abrupt s = Some (Error err))"
+
+definition
+  error_free :: "state \<Rightarrow> bool"
+  where "error_free s = (\<not> (\<exists> err. abrupt s = Some (Error err)))"
 
 lemma error_free_Norm [simp,intro]: "error_free (Norm s)"
 by (simp add: error_free_def)
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Table.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -54,15 +54,15 @@
 
 --{* when merging tables old and new, only override an entry of table old when  
    the condition cond holds *}
-"cond_override cond old new \<equiv>
- \<lambda> k.
+"cond_override cond old new =
+ (\<lambda>k.
   (case new k of
      None         \<Rightarrow> old k                       
    | Some new_val \<Rightarrow> (case old k of
                         None         \<Rightarrow> Some new_val          
                       | Some old_val \<Rightarrow> (if cond new_val old_val
                                          then Some new_val     
-                                         else Some old_val)))"
+                                         else Some old_val))))"
 
 lemma cond_override_empty1[simp]: "cond_override c empty t = t"
 by (simp add: cond_override_def expand_fun_eq)
@@ -95,10 +95,11 @@
 
 section {* Filter on Tables *}
 
-definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
-"filter_tab c t \<equiv> \<lambda> k. (case t k of 
+definition
+  filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
+  "filter_tab c t = (\<lambda>k. (case t k of 
                            None   \<Rightarrow> None
-                         | Some x \<Rightarrow> if c k x then Some x else None)"
+                         | Some x \<Rightarrow> if c k x then Some x else None))"
 
 lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
 by (simp add: filter_tab_def empty_def)
@@ -279,27 +280,31 @@
 done
 
 
-consts
-  Un_tables      :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
-  overrides_t    :: "('a, 'b) tables     \<Rightarrow> ('a, 'b) tables \<Rightarrow>
-                     ('a, 'b) tables"             (infixl "\<oplus>\<oplus>" 100)
-  hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> 
-                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hidings _ entails _" 20)
+definition
+  Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
+  where "Un_tables ts\<spacespace>\<spacespace>= (\<lambda>k. \<Union>t\<in>ts. t k)"
+
+definition
+  overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables"  (infixl "\<oplus>\<oplus>" 100)
+  where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)"
+
+definition
+  hidings_entails :: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
+    ("_ hidings _ entails _" 20)
+  where "(t hidings s entails R) = (\<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y)"
+
+definition
   --{* variant for unique table: *}
-  hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> 
-                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hiding _ entails _"  20)
+  hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
+    ("_ hiding _ entails _"  20)
+  where "(t hiding  s entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y)"
+
+definition
   --{* variant for a unique table and conditional overriding: *}
   cond_hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  
                           \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"  
                           ("_ hiding _ under _ entails _"  20)
-
-defs
-  Un_tables_def:       "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k"
-  overrides_t_def:     "s \<oplus>\<oplus> t        \<equiv> \<lambda>k. if t k = {} then s k else t k"
-  hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y"
-  hiding_entails_def:  "t hiding  s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y"
-  cond_hiding_entails_def: "t hiding  s under C entails R
-                            \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y"
+  where "(t hiding  s under C entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y)"
 
 section "Untables"
 
@@ -383,12 +388,10 @@
 
 
 (*###TO Map?*)
-consts
-  atleast_free :: "('a ~=> 'b) => nat => bool"
-primrec
- "atleast_free m 0       = True"
- atleast_free_Suc: 
- "atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
+primrec atleast_free :: "('a ~=> 'b) => nat => bool"
+where
+  "atleast_free m 0 = True"
+| atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a|->b)) n))"
 
 lemma atleast_free_weaken [rule_format (no_asm)]: 
   "!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Term.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -258,8 +258,9 @@
   StatRef :: "ref_ty \<Rightarrow> expr"
   where "StatRef rt == Cast (RefT rt) (Lit Null)"
   
-definition is_stmt :: "term \<Rightarrow> bool" where
- "is_stmt t \<equiv> \<exists>c. t=In1r c"
+definition
+  is_stmt :: "term \<Rightarrow> bool"
+  where "is_stmt t = (\<exists>c. t=In1r c)"
 
 ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
 
@@ -307,7 +308,7 @@
 begin
 
 definition
-  stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+  stmt_inj_term_def: "\<langle>c::stmt\<rangle> = In1r c"
 
 instance ..
 
@@ -323,7 +324,7 @@
 begin
 
 definition
-  expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+  expr_inj_term_def: "\<langle>e::expr\<rangle> = In1l e"
 
 instance ..
 
@@ -339,7 +340,7 @@
 begin
 
 definition
-  var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+  var_inj_term_def: "\<langle>v::var\<rangle> = In2 v"
 
 instance ..
 
@@ -368,7 +369,7 @@
 begin
 
 definition
-  "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
+  "\<langle>es::'a list\<rangle> = In3 (map expr_of es)"
 
 instance ..
 
@@ -425,46 +426,47 @@
   done
 
 section {* Evaluation of unary operations *}
-consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
-primrec
-"eval_unop UPlus   v = Intg (the_Intg v)"
-"eval_unop UMinus  v = Intg (- (the_Intg v))"
-"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
-"eval_unop UNot    v = Bool (\<not> the_Bool v)"
+primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
+where
+  "eval_unop UPlus v = Intg (the_Intg v)"
+| "eval_unop UMinus v = Intg (- (the_Intg v))"
+| "eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
+| "eval_unop UNot v = Bool (\<not> the_Bool v)"
 
 section {* Evaluation of binary operations *}
-consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
-primrec
-"eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
-"eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
-"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
-"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
-"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
+primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
+where
+  "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
+| "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
+| "eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
+| "eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
+| "eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
 
 -- "Be aware of the explicit coercion of the shift distance to nat"
-"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
-"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
-"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
+| "eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
+| "eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
+| "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
 
-"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
-"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
-"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
-"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
+| "eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
+| "eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
+| "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
+| "eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
 
-"eval_binop Eq      v1 v2 = Bool (v1=v2)"
-"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
-"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
-"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
-"eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
-"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
-"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+| "eval_binop Eq      v1 v2 = Bool (v1=v2)"
+| "eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
+| "eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+| "eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
+| "eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+| "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+| "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
 
-definition need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
-"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
-                               (binop=CondOr  \<and> the_Bool v1))"
+definition
+  need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
+  "need_second_arg binop v1 = (\<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
+                                 (binop=CondOr  \<and> the_Bool v1)))"
 text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
  if the value isn't already determined by the first argument*}
 
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Trans.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -9,12 +9,13 @@
 
 theory Trans imports Evaln begin
 
-definition groundVar :: "var \<Rightarrow> bool" where
-"groundVar v \<longleftrightarrow> (case v of
-                   LVar ln \<Rightarrow> True
-                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
-                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
-                 | InsInitV c v \<Rightarrow> False)"
+definition
+  groundVar :: "var \<Rightarrow> bool" where
+  "groundVar v \<longleftrightarrow> (case v of
+                     LVar ln \<Rightarrow> True
+                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
+                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
+                   | InsInitV c v \<Rightarrow> False)"
 
 lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
   assumes ground: "groundVar v" and
@@ -34,14 +35,15 @@
     done
 qed
 
-definition groundExprs :: "expr list \<Rightarrow> bool" where
-  "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
+definition
+  groundExprs :: "expr list \<Rightarrow> bool"
+  where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
   
-primrec the_val:: "expr \<Rightarrow> val" where
-  "the_val (Lit v) = v"
+primrec the_val:: "expr \<Rightarrow> val"
+  where "the_val (Lit v) = v"
 
 primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
-  "the_var G s (LVar ln)                    =(lvar ln (store s),s)"
+  "the_var G s (LVar ln) = (lvar ln (store s),s)"
 | the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
 | the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
 
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Type.thy
--- a/src/HOL/Bali/Type.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Type.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -36,8 +36,9 @@
 abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
   where "T.[] == RefT (ArrayT T)"
 
-definition the_Class :: "ty \<Rightarrow> qtname" where
- "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
+definition
+  the_Class :: "ty \<Rightarrow> qtname"
+  where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
  
 lemma the_Class_eq [simp]: "the_Class (Class C)= C"
 by (auto simp add: the_Class_def)
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -25,14 +25,17 @@
 \end{itemize}
 *}
 
-consts
-
 (*subint1, in Decl.thy*)                     (* direct subinterface       *)
 (*subint , by translation*)                  (* subinterface (+ identity) *)
 (*subcls1, in Decl.thy*)                     (* direct subclass           *)
 (*subcls , by translation*)                  (*        subclass           *)
 (*subclseq, by translation*)                 (* subclass + identity       *)
-  implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
+
+definition
+  implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
+  --{* direct implementation, cf. 8.1.3 *}
+  where "implmt1 G = {(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
+
 
 abbreviation
   subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
@@ -325,16 +328,11 @@
 
 section "implementation relation"
 
-defs
-  --{* direct implementation, cf. 8.1.3 *}
-implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
-
 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
 apply (unfold implmt1_def)
 apply auto
 done
 
-
 inductive --{* implementation, cf. 8.1.4 *}
   implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
   for G :: prog
@@ -568,8 +566,9 @@
 apply (fast dest: widen_Class_Class widen_Class_Iface)
 done
 
-definition widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) where
- "G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
+definition
+  widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
+  where "G\<turnstile>Ts[\<preceq>]Ts' = list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
 
 lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
 apply (unfold widens_def)
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -93,23 +93,27 @@
 
 section "result conformance"
 
-definition assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70) where
-"s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
- (\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
- (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
+definition
+  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
+where
+  "s\<le>|f\<preceq>T\<Colon>\<preceq>E =
+   ((\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
+    (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s'))))"
 
 
-definition rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool" ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70) where
-  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
-    \<equiv> case T of
-        Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
-                  then (\<forall> n. (the_In2 t) = LVar n 
-                         \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
-                             (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
-                      (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
-                      (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
-                  else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
-      | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
+definition
+  rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool" ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70)
+where
+  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T =
+    (case T of
+      Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
+                then (\<forall> n. (the_In2 t) = LVar n 
+                       \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
+                           (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
+                    (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
+                    (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
+                else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
+    | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts)"
 
 text {*
  With @{term rconf} we describe the conformance of the result value of a term.
@@ -324,9 +328,11 @@
 
 declare fun_upd_apply [simp del]
 
-definition DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70) where
-  "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
-                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
+definition
+  DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
+where
+  "G\<turnstile>mode\<rightarrow>D\<preceq>t = (mode = IntVir \<longrightarrow> is_class G D \<and> 
+                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t))"
 
 lemma DynT_propI: 
  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> 
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/Value.thy
--- a/src/HOL/Bali/Value.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/Value.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -17,29 +17,34 @@
         | Addr loc      --{* addresses, i.e. locations of objects *}
 
 
-consts   the_Bool   :: "val \<Rightarrow> bool"  
-primrec "the_Bool (Bool b) = b"
-consts   the_Intg   :: "val \<Rightarrow> int"
-primrec "the_Intg (Intg i) = i"
-consts   the_Addr   :: "val \<Rightarrow> loc"
-primrec "the_Addr (Addr a) = a"
+primrec the_Bool :: "val \<Rightarrow> bool"
+  where "the_Bool (Bool b) = b"
+
+primrec the_Intg :: "val \<Rightarrow> int"
+  where "the_Intg (Intg i) = i"
+
+primrec the_Addr :: "val \<Rightarrow> loc"
+  where "the_Addr (Addr a) = a"
 
 types   dyn_ty      = "loc \<Rightarrow> ty option"
-consts
-  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
-  defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
-  default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}
+
+primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
+where
+  "typeof dt  Unit = Some (PrimT Void)"
+| "typeof dt (Bool b) = Some (PrimT Boolean)"
+| "typeof dt (Intg i) = Some (PrimT Integer)"
+| "typeof dt  Null = Some NT"
+| "typeof dt (Addr a) = dt a"
 
-primrec "typeof dt  Unit    = Some (PrimT Void)"
-        "typeof dt (Bool b) = Some (PrimT Boolean)"
-        "typeof dt (Intg i) = Some (PrimT Integer)"
-        "typeof dt  Null    = Some NT"
-        "typeof dt (Addr a) = dt a"
+primrec defpval :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
+where
+  "defpval Void = Unit"
+| "defpval Boolean = Bool False"
+| "defpval Integer = Intg 0"
 
-primrec "defpval Void    = Unit"
-        "defpval Boolean = Bool False"
-        "defpval Integer = Intg 0"
-primrec "default_val (PrimT pt) = defpval pt"
-        "default_val (RefT  r ) = Null"
+primrec default_val :: "ty \<Rightarrow> val"  --{* default value for all types *}
+where
+  "default_val (PrimT pt) = defpval pt"
+| "default_val (RefT  r ) = Null"
 
 end
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/WellForm.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -31,8 +31,9 @@
 text  {* well-formed field declaration (common part for classes and interfaces),
         cf. 8.3 and (9.3) *}
 
-definition wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" where
- "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
+definition
+  wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
+  where "wf_fdecl G P = (\<lambda>(fn,f). is_acc_type G P (type f))"
 
 lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
 apply (unfold wf_fdecl_def)
@@ -54,11 +55,12 @@
 \item the parameter names are unique
 \end{itemize} 
 *}
-definition wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
- "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
+definition
+  wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
+  "wf_mhead G P = (\<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
                             \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
                             is_acc_type G P (resTy mh) \<and>
-                            \<spacespace> distinct (pars mh)"
+                            \<spacespace> distinct (pars mh))"
 
 
 text {*
@@ -76,23 +78,25 @@
 \end{itemize}
 *}
 
-definition callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
-"callee_lcl C sig m 
- \<equiv> \<lambda> k. (case k of
+definition
+  callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
+  "callee_lcl C sig m =
+    (\<lambda>k. (case k of
             EName e 
             \<Rightarrow> (case e of 
                   VNam v 
                   \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
                 | Res \<Rightarrow> Some (resTy m))
-          | This \<Rightarrow> if is_static m then None else Some (Class C))"
+          | This \<Rightarrow> if is_static m then None else Some (Class C)))"
 
-definition parameters :: "methd \<Rightarrow> lname set" where
-"parameters m \<equiv>  set (map (EName \<circ> VNam) (pars m)) 
-                  \<union> (if (static m) then {} else {This})"
+definition
+  parameters :: "methd \<Rightarrow> lname set" where
+  "parameters m = set (map (EName \<circ> VNam) (pars m)) \<union> (if (static m) then {} else {This})"
 
-definition wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
- "wf_mdecl G C \<equiv> 
-      \<lambda>(sig,m).
+definition
+  wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
+  "wf_mdecl G C =
+      (\<lambda>(sig,m).
           wf_mhead G (pid C) sig (mhead m) \<and> 
           unique (lcls (mbody m)) \<and> 
           (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
@@ -102,7 +106,7 @@
           \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and>
           (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> 
                 \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 
-               \<and> Result \<in> nrm A)"
+               \<and> Result \<in> nrm A))"
 
 lemma callee_lcl_VNam_simp [simp]:
 "callee_lcl C sig m (EName (VNam v)) 
@@ -216,9 +220,10 @@
       superinterfaces widens to each of the corresponding result types
 \end{itemize}
 *}
-definition wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
- "wf_idecl G \<equiv> 
-    \<lambda>(I,i). 
+definition
+  wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
+ "wf_idecl G =
+    (\<lambda>(I,i). 
         ws_idecl G I (isuperIfs i) \<and> 
         \<not>is_class G I \<and>
         (\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
@@ -233,7 +238,7 @@
                              is_static new = is_static old)) \<and> 
         (Option.set \<circ> table_of (imethods i) 
                hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
-               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
+               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))"
 
 lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow>  
   wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
@@ -317,8 +322,9 @@
 \end{itemize}
 *}
 (* to Table *)
-definition entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20) where
-"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
+definition
+  entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20)
+  where "(t entails P) = (\<forall>k. \<forall> x \<in> t k: P x)"
 
 lemma entailsD:
  "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
@@ -327,9 +333,10 @@
 lemma empty_entails[simp]: "empty entails P"
 by (simp add: entails_def)
 
-definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
-"wf_cdecl G \<equiv> 
-   \<lambda>(C,c).
+definition
+  wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
+  "wf_cdecl G =
+     (\<lambda>(C,c).
       \<not>is_iface G C \<and>
       (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
         (\<forall>s. \<forall> im \<in> imethds G I s.
@@ -352,7 +359,7 @@
                        (G,sig\<turnstile>new hides old 
                          \<longrightarrow> (accmodi old \<le> accmodi new \<and>
                               is_static old)))) 
-            ))"
+            )))"
 
 (*
 definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
@@ -511,13 +518,14 @@
 \item all defined classes are wellformed
 \end{itemize}
 *}
-definition wf_prog :: "prog \<Rightarrow> bool" where
- "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
+definition
+  wf_prog :: "prog \<Rightarrow> bool" where
+ "wf_prog G = (let is = ifaces G; cs = classes G in
                  ObjectC \<in> set cs \<and> 
                 (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
                 (\<forall>xn. SXcptC xn \<in> set cs) \<and>
                 (\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
-                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
+                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs)"
 
 lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)"
 apply (unfold wf_prog_def Let_def)
@@ -2095,16 +2103,16 @@
  Class    dynC 
  Array    Object
 *}
-consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
+primrec valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
                         ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
-primrec
-"G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
-"G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
-              = (if static_membr 
-                    then dynC=Object 
-                    else G\<turnstile>Class dynC\<preceq> Iface I)"
-"G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
-"G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
+where
+  "G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
+| "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
+                = (if static_membr 
+                      then dynC=Object 
+                      else G\<turnstile>Class dynC\<preceq> Iface I)"
+| "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
+| "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
 
 lemma valid_lookup_cls_is_class:
   assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
diff -r f87d1105e181 -r ee939247b2fb src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/WellType.thy	Mon Jul 26 17:41:26 2010 +0200
@@ -53,11 +53,13 @@
   emhead = "ref_ty \<times> mhead"
 
 --{* Some mnemotic selectors for emhead *}
-definition "declrefT" :: "emhead \<Rightarrow> ref_ty" where
-  "declrefT \<equiv> fst"
+definition
+  "declrefT" :: "emhead \<Rightarrow> ref_ty"
+  where "declrefT = fst"
 
-definition "mhd"     :: "emhead \<Rightarrow> mhead" where
-  "mhd \<equiv> snd"
+definition
+  "mhd" :: "emhead \<Rightarrow> mhead"
+  where "mhd \<equiv> snd"
 
 lemma declrefT_simp[simp]:"declrefT (r,m) = r"
 by (simp add: declrefT_def)
@@ -77,50 +79,51 @@
 lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
 by (cases m) simp
 
-consts
-  cmheads        :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
-  Objectmheads   :: "prog \<Rightarrow> qtname           \<Rightarrow> sig \<Rightarrow> emhead set"
-  accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
-  mheads         :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
-defs
- cmheads_def:
-"cmheads G S C 
-  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
-  Objectmheads_def:
-"Objectmheads G S  
-  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
-    ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
-  accObjectmheads_def:
-"accObjectmheads G S T
-   \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
-        then Objectmheads G S
-        else (\<lambda>sig. {})"
-primrec
-"mheads G S  NullT     = (\<lambda>sig. {})"
-"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
-                         ` accimethds G (pid S) I sig \<union> 
-                           accObjectmheads G S (IfaceT I) sig)"
-"mheads G S (ClassT C) = cmheads G S C"
-"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
+definition
+  cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
+  where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))"
+
+definition
+  Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
+  "Objectmheads G S =
+    (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
+      ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
+
+definition
+  accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
+where
+  "accObjectmheads G S T =
+    (if G\<turnstile>RefT T accessible_in (pid S)
+     then Objectmheads G S
+     else (\<lambda>sig. {}))"
+
+primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
+where
+  "mheads G S  NullT     = (\<lambda>sig. {})"
+| "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
+                           ` accimethds G (pid S) I sig \<union> 
+                             accObjectmheads G S (IfaceT I) sig)"
+| "mheads G S (ClassT C) = cmheads G S C"
+| "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
 
 definition
   --{* applicable methods, cf. 15.11.2.1 *}
-  appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
- "appl_methds G S rt = (\<lambda> sig. 
+  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+  "appl_methds G S rt = (\<lambda> sig. 
       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
                            G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
 
 definition
   --{* more specific methods, cf. 15.11.2.2 *}
-  more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
- "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
+  more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
+  "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
 (*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
 
 definition
   --{* maximally specific methods, cf. 15.11.2.2 *}
-   max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
- "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
-                      (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
+  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+  "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
+                          (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
 
 
 lemma max_spec2appl_meths: 
@@ -138,13 +141,15 @@
 done
 
 
-definition empty_dt :: "dyn_ty" where
- "empty_dt \<equiv> \<lambda>a. None"
+definition
+  empty_dt :: "dyn_ty"
+  where "empty_dt = (\<lambda>a. None)"
 
-definition invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
-"invmode m e \<equiv> if is_static m 
+definition
+  invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
+  "invmode m e = (if is_static m 
                   then Static 
-                  else if e=Super then SuperM else IntVir"
+                  else if e=Super then SuperM else IntVir)"
 
 lemma invmode_nonstatic [simp]: 
   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
@@ -171,71 +176,71 @@
 
 section "Typing for unary operations"
 
-consts unop_type :: "unop \<Rightarrow> prim_ty"
-primrec 
-"unop_type UPlus   = Integer"
-"unop_type UMinus  = Integer"
-"unop_type UBitNot = Integer"
-"unop_type UNot    = Boolean"    
+primrec unop_type :: "unop \<Rightarrow> prim_ty"
+where
+  "unop_type UPlus   = Integer"
+| "unop_type UMinus  = Integer"
+| "unop_type UBitNot = Integer"
+| "unop_type UNot    = Boolean"    
 
-consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
-primrec
-"wt_unop UPlus   t = (t = PrimT Integer)"
-"wt_unop UMinus  t = (t = PrimT Integer)"
-"wt_unop UBitNot t = (t = PrimT Integer)"
-"wt_unop UNot    t = (t = PrimT Boolean)"
+primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
+where
+  "wt_unop UPlus   t = (t = PrimT Integer)"
+| "wt_unop UMinus  t = (t = PrimT Integer)"
+| "wt_unop UBitNot t = (t = PrimT Integer)"
+| "wt_unop UNot    t = (t = PrimT Boolean)"
 
 section "Typing for binary operations"
 
-consts binop_type :: "binop \<Rightarrow> prim_ty"
-primrec
-"binop_type Mul      = Integer"     
-"binop_type Div      = Integer"
-"binop_type Mod      = Integer"
-"binop_type Plus     = Integer"
-"binop_type Minus    = Integer"
-"binop_type LShift   = Integer"
-"binop_type RShift   = Integer"
-"binop_type RShiftU  = Integer"
-"binop_type Less     = Boolean"
-"binop_type Le       = Boolean"
-"binop_type Greater  = Boolean"
-"binop_type Ge       = Boolean"
-"binop_type Eq       = Boolean"
-"binop_type Neq      = Boolean"
-"binop_type BitAnd   = Integer"
-"binop_type And      = Boolean"
-"binop_type BitXor   = Integer"
-"binop_type Xor      = Boolean"
-"binop_type BitOr    = Integer"
-"binop_type Or       = Boolean"
-"binop_type CondAnd  = Boolean"
-"binop_type CondOr   = Boolean"
+primrec binop_type :: "binop \<Rightarrow> prim_ty"
+where
+  "binop_type Mul      = Integer"     
+| "binop_type Div      = Integer"
+| "binop_type Mod      = Integer"
+| "binop_type Plus     = Integer"
+| "binop_type Minus    = Integer"
+| "binop_type LShift   = Integer"
+| "binop_type RShift   = Integer"
+| "binop_type RShiftU  = Integer"
+| "binop_type Less     = Boolean"
+| "binop_type Le       = Boolean"
+| "binop_type Greater  = Boolean"
+| "binop_type Ge       = Boolean"
+| "binop_type Eq       = Boolean"
+| "binop_type Neq      = Boolean"
+| "binop_type BitAnd   = Integer"
+| "binop_type And      = Boolean"
+| "binop_type BitXor   = Integer"
+| "binop_type Xor      = Boolean"
+| "binop_type BitOr    = Integer"
+| "binop_type Or       = Boolean"
+| "binop_type CondAnd  = Boolean"
+| "binop_type CondOr   = Boolean"
 
-consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
-primrec
-"wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
-"wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
-"wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+  "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
+| "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
+| "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 
 section "Typing for terms"
 
@@ -244,9 +249,8 @@
   (type) "tys" <= (type) "ty + ty list"
 
 
-inductive
-  wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
-  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
+inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
+  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51] 50)
   and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"