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 weakly_welltyped_atom where
  "weakly_welltyped_atom 𝒱 a ≡
    case rep_uprod a of (t, t') ⇒ ∀τ. 𝒱 ⊢ t : τ ⟷ 𝒱 ⊢ t' : τ"

definition weakly_welltyped_literal where
  "weakly_welltyped_literal 𝒱 l ≡ weakly_welltyped_atom 𝒱 (atm_of l)"

lemma imgu_weakly_welltyped_atom [intro]:
  assumes "type_preserving_on (atom.vars a) 𝒱 μ" "term.is_imgu μ {set_uprod a}"
  shows "weakly_welltyped_atom 𝒱 a"
proof -

  obtain t t' where rep_uprod_a: "rep_uprod a = (t, t')" and a: "a = Upair t t'"
    by (cases a) (metis Quotient3_uprod surj_pair Quotient3_def Upair.abs_eq)

  have "type_preserving_on (term.vars t ∪ term.vars t') 𝒱 μ" "term.is_imgu μ {{t, t'}}"
    using assms
    unfolding a
    by simp_all

  then show ?thesis
    using term.imgu_same_type
    unfolding weakly_welltyped_atom_def rep_uprod_a
    by blast
qed  

lemma imgu_weakly_welltyped_literal [intro]:
  assumes "type_preserving_on (literal.vars l) 𝒱 μ" "term.is_imgu μ {uprod_literal_to_set l}"
  shows "weakly_welltyped_literal 𝒱 l"
  using imgu_weakly_welltyped_atom assms
  unfolding weakly_welltyped_literal_def
  by (cases l) simp_all

lemma [intro]:
  assumes "type_preserving_on (term.vars t ∪ term.vars t') 𝒱 μ" "term.is_imgu μ {{t, t'}}"
  shows 
    imgu_weakly_welltyped_literal_Pos: "weakly_welltyped_literal 𝒱 (t ≈ t')" and 
    imgu_weakly_welltyped_literal_Neg: "weakly_welltyped_literal 𝒱 (t !≈ t')"
  using imgu_weakly_welltyped_atom assms
  unfolding weakly_welltyped_literal_def
  by simp_all

definition weakly_welltyped_clause where
  "weakly_welltyped_clause 𝒱 C ≡ ∀l∈# C. weakly_welltyped_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 𝒱 ∧
    weakly_welltyped_clause 𝒱 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 weakly_welltyped_atom_iff [simp]: 
  "weakly_welltyped_atom 𝒱 (Upair t t') ⟷ (∀τ. 𝒱 ⊢ t : τ ⟷ 𝒱 ⊢ t' : τ)"
  unfolding weakly_welltyped_atom_def
  by auto

lemma weakly_welltyped_literal_iff [simp]:
  "weakly_welltyped_literal 𝒱 (Pos a) ⟷ weakly_welltyped_atom 𝒱 a"
  "weakly_welltyped_literal 𝒱 (Neg a) ⟷ weakly_welltyped_atom 𝒱 a"
  unfolding weakly_welltyped_literal_def
  by auto

lemma weakly_welltyped_clause_add_mset [simp]: 
  "weakly_welltyped_clause 𝒱 (add_mset l C) ⟷
   weakly_welltyped_literal 𝒱 l ∧ weakly_welltyped_clause 𝒱 C"
  unfolding weakly_welltyped_clause_def
  by auto

lemma weakly_welltyped_clause_plus [simp]: 
  "weakly_welltyped_clause 𝒱 (C + C') ⟷ 
   weakly_welltyped_clause 𝒱 C ∧ weakly_welltyped_clause 𝒱 C'"
  unfolding weakly_welltyped_clause_def
  by auto

lemma weakly_welltyped_clause_empty [intro]: "weakly_welltyped_clause 𝒱' {#}"
  unfolding weakly_welltyped_clause_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. weakly_welltyped_literal 𝒱 (𝒫 a) ⟷ weakly_welltyped_atom 𝒱 a"
  using assms
  by (auto simp: literal_is_welltyped_iff_atm_of)

(* TODO: Lifting? *)
lemma weakly_welltyped_atom_subst [simp]:
  assumes "type_preserving_on (atom.vars a) 𝒱 σ"
  shows "weakly_welltyped_atom 𝒱 (a ⋅a σ) ⟷ weakly_welltyped_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 weakly_welltyped_literal_subst [simp]:
  assumes "type_preserving_on (literal.vars l) 𝒱 σ"
  shows "weakly_welltyped_literal 𝒱 (l ⋅l σ) ⟷ weakly_welltyped_literal 𝒱 l"
  using assms
  unfolding weakly_welltyped_literal_def
  by (cases l) auto

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

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

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

lemma weakly_welltyped_clause_renaming [simp]:
  assumes
    ρ: "term.is_renaming ρ" and
    𝒱_𝒱': "∀x∈clause.vars C. 𝒱 x = 𝒱' (term.rename ρ x)"
  shows "weakly_welltyped_clause 𝒱' (C ⋅ ρ) ⟷ weakly_welltyped_clause 𝒱 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