Theory Graph_Impl

theory Graph_Impl
  imports Main Graph Stack_Set
begin

  type_synonym node_T = size_T
  type_synonym node_t = size_t

  abbreviation "node_rel' N ≡ b_rel nat_rel (λx. x<N)"
  abbreviation "node_assn' N ≡ b_assn (snat_assn' TYPE(node_T)) (λx. x<N)"


  type_synonym list_graph = "nat list list"
  
  definition list_graph_α :: "list_graph ⇒ nat rel" where "list_graph_α xss = {(i,j). i < length xss ∧ j ∈ set (xss ! i)}"
    
  definition list_graph_invar :: "nat ⇒ list_graph ⇒ bool" where "list_graph_invar N xss = ((∀xs ∈ set xss. set xs ⊆ {0..<N}) ∧ (length xss = N))"

  definition "list_graph_rel N = br list_graph_α (list_graph_invar N)"

  definition "list_graph_succ xss v = mop_list_get xss v"

  lemma list_graph_succ_refine: "(list_graph_succ, mop_graph_succ) ∈ list_graph_rel N → node_rel' N → ⟨⟨node_rel' N⟩ list_rel⟩ nres_rel"
    unfolding list_graph_succ_def mop_graph_succ_def list_graph_rel_def list_set_rel_def
    apply(refine_vcg RETURN_SPEC_refine)
    apply (auto simp: in_br_conv list_graph_invar_def list_graph_α_def set_rel_def)
    subgoal for xss i (* TODO: Clean up this mess *)
      apply (rule exI[where x="xss!i"])
      apply (auto simp: b_rel_list_rel list_all_iff)
      apply (auto simp: in_set_conv_nth Ball_def subset_code) 
      done
    done


  definition "list_graph_assn_aux = stack_assn' TYPE(size_T) (stack_assn' TYPE(size_T) (snat_assn' TYPE(node_T)))"

  sepref_def list_graph_succ_ll is "uncurry list_graph_succ" :: "(list_graph_assn_aux)⇧k *⇩a (snat_assn' TYPE(node_T))⇧k →⇩a stack_assn' TYPE(size_T) (snat_assn' TYPE(node_T))"
    unfolding list_graph_succ_def list_graph_assn_aux_def
    supply [sepref_fr_rules] = stack_nth_copy_hnr
    apply sepref
    done

thm stack_nth_copy_hnr

  definition "list_graph_assn N = (hr_comp list_graph_assn_aux (list_graph_rel N))"

  
  lemma list_assn_shift_bound: "↿(list_assn (mk_assn (b_assn A P))) = hr_comp (↿(list_assn (mk_assn A))) (⟨b_rel Id P⟩list_rel)"
    apply (rule ext)
    apply (rule ext)
    subgoal for xs ys 
      apply(cases "length xs  = length ys")
      subgoal apply(induction rule: list_induct2)
        apply (auto simp: sep_algebra_simps hr_comp_def list_assn_one_side_conv) 
        done
      apply (auto simp: hr_comp_def fun_eq_iff)
      by (metis list_assn_neq_len(2) list_rel_pres_length pred_lift_extract_simps(2) sep_conj_commuteI)
    done

thm list_induct2

  lemma bounded_list_rel_eq: "(xs, ys) ∈ ⟨b_rel A P⟩list_rel ⟷(xs, ys) ∈ ⟨A⟩list_rel ∧ (∀ y ∈ set ys. P y)"
    apply(induction xs arbitrary: ys)
    apply auto[]
    apply clarsimp
    subgoal for x xs ys 
      apply(cases ys) 
      by auto
    done

  lemma bounded_set_rel_eq: "(xs, ys) ∈ ⟨b_rel A P⟩set_rel ⟷ (xs, ys) ∈ ⟨A⟩set_rel ∧ (∀ y ∈ ys. P y)"
    apply (auto simp: set_rel_def)
    done

  lemma br_distinct_set_to_list: "br set distinct O ⟨b_rel Id P⟩set_rel = ⟨b_rel Id P⟩list_rel O br set distinct"
    apply (auto simp: in_br_conv bounded_list_rel_eq bounded_set_rel_eq)
    done

  lemma stack_set_node_assn_shift_bound: "hr_comp (stack_set_assn snat_assn) (⟨node_rel' N⟩set_rel) = stack_set_assn (node_assn' N)"
    apply (simp add: stack_set_assn_def stack_assn_def stack_assn_raw_alt list_assn_shift_bound list_assn_pure stack_set_rel_def)
    apply (simp add: hr_comp_pure flip: hr_comp_to_assn_comp)
    apply (simp add: hr_comp_assoc br_distinct_set_to_list O_assoc flip: list_rel_compp)
    apply (simp add: list_rel_compp O_assoc) 
    done

  lemma stack_node_assn_shift_bound: "hr_comp (stack_assn snat_assn) (⟨node_rel' N⟩list_rel) = stack_assn (node_assn' N)"
    apply (simp add: stack_assn_def stack_assn_raw_alt list_assn_shift_bound list_assn_pure)
    apply (simp add: hr_comp_pure flip: hr_comp_to_assn_comp)
    apply (simp add: hr_comp_assoc br_distinct_set_to_list O_assoc flip: list_rel_compp)
    done

  context 
    notes [fcomp_norm_unfold] = list_graph_assn_def[symmetric] stack_node_assn_shift_bound
  begin

    lemmas mop_graph_succ_hnr[sepref_fr_rules] = list_graph_succ_ll.refine[FCOMP list_graph_succ_refine]
  
  end
  

end