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