*** empty log message ***
authorwenzelm
Mon Apr 26 14:56:18 2004 +0200 (2004-04-26)
changeset 146743506a9af46fc
parent 14673 3d760a971fde
child 14675 08b9c690f9cf
*** empty log message ***
src/HOL/Bali/Conform.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/TypeRel.thy
     1.1 --- a/src/HOL/Bali/Conform.thy	Mon Apr 26 14:54:45 2004 +0200
     1.2 +++ b/src/HOL/Bali/Conform.thy	Mon Apr 26 14:56:18 2004 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -  gext    :: "st \<Rightarrow> st \<Rightarrow> bool"                ("_\<le>|_"       [71,71]   70)
     1.8 +  gext    :: "st \<Rightarrow> st \<Rightarrow> bool"                ("_\<le>|_"       [71,71]   70)
     1.9     "s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj"
    1.10  
    1.11  text {* For the the proof of type soundness we will need the 
    1.12 @@ -186,7 +186,7 @@
    1.13  constdefs
    1.14  
    1.15    lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
    1.16 -                                                ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
    1.17 +                                                ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
    1.18             "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"
    1.19  
    1.20  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"
    1.21 @@ -272,7 +272,7 @@
    1.22  constdefs
    1.23  
    1.24    wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
    1.25 -                                          ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
    1.26 +                                          ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
    1.27             "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"
    1.28  
    1.29  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"
    1.30 @@ -389,7 +389,7 @@
    1.31  
    1.32  constdefs
    1.33  
    1.34 -  conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
    1.35 +  conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
    1.36     "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
    1.37      (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
    1.38                  \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
     2.1 --- a/src/HOL/Bali/Decl.thy	Mon Apr 26 14:54:45 2004 +0200
     2.2 +++ b/src/HOL/Bali/Decl.thy	Mon Apr 26 14:56:18 2004 +0200
     2.3 @@ -366,9 +366,9 @@
     2.4  
     2.5  consts
     2.6  
     2.7 -  Object_mdecls  ::  "mdecl list" --{* methods of Object *}
     2.8 -  SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
     2.9 -  ObjectC ::         "cdecl"      --{* declaration  of root      class   *}
    2.10 +  Object_mdecls  ::  "mdecl list" --{* methods of Object *}
    2.11 +  SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
    2.12 +  ObjectC ::         "cdecl"      --{* declaration  of root      class   *}
    2.13    SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *}
    2.14  
    2.15  defs 
     3.1 --- a/src/HOL/Bali/Evaln.thy	Mon Apr 26 14:54:45 2004 +0200
     3.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Apr 26 14:56:18 2004 +0200
     3.3 @@ -57,7 +57,7 @@
     3.4    evalsn:: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
     3.5  				("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
     3.6    execn	:: "[prog, state, stmt ,                nat, state] \<Rightarrow> bool"
     3.7 -				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
     3.8 +				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
     3.9  
    3.10  translations
    3.11  
     4.1 --- a/src/HOL/Bali/TypeRel.thy	Mon Apr 26 14:54:45 2004 +0200
     4.2 +++ b/src/HOL/Bali/TypeRel.thy	Mon Apr 26 14:56:18 2004 +0200
     4.3 @@ -29,16 +29,16 @@
     4.4  
     4.5  consts
     4.6  
     4.7 -(*subint1, in Decl.thy*)                     (* direct subinterface       *)
     4.8 -(*subint , by translation*)                  (* subinterface (+ identity) *)
     4.9 -(*subcls1, in Decl.thy*)                     (* direct subclass           *)
    4.10 -(*subcls , by translation*)                  (*        subclass           *)
    4.11 -(*subclseq, by translation*)                 (* subclass + identity       *)
    4.12 +(*subint1, in Decl.thy*)                     (* direct subinterface       *)
    4.13 +(*subint , by translation*)                  (* subinterface (+ identity) *)
    4.14 +(*subcls1, in Decl.thy*)                     (* direct subclass           *)
    4.15 +(*subcls , by translation*)                  (*        subclass           *)
    4.16 +(*subclseq, by translation*)                 (* subclass + identity       *)
    4.17    implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
    4.18 -  implmt    :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{*        implementation *}
    4.19 +  implmt    :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{*        implementation *}
    4.20    widen     :: "prog \<Rightarrow> (ty    \<times> ty   ) set" --{*        widening       *}
    4.21    narrow    :: "prog \<Rightarrow> (ty    \<times> ty   ) set" --{*        narrowing      *}
    4.22 -  cast     :: "prog \<Rightarrow> (ty    \<times> ty   ) set"  --{*        casting        *}
    4.23 +  cast     :: "prog \<Rightarrow> (ty    \<times> ty   ) set"  --{*        casting        *}
    4.24  
    4.25  syntax
    4.26