Theory LS_Prelude

(*
Author:  Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at> (2015-2017)
Author:  Franziska Rapp <franziska.rapp@uibk.ac.at> (2015-2017)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Layer systems definitions and main results›

theory LS_Prelude
  imports LS_Extras
begin

text ‹
  This formalization is based on the layer framework by Felgenhauer et al.\ @{cite FMZvO15}.
  In this file we formalize the layer system definitions and the main results as locales.
  This way, the applications of layer systems are decoupled from the proofs of the main theorems.
›

subsection ‹Definitions›

text ‹Layer systems @{cite ‹Definition 3.3› FMZvO15}.›

locale layer_system_sig =
  fixes ℱ :: "'f sig" and 𝔏 :: "('f, 'v) mctxt set"
begin

definition 𝒯 where "𝒯 = { t :: ('f,'v) term. funas_term t ⊆ ℱ }"
definition 𝒞 where "𝒞 = { C :: ('f,'v) mctxt. funas_mctxt C ⊆ ℱ }"

text ‹Tops and max-top @{cite ‹Definition 3.1› FMZvO15}.›

definition topsC :: "('f, 'v) mctxt ⇒ ('f, 'v) mctxt set" where
  "topsC C = { L ∈ 𝔏. L ≤ C }"

abbreviation tops where
  "tops t ≡ topsC (mctxt_of_term t)"

definition max_topC :: "('f, 'v) mctxt ⇒ ('f, 'v) mctxt" where
  "max_topC C = (THE M. M ∈ topsC C ∧ (∀L ∈ topsC C. L ≤ M))"

abbreviation max_top where
  "max_top t ≡ max_topC (mctxt_of_term t)"

abbreviation aliensC where
  "aliensC C ≡ unfill_holes_mctxt (max_topC C) C"

abbreviation aliens where
  "aliens t ≡ unfill_holes (max_top t) t"

end (* layer_system_sig *)

locale layer_system = layer_system_sig ℱ 𝔏 for ℱ :: "('f × nat) set" and 𝔏 :: "('f, 'v :: infinite) mctxt set" +
  assumes 𝔏_sig: "𝔏 ⊆ 𝒞"
  and L⇩1: "funas_term t ⊆ ℱ ⟹ ∃L ∈ 𝔏. L ≠ MHole ∧ L ≤ mctxt_of_term t"
  and L⇩2: "p ∈ poss_mctxt C ⟹ mreplace_at C p (MVar x) ∈ 𝔏 ⟷ mreplace_at C p MHole ∈ 𝔏"
  and L⇩3: "L ∈ 𝔏 ⟹ N ∈ 𝔏 ⟹ p ∈ funposs_mctxt L ⟹ (subm_at L p, N) ∈ comp_mctxt ⟹
    mreplace_at L p (subm_at L p ⊔ N) ∈ 𝔏"

text ‹Weakly layered TRSs @{cite ‹Definition 3.3› FMZvO15}.›

locale weakly_layered = layer_system ℱ 𝔏 for ℱ :: "('f × nat) set" and 𝔏 :: "('f, 'v :: infinite) mctxt set" +
  fixes ℛ :: "('f, 'v) trs"
  assumes trs: "wf_trs ℛ" and ℛ_sig: "funas_trs ℛ ⊆ ℱ"
  and W: "s ∈ 𝒯 ⟹ t ∈ 𝒯 ⟹ p ∈ funposs_mctxt (max_top s) ⟹ (s, t) ∈ rstep_r_p_s' ℛ r p σ ⟹
    ∃D τ. D ∈ 𝔏 ∧ (mctxt_term_conv (max_top s), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ r p τ"

text ‹Layered TRSs @{cite ‹Definition 3.3› FMZvO15}.›

locale layered = layer_system ℱ 𝔏 for ℱ :: "('f × nat) set" and 𝔏 :: "('f, 'v :: infinite) mctxt set" +
  fixes ℛ :: "('f, 'v) trs"
  assumes trs: "wf_trs ℛ" and ℛ_sig: "funas_trs ℛ ⊆ ℱ"
  and C⇩1: "s ∈ 𝒯 ⟹ t ∈ 𝒯 ⟹ p ∈ funposs_mctxt (max_top s) ⟹ (s, t) ∈ rstep_r_p_s' ℛ r p σ ⟹
    ∃τ. (mctxt_term_conv (max_top s), mctxt_term_conv (max_top t)) ∈ rstep_r_p_s' ℛ r p τ ∨
        (mctxt_term_conv (max_top s), mctxt_term_conv MHole) ∈ rstep_r_p_s' ℛ r p τ"
  and C⇩2: "L ∈ 𝔏 ⟹ N ∈ 𝔏 ⟹ L ≤ N ⟹ p ∈ hole_poss L ⟹ mreplace_at L p (subm_at N p) ∈ 𝔏"

text ‹
  Layered TRSs are also weakly layered, i.e., @{locale layered} is a sublocale of
  @{locale weakly_layered}. However, (W) is omitted from the Isabelle definition of layered TRSs,
  making this statement non-trivial, because we have to show that (C1) implies (W). We do this in
  @{file "LS_Basics.thy"}.
›

subsection ‹Claims›

text ‹Confluence of weakly layered, left-linear TRSs @{cite ‹Theorem 4.1› FMZvO15}.›

locale weakly_layered_cr_ll = weakly_layered +
  assumes CR_ll: "left_linear_trs ℛ ⟹
    CR_on (rstep ℛ) { t. mctxt_of_term t ∈ 𝔏 } ⟹ CR_on (rstep ℛ) 𝒯"

text ‹
  Proving @{cite ‹Theorem 4.1› FMZvO15} amounts to showing that @{locale weakly_layered_cr_ll}
  is a sublocale of @{locale weakly_layered}. This will be done in @{file "LS_Left_Linear.thy"}.
›

text ‹
  Confluence of weakly layered, bounded duplicating TRSs @{cite ‹Theorem 4.3› FMZvO15}.
›

locale weakly_layered_cr_bd = weakly_layered +
  assumes CR_bd: "bounded_duplicating ℛ ⟹
    CR_on (rstep ℛ) { t. mctxt_of_term t ∈ 𝔏 } ⟹ CR_on (rstep ℛ) 𝒯"
begin

text ‹Confluence of weakly layered, non-duplicating TRSs @{cite ‹Lemma 4.4› FMZvO15}.›

lemmas CR_nd = CR_bd[OF non_duplicating_imp_bounded_duplicating]

end (* weakly_layered_bd *)

text ‹
  We have to show that @{locale weakly_layered_cr_bd} is a sublocale of @{locale weakly_layered}.
  This is still open (but see @{file "LS_Bounded_Duplicating.thy"}).
›

text ‹Confluence of layered TRSs @{cite ‹Theorem 4.4› FMZvO15}.›

locale layered_cr = layered +
  assumes CR: "CR_on (rstep ℛ) { t. mctxt_of_term t ∈ 𝔏 } ⟹ CR_on (rstep ℛ) 𝒯"

text ‹
  We show that @{locale layered_cr} is a sublocale of @{locale layered} in @{file "LS_General.thy"}.
›

end (* LS_Prelude *)