Theory Hoare_Logic

(*  Title:      HOL/Hoare/Hoare_Logic.thy
    Author:     Leonor Prensa Nieto & Tobias Nipkow
    Copyright   1998 TUM
    Author:     Walter Guttmann (extension to total-correctness proofs)
*)

section ‹Hoare logic›

theory Hoare_Logic
  imports Hoare_Syntax Hoare_Tac
begin

subsection ‹Sugared semantic embedding of Hoare logic›

text ‹
  Strictly speaking a shallow embedding (as implemented by Norbert Galm
  following Mike Gordon) would suffice. Maybe the datatype com comes in useful
  later.
›

type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"

datatype 'a com =
  Basic "'a ⇒ 'a"
| Seq "'a com" "'a com"
| Cond "'a bexp" "'a com" "'a com"
| While "'a bexp" "'a com"

abbreviation annskip ("SKIP") where "SKIP == Basic id"

type_synonym 'a sem = "'a => 'a => bool"

inductive Sem :: "'a com ⇒ 'a sem"
where
  "Sem (Basic f) s (f s)"
| "Sem c1 s s'' ⟹ Sem c2 s'' s' ⟹ Sem (Seq c1 c2) s s'"
| "s ∈ b ⟹ Sem c1 s s' ⟹ Sem (Cond b c1 c2) s s'"
| "s ∉ b ⟹ Sem c2 s s' ⟹ Sem (Cond b c1 c2) s s'"
| "s ∉ b ⟹ Sem (While b c) s s"
| "s ∈ b ⟹ Sem c s s'' ⟹ Sem (While b c) s'' s' ⟹
   Sem (While b c) s s'"

definition Valid :: "'a bexp ⇒ 'a com ⇒ 'a anno ⇒ 'a bexp ⇒ bool"
  where "Valid p c a q ≡ ∀s s'. Sem c s s' ⟶ s ∈ p ⟶ s' ∈ q"

definition ValidTC :: "'a bexp ⇒ 'a com ⇒ 'a anno ⇒ 'a bexp ⇒ bool"
  where "ValidTC p c a q ≡ ∀s. s ∈ p ⟶ (∃t. Sem c s t ∧ t ∈ q)"

inductive_cases [elim!]:
  "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
  "Sem (Cond b c1 c2) s s'"

lemma Sem_deterministic:
  assumes "Sem c s s1"
      and "Sem c s s2"
    shows "s1 = s2"
proof -
  have "Sem c s s1 ⟹ (∀s2. Sem c s s2 ⟶ s1 = s2)"
    by (induct rule: Sem.induct) (subst Sem.simps, blast)+
  thus ?thesis
    using assms by simp
qed

lemma tc_implies_pc:
  "ValidTC p c a q ⟹ Valid p c a q"
  by (metis Sem_deterministic Valid_def ValidTC_def)

lemma tc_extract_function:
  "ValidTC p c a q ⟹ ∃f . ∀s . s ∈ p ⟶ f s ∈ q"
  by (metis ValidTC_def)


lemma SkipRule: "p ⊆ q ⟹ Valid p (Basic id) a q"
by (auto simp:Valid_def)

lemma BasicRule: "p ⊆ {s. f s ∈ q} ⟹ Valid p (Basic f) a q"
by (auto simp:Valid_def)

lemma SeqRule: "Valid P c1 a1 Q ⟹ Valid Q c2 a2 R ⟹ Valid P (Seq c1 c2) (Aseq a1 a2) R"
by (auto simp:Valid_def)

lemma CondRule:
 "p ⊆ {s. (s ∈ b ⟶ s ∈ w) ∧ (s ∉ b ⟶ s ∈ w')}
  ⟹ Valid w c1 a1 q ⟹ Valid w' c2 a2 q ⟹ Valid p (Cond b c1 c2) (Acond a1 a2) q"
by (auto simp:Valid_def)

lemma While_aux:
  assumes "Sem (While b c) s s'"
  shows "∀s s'. Sem c s s' ⟶ s ∈ I ∧ s ∈ b ⟶ s' ∈ I ⟹
    s ∈ I ⟹ s' ∈ I ∧ s' ∉ b"
  using assms
  by (induct "While b c" s s') auto

lemma WhileRule:
 "p ⊆ i ⟹ Valid (i ∩ b) c (A 0) i ⟹ i ∩ (-b) ⊆ q ⟹ Valid p (While b c) (Awhile i v A) q"
apply (clarsimp simp:Valid_def)
apply(drule While_aux)
  apply assumption
 apply blast
apply blast
done

lemma SkipRuleTC:
  assumes "p ⊆ q"
    shows "ValidTC p (Basic id) a q"
  by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)

