# HG changeset patch # User desharna # Date 1656490414 -7200 # Node ID 3ba38a1197393da7331e46c4f9211a4a913dcbe7 # Parent f5015fa7cb1909ad65b88c9cbdd5edff7e6eb6b4 added definition IMGU and lemmas IMGU_iff_Idem_and_MGU and unify_computes_IMGU diff -r f5015fa7cb19 -r 3ba38a119739 src/HOL/ex/Unification.thy --- a/src/HOL/ex/Unification.thy Tue Jun 28 17:55:30 2022 +0200 +++ b/src/HOL/ex/Unification.thy Wed Jun 29 10:13:34 2022 +0200 @@ -524,4 +524,18 @@ qed qed (auto intro!: Var_Idem split: option.splits if_splits) + +subsection \Idempotent Most General Unifier\ + +definition IMGU :: "'a subst \ 'a trm \ 'a trm \ bool" where + "IMGU \ t u \ Unifier \ t u \ (\\. Unifier \ t u \ \ \ \ \ \)" + +lemma IMGU_iff_Idem_and_MGU: "IMGU \ t u \ Idem \ \ MGU \ t u" + unfolding IMGU_def Idem_def MGU_def + by (smt (verit, best) subst_comp subst_eq_def) + +lemma unify_computes_IMGU: + "unify M N = Some \ \ IMGU \ M N" + by (simp add: IMGU_iff_Idem_and_MGU unify_computes_MGU unify_gives_Idem) + end