Theory Refine_Imperative_HOL.IICF_Prio_Bag

section ‹Priority Bag Interface›
theory IICF_Prio_Bag
imports IICF_Multiset
begin
subsection ‹Operations›
  
  text ‹We prove quite general parametricity lemmas, but restrict 
    them to relations below identity when we register the operations.

    This restriction, although not strictly necessary, makes usage of the tool
    much simpler, as we do not need to handle different prio-functions for 
    abstract and concrete types.
  ›

  context
    fixes prio:: "'a ⇒ 'b::linorder"
  begin  
    definition "mop_prio_pop_min b = ASSERT (b≠{#}) ⪢ SPEC (λ(v,b'). 
        v ∈# b
      ∧ b'=b - {#v#} 
      ∧ (∀v'∈set_mset b. prio v ≤ prio v'))"

    definition "mop_prio_peek_min b ≡ ASSERT (b≠{#}) ⪢ SPEC (λv. 
          v ∈# b
        ∧ (∀v'∈set_mset b. prio v ≤ prio v'))"

  end

  lemma param_mop_prio_pop_min[param]: 
    assumes [param]: "(prio',prio) ∈ A → B"
    assumes [param]: "((≤),(≤)) ∈ B → B → bool_rel"
    shows "(mop_prio_pop_min prio',mop_prio_pop_min prio) ∈ ⟨A⟩mset_rel → ⟨A ×⇩r ⟨A⟩mset_rel⟩nres_rel"
    unfolding mop_prio_pop_min_def[abs_def]
    apply (clarsimp simp: mop_prio_pop_min_def nres_rel_def pw_le_iff refine_pw_simps)
    apply (safe; simp)
  proof goal_cases
    case (1 m n x)
    (*fix m n x*)
    assume "(m,n)∈⟨A⟩mset_rel"
      and "x∈#m"
      and P': "∀x'∈set_mset m. prio' x ≤ prio' x'"
    hence R: "rel_mset (rel2p A) m n" by (simp add: mset_rel_def p2rel_def)
    from multi_member_split[OF ‹x∈#m›] obtain m' where [simp]: "m=m'+{#x#}" by auto
  
    from msed_rel_invL[OF R[simplified]] obtain n' y where 
      [simp]: "n=n'+{#y#}" and [param, simp]: "(x,y)∈A" and R': "(m',n')∈⟨A⟩mset_rel"
      by (auto simp: rel2p_def mset_rel_def p2rel_def)
    have "∀y'∈set_mset n. prio y ≤ prio y'"  
    proof
      fix y' assume "y'∈set_mset n"
      then obtain x' where [param]: "(x',y')∈A" and "x'∈set_mset m"
        using R
        by (metis insert_DiffM msed_rel_invR rel2pD union_single_eq_member)
      with P' have "prio' x ≤ prio' x'" by blast
      moreover have "(prio' x ≤ prio' x', prio y ≤ prio y') ∈ bool_rel"
        by parametricity
      ultimately show "prio y ≤ prio y'" by simp
    qed 
    thus 
      "∃a. (x, a) ∈ A ∧ (m - {#x#}, n - {#a#}) ∈ ⟨A⟩mset_rel ∧ a ∈# n ∧ (∀v'∈set_mset n. prio a ≤ prio v')"
      using R' by (auto intro!: exI[where x=n'] exI[where x=y])
  qed    

  lemma param_mop_prio_peek_min[param]: 
    assumes [param]: "(prio',prio) ∈ A → B"
    assumes [param]: "((≤),(≤)) ∈ B → B → bool_rel"
    shows "(mop_prio_peek_min prio',mop_prio_peek_min prio) ∈ ⟨A⟩mset_rel → ⟨A⟩nres_rel"
    unfolding mop_prio_peek_min_def[abs_def]
    apply (clarsimp 
      simp: mop_prio_pop_min_def nres_rel_def pw_le_iff refine_pw_simps
      )
    apply (safe; simp?)
  proof -
    fix m n x
    assume "(m,n)∈⟨A⟩mset_rel"
      and "x∈#m"
      and P': "∀x'∈set_mset m. prio' x ≤ prio' x'"
    hence R: "rel_mset (rel2p A) m n" by (simp add: mset_rel_def p2rel_def)
    from multi_member_split[OF ‹x∈#m›] obtain m' where [simp]: "m=m'+{#x#}" by auto
  
    from msed_rel_invL[OF R[simplified]] obtain n' y where 
      [simp]: "n=n'+{#y#}" and [param, simp]: "(x,y)∈A" and R': "(m',n')∈⟨A⟩mset_rel"
      by (auto simp: rel2p_def mset_rel_def p2rel_def)
  
    have "∀y'∈set_mset n. prio y ≤ prio y'"  
    proof
      fix y' assume "y'∈set_mset n"
      then obtain x' where [param]: "(x',y')∈A" and "x'∈set_mset m"
        using R
        by (metis msed_rel_invR mset_contains_eq rel2pD union_mset_add_mset_left union_single_eq_member)
      with P' have "prio' x ≤ prio' x'" by blast
      moreover have "(prio' x ≤ prio' x', prio y ≤ prio y') ∈ bool_rel"
        by parametricity
      ultimately show "prio y ≤ prio y'" by simp
    qed  
    thus "∃y. (x, y) ∈ A ∧ y ∈# n ∧ (∀v'∈set_mset n. prio y ≤ prio v')"
      using R' by (auto intro!: exI[where x=y])
  qed




  context fixes prio :: "'a ⇒ 'b::linorder" and A :: "('a×'a) set" begin
    sepref_decl_op (no_def,no_mop) prio_pop_min: 
      "PR_CONST (mop_prio_pop_min prio)" :: "⟨A⟩mset_rel →⇩f ⟨A ×⇩r ⟨A⟩mset_rel⟩nres_rel"
      where "IS_BELOW_ID A"
    proof goal_cases
      case 1
      hence [param]: "(prio,prio)∈A → Id" 
        by (auto simp: IS_BELOW_ID_def)
      show ?case
        apply (rule fref_ncI)
        apply parametricity
        by auto
    qed

    sepref_decl_op (no_def,no_mop) prio_peek_min: 
      "PR_CONST (mop_prio_peek_min prio)" :: "⟨A⟩mset_rel →⇩f ⟨A⟩nres_rel"
      where "IS_BELOW_ID A"
    proof goal_cases
      case 1
      hence [param]: "(prio,prio)∈A → Id" 
        by (auto simp: IS_BELOW_ID_def)
      show ?case
        apply (rule fref_ncI)
        apply parametricity
        by auto
    qed
  end  

subsection ‹Patterns›

lemma [def_pat_rules]:
  "mop_prio_pop_min$prio ≡ UNPROTECT (mop_prio_pop_min prio)"
  "mop_prio_peek_min$prio ≡ UNPROTECT (mop_prio_peek_min prio)"
  by auto

end