src/HOL/MicroJava/J/Conform.thy
changeset 10042 7164dc0d24d8
parent 9346 297dcbf64526
child 10061 fe82134773dc
     1.1 --- a/src/HOL/MicroJava/J/Conform.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -12,23 +12,23 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -  hext :: "aheap \\<Rightarrow> aheap \\<Rightarrow> bool"		 (     "_\\<le>|_"  [51,51] 50)
     1.8 - "h\\<le>|h' \\<equiv> \\<forall>a C fs. h a = Some(C,fs) \\<longrightarrow> (\\<exists>fs'. h' a = Some(C,fs'))"
     1.9 +  hext :: "aheap => aheap => bool"		 (     "_\\<le>|_"  [51,51] 50)
    1.10 + "h\\<le>|h' == \\<forall>a C fs. h a = Some(C,fs) --> (\\<exists>fs'. h' a = Some(C,fs'))"
    1.11  
    1.12 -  conf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> ty \\<Rightarrow> bool"	 ( "_,_\\<turnstile>_\\<Colon>\\<preceq>_"  [51,51,51,51] 50)
    1.13 - "G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<equiv> \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
    1.14 +  conf :: "'c prog => aheap => val => ty => bool"	 ( "_,_\\<turnstile>_::\\<preceq>_"  [51,51,51,51] 50)
    1.15 + "G,h\\<turnstile>v::\\<preceq>T == \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
    1.16  
    1.17 -  lconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> ('a \\<leadsto> val) \\<Rightarrow> ('a \\<leadsto> ty) \\<Rightarrow> bool"
    1.18 -                                                 ("_,_\\<turnstile>_[\\<Colon>\\<preceq>]_" [51,51,51,51] 50)
    1.19 - "G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts \\<equiv> \\<forall>n T. Ts n = Some T \\<longrightarrow> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T)"
    1.20 +  lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
    1.21 +                                                 ("_,_\\<turnstile>_[::\\<preceq>]_" [51,51,51,51] 50)
    1.22 + "G,h\\<turnstile>vs[::\\<preceq>]Ts == \\<forall>n T. Ts n = Some T --> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T)"
    1.23  
    1.24 -  oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool"      ("_,_\\<turnstile>_\\<surd>"     [51,51,51]    50)
    1.25 - "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))"
    1.26 +  oconf :: "'c prog => aheap => obj => bool"      ("_,_\\<turnstile>_\\<surd>"     [51,51,51]    50)
    1.27 + "G,h\\<turnstile>obj\\<surd> == G,h\\<turnstile>snd obj[::\\<preceq>]map_of (fields (G,fst obj))"
    1.28  
    1.29 -  hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
    1.30 - "G\\<turnstile>h h\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
    1.31 +  hconf :: "'c prog => aheap => bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
    1.32 + "G\\<turnstile>h h\\<surd>    == \\<forall>a obj. h a = Some obj --> G,h\\<turnstile>obj\\<surd>"
    1.33  
    1.34 -  conforms :: "state \\<Rightarrow> java_mb env_ \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
    1.35 - "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
    1.36 +  conforms :: "state => java_mb env_ => bool"	 ("_::\\<preceq>_"       [51,51]       50)
    1.37 + "s::\\<preceq>E == prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[::\\<preceq>]localT E"
    1.38  
    1.39  end