equal
deleted
inserted
replaced
5 |
5 |
6 section \<open>Conformity Relations for Type Soundness Proof\<close> |
6 section \<open>Conformity Relations for Type Soundness Proof\<close> |
7 |
7 |
8 theory Conform imports State WellType Exceptions begin |
8 theory Conform imports State WellType Exceptions begin |
9 |
9 |
10 type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" \<comment> "same as \<open>env\<close> of \<open>WellType.thy\<close>" |
10 type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" \<comment> \<open>same as \<open>env\<close> of \<open>WellType.thy\<close>\<close> |
11 |
11 |
12 definition hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50) where |
12 definition hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50) where |
13 "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))" |
13 "h\<le>|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" |