Theory Nonground_Abstract_Context

theory Nonground_Abstract_Context
  imports 
    Abstract_Context
    Nonground_Context
    Multiset_Extra
begin

(* TODO: Put assumptions into own locale *) 
(* TODO: Interpret nonground_term with term_interpretation *) 
(* TODO: Create version with and without grounding *)
(* TODO: Could we make the liftings more general that they also works here? *)
locale nonground_abstract_context = 
  "term": nonground_term where apply_subst = apply_subst and term_to_ground = term_to_ground +

  extra: grounding where 
  is_ground = extra_is_ground and apply_subst = extra_apply_subst and subst = extra_subst and
  from_ground = extra_from_ground and to_ground = extra_to_ground and vars = extra_vars +


  ground: abstract_context where
  is_var = "λ_. False" and Fun = GFun and fun_sym = fun_sym⇩G and extra = extra⇩G and
  subterms = subterms⇩G and size = size⇩G +

  abstract_context where is_var = term.is_Var and Fun = Fun 
for 
  apply_subst :: "'v ⇒ 'subst ⇒ 't" and 
  Fun :: "'f ⇒ 'e ⇒ 't list ⇒ 't" and
  term_to_ground :: "'t ⇒ 't⇩G" and

  extra_is_ground :: "'e ⇒ bool" and
  extra_to_ground :: "'e ⇒ 'e⇩G" and
  extra_vars :: "'e ⇒ 'v⇩e set" and
  extra_apply_subst extra_subst extra_from_ground and

  GFun :: "'f ⇒ 'e⇩G ⇒ 't⇩G list ⇒ 't⇩G" and
  fun_sym⇩G extra⇩G subterms⇩G size⇩G +
assumes
  term_from_ground [simp]:
    "⋀f e ts. 
      term.from_ground (GFun f e ts) = Fun f (extra_from_ground e) (map term.from_ground ts)" and
  term_to_ground [simp]:
    "⋀f e ts. term.to_ground (Fun f e ts) = GFun f (extra_to_ground e) (map term.to_ground ts)" and
  term_is_ground [simp]:
    "⋀f e ts.
      term.is_ground (Fun f e ts) ⟷ extra_is_ground e ∧ (∀t ∈ set ts. term.is_ground t)" and
  term_vars [simp]: "⋀f e ts. term.vars (Fun f e ts) = ⋃(term.vars ` set ts)" and
  term_subst [simp]: "⋀f e ts σ. Fun f e ts ⋅t σ = Fun f (extra_subst e σ) (map (λt. t ⋅t σ) ts)"
begin

(* TODO: Extract *)
lemma var_all_subterms_eq:
  assumes "x ∈ term.vars t"
  shows "term.Var x ∈ all_subterms_eq t"
  using assms
proof (induction rule: all_subterms_eq.induct)
  case (1 t)

  then show ?case
  proof (cases "term.is_Var t")
    case True
    then show ?thesis
      using "1.prems" term.vars_id_subst 
      by auto
  next
    case False

    then obtain t' where "t' ∈ set (subterms t)"  "x ∈ term.vars t'"
      by (metis "1.prems" UN_iff interpret_term term_vars)

    then show ?thesis
      using 1(1)
      by (metis UN_I Un_iff all_subterms_eq.simps)
  qed
qed
  
lemma var_is_subterm:
  assumes "x ∈ term.vars t"
  shows "term.Var x ⊴ t"
  using var_all_subterms_eq[OF assms] all_subterms_eq_is_subterm_eq
  by auto

definition is_ground where
  "is_ground c ≡ (∀t ∈ term_set c. term.is_ground t) ∧ (∀e ∈ extra_set c. extra_is_ground e)"

definition subst (infixl "⋅t⇩c" 67) where
  "subst c σ ≡ map_context id (λe. extra_subst e σ) (λt. t ⋅t σ) c"

definition vars where
  "vars c ≡ ⋃(term.vars ` term_set c)"

definition from_ground where
  "from_ground ≡ map_context id extra_from_ground term.from_ground"

definition to_ground where
  "to_ground ≡ map_context id extra_to_ground term.to_ground"

