Theory Ord.Term_Order_Impl

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2011-2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Term_Order_Impl
imports 
  Term_Order
  Certification_Monads.Check_Monad
  Show.Shows_Literal
begin
 
record ('f, 'v) rel_impl =
  valid :: "showsl check"
  standard :: "showsl check" 
  desc :: showsl
  s :: "('f, 'v) rule ⇒ showsl check"
  ns :: "('f, 'v) rule ⇒ showsl check"
  nst :: "('f, 'v) rule ⇒ showsl check"
  af :: "'f af"
  top_af :: "'f af"
  SN :: "showsl check" 
  subst_s :: "showsl check" 
  ce_compat :: "showsl check" 
  co_rewr :: "showsl check" 
  top_mono :: "showsl check" 
  top_refl :: "showsl check" 
  mono_af :: "'f af"
  mono :: "('f × nat) list ⇒ showsl check"
  not_wst :: "('f × nat) list option"
  not_sst :: "('f × nat) list option"
  cpx :: "('f, 'v) complexity_measure ⇒ complexity_class ⇒ showsl check"

hide_const (open) valid standard desc s ns nst af top_af SN subst_s 
  ce_compat co_rewr top_mono mono_af mono not_wst not_sst cpx 

definition rel_impl_s :: "('f,'v)rel_impl ⇒ _ ⇒ _" where
  "rel_impl_s ri = check_allm (rel_impl.s ri)" 

definition rel_impl_ns :: "('f,'v)rel_impl ⇒ _ ⇒ _" where
  "rel_impl_ns ri = check_allm (rel_impl.ns ri)" 

definition rel_impl_nst :: "('f,'v)rel_impl ⇒ _ ⇒ _" where
  "rel_impl_nst ri = check_allm (rel_impl.nst ri)" 

lemmas rel_impl_list = rel_impl_s_def rel_impl_ns_def rel_impl_nst_def

fun not_subterm_rel_info :: "('f,'v)trs ⇒ ('f × nat)list option ⇒ bool" where
  "not_subterm_rel_info rel None = True"
| "not_subterm_rel_info rel (Some ws) =  (∀ f i. f ∉ set ws ⟶ simple_arg_pos rel f i)"

lemma simple_impl_not_subterm_rel_info: assumes "supt ⊆ rel"
  shows "not_subterm_rel_info rel anything" 
proof (cases anything)
  case (Some ws)
  show ?thesis unfolding Some not_subterm_rel_info.simps
  proof (intro allI impI)
    fix fn i
    show "simple_arg_pos rel fn i" 
    proof (cases fn)
      case fn: (Pair f n)
      show ?thesis unfolding fn
      proof (intro simple_arg_posI)
        fix ts
        show  "length ts = n ⟹ i < n ⟹ (Fun f ts, ts ! i) ∈ rel" 
          by (intro set_mp[OF assms], simp)
      qed
    qed
  qed
qed auto


abbreviation rel_impl_prop :: "('f,'v)rel_impl ⇒ ('f,'v)rule list ⇒ ('f,'v)trs ⇒ ('f,'v)trs ⇒ ('f,'v)trs ⇒ bool" where
  "rel_impl_prop impl U S NS NST ≡
       (∀ st. st ∈ set U ⟶ (
            (isOK(rel_impl.s impl st) ⟶ st ∈ S) ∧ 
            (isOK(rel_impl.ns impl st) ⟶ st ∈ NS) ∧ 
            (isOK(rel_impl.nst impl st) ⟶ st ∈ NST)))
  
       ― ‹unconditional properties›
       ∧ irrefl S 
       ∧ ctxt.closed NS 
       ∧ subst.closed NS       
       ∧ trans NS 
       ∧ refl NS 
       ∧ af_compatible (rel_impl.af impl) NS
       ∧ af_compatible (rel_impl.top_af impl) NST
       ∧ af_monotone (rel_impl.mono_af impl) S
       ∧ not_subterm_rel_info NS (rel_impl.not_wst impl) 
       ∧ not_subterm_rel_info S (rel_impl.not_sst impl)
       ― ‹properties that can be tested via flags›
       ∧ (isOK(rel_impl.standard impl) ⟶ trans S ∧ S ⊆ NS ∧ S O NS ⊆ S ∧ NS O S ⊆ S)
       ∧ (isOK(rel_impl.top_mono impl) ∨ isOK(rel_impl.standard impl) ⟶ trans S ∧ subst.closed NST ∧ trans NST ∧ NST O S ⊆ S ∧ S O NST ⊆ S)
       ∧ (∀ sig. funas_trs (set U) ⊆ set sig ⟶ isOK(rel_impl.mono impl sig) ⟶ ctxt.closed S)
       ∧ (isOK(rel_impl.top_mono impl) ⟶ top_mono NS NST)
       ∧ (isOK(rel_impl.top_refl impl) ⟶ refl NST)
       ∧ (isOK(rel_impl.SN impl) ⟶ SN S)
       ∧ (isOK(rel_impl.subst_s impl) ⟶ subst.closed S)
       ∧ (isOK(rel_impl.ce_compat impl) ⟶ ce_compatible NS)
       ∧ (∀ sig. funas_trs (set U) ⊆ set sig ⟶ isOK(rel_impl.ce_compat impl) ⟶ isOK(rel_impl.mono impl sig) ⟶ ce_compatible S)
       ∧ (isOK(rel_impl.co_rewr impl) ⟶ NS ∩ S¯ = {})
       ∧ (∀ cm cc. isOK(rel_impl.cpx impl cm cc) ⟶ deriv_bound_measure_class S cm cc)" 