lemma BasicRuleTC:
  assumes "p ⊆ {s. f s ∈ q}"
    shows "ValidTC p (Basic f) a q"
  by (metis assms Ball_Collect Sem.intros(1) ValidTC_def)

lemma SeqRuleTC:
  assumes "ValidTC p c1 a1 q"
      and "ValidTC q c2 a2 r"
    shows "ValidTC p (Seq c1 c2) (Aseq a1 a2) r"
  by (meson assms Sem.intros(2) ValidTC_def)

lemma CondRuleTC:
 assumes "p ⊆ {s. (s ∈ b ⟶ s ∈ w) ∧ (s ∉ b ⟶ s ∈ w')}"
     and "ValidTC w c1 a1 q"
     and "ValidTC w' c2 a2 q"
   shows "ValidTC p (Cond b c1 c2) (Acond a1 a2) q"
proof (unfold ValidTC_def, rule allI)
  fix s
  show "s ∈ p ⟶ (∃t . Sem (Cond b c1 c2) s t ∧ t ∈ q)"
    apply (cases "s ∈ b")
    apply (metis (mono_tags, lifting) assms(1,2) Ball_Collect Sem.intros(3) ValidTC_def)
    by (metis (mono_tags, lifting) assms(1,3) Ball_Collect Sem.intros(4) ValidTC_def)
qed

lemma WhileRuleTC:
  assumes "p ⊆ i"
      and "⋀n::nat . ValidTC (i ∩ b ∩ {s . v s = n}) c (A n) (i ∩ {s . v s < n})"
      and "i ∩ uminus b ⊆ q"
    shows "ValidTC p (While b c) (Awhile i v (λn. A n)) q"
proof -                             
  {
    fix s n
    have "s ∈ i ∧ v s = n ⟶ (∃t . Sem (While b c) s t ∧ t ∈ q)"
    proof (induction "n" arbitrary: s rule: less_induct)
      fix n :: nat
      fix s :: 'a
      assume 1: "⋀(m::nat) s::'a . m < n ⟹ s ∈ i ∧ v s = m ⟶ (∃t . Sem (While b c) s t ∧ t ∈ q)"
      show "s ∈ i ∧ v s = n ⟶ (∃t . Sem (While b c) s t ∧ t ∈ q)"
      proof (rule impI, cases "s ∈ b")
        assume 2: "s ∈ b" and "s ∈ i ∧ v s = n"
        hence "s ∈ i ∩ b ∩ {s . v s = n}"
          using assms(1) by auto
        hence "∃t . Sem c s t ∧ t ∈ i ∩ {s . v s < n}"
          by (metis assms(2) ValidTC_def)
        from this obtain t where 3: "Sem c s t ∧ t ∈ i ∩ {s . v s < n}"
          by auto
        hence "∃u . Sem (While b c) t u ∧ u ∈ q"
          using 1 by auto
        thus "∃t . Sem (While b c) s t ∧ t ∈ q"
          using 2 3 Sem.intros(6) by force
      next
        assume "s ∉ b" and "s ∈ i ∧ v s = n"
        thus "∃t . Sem (While b c) s t ∧ t ∈ q"
          using Sem.intros(5) assms(3) by fastforce
      qed
    qed
  }
  thus ?thesis
    using assms(1) ValidTC_def by force
qed


subsubsection ‹Concrete syntax›

setup ‹
  Hoare_Syntax.setup
   {Basic = \<^const_syntax>‹Basic›,
    Skip = \<^const_syntax>‹annskip›,
    Seq = \<^const_syntax>‹Seq›,
    Cond = \<^const_syntax>‹Cond›,
    While = \<^const_syntax>‹While›,
    Valid = \<^const_syntax>‹Valid›,
    ValidTC = \<^const_syntax>‹ValidTC›}
›


subsubsection ‹Proof methods: VCG›

declare BasicRule [Hoare_Tac.BasicRule]
  and SkipRule [Hoare_Tac.SkipRule]
  and SeqRule [Hoare_Tac.SeqRule]
  and CondRule [Hoare_Tac.CondRule]
  and WhileRule [Hoare_Tac.WhileRule]

declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
  and SkipRuleTC [Hoare_Tac.SkipRuleTC]
  and SeqRuleTC [Hoare_Tac.SeqRuleTC]
  and CondRuleTC [Hoare_Tac.CondRuleTC]
  and WhileRuleTC [Hoare_Tac.WhileRuleTC]

method_setup vcg = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))›
  "verification condition generator"

method_setup vcg_simp = ‹
  Scan.succeed (fn ctxt =>
    SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))›
  "verification condition generator plus simplification"

method_setup vcg_tc = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))›
  "verification condition generator"

method_setup vcg_tc_simp = ‹
  Scan.succeed (fn ctxt =>
    SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))›
  "verification condition generator plus simplification"

end