Theory Refine_Imperative_HOL.IICF_Prio_Map

section ‹Priority Maps›
theory IICF_Prio_Map
imports IICF_Map
begin
  text ‹This interface inherits from maps, and adds some operations›

  (* TODO: Hack! *)  
  lemma uncurry_fun_rel_conv: 
    "(uncurry f, uncurry g)  A×rB  R  (f,g)ABR"  
    by (auto simp: uncurry_def dest!: fun_relD intro: prod_relI)

  lemma uncurry0_fun_rel_conv: 
    "(uncurry0 f, uncurry0 g)  unit_rel  R  (f,g)R"  
    by (auto dest!: fun_relD)

  lemma RETURN_rel_conv0: "(RETURN f, RETURN g)Anres_rel  (f,g)A"
    by (auto simp: nres_rel_def)

  lemma RETURN_rel_conv1: "(RETURN o f, RETURN o g)A  Bnres_rel  (f,g)AB"
    by (auto simp: nres_rel_def dest!: fun_relD)

  lemma RETURN_rel_conv2: "(RETURN oo f, RETURN oo g)A  B  Rnres_rel  (f,g)ABR"
    by (auto simp: nres_rel_def dest!: fun_relD)

  lemma RETURN_rel_conv3: "(RETURN ooo f, RETURN ooo g)ABC  Rnres_rel  (f,g)ABCR"
    by (auto simp: nres_rel_def dest!: fun_relD)

  lemmas fref2param_unfold = 
    uncurry_fun_rel_conv uncurry0_fun_rel_conv 
    RETURN_rel_conv0 RETURN_rel_conv1 RETURN_rel_conv2 RETURN_rel_conv3


  (* TODO: Generate these lemmas in sepref_decl_op! *)  
  lemmas param_op_map_update[param] = op_map_update.fref[THEN fref_ncD, unfolded fref2param_unfold]
  lemmas param_op_map_delete[param] = op_map_delete.fref[THEN fref_ncD, unfolded fref2param_unfold]
  lemmas param_op_map_is_empty[param] = op_map_is_empty.fref[THEN fref_ncD, unfolded fref2param_unfold]

  subsection ‹Additional Operations›

  sepref_decl_op map_update_new: "op_map_update" :: "[λ((k,v),m). kdom m]f (K×rV)×rK,Vmap_rel  K,Vmap_rel"
    where "single_valued K" "single_valued (K¯)" .

  sepref_decl_op map_update_ex: "op_map_update" :: "[λ((k,v),m). kdom m]f (K×rV)×rK,Vmap_rel  K,Vmap_rel"
    where "single_valued K" "single_valued (K¯)" .
    
  sepref_decl_op map_delete_ex: "op_map_delete" :: "[λ(k,m). kdom m]f K×rK,Vmap_rel  K,Vmap_rel"
    where "single_valued K" "single_valued (K¯)" .

  context
    fixes prio :: "'v  'p::linorder"  
  begin
    sepref_decl_op pm_decrease_key: "op_map_update" 
      :: "[λ((k,v),m). kdom m  prio v  prio (the (m k))]f (K×rV)×rK,Vmap_rel  K,(V::('v×'v) set)map_rel"
      where "single_valued K" "single_valued (K¯)" "IS_BELOW_ID V"
    proof goal_cases  
      case 1 
      have [param]: "((≤),(≤))IdIdbool_rel" by simp
      from 1 show ?case
        apply (parametricity add: param_and_cong1)
        apply (auto simp: IS_BELOW_ID_def map_rel_def dest!: fun_relD)
        done
    qed

    sepref_decl_op pm_increase_key: "op_map_update" 
      :: "[λ((k,v),m). kdom m  prio v  prio (the (m k))]f (K×rV)×rK,Vmap_rel  K,(V::('v×'v) set)map_rel"
      where "single_valued K" "single_valued (K¯)" "IS_BELOW_ID V"
    proof goal_cases  
      case 1 
      have [param]: "((≤),(≤))IdIdbool_rel" by simp
      from 1 show ?case
        apply (parametricity add: param_and_cong1)
        apply (auto simp: IS_BELOW_ID_def map_rel_def dest!: fun_relD)
        done
    qed


    lemma IS_BELOW_ID_D: "(a,b)R  IS_BELOW_ID R  a=b" by (auto simp: IS_BELOW_ID_def)

    sepref_decl_op pm_peek_min: "λm. SPEC (λ(k,v). 
      m k = Some v  (k' v'. m k' = Some v'  prio v  prio v'))"
      :: "[Not o op_map_is_empty]f K,Vmap_rel  K×r(V::('v×'v) set)"
      where "IS_BELOW_ID V"
      apply (rule frefI)
      apply (intro nres_relI)
      apply (clarsimp simp: pw_le_iff refine_pw_simps)
      apply (rule map_rel_obtain2, assumption, assumption)
      apply1 (intro exI conjI allI impI; assumption?)
    proof -
      fix x y k' v' b w
      assume "(x, y)  K, Vmap_rel" "y k' = Some v'"
      then obtain k v where "(k,k')K" "(v,v')V" "x k = Some v"
        by (rule map_rel_obtain1)
        
      assume "IS_BELOW_ID V" "(b, w)  V" 
      with (v,v')V have [simp]: "b=w" "v=v'" by (auto simp: IS_BELOW_ID_def)

      assume "k' v'. x k' = Some v'  prio b  prio v'"
      with x k = Some v show "prio w  prio v'"
        by auto
    qed    

    sepref_decl_op pm_pop_min: "λm. SPEC (λ((k,v),m'). 
        m k = Some v
       m' = op_map_delete k m  
       (k' v'. m k' = Some v'  prio v  prio v')
      )" :: "[Not o op_map_is_empty]f K,Vmap_rel  (K×r(V::('v×'v) set))×rK,Vmap_rel"
      where "single_valued K" "single_valued (K¯)" "IS_BELOW_ID V"
      apply (rule frefI)
      apply (intro nres_relI)
      apply (clarsimp simp: pw_le_iff refine_pw_simps simp del: op_map_delete_def)
      apply (rule map_rel_obtain2, assumption, assumption)
      apply (intro exI conjI allI impI; assumption?)
      applyS parametricity
    proof -
      fix x y k' v' b w
      assume "(x, y)  K, Vmap_rel" "y k' = Some v'"
      then obtain k v where "(k,k')K" "(v,v')V" "x k = Some v"
        by (rule map_rel_obtain1)
        
      assume "IS_BELOW_ID V" "(b, w)  V" 
      with (v,v')V have [simp]: "b=w" "v=v'" by (auto simp: IS_BELOW_ID_def)

      assume "k' v'. x k' = Some v'  prio b  prio v'"
      with x k = Some v show "prio w  prio v'"
        by auto
    qed    
  end  

end