sublocale nonground_context where
  is_ground = is_ground and subst = subst and vars = vars and from_ground = from_ground and
  to_ground = to_ground and apply_context = apply_context and hole = □ and
  compose_context = "(∘⇩c)" and ground_hole = □ and compose_ground_context = "(∘⇩c)" and
  apply_ground_context = ground.apply_context
proof unfold_locales
  fix c :: "('f, 'e, 't) context" and t
  assume "c⟨t⟩ = t"

  then show "c = □"
    using size_apply_context
    by (metis nat_neq_iff)
next
  fix c :: "('f, 'e, 't) context" and σ σ'

  show "c ⋅t⇩c σ ⊙ σ' = c ⋅t⇩c σ ⋅t⇩c σ'"
    unfolding subst_def
    by (induction c) auto

  show "c ⋅t⇩c id_subst = c"
    unfolding subst_def
    by (induction c) auto

  show "vars (c ⋅t⇩c σ) = ⋃ (term.vars ` (λx. apply_subst x σ) ` vars c)"
    unfolding vars_def subst_def
    using term.base_vars_subst
    by (induction c) auto
next
  fix c :: "('f, 'e, 't) context"
  assume is_ground: "is_ground c"

  then show "∀σ. c ⋅t⇩c σ = c"
    unfolding is_ground_def subst_def
    by (induction c) (auto simp: map_idI)

  show "vars c = {}"
    using is_ground term.no_vars_if_is_ground
    unfolding is_ground_def vars_def
    by simp
next

  show "(∃expr. ¬ is_ground expr) ⟷ term.exists_nonground"
    unfolding is_ground_def
    using term_is_ground
    by (metis list.set_intros(1) context.set_intros(5))
next
  fix c :: "('f, 'e, 't) context" and γ
  assume "is_ground (c ⋅t⇩c γ)"

  then show "∀x∈vars c. term.is_ground (apply_subst x γ)"
  proof (unfold is_ground_def subst_def vars_def, induction c)
    case Hole

    then show ?case
      by simp
  next
    case (More f e ls c rs)

    then show ?case
      by (metis (no_types, lifting) UN_iff context.set_map(3) rev_image_eqI term.variable_grounding)
  qed
next
  {
    fix c :: "('f, 'e, 't) context"
    assume c_is_ground: "is_ground c"

    have "∃c⇩G. from_ground c⇩G = c"
    proof(intro exI)

      from c_is_ground
      show "from_ground (to_ground c) = c"
        unfolding is_ground_def from_ground_def to_ground_def
        by (induction c) (auto simp: map_idI)
    qed
  }

  moreover have "is_ground (from_ground c⇩G)" for c⇩G :: "('f, 'e⇩G, 't⇩G) context"
    unfolding is_ground_def from_ground_def
    by (induction c⇩G) auto  

  ultimately show "{c :: ('f, 'e, 't) context. is_ground c} = range from_ground"
    by blast
next
  fix c⇩G :: "('f, 'e⇩G, 't⇩G) context"

  show "to_ground (from_ground c⇩G) = c⇩G"
    unfolding to_ground_def from_ground_def
    by (induction c⇩G) auto
next
  fix c t

  show "term.to_ground c⟨t⟩ = ground.apply_context (to_ground c) (term.to_ground t)"
    unfolding to_ground_def
    by (induction c) auto
next
  fix c⇩G t⇩G

  show "term.from_ground (ground.apply_context c⇩G t⇩G) = (from_ground c⇩G)⟨term.from_ground t⇩G⟩"
    unfolding from_ground_def
    by (induction c⇩G) auto
next
  fix c t

  show "term.is_ground c⟨t⟩ ⟷ is_ground c ∧ term.is_ground t"
    unfolding is_ground_def
    by (induction c) auto
next
  fix c⇩G c'⇩G :: "('f, 'e⇩G, 't⇩G) context"

  show "from_ground (c⇩G ∘⇩c c'⇩G) = from_ground c⇩G ∘⇩c from_ground c'⇩G"
    unfolding from_ground_def
    by (induction c⇩G) auto
