Theory Sort_Descending

theory Sort_Descending
imports Main
begin

sectionsorting descending
  context linorder
  begin
  fun sorted_descending :: "'a list  bool" where
    "sorted_descending []  True" |
    "sorted_descending (a#as)  (x  set as. a  x)  sorted_descending as"
  
  definition sort_descending_key :: "('b  'a)  'b list  'b list" where
    "sort_descending_key f xs  rev (sort_key f xs)"
  end
  lemma sorted_descending_Cons: "sorted_descending (x#xs)  sorted_descending xs  (yset xs. y  x)"
  by(induction xs) auto
  
  lemma sorted_descending_tail: "sorted_descending (xs@[x])  sorted_descending xs  (yset xs. x  y)"
  by(induction xs) auto
  
  lemma sorted_descending_append: "sorted_descending (xs @ ys) = 
    (sorted_descending xs  sorted_descending ys  (xset xs. yset ys. x  y))"
  by(induction xs) auto
  
  lemma sorted_descending: "sorted_descending (rev xs)  sorted xs"
  apply(induction xs)
   apply(simp)
  apply(auto simp add: sorted_descending_tail)
  done
  lemma sorted_descending_alt: "sorted_descending xs  sorted (rev xs)"
    using sorted_descending[of "rev xs"] unfolding rev_rev_ident .
  
  lemma sort_descending: "sorted_descending (sort_descending_key (λx. x) xs)"
    by(simp add: sort_descending_key_def sorted_descending)

  lemma sort_descending_key_distinct: "distinct xs  distinct (sort_descending_key f xs)"
    by(simp add: sort_descending_key_def)

  lemma sorted_descending_sort_descending_key: "sorted_descending (map f (sort_descending_key f xs))"
    apply(simp add: sort_descending_key_def)
    using sorted_descending by (metis rev_map sorted_sort_key)

  lemma sorted_descending_split: "sorted_descending (map f l)  
  	m n. l = m @ n  (e  set m. f (hd l) = f e)  (e  set n. f e < f (hd l))"
  proof(induction l)
  	case Nil thus ?case by simp
  next
  	case (Cons a as)
  	from Cons(2) have IHm: "sorted_descending (map f as)" by simp
  	note mIH = Cons(1)[OF this]
  	thus ?case (is ?kees)
  	proof(cases as)
  		case Nil
  		show ?kees unfolding Nil by force
  	next
  		case (Cons aa ass)
  		show ?kees
  		proof(cases "f a = f aa")
  			case True
  			from mIH obtain m n where mn: "as = m @ n" "(eset m. f a = f e)" "(eset n. f e < f a)" 
  				using True local.Cons by auto
  			have "a # as = a # m @ n" using mn(1) by simp
  			moreover have "eset (a # m). f (hd (a # m)) = f e" unfolding list.sel(1) using True mn(2) using Cons by auto
  			ultimately show "m n. a # as = m @ n  (eset m. f (hd (a # as)) = f e)  
  				(eset n. f e < f (hd (a # as)))" using mn(3) by (metis append.simps(2) list.sel(1))
  		next
  			case False
  			from Cons.prems have "yset (map f as). y < f a"
  				unfolding list.map(2) 
  				unfolding sorted_descending_Cons
  				unfolding set_map
  				unfolding local.Cons
  				using False 
  				by auto
  			then have "eset as. f e < f a" by simp
  			moreover have "a # as = [a] @ as  (eset [a]. f (hd [a]) = f e)" by simp
  			ultimately show ?kees by (metis list.sel(1))
  		qed
  	qed
  qed
  
  lemma sort_descending_set_inv[simp]: "set (sort_descending_key k t) = set t"
  	by (simp add: sort_descending_key_def)
  	
end