Theory Level_Confluence_Impl

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2015-2017)
Author:  Thomas Sternagel <thomas.sternagel@uibk.ac.at> (2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Level_Confluence_Impl
imports
  Infeasibility
  Level_Confluence
begin

text ‹
  Operations required to support a check function for almost-orthogonality (modulo infeasibility)
›
locale almost_orthogonal_ops =
  fixes xvar yvar :: "'v::{show, infinite} ⇒ 'v"
    and check_infeasible ::
      "('f::show, 'v) crules ⇒ ('f, 'v) rules ⇒ ('f, 'v) rules ⇒ shows check"
begin

definition
  check_overlap :: "('f, 'v) crules ⇒ ('f, 'v) crule ⇒ ('f, 'v) crule ⇒ pos ⇒ shows check"
where
  "check_overlap R ρ⇩1 ρ⇩2 p =
    (case mgu_var_disjoint_generic xvar yvar (clhs ρ⇩1 |_ p) (clhs ρ⇩2) of
      None ⇒ succeed
    | Some (σ⇩1, σ⇩2) ⇒
      choice [
        check (p = ε ∧ crhs ρ⇩1 ⋅ σ⇩1 = crhs ρ⇩2 ⋅ σ⇩2) (shows ''is not a trivial root-overlap''),
        check (p = ε ∧ match_crule ρ⇩1 ρ⇩2 ≠ None ∧ match_crule ρ⇩2 ρ⇩1 ≠ None)
          (shows ''is not a root-overlap of variants of the same rule''),
        check_infeasible R (subst_list σ⇩1 (snd ρ⇩1)) (subst_list σ⇩2 (snd ρ⇩2))
          <+? (λe. shows ''could not be shown to be infeasible'' ∘ shows_nl ∘ e)]
      <+? shows_sep id shows_nl)
    <+? (λe. shows ''the '' ∘ shows_coverlap ρ⇩1 ρ⇩2 p ∘ shows_nl ∘ e)"

definition
  "check_ao R = do {
    check_left_linear_trs (map fst R);
    check_allm (λρ⇩1. let l⇩1 = clhs ρ⇩1 in check_allm (λρ⇩2. check_allm (λp.
      check_overlap R ρ⇩1 ρ⇩2 p) (funposs_list l⇩1)) R) R
  }"

end

lemmas [code] =
  almost_orthogonal_ops.check_overlap_def almost_orthogonal_ops.check_ao_def

locale almost_orthogonal_spec = almost_orthogonal_ops +
  assumes infeasible: "isOK (check_infeasible R cs⇩1 cs⇩2) ⟹
    (∀m n. comm ((cstep_n (set R) m)⇧*) ((cstep_n (set R) n)⇧*) ⟶
    ¬ (∃σ. conds_n_sat (set R) m cs⇩1 σ ∧ conds_n_sat (set R) n cs⇩2 σ))"
    and ren: "inj xvar" "inj yvar" "range xvar ∩ range yvar = {}"
begin

lemma isOK_check_ao [simp]:
  assumes "isOK (check_ao R)"
  shows "almost_orthogonal (set R)"
proof (unfold almost_orthogonal_def, intro conjI allI impI)
  show "left_linear_trs (Ru (set R))"
    using assms by (simp add: check_ao_def Ru_def)
