Theory Encompassment

theory Encompassment
imports Litsim_Trs
(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2014, 2015, 2017)
License: LGPL (see file COPYING.LESSER)
*)

section ‹The Encompassment Relation›

theory Encompassment
  imports Litsim_Trs
begin

(*TODO: move*)
(*from Decreasing_Diagrams_II_Aux in AFP*)
lemmas converse_inward = rtrancl_converse[symmetric] converse_Un converse_UNION converse_relcomp
  converse_converse converse_Id

(*TODO: move*)
lemma qc_SN_relto_iff:
  assumes "r O s ⊆ s O (s ∪ r)*"
  shows "SN (r* O s O r*) = SN s"
proof -
  from converse_mono [THEN iffD2 , OF assms]
  have *: "s¯ O r¯ ⊆ (s¯ ∪ r¯)* O s¯" unfolding converse_inward .
  have "(r* O s O r*)¯ = (r¯)* O s¯ O (r¯)*"
    by (simp only: converse_relcomp O_assoc rtrancl_converse)
  with qc_wf_relto_iff [OF *]
  show ?thesis by (simp add: SN_iff_wf)
qed

inductive encompeq :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "⊴⋅" 50)
  where
    [intro]: "t = C⟨s ⋅ σ⟩ ⟹ s ⊴⋅ t"

lemma encompeq_termE [elim]:
  assumes "s ⊴⋅ t"
  obtains C σ where "t = C⟨s ⋅ σ⟩"
  using assms by (cases)

lemma encompeq_refl:
  "t ⊴⋅ t"
  by (rule encompeq.intros [of t  t Var]) simp

lemma encompeq_trans:
  assumes "s ⊴⋅ t"
    and "t ⊴⋅ u"
  shows "s ⊴⋅ u"
proof -
  obtain C D σ τ
    where [simp]: "t = C⟨s ⋅ σ⟩" "u = D⟨t ⋅ τ⟩" using assms by fastforce
  show ?thesis
    by (rule encompeq.intros [of _ "D ∘c (C ⋅c τ)" _ "σ ∘s τ"]) simp
qed

definition encomp (infix "⊲⋅" 50)
  where
    "t ⊲⋅ s ⟷ t ⊴⋅ s ∧ ¬ s ⊴⋅ t"

abbreviation (input) revencompeq  (infix "⋅⊵" 50) where
  "x ⋅⊵ y ≡ y ⊴⋅ x"

abbreviation (input) revencomp (infix "⋅⊳" 50) where
  "x ⋅⊳ y ≡ y ⊲⋅ x"

abbreviation encompeq_set ("{⊴⋅}")
  where
    "{⊴⋅} ≡ {(x, y). x ⊴⋅ y}"

abbreviation encomp_set ("{⊲⋅}")
  where
    "{⊲⋅} ≡ {(x, y). x ⊲⋅ y}"

abbreviation revencompeq_set ("{⋅⊵}")
  where
    "{⋅⊵} ≡ {(x, y). y ⊴⋅ x}"

abbreviation revencomp_set ("{⋅⊳}")
  where
    "{⋅⊳} ≡ {(x, y). y ⊲⋅ x}"

interpretation encomp_order: preorder "op ⊴⋅" "op ⊲⋅"
  by standard (auto simp: encomp_def encompeq_refl elim: encompeq_trans)

text ‹Encompassment is the composition of subsumption and the subterm relation.›
lemma encompeq_eq_subteq_instance:
  "s ⊴⋅ t ⟷ (op ≤⋅ OO op ⊴) s t"
  by (force simp: OO_def subsumeseq_term_iff)

lemma subsumeseq_size:
  "s ≤⋅ t ⟹ size s ≤ size t"
  by (cases s t rule: subsumeseq_term.cases) (auto simp: size_subst)

lemma subsumeseq_imp_encompeq:
  "s ≤⋅ t ⟹ s ⊴⋅ t"
  by (cases s t rule: subsumeseq_term.cases) (auto intro: encompeq.intros [of _ ])

