theory Scratch
  imports Main "HOL-Statespace.StateSpaceLocale" "HOL-Statespace.StateSpaceSyntax"
    "HOL-Library.FSet"
begin

statespace ('k, 'm) set_adt =
  empty :: 'm
  insert :: "'k ⇒ 'm ⇒ 'm"
  isin :: "'k ⇒ 'm ⇒ bool"
  invar :: "'m ⇒ bool"

statespace ('k, 'm) set_adt_delete =
  ('k, 'm) set_adt +
  delete :: "'k ⇒ 'm ⇒ 'm"

locale set_adt_if = set_adt +
  fixes s :: "'n ⇒ 's"
  assumes Not_isin_empty: "¬ (s⋅isin) k (s⋅empty)"
  assumes isin_insert: "(s⋅invar) m ⟹ (s⋅isin) k ((s⋅insert) k m)"
  assumes invar_empty: "(s⋅invar) (s⋅empty)"
  assumes invar_insert: "(s⋅invar) m ⟹ (s⋅invar) ((s⋅insert) k m)"
begin
thm isin_insert
end


locale set_adt_delete_if = set_adt_delete + set_adt_if where s = "s" for s :: "'n ⇒ 's" +
  assumes Not_isin_delete: "(s⋅invar) m ⟹ ¬ (s⋅isin) k ((s⋅delete) k m)"
  assumes invar_delete: "(s⋅invar) m ⟹ (s⋅invar) ((s⋅delete) k m)"

datatype set_adt_delete_fset_op_kind =
  EmptyO | InsertO | IsInO | InvarO | DeleteO

datatype 'a set_adt_delete_fset_op =
    aF (af: "'a fset")
  | a_aF_aF (a_af_af: "'a ⇒ 'a fset ⇒ 'a fset")
  | a_aF_bool (a_af_bool: "'a ⇒ 'a fset ⇒ bool")
  | aF_bool (af_bool: "'a fset ⇒ bool")

fun mk_set_adt_delete_fset_op where
  "mk_set_adt_delete_fset_op EmptyO = aF fempty"
| "mk_set_adt_delete_fset_op InsertO = a_aF_aF finsert"
| "mk_set_adt_delete_fset_op IsInO = a_aF_bool fmember"
| "mk_set_adt_delete_fset_op InvarO = aF_bool (λ_. True)"
| "mk_set_adt_delete_fset_op DeleteO = a_aF_aF (λx s. s |-| {|x|})"

print_locale set_adt_delete_if

interpretation set_adt_delete_fset: set_adt_delete_if
    EmptyO InsertO IsInO InvarO DeleteO
    af aF
    a_af_af a_aF_aF
    a_af_bool a_aF_bool
    af_bool aF_bool
    mk_set_adt_delete_fset_op
  apply(unfold_locales)
  apply(auto simp: lookup_def)
  done ― ‹‹dest_Free› error here›

end