Theory CR.Mgu_List

(* an mgu-function for lists of pairs of terms *)

(* TODO: merge into AFP-entry *)

theory Mgu_List
imports
  First_Order_Terms.Unification
begin
text ‹Computing the mgu of a list of term pairs.›
definition mgu_list :: "(('f, 'v) term × ('f,'v) term) list ⇒ ('f, 'v) subst option" where
  "mgu_list pairs = map_option subst_of (unify pairs [])" 

lemma mgu_list_None: "mgu_list pairs = None ⟹ unifiers (set pairs) = {}"
  unfolding mgu_list_def by (intro unify_complete, auto)

lemma mgu_list_Some: "mgu_list pairs = Some τ ⟹ is_imgu τ (set pairs)" 
  unfolding mgu_list_def using unify_sound by blast
end