Theory First_Order_Clause.IsaFoR_Nonground_Context

theory IsaFoR_Nonground_Context
  imports 
    IsaFoR_Nonground_Term
    IsaFoR_Ground_Context
    Nonground_Context
    Context_Functor
begin

type_synonym ('f, 'v) "context" = "('f, 'v) ctxt"

abbreviation occurences where
  "occurences t x ≡ count (vars_term_ms t) x"

interpretation "context": term_based_lifting where
  sub_subst = "(⋅)" and sub_vars = term.vars and sub_to_ground = term.to_ground and 
  comp_subst = "(∘s)" and Var = Var and sub_from_ground = term.from_ground and
  term_vars = term.vars and term_subst = "(⋅)" and term_to_ground = term.to_ground and
  term_from_ground = term.from_ground and to_ground_map = map_args_actxt and
  ground_map = map_args_actxt and from_ground_map = map_args_actxt and map = map_args_actxt and
  to_set = set2_actxt and to_set_ground = set2_actxt
  by unfold_locales

no_notation subst_apply_actxt (infixl ‹⋅c› 67)
notation context.subst (infixl ‹⋅c› 67)

interpretation "context": nonground_context where
  comp_subst = "(∘s)" and Var = Var and term_subst = "(⋅)" and term_vars = term.vars and 
  compose_context = "(∘c)" and term_from_ground = term.from_ground and
  term_to_ground = term.to_ground and map_context = map_args_actxt and
  to_ground_context_map = map_args_actxt and from_ground_context_map = map_args_actxt and
  context_to_set = set2_actxt and hole = □ and apply_context = ctxt_apply_term and 
  ground_hole = □ and compose_ground_context = "(∘c)" and ground_context_map = map_args_actxt and
  ground_context_to_set = set2_actxt and apply_ground_context = apply_ground_context
proof unfold_locales
  fix c and t :: "('f, 'v) term"

  show "term.to_ground c⟨t⟩ = (context.to_ground c)⟨term.to_ground t⟩G"
    by (induction c) (auto simp: context.to_ground_def)
next
  fix cG and tG :: "'f gterm"

  show "term.from_ground cG⟨tG⟩G = (context.from_ground cG)⟨term.from_ground tG⟩"
    by (induction cG) (auto simp: context.from_ground_def)
next
  fix c and t :: "('f, 'v) term"

  show "term.is_ground c⟨t⟩ ⟷ context.is_ground c ∧ term.is_ground t"
    by (induction c) (auto simp: context.vars_def)
next
  fix f :: "('f, 'v) term ⇒ ('f, 'v) term" and c c' :: "('f, 'v) context"

  show "map_args_actxt f (c ∘c c') = map_args_actxt f c ∘c map_args_actxt f c'"
    by (induction c) auto
next
  fix c c' :: "'f ground_context"

  show "context.from_ground (c ∘c c') = context.from_ground c ∘c context.from_ground c'"
    by (induction c) (auto simp: context.from_ground_def)
next
  fix c and t :: "('f, 'v) term"

  show "term.vars c⟨t⟩ = context.vars c ∪ term.vars t"
    unfolding  context.vars_def
    by (induction c) auto
next
  fix c t and σ :: "('f, 'v) subst"
  show "c⟨t⟩ ⋅ σ = (c ⋅c σ)⟨t ⋅ σ⟩"
    by (metis context.subst_def subst_apply_term_ctxt_apply_distrib)
next
  fix x and t :: "('f, 'v) term"

  show "x ∈ term.vars t ⟷ (∃c. t = c⟨Var x⟩)"
    by (metis Un_iff supteq_Var supteq_ctxtE term.set_intros(3) vars_term_ctxt_apply)
