15 hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) |
15 hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) |
16 "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))" |
16 "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))" |
17 |
17 |
18 conf :: "'c prog => aheap => val => ty => bool" |
18 conf :: "'c prog => aheap => val => ty => bool" |
19 ("_,_ |- _ ::<= _" [51,51,51,51] 50) |
19 ("_,_ |- _ ::<= _" [51,51,51,51] 50) |
20 "G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T" |
20 "G,h|-v::<=T == \<exists>T'. typeof (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T" |
21 |
21 |
22 lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool" |
22 lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool" |
23 ("_,_ |- _ [::<=] _" [51,51,51,51] 50) |
23 ("_,_ |- _ [::<=] _" [51,51,51,51] 50) |
24 "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)" |
24 "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)" |
25 |
25 |