src/HOL/IMP/Hoare_Sound_Complete.thy
changeset 54809 319358e48bb1
parent 53015 a1119cf551e8
child 63538 d7b5e2a222c2
equal deleted inserted replaced
54802:9ce867291c76 54809:319358e48bb1
    75   show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
    75   show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
    76     by (auto simp: hoare_valid_def wp_def)
    76     by (auto simp: hoare_valid_def wp_def)
    77   show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
    77   show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
    78 qed
    78 qed
    79 
    79 
       
    80 corollary hoare_sound_complete: "\<turnstile> {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}"
       
    81 by (metis hoare_complete hoare_sound)
       
    82 
    80 end
    83 end