definition rel_impl :: "('f,'v)rel_impl ⇒ bool" where
  "rel_impl impl = (isOK(rel_impl.valid impl) ⟶ (∀ U. ∃ S NS NST. 
      rel_impl_prop impl U S NS NST))"

definition rel_impl_mono_redpair :: "('f,'v)rel_impl ⇒ ('f,'v)rule list ⇒ ('f,'v)rule list ⇒ showsl check" where
  "rel_impl_mono_redpair ri s ns = do {
      rel_impl.valid ri;
      rel_impl.standard ri;
      rel_impl.SN ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring strong normalization of relation''));
      rel_impl.subst_s ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring stability of strict relation''));
      rel_impl.mono ri (funas_trs_list (s @ ns)) <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring monotonicity of strict relation''))      
    } <+? (λs. showsl_lit (STR ''problem with being a monotone reduction pair⏎'') ∘ s)" 

lemma rel_impl_mono_redpair: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_mono_redpair ri s ns)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_ns ri ns)" 
shows "∃ S NS NST. mono_redtriple_order S NS NST ∧ set s ⊆ S ∧ set ns ⊆ NS
   ∧ (isOK(rel_impl.cpx ri cm cc) ⟶ deriv_bound_measure_class S cm cc)" 
proof -
  from checks[unfolded rel_impl_mono_redpair_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and std: "isOK(rel_impl.standard ri)" 
    and sn: "isOK (rel_impl.SN ri)" 
    and mono: "isOK (rel_impl.mono ri (funas_trs_list (s @ ns)))" 
    and subst: "isOK (rel_impl.subst_s ri)" 
    by auto
  let ?U = "s @ ns" 
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S NS NST
    where "rel_impl_prop ri ?U S NS NST" by presburger
  with orient subst mono sn std
  have *: "set s ⊆ S" "set ns ⊆ NS" 
     "S ⊆ NS" 
     "ctxt.closed NS" "ctxt.closed S" 
     "subst.closed NS" "subst.closed S"
     "S O NS ⊆ S" "NS O S ⊆ S"
     "trans NS" 
     "refl NS" 
     "SN S"      
     "isOK (rel_impl.cpx ri cm cc) ⟶ deriv_bound_measure_class S cm cc" 
    by (auto simp: rel_impl_list)
  from ‹S O NS ⊆ S› ‹S ⊆ NS› have trans_S: "trans S" unfolding trans_def by auto
  show ?thesis
  proof (rule exI[of _ S], rule exI[of _ NS], rule exI[of _ Id], intro conjI *)
    show "mono_redtriple_order S NS Id" 
      by (unfold_locales; (intro trans_S *)?) (auto simp: trans_def refl_on_def)
  qed
qed

definition rel_impl_mono_ce_redpair :: "('f,'v)rel_impl ⇒ ('f,'v)rule list ⇒ ('f,'v)rule list ⇒ showsl check" where
  "rel_impl_mono_ce_redpair ri s ns = do {
      rel_impl.valid ri;
      rel_impl.standard ri;
      rel_impl.SN ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring strong normalization of relation''));
      rel_impl.subst_s ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring stability of strict relation''));
      rel_impl.ce_compat ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring ce-compatibility''));
      rel_impl.mono ri (funas_trs_list (s @ ns)) <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring monotonicity of strict relation''))      
    } <+? (λs. showsl_lit (STR ''problem with being a ce-compatible monotone reduction pair⏎'') ∘ s)" 

