Theory Gen_Map

section ‹\isaheader{Generic Map Algorithms}›
theory Gen_Map
imports "../Intf/Intf_Map" "../../Iterator/Iterator"
begin
  lemma map_to_set_distinct_conv:
    assumes "distinct tsl'" and "map_to_set m' = set tsl'"
    shows "distinct (map fst tsl')"
    apply (rule ccontr)
    apply (drule not_distinct_decomp)
    using assms
    apply (clarsimp elim!: map_eq_appendE)
    by (metis (opaque_lifting, no_types) insert_iff map_to_set_inj)


  (* TODO: Make foldli explicit, such that it is seen by 
  iterator-optimizations! cf Gen_Set for how to do this! *)
  lemma foldli_add: "det_fold_map X 
    (λ_. True) (λ(k,v) m. op_map_update k v m) m ((++) m)"
  proof (rule, goal_cases)
    case (1 l) thus ?case
      apply (induct l arbitrary: m) 
      apply (auto simp: map_of_distinct_upd[symmetric])
      done
  qed

  definition gen_add
    :: "('s2 ⇒ _) ⇒ ('k ⇒ 'v ⇒ 's1 ⇒ 's1) ⇒ 's1 ⇒ 's2 ⇒ 's1"
    where 
    "gen_add it upd A B ≡ it B (λ_. True) (λ(k,v) m. upd k v m) A"

  lemma gen_add[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes UPD: "GEN_OP ins op_map_update (Rk→Rv→⟨Rk,Rv⟩Rs1→⟨Rk,Rv⟩Rs1)"
    assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs2 tsl)"
    shows "(gen_add (foldli o tsl) ins,(++)) 
      ∈ (⟨Rk,Rv⟩Rs1) → (⟨Rk,Rv⟩Rs2) → (⟨Rk,Rv⟩Rs1)"
    apply (intro fun_relI)
    unfolding gen_add_def comp_def
    apply (rule det_fold_map[OF foldli_add IT[unfolded autoref_tag_defs]])
    apply (parametricity add: UPD[unfolded autoref_tag_defs])+
    done

  lemma foldli_restrict: "det_fold_map X (λ_. True) 
    (λ(k,v) m. if P (k,v) then op_map_update k v m else m) Map.empty
      (op_map_restrict P )" (is "det_fold_map _ _ ?f _ _")
  proof -
    {
      fix l m
      have "distinct (map fst l) ⟹
        foldli l (λ_. True) ?f m = m ++ op_map_restrict P (map_of l)"
      proof (induction l arbitrary: m) 
        case Nil thus ?case by simp
      next
        case (Cons kv l)
        obtain k v where [simp]: "kv = (k,v)" by fastforce
        from Cons.prems have 
          DL: "distinct (map fst l)" and KNI: "k ∉ set (map fst l)" 
          by auto

        show ?case proof (cases "P (k,v)")
          case [simp]: True 
          have "foldli (kv#l) (λ_. True) ?f m = foldli l (λ_. True) ?f (m(k↦v))"
            by simp
          also from Cons.IH[OF DL] have 
            "… = m(k↦v) ++ op_map_restrict P (map_of l)" .
          also have "… = m ++ op_map_restrict P (map_of (kv#l))"
            using KNI
            by (auto
              split: option.splits
              intro!: ext 
              simp: Map.restrict_map_def Map.map_add_def
              simp: map_of_eq_None_iff[symmetric])
          finally show ?thesis .
        next
          case [simp]: False 
          have "foldli (kv#l) (λ_. True) ?f m = foldli l (λ_. True) ?f m"
            by simp
          also from Cons.IH[OF DL] have 
            "… = m ++ op_map_restrict P (map_of l)" .
          also have "… = m ++ op_map_restrict P (map_of (kv#l))"
            using KNI
            by (auto 
              intro!: ext
              simp: Map.restrict_map_def Map.map_add_def
              simp: map_of_eq_None_iff[symmetric]
            )
          finally show ?thesis .
        qed
      qed
    } 
    from this[of _ Map.empty] show ?thesis
      by (auto intro!: det_fold_mapI)
  qed

  definition gen_restrict :: "('s1 ⇒ _) ⇒ _"
    where "gen_restrict it upd emp P m 
    ≡ it m (λ_. True) (λ(k,v) m. if P (k,v) then upd k v m else m) emp"

  lemma gen_restrict[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs1 tsl)"
    assumes INS: 
      "GEN_OP upd op_map_update (Rk→Rv→⟨Rk,Rv⟩Rs2→⟨Rk,Rv⟩Rs2)"
    assumes EMPTY: 
      "GEN_OP emp Map.empty (⟨Rk,Rv⟩Rs2)"
    shows "(gen_restrict (foldli o tsl) upd emp,op_map_restrict) 
    ∈ (⟨Rk,Rv⟩prod_rel → Id) → (⟨Rk,Rv⟩Rs1) → (⟨Rk,Rv⟩Rs2)"
    apply (intro fun_relI)
    unfolding gen_restrict_def comp_def
    apply (rule det_fold_map[OF foldli_restrict IT[unfolded autoref_tag_defs]])
    using INS EMPTY unfolding autoref_tag_defs
    apply (parametricity)+
    done

  lemma fold_map_of: 
    "fold (λ(k,v) s. op_map_update k v s) (rev l) Map.empty = map_of l"
  proof -
    {
      fix m
      have "fold (λ(k,v) s. s(k↦v)) (rev l) m = m ++ map_of l"
        apply (induct l arbitrary: m)
        apply auto
        done
    } thus ?thesis by simp
  qed

  definition gen_map_of :: "'m ⇒ ('k⇒'v⇒'m⇒'m) ⇒ _" where 
    "gen_map_of emp upd l ≡ fold (λ(k,v) s. upd k v s) (rev l) emp"


  lemma gen_map_of[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes UPD: "GEN_OP upd op_map_update (Rk→Rv→⟨Rk,Rv⟩Rm→⟨Rk,Rv⟩Rm)"
    assumes EMPTY: "GEN_OP emp Map.empty (⟨Rk,Rv⟩Rm)"
    shows "(gen_map_of emp upd,map_of) ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel → ⟨Rk,Rv⟩Rm"
    using assms
    apply (intro fun_relI)
    unfolding gen_map_of_def[abs_def]
    unfolding autoref_tag_defs
    apply (subst fold_map_of[symmetric])
    apply parametricity
    done

  lemma foldli_ball_aux: 
    "distinct (map fst l) ⟹ foldli l (λx. x) (λx _. P x) b 
    ⟷ b ∧ op_map_ball (map_of l) P"
    apply (induct l arbitrary: b)
    apply simp
    apply (force simp: map_to_set_map_of image_def)
    done
  
  lemma foldli_ball: 
    "det_fold_map X (λx. x) (λx _. P x) True (λm. op_map_ball m P)"
    apply rule
    using foldli_ball_aux[where b=True] by auto
    
  definition gen_ball :: "('m ⇒ _) ⇒ _" where
    "gen_ball it m P ≡ it m (λx. x) (λx _. P x) True"

  lemma gen_ball[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm tsl)"
    shows "(gen_ball (foldli o tsl),op_map_ball) 
    ∈ ⟨Rk,Rv⟩Rm → (⟨Rk,Rv⟩prod_rel → Id) → Id"
    apply (intro fun_relI)
    unfolding gen_ball_def comp_def
    apply (rule det_fold_map[OF foldli_ball IT[unfolded autoref_tag_defs]])
    apply (parametricity)+
    done

  lemma foldli_bex_aux: 
    "distinct (map fst l) ⟹ foldli l (λx. ¬x) (λx _. P x) b 
    ⟷ b ∨ op_map_bex (map_of l) P"
    apply (induct l arbitrary: b)
    apply simp
    apply (force simp: map_to_set_map_of image_def)
    done
  
  lemma foldli_bex: 
    "det_fold_map X (λx. ¬x) (λx _. P x) False (λm. op_map_bex m P)"
    apply rule
    using foldli_bex_aux[where b=False] by auto

  definition gen_bex :: "('m ⇒ _) ⇒ _" where
    "gen_bex it m P ≡ it m (λx. ¬x) (λx _. P x) False"

  lemma gen_bex[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm tsl)"
    shows "(gen_bex (foldli o tsl),op_map_bex) 
    ∈ ⟨Rk,Rv⟩Rm → (⟨Rk,Rv⟩prod_rel → Id) → Id"
    apply (intro fun_relI)
    unfolding gen_bex_def comp_def
    apply (rule det_fold_map[OF foldli_bex IT[unfolded autoref_tag_defs]])
    apply (parametricity)+
    done

  lemma ball_isEmpty: "op_map_isEmpty m = op_map_ball m (λ_. False)"
    apply (auto intro!: ext)
    by (metis map_to_set_simps(7) option.exhaust)

  definition "gen_isEmpty ball m ≡ ball m (λ_. False)"

  lemma gen_isEmpty[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes BALL: 
      "GEN_OP ball op_map_ball (⟨Rk,Rv⟩Rm→(⟨Rk,Rv⟩prod_rel→Id) → Id)"
    shows "(gen_isEmpty ball,op_map_isEmpty) 
    ∈ ⟨Rk,Rv⟩Rm → Id"
    apply (intro fun_relI)
    unfolding gen_isEmpty_def using assms
    unfolding autoref_tag_defs
    apply -
    apply (subst ball_isEmpty)
    apply parametricity+
    done
  
  lemma foldli_size_aux: "distinct (map fst l) 
    ⟹ foldli l (λ_. True) (λ_ n. Suc n) n = n + op_map_size (map_of l)"
    apply (induct l arbitrary: n)
    apply (auto simp: dom_map_of_conv_image_fst)
    done

  lemma foldli_size: "det_fold_map X (λ_. True) (λ_ n. Suc n) 0 op_map_size"
    apply rule
    using foldli_size_aux[where n=0] by simp

  definition gen_size :: "('m ⇒ _) ⇒ _"
    where "gen_size it m ≡ it m (λ_. True) (λ_ n. Suc n) 0"

  lemma gen_size[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm tsl)"
    shows "(gen_size (foldli o tsl),op_map_size) ∈ ⟨Rk,Rv⟩Rm → Id"
    apply (intro fun_relI)
    unfolding gen_size_def comp_def
    apply (rule det_fold_map[OF foldli_size IT[unfolded autoref_tag_defs]])
    apply (parametricity)+
    done
  
  lemma foldli_size_abort_aux:
    "⟦n0≤m; distinct (map fst l)⟧ ⟹ 
      foldli l (λn. n<m) (λ_ n. Suc n) n0 = min m (n0 + card (dom (map_of l)))"
    apply (induct l arbitrary: n0)
    apply (auto simp: dom_map_of_conv_image_fst)
    done

  lemma foldli_size_abort: 
    "det_fold_map X (λn. n<m) (λ_ n. Suc n) 0 (op_map_size_abort m)"
    apply rule
    using foldli_size_abort_aux[where ?n0.0=0]
    by simp

  definition gen_size_abort :: "('s ⇒ _) ⇒ _" where
    "gen_size_abort it m s ≡ it s (λn. n<m) (λ_ n. Suc n) 0"

  lemma gen_size_abort[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm tsl)"
    shows "(gen_size_abort (foldli o tsl),op_map_size_abort) 
      ∈ Id → ⟨Rk,Rv⟩Rm → Id"
    apply (intro fun_relI)
    unfolding gen_size_abort_def comp_def
    apply (rule det_fold_map[OF foldli_size_abort 
      IT[unfolded autoref_tag_defs]])
    apply (parametricity)+
    done
  
  lemma size_abort_isSng: "op_map_isSng s ⟷ op_map_size_abort 2 s = 1"
    by (auto simp: dom_eq_singleton_conv min_def dest!: card_eq_SucD)

  definition gen_isSng :: "(nat ⇒ 's ⇒ nat) ⇒ _" where
    "gen_isSng sizea s ≡ sizea 2 s = 1"

  lemma gen_isSng[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes "GEN_OP sizea op_map_size_abort (Id → (⟨Rk,Rv⟩Rm) → Id)"
    shows "(gen_isSng sizea,op_map_isSng) 
    ∈ ⟨Rk,Rv⟩Rm → Id"
    apply (intro fun_relI)
    unfolding gen_isSng_def using assms
    unfolding autoref_tag_defs
    apply -
    apply (subst size_abort_isSng)
    apply parametricity
    done


  (* TODO: Also do sel! *)

  lemma foldli_pick:
    assumes "l≠[]" 
    obtains k v where "(k,v)∈set l" 
    and "(foldli l (case_option True (λ_. False)) (λx _. Some x) None) 
      = Some (k,v)"
    using assms by (cases l) auto

  definition gen_pick where
    "gen_pick it s ≡ 
      (the (it s (case_option True (λ_. False)) (λx _. Some x) None))"



context begin interpretation autoref_syn .

  lemma gen_pick[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rm it)"
    assumes NE: "SIDE_PRECOND (m'≠Map.empty)"
    assumes SREF: "(m,m')∈⟨Rk,Rv⟩Rm"
    shows "(RETURN (gen_pick (λx. foldli (it x)) m), 
      (OP op_map_pick ::: ⟨Rk,Rv⟩Rm→⟨Rk×⇩rRv⟩nres_rel)$m')∈⟨Rk×⇩rRv⟩nres_rel"
  proof -
    thm is_map_to_list_def is_map_to_sorted_listE

    obtain tsl' where
      [param]: "(it m,tsl') ∈ ⟨Rk×⇩rRv⟩list_rel" 
      and IT': "RETURN tsl' ≤ it_to_sorted_list (λ_ _. True) (map_to_set m')"
      using IT[unfolded autoref_tag_defs is_map_to_list_def] SREF
      by (auto intro: is_map_to_sorted_listE)

    from IT' NE have "tsl'≠[]" and [simp]: "m'=map_of tsl'" 
      and DIS': "distinct (map fst tsl')"
      unfolding it_to_sorted_list_def 
      apply simp_all
      apply (metis empty_set map_to_set_empty_iff(1))
      apply (metis map_of_map_to_set map_to_set_distinct_conv)
      apply (metis map_to_set_distinct_conv)
      done

    then obtain k v where "m' k = Some v" and
      "(foldli tsl' (case_option True (λ_. False)) (λx _. Some x) None) 
        = Some (k,v)"
      (is "?fld = _")
      by (cases rule: foldli_pick) auto
    moreover 
    have "(RETURN (gen_pick (λx. foldli (it x)) m), RETURN (the ?fld)) 
      ∈ ⟨Rk×⇩rRv⟩nres_rel"
      unfolding gen_pick_def
      apply (parametricity add: the_paramR)
      using ‹?fld = Some (k,v)›
      by simp
    ultimately show ?thesis
      unfolding autoref_tag_defs
      apply -
      apply (drule nres_relD)
      apply (rule nres_relI)
      apply (erule ref_two_step)
      by simp
  qed
end


  definition "gen_map_pick_remove pick del m ≡ do {
    (k,v)←pick m;
    let m = del k m;
    RETURN ((k,v),m)
    }"
  
context begin interpretation autoref_syn .
  lemma gen_map_pick_remove
    [unfolded gen_map_pick_remove_def, autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes PICK: "SIDE_GEN_OP (
      (pick m, 
      (OP op_map_pick ::: ⟨Rk,Rv⟩Rm → ⟨Rk×⇩rRv⟩nres_rel)$m') ∈
      ⟨Rk×⇩rRv⟩nres_rel)"
    assumes DEL: "GEN_OP del op_map_delete (Rk → ⟨Rk,Rv⟩Rm → ⟨Rk,Rv⟩Rm)"
    assumes [param]: "(m,m')∈⟨Rk,Rv⟩Rm"
    shows "(gen_map_pick_remove pick del m, 
      (OP op_map_pick_remove 
        ::: ⟨Rk,Rv⟩Rm → ⟨(Rk×⇩rRv) ×⇩r ⟨Rk,Rv⟩Rm⟩nres_rel)$m')
      ∈ ⟨(Rk×⇩rRv) ×⇩r ⟨Rk,Rv⟩Rm⟩nres_rel"
  proof -
    note [param] = 
      PICK[unfolded autoref_tag_defs] 
      DEL[unfolded autoref_tag_defs]

    have "(gen_map_pick_remove pick del m, 
      do {    
        (k,v)←op_map_pick m';
        let m' = op_map_delete k m';
        RETURN ((k,v),m')
      }) ∈ ⟨(Rk×⇩rRv) ×⇩r ⟨Rk,Rv⟩Rm⟩nres_rel" (is "(_,?h):_")
      unfolding gen_map_pick_remove_def[abs_def]
      apply parametricity
      done
    also have "?h = op_map_pick_remove m'"
      by (auto simp add: pw_eq_iff refine_pw_simps)
    finally show ?thesis by simp
  qed
end


end