Theory Refine_Dflt

section ‹\isaheader{Default Setup}›
theory Refine_Dflt
imports 
  Refine_Monadic.Refine_Monadic
  "GenCF/GenCF"
  "Lib/Code_Target_ICF"
begin

text ‹Configurations›

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

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

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

lemmas tyrel_dflt_old = tyrel_dflt_nat_set tyrel_dflt_bool_set tyrel_dflt_nat_map

lemmas tyrel_dflt_linorder_set = 
  ty_REL[where R="⟨Id::('a::linorder×'a) set⟩dflt_rs_rel"]
  
lemmas tyrel_dflt_linorder_map = 
  ty_REL[where R="⟨Id::('a::linorder×'a) set,R⟩dflt_rm_rel"] for R
  
lemmas tyrel_dflt_bool_map = 
  ty_REL[where R="⟨Id::(bool×bool) set,R⟩list_map_rel"] for R

lemmas tyrel_dflt = tyrel_dflt_linorder_set tyrel_dflt_bool_set tyrel_dflt_linorder_map tyrel_dflt_bool_map

declare tyrel_dflt[autoref_tyrel]



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
›

text ‹Quick test of setup:›
context begin
private schematic_goal test_dflt_tyrel1: "(?c::?'c,{1,2,3::int})∈?R" (*RBT*)
  by autoref
private lemmas asm_rl[of "_∈⟨int_rel⟩dflt_rs_rel", OF test_dflt_tyrel1]

private schematic_goal test_dflt_tyrel2: "(?c::?'c,{True, False})∈?R" (*List*)
  by autoref
private lemmas asm_rl[of "_∈⟨bool_rel⟩list_set_rel", OF test_dflt_tyrel2]

private schematic_goal test_dflt_tyrel3: "(?c::?'c,[1::int↦0::nat])∈?R" (*RBT*)
  by autoref
private lemmas asm_rl[of "_∈⟨int_rel,nat_rel⟩dflt_rm_rel", OF test_dflt_tyrel3]

private schematic_goal test_dflt_tyrel4: "(?c::?'c,[False↦0::nat])∈?R" (*List*)
  by autoref
private lemmas asm_rl[of "_∈⟨bool_rel,nat_rel⟩list_map_rel", OF test_dflt_tyrel4]

end





end