Theory Refine_Imperative_HOL.IICF_List

theory IICF_List
imports 
  "../../Sepref"
  "List-Index.List_Index"
begin

lemma param_index[param]: 
  "⟦single_valued A; single_valued (A¯)⟧ ⟹ (index,index) ∈ ⟨A⟩list_rel → A → nat_rel"
  unfolding index_def[abs_def] find_index_def 
  apply (subgoal_tac "(((=), (=)) ∈ A → A → bool_rel)")
  apply parametricity
  by (simp add: pres_eq_iff_svb)


(* TODO: Move? *)
subsection ‹Swap two elements of a list, by index›

definition "swap l i j ≡ l[i := l!j, j:=l!i]"
lemma swap_nth[simp]: "⟦i < length l; j<length l; k<length l⟧ ⟹
  swap l i j!k = (
    if k=i then l!j
    else if k=j then l!i
    else l!k
  )"
  unfolding swap_def
  by auto

lemma swap_set[simp]: "⟦ i < length l; j<length l ⟧ ⟹ set (swap l i j) = set l"  
  unfolding swap_def
  by auto

lemma swap_multiset[simp]: "⟦ i < length l; j<length l ⟧ ⟹ mset (swap l i j) = mset l"  
  unfolding swap_def
  by (auto simp: mset_swap)


lemma swap_length[simp]: "length (swap l i j) = length l"  
  unfolding swap_def
  by auto

lemma swap_same[simp]: "swap l i i = l"
  unfolding swap_def by auto

lemma distinct_swap[simp]: 
  "⟦i<length l; j<length l⟧ ⟹ distinct (swap l i j) = distinct l"
  unfolding swap_def
  by auto

lemma map_swap: "⟦i<length l; j<length l⟧ 
  ⟹ map f (swap l i j) = swap (map f l) i j"
  unfolding swap_def 
  by (auto simp add: map_update)

