theory Orthogonality_Impl
imports
Orthogonality
"Check-NT.Critical_Pairs_Impl"
QTRS.QDP_Framework_Impl
begin
subsection ‹Proving confluence of TRSs›
definition check_weakly_orthogonal where
"check_weakly_orthogonal R = do {
check_left_linear_trs R;
check_allm (λ (l,r). check (is_Fun l) (shows ''the TRS has variables as left-hand sides'')) R;
check_allm (λ (b,s,t). do {
check (s = t) (shows ''there is a non-trivial critical pair: '' +@+ shows_term s +@+ shows '' <- . -> ''
+@+ shows_term t)
}) (critical_pairs_impl R R)
} <+? (λs. s +@+ shows_nl +@+ shows ''hence, the following TRS is not weakly orthogonal '' +@+ shows_nl +@+ shows_trs R
+@+ indent s)"
lemma check_weakly_orthogonal: assumes "isOK(check_weakly_orthogonal R)"
shows "CR (rstep (set R))"
by (rule weakly_orthogonal_rstep_CR, insert assms[unfolded check_weakly_orthogonal_def], auto)
end