Theory Nonground_Typing_With_Equality

theory Nonground_Typing_With_Equality
  imports
    Nonground_Typing_Generic
    Clause_Typing_With_Equality
    Nonground_Clause_With_Equality
begin

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

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 
  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_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

definition type_preserving_atom where
  "type_preserving_atom 𝒱 a ≡
    case rep_uprod a of (t, t') ⇒ ∀τ. 𝒱 ⊢ t : τ ⟷ 𝒱 ⊢ t' : τ"

definition type_preserving_literal where
  "type_preserving_literal 𝒱 l ≡ type_preserving_atom 𝒱 (atm_of l)"

definition type_preserving_literals where
  "type_preserving_literals 𝒱 C ≡ ∀l∈# C. type_preserving_literal 𝒱 l"

abbreviation is_ground_instance where 
  "is_ground_instance 𝒱 C γ ≡
    clause.is_ground (C ⋅ γ) ∧
    type_preserving_on (clause.vars C) 𝒱 γ ∧
    infinite_variables_per_type 𝒱 ∧
    type_preserving_literals 𝒱 C"

sublocale groundable_nonground_clause where 
  atom_subst = "(⋅a)" and atom_vars = atom.vars 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 rep_uprod_same_type [simp]: 
  "(case rep_uprod (Upair t t') of (t, t') ⇒ ∀τ. 𝒱 ⊢ t : τ ⟷ 𝒱 ⊢ t' : τ) ⟷
   (∀τ. 𝒱 ⊢ t : τ ⟷ 𝒱 ⊢ t' : τ)"
  by (rule rep_uprod_UpairI) auto

lemma type_preserving_atom_iff [simp]: 
  "type_preserving_atom 𝒱 (Upair t t') ⟷ (∀τ. 𝒱 ⊢ t : τ ⟷ 𝒱 ⊢ t' : τ)"
  unfolding type_preserving_atom_def
  by auto

lemma type_preserving_literal_iff [simp]:
  "type_preserving_literal 𝒱 (Pos a) ⟷ type_preserving_atom 𝒱 a"
  "type_preserving_literal 𝒱 (Neg a) ⟷ type_preserving_atom 𝒱 a"
  unfolding type_preserving_literal_def
  by auto

lemma type_preserving_literals_add_mset [simp]: 
  "type_preserving_literals 𝒱 (add_mset l C) ⟷ 
   type_preserving_literal 𝒱 l ∧  type_preserving_literals 𝒱 C"
  unfolding type_preserving_literals_def
  by auto

lemma type_preserving_literals_plus [simp]: 
  "type_preserving_literals 𝒱 (C + C') ⟷ 
   type_preserving_literals 𝒱 C ∧ type_preserving_literals 𝒱 C'"
  unfolding type_preserving_literals_def
  by auto

lemma type_preserving_literals_empty [intro]: "type_preserving_literals 𝒱' {#}"
  unfolding type_preserving_literals_def
  by 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. type_preserving_literal 𝒱 (𝒫 a) ⟷ type_preserving_atom 𝒱 a"
  using assms
  by (auto simp: literal_is_welltyped_iff_atm_of)

(* TODO: Lifting? *)
lemma type_preserving_atom_subst [simp]:
  assumes "type_preserving_on (atom.vars a) 𝒱 σ"
  shows "type_preserving_atom 𝒱 (a ⋅a σ) ⟷ type_preserving_atom 𝒱 a"
  using assms
proof (cases a)
  case (Upair t t')

  have type_preserving_σ: "type_preserving_on (term.vars t ∪ term.vars t') 𝒱 σ"
    using assms
    unfolding Upair
    by auto
    
  then show ?thesis
    unfolding Upair
    using term.welltyped_subst_stability
    by auto
qed

lemma type_preserving_literal_subst [simp]:
  assumes "type_preserving_on (literal.vars l) 𝒱 σ"
  shows "type_preserving_literal 𝒱 (l ⋅l σ) ⟷ type_preserving_literal 𝒱 l"
  using assms
  unfolding type_preserving_literal_def
  by (cases l) auto

lemma type_preserving_literals_subst [simp]:
  assumes "type_preserving_on (clause.vars C) 𝒱 σ"
  shows "type_preserving_literals 𝒱 (C ⋅ σ) ⟷ type_preserving_literals 𝒱 C"
  using assms
  by (induction C) auto

lemma type_preserving_atom_renaming [simp]:
  assumes
    ρ: "term.is_renaming ρ" and
    𝒱_𝒱': "∀x∈atom.vars a. 𝒱 x = 𝒱' (term.rename ρ x)"
  shows "type_preserving_atom 𝒱' (a ⋅a ρ) ⟷ type_preserving_atom 𝒱 a"
  using term.welltyped_renaming[OF ρ] 𝒱_𝒱'
  unfolding type_preserving_atom_def
  by (cases a) (auto simp: Set.ball_Un)

lemma type_preserving_literal_renaming [simp]:
  assumes
    ρ: "term.is_renaming ρ" and
    𝒱_𝒱': "∀x∈literal.vars l. 𝒱 x = 𝒱' (term.rename ρ x)"
  shows "type_preserving_literal 𝒱' (l ⋅l ρ) ⟷ type_preserving_literal 𝒱 l"
  using assms type_preserving_atom_renaming
  unfolding type_preserving_literal_def
  by (cases l) auto

lemma type_preserving_literals_renaming [simp]:
  assumes
    ρ: "term.is_renaming ρ" and
    𝒱_𝒱': "∀x∈clause.vars C. 𝒱 x = 𝒱' (term.rename ρ x)"
  shows "type_preserving_literals 𝒱' (C ⋅ ρ) ⟷ type_preserving_literals 𝒱 C"
  using assms 
  by (induction C) (auto simp: Set.ball_Un)

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
  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_to_ground = atom.to_ground and atom_from_ground = atom.from_ground
  by unfold_locales

end

end