equal
deleted
inserted
replaced
7 The invariant for the type safety proof. |
7 The invariant for the type safety proof. |
8 *) |
8 *) |
9 |
9 |
10 header {* \isaheader{BV Type Safety Invariant} *} |
10 header {* \isaheader{BV Type Safety Invariant} *} |
11 |
11 |
12 theory Correct = BVSpec + JVMExec: |
12 theory Correct imports BVSpec JVMExec begin |
13 |
13 |
14 constdefs |
14 constdefs |
15 approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool" |
15 approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool" |
16 "approx_val G h v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T" |
16 "approx_val G h v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T" |
17 |
17 |