Hoare logic soundness sketch for procedure calls

HoareProcCall.thy

theory HoareProcCall
imports Main
begin

typedecl state
typedecl procname
typedecl bexpr

datatype com = Call procname | Skip | Cond bexpr com com

consts procenv :: "procname \<Rightarrow> com"

consts bexpr_eval :: "bexpr \<Rightarrow> state \<Rightarrow> bool"

inductive
  sem :: "state \<times> com \<Rightarrow> state \<times> com \<Rightarrow> bool"
where
  sem_Call: "procenv p = c \<Longrightarrow> sem (s,(Call p)) (s,c)" |
  sem_Cond: "sem (s, (Cond b c c')) (s, (if (bexpr_eval b s) then c else c'))"

inductive_cases sem_CallE: "sem (s,(Call p)) (s',c')"
inductive_cases sem_CondE: "sem (s, (Cond b c c')) (s', c'')"

text {*
  pre- and post-condition annotations on each procedure
*}
consts annotations :: "procname \<Rightarrow> (state \<Rightarrow> bool) \<times> (state \<Rightarrow> bool)"

inductive
  derived :: "(state \<Rightarrow> bool) \<Rightarrow> com \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> bool"
where
  derived_Skip: "derived P Skip P"  |
  derived_Call: "annotations p = (P,Q) \<Longrightarrow> derived P (Call p) Q" |
  derived_Cond: "derived (\<lambda>s. P s \<and> bexpr_eval b s) c Q \<Longrightarrow> 
   derived (\<lambda>s. P s \<and> \<not> (bexpr_eval b s)) c' Q \<Longrightarrow> derived P (Cond b c c') Q"

inductive_cases derived_SkipE: "derived P Skip Q"
inductive_cases derived_CallE: "derived P (Call p) Q"
inductive_cases derived_CondE: "derived P (Cond b c c') Q"

primrec
  valid :: "nat \<Rightarrow> state \<Rightarrow> com \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> bool"
where
  "valid 0 s c Q = (if (c = Skip) then Q s else True)" |
  "valid (Suc n) s c Q = (if (c = Skip) then Q s else
                         (\<forall>s' c'. sem (s,c) (s',c') \<longrightarrow> valid n s' c' Q))"

lemma valid_Suc:
  "valid (Suc n) s c Q \<Longrightarrow> valid n s c Q"
proof(induct n arbitrary: s c)
  case 0
  thus ?case by simp
next
  case (Suc n)
  show ?case
  proof(clarsimp, safe)
    assume "c = Skip"
    with `valid (Suc (Suc n)) s c Q`
      show "Q s"
      by simp
  next
    fix s' c'
    assume "c \<noteq> Skip" and
           "sem (s,c) (s',c')"
    with `valid (Suc (Suc n)) s c Q` Suc(1)
    show "valid n s' c' Q"
      by (auto split: if_splits)
  qed
qed

lemma derived_valid:
  "(\<forall>p P Q c. annotations p = (P,Q) \<longrightarrow> procenv p = c \<longrightarrow> derived P c Q) \<Longrightarrow> 
   derived P c Q \<Longrightarrow> P s \<Longrightarrow> valid n s c Q"
proof(induct n arbitrary: P Q c s)
  case 0
  have "c = Skip \<longrightarrow> Q s"
    using `derived P c Q` `P s` derived_SkipE by auto
  thus ?case
    by simp
next
  case (Suc n)
  show ?case
  proof -
    from `derived P c Q` `P s` show "valid (Suc n) s c Q"
    proof(induct P c Q rule: derived.induct)
      case (derived_Skip P)
      thus ?case
        by simp
    next
      case (derived_Call p P Q)
      show ?case
      proof(clarsimp)
        fix s' c'
        assume "sem (s,(Call p)) (s',c')"
        hence [simp]: "s' = s \<and> c' = procenv p"
          using sem_CallE by blast
        have "valid n s (procenv p) Q"
        proof -
          have "derived P (procenv p) Q"
            using Suc(2) derived_Call by simp
          from Suc(1)[OF Suc(2), OF this] `P s` show ?thesis by blast
        qed
        thus "valid n s' c' Q" by simp
      qed
    next
      case (derived_Cond P b c Q c')
      show ?case
      proof(clarsimp)
        fix s' c''
        assume a: "sem (s,(Cond b c c')) (s',c'')"
        have [simp]: "s' = s \<and> c'' = (if (bexpr_eval b s) then c else c')"
          using sem_CondE[OF a] by blast
        from `P s` derived_Cond(2) derived_Cond(4) valid_Suc show "valid n s' c'' Q"
        by auto 
      qed
    qed
  qed
qed

definition
  partial_correct :: "(state \<Rightarrow> bool) \<Rightarrow> com \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> bool"
where
  "partial_correct P c Q \<equiv> \<forall>s s'. P s \<and> sem\<^sup>*\<^sup>* (s,c) (s',Skip) \<longrightarrow> Q s'"

lemma semn_partial_correct:
  "\<forall>s s' n. P s \<and> (sem^^n) (s,c) (s',Skip) \<longrightarrow> Q s' \<Longrightarrow>
  partial_correct P c Q"
  apply(clarsimp simp: partial_correct_def)
  using rtranclp_imp_relpowp
  by fastforce

lemma valid_semn:
  "valid n s c Q \<Longrightarrow> (sem^^n) (s,c) (s',Skip) \<Longrightarrow> Q s'"
proof(induct n arbitrary: s c)
  case 0
  thus ?case by simp
next
  case (Suc n)
  from `(sem ^^ Suc n) (s, c) (s', Skip)` 
  obtain s'' c'' 
  where step: "sem (s,c) (s'',c'')" and stepn: "(sem ^^ n) (s'',c'') (s',Skip)"
    using relpowp_Suc_D2 by fastforce
  from step have "c \<noteq> Skip" using sem.cases by blast
  with step `valid (Suc n) s c Q` have "valid n s'' c'' Q"
    by simp
  with stepn Suc(1) show "Q s'" by blast
qed

lemma valid_is_partial_correct:
  "\<forall>s. P s \<longrightarrow> (\<forall>n. valid n s c Q) \<Longrightarrow> partial_correct P c Q"
  apply(rule semn_partial_correct)
  using valid_semn by metis

lemma derived_partial_correct:
  "(\<forall>p P Q c. annotations p = (P,Q) \<longrightarrow> procenv p = c \<longrightarrow> derived P c Q) \<Longrightarrow> 
   derived P c Q \<Longrightarrow> partial_correct P c Q"
  apply(rule valid_is_partial_correct)
  using derived_valid by metis


end