Theory IICF_List

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

lemma param_index[param]: 
  "single_valued A; single_valued (A¯)  (index,index)  Alist_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)Alist_rel; (i',i)nat_rel; (j',j)nat_rel
   (swap l' i' j', swap l i j)Alist_rel"
  unfolding swap_def
  by parametricity

lemma swap_param_fref: "(uncurry2 swap,uncurry2 swap)  
  [λ((l,i),j). i<length l  j<length l]f (Alist_rel ×r nat_rel) ×r nat_rel  Alist_rel"
  apply rule apply clarsimp
  unfolding swap_def
  apply parametricity
  by simp_all

lemma param_list_null[param]: "(List.null,List.null)  Alist_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: "[]" :: "Alist_rel" .
context notes [simp] = eq_Nil_null begin
  sepref_decl_op list_is_empty: "λl. l=[]" :: "Alist_rel f bool_rel" .
end
sepref_decl_op list_replicate: replicate :: "nat_rel  A  Alist_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" :: "Alist_rel  Alist_rel" .
sepref_decl_op list_prepend: "(#)" :: "A  Alist_rel  Alist_rel" .
sepref_decl_op list_append: "λxs x. xs@[x]" :: "Alist_rel  A  Alist_rel" .
sepref_decl_op list_concat: "(@)" :: "Alist_rel  Alist_rel  Alist_rel" .
sepref_decl_op list_length: length :: "Alist_rel  nat_rel" .
sepref_decl_op list_get: nth :: "[λ(l,i). i<length l]f Alist_rel ×r nat_rel  A" .
sepref_decl_op list_set: list_update :: "[λ((l,i),_). i<length l]f (Alist_rel ×r nat_rel) ×r A  Alist_rel" .
context notes [simp] = eq_Nil_null begin
  sepref_decl_op list_hd: hd :: "[λl. l[]]f Alist_rel  A" .
  sepref_decl_op list_tl: tl :: "[λl. l[]]f Alist_rel  Alist_rel" .
  sepref_decl_op list_last: last :: "[λl. l[]]f Alist_rel  A" .
  sepref_decl_op list_butlast: butlast :: "[λl. l[]]f Alist_rel  Alist_rel" .
end
sepref_decl_op list_contains: "λx l. xset l" :: "A  Alist_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 (Alist_rel ×r nat_rel) ×r nat_rel  Alist_rel" .
sepref_decl_op list_rotate1: rotate1 :: "Alist_rel  Alist_rel" .
sepref_decl_op list_rev: rev :: "Alist_rel  Alist_rel" .
sepref_decl_op list_index: index :: "Alist_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)Alist_rel  x'[]  x[]" by auto
lemma list_rel_pres_length[fcomp_prenorm_simps]: "(x',x)Alist_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_assnk 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