Theory HOL-Hoare.Hoare_Logic_Abort

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

section ‹Hoare Logic with an Abort statement for modelling run time errors›

theory Hoare_Logic_Abort
  imports Hoare_Syntax Hoare_Tac
begin

type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
type_synonym 'a var = "'a ⇒ nat"

datatype 'a com =
  Basic "'a ⇒ 'a"
| Abort
| 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 option => 'a option => bool"

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

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

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

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

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

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

text ‹The proof rules for partial correctness›

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 (fastforce simp:Valid_def image_def)

lemma While_aux:
  assumes "Sem (While b c) s s'"
  shows "∀s s'. Sem c s s' ⟶ s ∈ Some ` (I ∩ b) ⟶ s' ∈ Some ` I ⟹
    s ∈ Some ` I ⟹ s' ∈ Some ` (I ∩ -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 AbortRule: "p ⊆ {s. False} ⟹ Valid p Abort a q"
by(auto simp:Valid_def)

text ‹The proof rules for total correctness›

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

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

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(4) 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) (Acons a1 a2)  q"
proof (unfold ValidTC_def, rule allI)
  fix s
  show "s ∈ p ⟶ (∃t . Sem (Cond b c1 c2) (Some s) (Some t) ∧ t ∈ q)"
    apply (cases "s ∈ b")
    apply (metis (mono_tags, lifting) Ball_Collect Sem.intros(6) ValidTC_def assms(1,2))
    by (metis (mono_tags, lifting) Ball_Collect Sem.intros(7) ValidTC_def assms(1,3))
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 A) q"
proof -
  {
    fix s n
    have "s ∈ i ∧ v s = n ⟶ (∃t . Sem (While b c) (Some s) (Some 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) (Some s) (Some t) ∧ t ∈ q)"
      show "s ∈ i ∧ v s = n ⟶ (∃t . Sem (While b c) (Some s) (Some 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 (Some s) (Some t) ∧ t ∈ i ∩ {s . v s < n}"
          by (metis assms(2) ValidTC_def)
        from this obtain t where 3: "Sem c (Some s) (Some t) ∧ t ∈ i ∩ {s . v s < n}"
          by auto
        hence "∃u . Sem (While b c) (Some t) (Some u) ∧ u ∈ q"
          using 1 by auto
        thus "∃t . Sem (While b c) (Some s) (Some t) ∧ t ∈ q"
          using 2 3 Sem.intros(10) by force
      next
        assume "s ∉ b" and "s ∈ i ∧ v s = n"
        thus "∃t . Sem (While b c) (Some s) (Some t) ∧ t ∈ q"
          using Sem.intros(9) assms(3) by fastforce
      qed
    qed
  }
  thus ?thesis
    using assms(1) ValidTC_def by force
qed


subsection ‹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›}
›

― ‹Special syntax for guarded statements and guarded array updates:›
syntax
  "_guarded_com" :: "bool ⇒ 'a com ⇒ 'a com"  ("(2_ →/ _)" 71)
  "_array_update" :: "'a list ⇒ nat ⇒ 'a ⇒ 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
translations
  "P → c" ⇌ "IF P THEN c ELSE CONST Abort FI"
  "a[i] := v" ⇀ "(i < CONST length a) → (a := CONST list_update a i v)"
  ― ‹reverse translation not possible because of duplicate ‹a››

text ‹
  Note: there is no special syntax for guarded array access. Thus
  you must write ‹j < length a → a[i] := a!j›.
›


subsection ‹Proof methods: VCG›

declare BasicRule [Hoare_Tac.BasicRule]
  and SkipRule [Hoare_Tac.SkipRule]
  and AbortRule [Hoare_Tac.AbortRule]
  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