Theory FCF_Problem

theory FCF_Problem
  imports Pattern_Completeness_Set
begin

type_synonym('f,'s)simple_match_problem = "('f,nat × 's)term set set" 

definition UNIQ_subst where "UNIQ_subst σ A = UNIQ (A ⋅⇩s⇩e⇩t σ)" 

lemma UNIQ_subst_pairI: assumes "⋀ s t. s ∈ A ⟹ t ∈ A ⟹ s ⋅ σ = t ⋅ σ" 
  shows "UNIQ_subst σ A" unfolding UNIQ_subst_def Uniq_def using assms by blast

lemma UNIQ_subst_trivial[simp]: "UNIQ_subst σ {t}" "UNIQ_subst σ {}" 
  by (auto simp: UNIQ_subst_def Uniq_def)

lemma UNIQ_subst_pairD: assumes "UNIQ_subst σ A" 
  shows "s ∈ A ⟹ t ∈ A ⟹ s ⋅ σ = t ⋅ σ" 
  using assms unfolding UNIQ_subst_def Uniq_def by blast

lemma UNIQ_mono: assumes "A ⊆ B" 
  shows "UNIQ B ⟹ UNIQ A" using assms
  by (simp add: Uniq_def subset_iff)

lemma UNIQ_subst_mono: assumes "A ⊆ B"
  shows "UNIQ_subst σ B ⟹ UNIQ_subst σ A" 
  unfolding UNIQ_subst_def using assms
  by (metis UNIQ_mono image_mono)

lemma UNIQ_subst_alt_def: "UNIQ_subst σ A = (∀ s t. s ∈ A ⟶ t ∈ A ⟶ s ⋅ σ = t ⋅ σ)" 
  unfolding UNIQ_subst_def Uniq_def by auto

definition simple_match_complete_wrt :: "('f,nat × 's,'w)gsubst ⇒ ('f,'s)simple_match_problem ⇒ bool" where
  "simple_match_complete_wrt σ mp = (∀ eqc ∈ mp. UNIQ_subst σ eqc)" 

type_synonym('f,'s)simple_pat_problem = "('f,'s)simple_match_problem set" 

abbreviation tvars_spat :: "('f,'s)simple_pat_problem ⇒ (nat × 's) set" where
  "tvars_spat spp ≡ ⋃ (⋃ (⋃ (image (image vars) ` spp)))" 

abbreviation tvars_smp :: "('f,'s)simple_match_problem ⇒ (nat × 's) set" where
  "tvars_smp smp ≡ ⋃ (⋃ (image vars ` smp))" 

definition simple_pat_complete :: "('f,'s) ssig ⇒ (nat × 's) set ⇒ ('f,'s)simple_pat_problem ⇒ bool" where
  "simple_pat_complete C S pp ⟷ (∀σ :⇩s 𝒱 |` S → 𝒯(C). ∃ mp ∈ pp. simple_match_complete_wrt σ mp)"

lemma tvars_spat_cong: assumes "⋀ x. x ∈ tvars_spat spp ⟹ σ x = δ x" 
  and "mp ∈ spp" 
shows "simple_match_complete_wrt σ mp = simple_match_complete_wrt δ mp" 
  unfolding simple_match_complete_wrt_def UNIQ_subst_alt_def
  apply (intro ball_cong refl all_cong1 imp_cong)
  apply (subst (1 2) term_subst_eq[of _ σ δ])
  using assms by force+


abbreviation set2 :: "'a list list ⇒ 'a set set" where "set2 ≡ image set o set" 
abbreviation set3 :: "'a list list list ⇒ 'a set set set" where "set3 ≡ image set2 o set"

context pattern_completeness_context
begin

definition finite_constructor_form_mp :: "('f,'s)simple_match_problem ⇒ bool" where
  "finite_constructor_form_mp mp = (∀ eqc ∈ mp. eqc ≠ {} ∧ (∃ ι. finite_sort C ι ∧ (∀ t ∈ eqc. t : ι in 𝒯(C,𝒱 |` SS))))" 

definition "finite_constructor_form_pat p = Ball p finite_constructor_form_mp" 

lemmas finite_constructor_form_defs = finite_constructor_form_pat_def finite_constructor_form_mp_def

definition fcf_solver where 
  "fcf_solver solver = (∀ fcf n . 
    finite_constructor_form_pat (set3 fcf) ⟶ 
    tvars_spat (set3 fcf) ⊆ {..<n} × UNIV ⟶
      solver n fcf = simple_pat_complete C SS (set3 fcf))" 
end

end