lemma encompeq_size:
  "s ⊴⋅ t ⟹ size s ≤ size t"
  by (force simp: encompeq_eq_subteq_instance dest: subsumeseq_size supteq_size)

lemma encompeq_subsumeseq_cases:
  "s ⊴⋅ t ⟷ s ≤⋅ t ∨ (op ≤⋅ OO op ⊲) s t"
  by (auto simp: encompeq_eq_subteq_instance)

lemma revencompeq_set_cases:
  "{⋅⊵} = {⋅≥} ∪ ({⊳} O {⋅≥})"
  unfolding encompeq_subsumeseq_cases by blast

lemma encomp_subsumes_cases:
  "s ⊲⋅ t ⟷ s <⋅ t ∨ (op ≤⋅ OO op ⊲) s t"
  by (auto simp: encomp_def term_subsumable.subsumes_def encompeq_subsumeseq_cases OO_def)
    (auto dest!: supt_size subsumeseq_size)

lemma wf_subsumeseq_O_subt:
  "wf ({≤⋅} O {(x, y). x ⊲ y})"
proof -
  have "⋀x y. (x, y) ∈ {≤⋅} O {(x, y). x ⊲ y} ⟹ size x < size y"
    by (auto simp: OO_def dest!: subsumeseq_size supt_size)
  then have "{≤⋅} O {(x, y). x ⊲ y} ⊆ inv_image {(x, y). x < y} size"
    by (auto simp: inv_image_def)
  moreover have "wf (inv_image {(x, y). x < y} size)" by (rule wf_inv_image [OF wf_less])
  ultimately show ?thesis by (metis wf_subset)
qed

lemma litsim_encompeq_iff:
  "s ≐ t ⟷ s ⊴⋅ t ∧ t ⊴⋅ s"
proof
  assume "s ≐ t"
  then show "s ⊴⋅ t ∧ t ⊴⋅ s"
    by (auto simp: term_subsumable.litsim_def dest: subsumeseq_imp_encompeq)
next
  presume "s ⊴⋅ t" and "t ⊴⋅ s"
  then have "s ≤⋅ t" and "t ≤⋅ s"
    by (auto simp: encompeq_subsumeseq_cases dest!: supt_size subsumeseq_size)
  then show "s ≐ t" by (auto simp: term_subsumable.litsim_def)
qed auto

lemma encompeq_litsim_encomp_iff:
  "s ⊴⋅ t ⟷ s ≐ t ∨ s ⊲⋅ t"
  by (auto simp: litsim_encompeq_iff encomp_def)

lemmas encompeq_cases [consumes 1] = encompeq_litsim_encomp_iff [THEN iffD1]

lemma encomp_supt:
  assumes "s ⋅> t" and "t ⊳ u"
  shows "∃t ⊲ s. t ⋅≥ u"
proof -
  from assms [unfolded term_subsumable.subsumes_def subsumeseq_term_iff] obtain σ
    where "s = t ⋅ σ" and "¬ (∃σ. t = s ⋅ σ)" by blast
  moreover with ‹t ⊳ u› have "t ⋅ σ ⊳ u ⋅ σ"
    by (metis instance_no_supt_imp_no_supt)
  ultimately have "s ⊳ u ⋅ σ" and "u ⋅ σ ⋅≥ u"
    by (auto simp: term_subsumable.subsumes_def)
  then show ?thesis by blast
qed

lemma wf_encomp:
  "wf ({⊲⋅} :: ('f, 'v) term rel)"
