Theory First_Order_Clause.Nonground_Typing_Generic

theory Nonground_Typing_Generic
  imports
    Nonground_Term_Typing
    Clause_Typing_Generic
    Typed_Functional_Substitution_Lifting
    Nonground_Clause_Generic
begin

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

locale nonground_typing_lifting =
  typed_subst_stability_lifting +
  replaceable_𝒱_lifting +
  typed_renaming_lifting +
  grounding_lifting

locale term_based_nonground_typing_lifting =
  term_typing_properties +
  nonground_typing_lifting where
  base_welltyped = welltyped and id_subst = Var and comp_subst = "(⊙)" and
  base_subst = "(⋅t)" and base_vars = term.vars

locale term_based_witnessed_nonground_typing_lifting =
  term_based_nonground_typing_lifting +
  witnessed_typed_functional_substitution_lifting where
  id_subst = Var and comp_subst = "(⊙)" and base_subst = "(⋅t)" and base_vars = term.vars and 
  base_welltyped = welltyped

locale nonground_typing_generic =
  term_typing_properties where welltyped = welltyped +
  literal: term_based_nonground_typing_lifting where sub_welltyped = atom_welltyped and
  sub_to_ground = "atom_to_ground :: 'a ⇒ 'g" and sub_from_ground = atom_from_ground and
  sub_subst = atom_subst and sub_vars = atom_vars and map = map_literal and to_set = set_literal and
  to_ground_map = map_literal and from_ground_map = map_literal and ground_map = map_literal and
  to_set_ground = set_literal and welltyped = welltyped +
  nonground_clause_generic
for
  welltyped :: "('v, 'ty) var_types ⇒ 't ⇒ 'ty ⇒ bool" and
  atom_welltyped :: "('v, 'ty) var_types ⇒ 'a ⇒ 'ty' ⇒ bool"
begin

sublocale clause_typing_generic "atom_welltyped 𝒱"
  by unfold_locales

sublocale clause: term_based_nonground_typing_lifting where
  sub_vars = literal.vars and sub_subst = "(⋅l)" and map = image_mset and to_set = set_mset and
  sub_welltyped = literal.welltyped and sub_to_ground = literal.to_ground and
  sub_from_ground = literal.from_ground and to_ground_map = image_mset and
  from_ground_map = image_mset and ground_map = image_mset and to_set_ground = set_mset
  by unfold_locales

end

locale witnessed_nonground_typing_generic =
  literal: term_based_witnessed_nonground_typing_lifting where sub_welltyped = atom_welltyped and
  sub_to_ground = "atom_to_ground :: 'a ⇒ 'g" and sub_from_ground = atom_from_ground and
  sub_subst = atom_subst and sub_vars = atom_vars and map = map_literal and to_set = set_literal and
  to_ground_map = map_literal and from_ground_map = map_literal and ground_map = map_literal and
  to_set_ground = set_literal and welltyped = welltyped +
  nonground_typing_generic
begin

sublocale clause: term_based_witnessed_nonground_typing_lifting where
  sub_vars = literal.vars and sub_subst = "(⋅l)" and map = image_mset and to_set = set_mset and
  sub_welltyped = literal.welltyped and
  sub_to_ground = literal.to_ground and sub_from_ground = literal.from_ground and
  to_ground_map = image_mset and from_ground_map = image_mset and ground_map = image_mset and
  to_set_ground = set_mset
  by unfold_locales

end

end