Theory Order_Pair

```section ‹Order Pairs›

text ‹
An order pair consists of two relations @{term S} and @{term NS}, where @{term S}
is a strict order and @{term NS} a compatible non-strict order,
such that the combination of @{term S} and @{term NS} always results in strict decrease.
›

theory Order_Pair
imports "Abstract-Rewriting.Relative_Rewriting"
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])+

lemma compat_rtrancl:
assumes ab: "(a, b) ∈ S"
and bc: "(b, c) ∈ (NS ∪ S)⇧*"
shows "(a, c) ∈ S"
using bc
proof (induct)
case base
show ?case by (rule ab)
next
case (step c d)
from step(2-3) show ?case using compat_S_NS_point trans_S unfolding trans_def by blast
qed

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 ..

end
```