Theory Unification_Theorem

section ‹The Unification Theorem›

theory Unification_Theorem imports
  First_Order_Terms.Unification Resolution
begin

definition set_to_list :: "'a set ⇒ 'a list" where
  "set_to_list ≡ inv set"

lemma set_set_to_list: "finite xs ⟹ set (set_to_list xs) = xs"
proof (induction rule: finite.induct)
  case (emptyI) 
  have "set [] = {}" by auto
  then show ?case unfolding set_to_list_def inv_into_def by auto
next
  case (insertI A a)
  then have "set (a#set_to_list A) = insert a A" by auto
  then show ?case unfolding set_to_list_def inv_into_def by (metis (mono_tags, lifting) UNIV_I someI) 
qed

fun iterm_to_fterm :: "(fun_sym, var_sym) term ⇒ fterm" where
  "iterm_to_fterm (Term.Var x) = Var x"
| "iterm_to_fterm (Term.Fun f ts) = Fun f (map iterm_to_fterm ts)"

fun fterm_to_iterm :: "fterm ⇒ (fun_sym, var_sym) term" where
  "fterm_to_iterm (Var x) = Term.Var x"
| "fterm_to_iterm (Fun f ts) = Term.Fun f (map fterm_to_iterm ts)"

lemma iterm_to_fterm_cancel[simp]: "iterm_to_fterm (fterm_to_iterm t) = t"
  by (induction t) (auto simp add: map_idI)

lemma fterm_to_iterm_cancel[simp]: "fterm_to_iterm (iterm_to_fterm t) = t"
  by (induction t) (auto simp add: map_idI)

abbreviation(input) fsub_to_isub :: "substitution ⇒ (fun_sym, var_sym) subst" where
  "fsub_to_isub σ ≡ λx. fterm_to_iterm (σ x)"

abbreviation(input) isub_to_fsub :: "(fun_sym, var_sym) subst ⇒ substitution" where
  "isub_to_fsub σ ≡ λx. iterm_to_fterm (σ x)"

lemma iterm_to_fterm_subt: "(iterm_to_fterm t1) ⋅⇩t σ = iterm_to_fterm (t1 ⋅ (λx. fterm_to_iterm (σ x)))"
  by (induction t1) auto

lemma unifiert_unifiers:
  assumes "unifier⇩t⇩s σ ts"
  shows "fsub_to_isub σ ∈ unifiers (fterm_to_iterm ` ts × fterm_to_iterm ` ts)"
proof -
  have "∀t1 ∈ fterm_to_iterm ` ts. ∀t2 ∈ fterm_to_iterm ` ts. t1 ⋅ (fsub_to_isub σ) = t2 ⋅ (fsub_to_isub σ)"
    proof (rule ballI;rule ballI)
      fix t1 t2 
      assume t1_p: "t1 ∈ fterm_to_iterm ` ts" assume t2_p: "t2 ∈ fterm_to_iterm ` ts"
      from t1_p t2_p have "iterm_to_fterm t1 ∈ ts ∧ iterm_to_fterm t2 ∈ ts" by auto 
      then have "(iterm_to_fterm t1) ⋅⇩t σ = (iterm_to_fterm t2) ⋅⇩t σ" using assms unfolding unifier⇩t⇩s_def by auto
      then have "iterm_to_fterm (t1 ⋅ fsub_to_isub σ) = iterm_to_fterm (t2 ⋅ fsub_to_isub σ)" using iterm_to_fterm_subt by auto 
      then have "fterm_to_iterm (iterm_to_fterm (t1 ⋅ fsub_to_isub σ)) = fterm_to_iterm (iterm_to_fterm (t2 ⋅ fsub_to_isub σ))" by auto
      then show "t1 ⋅ fsub_to_isub σ = t2 ⋅ fsub_to_isub σ" using fterm_to_iterm_cancel by auto
    qed
  then have "∀p∈fterm_to_iterm ` ts × fterm_to_iterm ` ts. fst p ⋅ fsub_to_isub σ = snd p ⋅ fsub_to_isub σ" by (metis mem_Times_iff) 
  then show ?thesis unfolding unifiers_def by blast
qed

abbreviation(input) get_mgut :: "fterm list ⇒ substitution option" where
  "get_mgut ts ≡ map_option (isub_to_fsub ∘ subst_of) (unify (List.product (map fterm_to_iterm ts) (map fterm_to_iterm ts)) [])"

lemma unify_unification:
  assumes "σ ∈ unifiers (set E)"
  shows "∃θ. is_imgu θ (set E)"
proof -
  from assms have "∃cs. unify E [] = Some cs" using unify_complete by auto
  then show ?thesis using unify_sound by auto
qed

