Theory Refine_Dflt_ICF

section ‹\isaheader{Entry Point with genCF and original ICF}›
theory Refine_Dflt_ICF
imports 
  Refine_Monadic.Refine_Monadic
  "GenCF/GenCF"
  "ICF/Collections"
  "Lib/Code_Target_ICF"
begin


text ‹Contains the Monadic Refinement Framework, the generic collection 
  framework and the original Isabelle Collection Framework›

local_setup ‹
  let open Autoref_Fix_Rel in
    declare_prio "Gen-RBT-set" @{term "⟨R⟩dflt_rs_rel"} PR_LAST #>
    declare_prio "RBT-set" @{term "⟨R⟩rs.rel"} PR_LAST #>
    declare_prio "Hash-set" @{term "⟨R⟩hs.rel"} PR_LAST #>
    declare_prio "List-set" @{term "⟨R⟩lsi.rel"} PR_LAST
  end
›

local_setup ‹
  let open Autoref_Fix_Rel in
    declare_prio "RBT-map" @{term "⟨Rk,Rv⟩rm.rel"} PR_LAST #>
    declare_prio "Hash-map" @{term "⟨Rk,Rv⟩hm.rel"} PR_LAST #>
    (* declare_prio "Gen-RBT-map" @{term "⟨Rk,Rv⟩rbt_map_rel ?cmp"} PR_LAST #>*)
    declare_prio "List-map" @{term "⟨Rk,Rv⟩lmi.rel"} 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 "⟨Rk,Rv⟩list_map_rel"} PR_LAST
  end
›

class id_refine

instance nat :: id_refine ..
instance bool :: id_refine ..
instance int :: id_refine ..

lemmas [autoref_tyrel] = 
  ty_REL[where 'a="nat" and R="nat_rel"]
  ty_REL[where 'a="int" and R="int_rel"]
  ty_REL[where 'a="bool" and R="bool_rel"]
lemmas [autoref_tyrel] = 
  ty_REL[where 'a="nat set" and R="⟨Id⟩rs.rel"]
  ty_REL[where 'a="int set" and R="⟨Id⟩rs.rel"]
  ty_REL[where 'a="bool set" and R="⟨Id⟩lsi.rel"]
lemmas [autoref_tyrel] = 
  ty_REL[where 'a="(nat ⇀ 'b)", where R="⟨nat_rel,Rv⟩dflt_rm_rel"]
  ty_REL[where 'a="(int ⇀ 'b)", where R="⟨int_rel,Rv⟩dflt_rm_rel"]
  ty_REL[where 'a="(bool ⇀ 'b)", where R="⟨bool_rel,Rv⟩dflt_rm_rel"]
  for Rv

lemmas [autoref_tyrel] = 
  ty_REL[where 'a="(nat ⇀ 'b::id_refine)", where R="⟨nat_rel,Id⟩rm.rel"]
  ty_REL[where 'a="(int ⇀ 'b::id_refine)", where R="⟨int_rel,Id⟩rm.rel"]
  ty_REL[where 'a="(bool ⇀ 'b::id_refine)", where R="⟨bool_rel,Id⟩rm.rel"]

end