lemma rel_impl_mono_ce_redpair: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_mono_ce_redpair ri s ns)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_ns ri ns)" 
shows "∃ S NS NST. mono_ce_af_redtriple_order S NS NST full_af ∧ set s ⊆ S ∧ set ns ⊆ NS" 
proof -
  let ?U = "s @ ns" 
  from checks[unfolded rel_impl_mono_ce_redpair_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and std: "isOK(rel_impl.standard ri)" 
    and sn: "isOK (rel_impl.SN ri)" 
    and mono: "isOK (rel_impl.mono ri (funas_trs_list ?U))" 
    and subst: "isOK (rel_impl.subst_s ri)" 
    and ce: "isOK(rel_impl.ce_compat ri)" 
    by auto
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S NS NST
    where "rel_impl_prop ri ?U S NS NST" by presburger
  with orient subst mono sn ce std
  have *: "set s ⊆ S" "set ns ⊆ NS" 
     "S ⊆ NS" 
     "ctxt.closed NS" "ctxt.closed S" 
     "subst.closed NS" "subst.closed S"
     "S O NS ⊆ S" "NS O S ⊆ S"
     "trans NS" 
     "refl NS" 
     "SN S"      
     "ce_compatible NS" "ce_compatible S" 
    by (auto simp: rel_impl_list)
  from ‹S O NS ⊆ S› ‹S ⊆ NS› have trans_S: "trans S" unfolding trans_def by auto
  show ?thesis
  proof (rule exI[of _ S], rule exI[of _ NS], rule exI[of _ Id], intro conjI *)
    show "mono_ce_af_redtriple_order S NS Id full_af" 
      by (unfold_locales; (intro trans_S full_af *)?) (auto simp: trans_def refl_on_def)
  qed
qed


definition rel_impl_redpair :: "('f,'v)rel_impl ⇒ showsl check" where
  "rel_impl_redpair ri = do {
      rel_impl.valid ri;
      rel_impl.standard ri;
      rel_impl.SN ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring strong normalization of relation''));
      rel_impl.subst_s ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring stability of strict relation''))
    } <+? (λs. showsl_lit (STR ''problem with being a reduction pair⏎'') ∘ s)" 


lemma rel_impl_redpair: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_redpair ri)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_ns ri ns)"  
shows "∃ S NS. compat_redpair_order S NS ∧ set s ⊆ S ∧ set ns ⊆ NS 
   ∧ af_monotone (rel_impl.mono_af ri) S ∧ af_compatible (rel_impl.af ri) NS
   ∧ (isOK(rel_impl.cpx ri cm cc) ⟶ deriv_bound_measure_class S cm cc)
   ∧ (isOK(rel_impl.ce_compat ri) ⟶ ce_compatible NS)" 
proof -
  from checks[unfolded rel_impl_redpair_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and std: "isOK(rel_impl.standard ri)" 
    and sn: "isOK (rel_impl.SN ri)" 
    and subst: "isOK (rel_impl.subst_s ri)" 
    by auto
  let ?U = "s @ ns" 
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S NS NST
    where "rel_impl_prop ri ?U S NS NST" by presburger
  with orient subst sn std
  have *: "set s ⊆ S" "set ns ⊆ NS" 
     "S ⊆ NS" 
     "ctxt.closed NS" 
     "trans NS" 
     "refl NS" 
     "af_monotone (rel_impl.mono_af ri) S" 
     "af_compatible (rel_impl.af ri) NS" 
     "subst.closed NS" "subst.closed S"
     "S O NS ⊆ S" "NS O S ⊆ S"
     "SN S" 
     "isOK (rel_impl.cpx ri cm cc) ⟶ deriv_bound_measure_class S cm cc" 
     "isOK (rel_impl.ce_compat ri) ⟶ ce_compatible NS" 
    by (auto simp: rel_impl_list)
  from ‹S O NS ⊆ S› ‹S ⊆ NS› have trans_S: "trans S" unfolding trans_def by auto
  show ?thesis
  proof (rule exI[of _ S], rule exI[of _ NS], intro conjI *)
    show "compat_redpair_order S NS" 
      by (unfold_locales; (intro * trans_S)?) 
  qed
qed

definition rel_impl_redtriple :: "('f,'v)rel_impl ⇒ showsl check" where
  "rel_impl_redtriple ri = do {
      rel_impl.valid ri;
      rel_impl.standard ri;
      rel_impl.top_refl ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring reflexivity of top-non-strict relation''));
      rel_impl.SN ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring strong normalization of relation''));
      rel_impl.subst_s ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring stability of strict relation''))
    } <+? (λs. showsl_lit (STR ''problem with being a reduction triple⏎'') ∘ s)" 

