Theory Refine_Imperative_HOL.IICF_Indexed_Array_List

theory IICF_Indexed_Array_List
imports 
  "HOL-Library.Rewrite"
  "../Intf/IICF_List"
  "List-Index.List_Index"
  IICF_Array
  IICF_MS_Array_List
begin

  text ‹We implement distinct lists of natural numbers in the range ‹{0..<N}›
    by a length counter and two arrays of size ‹N›. 
    The first array stores the list, and the second array stores the positions of
    the elements in the list, or ‹N› if the element is not in the list.

    This allows for an efficient index query.

    The implementation is done in two steps: 
      First, we use a list and a fixed size list for the index mapping.
      Second, we refine the lists to arrays.
 ›

  type_synonym aial = "nat list × nat list"

  locale ial_invar = fixes
         maxsize :: nat 
    and  l :: "nat list"
    and qp :: "nat list"
    assumes maxsize_eq[simp]: "maxsize = length qp"
    assumes l_distinct[simp]: "distinct l"
    assumes l_set: "set l ⊆ {0..<length qp}"
    assumes qp_def: "∀k<length qp. qp!k = (if k∈set l then List_Index.index l k else length qp)"
  begin  
    lemma l_len: "length l ≤ length qp"
    proof -
      from card_mono[OF _ l_set] have "card (set l) ≤ length qp" by auto
      with distinct_card[OF l_distinct] show ?thesis by simp
    qed  

    lemma idx_len[simp]: "i<length l ⟹ l!i < length qp"
      using l_set
      by (metis atLeastLessThan_iff nth_mem psubsetD psubsetI)

    lemma l_set_simp[simp]: "k∈set l ⟹ k < length qp" 
      by (auto dest: subsetD[OF l_set])

    lemma qpk_idx: "k<length qp ⟹ qp ! k < length l ⟷ k ∈ set l"
    proof (rule iffI)
      assume A: "k<length qp"
      {
        assume "qp!k < length l"
        hence "qp!k < length qp" using l_len by simp
        with spec[OF qp_def, of k] A show "k∈set l" 
          by (auto split: if_split_asm)
      }
      {
        assume "k∈set l"
        thus "qp!k<length l"
          using qp_def by (auto split: if_split_asm) []
      }
    qed 

    lemma lqpk[simp]: "k ∈ set l ⟹ l ! (qp ! k) = k"
      using spec[OF qp_def, of k] by auto

    lemma "⟦i<length l; j<length l; l!i=l!j⟧ ⟹ i=j"
      by (simp add: nth_eq_iff_index_eq)
      
    lemmas index_swap[simp] = index_swap_if_distinct[folded swap_def, OF l_distinct]  

    lemma swap_invar:  
      assumes "i<length l" "j<length l"
      shows "ial_invar (length qp) (swap l i j) (qp[l ! j := i, l ! i := j])"
      using assms
      apply unfold_locales
      apply auto []
      apply auto []
      apply auto []
      apply (auto simp: simp: nth_list_update nth_eq_iff_index_eq index_nth_id) []
      using qp_def apply auto [2]
      done

  end

  definition "ial_rel1 maxsize ≡ br fst (uncurry (ial_invar maxsize))"

  definition ial_assn2 :: "nat ⇒ nat list * nat list ⇒ _" where
    "ial_assn2 maxsize ≡ prod_assn (marl_assn maxsize nat_assn) (array_assn nat_assn)"

(*  definition "ial_assn maxsize ≡ hr_comp (ial_assn2 maxsize) (ial_rel1 maxsize)"*)

  definition "ial_assn maxsize A ≡ hr_comp (hr_comp (ial_assn2 maxsize) (ial_rel1 maxsize)) (⟨the_pure A⟩list_rel)"
  lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "ial_assn maxsize A" for maxsize A]

