Theory Context_Compatible_Order

theory Context_Compatible_Order
  imports
    Ground_Context
    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 +
  fixes R Fun
  assumes
    context_compatible [simp]:
      "⋀c t⇩1 t⇩2.
        restricted t⇩1 ⟹
        restricted t⇩2 ⟹
        restricted_context c ⟹
        R (Fun⟨c;t⇩1⟩) (Fun⟨c;t⇩2⟩) ⟷ R t⇩1 t⇩2"

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 (Fun⟨c;t⇩1⟩) (Fun⟨c;t⇩2⟩) ⟷ R t⇩1 t⇩2"
  by simp

end

locale context_compatible_restricted_order =
  restricted_total_strict_order +
  restriction_restricted +
  fixes Fun
  assumes less_context_compatible:
    "⋀c t⇩1 t⇩2.
      restricted t⇩1 ⟹
      restricted t⇩2 ⟹
      restricted_context c ⟹
      t⇩1 ≺ t⇩2 ⟹
      Fun⟨c;t⇩1⟩ ≺ Fun⟨c;t⇩2⟩"
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 ⟹ Fun⟨c;t⟩ ≺ Fun⟨c';t⟩"
    "t ≼ t'"
  shows "Fun⟨c;t⟩ ≺ Fun⟨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 ⟹ Fun⟨c;t⟩ ≼ Fun⟨c';t⟩"
    "t ≺ t'"
  shows "Fun⟨c;t⟩ ≺ Fun⟨c';t'⟩"
  using assms context_compatible dual_order.strict_trans1
  by meson

end

locale context_compatible_order =
  total_strict_order +
  fixes Fun
  assumes less_context_compatible: "t⇩1 ≺ t⇩2 ⟹ Fun⟨c;t⇩1⟩ ≺ Fun⟨c;t⇩2⟩"
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 "(≺)"
  by unfold_locales

sublocale less_eq: context_compatibility "(≼)"
  by unfold_locales

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

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

end

end