Theory PhiSem_CF_Breakable

theory PhiSem_CF_Breakable
  imports PhiSem_CF_Break PhiSem_CF_Basic
begin

(*declare [[φhide_techinicals=false]]*)

text ‹Since we have ▩‹break› and ▩‹continue› now, the termination condition of a loop is not
  necessarily the negative of the loop guard. Therefore here we need 3 assertions, invariance,
  guard, and termination condition.›

proc while:
  requires ‹𝗉𝖺𝗋𝖺𝗆 (X x 𝗌𝗎𝖻𝗃 x. Inv: invariant x ∧ Guard: cond x ∧ End: termination x)›
  and S: ‹U 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ((X x 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R) 𝗌𝗎𝖻𝗃 x. invariant x)›
  and ‹𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (∀x. invariant x ∧ ¬ cond x ⟶ termination x)›
  and C: "⋀x. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 invariant x ⟹
                  𝗉𝗋𝗈𝖼 Cond ⦃ X x❟ R ⟼ 𝗏𝖺𝗅 cond x' ⦂ 𝔹❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1"
  and B: "⋀x lb lc. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 invariant x ⟹
                    𝗉𝗋𝖾𝗆𝗂𝗌𝖾 cond x ⟹
                    break_φapp❙: TECHNICAL
                        𝗉𝗋𝗈𝖼 op_break TYPE(unit) TYPE(unit) lb φV_none
                           ⦃ TECHNICAL Brk_Frame lb❟ (TECHNICAL Brk_Frame lc❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x' ∧ termination x') ⟼ 0 ⦄
                        𝗍𝗁𝗋𝗈𝗐𝗌 (λ_. Brking_Frame lb (λ_::unit φarg. TECHNICAL Brk_Frame lc❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x' ∧ termination x')) ⟹
                    continue_φapp❙: TECHNICAL
                        𝗉𝗋𝗈𝖼 op_break TYPE(unit) TYPE(unit) lc φV_none
                           ⦃ TECHNICAL Brk_Frame lc❟ (TECHNICAL Brk_Frame lb❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x') ⟼ 0 ⦄
                        𝗍𝗁𝗋𝗈𝗐𝗌 (λ_. Brking_Frame lc (λ_::unit φarg. TECHNICAL Brk_Frame lb❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x')) ⟹
                    𝗉𝗋𝗈𝖼 Body lb lc
                        ⦃ TECHNICAL Brk_Frame lb❟ TECHNICAL Brk_Frame lc❟ X x❟ R
                      ⟼ TECHNICAL Brk_Frame lb❟ TECHNICAL Brk_Frame lc❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x'
                         ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. 𝖻𝗋𝖾𝖺𝗄 lb 𝗐𝗂𝗍𝗁 (λ_::unit φarg. TECHNICAL Brk_Frame lc❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x' ∧ termination x')
                                    𝗈𝗋 𝖻𝗋𝖾𝖺𝗄 lc 𝗐𝗂𝗍𝗁 (λ_::unit φarg. X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x')
                                    𝗈𝗋 E2 e)"
  input ‹U›
  output ‹R❟ X x 𝗌𝗎𝖻𝗃 x. invariant x ∧ termination x›
  throws ‹E1 + E2›
  ❴ S
    op_brk_scope ❴ for lb
      PhiSem_CF_Basic.while ‹X x❟ R❟ TECHNICAL Brk_Frame lb 𝗌𝗎𝖻𝗃 x. Inv: invariant x ∧ Guard: cond x›
      ❴ C ❵
      ❴ op_brk_scope ❴ for lc 
          apply_rule B[where lb1=lb]
          apply_rule op_break[THEN Technical_I, THEN Labelled_I]
          apply_rule op_break[THEN Technical_I, THEN Labelled_I] ；
        ❵ for ‹TECHNICAL Brk_Frame lc❟ (TECHNICAL Brk_Frame lb❟ X x'❟ R 𝗌𝗎𝖻𝗃 x'. invariant x')› ；
      ❵ ；
    ❵ for ‹(R❟ X x' 𝗌𝗎𝖻𝗃 x'. invariant x' ∧ termination x')❟ TECHNICAL Brk_Frame lb› ；
  ❵.

hide_const (open) PhiSem_CF_Basic.while

lemmas while'_φapp = PhiSem_CF_Basic.while_φapp ― ‹Non-breaking while loop›


subsection ‹Syntax›

optional_translations (do_notation)
  "_while_ C B" <= "CONST PhiSem_CF_Breakable.while C B"

syntax "_continue_" :: ‹do_bind› ("𝖼𝗈𝗇𝗍𝗂𝗇𝗎𝖾")
       "_break_" :: ‹do_bind› ("𝖻𝗋𝖾𝖺𝗄")

print_ast_translation ‹let open Ast
  fun get_label (Appl [Constant "_constrain", BV, _]) = get_label BV
    | get_label (Appl [Constant "_bound", Variable bv]) = bv
  fun is_label lb (Appl [Constant "_constrain", BV, _]) = is_label lb BV
    | is_label lb (Appl [Constant "_bound", Variable bv]) = bv = lb
  fun tr (lc,lb) (tm as Appl [Constant \<^const_syntax>‹PhiSem_CF_Break.op_break›, _, _, BV, _]) =
        if is_label lc BV
        then Constant \<^syntax_const>‹_continue_›
        else if is_label lb BV
        then Constant \<^syntax_const>‹_break_›
        else tm
    | tr lbc (Appl aps) = Appl (map (tr lbc) aps)
    | tr _ X = X
  fun tr0 cfg (Appl [Constant \<^syntax_const>‹_do_block›, X]) = tr cfg X
    | tr0 cfg X = tr cfg X
in [
  (\<^syntax_const>‹_while_›, fn ctxt =>
    fn [C, Appl [Constant "_abs", lb0, Appl [Constant "_abs", lc0, X]]] =>
      if Syntax_Group.is_enabled (Proof_Context.theory_of ctxt) @{syntax_group do_notation}
      then Appl [Constant \<^syntax_const>‹_while_›, C, tr0 (get_label lc0, get_label lb0) X]
      else raise Match)
] end›


end