Theory Nonground_Typing_With_Equality

theory Nonground_Typing_With_Equality
  imports
    Nonground_Typing_Generic
    Clause_Typing_With_Equality
    Nonground_Clause_With_Equality
    Weakly_Typed_Substitution
begin

type_synonym ('t, 'v, 'ty) typed_clause = "('v, 'ty) var_types × 't clause"

locale base_weakly_welltyped_properties =
  base_weakly_welltyped_unifier +
  base_weakly_welltyped_subst_stability +
  base_weakly_welltyped_renaming

locale weakly_welltyped_properties_lifting =
  weakly_welltyped_unifier_lifting +
  weakly_welltyped_subst_stability_lifting +
  weakly_welltyped_renaming_lifting

locale term_based_weakly_welltyped_lifting =
  term_typing_properties +
  weakly_welltyped_properties_lifting where base_subst = "(⋅t)" and base_vars = term.vars and
  base_is_ground = term.is_ground and
  base_welltyped = welltyped 

locale nonground_typing =
  nonground_clause +
  term_typing_properties +
  atom: term_based_nonground_typing_lifting where 
  sub_welltyped = welltyped and sub_subst = "(⋅t)" and sub_vars = term.vars and
  sub_is_ground = term.is_ground and
  to_set = set_uprod and map = map_uprod and sub_to_ground = term.to_ground and 
  sub_from_ground = term.from_ground and to_ground_map = map_uprod and 
  from_ground_map = map_uprod and ground_map = map_uprod and to_set_ground = set_uprod
begin

sublocale nonground_typing_generic where 
  atom_subst = "(⋅a)" and atom_vars = atom.vars and atom_is_ground = atom.is_ground and
  atom_to_ground = atom.to_ground and atom_from_ground = atom.from_ground and
  atom_welltyped = atom.welltyped
  by unfold_locales

sublocale clause_typing "welltyped 𝒱"
  by unfold_locales

sublocale atom: base_weakly_welltyped_properties where 
  base_subst = "(⋅t)" and base_vars = term.vars and base_is_ground = term.is_ground and
  base_welltyped = welltyped and map = map_uprod and to_set = set_uprod
  by unfold_locales

sublocale literal: term_based_weakly_welltyped_lifting where
  map = map_literal and to_set = set_literal and sub_subst = "(⋅a)" and sub_vars = atom.vars and
  sub_is_ground = atom.is_ground and sub_welltyped = atom.welltyped and
  sub_to_base_set = set_uprod and sub_weakly_welltyped = atom.weakly_welltyped
  by unfold_locales

sublocale clause: term_based_weakly_welltyped_lifting where
  map = image_mset and to_set = set_mset and sub_subst = "(⋅l)" and sub_vars = literal.vars and
  sub_is_ground = literal.is_ground and sub_welltyped = literal.welltyped and
  sub_to_base_set = literal.to_base_set and sub_weakly_welltyped = literal.weakly_welltyped
  by unfold_locales

lemma [intro]:
  assumes "type_preserving_on (term.vars t ∪ term.vars t') 𝒱 μ" "term.is_imgu μ {{t, t'}}"
  shows
    imgu_weakly_welltyped_literal_Pos: "literal.weakly_welltyped 𝒱 (t ≈ t')" and 
    imgu_weakly_welltyped_literal_Neg: "literal.weakly_welltyped 𝒱 (t !≈ t')"
  using atom.is_imgu_weakly_welltyped[of "Upair t t'"] assms
  unfolding literal.weakly_welltyped_def
  by auto

abbreviation is_ground_instance where 
  "is_ground_instance 𝒱 C γ ≡
    clause.is_ground (C ⋅ γ) ∧
    type_preserving_on (clause.vars C) 𝒱 γ ∧
    (term.exists_nonground ⟶ infinite_variables_per_type 𝒱) ∧
    clause.weakly_welltyped 𝒱 C"

sublocale groundable_nonground_clause where 
  atom_subst = "(⋅a)" and atom_vars = atom.vars and atom_is_ground = atom.is_ground and
  atom_to_ground = atom.to_ground and atom_from_ground = atom.from_ground and
  is_ground_instance = is_ground_instance
  by unfold_locales simp

lemma 𝒫_simps:
  assumes "𝒫 ∈ {Pos, Neg}"
  shows 
    "⋀a σ. 𝒫 a ⋅l σ = 𝒫 (a ⋅a σ)"
    "⋀𝒱 a. literal.is_welltyped 𝒱 (𝒫 a) ⟷ atom.is_welltyped 𝒱 a"
    "⋀a. literal.vars (𝒫 a) = atom.vars a"
    "⋀a. atm_of (𝒫 a) = a"
    "⋀𝒱 a. literal.weakly_welltyped 𝒱 (𝒫 a) ⟷ atom.weakly_welltyped 𝒱 a"
  using assms
  by (auto simp: literal_is_welltyped_iff_atm_of)

end

locale witnessed_nonground_typing =
  nonground_typing +

  atom: term_based_witnessed_nonground_typing_lifting where
  sub_welltyped = welltyped and sub_subst = "(⋅t)" and sub_vars = term.vars and
  sub_is_ground = term.is_ground and
  to_set = set_uprod and map = map_uprod and sub_to_ground = term.to_ground and
  sub_from_ground = term.from_ground and to_ground_map = map_uprod and
  from_ground_map = map_uprod and ground_map = map_uprod and to_set_ground = set_uprod
begin

sublocale witnessed_nonground_typing_generic where
  atom_welltyped = atom.welltyped and atom_subst = "(⋅a)" and atom_vars = atom.vars and
  atom_is_ground = atom.is_ground and atom_to_ground = atom.to_ground and
  atom_from_ground = atom.from_ground
  by unfold_locales

end

end