Theory Ordered_Algebra_Impl

theory Ordered_Algebra_Impl
  imports Ordered_Algebra "../LTS/Map_Of" Check_Monad Map_Choice
begin

text {* Checking well-formedness: *}

type_synonym ('f, 'g) encoder_inter = "(('f × nat) × ('g, nat) term) list"

locale encoding_impl =
  fixes alist :: "('f :: show,'g) encoder_inter"
    and default_fun :: "nat ⇒ 'g"
begin

definition "E = curry (fun_of_map_fun (map_of alist) (λ(f, n). Fun (default_fun n) (map Var [0..<n])))"

sublocale pre_encoding E.

definition "check_encoding ≡
  check_allm (λ((f,n),t).
    check (vars_term t ⊆ {..<n})
    (shows ''interpretation of '' ∘ shows f ∘ shows '' arity '' ∘ shows n ∘ shows '' has extra parameter'')
  ) alist"

lemma check_encoding:
  assumes ok: "isOK check_encoding" shows "encoding E"
  apply (unfold_locales)
  apply (unfold atomize_imp curry_def)
  using ok by (auto simp: check_encoding_def o_def E_def split:option.split elim!:ballE dest:map_of_SomeD)

end

declare encoding_impl.E_def [code]
declare encoding_impl.check_encoding_def [code]

end