modernized/unified some specifications;
authorwenzelm
Mon Jul 26 17:41:26 2010 +0200 (2010-07-26)
changeset 37956ee939247b2fb
parent 37955 f87d1105e181
child 37957 00e848690339
modernized/unified some specifications;
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxExample.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Conform.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/Trans.thy
src/HOL/Bali/Type.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/Value.thy
src/HOL/Bali/WellForm.thy
src/HOL/Bali/WellType.thy
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -20,8 +20,9 @@
     1.4             
     1.5  section "set of not yet initialzed classes"
     1.6  
     1.7 -definition nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set" where
     1.8 - "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
     1.9 +definition
    1.10 +  nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
    1.11 +  where "nyinitcls G s = {C. is_class G C \<and> \<not> initd C s}"
    1.12  
    1.13  lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
    1.14  apply (unfold nyinitcls_def)
    1.15 @@ -113,8 +114,9 @@
    1.16  
    1.17  section "init-le"
    1.18  
    1.19 -definition init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_"  [51,51] 50) where
    1.20 - "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
    1.21 +definition
    1.22 +  init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_"  [51,51] 50)
    1.23 +  where "G\<turnstile>init\<le>n = (\<lambda>s. card (nyinitcls G s) \<le> n)"
    1.24    
    1.25  lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
    1.26  apply (unfold init_le_def)
    1.27 @@ -132,27 +134,22 @@
    1.28  
    1.29  section "Most General Triples and Formulas"
    1.30  
    1.31 -definition remember_init_state :: "state assn" ("\<doteq>") where
    1.32 -  "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
    1.33 +definition
    1.34 +  remember_init_state :: "state assn" ("\<doteq>")
    1.35 +  where "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
    1.36  
    1.37  lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
    1.38  apply (unfold remember_init_state_def)
    1.39  apply (simp (no_asm))
    1.40  done
    1.41  
    1.42 -consts
    1.43 -  
    1.44 +definition
    1.45    MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
    1.46 -  MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
    1.47 +  where "{P} t\<succ> {G\<rightarrow>} = {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
    1.48  
    1.49 -defs
    1.50 -  
    1.51 -
    1.52 -  MGF_def:
    1.53 -  "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
    1.54 -
    1.55 -  MGFn_def:
    1.56 -  "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
    1.57 +definition
    1.58 +  MGFn :: "[nat, term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
    1.59 +  where "{=:n} t\<succ> {G\<rightarrow>} = {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
    1.60  
    1.61  (* unused *)
    1.62  lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
    1.63 @@ -574,9 +571,9 @@
    1.64  unroll the loop in iterated evaluations of the expression and evaluations of
    1.65  the loop body. *}
    1.66  
    1.67 -definition unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set" where
    1.68 -
    1.69 - "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2.
    1.70 +definition
    1.71 +  unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set" where
    1.72 +  "unroll G l e c = {(s,t). \<exists> v s1 s2.
    1.73                               G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and>
    1.74                               G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}"
    1.75  
     2.1 --- a/src/HOL/Bali/AxExample.thy	Mon Jul 26 13:50:52 2010 +0200
     2.2 +++ b/src/HOL/Bali/AxExample.thy	Mon Jul 26 17:41:26 2010 +0200
     2.3 @@ -8,10 +8,11 @@
     2.4  imports AxSem Example
     2.5  begin
     2.6  
     2.7 -definition arr_inv :: "st \<Rightarrow> bool" where
     2.8 - "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
     2.9 +definition
    2.10 +  arr_inv :: "st \<Rightarrow> bool" where
    2.11 + "arr_inv = (\<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
    2.12                                values obj (Inl (arr, Base)) = Some (Addr a) \<and>
    2.13 -                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"
    2.14 +                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)"
    2.15  
    2.16  lemma arr_inv_new_obj: 
    2.17  "\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"
     3.1 --- a/src/HOL/Bali/AxSem.thy	Mon Jul 26 13:50:52 2010 +0200
     3.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Jul 26 17:41:26 2010 +0200
     3.3 @@ -62,8 +62,9 @@
     3.4  translations
     3.5    (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
     3.6  
     3.7 -definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
     3.8 - "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
     3.9 +definition
    3.10 +  assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25)
    3.11 +  where "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
    3.12    
    3.13  lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
    3.14  apply (unfold assn_imp_def)
    3.15 @@ -75,8 +76,9 @@
    3.16  
    3.17  subsection "peek-and"
    3.18  
    3.19 -definition peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13) where
    3.20 - "P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"
    3.21 +definition
    3.22 +  peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
    3.23 +  where "(P \<and>. p) = (\<lambda>Y s Z. P Y s Z \<and> p s)"
    3.24  
    3.25  lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"
    3.26  apply (unfold peek_and_def)
    3.27 @@ -114,8 +116,9 @@
    3.28  
    3.29  subsection "assn-supd"
    3.30  
    3.31 -definition assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13) where
    3.32 - "P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"
    3.33 +definition
    3.34 +  assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
    3.35 +  where "(P ;. f) = (\<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s)"
    3.36  
    3.37  lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"
    3.38  apply (unfold assn_supd_def)
    3.39 @@ -124,8 +127,9 @@
    3.40  
    3.41  subsection "supd-assn"
    3.42  
    3.43 -definition supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13) where
    3.44 - "f .; P \<equiv> \<lambda>Y s. P Y (f s)"
    3.45 +definition
    3.46 +  supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
    3.47 +  where "(f .; P) = (\<lambda>Y s. P Y (f s))"
    3.48  
    3.49  
    3.50  lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"
    3.51 @@ -143,8 +147,9 @@
    3.52  
    3.53  subsection "subst-res"
    3.54  
    3.55 -definition subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_"  [60,61] 60) where
    3.56 - "P\<leftarrow>w \<equiv> \<lambda>Y. P w"
    3.57 +definition
    3.58 +  subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_"  [60,61] 60)
    3.59 +  where "P\<leftarrow>w = (\<lambda>Y. P w)"
    3.60  
    3.61  lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"
    3.62  apply (unfold subst_res_def)
    3.63 @@ -178,8 +183,9 @@
    3.64  
    3.65  subsection "subst-Bool"
    3.66  
    3.67 -definition subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60) where
    3.68 - "P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
    3.69 +definition
    3.70 +  subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60)
    3.71 +  where "P\<leftarrow>=b = (\<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
    3.72  
    3.73  lemma subst_Bool_def2 [simp]: 
    3.74  "(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
    3.75 @@ -193,8 +199,9 @@
    3.76  
    3.77  subsection "peek-res"
    3.78  
    3.79 -definition peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
    3.80 - "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
    3.81 +definition
    3.82 +  peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
    3.83 +  where "peek_res Pf = (\<lambda>Y. Pf Y Y)"
    3.84  
    3.85  syntax
    3.86    "_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
    3.87 @@ -221,8 +228,9 @@
    3.88  
    3.89  subsection "ign-res"
    3.90  
    3.91 -definition ign_res :: "        'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000) where
    3.92 -  "P\<down>        \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
    3.93 +definition
    3.94 +  ign_res :: "'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000)
    3.95 +  where "P\<down> = (\<lambda>Y s Z. \<exists>Y. P Y s Z)"
    3.96  
    3.97  lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"
    3.98  apply (unfold ign_res_def)
    3.99 @@ -252,8 +260,9 @@
   3.100  
   3.101  subsection "peek-st"
   3.102  
   3.103 -definition peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
   3.104 - "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
   3.105 +definition
   3.106 +  peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
   3.107 +  where "peek_st P = (\<lambda>Y s. P (store s) Y s)"
   3.108  
   3.109  syntax
   3.110    "_peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
   3.111 @@ -296,8 +305,9 @@
   3.112  
   3.113  subsection "ign-res-eq"
   3.114  
   3.115 -definition ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_"  [60,61] 60) where
   3.116 - "P\<down>=w       \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
   3.117 +definition
   3.118 +  ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_"  [60,61] 60)
   3.119 +  where "P\<down>=w \<equiv> (\<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w))"
   3.120  
   3.121  lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"
   3.122  apply (unfold ign_res_eq_def)
   3.123 @@ -326,8 +336,9 @@
   3.124  
   3.125  subsection "RefVar"
   3.126  
   3.127 -definition RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13) where
   3.128 - "vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"
   3.129 +definition
   3.130 +  RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13)
   3.131 +  where "(vf ..; P) = (\<lambda>Y s. let (v,s') = vf s in P (Var v) s')"
   3.132   
   3.133  lemma RefVar_def2 [simp]: "(vf ..; P) Y s =  
   3.134    P (Var (fst (vf s))) (snd (vf s))"
   3.135 @@ -337,12 +348,13 @@
   3.136  
   3.137  subsection "allocation"
   3.138  
   3.139 -definition Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
   3.140 - "Alloc G otag P \<equiv> \<lambda>Y s Z.
   3.141 -                   \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"
   3.142 +definition
   3.143 +  Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   3.144 +  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)"
   3.145  
   3.146 -definition SXAlloc     :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
   3.147 - "SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"
   3.148 +definition
   3.149 +  SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   3.150 +  where "SXAlloc G P = (\<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"
   3.151  
   3.152  
   3.153  lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =  
   3.154 @@ -359,11 +371,12 @@
   3.155  
   3.156  section "validity"
   3.157  
   3.158 -definition type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
   3.159 - "type_ok G t s \<equiv> 
   3.160 -    \<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
   3.161 -                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
   3.162 -              \<and> s\<Colon>\<preceq>(G,L)"
   3.163 +definition
   3.164 +  type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
   3.165 +  "type_ok G t s =
   3.166 +    (\<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
   3.167 +                             \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
   3.168 +               \<and> s\<Colon>\<preceq>(G,L))"
   3.169  
   3.170  datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
   3.171  something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
   3.172 @@ -407,34 +420,35 @@
   3.173  
   3.174  definition mtriples :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 
   3.175                  ('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times>  'sig) set \<Rightarrow> 'a triples" ("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75) where
   3.176 - "{{P} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
   3.177 + "{{P} tf-\<succ> {Q} | ms} = (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
   3.178    
   3.179 -consts
   3.180 -
   3.181 - triple_valid :: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
   3.182 -                                                (   "_\<Turnstile>_:_" [61,0, 58] 57)
   3.183 -    ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
   3.184 -                                                ("_,_|\<Turnstile>_"   [61,58,58] 57)
   3.185 +definition
   3.186 +  triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple  \<Rightarrow> bool"  ("_\<Turnstile>_:_" [61,0, 58] 57)
   3.187 +  where
   3.188 +    "G\<Turnstile>n:t =
   3.189 +      (case t of {P} t\<succ> {Q} \<Rightarrow>
   3.190 +        \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
   3.191 +        (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z))"
   3.192  
   3.193  abbreviation
   3.194 - triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
   3.195 -                                                (  "_||=_:_" [61,0, 58] 57)
   3.196 - where "G||=n:ts == Ball ts (triple_valid G n)"
   3.197 +  triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"  (  "_||=_:_" [61,0, 58] 57)
   3.198 +  where "G||=n:ts == Ball ts (triple_valid G n)"
   3.199 +
   3.200 +notation (xsymbols)
   3.201 +  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57)
   3.202 +
   3.203 +
   3.204 +definition
   3.205 +  ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"  ("_,_|\<Turnstile>_" [61,58,58] 57)
   3.206 +  where "(G,A|\<Turnstile>ts) = (\<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts)"
   3.207  
   3.208  abbreviation
   3.209 - ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   3.210 -                                                ( "_,_|=_"   [61,58,58] 57)
   3.211 - where "G,A |=t == G,A|\<Turnstile>{t}"
   3.212 +  ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"  ( "_,_|=_"   [61,58,58] 57)
   3.213 +  where "G,A |=t == G,A|\<Turnstile>{t}"
   3.214  
   3.215  notation (xsymbols)
   3.216 -  triples_valid  ("_|\<Turnstile>_:_" [61,0, 58] 57) and
   3.217    ax_valid  ("_,_\<Turnstile>_" [61,58,58] 57)
   3.218  
   3.219 -defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
   3.220 -                          \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
   3.221 -                          (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
   3.222 -
   3.223 -defs  ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
   3.224  
   3.225  lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
   3.226   (\<forall>Y s Z. P Y s Z 
   3.227 @@ -625,8 +639,9 @@
   3.228  axioms 
   3.229  *)
   3.230  
   3.231 -definition adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
   3.232 -"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)"
   3.233 +definition
   3.234 +  adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   3.235 +  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))"
   3.236  
   3.237  
   3.238  section "rules derived by induction"
     4.1 --- a/src/HOL/Bali/AxSound.thy	Mon Jul 26 13:50:52 2010 +0200
     4.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Jul 26 17:41:26 2010 +0200
     4.3 @@ -9,18 +9,15 @@
     4.4  
     4.5  section "validity"
     4.6  
     4.7 -consts
     4.8 -
     4.9 - triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
    4.10 -                                                (   "_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
    4.11 -    ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
    4.12 -                                                ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
    4.13 -
    4.14 -defs  triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
    4.15 - \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) 
    4.16 - \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
    4.17 -                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
    4.18 - (\<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))))"
    4.19 +definition
    4.20 +  triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool"  ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
    4.21 +  where
    4.22 +    "G\<Turnstile>n\<Colon>t =
    4.23 +      (case t of {P} t\<succ> {Q} \<Rightarrow>
    4.24 +        \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L)
    4.25 +          \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and>
    4.26 +            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
    4.27 +             (\<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)))))"
    4.28  
    4.29  text {* This definition differs from the ordinary  @{text triple_valid_def} 
    4.30  manly in the conclusion: We also ensures conformance of the result state. So
    4.31 @@ -29,8 +26,10 @@
    4.32  proof of the axiomatic semantics, in the end we will conclude to 
    4.33  the ordinary definition.
    4.34  *}
    4.35 - 
    4.36 -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)"
    4.37 +
    4.38 +definition
    4.39 +  ax_valids2 :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"  ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
    4.40 +  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))"
    4.41  
    4.42  lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} =  
    4.43   (\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow>  
     5.1 --- a/src/HOL/Bali/Basis.thy	Mon Jul 26 13:50:52 2010 +0200
     5.2 +++ b/src/HOL/Bali/Basis.thy	Mon Jul 26 17:41:26 2010 +0200
     5.3 @@ -180,31 +180,34 @@
     5.4  
     5.5  notation sum_case  (infixr "'(+')"80)
     5.6  
     5.7 -consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
     5.8 -          the_Inr  :: "'a + 'b \<Rightarrow> 'b"
     5.9 -primrec  "the_Inl (Inl a) = a"
    5.10 -primrec  "the_Inr (Inr b) = b"
    5.11 +primrec the_Inl  :: "'a + 'b \<Rightarrow> 'a"
    5.12 +  where "the_Inl (Inl a) = a"
    5.13 +
    5.14 +primrec the_Inr  :: "'a + 'b \<Rightarrow> 'b"
    5.15 +  where "the_Inr (Inr b) = b"
    5.16  
    5.17  datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
    5.18  
    5.19 -consts    the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
    5.20 -          the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
    5.21 -          the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
    5.22 -primrec  "the_In1 (In1 a) = a"
    5.23 -primrec  "the_In2 (In2 b) = b"
    5.24 -primrec  "the_In3 (In3 c) = c"
    5.25 +primrec the_In1  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
    5.26 +  where "the_In1 (In1 a) = a"
    5.27 +
    5.28 +primrec the_In2  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
    5.29 +  where "the_In2 (In2 b) = b"
    5.30 +
    5.31 +primrec the_In3  :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
    5.32 +  where "the_In3 (In3 c) = c"
    5.33  
    5.34  abbreviation In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    5.35 -      where "In1l e == In1 (Inl e)"
    5.36 +  where "In1l e == In1 (Inl e)"
    5.37  
    5.38  abbreviation In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    5.39 -      where "In1r c == In1 (Inr c)"
    5.40 +  where "In1r c == In1 (Inr c)"
    5.41  
    5.42  abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
    5.43 -      where "the_In1l == the_Inl \<circ> the_In1"
    5.44 +  where "the_In1l == the_Inl \<circ> the_In1"
    5.45  
    5.46  abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
    5.47 -      where "the_In1r == the_Inr \<circ> the_In1"
    5.48 +  where "the_In1r == the_Inr \<circ> the_In1"
    5.49  
    5.50  ML {*
    5.51  fun sum3_instantiate ctxt thm = map (fn s =>
    5.52 @@ -232,8 +235,9 @@
    5.53  
    5.54  text{* Deemed too special for theory Map. *}
    5.55  
    5.56 -definition chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" where
    5.57 - "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    5.58 +definition
    5.59 +  chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    5.60 +  where "chg_map f a m = (case m a of None => m | Some b => m(a|->f b))"
    5.61  
    5.62  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    5.63  by (unfold chg_map_def, auto)
    5.64 @@ -247,8 +251,9 @@
    5.65  
    5.66  section "unique association lists"
    5.67  
    5.68 -definition unique :: "('a \<times> 'b) list \<Rightarrow> bool" where
    5.69 - "unique \<equiv> distinct \<circ> map fst"
    5.70 +definition
    5.71 +  unique :: "('a \<times> 'b) list \<Rightarrow> bool"
    5.72 +  where "unique = distinct \<circ> map fst"
    5.73  
    5.74  lemma uniqueD [rule_format (no_asm)]: 
    5.75  "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"
    5.76 @@ -296,11 +301,11 @@
    5.77  
    5.78  section "list patterns"
    5.79  
    5.80 -consts
    5.81 -  lsplit         :: "[['a, 'a list] => 'b, 'a list] => 'b"
    5.82 -defs
    5.83 -  lsplit_def:    "lsplit == %f l. f (hd l) (tl l)"
    5.84 -(*  list patterns -- extends pre-defined type "pttrn" used in abstractions *)
    5.85 +definition
    5.86 +  lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b" where
    5.87 +  "lsplit = (\<lambda>f l. f (hd l) (tl l))"
    5.88 +
    5.89 +text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *}
    5.90  syntax
    5.91    "_lpttrn"    :: "[pttrn,pttrn] => pttrn"     ("_#/_" [901,900] 900)
    5.92  translations
     6.1 --- a/src/HOL/Bali/Conform.thy	Mon Jul 26 13:50:52 2010 +0200
     6.2 +++ b/src/HOL/Bali/Conform.thy	Mon Jul 26 17:41:26 2010 +0200
     6.3 @@ -96,8 +96,8 @@
     6.4  
     6.5  section "value conformance"
     6.6  
     6.7 -definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70) where
     6.8 -           "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"
     6.9 +definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
    6.10 +  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)"
    6.11  
    6.12  lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
    6.13  by (auto simp: conf_def)
    6.14 @@ -177,8 +177,9 @@
    6.15  
    6.16  section "value list conformance"
    6.17  
    6.18 -definition lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) where
    6.19 -           "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"
    6.20 +definition
    6.21 +  lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
    6.22 +  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)"
    6.23  
    6.24  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"
    6.25  by (force simp: lconf_def)
    6.26 @@ -260,8 +261,9 @@
    6.27  *}
    6.28  
    6.29    
    6.30 -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
    6.31 -           "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"
    6.32 +definition
    6.33 +  wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
    6.34 +  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)"
    6.35  
    6.36  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"
    6.37  by (auto simp: wlconf_def)
    6.38 @@ -338,11 +340,12 @@
    6.39  
    6.40  section "object conformance"
    6.41  
    6.42 -definition oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
    6.43 -           "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
    6.44 +definition
    6.45 +  oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
    6.46 +  "(G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r) = (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
    6.47                             (case r of 
    6.48                                Heap a \<Rightarrow> is_type G (obj_ty obj) 
    6.49 -                            | Stat C \<Rightarrow> True)"
    6.50 +                            | Stat C \<Rightarrow> True))"
    6.51  
    6.52  
    6.53  lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
    6.54 @@ -373,12 +376,14 @@
    6.55  
    6.56  section "state conformance"
    6.57  
    6.58 -definition conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"   ("_\<Colon>\<preceq>_"   [71,71]      70)  where
    6.59 -   "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
    6.60 -    (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
    6.61 -                \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
    6.62 -    (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
    6.63 -         (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)"
    6.64 +definition
    6.65 +  conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"  ("_\<Colon>\<preceq>_" [71,71] 70)  where
    6.66 +   "xs\<Colon>\<preceq>E =
    6.67 +      (let (G, L) = E; s = snd xs; l = locals s in
    6.68 +        (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
    6.69 +                    \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
    6.70 +        (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
    6.71 +             (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
    6.72  
    6.73  section "conforms"
    6.74  
     7.1 --- a/src/HOL/Bali/Decl.thy	Mon Jul 26 13:50:52 2010 +0200
     7.2 +++ b/src/HOL/Bali/Decl.thy	Mon Jul 26 17:41:26 2010 +0200
     7.3 @@ -206,8 +206,9 @@
     7.4    (type) "mdecl" <= (type) "sig \<times> methd"
     7.5  
     7.6  
     7.7 -definition mhead :: "methd \<Rightarrow> mhead" where
     7.8 -  "mhead m \<equiv> \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
     7.9 +definition
    7.10 +  mhead :: "methd \<Rightarrow> mhead"
    7.11 +  where "mhead m = \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
    7.12  
    7.13  lemma access_mhead [simp]:"access (mhead m) = access m"
    7.14  by (simp add: mhead_def)
    7.15 @@ -237,7 +238,7 @@
    7.16  
    7.17  definition
    7.18  memberdecl_memberid_def:
    7.19 -  "memberid m \<equiv> (case m of
    7.20 +  "memberid m = (case m of
    7.21                      fdecl (vn,f)  \<Rightarrow> fid vn
    7.22                    | mdecl (sig,m) \<Rightarrow> mid sig)"
    7.23  
    7.24 @@ -262,7 +263,7 @@
    7.25  
    7.26  definition
    7.27  pair_memberid_def:
    7.28 -  "memberid p \<equiv> memberid (snd p)"
    7.29 +  "memberid p = memberid (snd p)"
    7.30  
    7.31  instance ..
    7.32  
    7.33 @@ -274,8 +275,9 @@
    7.34  lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
    7.35  by (simp add: pair_memberid_def)
    7.36  
    7.37 -definition is_field :: "qtname \<times> memberdecl \<Rightarrow> bool" where
    7.38 -"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)"
    7.39 +definition
    7.40 +  is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
    7.41 +  where "is_field m = (\<exists> declC f. m=(declC,fdecl f))"
    7.42    
    7.43  lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
    7.44  by (simp add: is_field_def)
    7.45 @@ -283,8 +285,9 @@
    7.46  lemma is_fieldI: "is_field (C,fdecl f)"
    7.47  by (simp add: is_field_def)
    7.48  
    7.49 -definition is_method :: "qtname \<times> memberdecl \<Rightarrow> bool" where
    7.50 -"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)"
    7.51 +definition
    7.52 +  is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
    7.53 +  where "is_method membr = (\<exists>declC m. membr=(declC,mdecl m))"
    7.54    
    7.55  lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
    7.56  by (simp add: is_method_def)
    7.57 @@ -314,8 +317,9 @@
    7.58                        isuperIfs::qtname list,\<dots>::'a\<rparr>"
    7.59    (type) "idecl" <= (type) "qtname \<times> iface"
    7.60  
    7.61 -definition ibody :: "iface \<Rightarrow> ibody" where
    7.62 -  "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
    7.63 +definition
    7.64 +  ibody :: "iface \<Rightarrow> ibody"
    7.65 +  where "ibody i = \<lparr>access=access i,imethods=imethods i\<rparr>"
    7.66  
    7.67  lemma access_ibody [simp]: "(access (ibody i)) = access i"
    7.68  by (simp add: ibody_def)
    7.69 @@ -349,8 +353,9 @@
    7.70                        super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
    7.71    (type) "cdecl" <= (type) "qtname \<times> class"
    7.72  
    7.73 -definition cbody :: "class \<Rightarrow> cbody" where
    7.74 -  "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
    7.75 +definition
    7.76 +  cbody :: "class \<Rightarrow> cbody"
    7.77 +  where "cbody c = \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
    7.78  
    7.79  lemma access_cbody [simp]:"access (cbody c) = access c"
    7.80  by (simp add: cbody_def)
    7.81 @@ -368,18 +373,17 @@
    7.82  section "standard classes"
    7.83  
    7.84  consts
    7.85 -
    7.86    Object_mdecls  ::  "mdecl list" --{* methods of Object *}
    7.87    SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
    7.88 -  ObjectC ::         "cdecl"      --{* declaration  of root      class   *}
    7.89 -  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *}
    7.90 -
    7.91 -defs 
    7.92  
    7.93 +definition
    7.94 +  ObjectC ::         "cdecl"      --{* declaration  of root      class   *} where
    7.95 +  "ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
    7.96 +                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
    7.97  
    7.98 -ObjectC_def:"ObjectC  \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
    7.99 -                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
   7.100 -SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
   7.101 +definition
   7.102 +  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *} where
   7.103 +  "SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
   7.104                                     init=Skip,
   7.105                                     super=if xn = Throwable then Object 
   7.106                                                             else SXcpt Throwable,
   7.107 @@ -391,8 +395,9 @@
   7.108  lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
   7.109  by (simp add: SXcptC_def)
   7.110  
   7.111 -definition standard_classes :: "cdecl list" where
   7.112 -         "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
   7.113 +definition
   7.114 +  standard_classes :: "cdecl list" where
   7.115 +  "standard_classes = [ObjectC, SXcptC Throwable,
   7.116                  SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
   7.117                  SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
   7.118  
   7.119 @@ -426,16 +431,15 @@
   7.120  
   7.121  section "is type"
   7.122  
   7.123 -consts
   7.124 -  is_type :: "prog \<Rightarrow>     ty \<Rightarrow> bool"
   7.125 -  isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
   7.126 -
   7.127 -primrec "is_type G (PrimT pt)  = True"
   7.128 -        "is_type G (RefT  rt)  = isrtype G rt"
   7.129 -        "isrtype G (NullT    ) = True"
   7.130 -        "isrtype G (IfaceT tn) = is_iface G tn"
   7.131 -        "isrtype G (ClassT tn) = is_class G tn"
   7.132 -        "isrtype G (ArrayT T ) = is_type  G T"
   7.133 +primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
   7.134 +  and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
   7.135 +where
   7.136 +  "is_type G (PrimT pt)  = True"
   7.137 +| "is_type G (RefT  rt)  = isrtype G rt"
   7.138 +| "isrtype G (NullT) = True"
   7.139 +| "isrtype G (IfaceT tn) = is_iface G tn"
   7.140 +| "isrtype G (ClassT tn) = is_class G tn"
   7.141 +| "isrtype G (ArrayT T ) = is_type  G T"
   7.142  
   7.143  lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
   7.144  by auto
   7.145 @@ -446,13 +450,13 @@
   7.146  
   7.147  section "subinterface and subclass relation, in anticipation of TypeRel.thy"
   7.148  
   7.149 -consts 
   7.150 +definition
   7.151    subint1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
   7.152 -  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass     *}
   7.153 +  where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
   7.154  
   7.155 -defs
   7.156 -  subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
   7.157 -  subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
   7.158 +definition
   7.159 +  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass *}
   7.160 +  where "subcls1 G = {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
   7.161  
   7.162  abbreviation
   7.163    subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
   7.164 @@ -517,15 +521,18 @@
   7.165  
   7.166  section "well-structured programs"
   7.167  
   7.168 -definition ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool" where
   7.169 - "ws_idecl G I si \<equiv> \<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+"
   7.170 +definition
   7.171 +  ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
   7.172 +  where "ws_idecl G I si = (\<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+)"
   7.173    
   7.174 -definition ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" where
   7.175 - "ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
   7.176 +definition
   7.177 +  ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   7.178 +  where "ws_cdecl G C sc = (C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+)"
   7.179    
   7.180 -definition ws_prog  :: "prog \<Rightarrow> bool" where
   7.181 - "ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
   7.182 -              (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))"
   7.183 +definition
   7.184 +  ws_prog  :: "prog \<Rightarrow> bool" where
   7.185 +  "ws_prog G = ((\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
   7.186 +                 (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c)))"
   7.187  
   7.188  
   7.189  lemma ws_progI: 
   7.190 @@ -810,10 +817,10 @@
   7.191  apply simp
   7.192  done
   7.193  
   7.194 -definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   7.195 +definition
   7.196 +  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   7.197    --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
   7.198 -"imethds G I 
   7.199 -  \<equiv> iface_rec G I  
   7.200 +  "imethds G I = iface_rec G I
   7.201                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
   7.202                          (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
   7.203          
     8.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Jul 26 13:50:52 2010 +0200
     8.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Jul 26 17:41:26 2010 +0200
     8.3 @@ -9,7 +9,7 @@
     8.4  section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
     8.5  
     8.6  definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where
     8.7 -"is_public G qn \<equiv> (case class G qn of
     8.8 +"is_public G qn = (case class G qn of
     8.9                       None       \<Rightarrow> (case iface G qn of
    8.10                                        None       \<Rightarrow> False
    8.11                                      | Some i \<Rightarrow> access i = Public)
    8.12 @@ -21,33 +21,35 @@
    8.13  in their package or if they are defined public, an array type is accessible if
    8.14  its element type is accessible *}
    8.15   
    8.16 -consts accessible_in   :: "prog \<Rightarrow> ty     \<Rightarrow> pname \<Rightarrow> bool"  
    8.17 -                                      ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60)
    8.18 -       rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" 
    8.19 -                                      ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) 
    8.20  primrec
    8.21 -"G\<turnstile>(PrimT p)   accessible_in pack  = True"
    8.22 -accessible_in_RefT_simp: 
    8.23 -"G\<turnstile>(RefT  r)   accessible_in pack  = G\<turnstile>r accessible_in' pack"
    8.24 -
    8.25 -"G\<turnstile>(NullT)     accessible_in' pack = True"
    8.26 -"G\<turnstile>(IfaceT I)  accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
    8.27 -"G\<turnstile>(ClassT C)  accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
    8.28 -"G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
    8.29 +  accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool"  ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and
    8.30 +  rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool"  ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)
    8.31 +where
    8.32 +  "G\<turnstile>(PrimT p) accessible_in pack = True"
    8.33 +| accessible_in_RefT_simp:
    8.34 +  "G\<turnstile>(RefT  r) accessible_in pack = G\<turnstile>r accessible_in' pack"
    8.35 +| "G\<turnstile>(NullT) accessible_in' pack = True"
    8.36 +| "G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
    8.37 +| "G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
    8.38 +| "G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
    8.39  
    8.40  declare accessible_in_RefT_simp [simp del]
    8.41  
    8.42 -definition is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
    8.43 -    "is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
    8.44 +definition
    8.45 +  is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
    8.46 +  where "is_acc_class G P C = (is_class G C \<and> G\<turnstile>(Class C) accessible_in P)"
    8.47  
    8.48 -definition is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
    8.49 -    "is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
    8.50 +definition
    8.51 +  is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
    8.52 +  where "is_acc_iface G P I = (is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P)"
    8.53  
    8.54 -definition is_acc_type  :: "prog \<Rightarrow> pname \<Rightarrow> ty     \<Rightarrow> bool" where
    8.55 -    "is_acc_type  G P T \<equiv> is_type G T  \<and> G\<turnstile>T accessible_in P"
    8.56 +definition
    8.57 +  is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool"
    8.58 +  where "is_acc_type  G P T = (is_type G T  \<and> G\<turnstile>T accessible_in P)"
    8.59  
    8.60 -definition is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool" where
    8.61 -  "is_acc_reftype  G P T \<equiv> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
    8.62 +definition
    8.63 +  is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
    8.64 +  where "is_acc_reftype G P T = (isrtype G T  \<and> G\<turnstile>T accessible_in' P)"
    8.65  
    8.66  lemma is_acc_classD:
    8.67   "is_acc_class G P C \<Longrightarrow>  is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
    8.68 @@ -87,7 +89,7 @@
    8.69  begin
    8.70  
    8.71  definition
    8.72 -  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
    8.73 +  acc_modi_accmodi_def: "accmodi (a::acc_modi) = a"
    8.74  
    8.75  instance ..
    8.76  
    8.77 @@ -100,7 +102,7 @@
    8.78  begin
    8.79  
    8.80  definition
    8.81 -  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    8.82 +  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) = access d"
    8.83  
    8.84  instance ..
    8.85  
    8.86 @@ -113,7 +115,7 @@
    8.87  begin
    8.88  
    8.89  definition
    8.90 -  pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
    8.91 +  pair_acc_modi_def: "accmodi p = accmodi (snd p)"
    8.92  
    8.93  instance ..
    8.94  
    8.95 @@ -126,7 +128,7 @@
    8.96  begin
    8.97  
    8.98  definition
    8.99 -  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
   8.100 +  memberdecl_acc_modi_def: "accmodi m = (case m of
   8.101                                            fdecl f \<Rightarrow> accmodi f
   8.102                                          | mdecl m \<Rightarrow> accmodi m)"
   8.103  
   8.104 @@ -152,7 +154,7 @@
   8.105  begin
   8.106  
   8.107  definition
   8.108 -  "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
   8.109 +  "declclass q = \<lparr> pid = pid q, tid = tid q \<rparr>"
   8.110  
   8.111  instance ..
   8.112  
   8.113 @@ -169,7 +171,7 @@
   8.114  begin
   8.115  
   8.116  definition
   8.117 -  pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
   8.118 +  pair_declclass_def: "declclass p = declclass (fst p)"
   8.119  
   8.120  instance ..
   8.121  
   8.122 @@ -208,7 +210,7 @@
   8.123  begin
   8.124  
   8.125  definition
   8.126 -  pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
   8.127 +  pair_is_static_def: "is_static p = is_static (snd p)"
   8.128  
   8.129  instance ..
   8.130  
   8.131 @@ -225,7 +227,7 @@
   8.132  
   8.133  definition
   8.134  memberdecl_is_static_def: 
   8.135 - "is_static m \<equiv> (case m of
   8.136 + "is_static m = (case m of
   8.137                      fdecl f \<Rightarrow> is_static f
   8.138                    | mdecl m \<Rightarrow> is_static m)"
   8.139  
   8.140 @@ -246,28 +248,34 @@
   8.141  
   8.142  -- {* some mnemotic selectors for various pairs *} 
   8.143  
   8.144 -definition decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
   8.145 +definition
   8.146 +  decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
   8.147    "decliface = fst"          --{* get the interface component *}
   8.148  
   8.149 -definition mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
   8.150 +definition
   8.151 +  mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
   8.152    "mbr = snd"            --{* get the memberdecl component *}
   8.153  
   8.154 -definition mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
   8.155 +definition
   8.156 +  mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
   8.157    "mthd = snd"              --{* get the method component *}
   8.158      --{* also used for mdecl, mhead *}
   8.159  
   8.160 -definition fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
   8.161 +definition
   8.162 +  fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
   8.163    "fld = snd"               --{* get the field component *}
   8.164      --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
   8.165  
   8.166  -- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
   8.167  
   8.168 -definition fname:: "vname \<times> 'a \<Rightarrow> vname" where 
   8.169 -  "fname = fst"
   8.170 +definition
   8.171 +  fname:: "vname \<times> 'a \<Rightarrow> vname"
   8.172 +  where "fname = fst"
   8.173      --{* also used for fdecl *}
   8.174  
   8.175 -definition declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" where
   8.176 -  "declclassf = snd"
   8.177 +definition
   8.178 +  declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
   8.179 +  where "declclassf = snd"
   8.180  
   8.181  
   8.182  lemma decliface_simp[simp]: "decliface (I,m) = I"
   8.183 @@ -320,11 +328,13 @@
   8.184  
   8.185    --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
   8.186  
   8.187 -definition fldname :: "vname \<times> qtname \<Rightarrow> vname"  where
   8.188 -  "fldname = fst"
   8.189 +definition
   8.190 +  fldname :: "vname \<times> qtname \<Rightarrow> vname"
   8.191 +  where "fldname = fst"
   8.192  
   8.193 -definition fldclass :: "vname \<times> qtname \<Rightarrow> qtname" where
   8.194 -  "fldclass = snd"
   8.195 +definition
   8.196 +  fldclass :: "vname \<times> qtname \<Rightarrow> qtname"
   8.197 +  where "fldclass = snd"
   8.198  
   8.199  lemma fldname_simp[simp]: "fldname (n,c) = n"
   8.200  by (simp add: fldname_def)
   8.201 @@ -338,8 +348,9 @@
   8.202  text {* Convert a qualified method declaration (qualified with its declaring 
   8.203  class) to a qualified member declaration:  @{text methdMembr}  *}
   8.204  
   8.205 -definition methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" where
   8.206 - "methdMembr m = (fst m, mdecl (snd m))"
   8.207 +definition
   8.208 +  methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl"
   8.209 +  where "methdMembr m = (fst m, mdecl (snd m))"
   8.210  
   8.211  lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
   8.212  by (simp add: methdMembr_def)
   8.213 @@ -356,8 +367,9 @@
   8.214  text {* Convert a qualified method (qualified with its declaring 
   8.215  class) to a qualified member declaration:  @{text method}  *}
   8.216  
   8.217 -definition method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" where 
   8.218 -"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"
   8.219 +definition
   8.220 +  method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
   8.221 +  where "method sig m = (declclass m, mdecl (sig, mthd m))"
   8.222  
   8.223  lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
   8.224  by (simp add: method_def)
   8.225 @@ -377,8 +389,9 @@
   8.226  lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
   8.227    by (simp add: method_def) 
   8.228  
   8.229 -definition fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" where 
   8.230 -"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"
   8.231 +definition
   8.232 +  fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)"
   8.233 +  where "fieldm n f = (declclass f, fdecl (n, fld f))"
   8.234  
   8.235  lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
   8.236  by (simp add: fieldm_def)
   8.237 @@ -401,8 +414,9 @@
   8.238  text {* Select the signature out of a qualified method declaration:
   8.239   @{text msig} *}
   8.240  
   8.241 -definition msig :: "(qtname \<times> mdecl) \<Rightarrow> sig" where
   8.242 -"msig m \<equiv> fst (snd m)"
   8.243 +definition
   8.244 +  msig :: "(qtname \<times> mdecl) \<Rightarrow> sig"
   8.245 +  where "msig m = fst (snd m)"
   8.246  
   8.247  lemma msig_simp[simp]: "msig (c,(s,m)) = s"
   8.248  by (simp add: msig_def)
   8.249 @@ -410,8 +424,9 @@
   8.250  text {* Convert a qualified method (qualified with its declaring 
   8.251  class) to a qualified method declaration:  @{text qmdecl}  *}
   8.252  
   8.253 -definition qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)" where
   8.254 -"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"
   8.255 +definition
   8.256 +  qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
   8.257 +  where "qmdecl sig m = (declclass m, (sig,mthd m))"
   8.258  
   8.259  lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
   8.260  by (simp add: qmdecl_def)
   8.261 @@ -476,7 +491,7 @@
   8.262  begin
   8.263  
   8.264  definition
   8.265 -  pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
   8.266 +  pair_resTy_def: "resTy p = resTy (snd p)"
   8.267  
   8.268  instance ..
   8.269  
   8.270 @@ -503,14 +518,15 @@
   8.271        it is not accessible for inheritance at all.
   8.272  \end{itemize}
   8.273  *}
   8.274 -definition inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60) where
   8.275 -                  
   8.276 -"G\<turnstile>membr inheritable_in pack 
   8.277 -  \<equiv> (case (accmodi membr) of
   8.278 -       Private   \<Rightarrow> False
   8.279 -     | Package   \<Rightarrow> (pid (declclass membr)) = pack
   8.280 -     | Protected \<Rightarrow> True
   8.281 -     | Public    \<Rightarrow> True)"
   8.282 +definition
   8.283 +  inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
   8.284 +where
   8.285 +"G\<turnstile>membr inheritable_in pack =
   8.286 +  (case (accmodi membr) of
   8.287 +     Private   \<Rightarrow> False
   8.288 +   | Package   \<Rightarrow> (pid (declclass membr)) = pack
   8.289 +   | Protected \<Rightarrow> True
   8.290 +   | Public    \<Rightarrow> True)"
   8.291  
   8.292  abbreviation
   8.293  Method_inheritable_in_syntax::
   8.294 @@ -526,24 +542,26 @@
   8.295  
   8.296  subsubsection "declared-in/undeclared-in"
   8.297  
   8.298 -definition cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
   8.299 -"cdeclaredmethd G C 
   8.300 -  \<equiv> (case class G C of
   8.301 +definition
   8.302 +  cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
   8.303 +  "cdeclaredmethd G C =
   8.304 +    (case class G C of
   8.305         None \<Rightarrow> \<lambda> sig. None
   8.306 -     | Some c \<Rightarrow> table_of (methods c)
   8.307 -    )"
   8.308 +     | Some c \<Rightarrow> table_of (methods c))"
   8.309  
   8.310 -definition cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
   8.311 -"cdeclaredfield G C 
   8.312 -  \<equiv> (case class G C of
   8.313 -       None \<Rightarrow> \<lambda> sig. None
   8.314 -     | Some c \<Rightarrow> table_of (cfields c)
   8.315 -    )"
   8.316 +definition
   8.317 +  cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
   8.318 +  "cdeclaredfield G C =
   8.319 +    (case class G C of
   8.320 +      None \<Rightarrow> \<lambda> sig. None
   8.321 +    | Some c \<Rightarrow> table_of (cfields c))"
   8.322  
   8.323 -definition declared_in :: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60) where
   8.324 -"G\<turnstile>m declared_in C \<equiv> (case m of
   8.325 -                        fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
   8.326 -                      | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
   8.327 +definition
   8.328 +  declared_in :: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
   8.329 +where
   8.330 +  "G\<turnstile>m declared_in C = (case m of
   8.331 +                          fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
   8.332 +                        | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
   8.333  
   8.334  abbreviation
   8.335  method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   8.336 @@ -560,10 +578,12 @@
   8.337  by (cases m) 
   8.338     (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
   8.339  
   8.340 -definition undeclared_in :: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60) where
   8.341 -"G\<turnstile>m undeclared_in C \<equiv> (case m of
   8.342 -                            fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
   8.343 -                          | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
   8.344 +definition
   8.345 +  undeclared_in :: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
   8.346 +where
   8.347 +  "G\<turnstile>m undeclared_in C = (case m of
   8.348 +                           fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
   8.349 +                         | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
   8.350  
   8.351  
   8.352  subsubsection "members"
   8.353 @@ -607,17 +627,20 @@
   8.354                             ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
   8.355   where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
   8.356  
   8.357 -definition inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60) where
   8.358 -"G\<turnstile>C inherits m 
   8.359 -  \<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
   8.360 -    (\<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)"
   8.361 +definition
   8.362 +  inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60)
   8.363 +where
   8.364 +  "G\<turnstile>C inherits m =
   8.365 +    (G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
   8.366 +      (\<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))"
   8.367  
   8.368  lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
   8.369  by (auto simp add: inherits_def intro: members.Inherited)
   8.370  
   8.371  
   8.372 -definition member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60) where
   8.373 -"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
   8.374 +definition
   8.375 +  member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
   8.376 +  where "G\<turnstile>m member_in C = (\<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC)"
   8.377  text {* A member is in a class if it is member of the class or a superclass.
   8.378  If a member is in a class we can select this member. This additional notion
   8.379  is necessary since not all members are inherited to subclasses. So such
   8.380 @@ -703,13 +726,15 @@
   8.381  
   8.382  subsubsection "Hiding"
   8.383  
   8.384 -definition hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60) where 
   8.385 -"G\<turnstile>new hides old
   8.386 -  \<equiv> is_static new \<and> msig new = msig old \<and>
   8.387 -    G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   8.388 -    G\<turnstile>Method new declared_in (declclass new) \<and>
   8.389 -    G\<turnstile>Method old declared_in (declclass old) \<and> 
   8.390 -    G\<turnstile>Method old inheritable_in pid (declclass new)"
   8.391 +definition
   8.392 +  hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60)
   8.393 +where 
   8.394 +  "G\<turnstile>new hides old =
   8.395 +    (is_static new \<and> msig new = msig old \<and>
   8.396 +      G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   8.397 +      G\<turnstile>Method new declared_in (declclass new) \<and>
   8.398 +      G\<turnstile>Method old declared_in (declclass old) \<and> 
   8.399 +      G\<turnstile>Method old inheritable_in pid (declclass new))"
   8.400  
   8.401  abbreviation
   8.402  sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   8.403 @@ -762,16 +787,18 @@
   8.404  by (auto simp add: hides_def)
   8.405  
   8.406  subsubsection "permits access" 
   8.407 -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
   8.408 -"G\<turnstile>membr in cls permits_acc_from accclass 
   8.409 -  \<equiv> (case (accmodi membr) of
   8.410 -       Private   \<Rightarrow> (declclass membr = accclass)
   8.411 -     | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
   8.412 -     | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
   8.413 +definition
   8.414 +  permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
   8.415 +where
   8.416 +  "G\<turnstile>membr in cls permits_acc_from accclass =
   8.417 +    (case (accmodi membr) of
   8.418 +      Private   \<Rightarrow> (declclass membr = accclass)
   8.419 +    | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
   8.420 +    | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
   8.421                      \<or>
   8.422                      (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
   8.423                       \<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr)) 
   8.424 -     | Public    \<Rightarrow> True)"
   8.425 +    | Public    \<Rightarrow> True)"
   8.426  text {*
   8.427  The subcondition of the @{term "Protected"} case: 
   8.428  @{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
   8.429 @@ -1380,24 +1407,25 @@
   8.430  translations 
   8.431    (type) "fspec" <= (type) "vname \<times> qtname" 
   8.432  
   8.433 -definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   8.434 -"imethds G I 
   8.435 -  \<equiv> iface_rec G I  
   8.436 -              (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
   8.437 +definition
   8.438 +  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   8.439 +  "imethds G I =
   8.440 +    iface_rec G I  (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
   8.441                          (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
   8.442  text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
   8.443  
   8.444 -definition accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   8.445 -"accimethds G pack I
   8.446 -  \<equiv> if G\<turnstile>Iface I accessible_in pack 
   8.447 -       then imethds G I
   8.448 -       else (\<lambda> k. {})"
   8.449 +definition
   8.450 +  accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   8.451 +  "accimethds G pack I =
   8.452 +    (if G\<turnstile>Iface I accessible_in pack 
   8.453 +     then imethds G I
   8.454 +     else (\<lambda> k. {}))"
   8.455  text {* only returns imethds if the interface is accessible *}
   8.456  
   8.457 -definition methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.458 -
   8.459 -"methd G C 
   8.460 - \<equiv> class_rec G C empty
   8.461 +definition
   8.462 +  methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.463 +  "methd G C =
   8.464 +    class_rec G C empty
   8.465               (\<lambda>C c subcls_mthds. 
   8.466                 filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
   8.467                            subcls_mthds 
   8.468 @@ -1409,10 +1437,10 @@
   8.469       Every new method with the same signature coalesces the
   8.470       method of a superclass. *}
   8.471  
   8.472 -definition accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.473 -"accmethd G S C 
   8.474 - \<equiv> filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) 
   8.475 -              (methd G C)"
   8.476 +definition
   8.477 +  accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.478 +  "accmethd G S C =
   8.479 +    filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) (methd G C)"
   8.480  text {* @{term "accmethd G S C"}: only those methods of @{term "methd G C"}, 
   8.481          accessible from S *}
   8.482  
   8.483 @@ -1423,23 +1451,24 @@
   8.484      So we must test accessibility of method @{term m} of class @{term C} 
   8.485      (not @{term "declclass m"}) *}
   8.486  
   8.487 -definition dynmethd :: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.488 -"dynmethd G statC dynC  
   8.489 -  \<equiv> \<lambda> sig. 
   8.490 -     (if G\<turnstile>dynC \<preceq>\<^sub>C statC
   8.491 -        then (case methd G statC sig of
   8.492 -                None \<Rightarrow> None
   8.493 -              | Some statM 
   8.494 -                  \<Rightarrow> (class_rec G dynC empty
   8.495 -                       (\<lambda>C c subcls_mthds. 
   8.496 -                          subcls_mthds
   8.497 -                          ++
   8.498 -                          (filter_tab 
   8.499 -                            (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
   8.500 -                            (methd G C) ))
   8.501 -                      ) sig
   8.502 -              )
   8.503 -        else None)"
   8.504 +definition
   8.505 +  dynmethd :: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.506 +  "dynmethd G statC dynC =
   8.507 +    (\<lambda>sig.
   8.508 +       (if G\<turnstile>dynC \<preceq>\<^sub>C statC
   8.509 +          then (case methd G statC sig of
   8.510 +                  None \<Rightarrow> None
   8.511 +                | Some statM 
   8.512 +                    \<Rightarrow> (class_rec G dynC empty
   8.513 +                         (\<lambda>C c subcls_mthds. 
   8.514 +                            subcls_mthds
   8.515 +                            ++
   8.516 +                            (filter_tab 
   8.517 +                              (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
   8.518 +                              (methd G C) ))
   8.519 +                        ) sig
   8.520 +                )
   8.521 +          else None))"
   8.522  
   8.523  text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference 
   8.524          with dynamic class @{term dynC} and static class @{term statC} *}
   8.525 @@ -1449,11 +1478,12 @@
   8.526          filters the new methods (to get only those methods which actually
   8.527          override the methods of the static class) *}
   8.528  
   8.529 -definition dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.530 -"dynimethd G I dynC 
   8.531 -  \<equiv> \<lambda> sig. if imethds G I sig \<noteq> {}
   8.532 -               then methd G dynC sig
   8.533 -               else dynmethd G Object dynC sig"
   8.534 +definition
   8.535 +  dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.536 +  "dynimethd G I dynC =
   8.537 +    (\<lambda>sig. if imethds G I sig \<noteq> {}
   8.538 +           then methd G dynC sig
   8.539 +           else dynmethd G Object dynC sig)"
   8.540  text {* @{term "dynimethd G I dynC"}: dynamic method lookup of a reference with 
   8.541          dynamic class dynC and static interface type I *}
   8.542  text {* 
   8.543 @@ -1468,31 +1498,34 @@
   8.544     down to the actual dynamic class.
   8.545   *}
   8.546  
   8.547 -definition dynlookup :: "prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.548 -"dynlookup G statT dynC
   8.549 -  \<equiv> (case statT of
   8.550 -       NullT        \<Rightarrow> empty
   8.551 -     | IfaceT I     \<Rightarrow> dynimethd G I      dynC
   8.552 -     | ClassT statC \<Rightarrow> dynmethd  G statC  dynC
   8.553 -     | ArrayT ty    \<Rightarrow> dynmethd  G Object dynC)"
   8.554 +definition
   8.555 +  dynlookup :: "prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   8.556 +  "dynlookup G statT dynC =
   8.557 +    (case statT of
   8.558 +      NullT        \<Rightarrow> empty
   8.559 +    | IfaceT I     \<Rightarrow> dynimethd G I      dynC
   8.560 +    | ClassT statC \<Rightarrow> dynmethd  G statC  dynC
   8.561 +    | ArrayT ty    \<Rightarrow> dynmethd  G Object dynC)"
   8.562  text {* @{term "dynlookup G statT dynC"}: dynamic lookup of a method within the 
   8.563      static reference type statT and the dynamic class dynC. 
   8.564      In a wellformd context statT will not be NullT and in case
   8.565      statT is an array type, dynC=Object *}
   8.566  
   8.567 -definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
   8.568 -"fields G C 
   8.569 -  \<equiv> class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
   8.570 +definition
   8.571 +  fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
   8.572 +  "fields G C =
   8.573 +    class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
   8.574  text {* @{term "fields G C"} 
   8.575       list of fields of a class, including all the fields of the superclasses
   8.576       (private, inherited and hidden ones) not only the accessible ones
   8.577       (an instance of a object allocates all these fields *}
   8.578  
   8.579 -definition accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table" where
   8.580 -"accfield G S C
   8.581 -  \<equiv> let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
   8.582 -    in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
   8.583 -                  field_tab"
   8.584 +definition
   8.585 +  accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table" where
   8.586 +  "accfield G S C =
   8.587 +    (let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
   8.588 +      in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
   8.589 +                    field_tab)"
   8.590  text  {* @{term "accfield G C S"}: fields of a class @{term C} which are 
   8.591           accessible from scope of class
   8.592           @{term S} with inheritance and hiding, cf. 8.3 *}
   8.593 @@ -1503,11 +1536,13 @@
   8.594     inheritance, too. So we must test accessibility of field @{term f} of class 
   8.595     @{term C} (not @{term "declclass f"}) *} 
   8.596  
   8.597 -definition is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool" where
   8.598 - "is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None"
   8.599 +definition
   8.600 +  is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool"
   8.601 +  where "is_methd G = (\<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None)"
   8.602  
   8.603 -definition efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)" where
   8.604 -"efname \<equiv> fst"
   8.605 +definition
   8.606 +  efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)"
   8.607 +  where "efname = fst"
   8.608  
   8.609  lemma efname_simp[simp]:"efname (n,f) = n"
   8.610  by (simp add: efname_def) 
   8.611 @@ -2270,8 +2305,9 @@
   8.612  
   8.613  section "calculation of the superclasses of a class"
   8.614  
   8.615 -definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
   8.616 - "superclasses G C \<equiv> class_rec G C {} 
   8.617 +definition
   8.618 +  superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
   8.619 + "superclasses G C = class_rec G C {} 
   8.620                         (\<lambda> C c superclss. (if C=Object 
   8.621                                              then {} 
   8.622                                              else insert (super c) superclss))"
     9.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Mon Jul 26 13:50:52 2010 +0200
     9.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Mon Jul 26 17:41:26 2010 +0200
     9.3 @@ -49,33 +49,33 @@
     9.4  with a jump, since no breaks, continues or returns are allowed in an 
     9.5  expression. *}
     9.6  
     9.7 -consts jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
     9.8 -primrec
     9.9 -"jumpNestingOkS jmps (Skip)   = True"
    9.10 -"jumpNestingOkS jmps (Expr e) = True"
    9.11 -"jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
    9.12 -"jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
    9.13 -                                 jumpNestingOkS jmps c2)"
    9.14 -"jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
    9.15 -                                           jumpNestingOkS jmps c2)"
    9.16 -"jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
    9.17 +primrec jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
    9.18 +where
    9.19 +  "jumpNestingOkS jmps (Skip)   = True"
    9.20 +| "jumpNestingOkS jmps (Expr e) = True"
    9.21 +| "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
    9.22 +| "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
    9.23 +                                   jumpNestingOkS jmps c2)"
    9.24 +| "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
    9.25 +                                             jumpNestingOkS jmps c2)"
    9.26 +| "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
    9.27  --{* The label of the while loop only handles continue jumps. Breaks are only
    9.28       handled by @{term Lab} *}
    9.29 -"jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
    9.30 -"jumpNestingOkS jmps (Throw e) = True"
    9.31 -"jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
    9.32 -                                                jumpNestingOkS jmps c2)"
    9.33 -"jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
    9.34 -                                        jumpNestingOkS jmps c2)"
    9.35 -"jumpNestingOkS jmps (Init C) = True" 
    9.36 +| "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
    9.37 +| "jumpNestingOkS jmps (Throw e) = True"
    9.38 +| "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
    9.39 +                                                  jumpNestingOkS jmps c2)"
    9.40 +| "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
    9.41 +                                          jumpNestingOkS jmps c2)"
    9.42 +| "jumpNestingOkS jmps (Init C) = True" 
    9.43   --{* wellformedness of the program must enshure that for all initializers 
    9.44        jumpNestingOkS {} holds *} 
    9.45  --{* Dummy analysis for intermediate smallstep term @{term  FinA} *}
    9.46 -"jumpNestingOkS jmps (FinA a c) = False"
    9.47 +| "jumpNestingOkS jmps (FinA a c) = False"
    9.48  
    9.49  
    9.50  definition jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool" where
    9.51 -"jumpNestingOk jmps t \<equiv> (case t of
    9.52 +"jumpNestingOk jmps t = (case t of
    9.53                        In1 se \<Rightarrow> (case se of
    9.54                                     Inl e \<Rightarrow> True
    9.55                                   | Inr s \<Rightarrow> jumpNestingOkS jmps s)
    9.56 @@ -116,48 +116,46 @@
    9.57  
    9.58  subsection {* Very restricted calculation fallback calculation *}
    9.59  
    9.60 -consts the_LVar_name:: "var \<Rightarrow> lname"
    9.61 -primrec 
    9.62 -"the_LVar_name (LVar n) = n"
    9.63 +primrec the_LVar_name :: "var \<Rightarrow> lname"
    9.64 +  where "the_LVar_name (LVar n) = n"
    9.65  
    9.66 -consts assignsE :: "expr      \<Rightarrow> lname set" 
    9.67 -       assignsV :: "var       \<Rightarrow> lname set"
    9.68 -       assignsEs:: "expr list \<Rightarrow> lname set"
    9.69 -text {* *}
    9.70 -primrec
    9.71 -"assignsE (NewC c)            = {}" 
    9.72 -"assignsE (NewA t e)          = assignsE e"
    9.73 -"assignsE (Cast t e)          = assignsE e"
    9.74 -"assignsE (e InstOf r)        = assignsE e"
    9.75 -"assignsE (Lit val)           = {}"
    9.76 -"assignsE (UnOp unop e)       = assignsE e"
    9.77 -"assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
    9.78 -                                     then (assignsE e1)
    9.79 -                                     else (assignsE e1) \<union> (assignsE e2))" 
    9.80 -"assignsE (Super)             = {}"
    9.81 -"assignsE (Acc v)             = assignsV v"
    9.82 -"assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
    9.83 -                                 (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
    9.84 -                                                     else {})"
    9.85 -"assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
    9.86 -"assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
    9.87 -                          = (assignsE objRef) \<union> (assignsEs args)"
    9.88 +primrec assignsE :: "expr \<Rightarrow> lname set" 
    9.89 +  and assignsV :: "var \<Rightarrow> lname set"
    9.90 +  and assignsEs:: "expr list \<Rightarrow> lname set"
    9.91 +where
    9.92 +  "assignsE (NewC c)            = {}" 
    9.93 +| "assignsE (NewA t e)          = assignsE e"
    9.94 +| "assignsE (Cast t e)          = assignsE e"
    9.95 +| "assignsE (e InstOf r)        = assignsE e"
    9.96 +| "assignsE (Lit val)           = {}"
    9.97 +| "assignsE (UnOp unop e)       = assignsE e"
    9.98 +| "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
    9.99 +                                       then (assignsE e1)
   9.100 +                                       else (assignsE e1) \<union> (assignsE e2))" 
   9.101 +| "assignsE (Super)             = {}"
   9.102 +| "assignsE (Acc v)             = assignsV v"
   9.103 +| "assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
   9.104 +                                   (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
   9.105 +                                                       else {})"
   9.106 +| "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
   9.107 +| "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
   9.108 +                            = (assignsE objRef) \<union> (assignsEs args)"
   9.109  -- {* Only dummy analysis for intermediate expressions  
   9.110        @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
   9.111 -"assignsE (Methd C sig)   = {}" 
   9.112 -"assignsE (Body  C s)     = {}"   
   9.113 -"assignsE (InsInitE s e)  = {}"  
   9.114 -"assignsE (Callee l e)    = {}" 
   9.115 +| "assignsE (Methd C sig)   = {}" 
   9.116 +| "assignsE (Body  C s)     = {}"   
   9.117 +| "assignsE (InsInitE s e)  = {}"  
   9.118 +| "assignsE (Callee l e)    = {}" 
   9.119  
   9.120 -"assignsV (LVar n)       = {}"
   9.121 -"assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
   9.122 -"assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
   9.123 +| "assignsV (LVar n)       = {}"
   9.124 +| "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
   9.125 +| "assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
   9.126  
   9.127 -"assignsEs     [] = {}"
   9.128 -"assignsEs (e#es) = assignsE e \<union> assignsEs es"
   9.129 +| "assignsEs     [] = {}"
   9.130 +| "assignsEs (e#es) = assignsE e \<union> assignsEs es"
   9.131  
   9.132  definition assigns :: "term \<Rightarrow> lname set" where
   9.133 -"assigns t \<equiv> (case t of
   9.134 +"assigns t = (case t of
   9.135                  In1 se \<Rightarrow> (case se of
   9.136                               Inl e \<Rightarrow> assignsE e
   9.137                             | Inr s \<Rightarrow> {})
   9.138 @@ -190,42 +188,42 @@
   9.139  
   9.140  subsection "Analysis of constant expressions"
   9.141  
   9.142 -consts constVal :: "expr \<Rightarrow> val option"
   9.143 -primrec 
   9.144 -"constVal (NewC c)      = None"
   9.145 -"constVal (NewA t e)    = None"
   9.146 -"constVal (Cast t e)    = None"
   9.147 -"constVal (Inst e r)    = None"
   9.148 -"constVal (Lit val)     = Some val"
   9.149 -"constVal (UnOp unop e) = (case (constVal e) of
   9.150 -                             None   \<Rightarrow> None
   9.151 -                           | Some v \<Rightarrow> Some (eval_unop unop v))" 
   9.152 -"constVal (BinOp binop e1 e2) = (case (constVal e1) of
   9.153 -                                   None    \<Rightarrow> None
   9.154 -                                 | Some v1 \<Rightarrow> (case (constVal e2) of 
   9.155 -                                                None    \<Rightarrow> None
   9.156 -                                              | Some v2 \<Rightarrow> Some (eval_binop 
   9.157 -                                                                 binop v1 v2)))"
   9.158 -"constVal (Super)         = None"
   9.159 -"constVal (Acc v)         = None"
   9.160 -"constVal (Ass v e)       = None"
   9.161 -"constVal (Cond b e1 e2)  = (case (constVal b) of
   9.162 +primrec constVal :: "expr \<Rightarrow> val option"
   9.163 +where
   9.164 +  "constVal (NewC c)      = None"
   9.165 +| "constVal (NewA t e)    = None"
   9.166 +| "constVal (Cast t e)    = None"
   9.167 +| "constVal (Inst e r)    = None"
   9.168 +| "constVal (Lit val)     = Some val"
   9.169 +| "constVal (UnOp unop e) = (case (constVal e) of
   9.170                                 None   \<Rightarrow> None
   9.171 -                             | Some bv\<Rightarrow> (case the_Bool bv of
   9.172 -                                            True \<Rightarrow> (case (constVal e2) of
   9.173 -                                                       None   \<Rightarrow> None
   9.174 -                                                     | Some v \<Rightarrow> constVal e1)
   9.175 -                                          | False\<Rightarrow> (case (constVal e1) of
   9.176 -                                                       None   \<Rightarrow> None
   9.177 -                                                     | Some v \<Rightarrow> constVal e2)))"
   9.178 +                             | Some v \<Rightarrow> Some (eval_unop unop v))" 
   9.179 +| "constVal (BinOp binop e1 e2) = (case (constVal e1) of
   9.180 +                                     None    \<Rightarrow> None
   9.181 +                                   | Some v1 \<Rightarrow> (case (constVal e2) of 
   9.182 +                                                  None    \<Rightarrow> None
   9.183 +                                                | Some v2 \<Rightarrow> Some (eval_binop 
   9.184 +                                                                   binop v1 v2)))"
   9.185 +| "constVal (Super)         = None"
   9.186 +| "constVal (Acc v)         = None"
   9.187 +| "constVal (Ass v e)       = None"
   9.188 +| "constVal (Cond b e1 e2)  = (case (constVal b) of
   9.189 +                                 None   \<Rightarrow> None
   9.190 +                               | Some bv\<Rightarrow> (case the_Bool bv of
   9.191 +                                              True \<Rightarrow> (case (constVal e2) of
   9.192 +                                                         None   \<Rightarrow> None
   9.193 +                                                       | Some v \<Rightarrow> constVal e1)
   9.194 +                                            | False\<Rightarrow> (case (constVal e1) of
   9.195 +                                                         None   \<Rightarrow> None
   9.196 +                                                       | Some v \<Rightarrow> constVal e2)))"
   9.197  --{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be.
   9.198       It requires that all tree expressions are constant even if we can decide
   9.199       which branch to choose, provided the constant value of @{term b} *}
   9.200 -"constVal (Call accC statT mode objRef mn pTs args) = None"
   9.201 -"constVal (Methd C sig)   = None" 
   9.202 -"constVal (Body  C s)     = None"   
   9.203 -"constVal (InsInitE s e)  = None"  
   9.204 -"constVal (Callee l e)    = None" 
   9.205 +| "constVal (Call accC statT mode objRef mn pTs args) = None"
   9.206 +| "constVal (Methd C sig)   = None" 
   9.207 +| "constVal (Body  C s)     = None"   
   9.208 +| "constVal (InsInitE s e)  = None"  
   9.209 +| "constVal (Callee l e)    = None" 
   9.210  
   9.211  lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]: 
   9.212    assumes const: "constVal e = Some v" and
   9.213 @@ -282,55 +280,55 @@
   9.214  to a specific boolean value. If the expression cannot evaluate to a 
   9.215  @{term Boolean} value UNIV is returned. If we expect true/false the opposite 
   9.216  constant false/true will also lead to UNIV. *}
   9.217 -consts assigns_if:: "bool \<Rightarrow> expr \<Rightarrow> lname set" 
   9.218 -primrec
   9.219 -"assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
   9.220 -"assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
   9.221 -"assigns_if b (Cast t e)          = assigns_if b e" 
   9.222 -"assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
   9.223 -                                                     e is a reference type*}
   9.224 -"assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
   9.225 -"assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
   9.226 -                                         None   \<Rightarrow> (if unop = UNot 
   9.227 -                                                       then assigns_if (\<not>b) e
   9.228 -                                                       else UNIV)
   9.229 -                                       | Some v \<Rightarrow> (if v=Bool b 
   9.230 -                                                       then {} 
   9.231 -                                                       else UNIV))"
   9.232 -"assigns_if b (BinOp binop e1 e2) 
   9.233 -  = (case constVal (BinOp binop e1 e2) of
   9.234 -       None \<Rightarrow> (if binop=CondAnd then
   9.235 -                   (case b of 
   9.236 -                       True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
   9.237 -                    |  False \<Rightarrow> assigns_if False e1 \<inter> 
   9.238 -                                (assigns_if True e1 \<union> assigns_if False e2))
   9.239 -                else
   9.240 -               (if binop=CondOr then
   9.241 -                   (case b of 
   9.242 -                       True  \<Rightarrow> assigns_if True e1 \<inter> 
   9.243 -                                (assigns_if False e1 \<union> assigns_if True e2)
   9.244 -                    |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
   9.245 -                else assignsE e1 \<union> assignsE e2))
   9.246 -     | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
   9.247 +primrec assigns_if :: "bool \<Rightarrow> expr \<Rightarrow> lname set"
   9.248 +where
   9.249 +  "assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
   9.250 +| "assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
   9.251 +| "assigns_if b (Cast t e)          = assigns_if b e" 
   9.252 +| "assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
   9.253 +                                                       e is a reference type*}
   9.254 +| "assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
   9.255 +| "assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
   9.256 +                                           None   \<Rightarrow> (if unop = UNot 
   9.257 +                                                         then assigns_if (\<not>b) e
   9.258 +                                                         else UNIV)
   9.259 +                                         | Some v \<Rightarrow> (if v=Bool b 
   9.260 +                                                         then {} 
   9.261 +                                                         else UNIV))"
   9.262 +| "assigns_if b (BinOp binop e1 e2) 
   9.263 +    = (case constVal (BinOp binop e1 e2) of
   9.264 +         None \<Rightarrow> (if binop=CondAnd then
   9.265 +                     (case b of 
   9.266 +                         True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
   9.267 +                      |  False \<Rightarrow> assigns_if False e1 \<inter> 
   9.268 +                                  (assigns_if True e1 \<union> assigns_if False e2))
   9.269 +                  else
   9.270 +                 (if binop=CondOr then
   9.271 +                     (case b of 
   9.272 +                         True  \<Rightarrow> assigns_if True e1 \<inter> 
   9.273 +                                  (assigns_if False e1 \<union> assigns_if True e2)
   9.274 +                      |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
   9.275 +                  else assignsE e1 \<union> assignsE e2))
   9.276 +       | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
   9.277  
   9.278 -"assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
   9.279 -"assigns_if b (Acc v)      = (assignsV v)"
   9.280 -"assigns_if b (v := e)     = (assignsE (Ass v e))"
   9.281 -"assigns_if b (c? e1 : e2) = (assignsE c) \<union>
   9.282 -                               (case (constVal c) of
   9.283 -                                  None    \<Rightarrow> (assigns_if b e1) \<inter> 
   9.284 -                                             (assigns_if b e2)
   9.285 -                                | Some bv \<Rightarrow> (case the_Bool bv of
   9.286 -                                                True  \<Rightarrow> assigns_if b e1
   9.287 -                                              | False \<Rightarrow> assigns_if b e2))"
   9.288 -"assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
   9.289 -          = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
   9.290 +| "assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
   9.291 +| "assigns_if b (Acc v)      = (assignsV v)"
   9.292 +| "assigns_if b (v := e)     = (assignsE (Ass v e))"
   9.293 +| "assigns_if b (c? e1 : e2) = (assignsE c) \<union>
   9.294 +                                 (case (constVal c) of
   9.295 +                                    None    \<Rightarrow> (assigns_if b e1) \<inter> 
   9.296 +                                               (assigns_if b e2)
   9.297 +                                  | Some bv \<Rightarrow> (case the_Bool bv of
   9.298 +                                                  True  \<Rightarrow> assigns_if b e1
   9.299 +                                                | False \<Rightarrow> assigns_if b e2))"
   9.300 +| "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
   9.301 +            = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
   9.302  -- {* Only dummy analysis for intermediate expressions  
   9.303        @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
   9.304 -"assigns_if b (Methd C sig)   = {}" 
   9.305 -"assigns_if b (Body  C s)     = {}"   
   9.306 -"assigns_if b (InsInitE s e)  = {}"  
   9.307 -"assigns_if b (Callee l e)    = {}" 
   9.308 +| "assigns_if b (Methd C sig)   = {}" 
   9.309 +| "assigns_if b (Body  C s)     = {}"   
   9.310 +| "assigns_if b (InsInitE s e)  = {}"  
   9.311 +| "assigns_if b (Callee l e)    = {}" 
   9.312  
   9.313  lemma assigns_if_const_b_simp:
   9.314    assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
   9.315 @@ -429,14 +427,17 @@
   9.316  
   9.317  subsection {* Lifting set operations to range of tables (map to a set) *}
   9.318  
   9.319 -definition union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65) where
   9.320 - "A \<Rightarrow>\<union> B \<equiv> \<lambda> k. A k \<union> B k"
   9.321 +definition
   9.322 +  union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65)
   9.323 +  where "A \<Rightarrow>\<union> B = (\<lambda> k. A k \<union> B k)"
   9.324  
   9.325 -definition intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71) where
   9.326 - "A \<Rightarrow>\<inter>  B \<equiv> \<lambda> k. A k \<inter> B k"
   9.327 +definition
   9.328 +  intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71)
   9.329 +  where "A \<Rightarrow>\<inter>  B = (\<lambda>k. A k \<inter> B k)"
   9.330  
   9.331 -definition all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40) where 
   9.332 - "A \<Rightarrow>\<union>\<^sub>\<forall> B \<equiv> \<lambda> k. A k \<union> B"
   9.333 +definition
   9.334 +  all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)
   9.335 +  where "(A \<Rightarrow>\<union>\<^sub>\<forall> B) = (\<lambda> k. A k \<union> B)"
   9.336    
   9.337  subsubsection {* Binary union of tables *}
   9.338  
   9.339 @@ -507,16 +508,19 @@
   9.340           brk :: "breakass" --{* Definetly assigned variables for 
   9.341                                  abrupt completion with a break *}
   9.342  
   9.343 -definition rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" where
   9.344 -"rmlab k A \<equiv> \<lambda> x. if x=k then UNIV else A x"
   9.345 +definition
   9.346 +  rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
   9.347 +  where "rmlab k A = (\<lambda>x. if x=k then UNIV else A x)"
   9.348   
   9.349  (*
   9.350 -definition setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
   9.351 -"setbrk b A \<equiv> {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
   9.352 +definition
   9.353 +  setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
   9.354 +  "setbrk b A = {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
   9.355  *)
   9.356  
   9.357 -definition range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80) where 
   9.358 - "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}"
   9.359 +definition
   9.360 +  range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
   9.361 +  where "\<Rightarrow>\<Inter>A = {x |x. \<forall> k. x \<in> A k}"
   9.362  
   9.363  text {*
   9.364  In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"},
    10.1 --- a/src/HOL/Bali/Eval.thy	Mon Jul 26 13:50:52 2010 +0200
    10.2 +++ b/src/HOL/Bali/Eval.thy	Mon Jul 26 17:41:26 2010 +0200
    10.3 @@ -141,7 +141,7 @@
    10.4    where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
    10.5  
    10.6  definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
    10.7 - "undefined3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
    10.8 + "undefined3 = sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
    10.9                       (\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
   10.10  
   10.11  lemma [simp]: "undefined3 (In1l x) = In1 undefined"
   10.12 @@ -159,8 +159,9 @@
   10.13  
   10.14  section "exception throwing and catching"
   10.15  
   10.16 -definition throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
   10.17 - "throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
   10.18 +definition
   10.19 +  throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
   10.20 +  "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
   10.21  
   10.22  lemma throw_def2: 
   10.23   "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
   10.24 @@ -168,8 +169,9 @@
   10.25  apply (simp (no_asm))
   10.26  done
   10.27  
   10.28 -definition fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60) where
   10.29 - "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"
   10.30 +definition
   10.31 +  fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
   10.32 +  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)"
   10.33  
   10.34  lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
   10.35  by (simp add: fits_def)
   10.36 @@ -192,9 +194,10 @@
   10.37  apply iprover
   10.38  done
   10.39  
   10.40 -definition catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
   10.41 - "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
   10.42 -                    G,store s\<turnstile>Addr (the_Loc xc) fits Class C"
   10.43 +definition
   10.44 +  catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
   10.45 +  "G,s\<turnstile>catch C = (\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
   10.46 +                        G,store s\<turnstile>Addr (the_Loc xc) fits Class C)"
   10.47  
   10.48  lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
   10.49  apply (unfold catch_def)
   10.50 @@ -217,9 +220,9 @@
   10.51  apply (simp (no_asm))
   10.52  done
   10.53  
   10.54 -definition new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
   10.55 - "new_xcpt_var vn \<equiv> 
   10.56 -     \<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
   10.57 +definition
   10.58 +  new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
   10.59 +  "new_xcpt_var vn = (\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s))"
   10.60  
   10.61  lemma new_xcpt_var_def2 [simp]: 
   10.62   "new_xcpt_var vn (x,s) = 
   10.63 @@ -232,9 +235,10 @@
   10.64  
   10.65  section "misc"
   10.66  
   10.67 -definition assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
   10.68 - "assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
   10.69 -                   in  (x',if x' = None then s' else s)"
   10.70 +definition
   10.71 +  assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
   10.72 + "assign f v = (\<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
   10.73 +                        in  (x',if x' = None then s' else s))"
   10.74  
   10.75  (*
   10.76  lemma assign_Norm_Norm [simp]: 
   10.77 @@ -293,26 +297,29 @@
   10.78  done
   10.79  *)
   10.80  
   10.81 -definition init_comp_ty :: "ty \<Rightarrow> stmt" where
   10.82 - "init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip"
   10.83 +definition
   10.84 +  init_comp_ty :: "ty \<Rightarrow> stmt"
   10.85 +  where "init_comp_ty T = (if (\<exists>C. T = Class C) then Init (the_Class T) else Skip)"
   10.86  
   10.87  lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
   10.88  apply (unfold init_comp_ty_def)
   10.89  apply (simp (no_asm))
   10.90  done
   10.91  
   10.92 -definition invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
   10.93 - "invocation_class m s a' statT 
   10.94 -    \<equiv> (case m of
   10.95 -         Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
   10.96 -                      then the_Class (RefT statT) 
   10.97 -                      else Object
   10.98 -       | SuperM \<Rightarrow> the_Class (RefT statT)
   10.99 -       | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
  10.100 +definition
  10.101 +  invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
  10.102 + "invocation_class m s a' statT =
  10.103 +    (case m of
  10.104 +       Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
  10.105 +                    then the_Class (RefT statT) 
  10.106 +                    else Object
  10.107 +     | SuperM \<Rightarrow> the_Class (RefT statT)
  10.108 +     | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
  10.109  
  10.110 -definition invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
  10.111 -"invocation_declclass G m s a' statT sig 
  10.112 -   \<equiv> declclass (the (dynlookup G statT 
  10.113 +definition
  10.114 +  invocation_declclass :: "prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
  10.115 +  "invocation_declclass G m s a' statT sig =
  10.116 +    declclass (the (dynlookup G statT
  10.117                                  (invocation_class m s a' statT)
  10.118                                  sig))" 
  10.119    
  10.120 @@ -330,10 +337,11 @@
  10.121                                              else Object)"
  10.122  by (simp add: invocation_class_def)
  10.123  
  10.124 -definition init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
  10.125 -                   state \<Rightarrow> state" where
  10.126 - "init_lvars G C sig mode a' pvs 
  10.127 -   \<equiv> \<lambda> (x,s). 
  10.128 +definition
  10.129 +  init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> state \<Rightarrow> state"
  10.130 +where
  10.131 +  "init_lvars G C sig mode a' pvs =
  10.132 +    (\<lambda>(x,s). 
  10.133        let m = mthd (the (methd G C sig));
  10.134            l = \<lambda> k. 
  10.135                (case k of
  10.136 @@ -343,7 +351,7 @@
  10.137                         | Res    \<Rightarrow> None)
  10.138                 | This 
  10.139                     \<Rightarrow> (if mode=Static then None else Some a'))
  10.140 -      in set_lvars l (if mode = Static then x else np a' x,s)"
  10.141 +      in set_lvars l (if mode = Static then x else np a' x,s))"
  10.142  
  10.143  
  10.144  
  10.145 @@ -364,9 +372,11 @@
  10.146  apply (simp (no_asm) add: Let_def)
  10.147  done
  10.148  
  10.149 -definition body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
  10.150 - "body G C sig \<equiv> let m = the (methd G C sig) 
  10.151 -                 in Body (declclass m) (stmt (mbody (mthd m)))"
  10.152 +definition
  10.153 +  body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
  10.154 + "body G C sig =
  10.155 +    (let m = the (methd G C sig) 
  10.156 +     in Body (declclass m) (stmt (mbody (mthd m))))"
  10.157  
  10.158  lemma body_def2: --{* better suited for simplification *} 
  10.159  "body G C sig = Body  (declclass (the (methd G C sig))) 
  10.160 @@ -377,28 +387,30 @@
  10.161  
  10.162  section "variables"
  10.163  
  10.164 -definition lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar" where
  10.165 - "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
  10.166 +definition
  10.167 +  lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
  10.168 +  where "lvar vn s = (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
  10.169  
  10.170 -definition fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
  10.171 - "fvar C stat fn a' s 
  10.172 -    \<equiv> let (oref,xf) = if stat then (Stat C,id)
  10.173 -                              else (Heap (the_Addr a'),np a');
  10.174 +definition
  10.175 +  fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
  10.176 + "fvar C stat fn a' s =
  10.177 +   (let (oref,xf) = if stat then (Stat C,id)
  10.178 +                            else (Heap (the_Addr a'),np a');
  10.179                    n = Inl (fn,C); 
  10.180                    f = (\<lambda>v. supd (upd_gobj oref n v)) 
  10.181 -      in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
  10.182 +    in ((the (values (the (globs (store s) oref)) n),f),abupd xf s))"
  10.183  
  10.184 -definition avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
  10.185 - "avar G i' a' s 
  10.186 -    \<equiv> let   oref = Heap (the_Addr a'); 
  10.187 -               i = the_Intg i'; 
  10.188 -               n = Inr i;
  10.189 -        (T,k,cs) = the_Arr (globs (store s) oref); 
  10.190 -               f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
  10.191 +definition
  10.192 +  avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
  10.193 +  "avar G i' a' s =
  10.194 +    (let   oref = Heap (the_Addr a'); 
  10.195 +              i = the_Intg i'; 
  10.196 +              n = Inr i;
  10.197 +       (T,k,cs) = the_Arr (globs (store s) oref); 
  10.198 +              f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
  10.199                                             ArrStore x
  10.200                                ,upd_gobj oref n v s)) 
  10.201 -      in ((the (cs n),f)
  10.202 -         ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
  10.203 +     in ((the (cs n),f),abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s))"
  10.204  
  10.205  lemma fvar_def2: --{* better suited for simplification *} 
  10.206  "fvar C stat fn a' s =  
  10.207 @@ -431,27 +443,29 @@
  10.208  apply (simp (no_asm) add: Let_def split_beta)
  10.209  done
  10.210  
  10.211 -definition check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
  10.212 -"check_field_access G accC statDeclC fn stat a' s
  10.213 - \<equiv> let oref = if stat then Stat statDeclC
  10.214 -                      else Heap (the_Addr a');
  10.215 -       dynC = case oref of
  10.216 +definition
  10.217 +  check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
  10.218 +  "check_field_access G accC statDeclC fn stat a' s =
  10.219 +    (let oref = if stat then Stat statDeclC
  10.220 +                else Heap (the_Addr a');
  10.221 +         dynC = case oref of
  10.222                     Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
  10.223                   | Stat C \<Rightarrow> C;
  10.224 -       f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
  10.225 -   in abupd 
  10.226 +         f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
  10.227 +     in abupd 
  10.228          (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
  10.229                    AccessViolation)
  10.230 -        s"
  10.231 +        s)"
  10.232  
  10.233 -definition check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
  10.234 -"check_method_access G accC statT mode sig  a' s
  10.235 - \<equiv> let invC = invocation_class mode (store s) a' statT;
  10.236 +definition
  10.237 +  check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
  10.238 +  "check_method_access G accC statT mode sig  a' s =
  10.239 +    (let invC = invocation_class mode (store s) a' statT;
  10.240         dynM = the (dynlookup G statT invC sig)
  10.241 -   in abupd 
  10.242 +     in abupd 
  10.243          (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
  10.244                    AccessViolation)
  10.245 -        s"
  10.246 +        s)"
  10.247         
  10.248  section "evaluation judgments"
  10.249  
    11.1 --- a/src/HOL/Bali/Example.thy	Mon Jul 26 13:50:52 2010 +0200
    11.2 +++ b/src/HOL/Bali/Example.thy	Mon Jul 26 17:41:26 2010 +0200
    11.3 @@ -70,22 +70,21 @@
    11.4  datatype vnam'  = arr' | vee' | z' | e'
    11.5  datatype label' = lab1'
    11.6  
    11.7 -consts
    11.8 -
    11.9 -  tnam' :: "tnam'  \<Rightarrow> tnam"
   11.10 -  vnam' :: "vnam'  \<Rightarrow> vname"
   11.11 +axiomatization
   11.12 +  tnam' :: "tnam'  \<Rightarrow> tnam" and
   11.13 +  vnam' :: "vnam'  \<Rightarrow> vname" and
   11.14    label':: "label' \<Rightarrow> label"
   11.15 -axioms  (** tnam', vnam' and label are intended to be isomorphic 
   11.16 +where
   11.17 +  (** tnam', vnam' and label are intended to be isomorphic 
   11.18              to tnam, vname and label **)
   11.19  
   11.20 -  inj_tnam'  [simp]: "(tnam'  x = tnam'  y) = (x = y)"
   11.21 -  inj_vnam'  [simp]: "(vnam'  x = vnam'  y) = (x = y)"
   11.22 -  inj_label' [simp]: "(label' x = label' y) = (x = y)"
   11.23 -  
   11.24 -  
   11.25 -  surj_tnam':  "\<exists>m. n = tnam'  m"
   11.26 -  surj_vnam':  "\<exists>m. n = vnam'  m"
   11.27 -  surj_label':" \<exists>m. n = label' m"
   11.28 +  inj_tnam'  [simp]: "\<And>x y. (tnam'  x = tnam'  y) = (x = y)" and
   11.29 +  inj_vnam'  [simp]: "\<And>x y. (vnam'  x = vnam'  y) = (x = y)" and
   11.30 +  inj_label' [simp]: "\<And>x y. (label' x = label' y) = (x = y)" and
   11.31 +    
   11.32 +  surj_tnam':  "\<And>n. \<exists>m. n = tnam'  m" and
   11.33 +  surj_vnam':  "\<And>n. \<exists>m. n = vnam'  m" and
   11.34 +  surj_label':" \<And>n. \<exists>m. n = label' m"
   11.35  
   11.36  abbreviation
   11.37    HasFoo :: qtname where
   11.38 @@ -149,22 +148,24 @@
   11.39    Object_mdecls_def: "Object_mdecls \<equiv> []"
   11.40    SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
   11.41  
   11.42 -consts
   11.43 -  
   11.44 +axiomatization  
   11.45    foo    :: mname
   11.46  
   11.47 -definition foo_sig :: sig
   11.48 - where "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
   11.49 +definition
   11.50 +  foo_sig :: sig
   11.51 +  where "foo_sig = \<lparr>name=foo,parTs=[Class Base]\<rparr>"
   11.52    
   11.53 -definition foo_mhead :: mhead
   11.54 - where "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
   11.55 +definition
   11.56 +  foo_mhead :: mhead
   11.57 +  where "foo_mhead = \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
   11.58  
   11.59 -definition Base_foo :: mdecl
   11.60 - where "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
   11.61 +definition
   11.62 +  Base_foo :: mdecl
   11.63 +  where "Base_foo = (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
   11.64                          mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
   11.65  
   11.66  definition Ext_foo :: mdecl
   11.67 - where "Ext_foo  \<equiv> (foo_sig, 
   11.68 +  where "Ext_foo = (foo_sig, 
   11.69                \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
   11.70                 mbody=\<lparr>lcls=[]
   11.71                       ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
   11.72 @@ -172,11 +173,13 @@
   11.73                                  Return (Lit Null)\<rparr>
   11.74                \<rparr>)"
   11.75  
   11.76 -definition arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var" where
   11.77 -"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
   11.78 +definition
   11.79 +  arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
   11.80 +  where "arr_viewed_from accC C = {accC,Base,True}StatRef (ClassT C)..arr"
   11.81  
   11.82 -definition BaseCl :: "class" where
   11.83 -"BaseCl \<equiv> \<lparr>access=Public,
   11.84 +definition
   11.85 +  BaseCl :: "class" where
   11.86 +  "BaseCl = \<lparr>access=Public,
   11.87             cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
   11.88                      (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
   11.89             methods=[Base_foo],
   11.90 @@ -185,16 +188,18 @@
   11.91             super=Object,
   11.92             superIfs=[HasFoo]\<rparr>"
   11.93    
   11.94 -definition ExtCl  :: "class" where
   11.95 -"ExtCl  \<equiv> \<lparr>access=Public,
   11.96 +definition
   11.97 +  ExtCl  :: "class" where
   11.98 +  "ExtCl = \<lparr>access=Public,
   11.99             cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
  11.100             methods=[Ext_foo],
  11.101             init=Skip,
  11.102             super=Base,
  11.103             superIfs=[]\<rparr>"
  11.104  
  11.105 -definition MainCl :: "class" where
  11.106 -"MainCl \<equiv> \<lparr>access=Public,
  11.107 +definition
  11.108 +  MainCl :: "class" where
  11.109 +  "MainCl = \<lparr>access=Public,
  11.110             cfields=[], 
  11.111             methods=[], 
  11.112             init=Skip,
  11.113 @@ -202,14 +207,17 @@
  11.114             superIfs=[]\<rparr>"
  11.115  (* The "main" method is modeled seperately (see tprg) *)
  11.116  
  11.117 -definition HasFooInt :: iface
  11.118 - where "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
  11.119 +definition
  11.120 +  HasFooInt :: iface
  11.121 +  where "HasFooInt = \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
  11.122  
  11.123 -definition Ifaces ::"idecl list"
  11.124 - where "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
  11.125 +definition
  11.126 +  Ifaces ::"idecl list"
  11.127 +  where "Ifaces = [(HasFoo,HasFooInt)]"
  11.128  
  11.129 -definition "Classes" ::"cdecl list"
  11.130 - where "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
  11.131 +definition
  11.132 +  "Classes" ::"cdecl list"
  11.133 +  where "Classes = [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
  11.134  
  11.135  lemmas table_classes_defs = 
  11.136       Classes_def standard_classes_def ObjectC_def SXcptC_def
  11.137 @@ -264,12 +272,13 @@
  11.138    tprg :: prog where
  11.139    "tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
  11.140  
  11.141 -definition test :: "(ty)list \<Rightarrow> stmt" where
  11.142 - "test pTs \<equiv> e:==NewC Ext;; 
  11.143 +definition
  11.144 +  test :: "(ty)list \<Rightarrow> stmt" where
  11.145 +  "test pTs = (e:==NewC Ext;; 
  11.146             \<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
  11.147             \<spacespace> Catch((SXcpt NullPointer) z)
  11.148             (lab1\<bullet> While(Acc 
  11.149 -                        (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)"
  11.150 +                        (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip))"
  11.151  
  11.152  
  11.153  section "well-structuredness"
  11.154 @@ -1185,9 +1194,9 @@
  11.155           rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
  11.156  lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
  11.157  
  11.158 -consts
  11.159 -  a :: loc
  11.160 -  b :: loc
  11.161 +axiomatization
  11.162 +  a :: loc and
  11.163 +  b :: loc and
  11.164    c :: loc
  11.165  
  11.166  abbreviation "one == Suc 0"
    12.1 --- a/src/HOL/Bali/Name.thy	Mon Jul 26 13:50:52 2010 +0200
    12.2 +++ b/src/HOL/Bali/Name.thy	Mon Jul 26 17:41:26 2010 +0200
    12.3 @@ -68,14 +68,14 @@
    12.4  begin
    12.5  
    12.6  definition
    12.7 -  tname_tname_def: "tname (t::tname) \<equiv> t"
    12.8 +  tname_tname_def: "tname (t::tname) = t"
    12.9  
   12.10  instance ..
   12.11  
   12.12  end
   12.13  
   12.14  definition
   12.15 -  qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
   12.16 +  qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
   12.17  
   12.18  translations
   12.19    (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
   12.20 @@ -84,16 +84,17 @@
   12.21  
   12.22  axiomatization java_lang::pname --{* package java.lang *}
   12.23  
   12.24 -consts 
   12.25 +definition
   12.26    Object :: qtname
   12.27 -  SXcpt  :: "xname \<Rightarrow> qtname"
   12.28 -defs
   12.29 -  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
   12.30 -  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
   12.31 +  where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>"
   12.32 +
   12.33 +definition SXcpt :: "xname \<Rightarrow> qtname"
   12.34 +  where "SXcpt = (\<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)"
   12.35  
   12.36  lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
   12.37  by (simp add: Object_def SXcpt_def)
   12.38  
   12.39  lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
   12.40  by (simp add: SXcpt_def)
   12.41 +
   12.42  end
    13.1 --- a/src/HOL/Bali/State.thy	Mon Jul 26 13:50:52 2010 +0200
    13.2 +++ b/src/HOL/Bali/State.thy	Mon Jul 26 17:41:26 2010 +0200
    13.3 @@ -38,8 +38,9 @@
    13.4    (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
    13.5    (type) "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
    13.6  
    13.7 -definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
    13.8 - "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
    13.9 +definition
   13.10 +  the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table"
   13.11 +  where "the_Arr obj = (SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>)"
   13.12  
   13.13  lemma the_Arr_Arr [simp]: "the_Arr (Some \<lparr>tag=Arr T k,values=cs\<rparr>) = (T,k,cs)"
   13.14  apply (auto simp: the_Arr_def)
   13.15 @@ -50,18 +51,20 @@
   13.16  apply (auto simp add: the_Arr_def)
   13.17  done
   13.18  
   13.19 -definition upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj" where 
   13.20 - "upd_obj n v \<equiv> \<lambda> obj . obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>"
   13.21 +definition
   13.22 +  upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj"
   13.23 +  where "upd_obj n v = (\<lambda>obj. obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>)"
   13.24  
   13.25  lemma upd_obj_def2 [simp]: 
   13.26    "upd_obj n v obj = obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>" 
   13.27  apply (auto simp: upd_obj_def)
   13.28  done
   13.29  
   13.30 -definition obj_ty :: "obj \<Rightarrow> ty" where
   13.31 - "obj_ty obj    \<equiv> case tag obj of 
   13.32 -                    CInst C \<Rightarrow> Class C 
   13.33 -                  | Arr T k \<Rightarrow> T.[]"
   13.34 +definition
   13.35 +  obj_ty :: "obj \<Rightarrow> ty" where
   13.36 +  "obj_ty obj = (case tag obj of 
   13.37 +                  CInst C \<Rightarrow> Class C 
   13.38 +                | Arr T k \<Rightarrow> T.[])"
   13.39  
   13.40  lemma obj_ty_eq [intro!]: "obj_ty \<lparr>tag=oi,values=x\<rparr> = obj_ty \<lparr>tag=oi,values=y\<rparr>" 
   13.41  by (simp add: obj_ty_def)
   13.42 @@ -97,10 +100,11 @@
   13.43  apply (auto split add: obj_tag.split_asm)
   13.44  done
   13.45  
   13.46 -definition obj_class :: "obj \<Rightarrow> qtname" where
   13.47 - "obj_class obj \<equiv> case tag obj of 
   13.48 -                    CInst C \<Rightarrow> C 
   13.49 -                  | Arr T k \<Rightarrow> Object"
   13.50 +definition
   13.51 +  obj_class :: "obj \<Rightarrow> qtname" where
   13.52 +  "obj_class obj = (case tag obj of 
   13.53 +                     CInst C \<Rightarrow> C 
   13.54 +                   | Arr T k \<Rightarrow> Object)"
   13.55  
   13.56  
   13.57  lemma obj_class_CInst [simp]: "obj_class \<lparr>tag=CInst C,values=vs\<rparr> = C" 
   13.58 @@ -136,9 +140,10 @@
   13.59    "Stat" => "CONST Inr"
   13.60    (type) "oref" <= (type) "loc + qtname"
   13.61  
   13.62 -definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
   13.63 - "fields_table G C P 
   13.64 -    \<equiv> Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
   13.65 +definition
   13.66 +  fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
   13.67 +  "fields_table G C P =
   13.68 +    Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
   13.69  
   13.70  lemma fields_table_SomeI: 
   13.71  "\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 
   13.72 @@ -173,20 +178,23 @@
   13.73  apply simp
   13.74  done
   13.75  
   13.76 -definition in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50) where
   13.77 - "i in_bounds k \<equiv> 0 \<le> i \<and> i < k"
   13.78 +definition
   13.79 +  in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50)
   13.80 +  where "i in_bounds k = (0 \<le> i \<and> i < k)"
   13.81  
   13.82 -definition arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option" where
   13.83 - "arr_comps T k \<equiv> \<lambda>i. if i in_bounds k then Some T else None"
   13.84 +definition
   13.85 +  arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option"
   13.86 +  where "arr_comps T k = (\<lambda>i. if i in_bounds k then Some T else None)"
   13.87    
   13.88 -definition var_tys       :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where
   13.89 -"var_tys G oi r 
   13.90 -  \<equiv> case r of 
   13.91 +definition
   13.92 +  var_tys :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where
   13.93 +  "var_tys G oi r =
   13.94 +    (case r of 
   13.95        Heap a \<Rightarrow> (case oi of 
   13.96                     CInst C \<Rightarrow> fields_table G C (\<lambda>n f. \<not>static f) (+) empty
   13.97                   | Arr T k \<Rightarrow> empty (+) arr_comps T k)
   13.98      | Stat C \<Rightarrow> fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) 
   13.99 -                (+) empty"
  13.100 +                (+) empty)"
  13.101  
  13.102  lemma var_tys_Some_eq: 
  13.103   "var_tys G oi r n = Some T 
  13.104 @@ -222,14 +230,16 @@
  13.105  
  13.106  subsection "access"
  13.107  
  13.108 -definition globs :: "st \<Rightarrow> globs" where
  13.109 - "globs  \<equiv> st_case (\<lambda>g l. g)"
  13.110 +definition
  13.111 +  globs :: "st \<Rightarrow> globs"
  13.112 +  where "globs = st_case (\<lambda>g l. g)"
  13.113    
  13.114 -definition locals :: "st \<Rightarrow> locals" where
  13.115 - "locals \<equiv> st_case (\<lambda>g l. l)"
  13.116 +definition
  13.117 +  locals :: "st \<Rightarrow> locals"
  13.118 +  where "locals = st_case (\<lambda>g l. l)"
  13.119  
  13.120 -definition heap   :: "st \<Rightarrow> heap" where
  13.121 - "heap s \<equiv> globs s \<circ> Heap"
  13.122 +definition heap :: "st \<Rightarrow> heap" where
  13.123 + "heap s = globs s \<circ> Heap"
  13.124  
  13.125  
  13.126  lemma globs_def2 [simp]: " globs (st g l) = g"
  13.127 @@ -250,8 +260,9 @@
  13.128  
  13.129  subsection "memory allocation"
  13.130  
  13.131 -definition new_Addr :: "heap \<Rightarrow> loc option" where
  13.132 - "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)"
  13.133 +definition
  13.134 +  new_Addr :: "heap \<Rightarrow> loc option" where
  13.135 +  "new_Addr h = (if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None))"
  13.136  
  13.137  lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
  13.138  apply (auto simp add: new_Addr_def)
  13.139 @@ -290,20 +301,25 @@
  13.140  
  13.141  subsection "update"
  13.142  
  13.143 -definition gupd :: "oref  \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')"[10,10]1000) where
  13.144 - "gupd r obj  \<equiv> st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
  13.145 +definition
  13.146 +  gupd :: "oref  \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')" [10, 10] 1000)
  13.147 +  where "gupd r obj = st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
  13.148  
  13.149 -definition lupd       :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')"[10,10]1000) where
  13.150 - "lupd vn v   \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
  13.151 +definition
  13.152 +  lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')" [10, 10] 1000)
  13.153 +  where "lupd vn v = st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
  13.154  
  13.155 -definition upd_gobj   :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" where
  13.156 - "upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
  13.157 +definition
  13.158 +  upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
  13.159 +  where "upd_gobj r n v = st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
  13.160  
  13.161 -definition set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st" where
  13.162 - "set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
  13.163 +definition
  13.164 +  set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st"
  13.165 +  where "set_locals l = st_case (\<lambda>g l'. st g l)"
  13.166  
  13.167 -definition init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st" where
  13.168 - "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
  13.169 +definition
  13.170 +  init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
  13.171 +  where "init_obj G oi r = gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
  13.172  
  13.173  abbreviation
  13.174    init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
  13.175 @@ -447,23 +463,22 @@
  13.176  
  13.177  
  13.178  
  13.179 -consts
  13.180 +primrec the_Xcpt :: "abrupt \<Rightarrow> xcpt"
  13.181 +  where "the_Xcpt (Xcpt x) = x"
  13.182  
  13.183 -  the_Xcpt :: "abrupt \<Rightarrow> xcpt"
  13.184 -  the_Jump :: "abrupt => jump"
  13.185 -  the_Loc  :: "xcpt \<Rightarrow> loc"
  13.186 -  the_Std  :: "xcpt \<Rightarrow> xname"
  13.187 +primrec the_Jump :: "abrupt => jump"
  13.188 +  where "the_Jump (Jump j) = j"
  13.189  
  13.190 -primrec "the_Xcpt (Xcpt x) = x"
  13.191 -primrec "the_Jump (Jump j) = j"
  13.192 -primrec "the_Loc (Loc a) = a"
  13.193 -primrec "the_Std (Std x) = x"
  13.194 +primrec the_Loc :: "xcpt \<Rightarrow> loc"
  13.195 +  where "the_Loc (Loc a) = a"
  13.196  
  13.197 -
  13.198 +primrec the_Std :: "xcpt \<Rightarrow> xname"
  13.199 +  where "the_Std (Std x) = x"
  13.200          
  13.201  
  13.202 -definition abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt" where
  13.203 - "abrupt_if c x' x \<equiv> if c \<and> (x = None) then x' else x"
  13.204 +definition
  13.205 +  abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt"
  13.206 +  where "abrupt_if c x' x = (if c \<and> (x = None) then x' else x)"
  13.207  
  13.208  lemma abrupt_if_True_None [simp]: "abrupt_if True x None = x"
  13.209  by (simp add: abrupt_if_def)
  13.210 @@ -542,8 +557,9 @@
  13.211  apply auto
  13.212  done
  13.213  
  13.214 -definition absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt" where
  13.215 -  "absorb j a \<equiv> if a=Some (Jump j) then None else a"
  13.216 +definition
  13.217 +  absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt"
  13.218 +  where "absorb j a = (if a=Some (Jump j) then None else a)"
  13.219  
  13.220  lemma absorb_SomeD [dest!]: "absorb j a = Some x \<Longrightarrow> a = Some x"
  13.221  by (auto simp add: absorb_def)
  13.222 @@ -593,16 +609,18 @@
  13.223  apply clarsimp
  13.224  done
  13.225  
  13.226 -definition normal :: "state \<Rightarrow> bool" where
  13.227 - "normal \<equiv> \<lambda>s. abrupt s = None"
  13.228 +definition
  13.229 +  normal :: "state \<Rightarrow> bool"
  13.230 +  where "normal = (\<lambda>s. abrupt s = None)"
  13.231  
  13.232  lemma normal_def2 [simp]: "normal s = (abrupt s = None)"
  13.233  apply (unfold normal_def)
  13.234  apply (simp (no_asm))
  13.235  done
  13.236  
  13.237 -definition heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool" where
  13.238 - "heap_free n \<equiv> \<lambda>s. atleast_free (heap (store s)) n"
  13.239 +definition
  13.240 +  heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool"
  13.241 +  where "heap_free n = (\<lambda>s. atleast_free (heap (store s)) n)"
  13.242  
  13.243  lemma heap_free_def2 [simp]: "heap_free n s = atleast_free (heap (store s)) n"
  13.244  apply (unfold heap_free_def)
  13.245 @@ -611,11 +629,13 @@
  13.246  
  13.247  subsection "update"
  13.248  
  13.249 -definition abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state" where
  13.250 - "abupd f \<equiv> prod_fun f id"
  13.251 +definition
  13.252 +  abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
  13.253 +  where "abupd f = prod_fun f id"
  13.254  
  13.255 -definition supd     :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state" where
  13.256 - "supd \<equiv> prod_fun id"
  13.257 +definition
  13.258 +  supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
  13.259 +  where "supd = prod_fun id"
  13.260    
  13.261  lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
  13.262  by (simp add: abupd_def)
  13.263 @@ -669,11 +689,13 @@
  13.264  
  13.265  section "initialisation test"
  13.266  
  13.267 -definition inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool" where
  13.268 - "inited C g \<equiv> g (Stat C) \<noteq> None"
  13.269 +definition
  13.270 +  inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool"
  13.271 +  where "inited C g = (g (Stat C) \<noteq> None)"
  13.272  
  13.273 -definition initd    :: "qtname \<Rightarrow> state \<Rightarrow> bool" where
  13.274 - "initd C \<equiv> inited C \<circ> globs \<circ> store"
  13.275 +definition
  13.276 +  initd :: "qtname \<Rightarrow> state \<Rightarrow> bool"
  13.277 +  where "initd C = inited C \<circ> globs \<circ> store"
  13.278  
  13.279  lemma not_inited_empty [simp]: "\<not>inited C empty"
  13.280  apply (unfold inited_def)
  13.281 @@ -706,8 +728,10 @@
  13.282  done
  13.283  
  13.284  section {* @{text error_free} *}
  13.285 -definition error_free :: "state \<Rightarrow> bool" where
  13.286 -"error_free s \<equiv> \<not> (\<exists> err. abrupt s = Some (Error err))"
  13.287 +
  13.288 +definition
  13.289 +  error_free :: "state \<Rightarrow> bool"
  13.290 +  where "error_free s = (\<not> (\<exists> err. abrupt s = Some (Error err)))"
  13.291  
  13.292  lemma error_free_Norm [simp,intro]: "error_free (Norm s)"
  13.293  by (simp add: error_free_def)
    14.1 --- a/src/HOL/Bali/Table.thy	Mon Jul 26 13:50:52 2010 +0200
    14.2 +++ b/src/HOL/Bali/Table.thy	Mon Jul 26 17:41:26 2010 +0200
    14.3 @@ -54,15 +54,15 @@
    14.4  
    14.5  --{* when merging tables old and new, only override an entry of table old when  
    14.6     the condition cond holds *}
    14.7 -"cond_override cond old new \<equiv>
    14.8 - \<lambda> k.
    14.9 +"cond_override cond old new =
   14.10 + (\<lambda>k.
   14.11    (case new k of
   14.12       None         \<Rightarrow> old k                       
   14.13     | Some new_val \<Rightarrow> (case old k of
   14.14                          None         \<Rightarrow> Some new_val          
   14.15                        | Some old_val \<Rightarrow> (if cond new_val old_val
   14.16                                           then Some new_val     
   14.17 -                                         else Some old_val)))"
   14.18 +                                         else Some old_val))))"
   14.19  
   14.20  lemma cond_override_empty1[simp]: "cond_override c empty t = t"
   14.21  by (simp add: cond_override_def expand_fun_eq)
   14.22 @@ -95,10 +95,11 @@
   14.23  
   14.24  section {* Filter on Tables *}
   14.25  
   14.26 -definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
   14.27 -"filter_tab c t \<equiv> \<lambda> k. (case t k of 
   14.28 +definition
   14.29 +  filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
   14.30 +  "filter_tab c t = (\<lambda>k. (case t k of 
   14.31                             None   \<Rightarrow> None
   14.32 -                         | Some x \<Rightarrow> if c k x then Some x else None)"
   14.33 +                         | Some x \<Rightarrow> if c k x then Some x else None))"
   14.34  
   14.35  lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
   14.36  by (simp add: filter_tab_def empty_def)
   14.37 @@ -279,27 +280,31 @@
   14.38  done
   14.39  
   14.40  
   14.41 -consts
   14.42 -  Un_tables      :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
   14.43 -  overrides_t    :: "('a, 'b) tables     \<Rightarrow> ('a, 'b) tables \<Rightarrow>
   14.44 -                     ('a, 'b) tables"             (infixl "\<oplus>\<oplus>" 100)
   14.45 -  hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> 
   14.46 -                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hidings _ entails _" 20)
   14.47 +definition
   14.48 +  Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
   14.49 +  where "Un_tables ts\<spacespace>\<spacespace>= (\<lambda>k. \<Union>t\<in>ts. t k)"
   14.50 +
   14.51 +definition
   14.52 +  overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables"  (infixl "\<oplus>\<oplus>" 100)
   14.53 +  where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)"
   14.54 +
   14.55 +definition
   14.56 +  hidings_entails :: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
   14.57 +    ("_ hidings _ entails _" 20)
   14.58 +  where "(t hidings s entails R) = (\<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y)"
   14.59 +
   14.60 +definition
   14.61    --{* variant for unique table: *}
   14.62 -  hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> 
   14.63 -                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hiding _ entails _"  20)
   14.64 +  hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
   14.65 +    ("_ hiding _ entails _"  20)
   14.66 +  where "(t hiding  s entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y)"
   14.67 +
   14.68 +definition
   14.69    --{* variant for a unique table and conditional overriding: *}
   14.70    cond_hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  
   14.71                            \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"  
   14.72                            ("_ hiding _ under _ entails _"  20)
   14.73 -
   14.74 -defs
   14.75 -  Un_tables_def:       "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k"
   14.76 -  overrides_t_def:     "s \<oplus>\<oplus> t        \<equiv> \<lambda>k. if t k = {} then s k else t k"
   14.77 -  hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y"
   14.78 -  hiding_entails_def:  "t hiding  s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y"
   14.79 -  cond_hiding_entails_def: "t hiding  s under C entails R
   14.80 -                            \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y"
   14.81 +  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)"
   14.82  
   14.83  section "Untables"
   14.84  
   14.85 @@ -383,12 +388,10 @@
   14.86  
   14.87  
   14.88  (*###TO Map?*)
   14.89 -consts
   14.90 -  atleast_free :: "('a ~=> 'b) => nat => bool"
   14.91 -primrec
   14.92 - "atleast_free m 0       = True"
   14.93 - atleast_free_Suc: 
   14.94 - "atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
   14.95 +primrec atleast_free :: "('a ~=> 'b) => nat => bool"
   14.96 +where
   14.97 +  "atleast_free m 0 = True"
   14.98 +| atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a|->b)) n))"
   14.99  
  14.100  lemma atleast_free_weaken [rule_format (no_asm)]: 
  14.101    "!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
    15.1 --- a/src/HOL/Bali/Term.thy	Mon Jul 26 13:50:52 2010 +0200
    15.2 +++ b/src/HOL/Bali/Term.thy	Mon Jul 26 17:41:26 2010 +0200
    15.3 @@ -258,8 +258,9 @@
    15.4    StatRef :: "ref_ty \<Rightarrow> expr"
    15.5    where "StatRef rt == Cast (RefT rt) (Lit Null)"
    15.6    
    15.7 -definition is_stmt :: "term \<Rightarrow> bool" where
    15.8 - "is_stmt t \<equiv> \<exists>c. t=In1r c"
    15.9 +definition
   15.10 +  is_stmt :: "term \<Rightarrow> bool"
   15.11 +  where "is_stmt t = (\<exists>c. t=In1r c)"
   15.12  
   15.13  ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
   15.14  
   15.15 @@ -307,7 +308,7 @@
   15.16  begin
   15.17  
   15.18  definition
   15.19 -  stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
   15.20 +  stmt_inj_term_def: "\<langle>c::stmt\<rangle> = In1r c"
   15.21  
   15.22  instance ..
   15.23  
   15.24 @@ -323,7 +324,7 @@
   15.25  begin
   15.26  
   15.27  definition
   15.28 -  expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
   15.29 +  expr_inj_term_def: "\<langle>e::expr\<rangle> = In1l e"
   15.30  
   15.31  instance ..
   15.32  
   15.33 @@ -339,7 +340,7 @@
   15.34  begin
   15.35  
   15.36  definition
   15.37 -  var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
   15.38 +  var_inj_term_def: "\<langle>v::var\<rangle> = In2 v"
   15.39  
   15.40  instance ..
   15.41  
   15.42 @@ -368,7 +369,7 @@
   15.43  begin
   15.44  
   15.45  definition
   15.46 -  "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
   15.47 +  "\<langle>es::'a list\<rangle> = In3 (map expr_of es)"
   15.48  
   15.49  instance ..
   15.50  
   15.51 @@ -425,46 +426,47 @@
   15.52    done
   15.53  
   15.54  section {* Evaluation of unary operations *}
   15.55 -consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
   15.56 -primrec
   15.57 -"eval_unop UPlus   v = Intg (the_Intg v)"
   15.58 -"eval_unop UMinus  v = Intg (- (the_Intg v))"
   15.59 -"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
   15.60 -"eval_unop UNot    v = Bool (\<not> the_Bool v)"
   15.61 +primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
   15.62 +where
   15.63 +  "eval_unop UPlus v = Intg (the_Intg v)"
   15.64 +| "eval_unop UMinus v = Intg (- (the_Intg v))"
   15.65 +| "eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
   15.66 +| "eval_unop UNot v = Bool (\<not> the_Bool v)"
   15.67  
   15.68  section {* Evaluation of binary operations *}
   15.69 -consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
   15.70 -primrec
   15.71 -"eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
   15.72 -"eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
   15.73 -"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
   15.74 -"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
   15.75 -"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
   15.76 +primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
   15.77 +where
   15.78 +  "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
   15.79 +| "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
   15.80 +| "eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
   15.81 +| "eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
   15.82 +| "eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
   15.83  
   15.84  -- "Be aware of the explicit coercion of the shift distance to nat"
   15.85 -"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
   15.86 -"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
   15.87 -"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
   15.88 +| "eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
   15.89 +| "eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
   15.90 +| "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
   15.91  
   15.92 -"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
   15.93 -"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
   15.94 -"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
   15.95 -"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
   15.96 +| "eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
   15.97 +| "eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
   15.98 +| "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
   15.99 +| "eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
  15.100  
  15.101 -"eval_binop Eq      v1 v2 = Bool (v1=v2)"
  15.102 -"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
  15.103 -"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
  15.104 -"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
  15.105 -"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
  15.106 -"eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
  15.107 -"eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
  15.108 -"eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
  15.109 -"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
  15.110 -"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
  15.111 +| "eval_binop Eq      v1 v2 = Bool (v1=v2)"
  15.112 +| "eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
  15.113 +| "eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
  15.114 +| "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
  15.115 +| "eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
  15.116 +| "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
  15.117 +| "eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
  15.118 +| "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
  15.119 +| "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
  15.120 +| "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
  15.121  
  15.122 -definition need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
  15.123 -"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
  15.124 -                               (binop=CondOr  \<and> the_Bool v1))"
  15.125 +definition
  15.126 +  need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
  15.127 +  "need_second_arg binop v1 = (\<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
  15.128 +                                 (binop=CondOr  \<and> the_Bool v1)))"
  15.129  text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
  15.130   if the value isn't already determined by the first argument*}
  15.131  
    16.1 --- a/src/HOL/Bali/Trans.thy	Mon Jul 26 13:50:52 2010 +0200
    16.2 +++ b/src/HOL/Bali/Trans.thy	Mon Jul 26 17:41:26 2010 +0200
    16.3 @@ -9,12 +9,13 @@
    16.4  
    16.5  theory Trans imports Evaln begin
    16.6  
    16.7 -definition groundVar :: "var \<Rightarrow> bool" where
    16.8 -"groundVar v \<longleftrightarrow> (case v of
    16.9 -                   LVar ln \<Rightarrow> True
   16.10 -                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
   16.11 -                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
   16.12 -                 | InsInitV c v \<Rightarrow> False)"
   16.13 +definition
   16.14 +  groundVar :: "var \<Rightarrow> bool" where
   16.15 +  "groundVar v \<longleftrightarrow> (case v of
   16.16 +                     LVar ln \<Rightarrow> True
   16.17 +                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
   16.18 +                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
   16.19 +                   | InsInitV c v \<Rightarrow> False)"
   16.20  
   16.21  lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
   16.22    assumes ground: "groundVar v" and
   16.23 @@ -34,14 +35,15 @@
   16.24      done
   16.25  qed
   16.26  
   16.27 -definition groundExprs :: "expr list \<Rightarrow> bool" where
   16.28 -  "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
   16.29 +definition
   16.30 +  groundExprs :: "expr list \<Rightarrow> bool"
   16.31 +  where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
   16.32    
   16.33 -primrec the_val:: "expr \<Rightarrow> val" where
   16.34 -  "the_val (Lit v) = v"
   16.35 +primrec the_val:: "expr \<Rightarrow> val"
   16.36 +  where "the_val (Lit v) = v"
   16.37  
   16.38  primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
   16.39 -  "the_var G s (LVar ln)                    =(lvar ln (store s),s)"
   16.40 +  "the_var G s (LVar ln) = (lvar ln (store s),s)"
   16.41  | the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
   16.42  | the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
   16.43  
    17.1 --- a/src/HOL/Bali/Type.thy	Mon Jul 26 13:50:52 2010 +0200
    17.2 +++ b/src/HOL/Bali/Type.thy	Mon Jul 26 17:41:26 2010 +0200
    17.3 @@ -36,8 +36,9 @@
    17.4  abbreviation Array :: "ty \<Rightarrow> ty"  ("_.[]" [90] 90)
    17.5    where "T.[] == RefT (ArrayT T)"
    17.6  
    17.7 -definition the_Class :: "ty \<Rightarrow> qtname" where
    17.8 - "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
    17.9 +definition
   17.10 +  the_Class :: "ty \<Rightarrow> qtname"
   17.11 +  where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
   17.12   
   17.13  lemma the_Class_eq [simp]: "the_Class (Class C)= C"
   17.14  by (auto simp add: the_Class_def)
    18.1 --- a/src/HOL/Bali/TypeRel.thy	Mon Jul 26 13:50:52 2010 +0200
    18.2 +++ b/src/HOL/Bali/TypeRel.thy	Mon Jul 26 17:41:26 2010 +0200
    18.3 @@ -25,14 +25,17 @@
    18.4  \end{itemize}
    18.5  *}
    18.6  
    18.7 -consts
    18.8 -
    18.9  (*subint1, in Decl.thy*)                     (* direct subinterface       *)
   18.10  (*subint , by translation*)                  (* subinterface (+ identity) *)
   18.11  (*subcls1, in Decl.thy*)                     (* direct subclass           *)
   18.12  (*subcls , by translation*)                  (*        subclass           *)
   18.13  (*subclseq, by translation*)                 (* subclass + identity       *)
   18.14 -  implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
   18.15 +
   18.16 +definition
   18.17 +  implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
   18.18 +  --{* direct implementation, cf. 8.1.3 *}
   18.19 +  where "implmt1 G = {(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
   18.20 +
   18.21  
   18.22  abbreviation
   18.23    subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
   18.24 @@ -325,16 +328,11 @@
   18.25  
   18.26  section "implementation relation"
   18.27  
   18.28 -defs
   18.29 -  --{* direct implementation, cf. 8.1.3 *}
   18.30 -implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
   18.31 -
   18.32  lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
   18.33  apply (unfold implmt1_def)
   18.34  apply auto
   18.35  done
   18.36  
   18.37 -
   18.38  inductive --{* implementation, cf. 8.1.4 *}
   18.39    implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
   18.40    for G :: prog
   18.41 @@ -568,8 +566,9 @@
   18.42  apply (fast dest: widen_Class_Class widen_Class_Iface)
   18.43  done
   18.44  
   18.45 -definition widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) where
   18.46 - "G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
   18.47 +definition
   18.48 +  widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
   18.49 +  where "G\<turnstile>Ts[\<preceq>]Ts' = list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
   18.50  
   18.51  lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
   18.52  apply (unfold widens_def)
    19.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Jul 26 13:50:52 2010 +0200
    19.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Jul 26 17:41:26 2010 +0200
    19.3 @@ -93,23 +93,27 @@
    19.4  
    19.5  section "result conformance"
    19.6  
    19.7 -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
    19.8 -"s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
    19.9 - (\<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>
   19.10 - (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
   19.11 +definition
   19.12 +  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
   19.13 +where
   19.14 +  "s\<le>|f\<preceq>T\<Colon>\<preceq>E =
   19.15 +   ((\<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>
   19.16 +    (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s'))))"
   19.17  
   19.18  
   19.19 -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
   19.20 -  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
   19.21 -    \<equiv> case T of
   19.22 -        Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
   19.23 -                  then (\<forall> n. (the_In2 t) = LVar n 
   19.24 -                         \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
   19.25 -                             (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
   19.26 -                      (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
   19.27 -                      (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
   19.28 -                  else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
   19.29 -      | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
   19.30 +definition
   19.31 +  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)
   19.32 +where
   19.33 +  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T =
   19.34 +    (case T of
   19.35 +      Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
   19.36 +                then (\<forall> n. (the_In2 t) = LVar n 
   19.37 +                       \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
   19.38 +                           (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
   19.39 +                    (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
   19.40 +                    (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
   19.41 +                else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
   19.42 +    | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts)"
   19.43  
   19.44  text {*
   19.45   With @{term rconf} we describe the conformance of the result value of a term.
   19.46 @@ -324,9 +328,11 @@
   19.47  
   19.48  declare fun_upd_apply [simp del]
   19.49  
   19.50 -definition DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70) where
   19.51 -  "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
   19.52 -                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
   19.53 +definition
   19.54 +  DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
   19.55 +where
   19.56 +  "G\<turnstile>mode\<rightarrow>D\<preceq>t = (mode = IntVir \<longrightarrow> is_class G D \<and> 
   19.57 +                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t))"
   19.58  
   19.59  lemma DynT_propI: 
   19.60   "\<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> 
    20.1 --- a/src/HOL/Bali/Value.thy	Mon Jul 26 13:50:52 2010 +0200
    20.2 +++ b/src/HOL/Bali/Value.thy	Mon Jul 26 17:41:26 2010 +0200
    20.3 @@ -17,29 +17,34 @@
    20.4          | Addr loc      --{* addresses, i.e. locations of objects *}
    20.5  
    20.6  
    20.7 -consts   the_Bool   :: "val \<Rightarrow> bool"  
    20.8 -primrec "the_Bool (Bool b) = b"
    20.9 -consts   the_Intg   :: "val \<Rightarrow> int"
   20.10 -primrec "the_Intg (Intg i) = i"
   20.11 -consts   the_Addr   :: "val \<Rightarrow> loc"
   20.12 -primrec "the_Addr (Addr a) = a"
   20.13 +primrec the_Bool :: "val \<Rightarrow> bool"
   20.14 +  where "the_Bool (Bool b) = b"
   20.15 +
   20.16 +primrec the_Intg :: "val \<Rightarrow> int"
   20.17 +  where "the_Intg (Intg i) = i"
   20.18 +
   20.19 +primrec the_Addr :: "val \<Rightarrow> loc"
   20.20 +  where "the_Addr (Addr a) = a"
   20.21  
   20.22  types   dyn_ty      = "loc \<Rightarrow> ty option"
   20.23 -consts
   20.24 -  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
   20.25 -  defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
   20.26 -  default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}
   20.27 +
   20.28 +primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
   20.29 +where
   20.30 +  "typeof dt  Unit = Some (PrimT Void)"
   20.31 +| "typeof dt (Bool b) = Some (PrimT Boolean)"
   20.32 +| "typeof dt (Intg i) = Some (PrimT Integer)"
   20.33 +| "typeof dt  Null = Some NT"
   20.34 +| "typeof dt (Addr a) = dt a"
   20.35  
   20.36 -primrec "typeof dt  Unit    = Some (PrimT Void)"
   20.37 -        "typeof dt (Bool b) = Some (PrimT Boolean)"
   20.38 -        "typeof dt (Intg i) = Some (PrimT Integer)"
   20.39 -        "typeof dt  Null    = Some NT"
   20.40 -        "typeof dt (Addr a) = dt a"
   20.41 +primrec defpval :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
   20.42 +where
   20.43 +  "defpval Void = Unit"
   20.44 +| "defpval Boolean = Bool False"
   20.45 +| "defpval Integer = Intg 0"
   20.46  
   20.47 -primrec "defpval Void    = Unit"
   20.48 -        "defpval Boolean = Bool False"
   20.49 -        "defpval Integer = Intg 0"
   20.50 -primrec "default_val (PrimT pt) = defpval pt"
   20.51 -        "default_val (RefT  r ) = Null"
   20.52 +primrec default_val :: "ty \<Rightarrow> val"  --{* default value for all types *}
   20.53 +where
   20.54 +  "default_val (PrimT pt) = defpval pt"
   20.55 +| "default_val (RefT  r ) = Null"
   20.56  
   20.57  end
    21.1 --- a/src/HOL/Bali/WellForm.thy	Mon Jul 26 13:50:52 2010 +0200
    21.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Jul 26 17:41:26 2010 +0200
    21.3 @@ -31,8 +31,9 @@
    21.4  text  {* well-formed field declaration (common part for classes and interfaces),
    21.5          cf. 8.3 and (9.3) *}
    21.6  
    21.7 -definition wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" where
    21.8 - "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
    21.9 +definition
   21.10 +  wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
   21.11 +  where "wf_fdecl G P = (\<lambda>(fn,f). is_acc_type G P (type f))"
   21.12  
   21.13  lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
   21.14  apply (unfold wf_fdecl_def)
   21.15 @@ -54,11 +55,12 @@
   21.16  \item the parameter names are unique
   21.17  \end{itemize} 
   21.18  *}
   21.19 -definition wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
   21.20 - "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
   21.21 +definition
   21.22 +  wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
   21.23 +  "wf_mhead G P = (\<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
   21.24                              \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
   21.25                              is_acc_type G P (resTy mh) \<and>
   21.26 -                            \<spacespace> distinct (pars mh)"
   21.27 +                            \<spacespace> distinct (pars mh))"
   21.28  
   21.29  
   21.30  text {*
   21.31 @@ -76,23 +78,25 @@
   21.32  \end{itemize}
   21.33  *}
   21.34  
   21.35 -definition callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
   21.36 -"callee_lcl C sig m 
   21.37 - \<equiv> \<lambda> k. (case k of
   21.38 +definition
   21.39 +  callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
   21.40 +  "callee_lcl C sig m =
   21.41 +    (\<lambda>k. (case k of
   21.42              EName e 
   21.43              \<Rightarrow> (case e of 
   21.44                    VNam v 
   21.45                    \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
   21.46                  | Res \<Rightarrow> Some (resTy m))
   21.47 -          | This \<Rightarrow> if is_static m then None else Some (Class C))"
   21.48 +          | This \<Rightarrow> if is_static m then None else Some (Class C)))"
   21.49  
   21.50 -definition parameters :: "methd \<Rightarrow> lname set" where
   21.51 -"parameters m \<equiv>  set (map (EName \<circ> VNam) (pars m)) 
   21.52 -                  \<union> (if (static m) then {} else {This})"
   21.53 +definition
   21.54 +  parameters :: "methd \<Rightarrow> lname set" where
   21.55 +  "parameters m = set (map (EName \<circ> VNam) (pars m)) \<union> (if (static m) then {} else {This})"
   21.56  
   21.57 -definition wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
   21.58 - "wf_mdecl G C \<equiv> 
   21.59 -      \<lambda>(sig,m).
   21.60 +definition
   21.61 +  wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
   21.62 +  "wf_mdecl G C =
   21.63 +      (\<lambda>(sig,m).
   21.64            wf_mhead G (pid C) sig (mhead m) \<and> 
   21.65            unique (lcls (mbody m)) \<and> 
   21.66            (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
   21.67 @@ -102,7 +106,7 @@
   21.68            \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and>
   21.69            (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> 
   21.70                  \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 
   21.71 -               \<and> Result \<in> nrm A)"
   21.72 +               \<and> Result \<in> nrm A))"
   21.73  
   21.74  lemma callee_lcl_VNam_simp [simp]:
   21.75  "callee_lcl C sig m (EName (VNam v)) 
   21.76 @@ -216,9 +220,10 @@
   21.77        superinterfaces widens to each of the corresponding result types
   21.78  \end{itemize}
   21.79  *}
   21.80 -definition wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
   21.81 - "wf_idecl G \<equiv> 
   21.82 -    \<lambda>(I,i). 
   21.83 +definition
   21.84 +  wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
   21.85 + "wf_idecl G =
   21.86 +    (\<lambda>(I,i). 
   21.87          ws_idecl G I (isuperIfs i) \<and> 
   21.88          \<not>is_class G I \<and>
   21.89          (\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
   21.90 @@ -233,7 +238,7 @@
   21.91                               is_static new = is_static old)) \<and> 
   21.92          (Option.set \<circ> table_of (imethods i) 
   21.93                 hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
   21.94 -               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
   21.95 +               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))"
   21.96  
   21.97  lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow>  
   21.98    wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
   21.99 @@ -317,8 +322,9 @@
  21.100  \end{itemize}
  21.101  *}
  21.102  (* to Table *)
  21.103 -definition entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20) where
  21.104 -"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
  21.105 +definition
  21.106 +  entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20)
  21.107 +  where "(t entails P) = (\<forall>k. \<forall> x \<in> t k: P x)"
  21.108  
  21.109  lemma entailsD:
  21.110   "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
  21.111 @@ -327,9 +333,10 @@
  21.112  lemma empty_entails[simp]: "empty entails P"
  21.113  by (simp add: entails_def)
  21.114  
  21.115 -definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
  21.116 -"wf_cdecl G \<equiv> 
  21.117 -   \<lambda>(C,c).
  21.118 +definition
  21.119 +  wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
  21.120 +  "wf_cdecl G =
  21.121 +     (\<lambda>(C,c).
  21.122        \<not>is_iface G C \<and>
  21.123        (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
  21.124          (\<forall>s. \<forall> im \<in> imethds G I s.
  21.125 @@ -352,7 +359,7 @@
  21.126                         (G,sig\<turnstile>new hides old 
  21.127                           \<longrightarrow> (accmodi old \<le> accmodi new \<and>
  21.128                                is_static old)))) 
  21.129 -            ))"
  21.130 +            )))"
  21.131  
  21.132  (*
  21.133  definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
  21.134 @@ -511,13 +518,14 @@
  21.135  \item all defined classes are wellformed
  21.136  \end{itemize}
  21.137  *}
  21.138 -definition wf_prog :: "prog \<Rightarrow> bool" where
  21.139 - "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
  21.140 +definition
  21.141 +  wf_prog :: "prog \<Rightarrow> bool" where
  21.142 + "wf_prog G = (let is = ifaces G; cs = classes G in
  21.143                   ObjectC \<in> set cs \<and> 
  21.144                  (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
  21.145                  (\<forall>xn. SXcptC xn \<in> set cs) \<and>
  21.146                  (\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
  21.147 -                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
  21.148 +                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs)"
  21.149  
  21.150  lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)"
  21.151  apply (unfold wf_prog_def Let_def)
  21.152 @@ -2095,16 +2103,16 @@
  21.153   Class    dynC 
  21.154   Array    Object
  21.155  *}
  21.156 -consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
  21.157 +primrec valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
  21.158                          ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
  21.159 -primrec
  21.160 -"G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
  21.161 -"G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
  21.162 -              = (if static_membr 
  21.163 -                    then dynC=Object 
  21.164 -                    else G\<turnstile>Class dynC\<preceq> Iface I)"
  21.165 -"G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
  21.166 -"G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
  21.167 +where
  21.168 +  "G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
  21.169 +| "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
  21.170 +                = (if static_membr 
  21.171 +                      then dynC=Object 
  21.172 +                      else G\<turnstile>Class dynC\<preceq> Iface I)"
  21.173 +| "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
  21.174 +| "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
  21.175  
  21.176  lemma valid_lookup_cls_is_class:
  21.177    assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
    22.1 --- a/src/HOL/Bali/WellType.thy	Mon Jul 26 13:50:52 2010 +0200
    22.2 +++ b/src/HOL/Bali/WellType.thy	Mon Jul 26 17:41:26 2010 +0200
    22.3 @@ -53,11 +53,13 @@
    22.4    emhead = "ref_ty \<times> mhead"
    22.5  
    22.6  --{* Some mnemotic selectors for emhead *}
    22.7 -definition "declrefT" :: "emhead \<Rightarrow> ref_ty" where
    22.8 -  "declrefT \<equiv> fst"
    22.9 +definition
   22.10 +  "declrefT" :: "emhead \<Rightarrow> ref_ty"
   22.11 +  where "declrefT = fst"
   22.12  
   22.13 -definition "mhd"     :: "emhead \<Rightarrow> mhead" where
   22.14 -  "mhd \<equiv> snd"
   22.15 +definition
   22.16 +  "mhd" :: "emhead \<Rightarrow> mhead"
   22.17 +  where "mhd \<equiv> snd"
   22.18  
   22.19  lemma declrefT_simp[simp]:"declrefT (r,m) = r"
   22.20  by (simp add: declrefT_def)
   22.21 @@ -77,50 +79,51 @@
   22.22  lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
   22.23  by (cases m) simp
   22.24  
   22.25 -consts
   22.26 -  cmheads        :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
   22.27 -  Objectmheads   :: "prog \<Rightarrow> qtname           \<Rightarrow> sig \<Rightarrow> emhead set"
   22.28 -  accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
   22.29 -  mheads         :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
   22.30 -defs
   22.31 - cmheads_def:
   22.32 -"cmheads G S C 
   22.33 -  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
   22.34 -  Objectmheads_def:
   22.35 -"Objectmheads G S  
   22.36 -  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
   22.37 -    ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
   22.38 -  accObjectmheads_def:
   22.39 -"accObjectmheads G S T
   22.40 -   \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
   22.41 -        then Objectmheads G S
   22.42 -        else (\<lambda>sig. {})"
   22.43 -primrec
   22.44 -"mheads G S  NullT     = (\<lambda>sig. {})"
   22.45 -"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
   22.46 -                         ` accimethds G (pid S) I sig \<union> 
   22.47 -                           accObjectmheads G S (IfaceT I) sig)"
   22.48 -"mheads G S (ClassT C) = cmheads G S C"
   22.49 -"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
   22.50 +definition
   22.51 +  cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
   22.52 +  where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))"
   22.53 +
   22.54 +definition
   22.55 +  Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
   22.56 +  "Objectmheads G S =
   22.57 +    (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
   22.58 +      ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
   22.59 +
   22.60 +definition
   22.61 +  accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
   22.62 +where
   22.63 +  "accObjectmheads G S T =
   22.64 +    (if G\<turnstile>RefT T accessible_in (pid S)
   22.65 +     then Objectmheads G S
   22.66 +     else (\<lambda>sig. {}))"
   22.67 +
   22.68 +primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
   22.69 +where
   22.70 +  "mheads G S  NullT     = (\<lambda>sig. {})"
   22.71 +| "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
   22.72 +                           ` accimethds G (pid S) I sig \<union> 
   22.73 +                             accObjectmheads G S (IfaceT I) sig)"
   22.74 +| "mheads G S (ClassT C) = cmheads G S C"
   22.75 +| "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
   22.76  
   22.77  definition
   22.78    --{* applicable methods, cf. 15.11.2.1 *}
   22.79 -  appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
   22.80 - "appl_methds G S rt = (\<lambda> sig. 
   22.81 +  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
   22.82 +  "appl_methds G S rt = (\<lambda> sig. 
   22.83        {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
   22.84                             G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
   22.85  
   22.86  definition
   22.87    --{* more specific methods, cf. 15.11.2.2 *}
   22.88 -  more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
   22.89 - "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
   22.90 +  more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
   22.91 +  "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
   22.92  (*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'*)
   22.93  
   22.94  definition
   22.95    --{* maximally specific methods, cf. 15.11.2.2 *}
   22.96 -   max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
   22.97 - "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
   22.98 -                      (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
   22.99 +  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
  22.100 +  "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
  22.101 +                          (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
  22.102  
  22.103  
  22.104  lemma max_spec2appl_meths: 
  22.105 @@ -138,13 +141,15 @@
  22.106  done
  22.107  
  22.108  
  22.109 -definition empty_dt :: "dyn_ty" where
  22.110 - "empty_dt \<equiv> \<lambda>a. None"
  22.111 +definition
  22.112 +  empty_dt :: "dyn_ty"
  22.113 +  where "empty_dt = (\<lambda>a. None)"
  22.114  
  22.115 -definition invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
  22.116 -"invmode m e \<equiv> if is_static m 
  22.117 +definition
  22.118 +  invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
  22.119 +  "invmode m e = (if is_static m 
  22.120                    then Static 
  22.121 -                  else if e=Super then SuperM else IntVir"
  22.122 +                  else if e=Super then SuperM else IntVir)"
  22.123  
  22.124  lemma invmode_nonstatic [simp]: 
  22.125    "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
  22.126 @@ -171,71 +176,71 @@
  22.127  
  22.128  section "Typing for unary operations"
  22.129  
  22.130 -consts unop_type :: "unop \<Rightarrow> prim_ty"
  22.131 -primrec 
  22.132 -"unop_type UPlus   = Integer"
  22.133 -"unop_type UMinus  = Integer"
  22.134 -"unop_type UBitNot = Integer"
  22.135 -"unop_type UNot    = Boolean"    
  22.136 +primrec unop_type :: "unop \<Rightarrow> prim_ty"
  22.137 +where
  22.138 +  "unop_type UPlus   = Integer"
  22.139 +| "unop_type UMinus  = Integer"
  22.140 +| "unop_type UBitNot = Integer"
  22.141 +| "unop_type UNot    = Boolean"    
  22.142  
  22.143 -consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
  22.144 -primrec
  22.145 -"wt_unop UPlus   t = (t = PrimT Integer)"
  22.146 -"wt_unop UMinus  t = (t = PrimT Integer)"
  22.147 -"wt_unop UBitNot t = (t = PrimT Integer)"
  22.148 -"wt_unop UNot    t = (t = PrimT Boolean)"
  22.149 +primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
  22.150 +where
  22.151 +  "wt_unop UPlus   t = (t = PrimT Integer)"
  22.152 +| "wt_unop UMinus  t = (t = PrimT Integer)"
  22.153 +| "wt_unop UBitNot t = (t = PrimT Integer)"
  22.154 +| "wt_unop UNot    t = (t = PrimT Boolean)"
  22.155  
  22.156  section "Typing for binary operations"
  22.157  
  22.158 -consts binop_type :: "binop \<Rightarrow> prim_ty"
  22.159 -primrec
  22.160 -"binop_type Mul      = Integer"     
  22.161 -"binop_type Div      = Integer"
  22.162 -"binop_type Mod      = Integer"
  22.163 -"binop_type Plus     = Integer"
  22.164 -"binop_type Minus    = Integer"
  22.165 -"binop_type LShift   = Integer"
  22.166 -"binop_type RShift   = Integer"
  22.167 -"binop_type RShiftU  = Integer"
  22.168 -"binop_type Less     = Boolean"
  22.169 -"binop_type Le       = Boolean"
  22.170 -"binop_type Greater  = Boolean"
  22.171 -"binop_type Ge       = Boolean"
  22.172 -"binop_type Eq       = Boolean"
  22.173 -"binop_type Neq      = Boolean"
  22.174 -"binop_type BitAnd   = Integer"
  22.175 -"binop_type And      = Boolean"
  22.176 -"binop_type BitXor   = Integer"
  22.177 -"binop_type Xor      = Boolean"
  22.178 -"binop_type BitOr    = Integer"
  22.179 -"binop_type Or       = Boolean"
  22.180 -"binop_type CondAnd  = Boolean"
  22.181 -"binop_type CondOr   = Boolean"
  22.182 +primrec binop_type :: "binop \<Rightarrow> prim_ty"
  22.183 +where
  22.184 +  "binop_type Mul      = Integer"     
  22.185 +| "binop_type Div      = Integer"
  22.186 +| "binop_type Mod      = Integer"
  22.187 +| "binop_type Plus     = Integer"
  22.188 +| "binop_type Minus    = Integer"
  22.189 +| "binop_type LShift   = Integer"
  22.190 +| "binop_type RShift   = Integer"
  22.191 +| "binop_type RShiftU  = Integer"
  22.192 +| "binop_type Less     = Boolean"
  22.193 +| "binop_type Le       = Boolean"
  22.194 +| "binop_type Greater  = Boolean"
  22.195 +| "binop_type Ge       = Boolean"
  22.196 +| "binop_type Eq       = Boolean"
  22.197 +| "binop_type Neq      = Boolean"
  22.198 +| "binop_type BitAnd   = Integer"
  22.199 +| "binop_type And      = Boolean"
  22.200 +| "binop_type BitXor   = Integer"
  22.201 +| "binop_type Xor      = Boolean"
  22.202 +| "binop_type BitOr    = Integer"
  22.203 +| "binop_type Or       = Boolean"
  22.204 +| "binop_type CondAnd  = Boolean"
  22.205 +| "binop_type CondOr   = Boolean"
  22.206  
  22.207 -consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
  22.208 -primrec
  22.209 -"wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.210 -"wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.211 -"wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.212 -"wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.213 -"wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.214 -"wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.215 -"wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.216 -"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.217 -"wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.218 -"wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.219 -"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.220 -"wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.221 -"wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
  22.222 -"wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
  22.223 -"wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.224 -"wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.225 -"wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.226 -"wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.227 -"wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.228 -"wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.229 -"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.230 -"wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.231 +primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
  22.232 +where
  22.233 +  "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.234 +| "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.235 +| "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.236 +| "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.237 +| "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.238 +| "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.239 +| "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.240 +| "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.241 +| "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.242 +| "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.243 +| "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.244 +| "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.245 +| "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
  22.246 +| "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
  22.247 +| "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.248 +| "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.249 +| "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.250 +| "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.251 +| "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
  22.252 +| "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.253 +| "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.254 +| "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
  22.255  
  22.256  section "Typing for terms"
  22.257  
  22.258 @@ -244,9 +249,8 @@
  22.259    (type) "tys" <= (type) "ty + ty list"
  22.260  
  22.261  
  22.262 -inductive
  22.263 -  wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
  22.264 -  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
  22.265 +inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
  22.266 +  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51] 50)
  22.267    and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
  22.268    and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
  22.269    and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"