Theory IICF_List_List

theory IICF_List_List
imports 
  "../../Sepref"
begin


  context begin
    private abbreviation (input) "LR A ≡ ⟨⟨A⟩list_rel⟩list_rel"

    sepref_decl_op list_list_lempty: "λn. replicate n []" :: "nat_rel → LR A" .
    sepref_decl_op list_list_push_back: "λxss i x. xss[i:=xss!i@[x]]" 
      :: "[λ((xss,i),_). i<length xss]⇩f (LR A ×⇩r nat_rel) ×⇩r A → LR A" .

    sepref_decl_op list_list_pop_back: "λxss i. (last (xss!i), xss[i:=butlast (xss!i)])" 
      :: "[λ(xss,i). i<length xss ∧ xss!i≠[]]⇩f (LR A ×⇩r nat_rel)→ A ×⇩r LR A" 
      unfolding conv_to_is_Nil short_circuit_conv
      by parametricity
      
    sepref_decl_op list_list_upd: "λxss i j x. xss[i:=(xss!i)[j:=x]]" 
      :: "[λ(((xss,i),j),x). i<length xss ∧ j<length (xss!i)]⇩f (((LR A ×⇩r nat_rel) ×⇩r nat_rel) ×⇩r A) → LR A" 
      unfolding short_circuit_conv
      by parametricity
      
    sepref_decl_op list_list_idx: "λxss i j. xss!i!j" :: "[λ((xss,i),j). i<length xss ∧ j<length (xss!i)]⇩f ((LR A ×⇩r nat_rel) ×⇩r nat_rel) → A" 
      unfolding short_circuit_conv
      by parametricity
    
    sepref_decl_op list_list_llen: "λxss i. length (xss!i)" :: "[λ(xss,i). i<length xss]⇩f LR A ×⇩r nat_rel → nat_rel" .
    (* TODO: list_list is a proper subtype of list. So share operations! length, empty, ... *)
    sepref_decl_op list_list_len: "length :: _ list list ⇒ _" :: "LR A → nat_rel" .
    
    sepref_decl_op list_list_take: "λxss i l. (xss[i:=take l (xss!i)])" 
      :: "[λ((xss,i),l). i<length xss ∧ l≤length (xss!i)]⇩f ((LR A ×⇩r nat_rel) ×⇩r nat_rel)→ LR A" 
      unfolding conv_to_is_Nil short_circuit_conv
      by parametricity
    
  end

  locale list_list_custom_empty = 
    fixes rel empty PRE and op_custom_empty :: "nat ⇒ 'a list list"
    assumes customize_hnr_aux: "(empty,(RETURN o (op_list_list_lempty::nat ⇒ 'a list list))) ∈ [PRE]⇩a snat_assn⇧k → rel"
    assumes op_custom_empty_def: "op_custom_empty = op_list_list_lempty"
  begin
    sepref_register op_custom_empty :: "nat ⇒ 'c list list"
  
    lemma fold_custom_empty:
      "replicate n [] = op_custom_empty n"
      "op_list_list_lempty = op_custom_empty"
      "mop_list_list_lempty n = RETURN (op_custom_empty n)"
      unfolding op_custom_empty_def by simp_all
  
    lemmas custom_hnr[sepref_fr_rules] = customize_hnr_aux[folded op_custom_empty_def]
  end


  text ‹Fold lemmas for manual folding.›
  (* TODO: Why not use interface and op-id for that? *)
  lemma fold_op_list_list_push_back: "xss[i:=xss!i@[x]] = op_list_list_push_back xss i x" by simp
  lemma fold_op_list_list_pop_back: "(last (xss!i), xss[i:=butlast (xss!i)]) = op_list_list_pop_back xss i" by simp
  lemma fold_op_list_list_upd: "xss[i:=(xss!i)[j:=x]] = op_list_list_upd xss i j x" by simp
  lemma fold_op_list_list_idx: "xs!i!j = op_list_list_idx xs i j" by simp
  lemma fold_op_list_list_llen: "length (xs!i) = op_list_list_llen xs i" by simp
  lemma fold_op_list_list_take: "xss[i:=take n (xss!i)] = op_list_list_take xss i n" by simp

  lemmas fold_op_list_list = 
    fold_op_list_list_push_back
    fold_op_list_list_pop_back 
    fold_op_list_list_upd
    fold_op_list_list_idx
    fold_op_list_list_llen
    fold_op_list_list_take  
  
end