Theory Nonground_Term_Order

theory Nonground_Term_Order
  imports
    Nonground_Term
    Nonground_Context
    Ground_Order
begin

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
  Fun = Fun 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 base_grounded_order =
  order: base_subst_update_stable_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 =
  nonground_term_with_context +
  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" +
  order: ground_context_compatible_order where less = less⇩t  +
  order: ground_subterm_property where R = less⇩t
for less⇩t :: "('f, 'v) Term.term ⇒ ('f, 'v) Term.term ⇒ bool"
begin

interpretation term_order_notation.

sublocale base_grounded_order where
  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" and less = "(≺⇩t)"
proof unfold_locales
  fix update x γ and t :: "('f, 'v) term"
  assume
    update_is_ground: "term.is_ground update" and
    update_less: "update ≺⇩t γ x" and
    term_grounding: "term.is_ground (t ⋅t γ)" and
    var: "x ∈ term.vars t"

  from term_grounding var
  show "t ⋅t γ(x := update) ≺⇩t t ⋅t γ"
  proof(induction t)
    case Var
    then show ?case
      using update_is_ground update_less
      by simp
  next
    case (Fun f subs)

    then have "∀sub ∈ set subs. sub ⋅t γ(x := update) ≼⇩t sub ⋅t γ"
      by (metis eval_with_fresh_var is_ground_iff reflclp_iff term.set_intros(4))

    moreover then have "∃sub ∈ set subs. sub ⋅t γ(x := update) ≺⇩t sub ⋅t γ"
      using Fun update_less
      by (metis (full_types) fun_upd_same term.distinct(1) term.sel(4) term.set_cases(2)
          order.dual_order.strict_iff_order term_subst_eq_rev)

    ultimately show ?case
      using Fun(2, 3)
    proof(induction "filter (λsub. sub ⋅t γ(x := update) ≺⇩t sub ⋅t γ) subs" arbitrary: subs)
      case Nil
      then show ?case
        unfolding empty_filter_conv
        by blast
    next
      case first: (Cons s ss)

      have groundings [simp]: "term.is_ground (s ⋅t γ(x := update))" "term.is_ground (s ⋅t γ)"
        using term.ground_subst_update update_is_ground
        by (metis (lifting) filter_eq_ConsD first.hyps(2) first.prems(3) in_set_conv_decomp
            is_ground_iff term.set_intros(4))+

      show ?case
      proof(cases ss)
        case Nil
        then obtain ss1 ss2 where subs: "subs = ss1 @ s # ss2"
          using filter_eq_ConsD[OF first.hyps(2)[symmetric]]
          by blast

        have ss1: "∀s ∈ set ss1. s ⋅t γ(x := update) = s ⋅t γ"
          using first.hyps(2) first.prems(1)
          unfolding Nil subs
          by (smt (verit, del_insts) Un_iff append_Cons_eq_iff filter_empty_conv filter_eq_ConsD
              set_append order.antisym_conv2)

        have ss2: "∀s ∈ set ss2. s ⋅t γ(x := update) = s ⋅t γ"
          using first.hyps(2) first.prems(1)
          unfolding Nil subs
          by (smt (verit, ccfv_SIG) Un_iff append_Cons_eq_iff filter_empty_conv filter_eq_ConsD
              list.set_intros(2) set_append order.antisym_conv2)

        let ?c = "More f ss1 □ ss2 ⋅t⇩c γ"

        have "context.is_ground ?c"
          using subs first(5)
          by auto

        moreover have "s ⋅t γ(x := update) ≺⇩t s ⋅t γ"
          using first.hyps(2)
          by (meson Cons_eq_filterD)

        ultimately have "?c⟨s ⋅t γ(x := update)⟩ ≺⇩t ?c⟨s ⋅t γ⟩"
          using order.ground_context_compatibility groundings
          by blast

        moreover have "Fun f subs ⋅t γ(x := update) = ?c⟨s ⋅t γ(x := update)⟩"
          unfolding subs
          using ss1 ss2
          by simp

        moreover have "Fun f subs ⋅t γ = ?c⟨s ⋅t γ⟩"
          unfolding subs
          by auto

        ultimately show ?thesis
          by argo
      next
        case (Cons t' ts')

        from first(2)
        obtain ss1 ss2 where
          subs: "subs = ss1 @ s # ss2" and
          ss1: "∀s∈set ss1. ¬ s ⋅t γ(x := update) ≺⇩t s ⋅t γ" and
          less: "s ⋅t γ(x := update) ≺⇩t s ⋅t γ" and
          ss: "ss = filter (λterm. term ⋅t γ(x := update)≺⇩t term ⋅t γ) ss2"
          using Cons_eq_filter_iff[of s ss "(λs. s ⋅t γ(x := update) ≺⇩t s ⋅t γ)"]
          by blast

        let ?subs' = "ss1 @ (s ⋅t γ(x := update)) # ss2"

        have [simp]: "s ⋅t γ(x := update) ⋅t γ = s ⋅t γ(x := update)"
          using first.prems(3) update_is_ground
          unfolding subs
          by (simp add: is_ground_iff)

        have [simp]: "s ⋅t γ(x := update) ⋅t γ(x := update) = s ⋅t γ(x := update)"
          using first.prems(3) update_is_ground
          unfolding subs
          by (simp add: is_ground_iff)

        have ss: "ss = filter (λsub. sub ⋅t γ(x := update) ≺⇩t sub ⋅t γ) ?subs'"
          using ss1 ss
          by auto

        moreover have "∀sub ∈ set ?subs'. sub ⋅t γ(x := update) ≼⇩t sub ⋅t γ"
          using first.prems(1)
          unfolding subs
          by simp

        moreover have ex_less: "∃sub ∈ set ?subs'. sub ⋅t γ(x := update) ≺⇩t sub ⋅t γ"
          using ss Cons neq_Nil_conv
          by force

        moreover have subs'_grounding: "term.is_ground (Fun f ?subs' ⋅t γ)"
          using first.prems(3)
          unfolding subs
          by simp

        moreover have "x ∈ term.vars (Fun f ?subs')"
          by (metis ex_less eval_with_fresh_var term.set_intros(4) order.less_irrefl)

        ultimately have less_subs': "Fun f ?subs' ⋅t γ(x := update) ≺⇩t Fun f ?subs' ⋅t γ"
          using first.hyps(1) first.prems(3)
          by blast

        have context_grounding: "context.is_ground (More f ss1 □ ss2 ⋅t⇩c γ)"
          using subs'_grounding
          by auto

        have "Fun f (ss1 @ s ⋅t γ(x := update) # ss2) ⋅t γ ≺⇩t Fun f subs ⋅t γ"
          unfolding subs
          using order.ground_context_compatibility[OF _ _ context_grounding less]
          by simp

        with less_subs' show ?thesis
          unfolding subs
          by simp
      qed
    qed
  qed
qed

(* 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 "(≺⇩t⇩G)"
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 :: "'f gterm" and c :: "'f ground_context"
  assume "c ≠ □"
  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