Theory First_Order_Clause.Context_Compatible_Order

theory Context_Compatible_Order
  imports
    Context_Notation
    Restricted_Order
begin

locale restriction_restricted =
  fixes restriction context_restriction restricted restricted_context
  assumes
    restricted:
      "⋀t. t ∈ restriction ⟷ restricted t"
      "⋀c. c ∈ context_restriction ⟷ restricted_context c"

locale restricted_context_compatibility =
  restriction_restricted +
  apply_context_notation +
  fixes R :: "'t ⇒ 't ⇒ bool"
  assumes
    context_compatible [simp]:
      "⋀(c :: 'c)  t1 t2.
        restricted t1 ⟹
        restricted t2 ⟹
        restricted_context c ⟹
        R c⟨t1⟩ c⟨t2⟩ ⟷ R t1 t2"

locale context_compatibility = restricted_context_compatibility where
  restriction = UNIV and context_restriction = UNIV and restricted = "λ_. True" and
  restricted_context = "λ_. True"
begin

lemma context_compatibility [simp]: "R c⟨t1⟩ c⟨t2⟩ = R t1 t2"
  by simp

end

locale context_compatible_restricted_order =
  restricted_total_strict_order +
  restriction_restricted +
  apply_context_notation +
  assumes less_context_compatible:
    "⋀c t1 t2. restricted t1 ⟹ restricted t2 ⟹ restricted_context c ⟹ t1 ≺ t2 ⟹ c⟨t1⟩ ≺ c⟨t2⟩"
begin

sublocale restricted_context_compatibility where R = "(≺)"
  using less_context_compatible restricted
  by unfold_locales (metis dual_order.asym totalp totalp_onD)

sublocale less_eq: restricted_context_compatibility where R = "(≼)"
  using context_compatible restricted_not_le dual_order.order_iff_strict restricted
  by unfold_locales metis

lemma context_less_term_lesseq:
  assumes
    "restricted t"
    "restricted t'"
    "restricted_context c"
    "restricted_context c'"
    "⋀t. restricted t ⟹  c⟨t⟩ ≺ c'⟨t⟩"
    "t ≼ t'"
  shows "c⟨t⟩ ≺ c'⟨t'⟩"
  using assms context_compatible dual_order.strict_trans
  by blast

lemma context_lesseq_term_less:
  assumes
    "restricted t"
    "restricted t'"
    "restricted_context c"
    "restricted_context c'"
    "⋀t. restricted t ⟹ c⟨t⟩ ≼ c'⟨t⟩"
    "t ≺ t'"
  shows "c⟨t⟩ ≺ c'⟨t'⟩"
  using assms context_compatible dual_order.strict_trans1
  by meson

end

locale context_compatible_order =
  total_strict_order +
  apply_context_notation +
  assumes less_context_compatible: "t1 ≺ t2 ⟹ c⟨t1⟩ ≺ c⟨t2⟩"
begin

sublocale restricted: context_compatible_restricted_order where
  restriction = UNIV and context_restriction = UNIV and restricted = "λ_. True" and
  restricted_context = "λ_. True"
  using less_context_compatible
  by unfold_locales simp_all

sublocale context_compatibility where R = "(≺)"
  by unfold_locales

sublocale less_eq: context_compatibility where R = "(≼)"
  by unfold_locales

lemma context_less_term_lesseq:
  assumes
   "⋀t. c⟨t⟩ ≺ c'⟨t⟩"
    "t ≼ t'"
  shows "c⟨t⟩ ≺ c'⟨t'⟩"
  using assms restricted.context_less_term_lesseq
  by blast

lemma context_lesseq_term_less:
  assumes
    "⋀t. c⟨t⟩ ≼ c'⟨t⟩"
    "t ≺ t'"
  shows "c⟨t⟩ ≺ c'⟨t'⟩"
  using assms restricted.context_lesseq_term_less
  by blast

end

end