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)∈A→B→R"  
    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)∈⟨A⟩nres_rel ⟷ (f,g)∈A"
    by (auto simp: nres_rel_def)

  lemma RETURN_rel_conv1: "(RETURN o f, RETURN o g)∈A → ⟨B⟩nres_rel ⟷ (f,g)∈A→B"
    by (auto simp: nres_rel_def dest!: fun_relD)

  lemma RETURN_rel_conv2: "(RETURN oo f, RETURN oo g)∈A → B → ⟨R⟩nres_rel ⟷ (f,g)∈A→B→R"
    by (auto simp: nres_rel_def dest!: fun_relD)

  lemma RETURN_rel_conv3: "(RETURN ooo f, RETURN ooo g)∈A→B→C → ⟨R⟩nres_rel ⟷ (f,g)∈A→B→C→R"
    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). k∉dom m]⇩f (K×⇩rV)×⇩r⟨K,V⟩map_rel → ⟨K,V⟩map_rel"
    where "single_valued K" "single_valued (K¯)" .

  sepref_decl_op map_update_ex: "op_map_update" :: "[λ((k,v),m). k∈dom m]⇩f (K×⇩rV)×⇩r⟨K,V⟩map_rel → ⟨K,V⟩map_rel"
    where "single_valued K" "single_valued (K¯)" .
    
  sepref_decl_op map_delete_ex: "op_map_delete" :: "[λ(k,m). k∈dom m]⇩f K×⇩r⟨K,V⟩map_rel → ⟨K,V⟩map_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). k∈dom m ∧ prio v ≤ prio (the (m k))]⇩f (K×⇩rV)×⇩r⟨K,V⟩map_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]: "((≤),(≤))∈Id→Id→bool_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). k∈dom m ∧ prio v ≥ prio (the (m k))]⇩f (K×⇩rV)×⇩r⟨K,V⟩map_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]: "((≤),(≤))∈Id→Id→bool_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,V⟩map_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, V⟩map_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,V⟩map_rel → (K×⇩r(V::('v×'v) set))×⇩r⟨K,V⟩map_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, V⟩map_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