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_syntaxBasic,
    Skip = const_syntaxannskip,
    Seq = const_syntaxSeq,
    Cond = const_syntaxCond,
    While = const_syntaxWhile,
    Valid = const_syntaxValid,
    ValidTC = const_syntaxValidTC}


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