lemma fterm_to_iterm_subst: "(fterm_to_iterm t1) ⋅ σ =fterm_to_iterm (t1 ⋅⇩t isub_to_fsub σ)"
  by (induction t1) auto

lemma unifiers_unifiert:
  assumes "σ ∈ unifiers (fterm_to_iterm ` ts × fterm_to_iterm ` ts)"
  shows "unifier⇩t⇩s (isub_to_fsub σ) ts"
proof (cases "ts={}")
  assume "ts = {}"
  then show "unifier⇩t⇩s (isub_to_fsub σ) ts" unfolding unifier⇩t⇩s_def by auto
next
  assume "ts ≠ {}"
  then obtain t' where t'_p: "t' ∈ ts" by auto

  have "∀t⇩1∈ts. ∀t⇩2∈ts. t⇩1 ⋅⇩t isub_to_fsub σ = t⇩2 ⋅⇩t isub_to_fsub σ"
    proof (rule ballI ; rule ballI)
      fix t⇩1 t⇩2 
      assume "t⇩1 ∈ ts" "t⇩2 ∈ ts" 
      then have "fterm_to_iterm t⇩1 ∈ fterm_to_iterm ` ts" "fterm_to_iterm t⇩2 ∈ fterm_to_iterm ` ts" by auto
      then have "(fterm_to_iterm t⇩1, fterm_to_iterm t⇩2) ∈ (fterm_to_iterm ` ts × fterm_to_iterm ` ts)" by auto
      then have "(fterm_to_iterm t⇩1) ⋅ σ = (fterm_to_iterm t⇩2) ⋅ σ" using assms unfolding unifiers_def
         by (metis (no_types, lifting) assms fst_conv in_unifiersE snd_conv)
      then have "fterm_to_iterm (t⇩1 ⋅⇩t isub_to_fsub σ) = fterm_to_iterm (t⇩2 ⋅⇩t isub_to_fsub σ)" using fterm_to_iterm_subst by auto
      then have "iterm_to_fterm (fterm_to_iterm (t⇩1 ⋅⇩t (isub_to_fsub σ))) = iterm_to_fterm (fterm_to_iterm (t⇩2 ⋅⇩t isub_to_fsub σ))" by auto
      then show "t⇩1 ⋅⇩t isub_to_fsub σ = t⇩2 ⋅⇩t isub_to_fsub σ" by auto
    qed
  then have "∀t⇩2∈ts. t' ⋅⇩t isub_to_fsub σ = t⇩2 ⋅⇩t isub_to_fsub σ" using t'_p by blast            
  then show "unifier⇩t⇩s (isub_to_fsub σ) ts" unfolding unifier⇩t⇩s_def by metis
qed

lemma icomp_fcomp: "θ ∘⇩s i = fsub_to_isub (isub_to_fsub θ ⋅ isub_to_fsub i)"
  unfolding composition_def subst_compose_def
proof
  fix x
  show "θ x ⋅ i = fterm_to_iterm (iterm_to_fterm (θ x) ⋅⇩t (λx. iterm_to_fterm (i x)))" using iterm_to_fterm_subt by auto
qed


lemma is_mgu_mgu⇩t⇩s: 
  assumes "finite ts"
  assumes "is_imgu θ (fterm_to_iterm ` ts × fterm_to_iterm ` ts)"
  shows "mgu⇩t⇩s (isub_to_fsub θ) ts"
proof -
  from assms have "unifier⇩t⇩s (isub_to_fsub θ) ts" unfolding is_imgu_def using unifiers_unifiert by auto
  moreover have "∀u. unifier⇩t⇩s u ts ⟶ (∃i. u = (isub_to_fsub θ) ⋅ i)"
    proof (rule allI; rule impI)
      fix u
      assume "unifier⇩t⇩s u ts"
      then have "fsub_to_isub u ∈ unifiers (fterm_to_iterm ` ts × fterm_to_iterm ` ts)" using unifiert_unifiers by auto
      then have "∃i. fsub_to_isub u = θ ∘⇩s i" using assms unfolding is_imgu_def by auto
      then obtain i where "fsub_to_isub u = θ ∘⇩s i" by auto 
      then have "fsub_to_isub u =  fsub_to_isub (isub_to_fsub θ ⋅ isub_to_fsub i)" using icomp_fcomp by auto
      then have "isub_to_fsub (fsub_to_isub u) = isub_to_fsub (fsub_to_isub (isub_to_fsub θ ⋅ isub_to_fsub i))" by metis
      then have "u = isub_to_fsub θ ⋅ isub_to_fsub i" by auto
      then show "∃i. u = isub_to_fsub θ ⋅ i" by metis
    qed
  ultimately show ?thesis unfolding mgu⇩t⇩s_def by auto
qed

