76 A |-e {P} Cast C e {Q}" |
76 A |-e {P} Cast C e {Q}" |
77 |
77 |
78 Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a}; |
78 Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a}; |
79 \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and> |
79 \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and> |
80 s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_locs s))} |
80 s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_locs s))} |
81 Meth C m {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==> |
81 Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==> |
82 A |-e {P} {C}e1..m(e2) {S}" |
82 A |-e {P} {C}e1..m(e2) {S}" |
83 |
83 |
84 Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> |
84 Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> |
85 P s \<and> s' = init_locs D m s} |
85 P s \<and> s' = init_locs D m s} |
86 Impl (D,m) {Q} ==> |
86 Impl (D,m) {Q} ==> |
87 A |- {P} Meth C m {Q}" |
87 A |- {P} Meth (C,m) {Q}" |
88 |
88 |
89 (*\<Union>z instead of \<forall>z in the conclusion and |
89 (*\<Union>z instead of \<forall>z in the conclusion and |
90 z restricted to type state due to limitations of the inductive package *) |
90 z restricted to type state due to limitations of the inductive package *) |
91 Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) ||- |
91 Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) ||- |
92 (\<lambda>M. (P z M, body M, Q z M))`Ms ==> |
92 (\<lambda>M. (P z M, body M, Q z M))`Ms ==> |