Theory Calculus_of_Programming

chapter β€ΉCalculus of Programmingβ€Ί

theory Calculus_of_Programming
  imports Spec_Framework IDE_CP_Reasoning1
  abbrevs "<state>" = "π—Œπ—π–Ίπ—π–Ύ"
      and "<results>" = "π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ"
      and "<in>" = "𝗂𝗇"
      and "<is>" = "π—‚π—Œ"
begin

section β€ΉImplementing CoP Sequentβ€Ί

text β€ΉCoP sequent β€ΉP | S |- Qβ€Ί for β€ΉS = (C1,v1); β‹― ; (Cn,vn)β€Ί is implemented as
\begin{align*}
& β€Ήπ–Όπ—Žπ—‹π—‹π–Ύπ—‡π— s0 [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 Pβ€Ί, \\
& β€ΉCode s0 s1 C1 v1,β€Ί         \\
&     \qquad β€Ήβ‹―β€Ί                 \\
& β€ΉCode si-1 si Ci vi,β€Ί       \\
&     \qquad β€Ήβ‹―β€Ί                 \\
& β€ΉCode sn-1 sn Cn vnβ€Ί        \\
β€ΉβŠ’β€Ί \;&\; β€Ήπ–Όπ—Žπ—‹π—‹π–Ύπ—‡π— sn [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 Qβ€Ί
\end{align*}
where β€Ήs0β€Ί denotes the initial state before execution and β€Ήsi, viβ€Ί denote
respectively the intermediate state after executing procedure β€ΉCiβ€Ί and
the return value of β€ΉCiβ€Ί.
Sequence β€Ή{si}nβ€Ί therefore links execution of each procedure.
β€ΉRβ€Ί is the frame variable.

[C]-modality β€Ή[C]{Q}{E}β€Ί is implemented by ‹𝗉𝖾𝗇𝖽𝗂𝗇𝗀 C π—ˆπ—‡ sn [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 Q π—π—π—‹π—ˆπ—π—Œ Eβ€Ί.

β€Ί

text β€Ή
In addition, besides programming of procedures,
the system is extended to deduce view shift and transformation of abstraction by programming.

The programming deduction of view shift is also realized using similar structures
(β€ΉCurrentConstructionβ€Ί). Thus we reuse the infrastructures and
give two modes β€Ήprogramming_modeβ€Ί and β€Ήview_shift_modeβ€Ί to differentiate the two modes.
β€Ί

consts programming_mode :: mode
       view_shift_mode  :: mode

definition CurrentConstruction :: " mode β‡’ resource β‡’ assn β‡’ assn β‡’ bool "
  where "CurrentConstruction mode s R S ⟷ s ⊨ INTERP_SPEC (S * R)"

abbreviation Programming_CurrentConstruction ("(2π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— _ [_] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇/ _)" [1000,1000,11] 10)
  where β€ΉProgramming_CurrentConstruction ≑ CurrentConstruction programming_modeβ€Ί

abbreviation View_Shift_CurrentConstruction ("(2𝗏𝗂𝖾𝗐 _ [_] π—‚π—Œ/ _)" [1000,1000,11] 10)
  where β€ΉView_Shift_CurrentConstruction ≑ CurrentConstruction view_shift_modeβ€Ί

consts Programming_CurrentConstruction_syntax :: β€Ήassn β‡’ boolβ€Ί ("(2π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— π—Œπ—π–Ίπ—π–Ύ:/ (β€Ήconsistent=trueβ€Ί_))" [11] 10)
consts View_Shift_CurrentConstruction_syntax :: β€Ήassn β‡’ boolβ€Ί ("(2π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— 𝗏𝗂𝖾𝗐:/ _)" [11] 10)

definition PendingConstruction :: " 'ret proc
                                  β‡’ resource
                                  β‡’ assn
                                  β‡’ ('ret Ο†arg β‡’ assn)
                                  β‡’ (ABNM β‡’ assn)
                                  β‡’ bool "
    ("𝗉𝖾𝗇𝖽𝗂𝗇𝗀 _ π—ˆπ—‡ _ [_]/ π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 _/ π—π—π—‹π—ˆπ—π—Œ _" [1000,1000,1000,11,11] 10)
    where "PendingConstruction f s R S E ⟷
              BI_lift (f s) ≀ LooseState (Ξ»ret. INTERP_SPEC (S ret * R)) (Ξ»ex. INTERP_SPEC (E ex * R))"

consts PendingConstruction_syntax :: β€Ή'ret proc β‡’ ('ret Ο†arg β‡’ assn) β‡’ (ABNM β‡’ assn) β‡’ boolβ€Ί
  ("𝗉𝖾𝗇𝖽𝗂𝗇𝗀 π—‰π—‹π—ˆπ–Ό _/ π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 _/ π—π—π—‹π—ˆπ—π—Œ _" [1000,11,11] 10)

translations
  "π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— π—Œπ—π–Ίπ—π–Ύ: S" <= "CONST Programming_CurrentConstruction s R S"
  "π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— 𝗏𝗂𝖾𝗐: S" <= "CONST View_Shift_CurrentConstruction s R S"
  "𝗉𝖾𝗇𝖽𝗂𝗇𝗀 π—‰π—‹π—ˆπ–Ό f π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 S π—π—π—‹π—ˆπ—π—Œ E" <= "CONST PendingConstruction f s R S E"

definition β€ΉCode s s' f ret ⟷ Success ret s' ∈ f sβ€Ί

lemma CurrentConstruction_D: "CurrentConstruction mode s H T ⟹ Satisfiable T"
  unfolding CurrentConstruction_def Satisfiable_def
  by (clarsimp simp add: INTERP_SPEC set_mult_expn, blast)

definition ToA_Construction :: β€Ή'a β‡’ 'a BI β‡’ boolβ€Ί ("π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡'(_') π—‚π—Œ/ _" [11,11] 10)
  where β€ΉToA_Construction = (⊨)β€Ί


subsection β€ΉReasoning Configurationβ€Ί

subsubsection β€ΉSimplificationβ€Ί

Ο†reasoner_ML Ο†programming_simps (β€Ήπ—Œπ—‚π—†π—‰π—…π—‚π–Ώπ—’[programming_mode] _ : _β€Ί) =
  β€Ήfn (_, (ctxt,sequent)) => Seq.make (fn () =>
    let val lev = Config.get ctxt Phi_Reasoner.auto_level
     in if lev <= 0
     then SOME ((ctxt, @{thm' Simplify_I} RS sequent), Seq.empty)
     else sequent
        |> PLPR_Simplifier.simplifier (K Seq.empty) (equip_Phi_Programming_Simp lev) {fix_vars=false} ctxt
        |> Seq.map (pair ctxt)
        |> Seq.pull
    end)β€Ί

section β€ΉRules for Constructing Programsβ€Ί

subsection β€ΉConstruct Procedureβ€Ί

lemma Ο†apply_proc:
  "(π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— blk [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 S)
⟹ π—‰π—‹π—ˆπ–Ό f ⦃ S ⟼ T ⦄ π—π—π—‹π—ˆπ—π—Œ E
⟹(𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E)"
  unfolding Ο†Procedure_def CurrentConstruction_def PendingConstruction_def bind_def Satisfaction_def
  by (simp add: mult.commute)

lemma
  β€Ή (βˆƒs' x. Code s  s'  f x ∧ Code s' s'' (g x) y)
⟷ Code s  s'' (f “ g) yβ€Ί
  unfolding Code_def bind_def
  apply (rule; clarsimp)
  apply blast
  by (case_tac x; clarsimp; blast)


(*Hint: because
𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 U π—π—π—‹π—ˆπ—π—Œ E1 ⟢
  Invalid βˆ‰ f s ∧ (βˆ€v s'. Abnormal v s' ∈ f s ⟢ s' ∈ INTERP_SPEC (R ❟ E v))*)

lemma Ο†assemble_proc:
  β€Ή 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E1
⟹ (β‹€s' ret. Code s s' f ret ⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 (g ret) π—ˆπ—‡ s' [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 U π—π—π—‹π—ˆπ—π—Œ E2)
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 (f “ g) π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 U π—π—π—‹π—ˆπ—π—Œ E1 + E2β€Ί
  unfolding CurrentConstruction_def PendingConstruction_def bind_def less_eq_BI_iff Code_def
  apply clarsimp subgoal for s s'
  by (cases s; simp; cases s'; simp add: split_comp_All ring_distribs plus_fun) .




lemma Ο†accept_proc:
  β€Ή 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E
⟹ Code s s' f ret
⟹ π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— s' [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T retβ€Ί
  unfolding PendingConstruction_def bind_def less_eq_BI_iff CurrentConstruction_def Code_def
  by blast

lemma Ο†accept_proc_optimize_return_v:
  β€Ή 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 (Return v) π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E
⟹ π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T vβ€Ί
  unfolding PendingConstruction_def bind_def less_eq_BI_iff CurrentConstruction_def Return_def det_lift_def
  by simp


(* lemma Ο†accept_proc: ― β€ΉDepreciated!β€Ί
  " 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E1
⟹ (β‹€s' ret. π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— s' [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T ret ⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 (g ret) π—ˆπ—‡ s' [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 U π—π—π—‹π—ˆπ—π—Œ E2)
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 (f “ g) π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 U π—π—π—‹π—ˆπ—π—Œ E1 + E2"
  unfolding CurrentConstruction_def PendingConstruction_def bind_def subset_iff plus_fun_def
  apply clarsimp subgoal for s' s'' by (cases s'; simp; cases s''; simp add: ring_distribs; blast) .*)

(*
lemma Ο†return_when_unreachable:
  β€Ή 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 (Ξ»_. T) π—π—π—‹π—ˆπ—π—Œ E
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 (f βͺ’ Return (Ο†arg undefined)) π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 (Ξ»_. T) π—π—π—‹π—ˆπ—π—Œ Eβ€Ί
  for f :: β€Ήunreachable procβ€Ί
  unfolding CurrentConstruction_def PendingConstruction_def bind_def Return_def det_lift_def subset_iff
  apply clarsimp subgoal for s' s'' by (cases s'; simp; cases s''; simp add: ring_distribs; blast) .
*)
lemma Ο†return_additional_unit:
  β€Ή 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 (f “ (Ξ»v. Return (Ο†V_pair v Ο†V_none))) π—ˆπ—‡ s [R]
        π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 (Ξ»ret. T (Ο†V_fst ret)) π—π—π—‹π—ˆπ—π—Œ Eβ€Ί
  unfolding CurrentConstruction_def PendingConstruction_def bind_def Return_def Ο†V_pair_def
    Ο†V_fst_def Ο†V_snd_def det_lift_def less_eq_BI_iff
  apply clarsimp subgoal for s' s'' by (cases s'; simp; cases s''; simp add: ring_distribs; blast) .

lemma Ο†return:
  " π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T'
⟹ T' = T ret
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 (Return ret) π—ˆπ—‡ s [R] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ 0"
  unfolding CurrentConstruction_def PendingConstruction_def bind_def Return_def det_lift_def less_eq_BI_iff
  by simp+

lemma Ο†reassemble_proc_final:
  "(β‹€s H. π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— s [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 S ⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 g π—ˆπ—‡ s [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E)
⟹ π—‰π—‹π—ˆπ–Ό g ⦃ S ⟼ T ⦄ π—π—π—‹π—ˆπ—π—Œ E"
  unfolding CurrentConstruction_def PendingConstruction_def Ο†Procedure_def bind_def split_paired_all
  by (simp add: mult.commute)

lemma "Ο†__Return_rule__":
  β€Ή X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 Any
⟹ π—‰π—‹π—ˆπ–Ό Return Ο†V_none ⦃ X ⟼ Ξ»_::unit Ο†arg. Y ⦄›
  unfolding Ο†Procedure_def Return_def View_Shift_def less_eq_BI_iff det_lift_def
  by clarsimp

subsection β€ΉConstruct View Shiftβ€Ί

lemma Ο†make_view_shift:
  β€Ή (β‹€s R. 𝗏𝗂𝖾𝗐 s [R] π—‚π—Œ S ⟹ (𝗏𝗂𝖾𝗐 s [R] π—‚π—Œ S' π—Œπ—Žπ–»π—ƒ P))
⟹ S π—Œπ—π—‚π–Ώπ—π—Œ S' 𝗐𝗂𝗍𝗁 Pβ€Ί
  unfolding CurrentConstruction_def View_Shift_def
  by (simp add: INTERP_SPEC_subj)


subsection β€ΉConstruct Implicationβ€Ί

lemma "Ο†make_implication":
  β€Ή(β‹€x. π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ S ⟹ π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ T π—Œπ—Žπ–»π—ƒ P) ⟹ S π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ T 𝗐𝗂𝗍𝗁 Pβ€Ί
  unfolding Transformation_def ToA_Construction_def
  by simp

subsection β€ΉCastβ€Ί

lemma Ο†apply_view_shift:
  " CurrentConstruction mode blk R S
⟹ S π—Œπ—π—‚π–Ώπ—π—Œ S' 𝗐𝗂𝗍𝗁 P
⟹ (CurrentConstruction mode blk R S') ∧ P"
  unfolding CurrentConstruction_def View_Shift_def
  by (simp_all add: split_paired_all)

lemmas Ο†apply_implication = Ο†apply_view_shift[OF _ view_shift_by_implication]

lemma Ο†apply_view_shift_pending:
  " PendingConstruction f blk H T E
⟹ (β‹€x. T x π—Œπ—π—‚π–Ώπ—π—Œ T' x 𝗐𝗂𝗍𝗁 P)
⟹ PendingConstruction f blk H T' E"
  unfolding PendingConstruction_def View_Shift_def
  by (clarsimp simp add: LooseState_expn' less_eq_BI_iff split_comp_All)

lemma Ο†apply_view_shift_pending_E:
  " PendingConstruction f blk H T E
⟹ (β‹€x. E x π—Œπ—π—‚π–Ώπ—π—Œ E' x 𝗐𝗂𝗍𝗁 P)
⟹ PendingConstruction f blk H T E'"
  unfolding PendingConstruction_def View_Shift_def
  by (clarsimp simp add: LooseState_expn' less_eq_BI_iff split_comp_All)

lemmas Ο†apply_implication_pending =
  Ο†apply_view_shift_pending[OF _ view_shift_by_implication]

lemmas Ο†apply_implication_pending_E =
  Ο†apply_view_shift_pending_E[OF _ view_shift_by_implication]

lemma Ο†ex_quantify_E:
  β€Ή 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ (E ret)
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ (Ξ»e. ExBI (Ξ»x. E x e))β€Ί
  using Ο†apply_implication_pending_E[OF _ ExBI_transformation_I[OF transformation_refl]] .

lemma Ο†apply_implication_impl:
  β€Ή π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(s) π—‚π—Œ S
⟹ S π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ S' 𝗐𝗂𝗍𝗁 P
⟹(π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(s) π—‚π—Œ S') ∧ Pβ€Ί
  unfolding ToA_Construction_def Transformation_def by blast

lemma "_Ο†cast_internal_rule_":
  " CurrentConstruction mode blk H T
⟹ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ T' 𝗐𝗂𝗍𝗁 Any
⟹ 𝗋Success
⟹ π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True
⟹ CurrentConstruction mode blk H T'"
  unfolding Action_Tag_def
  using Ο†apply_implication by blast


lemma "_Ο†cast_internal_rule_'":
  " 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E
⟹ (β‹€v. T v π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ T' v 𝗐𝗂𝗍𝗁 Any)
⟹ 𝗋Success
⟹ π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T' π—π—π—‹π—ˆπ—π—Œ E"
  unfolding Action_Tag_def
  using Ο†apply_implication_pending by blast

lemma "_Ο†cast_exception_":
  " 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E
⟹ (β‹€v. E v π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ E' v)
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E'"
  unfolding Action_Tag_def
  using Ο†apply_implication_pending_E by blast

lemma "_Ο†cast_exception_rule_":
  " 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E
⟹ (β‹€v. E v π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ E' v)
⟹ 𝗋Success
⟹ π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 T π—π—π—‹π—ˆπ—π—Œ E'"
  using "_Ο†cast_exception_" .

lemma "_Ο†cast_implication_":
  β€Ή π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ S
⟹ S π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ T 𝗐𝗂𝗍𝗁 Any
⟹ 𝗋Success
⟹ π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True
⟹ π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ Tβ€Ί
  unfolding ToA_Construction_def Action_Tag_def Transformation_def by blast

lemma "_Ο†cast_proc_return_internal_rule_":
  " π—‰π—‹π—ˆπ–Ό f ⦃ X ⟼ Y ⦄ π—π—π—‹π—ˆπ—π—Œ E
⟹ (β‹€v. Y v π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y' v 𝗐𝗂𝗍𝗁 Any)
⟹ 𝗋Success
⟹ π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True
⟹ π—‰π—‹π—ˆπ–Ό f ⦃ X ⟼ Y' ⦄ π—π—π—‹π—ˆπ—π—Œ E"
  unfolding Action_Tag_def
  using Ο†CONSEQ view_shift_by_implication view_shift_refl by blast

lemma "_Ο†cast_proc_exception_internal_rule_":
  " π—‰π—‹π—ˆπ–Ό f ⦃ X ⟼ Y ⦄ π—π—π—‹π—ˆπ—π—Œ E
⟹ (β‹€e. E e π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ E' e 𝗐𝗂𝗍𝗁 Any)
⟹ 𝗋Success
⟹ π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True
⟹ π—‰π—‹π—ˆπ–Ό f ⦃ X ⟼ Y ⦄ π—π—π—‹π—ˆπ—π—Œ E'"
  unfolding Action_Tag_def
  using Ο†CONSEQ view_shift_by_implication view_shift_refl by blast


subsection β€ΉFinalization Rewritesβ€Ί

text β€ΉRules showing the obtained procedure is identical to the desired goal
  in the end of the construction.β€Ί

ML β€Ήstructure Proc_Monad_SS = Simpset(
  val initial_ss = Simpset_Configure.Minimal_SS
  val binding = SOME bindingβ€Ήprocedure_simpsβ€Ί
  val comment = "declare the rules for simplifying procedure monad."
  val attribute = NONE
  val post_merging = I
)β€Ί

setup β€ΉContext.theory_map (Proc_Monad_SS.map (
  Simplifier.add_cong @{thm' mk_symbol_cong}
))β€Ί

consts procedure_ss :: mode

lemmas [procedure_simps] =
            proc_bind_SKIP proc_bind_SKIP'
            proc_bind_assoc proc_bind_return_none Ο†V_simps

Ο†reasoner_ML procedure_equivalence 1200 (β€ΉPremise procedure_ss ?Pβ€Ί)
  = β€ΉPhi_Reasoners.wrap (PLPR_Simplifier.simplifier_by_ss' (K Seq.empty) Proc_Monad_SS.get' {fix_vars=false}) o sndβ€Ί

Ο†reasoner_ML procedure_ss 1000 (β€ΉSimplify procedure_ss ?x ?yβ€Ί)
  = β€ΉPhi_Reasoners.wrap (PLPR_Simplifier.simplifier_by_ss' (K Seq.empty) Proc_Monad_SS.get' {fix_vars=true}) o sndβ€Ί

subsection β€ΉMiscβ€Ί

paragraph β€ΉInhabitanceβ€Ί

lemma ToA_Construction_Satisfiable_rule:
  β€Ήπ–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ S ⟹ Satisfiable Sβ€Ί
  unfolding ToA_Construction_def Satisfiable_def by blast

lemma CurrentConstruction_Satisfiable_rule:
  "CurrentConstruction mode s H T ⟹ Satisfiable T"
  using CurrentConstruction_D by blast


paragraph β€ΉFact Storeβ€Ί

lemma [Ο†programming_simps]:
  "CurrentConstruction mode s H (T π—Œπ—Žπ–»π—ƒ P) ⟷ (CurrentConstruction mode s H T) ∧ P"
  unfolding CurrentConstruction_def
  by (simp_all add: INTERP_SPEC_subj split_paired_all)

lemma [Ο†programming_simps]:
  "(CurrentConstruction mode s H T ∧ B) ∧ C ⟷ (CurrentConstruction mode s H T) ∧ (B ∧ C)"
  by simp

lemma [Ο†programming_simps]:
  β€Ή(π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ T π—Œπ—Žπ–»π—ƒ P) ⟷ (π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ T) ∧ Pβ€Ί
  unfolding ToA_Construction_def by simp

lemma [Ο†programming_simps]:
  β€Ή((π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ T) ∧ B) ∧ C ⟷ (π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(x) π—‚π—Œ T) ∧ (B ∧ C)β€Ί
  by simp

paragraph β€ΉFixing Existentially Quantified Variableβ€Ί

lemma Ο†ExTyp_strip:
  "(CurrentConstruction mode p H (βˆƒ*c. T c)) ≑ (βˆƒc. CurrentConstruction mode p H (T c))"
  unfolding CurrentConstruction_def atomize_eq
  by (simp_all add: INTERP_SPEC_ex split_paired_all)

lemma Ο†ExTyp_strip_imp:
  β€ΉToA_Construction s (βˆƒ*c. T c) ≑ (βˆƒc. ToA_Construction s (T c))β€Ί
  unfolding ToA_Construction_def by simp

paragraph β€ΉIntroducing Existential Quantificationβ€Ί

lemma introduce_Ex:
  β€ΉCurrentConstruction mode blk H (S x) ⟹ CurrentConstruction mode blk H (ExBI S)β€Ί
  using Ο†apply_implication[OF _ ExBI_transformation_I[OF transformation_refl], THEN conjunct1] .

lemma introduce_Ex_subj:
  β€ΉCurrentConstruction mode blk H (S x π—Œπ—Žπ–»π—ƒ Q) ⟹ CurrentConstruction mode blk H (ExBI S π—Œπ—Žπ–»π—ƒ Q)β€Ί
  by (metis Subjection_True Subjection_cong introduce_Ex)

lemma introduce_Ex_pending:
  β€Ή 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 (Ξ»v. Q x v) π—π—π—‹π—ˆπ—π—Œ E
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 (Ξ»v. βˆƒ*x. Q x v) π—π—π—‹π—ˆπ—π—Œ Eβ€Ί
  using Ο†apply_implication_pending[OF _ ExBI_transformation_I[OF transformation_refl]] .

lemma introduce_Ex_pending_E:
  β€Ή 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 Q π—π—π—‹π—ˆπ—π—Œ (Ξ»v. E x v)
⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f π—ˆπ—‡ blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 Q π—π—π—‹π—ˆπ—π—Œ (Ξ»v. βˆƒ*x. E x v)β€Ί
  using Ο†apply_implication_pending_E[OF _ ExBI_transformation_I[OF transformation_refl]] .

lemma introduce_Ex_ToA:
  β€Ή ToA_Construction s (S x)
⟹ ToA_Construction s (ExBI S) β€Ί
  using Ο†ExTyp_strip_imp by fastforce

lemma introduce_Ex_ToA_subj:
  β€Ή ToA_Construction s (S x π—Œπ—Žπ–»π—ƒ Q)
⟹ ToA_Construction s (ExBI S π—Œπ—Žπ–»π—ƒ Q) β€Ί
  by (metis (full_types) Subjection_Flase Subjection_True introduce_Ex_ToA)

lemma introduce_Ex_ToA_subj_P:
  β€Ή ToA_Construction s (X π—Œπ—Žπ–»π—ƒ S x)
⟹ ToA_Construction s (X π—Œπ—Žπ–»π—ƒ Ex S) β€Ί
  by (metis Subjection_expn ToA_Construction_def)
  


paragraph β€ΉReturnβ€Ί


lemma Ο†M_Success[intro!]: (*deprecated?*)
  β€Ή v ⊨ (y ⦂ T)
⟹ π—‰π—‹π—ˆπ–Ό Return (Ο†arg v) ⦃ X ⟼ Ξ»u. y ⦂ Val u T❟ X ⦄ π—π—π—‹π—ˆπ—π—Œ Any β€Ί
  unfolding Ο†Procedure_def det_lift_def Return_def
  by (clarsimp simp add: Val_def Ο†Type_def less_eq_BI_iff)

lemma Ο†M_Success_P:
  β€Ή v ⊨ (y ⦂ T)
⟹ P (Ο†arg v)
⟹ π—‰π—‹π—ˆπ–Ό Return (Ο†arg v) ⦃ X ⟼ Ξ»u. y ⦂ Val u T❟ X π—Œπ—Žπ–»π—ƒ P u ⦄ π—π—π—‹π—ˆπ—π—Œ Any β€Ί
  unfolding Ο†Procedure_def det_lift_def Return_def
  by (clarsimp simp add: Val_def Ο†Type_def INTERP_SPEC_subj less_eq_BI_iff)

declare Ο†M_Success[where X=1, simplified, intro!]

lemma Ο†M_Success'[intro!]:
  β€Ή π—‰π—‹π—ˆπ–Ό Return vs ⦃ X vs ⟼ X ⦄ π—π—π—‹π—ˆπ—π—Œ Any β€Ί
  unfolding Return_def Ο†Procedure_def det_lift_def less_eq_BI_iff by clarsimp

hide_const (open) Code

end