equal
deleted
inserted
replaced
64 correct_frame G hp s maxl ins f \<and> |
64 correct_frame G hp s maxl ins f \<and> |
65 correct_frames G hp phi rT sig fs)) |
65 correct_frames G hp phi rT sig fs)) |
66 | Some x \<Rightarrow> frs = []" |
66 | Some x \<Rightarrow> frs = []" |
67 |
67 |
68 |
68 |
69 syntax (xsymbols) |
69 notation (xsymbols) |
70 correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool" |
70 correct_state ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50) |
71 ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50) |
|
72 |
71 |
73 |
72 |
74 lemma sup_ty_opt_OK: |
73 lemma sup_ty_opt_OK: |
75 "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')" |
74 "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')" |
76 apply (cases X) |
75 apply (cases X) |