Theory OpUbx

theory OpUbx
  imports OpInl Unboxed
begin


section ‹n-ary operations›

locale nary_operations_ubx =
  nary_operations_inl 𝔒𝔭 𝔄𝔯𝔦𝔱𝔶 ℑ𝔫𝔩𝔒𝔭 ℑ𝔫𝔩 ℑ𝔰ℑ𝔫𝔩 𝔇𝔢ℑ𝔫𝔩 +
  unboxedval unitialized is_true is_false box_ubx1 unbox_ubx1 box_ubx2 unbox_ubx2
  for
    𝔒𝔭 :: "'op ⇒ 'dyn list ⇒ 'dyn" and 𝔄𝔯𝔦𝔱𝔶 and
    ℑ𝔫𝔩𝔒𝔭 and ℑ𝔫𝔩 and ℑ𝔰ℑ𝔫𝔩 and 𝔇𝔢ℑ𝔫𝔩 :: "'opinl ⇒ 'op" and
    unitialized :: 'dyn and is_true and is_false and
    box_ubx1 :: "'ubx1 ⇒ 'dyn" and unbox_ubx1 and
    box_ubx2 :: "'ubx2 ⇒ 'dyn" and unbox_ubx2 +
  fixes
    𝔘𝔟𝔵𝔒𝔭 :: "'opubx ⇒ ('dyn, 'ubx1, 'ubx2) unboxed list ⇒ ('dyn, 'ubx1, 'ubx2) unboxed option" and
    𝔘𝔟𝔵 :: "'opinl ⇒ type option list ⇒ 'opubx option" and
    𝔅𝔬𝔵 :: "'opubx ⇒ 'opinl" and
    𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭 :: "'opubx ⇒ type option list × type option"
  assumes
    𝔘𝔟𝔵_invertible:
      "𝔘𝔟𝔵 opinl ts = Some opubx ⟹ 𝔅𝔬𝔵 opubx = opinl" and
    𝔘𝔟𝔵𝔒𝔭_correct:
      "𝔘𝔟𝔵𝔒𝔭 opubx Σ = Some z ⟹ ℑ𝔫𝔩𝔒𝔭 (𝔅𝔬𝔵 opubx) (map norm_unboxed Σ) = norm_unboxed z" and
    𝔘𝔟𝔵𝔒𝔭_to_ℑ𝔫𝔩:
      "𝔘𝔟𝔵𝔒𝔭 opubx Σ = Some z ⟹ ℑ𝔫𝔩 (𝔇𝔢ℑ𝔫𝔩 (𝔅𝔬𝔵 opubx)) (map norm_unboxed Σ) = Some (𝔅𝔬𝔵 opubx)" and
    
    𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭_𝔄𝔯𝔦𝔱𝔶:
      "𝔄𝔯𝔦𝔱𝔶 (𝔇𝔢ℑ𝔫𝔩 (𝔅𝔬𝔵 opubx)) = length (fst (𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭 opubx))" and
    𝔘𝔟𝔵_opubx_type:
      "𝔘𝔟𝔵 opinl ts = Some opubx ⟹ fst (𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭 opubx) = ts" and

    𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭_correct:
      "𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭 opubx = (map typeof xs, τ) ⟹
        ∃y. 𝔘𝔟𝔵𝔒𝔭 opubx xs = Some y ∧ typeof y = τ" and
    𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭_complete:
      "𝔘𝔟𝔵𝔒𝔭 opubx xs = Some y ⟹ 𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭 opubx = (map typeof xs, typeof y)"

end