# Theory Finite_Partial_Order

theory Finite_Partial_Order
imports Main
```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```