(*  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 -                             
  have "s ∈ i ∧ v s = n ⟶ (∃t . Sem (While b c) s t ∧ t ∈ q)" for s n
  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