Theory First_Order_Clause.Grounded_Order

theory Grounded_Order
  imports
    Restricted_Order
    Abstract_Substitution.Functional_Substitution_Lifting
begin

section ‹Orders with ground restrictions›

locale grounded_order =
  strict_order where less = less +
  grounding where vars = vars
for
  less :: "'expr ⇒ 'expr ⇒ bool"  (infix ‹≺› 50) (* TODO *) and
  vars :: "'expr ⇒ 'var set"
begin

sublocale strict_order_restriction where lift = "from_ground"
  by unfold_locales (rule inj_from_ground)

abbreviation "less⇩G ≡ less⇩r"
lemmas less⇩G_def = less⇩r_def
notation less⇩G (infix "≺⇩G" 50)

abbreviation "less_eq⇩G ≡ less_eq⇩r"
notation less_eq⇩G (infix "≼⇩G" 50)

lemma to_ground_less⇩r [simp]:
  assumes "is_ground e" and "is_ground e'"
  shows "to_ground e ≺⇩G to_ground e' ⟷ e ≺ e'"
  by (simp add: assms less⇩r_def)

lemma to_ground_less_eq⇩r [simp]:
  assumes "is_ground e" and "is_ground e'"
  shows "to_ground e ≼⇩G to_ground e' ⟷ e ≼ e'"
  using assms obtain_grounding
  by fastforce

lemma less_eq⇩r_from_ground [simp]:
  "e⇩G ≼⇩G e⇩G' ⟷ from_ground e⇩G ≼ from_ground e⇩G'"
  unfolding R⇩r_def
  by (simp add: inj_eq inj_lift)

end

locale grounded_restricted_total_strict_order =
  order: restricted_total_strict_order where restriction = "range from_ground" +
  grounded_order
begin

sublocale total_strict_order_restriction where lift = "from_ground"
  by unfold_locales

lemma not_less_eq [simp]:
  assumes "is_ground expr" and "is_ground expr'"
  shows "¬ order.less_eq expr' expr ⟷ expr ≺ expr'"
  using assms order.totalp order.less_le_not_le
  unfolding totalp_on_def is_ground_iff_range_from_ground
  by blast

end

locale grounded_restricted_wellfounded_strict_order =
  restricted_wellfounded_strict_order where restriction = "range from_ground" +
  grounded_order
begin

sublocale wellfounded_strict_order_restriction where lift = "from_ground"
  by unfold_locales

end

subsection ‹Ground substitution stability›

locale ground_subst_stability = grounding +
  fixes R
  assumes
    ground_subst_stability:
      "⋀expr⇩1 expr⇩2 γ.
        is_ground (expr⇩1 ⋅ γ) ⟹
        is_ground (expr⇩2 ⋅ γ) ⟹
        R expr⇩1 expr⇩2 ⟹
        R (expr⇩1 ⋅ γ) (expr⇩2 ⋅ γ)"

locale ground_subst_stable_grounded_order =
  grounded_order +
  ground_subst_stability where R = "(≺)"
begin

sublocale less_eq: ground_subst_stability where R = "(≼)"
  using ground_subst_stability
  by unfold_locales blast

lemma ground_less_not_less_eq:
  assumes
    grounding: "is_ground (expr⇩1 ⋅ γ)" "is_ground (expr⇩2 ⋅ γ)" and
    less: "expr⇩1 ⋅ γ ≺ expr⇩2 ⋅ γ"
  shows
    "¬ expr⇩2 ≼ expr⇩1"
  using less ground_subst_stability[OF grounding(2, 1)] dual_order.asym
  by blast

end

subsection ‹Substitution update stability›

locale subst_update_stability =
  based_functional_substitution +
  fixes base_R R
  assumes
    subst_update_stability:
      "⋀update x γ expr.
        base.is_ground update ⟹
        base_R update (γ x) ⟹
        is_ground (expr ⋅ γ) ⟹
        x ∈ vars expr ⟹
        R (expr ⋅ γ(x := update)) (expr ⋅ γ)"

locale base_subst_update_stability =
  base_functional_substitution +
  subst_update_stability where base_R = R and base_subst = subst and base_vars = vars

locale subst_update_stable_grounded_order =
  grounded_order + subst_update_stability where R = less and base_R = base_less
for base_less
begin

sublocale less_eq: subst_update_stability
  where base_R = "base_less⇧=⇧=" and R = "less⇧=⇧="
  using subst_update_stability
  by unfold_locales auto

end

locale base_subst_update_stable_grounded_order =
  base_subst_update_stability where R = less +
  subst_update_stable_grounded_order where
  base_less = less and base_subst = subst and base_vars = vars

end