next
  fix c t

  show "term.vars c⟨t⟩ = vars c ∪ term.vars t"
    using term_vars
    unfolding vars_def
    by (induction c) auto
next
  fix c t σ

  show "c⟨t⟩ ⋅t σ = (c ⋅t⇩c σ)⟨t ⋅t σ⟩"
    unfolding subst_def
    by (induction c) auto
next
  fix x t
  assume "x ∈ term.vars t"

  then show "∃c. t = c⟨term.Var x⟩"
    unfolding is_subterm_iff_exists_context[symmetric]
    by (simp add: var_is_subterm)
next
  fix c :: "('f, 'e, 't) context" and μ XX
  assume imgu: "term.is_imgu μ XX" "finite XX" "∀X∈XX. finite X"

  show "vars (c ⋅t⇩c μ) ⊆ vars c ∪ ⋃ (term.vars ` ⋃ XX)"
    using term.variables_in_base_imgu[OF imgu]
    unfolding vars_def subst_def
    by (smt (verit, ccfv_threshold) UN_iff Un_iff context.set_map(3) image_iff subset_eq)
next
  fix t γ c⇩G t⇩G
  assume t_γ: "t ⋅t γ = c⇩G⟨t⇩G⟩" and t_grounding: "term.is_ground (t ⋅t γ)"

  {
    assume "∄c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = t⇩G ∧ c ⋅t⇩c γ = c⇩G"

    with t_γ t_grounding have "∃c c' x. t = c⟨term.Var x⟩ ∧ (c ⋅t⇩c γ) ∘⇩c c' = c⇩G"
    proof (induction c⇩G arbitrary: t)
      case Hole
      then show ?case
        by (simp add: subst_def)
    next
      case (More f e ls c⇩G rs)

      have t_γ: "t ⋅t γ = Fun f e (ls @ c⇩G⟨t⇩G⟩ # rs)"
        using More(2, 3)
        by simp

      show ?case
      proof (cases "term.is_Var t")
        case True

        then show ?thesis
          by (metis apply_hole compose_context.simps(1) context.map_disc_iff subst_def)
      next
        case False

        then obtain e' ts' where t: "t = Fun f e' ts'"
          by (metis More.prems(1) apply_context.simps(2) term_destruct term_fun_sym term_subst)

        have "map (λt. t ⋅t γ) ts' = ls @ c⇩G⟨t⇩G⟩ # rs"
          using t_γ
          unfolding t term_subst
          by (metis subterms)

        then obtain rs' t' ls' where 
          ts': "ts' = ls' @ t' # rs'" and
          ls: "ls = map (λt. t ⋅t γ) ls'" and
          t'_γ: "t' ⋅t γ = c⇩G⟨t⇩G⟩" and
          rs: "rs = map (λt. t ⋅t γ) rs'"
          by (smt (verit, ccfv_threshold) map_eq_Cons_conv map_eq_append_conv)

        have "∃c c' x. t' = c⟨term.Var x⟩ ∧ (c ⋅t⇩c γ) ∘⇩c c' = c⇩G"
        proof (rule More.IH[OF t'_γ])

          show "term.is_ground (t' ⋅t γ)"
            using More.prems(2) t'_γ t_γ term_is_ground 
            by fastforce
        next

          show "∄c t''. t' = c⟨t''⟩ ∧ t'' ⋅t γ = t⇩G ∧ c ⋅t⇩c γ = c⇩G"
          proof (rule notI)
            assume "∃c t''. t' = c⟨t''⟩ ∧ t'' ⋅t γ = t⇩G ∧ c ⋅t⇩c γ = c⇩G"

            then obtain c t'' where t': "t' = c⟨t''⟩" and t''_γ: "t'' ⋅t γ = t⇩G" and c: "c ⋅t⇩c γ = c⇩G"
              by blast

            have "(More f e' ls' c rs') ⋅t⇩c γ = More f e ls c⇩G rs"
              using c t t_γ term_inject ls rs
              unfolding subst_def
              by auto

            then show False
              using More(4) t' t''_γ t ts'
              by auto
          qed
        qed

        then obtain c c' x where t': "t' = c⟨term.Var x⟩" and c_c': "(c ⋅t⇩c γ) ∘⇩c c' = c⇩G"
          by blast

        show ?thesis
        proof (intro exI conjI)

          show "t = (More f e' ls' c rs')⟨term.Var x⟩"
            by (simp add: t' t ts')
        next

          show "(More f e' ls' c rs' ⋅t⇩c γ) ∘⇩c c' = More f e ls c⇩G rs"
            using t t_γ term_inject ls rs c_c'
            unfolding subst_def
            by auto
        qed
      qed
    qed
  }

  then show
    "(∃c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = t⇩G ∧ c ⋅t⇩c γ = c⇩G) ∨
     (∃c c⇩G' x. t = c⟨term.Var x⟩ ∧ c⇩G = (c ⋅t⇩c γ) ∘⇩c c⇩G')"
    by blast
qed

(* TODO: Extract *)
function vars_ms :: "'t ⇒ 'v multiset" where
  "vars_ms t =
    (if term.is_Var t then {# term.the_Var t #}
     else ∑⇩# (mset (map vars_ms (subterms t))))"
  by auto

termination
proof (relation "measure size")
  fix t t'
  assume "t' ∈ set (subterms t)"

  then show "(t', t) ∈ measure size"
    using subterms_smaller
    by simp  
qed auto

declare vars_ms.simps [simp del]

lemma vars_ms_Var [simp]: 
  assumes "term.exists_nonground"
  shows "vars_ms (term.Var x) = {#x#}"
  using assms
  by
    (subst vars_ms.simps)
    (metis rename_def term.id_subst_rename term.inv_renaming term.neutral_is_right_invertible)

lemma vars_ms_Fun [simp]: 
  "vars_ms (Fun f e ts) = ∑⇩# (mset (map vars_ms ts))"
  by (subst vars_ms.simps) (use term_destruct in auto)

lemma is_ground_vars_ms [simp]: 
  assumes "term.is_ground t"
  shows "vars_ms t = {#}"
  using assms
proof (induction rule: term_induct)
  case (1 t)

  then obtain f e ts where t: "t = Fun f e ts"
    by (metis ground.term_destruct term.to_ground_inverse term_from_ground)

  have "sum_list (map vars_ms ts) = {#}"
    using 1
    unfolding t
    by (smt (verit) map_eq_conv subterms sum_list_0 term_is_ground)

  then show ?case
    using 1
    unfolding t
    by auto
qed
  

lemma vars_ms_vars [simp]: "set_mset (vars_ms t) = term.vars t"
proof (induction rule: all_subterms_eq.induct)
  case (1 t)

  then show ?case
  proof (cases "term.exists_nonground")
    case True

    have [simp]: "vars_ms (term.Var x) = {#x#}" for x
      using True
      by simp

    have [simp]: "term.vars (term.Var x) = {x}" for x
      using True
      by (simp add: term.vars_id_subst)

    show ?thesis
    proof (cases "term.is_Var t")
      case is_Var: True

      then show ?thesis
        by auto
    next
      case is_Fun: False

      then obtain f e ts where t: "t = Fun f e ts"
        by (metis term_destruct)

      show ?thesis 
        using 1
        unfolding t
        by auto
    qed
  next
    case False

    then have "term.vars t = {}"
      by (metis term.no_vars_if_is_ground)

    then show ?thesis
      by (metis False set_mset_empty is_ground_vars_ms)
  qed
qed

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

sublocale occurences where
  is_ground = is_ground and subst = subst and vars = vars and from_ground = from_ground and
  to_ground = to_ground and apply_context = apply_context and hole = □ and
  compose_context = "(∘⇩c)" and ground_hole = □ and compose_ground_context = "(∘⇩c)" and
  apply_ground_context = ground.apply_context and occurences = occurences
proof unfold_locales
  fix x c t
  assume "term.exists_nonground" "term.is_ground t"

  then show "occurences c⟨term.Var x⟩ x = Suc (local.occurences c⟨t⟩ x)"
    by (induction c) auto
next
  fix x t 

  show "x ∈ term.vars t ⟷ 0 < occurences t x"
    by auto
qed

end

end