Theory First_Order_Clause.Nonground_Term_Order

theory Nonground_Term_Order
  imports
    Nonground_Context
    Ground_Term_Order 
    Grounded_Order 
begin

locale base_grounded_order =
  order: grounded_restricted_total_strict_order +
  order: grounded_restricted_wellfounded_strict_order +
  order: ground_subst_stable_grounded_order +
  grounding

locale nonground_term_order =
  "term": nonground_term where Var = Var +
  order: restricted_wellfounded_total_strict_order where
  less = less⇩t and restriction = "range term.from_ground" +
  order: ground_subst_stability where R = less⇩t and comp_subst = "(⊙)" and subst = "(⋅t)" and
  vars = term.vars and id_subst = Var and to_ground = term.to_ground and
  from_ground = "term.from_ground"
for less⇩t and Var :: "'v ⇒ 't"
begin

interpretation term_order_notation .

sublocale base_grounded_order where
  subst = "(⋅t)" and vars = term.vars and id_subst = Var and comp_subst = "(⊙)" and
  to_ground = term.to_ground and from_ground = "term.from_ground" and less = "(≺⇩t)"
  by unfold_locales

(* TODO: Find way to not have this twice *)
notation order.less⇩G (infix "≺⇩t⇩G" 50)
notation order.less_eq⇩G (infix "≼⇩t⇩G" 50)

sublocale restriction: ground_term_order where 
  less⇩t = "(≺⇩t⇩G)"
  by unfold_locales

end

locale ground_context_compatible_order =
  nonground_term_with_context +
  restricted_total_strict_order where restriction = "range term.from_ground" +
assumes ground_context_compatibility:
  "⋀c t⇩1 t⇩2.
      term.is_ground t⇩1 ⟹
      term.is_ground t⇩2 ⟹
      context.is_ground c ⟹
      t⇩1 ≺ t⇩2 ⟹
      c⟨t⇩1⟩ ≺ c⟨t⇩2⟩"
begin

sublocale context_compatible_restricted_order where
  restriction = "range term.from_ground" and context_restriction = "range context.from_ground" and
  restricted = term.is_ground and restricted_context = context.is_ground
  using ground_context_compatibility
  by unfold_locales
    (auto simp: term.is_ground_iff_range_from_ground context.is_ground_iff_range_from_ground)

end

locale ground_subterm_property =
  nonground_term_with_context +
  fixes R
  assumes ground_subterm_property:
    "⋀t⇩G c⇩G. term.is_ground t⇩G ⟹ context.is_ground c⇩G ⟹ c⇩G ≠ □ ⟹ R t⇩G c⇩G⟨t⇩G⟩"

locale context_compatible_nonground_term_order =
  nonground_term_with_context where
  Var = "Var :: 'v ⇒ 't" and
  from_ground_context_map = "from_ground_context_map :: ('t⇩G ⇒ 't) ⇒ 'c⇩G ⇒ 'c" +
  nonground_term_order +
  order: ground_context_compatible_order where less = less⇩t +
  order: ground_subterm_property where R = less⇩t
begin

interpretation term_order_notation .

sublocale order: base_subst_update_stable_grounded_order where 
  subst = "(⋅t)" and vars = term.vars and id_subst = Var and comp_subst = "(⊙)" and
  to_ground = term.to_ground and from_ground = "term.from_ground" and less = "(≺⇩t)"
proof unfold_locales
  fix update x γ t
  assume
    update_is_ground: "term.is_ground update" and
    update_less: "update ≺⇩t γ x" and
    term_grounding: "term.is_ground (t ⋅t γ)" and
    x_in_t: "x ∈ term.vars t"

  from x_in_t term_grounding show "t ⋅t γ(x := update) ≺⇩t t ⋅t γ"
  proof (induction "occurences t x - 1" arbitrary: t)
    case 0

    then have "occurences t x = 1"
      by (simp add: vars_occurences)

    then obtain c where t: "t = c⟨Var x⟩" and "x ∉ context.vars c"
      using one_occurence_obtain_context 
      by blast

    then have c_update: "c⟨Var x⟩ ⋅t γ(x := update) = (c ⋅t⇩c γ)⟨update⟩"
      by auto

    show ?case
      using 0(3) update_less update_is_ground
      unfolding t c_update
      by auto
  next
    case (Suc n)

    obtain c where t: "t = c⟨Var x⟩"
      using Suc.prems(1) context.context_Var
      by blast

    let ?t' = "c⟨update⟩"

    have "?t' ⋅t γ(x := update) ≺⇩t ?t' ⋅t γ"
    proof (rule Suc.hyps(1))

      show "n = occurences c⟨update⟩ x - 1"
        using Suc.hyps(2) occurences t update_is_ground 
        by auto
    next

      have "occurences c⟨update⟩ x = Suc n"
        using Suc.hyps(2)
        unfolding t occurences[OF update_is_ground]
        by auto

      then show "x ∈ term.vars c⟨update⟩"
        using vars_occurences
        by presburger
    next

      show "term.is_ground (c⟨update⟩ ⋅t γ)"
        using Suc.prems(2) update_is_ground
        unfolding t
        by fastforce
    qed

    moreover have "c⟨update⟩ ⋅t γ(x := update) = c⟨Var x⟩ ⋅t γ(x := update)"
      using update_is_ground
      by auto

    moreover have less: "c⟨update⟩ ⋅t γ ≺⇩t c⟨Var x⟩ ⋅t γ"
      using Suc.prems(2) update_is_ground update_less
      unfolding t
      by auto

    ultimately show ?case
      unfolding t
      by auto
  qed
qed

sublocale restriction: context_compatible_ground_term_order where 
  less⇩t = "(≺⇩t⇩G)" and compose_context = compose_ground_context and
  apply_context = apply_ground_context and hole = ground_hole
proof unfold_locales
  fix c t t'
  assume "t ≺⇩t⇩G t'"

  then show "c⟨t⟩⇩G ≺⇩t⇩G c⟨t'⟩⇩G"
    using
      order.ground_context_compatibility[OF
        term.ground_is_ground term.ground_is_ground context.ground_is_ground]
    unfolding order.less⇩G_def
    by simp
next
  fix t :: "'t⇩G" and c :: "'c⇩G"
  assume "c ≠ □⇩G"

  then show "t ≺⇩t⇩G c⟨t⟩⇩G"
    using order.ground_subterm_property[OF term.ground_is_ground context.ground_is_ground]
    unfolding order.less⇩G_def
    by simp
qed

end

end