Theory Refine_Dflt_No_Comp

section ‹Default Setup›
theory Refine_Dflt_No_Comp
imports
  Refine_Monadic.Refine_Monadic
  GenCF_No_Comp
  Collections.Code_Target_ICF
begin

text ‹TODO: need to keep in sync with ‹../../Collections/Refine_Dflt› ...›

text ‹ Configurations ›

lemmas tyrel_dflt_nat_set[autoref_tyrel] = 
  ty_REL[where 'a="nat set" and R="⟨Id⟩dflt_rs_rel"]

lemmas tyrel_dflt_bool_set[autoref_tyrel] = 
  ty_REL[where 'a="bool set" and R="⟨Id⟩list_set_rel"]

lemmas tyrel_dflt_nat_map[autoref_tyrel] = 
  ty_REL[where R="⟨nat_rel,Rv⟩dflt_rm_rel"] for Rv

lemmas tyrel_dflt = tyrel_dflt_nat_set tyrel_dflt_bool_set tyrel_dflt_nat_map


local_setup ‹
  let open Autoref_Fix_Rel in
    declare_prio "Gen-AHM-map-hashable" 
      @{term "⟨Rk::(_×_::hashable) set,Rv⟩ahm_rel bhc"} PR_LAST #>
    declare_prio "Gen-RBT-map-linorder" 
      @{term "⟨Rk::(_×_::linorder) set,Rv⟩rbt_map_rel lt"} PR_LAST #>
    declare_prio "Gen-AHM-map" @{term "⟨Rk,Rv⟩ahm_rel bhc"} PR_LAST #>
    declare_prio "Gen-RBT-map" @{term "⟨Rk,Rv⟩rbt_map_rel lt"} PR_LAST
  end
›


text "Fallbacks"
local_setup ‹
  let open Autoref_Fix_Rel in
    declare_prio "Gen-List-Set" @{term "⟨R⟩list_set_rel"} PR_LAST #>
    declare_prio "Gen-List-Map" @{term "⟨R⟩list_map_rel"} PR_LAST
  end
›

end