Theory Nonground_Context

theory Nonground_Context
  imports
    Nonground_Term
    Ground_Context
begin

section ‹Nonground Contexts and Substitutions›

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

abbreviation subst_apply_ctxt ::
  "('f, 'v) context ⇒ ('f, 'v) subst ⇒ ('f, 'v) context" (infixl "⋅t⇩c" 67) where (* TODO: Naming *)
  "subst_apply_ctxt ≡ subst_apply_actxt"

(* TODO: Move? *)
global_interpretation "context": finite_natural_functor where
  map = map_args_actxt and to_set = set2_actxt
proof unfold_locales
  fix t :: 't

  show "∃c. t ∈ set2_actxt c"
    by (metis actxt.set_intros(5) list.set_intros(1))
next
  fix c :: "('f, 't) actxt"

  show "finite (set2_actxt c)"
    by(induction c) auto
qed (auto
    simp: actxt.set_map(2) actxt.map_comp fun.map_ident actxt.map_ident_strong
    cong: actxt.map_cong)

global_interpretation "context": natural_functor_conversion where
  map = map_args_actxt and to_set = set2_actxt and map_to = map_args_actxt and
  map_from = map_args_actxt and map' = map_args_actxt and to_set' = set2_actxt
  by unfold_locales
    (auto simp: actxt.set_map(2) actxt.map_comp cong: actxt.map_cong)

locale nonground_context =
  "term": nonground_term
begin

sublocale term_based_lifting where
  sub_subst = "(⋅t)" and sub_vars = term.vars and
  to_set = "set2_actxt :: ('f, 'v) context ⇒ ('f, 'v) term set" and map = map_args_actxt and
  sub_to_ground = term.to_ground and sub_from_ground = term.from_ground and
  to_ground_map = map_args_actxt and from_ground_map = map_args_actxt and
  ground_map = map_args_actxt and to_set_ground = set2_actxt
rewrites
  "⋀c σ. subst c σ = c ⋅t⇩c σ" and
  "⋀c. vars c = vars_ctxt c" (* TODO: Name *)
proof unfold_locales
  interpret term_based_lifting where
    sub_vars = term.vars and sub_subst = "(⋅t)" and map = map_args_actxt and to_set = set2_actxt and
    sub_to_ground = term.to_ground and sub_from_ground = term.from_ground and
    ground_map = map_args_actxt and to_ground_map = map_args_actxt and
    from_ground_map = map_args_actxt and to_set_ground = set2_actxt
    by unfold_locales

  fix c :: "('f, 'v) context"
  show "vars c = vars_ctxt c"
    by(induction c) (auto simp: vars_def)

  fix σ
  show "subst c σ = c ⋅t⇩c σ"
    unfolding subst_def
    by blast
qed

lemma ground_ctxt_iff_context_is_ground [simp]: "ground_ctxt c ⟷ is_ground c"
  by(induction c) simp_all

lemma term_to_ground_context_to_ground [simp]:
  shows "term.to_ground c⟨t⟩ = (to_ground c)⟨term.to_ground t⟩⇩G"
  unfolding to_ground_def
  by(induction c) simp_all

lemma term_from_ground_context_from_ground [simp]:
  "term.from_ground c⇩G⟨t⇩G⟩⇩G = (from_ground c⇩G)⟨term.from_ground t⇩G⟩"
  unfolding from_ground_def
  by(induction c⇩G) simp_all

lemma term_from_ground_context_to_ground:
  assumes "is_ground c"
  shows "term.from_ground (to_ground c)⟨t⇩G⟩⇩G = c⟨term.from_ground t⇩G⟩"
  unfolding to_ground_def
  by (metis assms term_from_ground_context_from_ground to_ground_def to_ground_inverse)

lemmas safe_unfolds =
  eval_ctxt
  term_to_ground_context_to_ground
  term_from_ground_context_from_ground

lemma composed_context_is_ground [simp]:
  "is_ground (c ∘⇩c c') ⟷ is_ground c ∧ is_ground c'"
  by(induction c) auto

(* TODO: Name/ Remove? *)
lemma ground_context_subst:
  assumes
    "is_ground c⇩G"
    "c⇩G = (c ⋅t⇩c σ) ∘⇩c c'"
  shows
    "c⇩G = c ∘⇩c c' ⋅t⇩c σ"
  using assms
  by(induction c) simp_all

lemma from_ground_hole [simp]: "from_ground c⇩G = □ ⟷ c⇩G = □"
  by(cases c⇩G) (simp_all add: from_ground_def)

lemma hole_simps [simp]: "from_ground □ = □" "to_ground □ = □"
  by (auto simp: to_ground_def)

lemma term_with_context_is_ground [simp]:
  "term.is_ground c⟨t⟩ ⟷ is_ground c ∧ term.is_ground t"
  by simp

lemma map_args_actxt_compose [simp]:
  "map_args_actxt f (c ∘⇩c c') = map_args_actxt f c ∘⇩c map_args_actxt f c'"
  by(induction c) auto

lemma from_ground_compose [simp]: "from_ground (c ∘⇩c c') = from_ground c ∘⇩c from_ground c'"
  unfolding from_ground_def
  by simp

lemma to_ground_compose [simp]: "to_ground (c ∘⇩c c') = to_ground c ∘⇩c to_ground c'"
  unfolding to_ground_def
  by simp

end

locale nonground_term_with_context =
  "term": nonground_term +
  "context": nonground_context

end