equal
deleted
inserted
replaced
63 show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
63 show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
64 qed |
64 qed |
65 qed (auto intro: hoare.conseq) |
65 qed (auto intro: hoare.conseq) |
66 |
66 |
67 corollary vc_sound': |
67 corollary vc_sound': |
68 "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} strip c {Q}" |
68 "\<lbrakk> \<forall>s. vc c Q s; \<forall>s. P s \<longrightarrow> pre c Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip c {Q}" |
69 by (metis strengthen_pre vc_sound) |
69 by (metis strengthen_pre vc_sound) |
70 |
70 |
71 |
71 |
72 text{* Completeness: *} |
72 text{* Completeness: *} |
73 |
73 |