next
  fix cG tG and σ :: "('f, 'v) subst" and t :: "('f, 'v) term"
  assume t_σ: "t ⋅ σ = cG⟨tG⟩"

  {
    assume "∄c t'. t = c⟨t'⟩ ∧ t' ⋅ σ = tG ∧ c ⋅c σ = cG"
    with t_σ have "∃c c' x. t = c⟨Var x⟩ ∧ (c ⋅c σ) ∘c c' = cG"
    proof(induction t arbitrary: cG)
      case (Var x)

      show ?case
      proof (intro exI conjI)

        show "Var x = □⟨Var x⟩"
          by simp
      next

        show "(□ ⋅c σ) ∘c cG = cG"
          by (simp add: context.subst_def)
      qed
    next
      case (Fun f ts)

      have "cG ≠ □"
        using Fun.prems(1, 2)
        by (metis actxt.simps(8) context.subst_def intp_actxt.simps(1))

      then obtain tsG1 cG' tsG2 where
        cG: "cG = More f tsG1 cG' tsG2"
        using Fun.prems
        by (cases cG) auto

      have "map (λt. t ⋅ σ) ts = tsG1 @ cG'⟨tG⟩ # tsG2"
        using Fun.prems(1) 
        unfolding cG
        by simp

      moreover then obtain ts1 t ts2 where
        ts: "ts = ts1 @ t # ts2" and
        ts1_γ: "map (λt. t ⋅ σ) ts1 = tsG1" and
        ts2_γ: "map (λt. t ⋅ σ) ts2 = tsG2"
        by (smt append_eq_map_conv map_eq_Cons_D)

      ultimately have t_γ: "t ⋅ σ = cG'⟨tG⟩"
        by simp

      obtain x c1 cG'' where "t = c1⟨Var x⟩" and "cG' = (c1 ⋅c σ) ∘c cG''"
      proof -

        have "t ∈ set ts"
          by (simp add: ts)

        moreover have "∄c t'. t = c⟨t'⟩ ∧ t' ⋅ σ = tG ∧ c ⋅c σ = cG'"
        proof(rule notI, elim exE conjE)
          fix c t'
          assume "t = c⟨t'⟩" "t' ⋅ σ = tG" "c ⋅c σ = cG'"

          moreover then have
            "Fun f ts = (More f ts1 c ts2)⟨t'⟩"
            "(More f ts1 c ts2) ⋅c σ = cG"
            unfolding cG ts context.subst_def
            using ts1_γ ts2_γ
            by auto

          ultimately show False
            using Fun.prems(2) 
            by blast
        qed

        ultimately show ?thesis
          using Fun(1) t_γ that
          by blast
      qed

      moreover then have
        "Fun f ts = (More f ts1 c1 ts2)⟨Var x⟩"
        "cG = (More f ts1 c1 ts2 ⋅c σ) ∘c cG''"
        using ts1_γ ts2_γ
        unfolding cG ts context.subst_def
        by auto

      ultimately show ?case
        using Fun.prems(1)
        by blast
    qed
  }

  then show "(∃c t'. t = c⟨t'⟩ ∧ t' ⋅ σ = tG ∧ c ⋅c σ = cG) ∨
        (∃c cG' x. t = c⟨Var x⟩ ∧ cG = (c ⋅c σ) ∘c cG')"
    by metis
next
  fix c and t :: "('f, 'v) term"
  assume "c⟨t⟩ = t"
  then show "c = □"
    by (metis less_not_refl size_ne_ctxt)
qed auto

interpretation "term": occurences where
  comp_subst = "(∘s)" and Var = Var and term_subst = "(⋅)" and term_vars = term.vars and 
  compose_context = "(∘c)" and term_from_ground = term.from_ground and
  term_to_ground = term.to_ground and map_context = map_args_actxt and
  to_ground_context_map = map_args_actxt and from_ground_context_map = map_args_actxt and
  context_to_set = set2_actxt and hole = □ and apply_context = ctxt_apply_term and
  occurences = occurences and ground_hole = □ and compose_ground_context = "(∘c)" and
  ground_context_map = map_args_actxt and ground_context_to_set = set2_actxt and
  apply_ground_context = apply_ground_context
proof unfold_locales
  fix x c and t :: "('f, 'v) term"
  assume "term.is_ground t"

  then have "vars_term_ms t = {#}"
    by (induction t) auto

  then have "occurences t x = 0"
    by auto

  then show "occurences c⟨Var x⟩ x = Suc (occurences c⟨t⟩ x)"
    by (induction c) auto
next
  fix x and t :: "('f, 'v) term"

  show "x ∈ vars_term t ⟷ 0 < occurences t x"
    by auto
qed

end