(*  Title:      HOL/IMP/Hoare.ML

    ID:         $Id$

    Author:     Tobias Nipkow

    Copyright   1995 TUM

Soundness (and part of) relative completeness of Hoare rules

wrt denotational semantics

*)

Goal "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}";

by (etac hoare.conseq 1);

by  (atac 1);

by (Fast_tac 1);

qed "hoare_conseq1";

Goal "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}";

by (rtac hoare.conseq 1);

by    (atac 2);

by   (ALLGOALS Fast_tac);

qed "hoare_conseq2";

Goalw [hoare_valid_def] "|- {P}c{Q} ==> |= {P}c{Q}";

by (etac hoare.induct 1);

     by (ALLGOALS Asm_simp_tac);

  by (Fast_tac 1);

 by (Fast_tac 1);

by (EVERY' [rtac allI, rtac allI, rtac impI] 1);

by (etac induct2 1);

 by (rtac Gamma_mono 1);

by (rewtac Gamma_def);  

by (Fast_tac 1);

qed "hoare_sound";

Goalw [wp_def] "wp SKIP Q = Q";

by (Simp_tac 1);

qed "wp_SKIP";

Goalw [wp_def] "wp (x:==a) Q = (%s. Q(s[x::=a s]))";

by (Simp_tac 1);

qed "wp_Ass";

Goalw [wp_def] "wp (c;d) Q = wp c (wp d Q)";

by (Simp_tac 1);

by (rtac ext 1);

by (Fast_tac 1);

qed "wp_Semi";

Goalw [wp_def]

 "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))";

by (Simp_tac 1);

by (rtac ext 1);

by (Fast_tac 1);

qed "wp_If";

Goalw [wp_def]

  "b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";

by (stac C_While_If 1);

by (Asm_simp_tac 1);

qed "wp_While_True";

Goalw [wp_def] "~b s ==> wp (WHILE b DO c) Q s = Q s";

by (stac C_While_If 1);

by (Asm_simp_tac 1);

qed "wp_While_False";

Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];

(*Not suitable for rewriting: LOOPS!*)

Goal "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";

by (Simp_tac 1);

qed "wp_While_if";

Goal "wp (WHILE b DO c) Q s = \

\  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";

by (Simp_tac 1);

by (rtac iffI 1);

 by (rtac weak_coinduct 1);

  by (etac CollectI 1);

 by Safe_tac;

  by (rotate_tac ~1 1);

  by (Asm_full_simp_tac 1);

 by (rotate_tac ~1 1);

 by (Asm_full_simp_tac 1);

by (asm_full_simp_tac (simpset() addsimps [wp_def,Gamma_def]) 1);

by (strip_tac 1);

by (rtac mp 1);

 by (assume_tac 2);

by (etac induct2 1);

by (fast_tac (claset() addSIs [monoI]) 1);

by (stac gfp_Tarski 1);

 by (fast_tac (claset() addSIs [monoI]) 1);

by (Fast_tac 1);

qed "wp_While";

Delsimps [C_while];

AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];

Goal "!Q. |- {wp c Q} c {Q}";

by (induct_tac "c" 1);

    by (ALLGOALS Simp_tac);

    by (REPEAT_FIRST Fast_tac);

 by (blast_tac (claset() addIs [hoare_conseq1]) 1);

by Safe_tac;

by (rtac hoare_conseq2 1);

 by (rtac hoare.While 1);

 by (rtac hoare_conseq1 1);

  by (Fast_tac 2);

 by (safe_tac HOL_cs);

 by (ALLGOALS (EVERY'[rotate_tac ~1, Asm_full_simp_tac]));

qed_spec_mp "wp_is_pre";

Goal "|= {P}c{Q} ==> |- {P}c{Q}";

by (rtac (wp_is_pre RSN (2,hoare_conseq1)) 1);

by (rewrite_goals_tac [hoare_valid_def,wp_def]);

by (Fast_tac 1);

qed "hoare_relative_complete";