src/HOL/Bali/TypeSafe.thy
changeset 37956 ee939247b2fb
parent 36635 080b755377c0
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -93,23 +93,27 @@
     1.4  
     1.5  section "result conformance"
     1.6  
     1.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
     1.8 -"s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
     1.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>
    1.10 - (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
    1.11 +definition
    1.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)
    1.13 +where
    1.14 +  "s\<le>|f\<preceq>T\<Colon>\<preceq>E =
    1.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>
    1.16 +    (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s'))))"
    1.17  
    1.18  
    1.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
    1.20 -  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
    1.21 -    \<equiv> case T of
    1.22 -        Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
    1.23 -                  then (\<forall> n. (the_In2 t) = LVar n 
    1.24 -                         \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
    1.25 -                             (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
    1.26 -                      (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
    1.27 -                      (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
    1.28 -                  else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
    1.29 -      | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
    1.30 +definition
    1.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)
    1.32 +where
    1.33 +  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T =
    1.34 +    (case T of
    1.35 +      Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
    1.36 +                then (\<forall> n. (the_In2 t) = LVar n 
    1.37 +                       \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
    1.38 +                           (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
    1.39 +                    (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
    1.40 +                    (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
    1.41 +                else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
    1.42 +    | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts)"
    1.43  
    1.44  text {*
    1.45   With @{term rconf} we describe the conformance of the result value of a term.
    1.46 @@ -324,9 +328,11 @@
    1.47  
    1.48  declare fun_upd_apply [simp del]
    1.49  
    1.50 -definition DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70) where
    1.51 -  "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
    1.52 -                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
    1.53 +definition
    1.54 +  DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
    1.55 +where
    1.56 +  "G\<turnstile>mode\<rightarrow>D\<preceq>t = (mode = IntVir \<longrightarrow> is_class G D \<and> 
    1.57 +                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t))"
    1.58  
    1.59  lemma DynT_propI: 
    1.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>