Theory PhiSem_CF_Routine_Basic

theory PhiSem_CF_Routine_Basic
  imports PhiSem_CF_Basic
begin

section ‹Routine›

text ‹Procedure in ‹φ›-system is a program segment, which does not correspond to a function
  in the target language necessarily. To model them, we formalize a specific semantic statement
  and we call them ∗‹routine› to distinguish with ∗‹procedure›.›

definition op_routine_basic :: ‹TY list ⇒ TY list ⇒ ('a::FIX_ARITY_VALs, 'b::FIX_ARITY_VALs) proc' ⇒ ('a,'b) proc'›
  where ‹op_routine_basic argtys rettys F = (λargs.
      φM_assert (args ∈ Well_Typed_Vals argtys)
   ⪢ F args
  ⤜ (λrets. φM_assert (rets ∈ Well_Typed_Vals rettys)
           ⪢ Return rets))›

lemma "__routine_basic__":
  ‹ Semantic_Types X TY_ARGs
⟹ Semantic_Types Y TY_RETs
⟹ 𝗋Success
⟹ (⋀(vs:: 'a::FIX_ARITY_VALs φarg <named> 'names).
          𝗉𝗋𝗈𝖼 F (case_named id vs) ⦃ X (case_named id vs) ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E)
⟹ 𝗉𝗋𝗈𝖼 op_routine_basic TY_ARGs TY_RETs F vs ⦃ X vs ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E›
  unfolding op_routine_basic_def Semantic_Types_i_def Semantic_Types_def named_All named.case id_apply
  by (rule φSEQ, rule φSEQ, rule φM_assert, blast, assumption, rule φSEQ,
      rule φM_assert, blast, rule φM_Success')

ML_file ‹library/cf_routine.ML›

attribute_setup routine_basic =
  ‹Scan.succeed (Phi_Modifier.wrap_to_attribute
                    (PhiSem_Control_Flow.routine_mod I (K I) @{thm "__routine_basic__"}))›



end