Theory Finite_Partial_Order

section ‹Preliminaries›

subsection ‹Some Utilities for Finite Partial Orders›

text ‹For some reason there seems to be no Isaeblle support for maximal elements in finite regions
  of incomplete partial orders (such as the transitive step relation in cycle-compressed transition
  systems ;).)›

theory Finite_Partial_Order
  imports Main
begin

context preorder
begin

lemma foldl_max_inflation:
  ‹foldl max x0 xs ≤ foldl max x0 (xs @ [x])›
  unfolding foldl_append foldl.simps 
  by (simp add: ord.max_def)

lemma foldl_max_soundness:
  shows
    ‹foldl max x0 (x0 # xs) ∈ set (x0 # xs)›
proof (induct xs rule: rev_induct)
  case Nil
  then show ?case by (auto simp add: max_def)
next
  case (snoc x xs)
  then show ?case  unfolding foldl_append max_def by auto
qed

lemma foldl_max_maximal:
  shows
    ‹∀ y ∈ set (x0 # xs). foldl max x0 (x0 # xs) ≤ y ⟶ y ≤ foldl max x0 (x0 # xs)›
proof (induct xs rule: rev_induct)
  case Nil
  then show ?case by (auto simp add: max_def)
next
  case (snoc x xs)
  then show ?case unfolding foldl.simps foldl_append
    by (metis Un_insert_right append_Nil2 foldl_Cons insert_iff list.simps(15) local.order_refl
        local.order_trans ord.max_def set_append snoc.hyps)
qed
end

context order ―‹that is: partial order›
begin

lemma finite_max:
  fixes q
  defines ‹above_q ≡ {q'. q ≤ q'}›
  assumes
    ‹finite above_q›
  shows
    ‹∃ q_max. q_max ∈ above_q ∧ (∀ q''∈ above_q. q_max ≤ q'' ⟶ q'' = q_max)›
proof -
  have ‹q ∈ above_q› unfolding above_q_def by blast
  then obtain above_list where above_list_spec: ‹set (q#above_list) = above_q›
    using ‹finite above_q› finite_list by auto
  define q_max where ‹q_max ≡ foldl max q (q#above_list)›
  have ‹q_max ∈ above_q›
    unfolding q_max_def above_list_spec[symmetric] using foldl_max_soundness .
  moreover have ‹∀ q'' ∈ above_q. q_max ≤ q'' ⟶ q'' = q_max›
    unfolding q_max_def above_list_spec[symmetric] using foldl_max_maximal antisym by blast
  ultimately show ?thesis by blast
qed

end

end