equal
deleted
inserted
replaced
5 |
5 |
6 header {* \isaheader{Conformity Relations for Type Soundness Proof} *} |
6 header {* \isaheader{Conformity Relations for Type Soundness Proof} *} |
7 |
7 |
8 theory Conform imports State WellType Exceptions begin |
8 theory Conform imports State WellType Exceptions begin |
9 |
9 |
10 types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}" |
10 type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}" |
11 |
11 |
12 definition hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) where |
12 definition hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) where |
13 "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))" |
13 "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))" |
14 |
14 |
15 definition conf :: "'c prog => aheap => val => ty => bool" |
15 definition conf :: "'c prog => aheap => val => ty => bool" |