# 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

(* 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

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
```