Theory List_Assn

theory List_Assn
  imports "../lib/Base_MEC"
begin

  lemma dr_assn_eq_iff: "a=b ⟷ ↿a = ↿b"
    unfolding dr_assn_prefix_def
    by (metis Rep_dr_assn_inject)


  subsection ‹List Assertion›

  text ‹A list_assn encodes a list in which each element is related through assertion A›
  definition "list_assn A ≡ mk_assn (λxs xsi. ↑(length xs = length xsi) ** (⋃*i∈{0..<length xs}. ↿A (xs!i) (xsi!i)))"

  lemma pure_part_list_assn [vcg_prep_ext_rules]: "pure_part (↿(list_assn A) xs ys) ⟹ length ys = length xs"
    unfolding list_assn_def 
    by (auto simp: pure_part_def sep_algebra_simps)

  text ‹Inductive characterization›
  lemma list_assn_ee_simp:
    "↿(list_assn A) [] [] = □"
    unfolding list_assn_def
    by (auto simp: sep_algebra_simps)
  
  lemma list_assn_nm_simp:
    "↿(list_assn A) [] (xi#xsi) = sep_false"
    "↿(list_assn A) (x#xs) [] = sep_false"
    unfolding list_assn_def
    by (auto simp: sep_algebra_simps)


  lemma list_assn_cc_simp:
    shows "↿(list_assn A) (x#xs) (xi#xsi) = (↿A x xi ** ↿(list_assn A) xs xsi)"
    ― ‹Cons rule simp for list_assn ›
  proof -
    have intv_conv1: "{0..<Suc n} = insert 0 (Suc`{0..<n})" for n by auto
    have 1: "(⋃*i∈{0..<Suc n}. A i) = (A 0 ** (⋃*i∈{0..<n}. A (Suc i)))" for A :: "nat ⇒ ll_assn" and n
      by (simp del: image_Suc_atLeastLessThan add: intv_conv1 sep_set_img_map)
  
    show ?thesis
      unfolding list_assn_def
      by (auto simp: sep_algebra_simps entails_lift_extract_simps entails_eq_iff 1)
      
  qed
  
 
  lemmas list_assn_simps[simp] = list_assn_ee_simp list_assn_nm_simp list_assn_cc_simp
                   
  lemma list_assn_empty1_conv[simp]: "↿(list_assn A) [] ys = ↑(ys=[])"
    by (cases ys) (auto simp: sep_algebra_simps)

  lemma list_assn_empty2_conv[simp]: "↿(list_assn A) xs [] = ↑(xs=[])"
    by (cases xs) (auto simp: sep_algebra_simps)
    
    
  lemma list_assn_cons1_conv: "↿(list_assn A) (x#xs) yys = (EXS y ys. ↑(yys=y#ys) ** ↿A x y ** ↿(list_assn A) xs ys)"
    apply (cases yys)
    by (auto simp: entails_eq_iff sep_algebra_simps pred_lift_extract_simps)
  
  lemma list_assn_cons2_conv: "↿(list_assn A) xxs (y#ys) = (EXS x xs. ↑(xxs=x#xs) ** ↿A x y ** ↿(list_assn A) xs ys)"
    apply (cases xxs)
    by (auto simp: entails_eq_iff sep_algebra_simps pred_lift_extract_simps)
  
  lemma list_assn_append1_conv: "↿(list_assn A) (xs⇩1@xs⇩2) yys = (EXS ys⇩1 ys⇩2. ↑(yys=ys⇩1@ys⇩2) ** ↿(list_assn A) xs⇩1 ys⇩1 ** ↿(list_assn A) xs⇩2 ys⇩2)"
    apply (induction xs⇩1 arbitrary: yys)
    by (auto simp: sep_algebra_simps list_assn_cons1_conv)
  
  lemma list_assn_append2_conv: "↿(list_assn A) xxs (ys⇩1@ys⇩2) = (EXS xs⇩1 xs⇩2. ↑(xxs=xs⇩1@xs⇩2) ** ↿(list_assn A) xs⇩1 ys⇩1 ** ↿(list_assn A) xs⇩2 ys⇩2)"
    apply (induction ys⇩1 arbitrary: xxs)
    by (auto simp: sep_algebra_simps list_assn_cons2_conv)


  lemma list_assn_take1_conv: "↿(list_assn A) xxs yys = (EXS ys⇩1 ys⇩2. ↑(yys=ys⇩1@ys⇩2) ** ↿(list_assn A) (take n xxs) ys⇩1 ** ↿(list_assn A) (drop n xxs) ys⇩2)"
    apply(subgoal_tac "↿(list_assn A) xxs yys = ↿(list_assn A) ((take n xxs)@(drop n xxs)) yys")
    using list_assn_append1_conv[of A "(take n xxs)" "(drop n xxs)" yys] apply argo
    by force

  lemma list_assn_take2_conv: "↿(list_assn A) xxs yys = (EXS xs⇩1 xs⇩2. ↑(xxs=xs⇩1@xs⇩2) ** ↿(list_assn A) xs⇩1 (take n yys) ** ↿(list_assn A) xs⇩2 (drop n yys))"
    apply(subgoal_tac "↿(list_assn A) xxs yys = ↿(list_assn A) xxs ((take n yys)@(drop n yys))")
    using list_assn_append2_conv[of A xxs "(take n yys)" "(drop n yys)"] apply argo
    by force
    

  lemmas list_assn_one_side_conv = 
    list_assn_cons1_conv list_assn_cons2_conv
    list_assn_append1_conv list_assn_append2_conv


  lemma list_assn_neq_len[simp]: 
    "length xs ≠ length xsi ⟹ ↿(list_assn A) xs xsi = sep_false"  
    "length xsi ≠ length xs ⟹ ↿(list_assn A) xs xsi = sep_false"  
    by (auto simp: list_assn_def)
    
  lemma list_assn_append[simp]: "length xs⇩1 = length ys⇩1 
    ⟹ ↿(list_assn A) (xs⇩1@xs⇩2) (ys⇩1@ys⇩2) = (↿(list_assn A) xs⇩1 ys⇩1 ** ↿(list_assn A) xs⇩2 ys⇩2)"  
    apply (induction rule: list_induct2)
    by (auto simp: sep_algebra_simps)


  lemma entails_exE: assumes "(EXS x. P x) ⊢ Q" obtains x where "P x ⊢ Q"
    using assms unfolding entails_def   
    by blast 

  lemma entails_exE2: assumes "⋀ x. P x ⊢ Q" shows "(EXS x. P x) ⊢ Q"
    using assms unfolding entails_def   
    by blast 

  lemma list_assn_nth_conv1: "n < length xs ⟹ ↿(list_assn A) xs ys = (EXS ys1 y ys2. ↿(list_assn A) (take n xs) ys1 ** ↿A (xs ! n) y ** ↿(list_assn A) (drop (Suc n) xs) ys2 ** ↑(ys = ys1 @ y # ys2))"
    apply (subst id_take_nth_drop, assumption)
    apply (simp add: list_assn_one_side_conv sep_algebra_simps nth_append)
    done

  lemma list_assn_nth_conv2: "n < length xs ⟹(EXS ys1 y ys2. ↿(list_assn A) (take n xs) ys1 ** ↿A (xs ! n) y ** ↿(list_assn A) (drop (Suc n) xs) ys2 ** ↑(ys = ys1 @ y # ys2)) = (EXS ys1 y ys2. ↿(list_assn A) (take n xs) ys1 ** ↿A (xs ! n) y ** ↿(list_assn A) (drop (Suc n) xs) ys2 ** ↑(ys = ys1 @ y # ys2 ∧ ys ! n = y))"
    apply (rule entails_eqI)
    apply (intro entails_exE2)
    apply fri_keep
    apply (intro entails_exE2)
    apply fri_keep
    done


  lemma list_assn_nth_conv: "n < length xs ⟹ ↿(list_assn A) xs ys = (EXS ys1 y ys2. ↿(list_assn A) (take n xs) ys1 ** ↿A (xs ! n) y ** ↿(list_assn A) (drop (Suc n) xs) ys2 ** ↑(ys = ys1 @ y # ys2 ∧ ys ! n = y))"
    apply (auto simp: list_assn_nth_conv1 list_assn_nth_conv2)
    done


  lemma list_assn_pure_part[vcg_prep_ext_rules]: 
    "pure_part (↿(list_assn A) xs ys) ⟹ length xs = length ys" (* TODO: Extraction should also go to elements! *)  
    unfolding list_assn_def
    apply (vcg_prepare_external)
    by (auto)


  lemma list_assn_pure: "list_assn (mk_assn (pure R )) = (mk_assn (pure (⟨R⟩list_rel)))"
    apply(clarsimp simp add: dr_assn_eq_iff)
    apply(rule ext)
    apply(rule ext)
    proof(goal_cases)
      case (1 xs ys)
      then show ?case (*apply(induction xs arbitrary: ys) apply(case_tac ys) apply simp_all*)
      proof(induction xs arbitrary: ys)
        case Nil
        then show ?case 
          apply(cases ys) unfolding pure_def
          by auto
      next
        case (Cons a xs)
        then show ?case unfolding pure_def 
          apply(cases ys) 
          by(auto simp: sep_algebra_simps)
      qed
    qed 

  lemma list_assn_id: "list_assn (mk_assn id_assn) = (mk_assn id_assn)"
    by(simp add: list_assn_pure)


  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


  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 b_rel_list_rel: "⟨b_rel Id P⟩list_rel = b_rel Id (list_all P)"
  proof -
    have "list_all2 (eq_onp P) a b ⟹ list_all P b" for a b 
      unfolding list.rel_eq_onp 
      by(auto simp add: eq_onp_def)
    moreover have "(λx y. P x ∧ x = y) = (λx x'. x = x' ∧ P x')" 
      by fast
    moreover have "list_all P b ⟹ list_all2 (λx x'. x = x' ∧ P x') b b" for b using eq_onp_def list.pred_rel list_all2_same
      by (simp add: eq_onp_def list.pred_rel list_all2_same)
    moreover have "list_all2 (λx x'. x = x' ∧ P x') a b ⟹ a = b" for a b 
      using list_all2_eq list_all2_mono by fastforce
    ultimately show ?thesis unfolding list_rel_def b_rel_def eq_onp_def by auto
  qed

  lemma list_to_set_b_relI: "list_all P xs ⟹ distinct xs ⟹ X = set xs ⟹ (xs, X) ∈ ⟨b_rel Id P⟩list_set_rel"
    unfolding list_set_rel_def
    apply(auto simp: br_def b_rel_list_rel)
    done


  lemma list_to_set_b_rel'_setI: "list_all P xs ⟹ distinct xs ⟹ (xs, set xs) ∈ ⟨b_rel Id P⟩list_set_rel"
    unfolding list_set_rel_def
    apply(auto simp: br_def b_rel_list_rel)
    done

  lemma list_to_set_b_rel: "⟨b_rel Id P⟩list_set_rel = {(xs, set xs) | xs. list_all P xs ∧ distinct xs }"
    unfolding list_set_rel_def
    apply(auto simp: br_def b_rel_list_rel)
    done

end