lemma rel_impl_redtriple: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_redtriple ri)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_ns ri ns)" "isOK(rel_impl_nst ri nst)" 
shows "∃ S NS NST. af_redtriple_order S NS NST (rel_impl.af ri)
   ∧ set s ⊆ S ∧ set ns ⊆ NS ∧ set nst ⊆ NST   
   ∧ (isOK(rel_impl.ce_compat ri) ⟶ ce_compatible NS)" 
proof -
  from checks[unfolded rel_impl_redtriple_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and std: "isOK(rel_impl.standard ri)" 
    and sn: "isOK (rel_impl.SN ri)" 
    and subst: "isOK (rel_impl.subst_s ri)" 
    and refl: "isOK(rel_impl.top_refl ri)" 
    by auto
  let ?U = "s @ ns @ nst" 
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S NS NST
    where "rel_impl_prop ri ?U S NS NST" by presburger
  with orient subst sn std refl
  have *: "set s ⊆ S" "set ns ⊆ NS" "set nst ⊆ NST" 
     "S ⊆ NS" 
     "ctxt.closed NS" 
     "trans NS" "trans NST" 
     "refl NS" "refl NST" 
     "af_monotone (rel_impl.mono_af ri) S" 
     "af_compatible (rel_impl.af ri) NS" 
     "subst.closed NS" "subst.closed S" "subst.closed NST" 
     "S O NS ⊆ S" "NS O S ⊆ S" "NST O S ⊆ S" 
     "SN S" 
     "isOK (rel_impl.ce_compat ri) ⟶ ce_compatible NS" 
    by (simp_all add: rel_impl_list) (metis subrelI)+
  from ‹S O NS ⊆ S› ‹S ⊆ NS› have trans_S: "trans S" unfolding trans_def by auto
  show ?thesis
  proof (rule exI[of _ S], rule exI[of _ NS], rule exI[of _ NST], intro conjI *)
    show "af_redtriple_order S NS NST (rel_impl.af ri)" 
      by (unfold_locales; (intro * trans_S)?) 
  qed
qed

definition rel_impl_root_redtriple :: "('f,'v)rel_impl ⇒ showsl check" where
  "rel_impl_root_redtriple ri = do {
      rel_impl.valid ri;
      rel_impl.SN ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring strong normalization of relation''));
      rel_impl.subst_s ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring stability of strict relation''));
      rel_impl.top_mono ri <+? (λ e. e o showsl_lit (STR ''⏎problem in monotonicity from non-root to root''))
    } <+? (λs. showsl_lit (STR ''problem with being a root-reduction triple⏎'') ∘ s)" 

lemma rel_impl_root_redtriple: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_root_redtriple ri)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_ns ri ns)" "isOK(rel_impl_nst ri nst)" 
shows "∃ S NS NST. af_root_redtriple_order S NS NST (rel_impl.af ri) (rel_impl.top_af ri)
   ∧ set s ⊆ S ∧ set ns ⊆ NS ∧ set nst ⊆ NST   
   ∧ (isOK(rel_impl.ce_compat ri) ⟶ ce_compatible NS)" 
