Theory Op

theory Op
  imports Main
begin

section ‹n-ary operations›

locale nary_operations =
  fixes
    𝔒𝔭 :: "'op ⇒ 'a list ⇒ 'a" and
    𝔄𝔯𝔦𝔱𝔶 :: "'op ⇒ nat"
  assumes
    𝔒𝔭_𝔄𝔯𝔦𝔱𝔶_domain: "length xs = 𝔄𝔯𝔦𝔱𝔶 op ⟹ ∃y. 𝔒𝔭 op xs = y"

(* locale nary_operations_inl =
  nary_operations "λop args. fst (eval op args)" arity
  for
    eval :: "'op ⇒ 'dyn list ⇒ 'dyn × 'op option" and arity
begin

definition equiv_op where
  "equiv_op x y ≡ fst ∘ eval x = fst ∘ eval y"

lemma equivp_equiv_op[simp]: "equivp equiv_op"
proof (rule equivpI)
  show "reflp equiv_op"
    by (rule reflpI) (simp add: equiv_op_def)
next
  show "symp equiv_op"
    by (rule sympI) (simp add: equiv_op_def)
next
  show "transp equiv_op"
    by (rule transpI) (simp add: equiv_op_def)
qed

end *)

(* locale nary_operations0 =
  fixes
    eval :: "'op ⇒ 'dyn list ⇒ 'dyn × 'op option" and
    arity :: "'op ⇒ nat"
begin

definition equiv_op where
  "equiv_op x y ≡ fst ∘ eval x = fst ∘ eval y"

lemma equivp_equiv_op[simp]: "equivp equiv_op"
proof (rule equivpI)
  show "reflp equiv_op"
    by (rule reflpI) (simp add: equiv_op_def)
next
  show "symp equiv_op"
    by (rule sympI) (simp add: equiv_op_def)
next
  show "transp equiv_op"
    by (rule transpI) (simp add: equiv_op_def)
qed

end *)

end