next
  fix ρ⇩1' ρ⇩2' p
  assume "overlap (set R) ρ⇩1' ρ⇩2' p"
  then obtain π⇩1 and π⇩2 and μ
    where rules': "π⇩1 ∙ ρ⇩1' ∈ set R" "π⇩2 ∙ ρ⇩2' ∈ set R"
    and "vars_crule ρ⇩1' ∩ vars_crule ρ⇩2' = {}"
    and p': "p ∈ funposs (clhs ρ⇩1')"
    and mgu': "mgu (clhs ρ⇩1' |_ p) (clhs ρ⇩2') = Some μ"
    by (auto simp: overlap_def)
  define ρ⇩1 ρ⇩2 where "ρ⇩1 ≡ π⇩1 ∙ ρ⇩1'" and "ρ⇩2 ≡ π⇩2 ∙ ρ⇩2'"
  have p: "p ∈ funposs (clhs ρ⇩1)"
    and "ρ⇩1 ∈ set R" and "ρ⇩2 ∈ set R"
    using p' and rules' apply (auto simp: ρ⇩1_def ρ⇩2_def eqvt)
    by (metis crule_pt.fst_eqvt funposs_perm_simp rule_pt.fst_eqvt)
  with assms have *: "isOK (check_overlap R ρ⇩1 ρ⇩2 p)" by (auto simp: check_ao_def)

  let ?thesis = "let μ = the (mgu (clhs ρ⇩1' |_ p) (clhs ρ⇩2')) in
     p = ε ∧ crhs ρ⇩1' ⋅ μ = crhs ρ⇩2' ⋅ μ ∨
     p = ε ∧ (∃p. p ∙ ρ⇩1' = ρ⇩2') ∨
     (∀m n. comm ((cstep_n (set R) m)⇧*) ((cstep_n (set R) n)⇧*) ⟶
       ¬ (∃σ. conds_n_sat (set R) m (subst_list μ (snd ρ⇩1')) σ ∧
              conds_n_sat (set R) n (subst_list μ (snd ρ⇩2')) σ))"

  have "(clhs ρ⇩1' |_ p) ⋅ μ = clhs ρ⇩2' ⋅ μ" using mgu' [THEN mgu_sound] by (auto simp: is_imgu_def)
  then have "(clhs ρ⇩1' |_ p) ⋅ (μ ∘ Rep_perm (-π⇩1) ∘ Rep_perm π⇩1) =
    clhs ρ⇩2' ⋅ (μ ∘ Rep_perm (-π⇩2) ∘ Rep_perm π⇩2)"
    by (simp add: o_assoc [symmetric] Rep_perm_add [symmetric] Rep_perm_0)
  then have "clhs ρ⇩1 |_ p ⋅ (μ ∘ Rep_perm (-π⇩1)) = clhs ρ⇩2 ⋅ (μ ∘ Rep_perm (-π⇩2))"
    using p [THEN funposs_imp_poss]
    by (auto simp: ρ⇩1_def ρ⇩2_def permute_term_subst_apply_term [symmetric] eqvt)
  from mgu_var_disjoint_generic_complete [OF ren this] obtain μ⇩1 μ⇩2 δ
    where "mgu_var_disjoint_generic xvar yvar (clhs ρ⇩1 |_ p) (clhs ρ⇩2) = Some (μ⇩1, μ⇩2)"
    and **: "μ ∘ Rep_perm (- π⇩1) = μ⇩1 ∘⇩s δ" "μ ∘ Rep_perm (- π⇩2) = μ⇩2 ∘⇩s δ" by blast
  with * have "p = ε ∧ crhs ρ⇩1 ⋅ μ⇩1 = crhs ρ⇩2 ⋅ μ⇩2 ∨
    p = ε ∧ match_crule ρ⇩1 ρ⇩2 ≠ None ∧ match_crule ρ⇩2 ρ⇩1 ≠ None ∨
    isOK (check_infeasible R (subst_list μ⇩1 (snd ρ⇩1)) (subst_list μ⇩2 (snd ρ⇩2)))"
    by (auto simp: check_overlap_def)
  moreover
  { assume [simp]: "p = ε" and "crhs ρ⇩1 ⋅ μ⇩1 = crhs ρ⇩2 ⋅ μ⇩2"
    then have "crhs ρ⇩1 ⋅ (μ⇩1 ∘⇩s δ) = crhs ρ⇩2 ⋅ (μ⇩2 ∘⇩s δ)" by simp
    then have "crhs ρ⇩1' ⋅ μ = crhs ρ⇩2' ⋅ μ"
      unfolding ** [symmetric]
      by (simp add: ρ⇩1_def ρ⇩2_def permute_term_subst_apply_term [symmetric] eqvt)
    with mgu' have ?thesis by (auto) }
  moreover
  { assume "p = ε" and "match_crule ρ⇩1 ρ⇩2 ≠ None" and "match_crule ρ⇩2 ρ⇩1 ≠ None"
    with match_crule_imp_variants [of ρ⇩2 ρ⇩1] obtain π where "π ∙ ρ⇩1 = ρ⇩2" by blast
    then have "(-π⇩2 + π + π⇩1) ∙ ρ⇩1' = ρ⇩2'" by (simp add: ρ⇩1_def ρ⇩2_def)
    with ‹p = ε› have ?thesis unfolding Let_def by blast }
  moreover
  { assume *: "isOK (check_infeasible R (subst_list μ⇩1 (snd ρ⇩1)) (subst_list μ⇩2 (snd ρ⇩2)))"
    { fix m n assume comm: "comm ((cstep_n (set R) m)⇧*) ((cstep_n (set R) n)⇧*)"
      have "¬ (∃σ. conds_n_sat (set R) m (subst_list μ (snd ρ⇩1')) σ ∧
        conds_n_sat (set R) n (subst_list μ (snd ρ⇩2')) σ)"
      proof (intro notI, elim exE conjE)
        fix σ
        assume "conds_n_sat (set R) m (subst_list μ (snd ρ⇩1')) σ"
          and "conds_n_sat (set R) n (subst_list μ (snd ρ⇩2')) σ"
        then have "conds_n_sat (set R) m (subst_list (μ ∘ Rep_perm (-π⇩1)) (snd ρ⇩1)) σ"
          and "conds_n_sat (set R) n (subst_list (μ ∘ Rep_perm (-π⇩2)) (snd ρ⇩2)) σ"
          by (auto simp: ρ⇩1_def ρ⇩2_def subst_list_subst_compose subst_list_Rep_perm map_idI eqvt [symmetric])
        then have "∃σ. conds_n_sat (set R) m (subst_list μ⇩1 (snd ρ⇩1)) σ ∧
          conds_n_sat (set R) n (subst_list μ⇩2 (snd ρ⇩2)) σ"
          by (auto simp add: ** subst_list_subst_compose conds_n_sat_subst_list)
        with infeasible [OF *, THEN spec, THEN spec, THEN mp, OF comm] show False by blast
      qed }
    then have ?thesis using mgu' by auto }
  ultimately show ?thesis by blast
qed

end

global_interpretation wo_infeasibility: almost_orthogonal_spec x_var y_var
  "λR cs⇩1 cs⇩2. error (shows_string ''infeasibility check not supported'')"
  defines
    check_almost_orthogonal = wo_infeasibility.check_ao
by (unfold_locales; auto simp: inj_on_def)

definition check_level_confluence :: "('f::{key,show}, string) crules ⇒ shows check"
where
  "check_level_confluence R = do {
    check_varcond_no_Var_lhs (map fst R);
    check_type3 R;
    check_extended_properly_oriented R;
    check_right_stable R;
    check_almost_orthogonal R
  }"

lemma check_level_confluence [simp]:
  assumes "isOK (check_level_confluence R)"
  shows "level_confluent (set R)"
using assms by (force intro: level_confluence simp: check_level_confluence_def)

global_interpretation mod_infeasibility: almost_orthogonal_spec x_var y_var
  "check_infeasible css" for css
  defines
    check_almost_orthogonal_modulo_infeasibility = mod_infeasibility.check_ao
by (unfold_locales; force dest: infeasible_sufficient check_infeasible simp: inj_on_def)

definition
  check_level_confluence_modulo_infeasibility ::
    "_ ⇒ ('f::{key,show}, string) crules ⇒ shows check"
where
  "check_level_confluence_modulo_infeasibility css R = do {
    check_varcond_no_Var_lhs (map fst R);
    check_type3 R;
    check_extended_properly_oriented R;
    check_right_stable R;
    check_almost_orthogonal_modulo_infeasibility css R
  }"

lemma check_level_confluence_modulo_infeasibility [simp]:
  assumes "isOK (check_level_confluence_modulo_infeasibility css R)"
  shows "level_confluent (set R)"
using assms
by (intro level_confluence)
   (auto simp: check_level_confluence_modulo_infeasibility_def)

datatype ('f, 'v) ao_infeasibility_proof =
  AO_Infeasibility_Proof "('f, 'v) infeasibility_proof"
| AO_Lhss_Equal "('f, 'v) term" "('f, 'v) term" "('f, 'v) term" "('f, 'v) nonjoinability_proof"

fun check_ao_infeasible'
where
  "check_ao_infeasible' R cs⇩1 cs⇩2 (AO_Infeasibility_Proof p) = check_infeasible' R (cs⇩1 @ cs⇩2) p"
| "check_ao_infeasible' R cs⇩1 cs⇩2 (AO_Lhss_Equal s t u p) = do {
    check ((s, t) ∈ set cs⇩1)
      (shows_eq (s, t) ∘ shows '' is not an equation in '' ∘ shows_conditions cs⇩1);
    check ((s, u) ∈ set cs⇩2)
      (shows_eq (s, u) ∘ shows '' is not an equation in '' ∘ shows_conditions cs⇩2);
    check_nonjoinable (map fst R) t u p
  }"

lemma check_ao_infeasible':
  assumes "isOK (check_ao_infeasible' R cs⇩1 cs⇩2 p)"
  shows "(∀m n. comm ((cstep_n (set R) m)⇧*) ((cstep_n (set R) n)⇧*) ⟶
    ¬ (∃σ. conds_n_sat (set R) m cs⇩1 σ ∧ conds_n_sat (set R) n cs⇩2 σ))"
proof (intro allI impI)
  let ?R = "set R"
  fix m n assume comm: "comm ((cstep_n ?R m)⇧*) ((cstep_n ?R n)⇧*)"
  show "¬ (∃σ. conds_n_sat ?R m cs⇩1 σ ∧ conds_n_sat ?R n cs⇩2 σ)"
  proof (cases p)
    case (AO_Infeasibility_Proof q)
    then show ?thesis
      using assms and comm by (auto dest: check_infeasible' [THEN infeasible_sufficient])
  next
    case (AO_Lhss_Equal s t u q)
    with assms have *: "(s, t) ∈ set cs⇩1" "(s, u) ∈ set cs⇩2"
      and "isOK (check_nonjoinable (map fst R) t u q)" by auto
    then have **: "¬ (∃σ. (t ⋅ σ, u ⋅ σ) ∈ (rstep (Ru ?R))⇧↓)"
      by (auto simp: Ru_def dest: check_nonjoinable)
    { fix σ assume "conds_n_sat ?R m cs⇩1 σ" and "conds_n_sat ?R n cs⇩2 σ"
      with * and comm obtain v where "(t ⋅ σ, v) ∈ (cstep_n ?R n)⇧*"
        and "(u ⋅ σ, v) ∈ (cstep_n ?R m)⇧*" by (blast dest: conds_n_satD elim: commE)
      with ** have False
        using rtrancl_mono [OF cstep_imp_Ru_step] by (blast dest: csteps_n_imp_csteps) }
    then show ?thesis by auto
  qed
qed

definition
  check_ao_infeasible ::
    "(('f::{key, show}, 'v::{key, show}) rules × ('f, 'v) rules × ('f, 'v) ao_infeasibility_proof) list ⇒
      ('f, 'v) crules ⇒ ('f, 'v) rules ⇒ ('f, 'v) rules ⇒ shows check"
where
  "check_ao_infeasible css R cs⇩1' cs⇩2' = check_exm (λ(cs⇩1, cs⇩2, p). do {
    let cs' = cs⇩1' @ cs⇩2';
    let cs = cs⇩1 @ cs⇩2;
    check (length cs⇩1 = length cs⇩1' ∧ length cs⇩2 = length cs⇩2') (shows ''lengths differ'');
    check (match_rules cs cs' ≠ None ∧ match_rules cs' cs ≠ None) id;
    check_ao_infeasible' R cs⇩1 cs⇩2 p
  }) css (shows_sep id shows_nl)"

lemma check_ao_infeasible:
  fixes R :: "('f::{key, show}, 'v::{key, show, infinite}) crules"
  assumes "isOK (check_ao_infeasible css R cs⇩1 cs⇩2)"
  shows "(∀m n. comm ((cstep_n (set R) m)⇧*) ((cstep_n (set R) n)⇧*) ⟶
    ¬ (∃σ. conds_n_sat (set R) m cs⇩1 σ ∧ conds_n_sat (set R) n cs⇩2 σ))"
    (is "?P cs⇩1 cs⇩2")
proof -
  let ?cs = "cs⇩1 @ cs⇩2"
  obtain π :: "'v perm" and cs⇩1' and cs⇩2' and p where "(cs⇩1', cs⇩2', p) ∈ set css"
    and cs': "cs⇩1' = π ∙ cs⇩1" "cs⇩2' = π ∙ cs⇩2" and ok: "isOK (check_ao_infeasible' R cs⇩1' cs⇩2' p)"
    using assms and match_rules_imp_variants [of _ ?cs]
    by (auto simp: check_ao_infeasible_def Ru_def)
       (metis (no_types, hide_lams) List.append_eq_append_conv length_map)
  moreover then have "?P cs⇩1' cs⇩2'" by (auto dest: check_ao_infeasible')
  ultimately show ?thesis by (metis conds_n_sat_perm_shift rules_pt.permute_minus_cancel(2))
qed

global_interpretation mod_infeasibility': almost_orthogonal_spec x_var y_var
  "check_ao_infeasible css" for css
  defines
    check_almost_orthogonal_modulo_infeasibility' = mod_infeasibility'.check_ao
by (unfold_locales; force dest: infeasible_sufficient check_ao_infeasible simp: inj_on_def)

definition
  check_level_confluence_modulo_infeasibility' ::
    "_ ⇒ ('f::{key,show}, string) crules ⇒ shows check"
where
  "check_level_confluence_modulo_infeasibility' css R = do {
    check_varcond_no_Var_lhs (map fst R);
    check_type3 R;
    check_extended_properly_oriented R;
    check_right_stable R;
    check_almost_orthogonal_modulo_infeasibility' css R
  }"

lemma check_level_confluence_modulo_infeasibility' [simp]:
  assumes "isOK (check_level_confluence_modulo_infeasibility' css R)"
  shows "level_confluent (set R)"
using assms
by (intro level_confluence)
   (auto simp: check_level_confluence_modulo_infeasibility'_def)

end