Theory Sort_Descending

theory Sort_Descending
imports Main
begin

section‹sorting 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 ∧ (∀y∈set xs. y ≤ x)"
  by(induction xs) auto
  
  lemma sorted_descending_tail: "sorted_descending (xs@[x]) ⟷ sorted_descending xs ∧ (∀y∈set xs. x ≤ y)"
  by(induction xs) auto
  
  lemma sorted_descending_append: "sorted_descending (xs @ ys) = 
    (sorted_descending xs ∧ sorted_descending ys ∧ (∀x∈set xs. ∀y∈set 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" "(∀e∈set m. f a = f e)" "(∀e∈set n. f e < f a)" 
  				using True local.Cons by auto
  			have "a # as = a # m @ n" using mn(1) by simp
  			moreover have "∀e∈set (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 ∧ (∀e∈set m. f (hd (a # as)) = f e) ∧ 
  				(∀e∈set 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 "∀y∈set (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 "∀e∈set as. f e < f a" by simp
  			moreover have "a # as = [a] @ as ∧ (∀e∈set [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