proof -
  from checks[unfolded rel_impl_root_redtriple_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and sn: "isOK (rel_impl.SN ri)" 
    and subst: "isOK (rel_impl.subst_s ri)" 
    and tm: "isOK (rel_impl.top_mono ri)" 
    by auto
  let ?U = "s @ ns @ nst" 
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S NS NST
    where "rel_impl_prop ri ?U S NS NST" by presburger
  with orient subst sn tm
  have *: "set s ⊆ S" "set ns ⊆ NS" "set nst ⊆ NST" 
     "ctxt.closed NS" 
     "trans S" "trans NS" "trans NST" 
     "refl NS"  
     "af_monotone (rel_impl.mono_af ri) S" 
     "af_compatible (rel_impl.af ri) NS"
     "af_compatible (rel_impl.top_af ri) NST"
     "subst.closed NS" "subst.closed S" "subst.closed NST" 
     "NST O S ⊆ S" 
     "SN S" 
     "isOK (rel_impl.ce_compat ri) ⟶ ce_compatible NS" 
     "top_mono NS NST" 
    by (simp_all add: rel_impl_list) (metis subrelI)+
  show ?thesis
  proof (rule exI[of _ S], rule exI[of _ NS], rule exI[of _ NST], intro conjI *)
    show "af_root_redtriple_order S NS NST (rel_impl.af ri) (rel_impl.top_af ri)" 
      by (unfold_locales; (intro *)?) 
  qed
qed

definition rel_impl_discr_pair :: "('f,'v)rel_impl ⇒ showsl check" where
  "rel_impl_discr_pair ri = do {
      rel_impl.valid ri;
      rel_impl.standard ri
    } <+? (λs. showsl_lit (STR ''problem with being a discrimination pair⏎'') ∘ s)" 


lemma rel_impl_discr_pair: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_discr_pair ri)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_ns ri ns)"  
shows "∃ S NS. discrimination_pair S NS ∧ set s ⊆ S ∧ set ns ⊆ NS" 
proof -
  let ?U = "s @ ns" 
  from checks[unfolded rel_impl_discr_pair_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and std: "isOK(rel_impl.standard ri)" 
    by auto
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S NS NST
    where "rel_impl_prop ri ?U S NS NST" by presburger
  with orient std
  have *: "set s ⊆ S" "set ns ⊆ NS" 
     "S ⊆ NS" 
     "ctxt.closed NS" 
     "trans NS" 
     "refl NS" 
     "irrefl S" 
     "subst.closed NS" 
     "S O NS ⊆ S" "NS O S ⊆ S"
    by (simp_all add: rel_impl_list) (metis subrelI)+
  from ‹S O NS ⊆ S› ‹S ⊆ NS› have trans_S: "trans S" unfolding trans_def by auto
  show ?thesis
  proof (rule exI[of _ S], rule exI[of _ NS], intro conjI *)
    show "discrimination_pair S NS" 
      by (unfold_locales; (intro * trans_S)?) (insert ‹irrefl S›, auto simp: irrefl_def)
  qed
qed

definition rel_impl_co_rewrite_pair :: "('f,'v)rel_impl ⇒ showsl check" where
  "rel_impl_co_rewrite_pair ri = do {
      rel_impl.valid ri;
      rel_impl.co_rewr ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring disjointness property''));
      rel_impl.subst_s ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring stability of strict relation''))
    } <+? (λs. showsl_lit (STR ''problem with being a co-rewrite pair⏎'') ∘ s)" 

lemma rel_impl_co_rewrite_pair: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_co_rewrite_pair ri)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_ns ri ns)"  
shows "∃ S NS. co_rewrite_pair S NS ∧ set s ⊆ S ∧ set ns ⊆ NS" 
proof -
  let ?U = "s @ ns" 
  from checks[unfolded rel_impl_co_rewrite_pair_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and subst: "isOK (rel_impl.subst_s ri)" 
    and co: "isOK (rel_impl.co_rewr ri)"  
    by auto
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S NS NST
    where "rel_impl_prop ri ?U S NS NST" by presburger
  with orient subst co have *: "set s ⊆ S" "set ns ⊆ NS" 
    "ctxt.closed NS" 
    "trans NS" 
    "refl NS" 
    "subst.closed NS" "subst.closed S" 
    "NS ∩ S¯ = {}" 
    by (simp_all add: rel_impl_list) (metis subrelI)+
  show ?thesis
  proof (rule exI[of _ S], rule exI[of _ NS], intro conjI *)
    show "co_rewrite_pair S NS" 
      by (unfold_locales; (intro *)?)
  qed
qed

definition rel_impl_co_discrimination_pair :: "('f,'v)rel_impl ⇒ showsl check" where
  "rel_impl_co_discrimination_pair ri = do {
      rel_impl.valid ri;
      rel_impl.co_rewr ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring disjointness property''))
    } <+? (λs. showsl_lit (STR ''problem with being a co-discrimination pair⏎'') ∘ s)" 