(*  lemma ial_assn_precise[constraint_rules]: "precise (ial_assn maxsize)"
    unfolding ial_assn_def ial_rel1_def ial_assn2_def
    apply constraint_rules
*)



  subsection ‹Empty›

  definition op_ial_empty_sz :: "nat ⇒ 'a list" 
    where [simp]: "op_ial_empty_sz ms ≡ op_list_empty"

  lemma [def_pat_rules]: "op_ial_empty_sz$maxsize ≡ UNPROTECT (op_ial_empty_sz maxsize)"  
    by simp

  context fixes maxsize :: nat begin
  sepref_register "PR_CONST (op_ial_empty_sz maxsize)"
  end

  context 
    fixes maxsize :: nat (* If we do not fix maxsize here, the FCOMP-rule will 
      derive a more general rule with two different maxsizes! *)
    notes [fcomp_norm_unfold] = ial_assn_def[symmetric]  
    notes [simp] = hn_ctxt_def pure_def
  begin  
  
    definition "aial_empty ≡ do {
      let l = op_marl_empty_sz maxsize;
      let qp = op_array_replicate maxsize maxsize;
      RETURN (l,qp)
    }"

    lemma aial_empty_impl: "(aial_empty,RETURN op_list_empty) ∈ ⟨ial_rel1 maxsize⟩nres_rel"
      unfolding aial_empty_def
      apply (refine_vcg nres_relI)
      apply (clarsimp simp: ial_rel1_def br_def)
      apply unfold_locales
      apply auto
      done

    (* Note: This lemma requires some setup to handle maxsize simultaneously
      as a parameter, and as a constant. 
    *)
    context 
      notes [id_rules] = itypeI[Pure.of maxsize "TYPE(nat)"]
      notes [sepref_import_param] = IdI[of maxsize]
    begin
    sepref_definition ial_empty is "uncurry0 aial_empty" :: "unit_assn⇧k →⇩a ial_assn2 maxsize"
      unfolding aial_empty_def ial_assn2_def
      using [[id_debug]]
      by sepref
    end  

    sepref_decl_impl (no_register) ial_empty: ial_empty.refine[FCOMP aial_empty_impl] .
    lemma ial_empty_sz_hnr[sepref_fr_rules]: 
      "(uncurry0 local.ial_empty, uncurry0 (RETURN (PR_CONST (op_ial_empty_sz maxsize)))) ∈ unit_assn⇧k →⇩a ial_assn maxsize A"
      using ial_empty_hnr[of A] by simp
  
    subsection ‹Swap›
    definition "aial_swap ≡ λ(l,qp) i j. do {
      vi ← mop_list_get l i;
      vj ← mop_list_get l j;
      l ← mop_list_set l i vj;
      l ← mop_list_set l j vi;
      qp ← mop_list_set qp vj i;
      qp ← mop_list_set qp vi j;
      RETURN (l,qp)
    }"

    lemma in_ial_rel1_conv: 
      "((pq, qp), l) ∈ ial_rel1 ms ⟷ pq=l ∧ ial_invar ms l qp" 
      by (auto simp: ial_rel1_def in_br_conv)

    lemma aial_swap_impl: 
      "(aial_swap,mop_list_swap) ∈ ial_rel1 maxsize → nat_rel → nat_rel → ⟨ial_rel1 maxsize⟩nres_rel"
    proof (intro fun_relI nres_relI; clarsimp simp: in_ial_rel1_conv; refine_vcg; clarsimp)
      fix l qp i j
      assume [simp]: "i<length l" "j<length l" and "ial_invar maxsize l qp"
      then interpret ial_invar maxsize l qp by simp

      show "aial_swap (l, qp) i j ≤ SPEC (λc. (c, swap l i j) ∈ ial_rel1 maxsize)"
        unfolding aial_swap_def
        apply refine_vcg
        apply (vc_solve simp add: in_ial_rel1_conv swap_def[symmetric] swap_invar)
        done
    qed    
  
    sepref_definition ial_swap is
      "uncurry2 aial_swap" :: "(ial_assn2 maxsize)⇧d *⇩a nat_assn⇧k *⇩a nat_assn⇧k →⇩a ial_assn2 maxsize"
      unfolding aial_swap_def ial_assn2_def
      by sepref

    sepref_decl_impl (ismop) test: ial_swap.refine[FCOMP aial_swap_impl] 
      uses mop_list_swap.fref .

    subsection ‹Length›
    definition aial_length :: "aial ⇒ nat nres" 
      where "aial_length ≡ λ(l,_). RETURN (op_list_length l)"
  
    lemma aial_length_impl: "(aial_length, mop_list_length) ∈ ial_rel1 maxsize → ⟨nat_rel⟩nres_rel"
      apply (intro fun_relI nres_relI)
      unfolding ial_rel1_def in_br_conv aial_length_def
      by auto

    sepref_definition ial_length is "aial_length" :: "(ial_assn2 maxsize)⇧k →⇩a nat_assn"
      unfolding aial_length_def ial_assn2_def
      by sepref

    sepref_decl_impl (ismop) ial_length: ial_length.refine[FCOMP aial_length_impl] .  
    
    subsection ‹Index›  
    
    definition aial_index :: "aial ⇒ nat ⇒ nat nres" where
      "aial_index ≡ λ(l,qp) k. do {
        ASSERT (k∈set l);
        i ← mop_list_get qp k;
        RETURN i
      }"
  
    lemma aial_index_impl: 
      "(uncurry aial_index, uncurry mop_list_index) ∈ 
        [λ(l,k). k∈set l]⇩f ial_rel1 maxsize ×⇩r nat_rel → ⟨nat_rel⟩nres_rel"  
      apply (intro fun_relI nres_relI frefI)
      unfolding ial_rel1_def
    proof (clarsimp simp:  in_br_conv)
      fix l qp k
      assume "ial_invar maxsize l qp"
      then interpret ial_invar maxsize l qp .
  
      assume "k∈set l"
      then show "aial_index (l,qp) k ≤ RETURN (index l k)"
        unfolding aial_index_def
        apply (refine_vcg)
        by (auto simp: qp_def)
    qed
  
    sepref_definition ial_index is "uncurry aial_index" :: "(ial_assn2 maxsize)⇧k *⇩a nat_assn⇧k →⇩a nat_assn"
      unfolding aial_index_def ial_assn2_def
      by sepref

    sepref_decl_impl (ismop) ial_index: ial_index.refine[FCOMP aial_index_impl] .

    subsection ‹Butlast›  
    definition aial_butlast :: "aial ⇒ aial nres" where
      "aial_butlast ≡ λ(l,qp). do {
        ASSERT (l≠[]);
        len ← mop_list_length l;
        k ← mop_list_get l (len - 1);
        l ← mop_list_butlast l;
        qp ← mop_list_set qp k (length qp);
        RETURN (l,qp)
      }"
  
    lemma aial_butlast_refine: "(aial_butlast, mop_list_butlast) ∈ ial_rel1 maxsize → ⟨ial_rel1 maxsize⟩nres_rel"  
      apply (intro fun_relI nres_relI)
      unfolding ial_rel1_def
    proof (clarsimp simp: in_br_conv simp del: mop_list_butlast_alt)
      fix l qp
      assume "ial_invar maxsize l qp"
      then interpret ial_invar maxsize l qp .
  
      {
        assume A: "l≠[]"
        have "ial_invar (length qp) (butlast l) (qp[l ! (length l - Suc 0) := length qp])"
          apply standard
          apply clarsimp_all
          apply (auto simp: distinct_butlast) []
          using l_set apply (auto dest: in_set_butlastD) []
          using qp_def A l_distinct
          apply (auto simp: nth_list_update neq_Nil_rev_conv index_append simp del: l_distinct)
          done
      } note aux1=this
  
      show "aial_butlast (l, qp) ≤ ⇓ (br fst (uncurry (ial_invar maxsize))) (mop_list_butlast l)"
        unfolding aial_butlast_def mop_list_butlast_alt
        apply refine_vcg
        apply (clarsimp_all simp: in_br_conv aux1)
        done
    qed    

    sepref_definition ial_butlast is aial_butlast :: "(ial_assn2 maxsize)⇧d →⇩a ial_assn2 maxsize"
      unfolding aial_butlast_def ial_assn2_def by sepref

    sepref_decl_impl (ismop) ial_butlast: ial_butlast.refine[FCOMP aial_butlast_refine] .

    subsection ‹Append›  
    definition aial_append :: "aial ⇒ nat ⇒ aial nres" where
      "aial_append ≡ λ(l,qp) k. do {
        ASSERT (k<length qp ∧ k∉set l ∧ length l < length qp);
        len ← mop_list_length l;
        l ← mop_list_append l k;
        qp ← mop_list_set qp k len;
        RETURN (l,qp)
      }"

    lemma aial_append_refine: 
      "(uncurry aial_append,uncurry mop_list_append) ∈ 
        [λ(l,k). k<maxsize ∧ k∉set l]⇩f ial_rel1 maxsize ×⇩r nat_rel → ⟨ial_rel1 maxsize⟩nres_rel"
      apply (intro frefI nres_relI)  
      unfolding ial_rel1_def
    proof (clarsimp simp: in_br_conv)
      fix l qp k
      assume KLM: "k<maxsize" and KNL: "k∉set l"
      assume "ial_invar maxsize l qp"
      then interpret ial_invar maxsize l qp .
    
      from KLM have KLL: "k<length qp" by simp
    
      note distinct_card[OF l_distinct, symmetric]
      also from KNL l_set have "set l ⊆ {0..<k} ∪ {Suc k..<length qp}"
        by (auto simp: nat_less_le)
      from card_mono[OF _ this] have "card (set l) ≤ card …"
        by simp
      also note card_Un_le
      also have "card {0..<k} + card {Suc k..<length qp} = k + (length qp - Suc k)" 
        by simp
      also have "… < length qp" using KLL by simp
      finally have LLEN: "length l < length qp" .
    
      have aux1[simp]: "ial_invar (length qp) (l @ [k]) (qp[k := length l])"
        apply standard
        apply (clarsimp_all simp: KNL KLL)
        using KLL apply (auto simp: Suc_le_eq LLEN) []
        apply (auto simp: index_append KNL nth_list_update')
        apply (simp add: qp_def)
        apply (simp add: qp_def)
        done
    
      show "aial_append (l, qp) k ≤ ⇓ (br fst (uncurry (ial_invar maxsize))) (RETURN (l@[k]))"
        unfolding aial_append_def mop_list_append_def
        apply refine_vcg
        apply (clarsimp_all simp: in_br_conv KLL KNL LLEN)
        done
    qed    

    private lemma aial_append_impl_aux: "((l, qp), l') ∈ ial_rel1 maxsize ⟹ l'=l ∧ maxsize = length qp"
      unfolding ial_rel1_def
      by (clarsimp simp: in_br_conv ial_invar.maxsize_eq[symmetric])

    context      
      notes [dest!] = aial_append_impl_aux
    begin  
      (* TODO: Should we integrate the domain-condition, or some similar condition, 
        as assertion (relating length l and length qp) or into ial_assn2 ? *)
      sepref_definition ial_append is 
        "uncurry aial_append" :: "[λ(lqp,_). lqp∈Domain (ial_rel1 maxsize)]⇩a (ial_assn2 maxsize)⇧d *⇩a nat_assn⇧k → ial_assn2 maxsize"
        unfolding aial_append_def ial_assn2_def
        by sepref
    end    

    lemma "(λb. b<maxsize, X) ∈ A → bool_rel"
      apply auto
      oops

    context begin  
      (* TODO: Maybe inject additional restrictions on sepref_decl_impl command *)
      (* TODO: Maybe require Domain R ⊆ {0..<maxsize} instead ? *)
      private lemma append_fref': "⟦IS_BELOW_ID R⟧ 
        ⟹ (uncurry mop_list_append, uncurry mop_list_append) ∈ ⟨R⟩list_rel ×⇩r R →⇩f ⟨⟨R⟩list_rel⟩nres_rel"  
        by (rule mop_list_append.fref)
  
      sepref_decl_impl (ismop) ial_append: ial_append.refine[FCOMP aial_append_refine] uses append_fref'
        unfolding IS_BELOW_ID_def
        apply (parametricity; auto simp: single_valued_below_Id)
        done
    end    

    (*
    lemmas ial_append_hnr_mop[sepref_fr_rules] = ial_append.refine[FCOMP aial_append_refine]
    lemmas ial_append_hnr[sepref_fr_rules] = ial_append_hnr_mop[FCOMP mk_op_rl2_np[OF mop_list_append_alt]]
    *)

    subsection ‹Get›
    
    definition aial_get :: "aial ⇒ nat ⇒ nat nres" where
      "aial_get ≡ λ(l,qp) i. mop_list_get l i"
  
    lemma aial_get_refine: "(aial_get,mop_list_get) ∈ ial_rel1 maxsize → nat_rel → ⟨nat_rel⟩nres_rel"  
      apply (intro fun_relI nres_relI)
      unfolding aial_get_def ial_rel1_def mop_list_get_def in_br_conv
      apply refine_vcg
      apply clarsimp_all
      done

    sepref_definition ial_get is "uncurry aial_get" :: "(ial_assn2 maxsize)⇧k *⇩a nat_assn⇧k →⇩a nat_assn"
      unfolding aial_get_def ial_assn2_def by sepref

    sepref_decl_impl (ismop) ial_get: ial_get.refine[FCOMP aial_get_refine] .  

    subsection ‹Contains›
    
    definition aial_contains :: "nat ⇒ aial ⇒ bool nres" where
      "aial_contains ≡ λk (l,qp). do {
        if k<maxsize then do {
          i ← mop_list_get qp k;
          RETURN (i<maxsize)
        } else RETURN False  
      }"
  
    lemma aial_contains_refine: "(uncurry aial_contains,uncurry mop_list_contains) 
      ∈ (nat_rel ×⇩r ial_rel1 maxsize) →⇩f ⟨bool_rel⟩nres_rel"  
      apply (intro frefI nres_relI)
      unfolding ial_rel1_def
    proof (clarsimp simp: in_br_conv)
      fix l qp k
      (*assume A: "k<maxsize"*)
      assume "ial_invar maxsize l qp"
      then interpret ial_invar maxsize l qp .

      show "aial_contains k (l, qp) ≤ RETURN (k∈set l)"
        unfolding aial_contains_def
        apply refine_vcg
        by (auto simp: l_len qp_def split: if_split_asm)
    qed    
  
    context 
      notes [id_rules] = itypeI[Pure.of maxsize "TYPE(nat)"]
      notes [sepref_import_param] = IdI[of maxsize]
    begin
      sepref_definition ial_contains is "uncurry aial_contains" :: "nat_assn⇧k *⇩a (ial_assn2 maxsize)⇧k →⇩a bool_assn"
        unfolding aial_contains_def ial_assn2_def by sepref
    end  

    sepref_decl_impl (ismop) ial_contains: ial_contains.refine[FCOMP aial_contains_refine] .
  end



  interpretation ial_sz: list_custom_empty "ial_assn N A" "ial_empty N" "PR_CONST (op_ial_empty_sz N)"
    apply unfold_locales
    apply (rule ial_empty_sz_hnr [unfolded op_ial_empty_sz_def PR_CONST_def])
    by simp


end