Theory Sorting_Partially_Sorted

theory Sorting_Partially_Sorted
imports Main "HOL-Library.Multiset"
begin

  
  
context 
  fixes LT :: "'a⇒'a⇒bool"  
begin
    
  definition "slice_LT xs ys ≡ ∀x∈set xs. ∀y∈set ys. LT x y"  
  
  definition "is_slicing n xs ss ≡ xs = concat ss ∧ (∀s∈set ss. s≠[] ∧ length s ≤ n)"
  
  definition "part_sorted_wrt n xs ≡ ∃ss. is_slicing n xs ss ∧ sorted_wrt slice_LT ss"


  lemma slice_LT_cons1: 
    "slice_LT (x#xs) ys ⟷ (∀y∈set ys. LT x y) ∧ (slice_LT xs ys)" by (auto simp: slice_LT_def)
  
  lemma slice_LT_mset_eq1: "mset xs = mset xs' ⟹ slice_LT xs ys ⟷ slice_LT xs' ys"
    unfolding slice_LT_def by (auto dest: mset_eq_setD)
  
  lemma slice_LT_mset_eq2: "mset ys = mset ys' ⟹ slice_LT xs ys ⟷ slice_LT xs ys'"
    unfolding slice_LT_def by (auto dest: mset_eq_setD)
  
  lemma slice_LT_setcongI: "⟦slice_LT xs ys; set xs = set xs'; set ys = set ys' ⟧ ⟹ slice_LT xs' ys'"
    unfolding slice_LT_def by auto
    
  
    
  lemma is_slicing_empty1[simp]: "is_slicing n [] ss ⟷ ss=[]" by (auto simp: is_slicing_def)
  lemma is_slicing_empty2[simp]: "is_slicing n xs [] ⟷ xs=[]" by (auto simp: is_slicing_def)
    
  lemma is_slicing_cons2: "is_slicing n xs (s#ss) ⟷ s≠[] ∧ length s ≤ n ∧ (∃xs'. xs=s@xs' ∧ is_slicing n xs' ss)"
    by (auto simp: is_slicing_def)

  lemma part_sorted_wrt_Nil[iff]: "part_sorted_wrt n []"
    unfolding part_sorted_wrt_def is_slicing_def by (auto intro: exI[where x="[]"])
  
  lemma part_sorted_wrt_zero_iff_empty[simp]: "part_sorted_wrt 0 xs ⟷ xs=[]"
    unfolding part_sorted_wrt_def is_slicing_def
    by auto
  
  lemma part_sorted_wrt_mono: "n≤m ⟹ part_sorted_wrt n xs ⟹ part_sorted_wrt m xs"  
    unfolding part_sorted_wrt_def is_slicing_def
    by fastforce
    
  lemma part_sorted_wrt_init: "length xs ≤ n ⟹ part_sorted_wrt n xs"
    apply (cases xs)  
    subgoal by simp
    subgoal
      unfolding part_sorted_wrt_def is_slicing_def
      by (auto intro: exI[where x="[xs]"])
    done
  
  lemma part_sorted_concatI:
    assumes PSX: "part_sorted_wrt n xs"
        and PSY: "part_sorted_wrt n ys" 
        and SLT: "slice_LT xs ys" 
    shows "part_sorted_wrt n (xs@ys)"  
  proof -
    from PSX obtain xss where SLIX: "is_slicing n xs xss" and SX: "sorted_wrt slice_LT xss" unfolding part_sorted_wrt_def by blast
    from PSY obtain yss where SLIY: "is_slicing n ys yss" and SY: "sorted_wrt slice_LT yss" unfolding part_sorted_wrt_def by blast
  
    from SLIX SLIY have SLICING: "is_slicing n (xs@ys) (xss@yss)"  (* TODO: make this a lemma: is_slicing_concatI *)
      unfolding is_slicing_def
      by auto
  
    have XSS_ELEMS: "set x ⊆ set xs" if "x∈set xss" for x
      using that SLIX 
      unfolding is_slicing_def
      by auto
      
    have YSS_ELEMS: "set y ⊆ set ys" if "y∈set yss" for y
      using that SLIY 
      unfolding is_slicing_def
      by auto
      
    have "local.slice_LT lx ly" if "lx ∈ set xss" "ly ∈ set yss" for lx ly
      using that XSS_ELEMS YSS_ELEMS SLT unfolding slice_LT_def by blast
      
    then have "sorted_wrt slice_LT (xss@yss)" using SX SY 
      by (auto simp: sorted_wrt_append)
    with SLICING show ?thesis unfolding part_sorted_wrt_def by auto
  qed
  
    
  lemma sorted_wrt_imp_part_sorted1: "sorted_wrt LT xs ⟹ part_sorted_wrt 1 xs"  
    unfolding part_sorted_wrt_def
    apply (rule exI[where x="map (λx. [x]) xs"])
    unfolding is_slicing_def 
    by (auto simp: sorted_wrt_map slice_LT_def)

  lemma sorted_wrt_imp_part_sorted: "⟦sorted_wrt LT xs; 1≤n⟧ ⟹ part_sorted_wrt n xs"  
    using part_sorted_wrt_mono[of 1 n xs] sorted_wrt_imp_part_sorted1 by simp
    
        
  lemma part_sorted_guardedI:
    assumes S: "part_sorted_wrt n xs" and B: "n≤i" "i<length xs"  
    shows "LT (xs!0) (xs!i)"  
  proof -  
    from S have "n≠0" ‹i≠0› using B by (cases n; auto)+
    
    
    from S obtain ss where SL: "is_slicing n xs ss" and SORTED: "sorted_wrt slice_LT ss" unfolding part_sorted_wrt_def by auto
    from SL ‹i<length xs› obtain x s ss' where SSEQ: "ss=(x#s)#ss'" and XSEQ1: "xs = x#s@concat ss'" and L: "length (x#s) ≤ n"
      apply (cases xs; simp)
      apply (cases ss; simp)
      apply (auto simp: is_slicing_cons2 Cons_eq_append_conv)
      by (metis is_slicing_def)
  
    define xi where "xi = xs!i"
    obtain xs1 xs2 where XSEQ2: "xs=xs1@xi#xs2" and "length xs1 = i"
      unfolding xi_def using id_take_nth_drop[OF ‹i<length xs›] B by simp
    
    have "xs1 ≠ []" using ‹length xs1 = i› ‹i≠0› by auto
      
    from XSEQ1 XSEQ2 have "x#s@concat ss' = xs1@xi#xs2" by simp
    then have "xi∈set (concat ss')"
      supply [simp del] = set_concat
      using ‹xs1 ≠ []›
      using L B ‹length xs1 = i›
      by (auto simp: append_eq_append_conv2 Cons_eq_append_conv append_eq_Cons_conv)
      
    with SSEQ SORTED have "LT x xi"  
      by (auto simp: slice_LT_cons1)
    thus ?thesis unfolding xi_def XSEQ1 by simp
  qed      

    
end  


lemma slice_LT_mono: "⟦slice_LT R xs ys; (⋀x y. R x y ⟹ R' x y)⟧ ⟹ slice_LT R' xs ys"  
  by (auto simp: slice_LT_def)
  



end