proof -
  have "{⊳} O {⋅≥} ∪ {⋅>} = ({⋅⊳} :: ('f, 'v) term rel)" by (auto simp: encomp_subsumes_cases)
  moreover
  have "SN ({⊳} O {⋅≥} ∪ ({⋅>} :: ('f, 'v) term rel))"
  proof (rule quasi_commute_imp_SN)
    have [simp]: "{(s, u). ∃t. s ≤⋅ t ∧ u ⊳ t} = {(s, u). ∃t ⊲ u. s ≤⋅ t}" by auto
    show "SN ({⊳} O {⋅≥})"
      using wf_subsumeseq_O_subt
      by (auto simp: SN_iff_wf converse_unfold OO_def relcomp_def)
    show "SN ({⋅>} :: ('f, 'v) term rel)"
      using wf_subsumes by (auto simp: SN_iff_wf converse_unfold)
    show "quasi_commute ({⊳} O {⋅≥}) ({⋅>} :: ('f, 'v) term rel)"
    proof (unfold quasi_commute_def, intro subrelI)
      fix s t :: "('f, 'v) term"
      assume "(s, t) ∈ {⋅>} O {⊳} O {⋅≥}"
      moreover have "{⋅>} O {⊳} ⊆ {⊳} O {⋅≥}"
        by (auto simp: relcomp_def OO_def dest: encomp_supt)
      ultimately have "(s, t) ∈ {⊳} O {⋅≥} O {⋅≥}" by auto
      then have "(s, t) ∈ {⊳} O {⋅≥}"
        by (auto simp: relcomp_def OO_def dest: subsumeseq_term_trans)
      then show "(s, t) ∈ ({⊳} O {⋅≥}) O ({⊳} O {⋅≥} ∪ {⋅>})*" by auto
    qed
  qed
  ultimately
  show ?thesis by (auto simp: SN_iff_wf converse_unfold)
qed

lemmas encomp_induct = wfP_induct [OF wf_encomp [to_pred]]

lemma SN_encomp:
  "SN {⋅⊳}"
  using wf_encomp by (auto simp: SN_iff_wf converse_unfold)

lemma qc_SN_relto_encompeq:
  "SN r ⟹ {⋅⊵} O r ⊆ r O (r ∪ {⋅⊵})* ⟹ SN (relto r {⋅⊵})"
  by (intro qc_SN_relto_iff [THEN iffD2])

context
  fixes r :: "('f, 'v) term rel"
  assumes r_ctxt: "(s, t) ∈ r ⟹ (C⟨s⟩, C⟨t⟩) ∈ r"
    and r_subst: "(s, t) ∈ r ⟹ (s ⋅ σ, t ⋅ σ) ∈ r"
begin

lemma commutes_rewrel_encomp:
  "{⋅⊵} O r ⊆ r O {⋅⊵}"
proof -
  { fix s t u
    assume "s ⋅⊵ t" and "(t, u) ∈ r"
    then obtain C and σ :: "('f, 'v) subst" where "s = C⟨t ⋅ σ⟩"
      and "(C⟨t ⋅ σ⟩, C⟨u ⋅ σ⟩) ∈ r" by (auto simp: encomp_def r_ctxt r_subst)
    then have "(s, u) ∈ r O {⋅⊵}" by auto }
  then show ?thesis by blast
qed

context
  assumes SN_rewrel: "SN r"
begin

lemma SN_rewrel_relto_encomp:
  "SN (relto r {⋅⊵})"
  using SN_rewrel and commutes_rewrel_encomp
  by (intro qc_SN_relto_encompeq) auto

lemma SN_encomp_Un_rewrel:
  "SN ({⋅⊳} ∪ r)"
proof -
  have "{⋅⊳}* O r O {⋅⊳}* ⊆ {⋅⊵}* O r O {⋅⊵}*"
    by (intro relcomp_mono rtrancl_mono) (auto simp: encomp_def)
  with SN_rewrel_relto_encomp have "SN ({⋅⊳}* O r O {⋅⊳}*)" by (rule SN_subset)
  from SN_relto_split [of _ "{}" _ "{}", simplified, OF this SN_encomp]
  show ?thesis by (simp add: ac_simps)
qed

end

end

lemma revencompeq_set_eqvt [simp]:
  "π ∙ {⋅⊵} = {⋅⊵}"
  by (simp add: revencompeq_set_cases trs_pt.union_eqvt trs_pt.relcomp_eqvt)

end