lemma unification':
  assumes "finite ts"
  assumes  "unifier⇩t⇩s σ ts"
  shows "∃θ. mgu⇩t⇩s θ ts"
proof -
  let ?E = "fterm_to_iterm ` ts × fterm_to_iterm ` ts"
  let ?lE = "set_to_list ?E"
  from assms have "fsub_to_isub σ ∈ unifiers ?E" using unifiert_unifiers by auto
  then have "∃θ. is_imgu θ ?E"
    using unify_unification[of "fsub_to_isub σ" ?lE] assms by (simp add: set_set_to_list)
  then obtain θ where "is_imgu θ ?E" unfolding set_to_list_def by auto
  then have "mgu⇩t⇩s (isub_to_fsub θ) ts" using assms is_mgu_mgu⇩t⇩s by auto
  then show ?thesis by auto
qed

fun literal_to_term :: "fterm literal ⇒ fterm" where
  "literal_to_term (Pos p ts) = Fun ''Pos'' [Fun p ts]"
| "literal_to_term (Neg p ts) = Fun ''Neg'' [Fun p ts]"

fun term_to_literal :: "fterm ⇒ fterm literal" where
  "term_to_literal (Fun s [Fun p ts]) = (if s=''Pos'' then Pos else Neg) p ts"

lemma term_to_literal_cancel[simp]: "term_to_literal (literal_to_term l) = l"
  by (cases l) auto

lemma literal_to_term_sub: "literal_to_term (l ⋅⇩l σ) = (literal_to_term l) ⋅⇩t σ"
  by (induction l) auto


lemma unifier⇩l⇩s_unifier⇩t⇩s:
  assumes "unifier⇩l⇩s σ L"
  shows "unifier⇩t⇩s σ (literal_to_term `  L)"
proof -
  from assms obtain l' where "∀l∈L. l ⋅⇩l σ = l'" unfolding unifier⇩l⇩s_def by auto
  then have "∀l∈L. literal_to_term (l ⋅⇩l σ) = literal_to_term l'" by auto
  then have "∀l∈L. (literal_to_term l) ⋅⇩t σ = literal_to_term l'" using literal_to_term_sub by auto
  then have "∀t∈literal_to_term ` L. t ⋅⇩t σ = literal_to_term l'" by auto 
  then show ?thesis unfolding unifier⇩t⇩s_def by auto
qed

lemma unifiert_unifier⇩l⇩s:
  assumes "unifier⇩t⇩s σ (literal_to_term `  L)"
  shows "unifier⇩l⇩s σ L"
proof -
  from assms obtain t' where "∀t∈literal_to_term ` L. t ⋅⇩t σ = t'" unfolding unifier⇩t⇩s_def by auto
  then have "∀t∈literal_to_term ` L. term_to_literal (t ⋅⇩t σ) = term_to_literal t'"  by auto
  then have "∀l∈ L. term_to_literal ((literal_to_term l) ⋅⇩t σ) = term_to_literal t'" by auto
  then have "∀l∈ L. term_to_literal ((literal_to_term (l ⋅⇩l σ))) = term_to_literal t'" using literal_to_term_sub by auto
  then have "∀l∈ L. l ⋅⇩l σ = term_to_literal t'" by auto 
  then show ?thesis unfolding unifier⇩l⇩s_def by auto
qed

lemma mgu⇩t⇩s_mgu⇩l⇩s:
  assumes "mgu⇩t⇩s θ (literal_to_term `  L)"
  shows "mgu⇩l⇩s θ L"
proof -
  from assms have "unifier⇩t⇩s θ (literal_to_term `  L)" unfolding mgu⇩t⇩s_def by auto
  then have "unifier⇩l⇩s θ L" using unifiert_unifier⇩l⇩s by auto
  moreover
  {
    fix u
    assume "unifier⇩l⇩s u L"
    then have "unifier⇩t⇩s u (literal_to_term `  L)" using unifier⇩l⇩s_unifier⇩t⇩s by auto
    then have "∃i. u = θ ⋅ i" using assms unfolding mgu⇩t⇩s_def by auto
  }
  ultimately show ?thesis unfolding mgu⇩l⇩s_def by auto
qed

theorem unification:
  assumes fin: "finite L"
  assumes uni: "unifier⇩l⇩s σ L"
  shows "∃θ. mgu⇩l⇩s θ L"
proof -
  from uni have "unifier⇩t⇩s σ (literal_to_term `  L)" using unifier⇩l⇩s_unifier⇩t⇩s by auto
  then obtain θ where "mgu⇩t⇩s θ (literal_to_term `  L)" using fin unification' by blast
  then have "mgu⇩l⇩s θ L" using mgu⇩t⇩s_mgu⇩l⇩s by auto
  then show ?thesis by auto
qed

end