Theory OpInl

theory OpInl
  imports Op
begin

section β€Ήn-ary operationsβ€Ί

locale nary_operations_inl =
  nary_operations 𝔒𝔭 𝔄𝔯𝔦𝔱𝔢
  for
    𝔒𝔭 :: "'op β‡’ 'a list β‡’ 'a" and 𝔄𝔯𝔦𝔱𝔢 +
  fixes
    ℑ𝔫𝔩𝔒𝔭 :: "'opinl β‡’ 'a list β‡’ 'a" and
    ℑ𝔫𝔩 :: "'op β‡’ 'a list β‡’ 'opinl option" and
    ℑ𝔰ℑ𝔫𝔩 :: "'opinl β‡’ 'a list β‡’ bool" and
    𝔇𝔒ℑ𝔫𝔩 :: "'opinl β‡’ 'op"
  assumes
    ℑ𝔫𝔩_invertible: "ℑ𝔫𝔩 op xs = Some opinl ⟹ 𝔇𝔒ℑ𝔫𝔩 opinl = op" and
    ℑ𝔫𝔩𝔒𝔭_correct: "length xs = 𝔄𝔯𝔦𝔱𝔢 (𝔇𝔒ℑ𝔫𝔩 opinl) ⟹ ℑ𝔫𝔩𝔒𝔭 opinl xs = 𝔒𝔭 (𝔇𝔒ℑ𝔫𝔩 opinl) xs" and
    ℑ𝔫𝔩_ℑ𝔰ℑ𝔫𝔩: "ℑ𝔫𝔩 op xs = Some opinl ⟹ ℑ𝔰ℑ𝔫𝔩 opinl xs"

begin

lemma ℑ𝔫𝔩_inj_on: "inj_on ℑ𝔫𝔩 { op | op args. ℑ𝔫𝔩 op args β‰  None }"
  apply (simp add: inj_on_def)
proof (intro allI impI, elim exE)
  fix op1 op2 args1 args2 opinl1 opinl2
  assume assms: "ℑ𝔫𝔩 op1 = ℑ𝔫𝔩 op2" "ℑ𝔫𝔩 op1 args1 = Some opinl1" "ℑ𝔫𝔩 op2 args2 = Some opinl2"
  hence "𝔇𝔒ℑ𝔫𝔩 opinl1 = op1" "𝔇𝔒ℑ𝔫𝔩 opinl1 = op2"
    by (auto intro: ℑ𝔫𝔩_invertible)
  thus "op1 = op2"
    by simp
qed

abbreviation ℑ𝔫𝔩_dom where
  "ℑ𝔫𝔩_dom ≑ {op | op args. ℑ𝔫𝔩 op args β‰  None }"

lemma "bij_betw ℑ𝔫𝔩 ℑ𝔫𝔩_dom { ℑ𝔫𝔩 op | op. op ∈ ℑ𝔫𝔩_dom}"
  using bij_betw_def
  unfolding image_def
  using ℑ𝔫𝔩_inj_on
  by (auto simp add: bij_betw_def)

end

end