lemma rel_impl_co_discrimination_pair: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_co_discrimination_pair ri)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_ns ri ns)"  
shows "∃ S NS. co_discrimination_pair S NS ∧ set s ⊆ S ∧ set ns ⊆ NS" 
proof -
  let ?U = "s @ ns" 
  from checks[unfolded rel_impl_co_discrimination_pair_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and co: "isOK (rel_impl.co_rewr ri)"  
    by auto
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S NS NST
    where "rel_impl_prop ri ?U S NS NST" by presburger
  with orient subst co have *: "set s ⊆ S" "set ns ⊆ NS" 
    "ctxt.closed NS" 
    "trans NS" 
    "refl NS" 
    "subst.closed NS"  
    "NS ∩ S¯ = {}" 
    by (simp_all add: rel_impl_list) (metis subrelI)+
  show ?thesis
  proof (rule exI[of _ S], rule exI[of _ NS], intro conjI *)
    show "co_discrimination_pair S NS" 
      by (unfold_locales; (intro *)?)
  qed
qed

definition rel_impl_quasi_reduction_triple :: "('f,'v)rel_impl ⇒ showsl check" where
  "rel_impl_quasi_reduction_triple ri = do {
      rel_impl.valid ri;
      rel_impl.subst_s ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring stability of strict relation''));
      rel_impl.SN ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring strong normalization of strict relation''));
      rel_impl.top_mono ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring top-monotonicity of non-strict relations''));
      rel_impl.top_refl ri <+? (λ e. e o showsl_lit (STR ''⏎problem in ensuring top-reflexivity''))
    } <+? (λs. showsl_lit (STR ''problem with being a quasi-reduction triple⏎'') ∘ s)" 

lemma rel_impl_quasi_reduction_triple: assumes ri: "rel_impl ri" 
  and checks: "isOK(rel_impl_quasi_reduction_triple ri)"
  and orient: "isOK(rel_impl_s ri s)" "isOK(rel_impl_nst ri ns)" "isOK(rel_impl_ns ri h)"  
shows "∃ S NS H. 
    trans H ∧ refl H ∧ subst.closed H ∧ ctxt.closed H ∧ ― ‹H is a rewrite preorder›
    trans NS ∧ refl NS ∧ subst.closed NS ∧ ― ‹NS is a stable quasi-order›
    trans S ∧ irrefl S ∧ subst.closed S ∧ SN S ∧ ― ‹S is a stable well-founded order›
    NS O S ⊆ S ∧ S O NS ⊆ S ∧ ― ‹S and NS forms an order-pair›
    top_mono H NS ∧ ― ‹top-mono/harmony property›
    set s ⊆ S ∧ set ns ⊆ NS ∧ set h ⊆ H" 
proof -
  let ?U = "s @ ns @ h" 
  from checks[unfolded rel_impl_quasi_reduction_triple_def, simplified]
  have valid: "isOK (rel_impl.valid ri)" 
    and subst: "isOK (rel_impl.subst_s ri)" 
    and tm: "isOK (rel_impl.top_mono ri)"
    and tr: "isOK (rel_impl.top_refl ri)"
    and sn: "isOK(rel_impl.SN ri)" 
    by auto
  from ri[unfolded rel_impl_def, rule_format, OF valid, of ?U] obtain S H NS
    where "rel_impl_prop ri ?U S H NS" by presburger
  with orient subst tm tr sn have *: "set s ⊆ S" "set ns ⊆ NS" "set h ⊆ H" 
    "trans H" "refl H" "subst.closed H" "ctxt.closed H"
    "trans NS" "refl NS" "subst.closed NS"
    "trans S" "irrefl S" "subst.closed S" "SN S"
    "NS O S ⊆ S" "S O NS ⊆ S"
    "top_mono H NS"
      by (simp_all add: rel_impl_list) (metis subrelI)+
  show ?thesis
    by (rule exI[of _ S], rule exI[of _ NS], rule exI[of _ H], intro conjI *)
