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) ∈ ⟨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? *)

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›

find_theorems INTF_OF_REL


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_take: take :: "[λ(i,l). i≤length l]⇩f nat_rel ×⇩r ⟨A⟩list_rel → ⟨A⟩list_rel" .
sepref_decl_op list_drop: drop :: "[λ(i,l). i≤length l]⇩f nat_rel ×⇩r ⟨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" .
  sepref_decl_op list_pop_last: "(λl. (last l, butlast l))" :: "[λl. l≠[]]⇩f ⟨A⟩list_rel → A ×⇩r ⟨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¯)" .

sepref_decl_op split_list: "λi xs. (take i xs, drop i xs)" :: "[λ(i,xs). i≤length xs]⇩f nat_rel ×⇩r ⟨A⟩list_rel → ⟨A⟩list_rel ×⇩r ⟨A⟩list_rel" .
sepref_decl_op join_list: "(@)" :: "⟨A⟩list_rel → ⟨A⟩list_rel → ⟨A⟩list_rel" .
  
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"
  "take$i$l ≡ op_list_take$i$l"
  "drop$i$l ≡ op_list_drop$i$l"
  "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)

declare list_rel_imp_same_length[sepref_bounds_dest]

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_swap: "swap xs i j = (let
  xi = op_list_get xs i;
  xj = op_list_get xs j;
  xs = op_list_set xs i xj;
  xs = op_list_set xs j xi 
  in xs)"
  by (auto simp: swap_def)

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 gen_swap)

lemmas gen_op_list_swap = gen_swap[folded op_list_swap_def]
  
  
end