Theory Labeled_Hoare

theory Labeled_Hoare
imports
  "../../Case_Labeling"
  "HOL-Hoare.Hoare_Logic"
begin

subsection ‹A labeling VCG for HOL/Hoare›

context begin
  interpretation Labeling_Syntax .

  lemma LSeqRule:
    assumes "C⟨IC,CT,OC1: Valid P c1 a1 Q⟩"
      and "C⟨Suc OC1,CT,OC: Valid Q c2 a2 R⟩"
    shows "C⟨IC,CT,OC: Valid P (Seq c1 c2) (Aseq a1 a2) R⟩"
    using assms unfolding LABEL_simps by (rule SeqRule)

  lemma LSkipRule:
    assumes "V⟨(''weaken'', IC, []),CT: p ⊆ q⟩"
    shows "C⟨IC,CT,IC: Valid p SKIP a q⟩"
    using assms unfolding LABEL_simps  by (rule SkipRule)

  lemmas LAbortRule = LSkipRule  ― ‹dummy version›

  lemma LBasicRule:
    assumes "V⟨(''basic'', IC, []),CT: p ⊆ {s. f s ∈ q}⟩"
    shows "C⟨IC,CT,IC: Valid p (Basic f) a q⟩"
    using assms unfolding LABEL_simps  by (rule BasicRule)

  lemma LCondRule:
    fixes IC CT defines "CT' ≡ (''cond'', IC, []) # CT "
    assumes "V⟨(''vc'', IC, []),(''cond'', IC, []) # CT: p ⊆ {s. (s ∈ b ⟶ s ∈ w) ∧ (s ∉ b ⟶ s ∈ w')}⟩"
      and "C⟨Suc IC,(''then'', IC, []) # (''cond'', IC, []) # CT,OC1: Valid w c1 a1 q⟩"
      and "C⟨Suc OC1,(''else'', Suc OC1, []) # (''cond'', IC, []) # CT,OC: Valid w' c2 a2 q⟩"
    shows "C⟨IC,CT,OC: Valid p (Cond b c1 c2) (Acond a1 a2) q⟩"
    using assms(2-) unfolding LABEL_simps by (rule CondRule)

  lemma LWhileRule:
    fixes IC CT defines "CT' ≡ (''while'', IC, []) # CT"
    assumes "V⟨(''precondition'', IC, []),(''while'', IC, []) # CT: p ⊆ i⟩"
      and "C⟨Suc IC,(''invariant'', Suc IC, []) # (''while'', IC, []) # CT,OC: Valid (i ∩ b) c (A 0) i⟩"
      and "V⟨(''postcondition'', IC, []),(''while'', IC, []) # CT: i ∩ - b ⊆ q⟩"
    shows "C⟨IC,CT,OC: Valid p (While b c) (Awhile i v A) q⟩"
    using assms(2-) unfolding LABEL_simps  by (rule WhileRule)

  lemma LABELs_to_prems:
    "(C⟨IC, CT, OC: True⟩ ⟹ P) ⟹ C⟨IC, CT, OC: P⟩"
    "(V⟨x, ct: True⟩ ⟹ P) ⟹ V⟨x, ct: P⟩"
    unfolding LABEL_simps by simp_all

  lemma LABELs_to_concl:
    "C⟨IC, CT, OC: True⟩ ⟹ C⟨IC, CT, OC: P⟩ ⟹ P"
    "V⟨x, ct: True⟩ ⟹ V⟨x, ct: P⟩ ⟹ P"
    unfolding LABEL_simps .

end


ML_file ‹labeled_hoare_tac.ML›

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

method_setup labeled_vcg_simp = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Labeled_Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))›
  "verification condition generator"

method_setup casified_vcg = ‹
  Scan.lift (Casify.casify_options casify_defs) >>
    (fn opt => fn ctxt => Util.SIMPLE_METHOD_CASES (
      HEADGOAL (Labeled_Hoare.hoare_tac ctxt (K all_tac))
      THEN_CONTEXT Casify.casify_tac opt))
›

method_setup casified_vcg_simp = ‹
  Scan.lift (Casify.casify_options casify_defs) >>
    (fn opt => fn ctxt => Util.SIMPLE_METHOD_CASES (
      HEADGOAL (Labeled_Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt))
      THEN_CONTEXT Casify.casify_tac opt))
›

end