qed

lemma co_rewrite_irrefl: assumes "irrefl S" and "NS O S ⊆ S" 
  shows "NS ∩ S¯ = {}" 
proof (rule ccontr)
  assume "¬ ?thesis" 
  then obtain a b where "(a,b) ∈ NS" and "(b,a) ∈ S" by auto
  hence "(a,a) ∈ S" using assms(2) by auto
  with assms(1) show False unfolding irrefl_def by auto
qed

definition no_complexity where
  "no_complexity ≡ (λ _ _. False)"

definition no_complexity_check where
  "no_complexity_check ≡ (λ _ _. error (showsl (STR ''complexity analysis unsupported'')) :: showsl check)"

lemma isOK_no_complexity: "isOK(no_complexity_check cm cc) = False" 
  by (auto simp: no_complexity_check_def)

lemma no_complexity_check[simp]: "(λ cm cc. isOK(no_complexity_check cm cc)) = no_complexity"
  unfolding no_complexity_check_def no_complexity_def by auto

interpretation cpx_term_rel S no_complexity 
  by (unfold_locales) (auto simp: no_complexity_def)

definition faulty_rel_impl :: "'f itself ⇒ 'v itself ⇒ showsl ⇒ showsl ⇒ ('f, 'v)rel_impl"
  where
    "faulty_rel_impl _ _ err desc = ⦇
      rel_impl.valid = error err,
      standard = succeed,
      desc = desc,
      s = (λ _. succeed),
      ns = (λ _. succeed),
      nst = (λ _. succeed),
      af = full_af,
      top_af = full_af,
      SN = succeed,
      subst_s = succeed,
      ce_compat = succeed,
      co_rewr = succeed,
      top_mono = succeed,
      top_refl = succeed,
      mono_af = empty_af,
      mono = (λ _ . succeed),
      not_wst = None,
      not_sst = None,
      cpx = no_complexity_check
    ⦈"

lemma faulty_rel_impl[simp]: "¬ isOK (rel_impl.valid (faulty_rel_impl a b c d))"
  unfolding faulty_rel_impl_def by simp

typedef ('f,'v,'rp) rel_impl_type = "{ ri :: 'rp ⇒ ('f,'v)rel_impl.
  ∀ params. rel_impl (ri params) }" 
  by (intro exI[of _ "λ _. faulty_rel_impl TYPE('f) TYPE('v) undefined undefined"], 
      auto simp: faulty_rel_impl_def rel_impl_def)

setup_lifting type_definition_rel_impl_type

lift_definition rel_impl_of :: "('f,'v,'rp) rel_impl_type ⇒ 'rp ⇒ ('f,'v)rel_impl" is id .

lemma rel_impl_of: "rel_impl (rel_impl_of ri params)" 
  by (transfer, auto)

(* Precedences for natural numbers *)
definition prc_nat :: "('f × nat ⇒ nat) ⇒ ('f × nat ⇒ 'f × nat ⇒ bool × bool)"
  where "prc_nat pr ≡ λ f g. let pf = pr f; pg = pr g in (pg < pf, pg ≤ pf)"

definition prl_nat :: "('f × nat ⇒ nat) ⇒ 'f × nat ⇒ bool"
  where "prl_nat pr ≡ λ f. pr f = 0"

abbreviation pr_nat where "pr_nat pr ≡ (prc_nat pr, prl_nat pr)"

(* Precedences via natural numbers *)

lemma SN_pr_nat: "SN {(f,g). (pr :: 'f × nat ⇒ nat) g < pr f}"
  by (rule HOL.subst[of _ _ SN, OF _ SN_inv_image[OF SN_nat_gt, of "pr"]],
  auto simp: inv_image_def)

interpretation precedence_nat: precedence "prc_nat pr" "prl_nat pr" 
  for "pr" :: "'f × nat ⇒ nat" 
  by (unfold_locales, unfold prc_nat_def prl_nat_def Let_def, insert SN_pr_nat[of "pr"], auto)

― ‹show function symbol together with arity›
fun showsl_funa :: "('f::showl × nat) ⇒ showsl"
  where
    "showsl_funa (f, n) = showsl f ∘ showsl_lit (STR ''/'') ∘ showsl n"

end