Theory Sorting_Partially_Sorted

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

  
  
context 
  fixes LT :: "'a'abool"  
begin
    
  definition "slice_LT xs ys  xset xs. yset ys. LT x y"  
  
  definition "is_slicing n xs ss  xs = concat ss  (sset 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  (yset 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: "nm  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 "xset xss" for x
      using that SLIX 
      unfolding is_slicing_def
      by auto
      
    have YSS_ELEMS: "set y  set ys" if "yset 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; 1n  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: "ni" "i<length xs"  
    shows "LT (xs!0) (xs!i)"  
  proof -  
    from S have "n0" i0 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 i0 by auto
      
    from XSEQ1 XSEQ2 have "x#s@concat ss' = xs1@xi#xs2" by simp
    then have "xiset (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