theory List_Order
imports
"../Auxiliaries/Util"
begin
named_theorems order_simps
declare O_assoc[order_simps]
locale pre_order_pair =
fixes S :: "'a rel"
and NS :: "'a rel"
assumes refl_NS: "refl NS"
and trans_S: "trans S"
and trans_NS: "trans NS"
begin
lemma refl_NS_point: "(s,s) ∈ NS" using refl_NS unfolding refl_on_def by blast
lemma NS_O_NS[order_simps]: "NS O NS = NS" "NS O NS O T = NS O T"
proof-
show "NS O NS = NS" by(fact trans_refl_imp_O_id[OF trans_NS refl_NS])
then show "NS O NS O T = NS O T" by fast
qed
lemma trancl_NS[order_simps]: "NS⇧+ = NS" using trans_NS by simp
lemma rtrancl_NS[order_simps]: "NS⇧* = NS"
by (rule trans_refl_imp_rtrancl_id[OF trans_NS refl_NS])
lemma trancl_S[order_simps]: "S⇧+ = S" using trans_S by simp
lemma S_O_S: "S O S ⊆ S" "S O S O T ⊆ S O T"
proof-
show "S O S ⊆ S" by (fact trans_O_subset[OF trans_S])
then show "S O S O T ⊆ S O T" by blast
qed
lemma trans_S_point: "⋀ x y z. (x,y) ∈ S ⟹ (y,z) ∈ S ⟹ (x,z) ∈ S"
using trans_S unfolding trans_def by blast
lemma trans_NS_point: "⋀ x y z. (x,y) ∈ NS ⟹ (y,z) ∈ NS ⟹ (x,z) ∈ NS"
using trans_NS unfolding trans_def by blast
end
locale compat_pair =
fixes S NS :: "'a rel"
assumes compat_NS_S: "NS O S ⊆ S"
and compat_S_NS: "S O NS ⊆ S"
begin
lemma compat_NS_S_point: "⋀ x y z. (x,y) ∈ NS ⟹ (y,z) ∈ S ⟹ (x,z) ∈ S"
using compat_NS_S by blast
lemma compat_S_NS_point: "⋀ x y z. (x,y) ∈ S ⟹ (y,z) ∈ NS ⟹ (x,z) ∈ S"
using compat_S_NS by blast
lemma S_O_rtrancl_NS[order_simps]: "S O NS⇧* = S" "S O NS⇧* O T = S O T"
proof-
show "S O NS⇧* = S"
proof(intro equalityI subrelI)
fix x y assume "(x,y) ∈ S O NS⇧*"
then obtain n where "(x,y) ∈ S O NS^^n" by blast
then show "(x,y) ∈ S"
proof(induct n arbitrary: y)
case 0 then show ?case by auto
next
case IH: (Suc n)
then obtain z where xz: "(x,z) ∈ S O NS^^n" and zy: "(z,y) ∈ NS" by auto
from IH.hyps[OF xz] zy have "(x,y) ∈ S O NS" by auto
with compat_S_NS show ?case by auto
qed
qed auto
then show "S O NS⇧* O T = S O T" by auto
qed
lemma rtrancl_NS_O_S[order_simps]: "NS⇧* O S = S" "NS⇧* O S O T = S O T"
proof-
show "NS⇧* O S = S"
proof(intro equalityI subrelI)
fix x y assume "(x,y) ∈ NS⇧* O S"
then obtain n where "(x,y) ∈ NS^^n O S" by blast
then show "(x,y) ∈ S"
proof(induct n arbitrary: x)
case 0 then show ?case by auto
next
case IH: (Suc n)
then obtain z where xz: "(x,z) ∈ NS" and zy: "(z,y) ∈ NS^^n O S" by (unfold relpow_Suc, auto)
from xz IH.hyps[OF zy] have "(x,y) ∈ NS O S" by auto
with compat_NS_S show ?case by auto
qed
qed auto
then show "NS⇧* O S O T = S O T" by auto
qed
end
locale order_pair = pre_order_pair S NS + compat_pair S NS
for S NS :: "'a rel"
begin
lemma S_O_NS[order_simps]: "S O NS = S" "S O NS O T = S O T" by (fact S_O_rtrancl_NS[unfolded rtrancl_NS])+
lemma NS_O_S[order_simps]: "NS O S = S" "NS O S O T = S O T" by (fact rtrancl_NS_O_S[unfolded rtrancl_NS])+
end
locale SN_ars =
fixes S :: "'a rel"
assumes SN: "SN S"
locale SN_pair = compat_pair S NS + SN_ars S for S NS :: "'a rel"
locale SN_order_pair = order_pair S NS + SN_ars S for S NS :: "'a rel"
sublocale SN_order_pair ⊆ SN_pair ..
type_synonym 'a list_ext = "'a rel ⇒ 'a rel ⇒ 'a list rel"
locale list_order_extension =
fixes s_list :: "'a list_ext"
and ns_list :: "'a list_ext"
assumes extension: "SN_order_pair S NS ⟹ SN_order_pair (s_list S NS) (ns_list S NS)"
and s_map: "⟦⋀ a b. (a,b) ∈ S ⟹ (f a,f b) ∈ S; ⋀ a b. (a,b) ∈ NS ⟹ (f a,f b) ∈ NS⟧ ⟹ (as,bs) ∈ s_list S NS ⟹ (map f as, map f bs) ∈ s_list S NS"
and ns_map: "⟦⋀ a b. (a,b) ∈ S ⟹ (f a,f b) ∈ S; ⋀ a b. (a,b) ∈ NS ⟹ (f a,f b) ∈ NS⟧ ⟹ (as,bs) ∈ ns_list S NS ⟹ (map f as, map f bs) ∈ ns_list S NS"
and all_ns_imp_ns: "length as = length bs ⟹ ⟦⋀ i. i < length bs ⟹ (as ! i, bs ! i) ∈ NS⟧ ⟹ (as,bs) ∈ ns_list S NS"
end