lemma swap_param[param]: "⟦ i<length l; j<length l; (l',l)∈⟨A⟩list_rel; (i',i)∈nat_rel; (j',j)∈nat_rel⟧
  ⟹ (swap l' i' j', swap l i j)∈⟨A⟩list_rel"
  unfolding swap_def
  by parametricity

lemma swap_param_fref: "(uncurry2 swap,uncurry2 swap) ∈ 
  [λ((l,i),j). i<length l ∧ j<length l]⇩f (⟨A⟩list_rel ×⇩r nat_rel) ×⇩r nat_rel → ⟨A⟩list_rel"
  apply rule apply clarsimp
  unfolding swap_def
  apply parametricity
  by simp_all

lemma param_list_null[param]: "(List.null,List.null) ∈ ⟨A⟩list_rel → bool_rel"
proof -
  have 1: "List.null = (λ[] ⇒ True | _ ⇒ False)" 
    apply (rule ext) subgoal for l by (cases l) (auto simp: List.null_def)
    done 
  show ?thesis unfolding 1 by parametricity
qed

subsection ‹Operations›

sepref_decl_op list_empty: "[]" :: "⟨A⟩list_rel" .
context notes [simp] = eq_Nil_null begin
  sepref_decl_op list_is_empty: "λl. l=[]" :: "⟨A⟩list_rel →⇩f bool_rel" .
end
sepref_decl_op list_replicate: replicate :: "nat_rel → A → ⟨A⟩list_rel" .
definition op_list_copy :: "'a list ⇒ 'a list" where [simp]:  "op_list_copy l ≡ l"
sepref_decl_op (no_def) list_copy: "op_list_copy" :: "⟨A⟩list_rel → ⟨A⟩list_rel" .
sepref_decl_op list_prepend: "(#)" :: "A → ⟨A⟩list_rel → ⟨A⟩list_rel" .
sepref_decl_op list_append: "λxs x. xs@[x]" :: "⟨A⟩list_rel → A → ⟨A⟩list_rel" .
sepref_decl_op list_concat: "(@)" :: "⟨A⟩list_rel → ⟨A⟩list_rel → ⟨A⟩list_rel" .
sepref_decl_op list_length: length :: "⟨A⟩list_rel → nat_rel" .
sepref_decl_op list_get: nth :: "[λ(l,i). i<length l]⇩f ⟨A⟩list_rel ×⇩r nat_rel → A" .
sepref_decl_op list_set: list_update :: "[λ((l,i),_). i<length l]⇩f (⟨A⟩list_rel ×⇩r nat_rel) ×⇩r A → ⟨A⟩list_rel" .
context notes [simp] = eq_Nil_null begin
  sepref_decl_op list_hd: hd :: "[λl. l≠[]]⇩f ⟨A⟩list_rel → A" .
  sepref_decl_op list_tl: tl :: "[λl. l≠[]]⇩f ⟨A⟩list_rel → ⟨A⟩list_rel" .
  sepref_decl_op list_last: last :: "[λl. l≠[]]⇩f ⟨A⟩list_rel → A" .
  sepref_decl_op list_butlast: butlast :: "[λl. l≠[]]⇩f ⟨A⟩list_rel → ⟨A⟩list_rel" .
end
sepref_decl_op list_contains: "λx l. x∈set l" :: "A → ⟨A⟩list_rel → bool_rel" 
  where "single_valued A" "single_valued (A¯)" .
sepref_decl_op list_swap: swap :: "[λ((l,i),j). i<length l ∧ j<length l]⇩f (⟨A⟩list_rel ×⇩r nat_rel) ×⇩r nat_rel → ⟨A⟩list_rel" .
sepref_decl_op list_rotate1: rotate1 :: "⟨A⟩list_rel → ⟨A⟩list_rel" .
sepref_decl_op list_rev: rev :: "⟨A⟩list_rel → ⟨A⟩list_rel" .
sepref_decl_op list_index: index :: "⟨A⟩list_rel → A → nat_rel" 
  where "single_valued A" "single_valued (A¯)" .

subsection ‹Patterns›
lemma [def_pat_rules]:
  "[] ≡ op_list_empty"
  "(=) $l$[] ≡ op_list_is_empty$l"
  "(=) $[]$l ≡ op_list_is_empty$l"
  "replicate$n$v ≡ op_list_replicate$n$v"
  "Cons$x$xs ≡ op_list_prepend$x$xs"
  "(@) $xs$(Cons$x$[]) ≡ op_list_append$xs$x"
  "(@) $xs$ys ≡ op_list_concat$xs$ys"
  "op_list_concat$xs$(Cons$x$[]) ≡ op_list_append$xs$x"
  "length$xs ≡ op_list_length$xs"
  "nth$l$i ≡ op_list_get$l$i"
  "list_update$l$i$x ≡ op_list_set$l$i$x"
  "hd$l ≡ op_list_hd$l"
  "hd$l ≡ op_list_hd$l"
  "tl$l ≡ op_list_tl$l"
  "tl$l ≡ op_list_tl$l"
  "last$l ≡ op_list_last$l"
  "butlast$l ≡ op_list_butlast$l"
  "(∈) $x$(set$l) ≡ op_list_contains$x$l"
  "swap$l$i$j ≡ op_list_swap$l$i$j"
  "rotate1$l ≡ op_list_rotate1$l"
  "rev$l ≡ op_list_rev$l"
  "index$l$x ≡ op_list_index$l$x"
  by (auto intro!: eq_reflection)

text ‹Standard preconditions are preserved by list-relation. These lemmas are used for
  simplification of preconditions after composition.›
lemma list_rel_pres_neq_nil[fcomp_prenorm_simps]: "(x',x)∈⟨A⟩list_rel ⟹ x'≠[] ⟷ x≠[]" by auto
lemma list_rel_pres_length[fcomp_prenorm_simps]: "(x',x)∈⟨A⟩list_rel ⟹ length x' = length x" by (rule list_rel_imp_same_length)

locale list_custom_empty = 
  fixes rel empty and op_custom_empty :: "'a list"
  assumes customize_hnr_aux: "(uncurry0 empty,uncurry0 (RETURN (op_list_empty::'a list))) ∈ unit_assn⇧k →⇩a rel"
  assumes op_custom_empty_def: "op_custom_empty = op_list_empty"
begin
  sepref_register op_custom_empty :: "'c list"

  lemma fold_custom_empty:
    "[] = op_custom_empty"
    "op_list_empty = op_custom_empty"
    "mop_list_empty = RETURN op_custom_empty"
    unfolding op_custom_empty_def by simp_all

  lemmas custom_hnr[sepref_fr_rules] = customize_hnr_aux[folded op_custom_empty_def]
end


lemma gen_mop_list_swap: "mop_list_swap l i j = do {
    xi ← mop_list_get l i;
    xj ← mop_list_get l j;
    l ← mop_list_set l i xj;
    l ← mop_list_set l j xi;
    RETURN l
  }"
  unfolding mop_list_swap_def
  by (auto simp: pw_eq_iff refine_pw_simps swap_def)


end