Theory breakcontinue

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory breakcontinue
imports "AutoCorres2.CTranslation"
begin

declare sep_conj_ac [simp add]

install_C_file "breakcontinue.c"

context breakcontinue_simpl
begin

thm f_body_def
thm g_body_def
thm h_body_def
thm i_body_def
thm dotest_body_def
end

context h_impl
begin
term "⦃ -10 <=s ´e & ´e <s 0 ⦄"
end
lemma (in h_impl) h:
  "Γ ⊢ ⦃ -10 <=s ´e & ´e <s 0 ⦄
  ´ret' :== PROC h(´e)
  ⦃ ´ret' = ´e ⦄"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (hoare_rule HoarePartial.Catch [where R = "⦃ ´ret' = ´e & is_local ´global_exn_var'⦄"])
  defer
   apply vcg
   apply simp
apply (hoare_rule HoarePartial.conseq
           [where P' = "λe. ⦃ ´e = e & e <s 0 & -10 <=s e ⦄"
            and Q' = "λe. ⦃ ´e = e & ´ret' = e & is_local ´global_exn_var'⦄"
            and A' = "λe. ⦃ ´e = e & ´ret' = e & is_local ´global_exn_var'⦄"])
  defer
  apply (simp add: subset_iff)
apply (rule allI)
apply (rule_tac R="{}" in HoarePartial.Seq)
  defer
   apply vcg
  apply (rule Seq_propagate_precond)
  apply (vcg, simp)
apply (rule_tac R="⦃ ´e = Z ⦄" in HoarePartial.Seq)
  defer
   apply (vcg, simp)

apply (rule_tac R = "⦃ ´e = Z & ´global_exn_var' = Break ⦄" in HoarePartial.Catch)
  defer

  apply (vcg, simp)
  apply simp
apply (rule_tac P' = "⦃ ´e = Z & Z <s 0 & -10 <=s Z ⦄"
            and Q' = "⦃ ´e = Z & Z <s 0 & -10 <=s Z ⦄ ∩ - ⦃ ´e <s 10 ⦄"
            and A' = "⦃ ´e = Z & ´global_exn_var' = Break ⦄"
         in HoarePartial.conseq_no_aux)
  defer
  apply simp
apply (simp add: whileAnno_def)
apply (rule HoarePartialDef.While)
apply vcg
apply (simp add: subset_iff)
done

(* another example where vcg fails, generating impossible sub-goals *)
lemma (in dotest_impl) dotest:
  "Γ ⊢ ⦃ ´x = 4 ⦄ ´ret' :== PROC dotest(´x)
       ⦃ ´ret' = 4 ⦄"
apply (hoare_rule HoarePartial.ProcNoRec1)
apply (hoare_rule HoarePartial.Catch [where R="⦃ ´ret' = 4 & is_local ´global_exn_var'⦄"])
   apply (hoare_rule HoarePartial.Seq [where R="{}"])
    apply (rule Seq_propagate_precond)
  apply (vcg, simp)
    apply (hoare_rule HoarePartial.Seq [where R="⦃ ´x = 4 ⦄"])
      apply (hoare_rule HoarePartial.Catch [where R="⦃ ´x = 4 & ´global_exn_var' = Break ⦄"])
        apply (hoare_rule HoarePartial.Seq [where R="⦃ False ⦄"])
          apply (vcg, simp)
        apply (hoare_rule HoarePartial.conseq_exploit_pre, simp)
      apply (vcg, simp)
    apply (vcg, simp)
  apply vcg
apply (vcg, simp)
done

end