70 | Meth: "\<forall>D. A \<turnstile> {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D \<preceq>C C \<and> |
70 | Meth: "\<forall>D. A \<turnstile> {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D \<preceq>C C \<and> |
71 P s \<and> s' = init_locs D m s} |
71 P s \<and> s' = init_locs D m s} |
72 Impl (D,m) {Q} ==> |
72 Impl (D,m) {Q} ==> |
73 A \<turnstile> {P} Meth (C,m) {Q}" |
73 A \<turnstile> {P} Meth (C,m) {Q}" |
74 |
74 |
75 \<comment>\<open>\<open>\<Union>Z\<close> instead of \<open>\<forall>Z\<close> in the conclusion and\\ |
75 \<comment> \<open>\<open>\<Union>Z\<close> instead of \<open>\<forall>Z\<close> in the conclusion and\\ |
76 Z restricted to type state due to limitations of the inductive package\<close> |
76 Z restricted to type state due to limitations of the inductive package\<close> |
77 | Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> |
77 | Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> |
78 (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> |
78 (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> |
79 A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" |
79 A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" |
80 |
80 |
81 \<comment>\<open>structural rules\<close> |
81 \<comment> \<open>structural rules\<close> |
82 |
82 |
83 | Asm: " a \<in> A ==> A |\<turnstile> {a}" |
83 | Asm: " a \<in> A ==> A |\<turnstile> {a}" |
84 |
84 |
85 | ConjI: " \<forall>c \<in> C. A |\<turnstile> {c} ==> A |\<turnstile> C" |
85 | ConjI: " \<forall>c \<in> C. A |\<turnstile> {c} ==> A |\<turnstile> C" |
86 |
86 |
87 | ConjE: "[|A |\<turnstile> C; c \<in> C |] ==> A |\<turnstile> {c}" |
87 | ConjE: "[|A |\<turnstile> C; c \<in> C |] ==> A |\<turnstile> {c}" |
88 |
88 |
89 \<comment>\<open>Z restricted to type state due to limitations of the inductive package\<close> |
89 \<comment> \<open>Z restricted to type state due to limitations of the inductive package\<close> |
90 | Conseq:"[| \<forall>Z::state. A \<turnstile> {P' Z} c {Q' Z}; |
90 | Conseq:"[| \<forall>Z::state. A \<turnstile> {P' Z} c {Q' Z}; |
91 \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> |
91 \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> |
92 A \<turnstile> {P} c {Q }" |
92 A \<turnstile> {P} c {Q }" |
93 |
93 |
94 \<comment>\<open>Z restricted to type state due to limitations of the inductive package\<close> |
94 \<comment> \<open>Z restricted to type state due to limitations of the inductive package\<close> |
95 | eConseq:"[| \<forall>Z::state. A \<turnstile>\<^sub>e {P' Z} e {Q' Z}; |
95 | eConseq:"[| \<forall>Z::state. A \<turnstile>\<^sub>e {P' Z} e {Q' Z}; |
96 \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> |
96 \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> |
97 A \<turnstile>\<^sub>e {P} e {Q }" |
97 A \<turnstile>\<^sub>e {P} e {Q }" |
98 |
98 |
99 |
99 |